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 L:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (app 1 2) 0.002/0.002 (from 1) 0.002/0.002 (prefix 1) 0.002/0.002 (zWadr 1 2) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 app(cons(X:S,XS:S),YS:S) -> cons(X:S,app(XS:S,YS:S)) 0.002/0.002 app(nil,YS:S) -> YS:S 0.002/0.002 from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 zWadr(nil,YS:S) -> nil 0.002/0.002 zWadr(XS:S,nil) -> 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 L:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (app 1 2) 0.002/0.002 (from 1) 0.002/0.002 (prefix 1) 0.002/0.002 (zWadr 1 2) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 app(cons(X:S,XS:S),YS:S) -> cons(X:S,app(XS:S,YS:S)) 0.002/0.002 app(nil,YS:S) -> YS:S 0.002/0.002 from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 zWadr(nil,YS:S) -> nil 0.002/0.002 zWadr(XS:S,nil) -> 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 CS-TRS Processor: 0.002/0.002 R is a CS-TRS 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 L:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (app 1 2) 0.002/0.002 (from 1) 0.002/0.002 (prefix 1) 0.002/0.002 (zWadr 1 2) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 app(cons(X:S,XS:S),YS:S) -> cons(X:S,app(XS:S,YS:S)) 0.002/0.002 app(nil,YS:S) -> YS:S 0.002/0.002 from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 zWadr(nil,YS:S) -> nil 0.002/0.002 zWadr(XS:S,nil) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 1 (l' :-> r') => app(cons(X:S,XS:S),YS:S) -> cons(X:S,app(XS:S,YS:S)) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> app(cons(X:S,XS:S),YS:S)} 0.002/0.002 s => cons(x6:S,app(x7:S,app(cons(X:S,XS:S),YS:S))) 0.002/0.002 t => app(cons(x6:S,x7:S),cons(X:S,app(XS:S,YS:S))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 2 (l' :-> r') => app(nil,YS:S) -> YS:S 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> app(nil,YS:S)} 0.002/0.002 s => cons(x6:S,app(x7:S,app(nil,YS:S))) 0.002/0.002 t => app(cons(x6:S,x7:S),YS:S) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 3 (l' :-> r') => from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> from(X:S)} 0.002/0.002 s => cons(x6:S,app(x7:S,from(X:S))) 0.002/0.002 t => app(cons(x6:S,x7:S),cons(X:S,from(s(X:S)))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 4 (l' :-> r') => prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> prefix(L:S)} 0.002/0.002 s => cons(x6:S,app(x7:S,prefix(L:S))) 0.002/0.002 t => app(cons(x6:S,x7:S),cons(nil,zWadr(L:S,prefix(L:S)))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 5 (l' :-> r') => zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> zWadr(cons(X:S,XS:S),cons(Y:S,YS:S))} 0.002/0.002 s => cons(x6:S,app(x7:S,zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)))) 0.002/0.002 t => app(cons(x6:S,x7:S),cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 6 (l' :-> r') => zWadr(nil,YS:S) -> nil 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> zWadr(nil,YS:S)} 0.002/0.002 s => cons(x6:S,app(x7:S,zWadr(nil,YS:S))) 0.002/0.002 t => app(cons(x6:S,x7:S),nil) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)) 0.002/0.002 Rule 7 (l' :-> r') => zWadr(XS:S,nil) -> nil 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [2] 0.002/0.002 Sigma => {x8:S -> zWadr(XS:S,nil)} 0.002/0.002 s => cons(x6:S,app(x7:S,zWadr(XS:S,nil))) 0.002/0.002 t => app(cons(x6:S,x7:S),nil) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => from(x10:S) -> cons(x10:S,from(s(x10:S))) 0.002/0.002 Rule 3 (l' :-> r') => from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 Var => x10:S 0.002/0.002 Pos x10:S in l => [1] 0.002/0.002 Sigma => {x10:S -> from(X:S)} 0.002/0.002 s => cons(from(X:S),from(s(from(X:S)))) 0.002/0.002 t => from(cons(X:S,from(s(X:S)))) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => from(x10:S) -> cons(x10:S,from(s(x10:S))) 0.002/0.002 Rule 4 (l' :-> r') => prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 Var => x10:S 0.002/0.002 Pos x10:S in l => [1] 0.002/0.002 Sigma => {x10:S -> prefix(L:S)} 0.002/0.002 s => cons(prefix(L:S),from(s(prefix(L:S)))) 0.002/0.002 t => from(cons(nil,zWadr(L:S,prefix(L:S)))) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => from(x10:S) -> cons(x10:S,from(s(x10:S))) 0.002/0.002 Rule 5 (l' :-> r') => zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 Var => x10:S 0.002/0.002 Pos x10:S in l => [1] 0.002/0.002 Sigma => {x10:S -> zWadr(cons(X:S,XS:S),cons(Y:S,YS:S))} 0.002/0.002 s => cons(zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)),from(s(zWadr(cons(X:S,XS:S),cons(Y:S,YS:S))))) 0.002/0.002 t => from(cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S))) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => from(x10:S) -> cons(x10:S,from(s(x10:S))) 0.002/0.002 Rule 6 (l' :-> r') => zWadr(nil,YS:S) -> nil 0.002/0.002 Var => x10:S 0.002/0.002 Pos x10:S in l => [1] 0.002/0.002 Sigma => {x10:S -> zWadr(nil,YS:S)} 0.002/0.002 s => cons(zWadr(nil,YS:S),from(s(zWadr(nil,YS:S)))) 0.002/0.002 t => from(nil) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => from(x10:S) -> cons(x10:S,from(s(x10:S))) 0.002/0.002 Rule 7 (l' :-> r') => zWadr(XS:S,nil) -> nil 0.002/0.002 Var => x10:S 0.002/0.002 Pos x10:S in l => [1] 0.002/0.002 Sigma => {x10:S -> zWadr(XS:S,nil)} 0.002/0.002 s => cons(zWadr(XS:S,nil),from(s(zWadr(XS:S,nil)))) 0.002/0.002 t => from(nil) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => prefix(x11:S) -> cons(nil,zWadr(x11:S,prefix(x11:S))) 0.002/0.002 Rule 4 (l' :-> r') => prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 Var => x11:S 0.002/0.002 Pos x11:S in l => [1] 0.002/0.002 Sigma => {x11:S -> prefix(L:S)} 0.002/0.002 s => cons(nil,zWadr(prefix(L:S),prefix(prefix(L:S)))) 0.002/0.002 t => prefix(cons(nil,zWadr(L:S,prefix(L:S)))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => prefix(x11:S) -> cons(nil,zWadr(x11:S,prefix(x11:S))) 0.002/0.002 Rule 5 (l' :-> r') => zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 Var => x11:S 0.002/0.002 Pos x11:S in l => [1] 0.002/0.002 Sigma => {x11:S -> zWadr(cons(X:S,XS:S),cons(Y:S,YS:S))} 0.002/0.002 s => cons(nil,zWadr(zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)),prefix(zWadr(cons(X:S,XS:S),cons(Y:S,YS:S))))) 0.002/0.002 t => prefix(cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => prefix(x11:S) -> cons(nil,zWadr(x11:S,prefix(x11:S))) 0.002/0.002 Rule 6 (l' :-> r') => zWadr(nil,YS:S) -> nil 0.002/0.002 Var => x11:S 0.002/0.002 Pos x11:S in l => [1] 0.002/0.002 Sigma => {x11:S -> zWadr(nil,YS:S)} 0.002/0.002 s => cons(nil,zWadr(zWadr(nil,YS:S),prefix(zWadr(nil,YS:S)))) 0.002/0.002 t => prefix(nil) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => prefix(x11:S) -> cons(nil,zWadr(x11:S,prefix(x11:S))) 0.002/0.002 Rule 7 (l' :-> r') => zWadr(XS:S,nil) -> nil 0.002/0.002 Var => x11:S 0.002/0.002 Pos x11:S in l => [1] 0.002/0.002 Sigma => {x11:S -> zWadr(XS:S,nil)} 0.002/0.002 s => cons(nil,zWadr(zWadr(XS:S,nil),prefix(zWadr(XS:S,nil)))) 0.002/0.002 t => prefix(nil) 0.002/0.002 NW => 1 0.002/0.002 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 L:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (app 1 2) 0.002/0.002 (from 1) 0.002/0.002 (prefix 1) 0.002/0.002 (zWadr 1 2) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 app(cons(X:S,XS:S),YS:S) -> cons(X:S,app(XS:S,YS:S)) 0.002/0.002 app(nil,YS:S) -> YS:S 0.002/0.002 from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 zWadr(nil,YS:S) -> nil 0.002/0.002 zWadr(XS:S,nil) -> nil 0.002/0.002 ) 0.002/0.002 Critical Pairs: 0.002/0.002 => Not trivial, Not overlay, NW1, N1 0.002/0.002 => Not trivial, Not overlay, NW1, N2 0.002/0.002 => Not trivial, Not overlay, NW1, N3 0.002/0.002 => Not trivial, Not overlay, NW1, N4 0.002/0.002 => Not trivial, Not overlay, NW1, N5 0.002/0.002 => Not trivial, Not overlay, NW1, N6 0.002/0.002 => Not trivial, Not overlay, NW1, N7 0.002/0.002 => Not trivial, Not overlay, NW0, N8 0.002/0.002 => Not trivial, Not overlay, NW0, N9 0.002/0.002 => Not trivial, Not overlay, NW0, N10 0.002/0.002 => Not trivial, Not overlay, NW0, N11 0.002/0.002 => Not trivial, Not overlay, NW0, N12 0.002/0.002 => Not trivial, Not overlay, NW1, N13 0.002/0.002 => Not trivial, Not overlay, NW1, N14 0.002/0.002 => Not trivial, Not overlay, NW1, N15 0.002/0.002 => Not trivial, Not overlay, NW1, N16 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 app(cons(X:S,XS:S),YS:S) -> cons(X:S,app(XS:S,YS:S)) 0.002/0.002 app(nil,YS:S) -> YS:S 0.002/0.002 from(X:S) -> cons(X:S,from(s(X:S))) 0.002/0.002 prefix(L:S) -> cons(nil,zWadr(L:S,prefix(L:S))) 0.002/0.002 zWadr(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(app(Y:S,cons(X:S,nil)),zWadr(XS:S,YS:S)) 0.002/0.002 zWadr(nil,YS:S) -> nil 0.002/0.002 zWadr(XS:S,nil) -> nil 0.002/0.002 -> Vars: 0.002/0.002 X, XS, YS, YS, X, L, X, XS, Y, YS, YS, XS 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [X, YS], UV-RActive: [X], UV-LFrozen: [XS], UV-RFrozen: [XS, YS]) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [YS], UV-RActive: [YS], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: [X]) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [L], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [L]) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [X, Y], UV-RActive: [X, Y], UV-LFrozen: [XS, YS], UV-RFrozen: [XS, YS]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [YS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 -> FVars: 0.002/0.002 x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17 0.002/0.002 -> PVars: 0.002/0.002 X: [x6, x10, x12], XS: [x7, x13, x17], YS: [x8, x9, x15, x16], L: [x11], Y: [x14] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: app(cons(x6:S,x7:S),x8:S) -> cons(x6:S,app(x7:S,x8:S)), id: 1, possubterms: app(cons(x6:S,x7:S),x8:S)->[], cons(x6:S,x7:S)->[1]) 0.002/0.002 (rule: app(nil,x9:S) -> x9:S, id: 2, possubterms: app(nil,x9:S)->[], nil->[1]) 0.002/0.002 (rule: from(x10:S) -> cons(x10:S,from(s(x10:S))), id: 3, possubterms: from(x10:S)->[]) 0.002/0.002 (rule: prefix(x11:S) -> cons(nil,zWadr(x11:S,prefix(x11:S))), id: 4, possubterms: prefix(x11:S)->[]) 0.002/0.002 (rule: zWadr(cons(x12:S,x13:S),cons(x14:S,x15:S)) -> cons(app(x14:S,cons(x12:S,nil)),zWadr(x13:S,x15:S)), id: 5, possubterms: zWadr(cons(x12:S,x13:S),cons(x14:S,x15:S))->[], cons(x12:S,x13:S)->[1], cons(x14:S,x15:S)->[2]) 0.002/0.002 (rule: zWadr(nil,x16:S) -> nil, id: 6, possubterms: zWadr(nil,x16:S)->[], nil->[1]) 0.002/0.002 (rule: zWadr(x17:S,nil) -> nil, id: 7, possubterms: zWadr(x17:S,nil)->[], nil->[2]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R7 unifies with R6 at p: [], l: zWadr(x17:S,nil), lp: zWadr(x17:S,nil), sig: {YS:S -> nil,x17:S -> nil}, l': zWadr(nil,YS:S), r: nil, r': nil) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW1, N1 0.002/0.002 => Not trivial, Not overlay, NW1, N2 0.002/0.002 => Not trivial, Not overlay, NW1, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 => Trivial, Overlay, NW0, N5 0.002/0.002 => Not trivial, Not overlay, NW0, N6 0.002/0.002 => Not trivial, Not overlay, NW0, N7 0.002/0.002 => Not trivial, Not overlay, NW1, N8 0.002/0.002 => Not trivial, Not overlay, NW1, N9 0.002/0.002 => Not trivial, Not overlay, NW1, N10 0.002/0.002 => Not trivial, Not overlay, NW1, N11 0.002/0.002 => Not trivial, Not overlay, NW0, N12 0.002/0.002 => Not trivial, Not overlay, NW0, N13 0.002/0.002 => Not trivial, Not overlay, NW1, N14 0.002/0.002 => Not trivial, Not overlay, NW1, N15 0.002/0.002 => Not trivial, Not overlay, NW1, N16 0.002/0.002 => Not trivial, Not overlay, NW1, N17 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, Not 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: cons(X:S,app(XS:S,app(nil,YS:S))) 0.002/0.002 Nodes: [0] 0.002/0.002 Edges: [] 0.002/0.002 ID: 0 => ('cons(X:S,app(XS:S,app(nil,YS:S)))', D0) 0.002/0.002 t: app(cons(X:S,XS:S),YS:S) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('app(cons(X:S,XS:S),YS:S)', D0) 0.002/0.002 ID: 1 => ('cons(X:S,app(XS:S,YS:S))', D1, R1, P[], S{x6:S -> X:S, x7:S -> XS:S, x8:S -> YS:S}), NR: 'cons(X:S,app(XS:S,YS:S))' 0.002/0.002 cons(X:S,app(XS:S,app(nil,YS:S))) ->* no union *<- app(cons(X:S,XS:S),YS: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 58%CPU (0avgtext+0avgdata 10728maxresident)k 0.002/0.002 0inputs+0outputs (0major+1133minor)pagefaults 0swaps