0.002/0.002 NO 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S v_NonEmpty:S:S X:S:S Y:S:S Z:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (fcons) 0.002/0.002 (first 1 2) 0.002/0.002 (first1 1 2) 0.002/0.002 (from) 0.002/0.002 (quote 1) 0.002/0.002 (quote1 1) 0.002/0.002 (sel 1 2) 0.002/0.002 (sel1 1 2) 0.002/0.002 (unquote 1) 0.002/0.002 (unquote1 1) 0.002/0.002 (cons) 0.002/0.002 (cons1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (nil1) 0.002/0.002 (num0) 0.002/0.002 (num01) 0.002/0.002 (s) 0.002/0.002 (s1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 fcons(X:S:S,Z:S:S) -> cons(X:S:S,Z:S:S) 0.002/0.002 first(num0,Z:S:S) -> nil 0.002/0.002 first(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons(Y:S:S,first(X:S:S,Z:S:S)) 0.002/0.002 first1(num0,Z:S:S) -> nil1 0.002/0.002 first1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons1(quote(Y:S:S),first1(X:S:S,Z:S:S)) 0.002/0.002 from(X:S:S) -> cons(X:S:S,from(s(X:S:S))) 0.002/0.002 quote(sel(X:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 quote(num0) -> num01 0.002/0.002 quote(s(X:S:S)) -> s1(quote(X:S:S)) 0.002/0.002 quote1(first(X:S:S,Z:S:S)) -> first1(X:S:S,Z:S:S) 0.002/0.002 quote1(cons(X:S:S,Z:S:S)) -> cons1(quote(X:S:S),quote1(Z:S:S)) 0.002/0.002 quote1(nil) -> nil1 0.002/0.002 sel(num0,cons(X:S:S,Z:S:S)) -> X:S:S 0.002/0.002 sel(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel(X:S:S,Z:S:S) 0.002/0.002 sel1(num0,cons(X:S:S,Z:S:S)) -> quote(X:S:S) 0.002/0.002 sel1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 unquote(num01) -> num0 0.002/0.002 unquote(s1(X:S:S)) -> s(unquote(X:S:S)) 0.002/0.002 unquote1(cons1(X:S:S,Z:S:S)) -> fcons(unquote(X:S:S),unquote1(Z:S:S)) 0.002/0.002 unquote1(nil1) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 CleanTRS Processor: 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S v_NonEmpty:S:S X:S:S Y:S:S Z:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (fcons) 0.002/0.002 (first 1 2) 0.002/0.002 (first1 1 2) 0.002/0.002 (from) 0.002/0.002 (quote 1) 0.002/0.002 (quote1 1) 0.002/0.002 (sel 1 2) 0.002/0.002 (sel1 1 2) 0.002/0.002 (unquote 1) 0.002/0.002 (unquote1 1) 0.002/0.002 (cons) 0.002/0.002 (cons1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (nil1) 0.002/0.002 (num0) 0.002/0.002 (num01) 0.002/0.002 (s) 0.002/0.002 (s1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 fcons(X:S:S,Z:S:S) -> cons(X:S:S,Z:S:S) 0.002/0.002 first(num0,Z:S:S) -> nil 0.002/0.002 first(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons(Y:S:S,first(X:S:S,Z:S:S)) 0.002/0.002 first1(num0,Z:S:S) -> nil1 0.002/0.002 first1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons1(quote(Y:S:S),first1(X:S:S,Z:S:S)) 0.002/0.002 from(X:S:S) -> cons(X:S:S,from(s(X:S:S))) 0.002/0.002 quote(sel(X:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 quote(num0) -> num01 0.002/0.002 quote(s(X:S:S)) -> s1(quote(X:S:S)) 0.002/0.002 quote1(first(X:S:S,Z:S:S)) -> first1(X:S:S,Z:S:S) 0.002/0.002 quote1(cons(X:S:S,Z:S:S)) -> cons1(quote(X:S:S),quote1(Z:S:S)) 0.002/0.002 quote1(nil) -> nil1 0.002/0.002 sel(num0,cons(X:S:S,Z:S:S)) -> X:S:S 0.002/0.002 sel(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel(X:S:S,Z:S:S) 0.002/0.002 sel1(num0,cons(X:S:S,Z:S:S)) -> quote(X:S:S) 0.002/0.002 sel1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 unquote(num01) -> num0 0.002/0.002 unquote(s1(X:S:S)) -> s(unquote(X:S:S)) 0.002/0.002 unquote1(cons1(X:S:S,Z:S:S)) -> fcons(unquote(X:S:S),unquote1(Z:S:S)) 0.002/0.002 unquote1(nil1) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 Modular Confluence Combinations Decomposition Processor: 0.002/0.002 It is a CTRS -> No modular confluence 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 Left-Homogeneous u-Replacing Variables Processor: 0.002/0.002 R satisfies LHRV condition 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S v_NonEmpty:S:S X:S:S Y:S:S Z:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (fcons) 0.002/0.002 (first 1 2) 0.002/0.002 (first1 1 2) 0.002/0.002 (from) 0.002/0.002 (quote 1) 0.002/0.002 (quote1 1) 0.002/0.002 (sel 1 2) 0.002/0.002 (sel1 1 2) 0.002/0.002 (unquote 1) 0.002/0.002 (unquote1 1) 0.002/0.002 (cons) 0.002/0.002 (cons1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (nil1) 0.002/0.002 (num0) 0.002/0.002 (num01) 0.002/0.002 (s) 0.002/0.002 (s1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 fcons(X:S:S,Z:S:S) -> cons(X:S:S,Z:S:S) 0.002/0.002 first(num0,Z:S:S) -> nil 0.002/0.002 first(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons(Y:S:S,first(X:S:S,Z:S:S)) 0.002/0.002 first1(num0,Z:S:S) -> nil1 0.002/0.002 first1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons1(quote(Y:S:S),first1(X:S:S,Z:S:S)) 0.002/0.002 from(X:S:S) -> cons(X:S:S,from(s(X:S:S))) 0.002/0.002 quote(sel(X:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 quote(num0) -> num01 0.002/0.002 quote(s(X:S:S)) -> s1(quote(X:S:S)) 0.002/0.002 quote1(first(X:S:S,Z:S:S)) -> first1(X:S:S,Z:S:S) 0.002/0.002 quote1(cons(X:S:S,Z:S:S)) -> cons1(quote(X:S:S),quote1(Z:S:S)) 0.002/0.002 quote1(nil) -> nil1 0.002/0.002 sel(num0,cons(X:S:S,Z:S:S)) -> X:S:S 0.002/0.002 sel(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel(X:S:S,Z:S:S) 0.002/0.002 sel1(num0,cons(X:S:S,Z:S:S)) -> quote(X:S:S) 0.002/0.002 sel1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 unquote(num01) -> num0 0.002/0.002 unquote(s1(X:S:S)) -> s(unquote(X:S:S)) 0.002/0.002 unquote1(cons1(X:S:S,Z:S:S)) -> fcons(unquote(X:S:S),unquote1(Z:S:S)) 0.002/0.002 unquote1(nil1) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 fcons(X:S:S,Z:S:S) -> cons(X:S:S,Z:S:S) 0.002/0.002 first(num0,Z:S:S) -> nil 0.002/0.002 first(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons(Y:S:S,first(X:S:S,Z:S:S)) 0.002/0.002 first1(num0,Z:S:S) -> nil1 0.002/0.002 first1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> cons1(quote(Y:S:S),first1(X:S:S,Z:S:S)) 0.002/0.002 from(X:S:S) -> cons(X:S:S,from(s(X:S:S))) 0.002/0.002 quote(sel(X:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 quote(num0) -> num01 0.002/0.002 quote(s(X:S:S)) -> s1(quote(X:S:S)) 0.002/0.002 quote1(first(X:S:S,Z:S:S)) -> first1(X:S:S,Z:S:S) 0.002/0.002 quote1(cons(X:S:S,Z:S:S)) -> cons1(quote(X:S:S),quote1(Z:S:S)) 0.002/0.002 quote1(nil) -> nil1 0.002/0.002 sel(num0,cons(X:S:S,Z:S:S)) -> X:S:S 0.002/0.002 sel(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel(X:S:S,Z:S:S) 0.002/0.002 sel1(num0,cons(X:S:S,Z:S:S)) -> quote(X:S:S) 0.002/0.002 sel1(s(X:S:S),cons(Y:S:S,Z:S:S)) -> sel1(X:S:S,Z:S:S) 0.002/0.002 unquote(num01) -> num0 0.002/0.002 unquote(s1(X:S:S)) -> s(unquote(X:S:S)) 0.002/0.002 unquote1(cons1(X:S:S,Z:S:S)) -> fcons(unquote(X:S:S),unquote1(Z:S:S)) 0.002/0.002 unquote1(nil1) -> nil 0.002/0.002 -> Vars: 0.002/0.002 X:S, Z:S, Z:S, X:S, Y:S, Z:S, Z:S, X:S, Y:S, Z:S, X:S, X:S, Z:S, X:S, X:S, Z:S, X:S, Z:S, X:S, Z:S, X:S, Y:S, Z:S, X:S, Z:S, X:S, Y:S, Z:S, X:S, X:S, Z:S 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, Z:S], UV-RFrozen: [X:S, Z:S]) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [Z:S], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, Y:S, Z:S], UV-RFrozen: [X:S, Y:S, Z:S]) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [Z:S], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, Y:S, Z:S], UV-RFrozen: [X:S, Y:S, Z:S]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S], UV-RFrozen: [X:S]) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [X:S, Z:S], UV-RActive: [X:S, Z:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S], UV-RFrozen: [X:S]) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [X:S, Z:S], UV-RActive: [X:S, Z:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, Z:S], UV-RFrozen: [X:S, Z:S]) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Z:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [X:S, Z:S], UV-LFrozen: [X:S, Y:S, Z:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Z:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [X:S, Z:S], UV-LFrozen: [X:S, Y:S, Z:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S], UV-RFrozen: [X:S]) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, Z:S], UV-RFrozen: [X:S, Z:S]) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 -> FVars: 0.002/0.002 x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35 0.002/0.002 -> PVars: 0.002/0.002 X:S: [x5, x8, x12, x15, x16, x18, x19, x21, x23, x25, x28, x30, x33, x34], Z:S: [x6, x7, x10, x11, x14, x17, x20, x22, x24, x27, x29, x32, x35], Y:S: [x9, x13, x26, x31] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: fcons(x5:S,x6:S) -> cons(x5:S,x6:S), id: 1, possubterms: fcons(x5:S,x6:S)->[]) 0.002/0.002 (rule: first(num0,x7:S) -> nil, id: 2, possubterms: first(num0,x7:S)->[], num0->[1]) 0.002/0.002 (rule: first(s(x8:S),cons(x9:S,x10:S)) -> cons(x9:S,first(x8:S,x10:S)), id: 3, possubterms: first(s(x8:S),cons(x9:S,x10:S))->[], s(x8:S)->[1], cons(x9:S,x10:S)->[2]) 0.002/0.002 (rule: first1(num0,x11:S) -> nil1, id: 4, possubterms: first1(num0,x11:S)->[], num0->[1]) 0.002/0.002 (rule: first1(s(x12:S),cons(x13:S,x14:S)) -> cons1(quote(x13:S),first1(x12:S,x14:S)), id: 5, possubterms: first1(s(x12:S),cons(x13:S,x14:S))->[], s(x12:S)->[1], cons(x13:S,x14:S)->[2]) 0.002/0.002 (rule: from(x15:S) -> cons(x15:S,from(s(x15:S))), id: 6, possubterms: from(x15:S)->[]) 0.002/0.002 (rule: quote(sel(x16:S,x17:S)) -> sel1(x16:S,x17:S), id: 7, possubterms: quote(sel(x16:S,x17:S))->[], sel(x16:S,x17:S)->[1]) 0.002/0.002 (rule: quote(num0) -> num01, id: 8, possubterms: quote(num0)->[], num0->[1]) 0.002/0.002 (rule: quote(s(x18:S)) -> s1(quote(x18:S)), id: 9, possubterms: quote(s(x18:S))->[], s(x18:S)->[1]) 0.002/0.002 (rule: quote1(first(x19:S,x20:S)) -> first1(x19:S,x20:S), id: 10, possubterms: quote1(first(x19:S,x20:S))->[], first(x19:S,x20:S)->[1]) 0.002/0.002 (rule: quote1(cons(x21:S,x22:S)) -> cons1(quote(x21:S),quote1(x22:S)), id: 11, possubterms: quote1(cons(x21:S,x22:S))->[], cons(x21:S,x22:S)->[1]) 0.002/0.002 (rule: quote1(nil) -> nil1, id: 12, possubterms: quote1(nil)->[], nil->[1]) 0.002/0.002 (rule: sel(num0,cons(x23:S,x24:S)) -> x23:S, id: 13, possubterms: sel(num0,cons(x23:S,x24:S))->[], num0->[1], cons(x23:S,x24:S)->[2]) 0.002/0.002 (rule: sel(s(x25:S),cons(x26:S,x27:S)) -> sel(x25:S,x27:S), id: 14, possubterms: sel(s(x25:S),cons(x26:S,x27:S))->[], s(x25:S)->[1], cons(x26:S,x27:S)->[2]) 0.002/0.002 (rule: sel1(num0,cons(x28:S,x29:S)) -> quote(x28:S), id: 15, possubterms: sel1(num0,cons(x28:S,x29:S))->[], num0->[1], cons(x28:S,x29:S)->[2]) 0.002/0.002 (rule: sel1(s(x30:S),cons(x31:S,x32:S)) -> sel1(x30:S,x32:S), id: 16, possubterms: sel1(s(x30:S),cons(x31:S,x32:S))->[], s(x30:S)->[1], cons(x31:S,x32:S)->[2]) 0.002/0.002 (rule: unquote(num01) -> num0, id: 17, possubterms: unquote(num01)->[], num01->[1]) 0.002/0.002 (rule: unquote(s1(x33:S)) -> s(unquote(x33:S)), id: 18, possubterms: unquote(s1(x33:S))->[], s1(x33:S)->[1]) 0.002/0.002 (rule: unquote1(cons1(x34:S,x35:S)) -> fcons(unquote(x34:S),unquote1(x35:S)), id: 19, possubterms: unquote1(cons1(x34:S,x35:S))->[], cons1(x34:S,x35:S)->[1]) 0.002/0.002 (rule: unquote1(nil1) -> nil, id: 20, possubterms: unquote1(nil1)->[], nil1->[1]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R7 unifies with R13 at p: [1], l: quote(sel(x16:S,x17:S)), lp: sel(x16:S,x17:S), sig: {x16:S -> num0,x17:S -> cons(X:S:S,Z:S:S)}, l': sel(num0,cons(X:S:S,Z:S:S)), r: sel1(x16:S,x17:S), r': X:S:S) 0.002/0.002 (R7 unifies with R14 at p: [1], l: quote(sel(x16:S,x17:S)), lp: sel(x16:S,x17:S), sig: {x16:S -> s(X:S:S),x17:S -> cons(Y:S:S,Z:S:S)}, l': sel(s(X:S:S),cons(Y:S:S,Z:S:S)), r: sel1(x16:S,x17:S), r': sel(X:S:S,Z:S:S)) 0.002/0.002 (R10 unifies with R2 at p: [1], l: quote1(first(x19:S,x20:S)), lp: first(x19:S,x20:S), sig: {x19:S -> num0,x20:S -> Z:S:S}, l': first(num0,Z:S:S), r: first1(x19:S,x20:S), r': nil) 0.002/0.002 (R10 unifies with R3 at p: [1], l: quote1(first(x19:S,x20:S)), lp: first(x19:S,x20:S), sig: {x19:S -> s(X:S:S),x20:S -> cons(Y:S:S,Z:S:S)}, l': first(s(X:S:S),cons(Y:S:S,Z:S:S)), r: first1(x19:S,x20:S), r': cons(Y:S:S,first(X:S:S,Z:S:S))) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW0, N1 0.002/0.002 => Not trivial, Not overlay, NW0, N2 0.002/0.002 => Not trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 0.002/0.002 -> Problem conclusions: 0.002/0.002 Left linear, Not right linear, Not linear 0.002/0.002 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.002/0.002 Not Huet-Levy confluent, Not Newman confluent 0.002/0.002 R is a CS-TRS, Left-homogeneous u-replacing variables 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 No Convergence Brute Force Processor: 0.002/0.002 -> Rewritings: 0.002/0.002 s: quote1(cons(Y:S:S,first(X:S:S,Z:S:S))) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('quote1(cons(Y:S:S,first(X:S:S,Z:S:S)))', D0) 0.002/0.002 ID: 1 => ('cons1(quote(Y:S:S),quote1(first(X:S:S,Z:S:S)))', D1, R11, P[], S{x21:S -> Y:S:S, x22:S -> first(X:S:S,Z:S:S)}), NR: 'cons1(quote(Y:S:S),quote1(first(X:S:S,Z:S:S)))' 0.002/0.002 t: first1(s(X:S:S),cons(Y:S:S,Z:S:S)) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('first1(s(X:S:S),cons(Y:S:S,Z:S:S))', D0) 0.002/0.002 ID: 1 => ('cons1(quote(Y:S:S),first1(X:S:S,Z:S:S))', D1, R5, P[], S{x12:S -> X:S:S, x13:S -> Y:S:S, x14:S -> Z:S:S}), NR: 'cons1(quote(Y:S:S),first1(X:S:S,Z:S:S))' 0.002/0.002 quote1(cons(Y:S:S,first(X:S:S,Z:S:S))) ->* no union *<- first1(s(X:S:S),cons(Y:S:S,Z:S:S)) 0.002/0.002 "Not joinable" 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.00user 0.00system 0:00.02elapsed 60%CPU (0avgtext+0avgdata 10668maxresident)k 0.002/0.002 8inputs+0outputs (0major+978minor)pagefaults 0swaps