0.001/0.001 NO 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S v_NonEmpty:S:S x:S:S x0:S:S y:S:S z:S:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (*top*_0 1) 0.001/0.001 (cons_0 1 2) 0.001/0.001 (cons_1 2) 0.001/0.001 (s_0 1) 0.001/0.001 (big_0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (inf_1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 *top*_0(inf_1(x:S:S)) -> *top*_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_0(inf_1(x:S:S),x0:S:S) -> cons_0(cons_0(x:S:S,inf_1(s_0(x:S:S))),x0:S:S) 0.001/0.001 cons_0(x0:S:S,inf_1(x:S:S)) -> cons_1(x0:S:S,cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_1(x:S:S,cons_0(y:S:S,z:S:S)) -> big_0 0.001/0.001 cons_1(x:S:S,cons_1(y:S:S,z:S:S)) -> big_0 0.001/0.001 s_0(inf_1(x:S:S)) -> s_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 CleanTRS Processor: 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S v_NonEmpty:S:S x:S:S x0:S:S y:S:S z:S:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (*top*_0 1) 0.001/0.001 (cons_0 1 2) 0.001/0.001 (cons_1 2) 0.001/0.001 (s_0 1) 0.001/0.001 (big_0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (inf_1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 *top*_0(inf_1(x:S:S)) -> *top*_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_0(inf_1(x:S:S),x0:S:S) -> cons_0(cons_0(x:S:S,inf_1(s_0(x:S:S))),x0:S:S) 0.001/0.001 cons_0(x0:S:S,inf_1(x:S:S)) -> cons_1(x0:S:S,cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_1(x:S:S,cons_0(y:S:S,z:S:S)) -> big_0 0.001/0.001 cons_1(x:S:S,cons_1(y:S:S,z:S:S)) -> big_0 0.001/0.001 s_0(inf_1(x:S:S)) -> s_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 Modular Confluence Combinations Decomposition Processor: 0.001/0.001 It is a CTRS -> No modular confluence 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 CS-TRS Processor: 0.001/0.001 R is a CS-TRS 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S v_NonEmpty:S:S x:S:S x0:S:S y:S:S z:S:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (*top*_0 1) 0.001/0.001 (cons_0 1 2) 0.001/0.001 (cons_1 2) 0.001/0.001 (s_0 1) 0.001/0.001 (big_0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (inf_1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 *top*_0(inf_1(x:S:S)) -> *top*_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_0(inf_1(x:S:S),x0:S:S) -> cons_0(cons_0(x:S:S,inf_1(s_0(x:S:S))),x0:S:S) 0.001/0.001 cons_0(x0:S:S,inf_1(x:S:S)) -> cons_1(x0:S:S,cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_1(x:S:S,cons_0(y:S:S,z:S:S)) -> big_0 0.001/0.001 cons_1(x:S:S,cons_1(y:S:S,z:S:S)) -> big_0 0.001/0.001 s_0(inf_1(x:S:S)) -> s_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 Huet Levy Processor: 0.001/0.001 -> Rules: 0.001/0.001 *top*_0(inf_1(x:S:S)) -> *top*_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_0(inf_1(x:S:S),x0:S:S) -> cons_0(cons_0(x:S:S,inf_1(s_0(x:S:S))),x0:S:S) 0.001/0.001 cons_0(x0:S:S,inf_1(x:S:S)) -> cons_1(x0:S:S,cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 cons_1(x:S:S,cons_0(y:S:S,z:S:S)) -> big_0 0.001/0.001 cons_1(x:S:S,cons_1(y:S:S,z:S:S)) -> big_0 0.001/0.001 s_0(inf_1(x:S:S)) -> s_0(cons_0(x:S:S,inf_1(s_0(x:S:S)))) 0.001/0.001 -> Vars: 0.001/0.001 x:S, x:S, x0:S, x:S, x0:S, x:S, y:S, z:S, x:S, y:S, z:S, x:S 0.001/0.001 -> UVars: 0.001/0.001 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [x:S], UV-LFrozen: [x:S], UV-RFrozen: [x:S]) 0.001/0.001 (UV-RuleId: 2, UV-LActive: [x0:S], UV-RActive: [x:S, x0:S], UV-LFrozen: [x:S], UV-RFrozen: [x:S]) 0.001/0.001 (UV-RuleId: 3, UV-LActive: [x0:S], UV-RActive: [x:S], UV-LFrozen: [x:S], UV-RFrozen: [x:S, x0:S]) 0.001/0.001 (UV-RuleId: 4, UV-LActive: [y:S, z:S], UV-RActive: [], UV-LFrozen: [x:S], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 5, UV-LActive: [z:S], UV-RActive: [], UV-LFrozen: [x:S, y:S], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [x:S], UV-LFrozen: [x:S], UV-RFrozen: [x:S]) 0.001/0.001 -> FVars: 0.001/0.001 x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17 0.001/0.001 -> PVars: 0.001/0.001 x:S: [x6, x7, x9, x11, x14, x17], x0:S: [x8, x10], y:S: [x12, x15], z:S: [x13, x16] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 (rule: *top*_0(inf_1(x6:S)) -> *top*_0(cons_0(x6:S,inf_1(s_0(x6:S)))), id: 1, possubterms: *top*_0(inf_1(x6:S))->[], inf_1(x6:S)->[1]) 0.001/0.001 (rule: cons_0(inf_1(x7:S),x8:S) -> cons_0(cons_0(x7:S,inf_1(s_0(x7:S))),x8:S), id: 2, possubterms: cons_0(inf_1(x7:S),x8:S)->[], inf_1(x7:S)->[1]) 0.001/0.001 (rule: cons_0(x10:S,inf_1(x9:S)) -> cons_1(x10:S,cons_0(x9:S,inf_1(s_0(x9:S)))), id: 3, possubterms: cons_0(x10:S,inf_1(x9:S))->[], inf_1(x9:S)->[2]) 0.001/0.001 (rule: cons_1(x11:S,cons_0(x12:S,x13:S)) -> big_0, id: 4, possubterms: cons_1(x11:S,cons_0(x12:S,x13:S))->[], cons_0(x12:S,x13:S)->[2]) 0.001/0.001 (rule: cons_1(x14:S,cons_1(x15:S,x16:S)) -> big_0, id: 5, possubterms: cons_1(x14:S,cons_1(x15:S,x16:S))->[], cons_1(x15:S,x16:S)->[2]) 0.001/0.001 (rule: s_0(inf_1(x17:S)) -> s_0(cons_0(x17:S,inf_1(s_0(x17:S)))), id: 6, possubterms: s_0(inf_1(x17:S))->[], inf_1(x17:S)->[1]) 0.001/0.001 0.001/0.001 -> Unifications: 0.001/0.001 (R3 unifies with R2 at p: [], l: cons_0(x10:S,inf_1(x9:S)), lp: cons_0(x10:S,inf_1(x9:S)), sig: {x0:S:S -> inf_1(x9:S),x10:S -> inf_1(x:S:S)}, l': cons_0(inf_1(x:S:S),x0:S:S), r: cons_1(x10:S,cons_0(x9:S,inf_1(s_0(x9:S)))), r': cons_0(cons_0(x:S:S,inf_1(s_0(x:S:S))),x0:S:S)) 0.001/0.001 (R4 unifies with R2 at p: [2], l: cons_1(x11:S,cons_0(x12:S,x13:S)), lp: cons_0(x12:S,x13:S), sig: {x12:S -> inf_1(x:S:S),x13:S -> x0:S:S}, l': cons_0(inf_1(x:S:S),x0:S:S), r: big_0, r': cons_0(cons_0(x:S:S,inf_1(s_0(x:S:S))),x0:S:S)) 0.001/0.001 (R4 unifies with R3 at p: [2], l: cons_1(x11:S,cons_0(x12:S,x13:S)), lp: cons_0(x12:S,x13:S), sig: {x12:S -> x0:S:S,x13:S -> inf_1(x:S:S)}, l': cons_0(x0:S:S,inf_1(x:S:S)), r: big_0, r': cons_1(x0:S:S,cons_0(x:S:S,inf_1(s_0(x:S:S))))) 0.001/0.001 (R5 unifies with R4 at p: [2], l: cons_1(x14:S,cons_1(x15:S,x16:S)), lp: cons_1(x15:S,x16:S), sig: {x15:S -> x:S:S,x16:S -> cons_0(y:S:S,z:S:S)}, l': cons_1(x:S:S,cons_0(y:S:S,z:S:S)), r: big_0, r': big_0) 0.001/0.001 (R5 unifies with R5 at p: [2], l: cons_1(x14:S,cons_1(x15:S,x16:S)), lp: cons_1(x15:S,x16:S), sig: {x15:S -> x:S:S,x16:S -> cons_1(y:S:S,z:S:S)}, l': cons_1(x:S:S,cons_1(y:S:S,z:S:S)), r: big_0, r': big_0) 0.001/0.001 0.001/0.001 -> Critical pairs info: 0.001/0.001 => Not trivial, Not overlay, NW0, N1 0.001/0.001 => Not trivial, Not overlay, NW0, N2 0.001/0.001 => Not trivial, Not overlay, NW0, N3 0.001/0.001 => Not trivial, Not overlay, NW0, N4 0.001/0.001 => Not trivial, Overlay, NW0, N5 0.001/0.001 0.001/0.001 -> Problem conclusions: 0.001/0.001 Left linear, Not right linear, Not linear 0.001/0.001 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.001/0.001 Not Huet-Levy confluent, Not Newman confluent 0.001/0.001 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 Different Normal CP Terms Processor: 0.001/0.001 => Not trivial, Not overlay, NW0, N3, Normal and not trivial cp 0.001/0.001 0.001/0.001 The problem is not joinable. 0.001/0.001 0.01user 0.00system 0:00.01elapsed 91%CPU (0avgtext+0avgdata 10220maxresident)k 0.001/0.001 8inputs+0outputs (0major+856minor)pagefaults 0swaps