0.019/0.019 NO 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 0.019/0.019 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 Confluence Problem: 0.019/0.019 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S ZS:S) 0.019/0.019 (STRATEGY CONTEXTSENSITIVE 0.019/0.019 (U11 1) 0.019/0.019 (U12 1) 0.019/0.019 (U21 1) 0.019/0.019 (U22 1) 0.019/0.019 (U31 1) 0.019/0.019 (U32 1) 0.019/0.019 (U41 1) 0.019/0.019 (U42 1) 0.019/0.019 (U51 1) 0.019/0.019 (U52 1) 0.019/0.019 (U61 1) 0.019/0.019 (U62 1) 0.019/0.019 (U63 1) 0.019/0.019 (U64 1) 0.019/0.019 (U71 1) 0.019/0.019 (U72 1) 0.019/0.019 (U81 1) 0.019/0.019 (U82 1) 0.019/0.019 (afterNth 1 2) 0.019/0.019 (fst 1) 0.019/0.019 (head 1) 0.019/0.019 (natsFrom 1) 0.019/0.019 (sel 1 2) 0.019/0.019 (snd 1) 0.019/0.019 (splitAt 1 2) 0.019/0.019 (tail 1) 0.019/0.019 (take 1 2) 0.019/0.019 (0) 0.019/0.019 (cons 1) 0.019/0.019 (fSNonEmpty) 0.019/0.019 (nil) 0.019/0.019 (pair 1 2) 0.019/0.019 (s 1) 0.019/0.019 (tt) 0.019/0.019 ) 0.019/0.019 (RULES 0.019/0.019 U11(tt,N:S,XS:S) -> U12(tt,N:S,XS:S) 0.019/0.019 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.019/0.019 U21(tt,X:S) -> U22(tt,X:S) 0.019/0.019 U22(tt,X:S) -> X:S 0.019/0.019 U31(tt,N:S) -> U32(tt,N:S) 0.019/0.019 U32(tt,N:S) -> N:S 0.019/0.019 U41(tt,N:S,XS:S) -> U42(tt,N:S,XS:S) 0.019/0.019 U42(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.019/0.019 U51(tt,Y:S) -> U52(tt,Y:S) 0.019/0.019 U52(tt,Y:S) -> Y:S 0.019/0.019 U61(tt,N:S,X:S,XS:S) -> U62(tt,N:S,X:S,XS:S) 0.019/0.019 U62(tt,N:S,X:S,XS:S) -> U63(tt,N:S,X:S,XS:S) 0.019/0.019 U63(tt,N:S,X:S,XS:S) -> U64(splitAt(N:S,XS:S),X:S) 0.019/0.019 U64(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.019/0.019 U71(tt,XS:S) -> U72(tt,XS:S) 0.019/0.019 U72(tt,XS:S) -> XS:S 0.019/0.019 U81(tt,N:S,XS:S) -> U82(tt,N:S,XS:S) 0.019/0.019 U82(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.019/0.019 afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 ) 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 0.019/0.019 CleanTRS Processor: 0.019/0.019 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 Confluence Problem: 0.019/0.019 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S ZS:S) 0.019/0.019 (STRATEGY CONTEXTSENSITIVE 0.019/0.019 (U11 1) 0.019/0.019 (U12 1) 0.019/0.019 (U21 1) 0.019/0.019 (U22 1) 0.019/0.019 (U31 1) 0.019/0.019 (U32 1) 0.019/0.019 (U41 1) 0.019/0.019 (U42 1) 0.019/0.019 (U51 1) 0.019/0.019 (U52 1) 0.019/0.019 (U61 1) 0.019/0.019 (U62 1) 0.019/0.019 (U63 1) 0.019/0.019 (U64 1) 0.019/0.019 (U71 1) 0.019/0.019 (U72 1) 0.019/0.019 (U81 1) 0.019/0.019 (U82 1) 0.019/0.019 (afterNth 1 2) 0.019/0.019 (fst 1) 0.019/0.019 (head 1) 0.019/0.019 (natsFrom 1) 0.019/0.019 (sel 1 2) 0.019/0.019 (snd 1) 0.019/0.019 (splitAt 1 2) 0.019/0.019 (tail 1) 0.019/0.019 (take 1 2) 0.019/0.019 (0) 0.019/0.019 (cons 1) 0.019/0.019 (fSNonEmpty) 0.019/0.019 (nil) 0.019/0.019 (pair 1 2) 0.019/0.019 (s 1) 0.019/0.019 (tt) 0.019/0.019 ) 0.019/0.019 (RULES 0.019/0.019 U11(tt,N:S,XS:S) -> U12(tt,N:S,XS:S) 0.019/0.019 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.019/0.019 U21(tt,X:S) -> U22(tt,X:S) 0.019/0.019 U22(tt,X:S) -> X:S 0.019/0.019 U31(tt,N:S) -> U32(tt,N:S) 0.019/0.019 U32(tt,N:S) -> N:S 0.019/0.019 U41(tt,N:S,XS:S) -> U42(tt,N:S,XS:S) 0.019/0.019 U42(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.019/0.019 U51(tt,Y:S) -> U52(tt,Y:S) 0.019/0.019 U52(tt,Y:S) -> Y:S 0.019/0.019 U61(tt,N:S,X:S,XS:S) -> U62(tt,N:S,X:S,XS:S) 0.019/0.019 U62(tt,N:S,X:S,XS:S) -> U63(tt,N:S,X:S,XS:S) 0.019/0.019 U63(tt,N:S,X:S,XS:S) -> U64(splitAt(N:S,XS:S),X:S) 0.019/0.019 U64(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.019/0.019 U71(tt,XS:S) -> U72(tt,XS:S) 0.019/0.019 U72(tt,XS:S) -> XS:S 0.019/0.019 U81(tt,N:S,XS:S) -> U82(tt,N:S,XS:S) 0.019/0.019 U82(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.019/0.019 afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 ) 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 0.019/0.019 Modular Confluence Combinations Decomposition Processor: 0.019/0.019 It is a CTRS -> No modular confluence 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 CS-TRS Processor: 0.019/0.019 R is a CS-TRS 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 Confluence Problem: 0.019/0.019 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S ZS:S) 0.019/0.019 (STRATEGY CONTEXTSENSITIVE 0.019/0.019 (U11 1) 0.019/0.019 (U12 1) 0.019/0.019 (U21 1) 0.019/0.019 (U22 1) 0.019/0.019 (U31 1) 0.019/0.019 (U32 1) 0.019/0.019 (U41 1) 0.019/0.019 (U42 1) 0.019/0.019 (U51 1) 0.019/0.019 (U52 1) 0.019/0.019 (U61 1) 0.019/0.019 (U62 1) 0.019/0.019 (U63 1) 0.019/0.019 (U64 1) 0.019/0.019 (U71 1) 0.019/0.019 (U72 1) 0.019/0.019 (U81 1) 0.019/0.019 (U82 1) 0.019/0.019 (afterNth 1 2) 0.019/0.019 (fst 1) 0.019/0.019 (head 1) 0.019/0.019 (natsFrom 1) 0.019/0.019 (sel 1 2) 0.019/0.019 (snd 1) 0.019/0.019 (splitAt 1 2) 0.019/0.019 (tail 1) 0.019/0.019 (take 1 2) 0.019/0.019 (0) 0.019/0.019 (cons 1) 0.019/0.019 (fSNonEmpty) 0.019/0.019 (nil) 0.019/0.019 (pair 1 2) 0.019/0.019 (s 1) 0.019/0.019 (tt) 0.019/0.019 ) 0.019/0.019 (RULES 0.019/0.019 U11(tt,N:S,XS:S) -> U12(tt,N:S,XS:S) 0.019/0.019 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.019/0.019 U21(tt,X:S) -> U22(tt,X:S) 0.019/0.019 U22(tt,X:S) -> X:S 0.019/0.019 U31(tt,N:S) -> U32(tt,N:S) 0.019/0.019 U32(tt,N:S) -> N:S 0.019/0.019 U41(tt,N:S,XS:S) -> U42(tt,N:S,XS:S) 0.019/0.019 U42(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.019/0.019 U51(tt,Y:S) -> U52(tt,Y:S) 0.019/0.019 U52(tt,Y:S) -> Y:S 0.019/0.019 U61(tt,N:S,X:S,XS:S) -> U62(tt,N:S,X:S,XS:S) 0.019/0.019 U62(tt,N:S,X:S,XS:S) -> U63(tt,N:S,X:S,XS:S) 0.019/0.019 U63(tt,N:S,X:S,XS:S) -> U64(splitAt(N:S,XS:S),X:S) 0.019/0.019 U64(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.019/0.019 U71(tt,XS:S) -> U72(tt,XS:S) 0.019/0.019 U72(tt,XS:S) -> XS:S 0.019/0.019 U81(tt,N:S,XS:S) -> U82(tt,N:S,XS:S) 0.019/0.019 U82(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.019/0.019 afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 ) 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 0.019/0.019 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 14 (l' :-> r') => U64(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> U64(pair(YS:S,ZS:S),X:S)} 0.019/0.019 s => pair(cons(x30:S,U64(pair(YS:S,ZS:S),X:S)),x32:S) 0.019/0.019 t => U64(pair(pair(cons(X:S,YS:S),ZS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 15 (l' :-> r') => U71(tt,XS:S) -> U72(tt,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> U71(tt,XS:S)} 0.019/0.019 s => pair(cons(x30:S,U71(tt,XS:S)),x32:S) 0.019/0.019 t => U64(pair(U72(tt,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 16 (l' :-> r') => U72(tt,XS:S) -> XS:S 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> U72(tt,XS:S)} 0.019/0.019 s => pair(cons(x30:S,U72(tt,XS:S)),x32:S) 0.019/0.019 t => U64(pair(XS:S,x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 17 (l' :-> r') => U81(tt,N:S,XS:S) -> U82(tt,N:S,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> U81(tt,N:S,XS:S)} 0.019/0.019 s => pair(cons(x30:S,U81(tt,N:S,XS:S)),x32:S) 0.019/0.019 t => U64(pair(U82(tt,N:S,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 18 (l' :-> r') => U82(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> U82(tt,N:S,XS:S)} 0.019/0.019 s => pair(cons(x30:S,U82(tt,N:S,XS:S)),x32:S) 0.019/0.019 t => U64(pair(fst(splitAt(N:S,XS:S)),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 19 (l' :-> r') => afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> afterNth(N:S,XS:S)} 0.019/0.019 s => pair(cons(x30:S,afterNth(N:S,XS:S)),x32:S) 0.019/0.019 t => U64(pair(U11(tt,N:S,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 20 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> fst(pair(X:S,Y:S))} 0.019/0.019 s => pair(cons(x30:S,fst(pair(X:S,Y:S))),x32:S) 0.019/0.019 t => U64(pair(U21(tt,X:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 21 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> head(cons(N:S,XS:S))} 0.019/0.019 s => pair(cons(x30:S,head(cons(N:S,XS:S))),x32:S) 0.019/0.019 t => U64(pair(U31(tt,N:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 22 (l' :-> r') => natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> natsFrom(N:S)} 0.019/0.019 s => pair(cons(x30:S,natsFrom(N:S)),x32:S) 0.019/0.019 t => U64(pair(cons(N:S,natsFrom(s(N:S))),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 23 (l' :-> r') => sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> sel(N:S,XS:S)} 0.019/0.019 s => pair(cons(x30:S,sel(N:S,XS:S)),x32:S) 0.019/0.019 t => U64(pair(U41(tt,N:S,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => pair(cons(x30:S,snd(pair(X:S,Y:S))),x32:S) 0.019/0.019 t => U64(pair(U51(tt,Y:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> splitAt(0,XS:S)} 0.019/0.019 s => pair(cons(x30:S,splitAt(0,XS:S)),x32:S) 0.019/0.019 t => U64(pair(pair(nil,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => pair(cons(x30:S,splitAt(s(N:S),cons(X:S,XS:S))),x32:S) 0.019/0.019 t => U64(pair(U61(tt,N:S,X:S,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => pair(cons(x30:S,tail(cons(N:S,XS:S))),x32:S) 0.019/0.019 t => U64(pair(U71(tt,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x31:S 0.019/0.019 Pos x31:S in l => [1,1] 0.019/0.019 Sigma => {x31:S -> take(N:S,XS:S)} 0.019/0.019 s => pair(cons(x30:S,take(N:S,XS:S)),x32:S) 0.019/0.019 t => U64(pair(U81(tt,N:S,XS:S),x32:S),x30:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 19 (l' :-> r') => afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> afterNth(N:S,XS:S)} 0.019/0.019 s => U11(tt,afterNth(N:S,XS:S),x40:S) 0.019/0.019 t => afterNth(U11(tt,N:S,XS:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 20 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> fst(pair(X:S,Y:S))} 0.019/0.019 s => U11(tt,fst(pair(X:S,Y:S)),x40:S) 0.019/0.019 t => afterNth(U21(tt,X:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 21 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> head(cons(N:S,XS:S))} 0.019/0.019 s => U11(tt,head(cons(N:S,XS:S)),x40:S) 0.019/0.019 t => afterNth(U31(tt,N:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 22 (l' :-> r') => natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> natsFrom(N:S)} 0.019/0.019 s => U11(tt,natsFrom(N:S),x40:S) 0.019/0.019 t => afterNth(cons(N:S,natsFrom(s(N:S))),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 23 (l' :-> r') => sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> sel(N:S,XS:S)} 0.019/0.019 s => U11(tt,sel(N:S,XS:S),x40:S) 0.019/0.019 t => afterNth(U41(tt,N:S,XS:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => U11(tt,snd(pair(X:S,Y:S)),x40:S) 0.019/0.019 t => afterNth(U51(tt,Y:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> splitAt(0,XS:S)} 0.019/0.019 s => U11(tt,splitAt(0,XS:S),x40:S) 0.019/0.019 t => afterNth(pair(nil,XS:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => U11(tt,splitAt(s(N:S),cons(X:S,XS:S)),x40:S) 0.019/0.019 t => afterNth(U61(tt,N:S,X:S,XS:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => U11(tt,tail(cons(N:S,XS:S)),x40:S) 0.019/0.019 t => afterNth(U71(tt,XS:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x39:S 0.019/0.019 Pos x39:S in l => [1] 0.019/0.019 Sigma => {x39:S -> take(N:S,XS:S)} 0.019/0.019 s => U11(tt,take(N:S,XS:S),x40:S) 0.019/0.019 t => afterNth(U81(tt,N:S,XS:S),x40:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 20 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> fst(pair(X:S,Y:S))} 0.019/0.019 s => U21(tt,fst(pair(X:S,Y:S))) 0.019/0.019 t => fst(pair(U21(tt,X:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 21 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> head(cons(N:S,XS:S))} 0.019/0.019 s => U21(tt,head(cons(N:S,XS:S))) 0.019/0.019 t => fst(pair(U31(tt,N:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 22 (l' :-> r') => natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> natsFrom(N:S)} 0.019/0.019 s => U21(tt,natsFrom(N:S)) 0.019/0.019 t => fst(pair(cons(N:S,natsFrom(s(N:S))),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 23 (l' :-> r') => sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> sel(N:S,XS:S)} 0.019/0.019 s => U21(tt,sel(N:S,XS:S)) 0.019/0.019 t => fst(pair(U41(tt,N:S,XS:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => U21(tt,snd(pair(X:S,Y:S))) 0.019/0.019 t => fst(pair(U51(tt,Y:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> splitAt(0,XS:S)} 0.019/0.019 s => U21(tt,splitAt(0,XS:S)) 0.019/0.019 t => fst(pair(pair(nil,XS:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => U21(tt,splitAt(s(N:S),cons(X:S,XS:S))) 0.019/0.019 t => fst(pair(U61(tt,N:S,X:S,XS:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => U21(tt,tail(cons(N:S,XS:S))) 0.019/0.019 t => fst(pair(U71(tt,XS:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => fst(pair(x41:S,x42:S)) -> U21(tt,x41:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x41:S 0.019/0.019 Pos x41:S in l => [1,1] 0.019/0.019 Sigma => {x41:S -> take(N:S,XS:S)} 0.019/0.019 s => U21(tt,take(N:S,XS:S)) 0.019/0.019 t => fst(pair(U81(tt,N:S,XS:S),x42:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 21 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> head(cons(N:S,XS:S))} 0.019/0.019 s => U31(tt,head(cons(N:S,XS:S))) 0.019/0.019 t => head(cons(U31(tt,N:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 22 (l' :-> r') => natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> natsFrom(N:S)} 0.019/0.019 s => U31(tt,natsFrom(N:S)) 0.019/0.019 t => head(cons(cons(N:S,natsFrom(s(N:S))),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 23 (l' :-> r') => sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> sel(N:S,XS:S)} 0.019/0.019 s => U31(tt,sel(N:S,XS:S)) 0.019/0.019 t => head(cons(U41(tt,N:S,XS:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => U31(tt,snd(pair(X:S,Y:S))) 0.019/0.019 t => head(cons(U51(tt,Y:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> splitAt(0,XS:S)} 0.019/0.019 s => U31(tt,splitAt(0,XS:S)) 0.019/0.019 t => head(cons(pair(nil,XS:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => U31(tt,splitAt(s(N:S),cons(X:S,XS:S))) 0.019/0.019 t => head(cons(U61(tt,N:S,X:S,XS:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => U31(tt,tail(cons(N:S,XS:S))) 0.019/0.019 t => head(cons(U71(tt,XS:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => head(cons(x43:S,x44:S)) -> U31(tt,x43:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x43:S 0.019/0.019 Pos x43:S in l => [1,1] 0.019/0.019 Sigma => {x43:S -> take(N:S,XS:S)} 0.019/0.019 s => U31(tt,take(N:S,XS:S)) 0.019/0.019 t => head(cons(U81(tt,N:S,XS:S),x44:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 22 (l' :-> r') => natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> natsFrom(N:S)} 0.019/0.019 s => cons(natsFrom(N:S),natsFrom(s(natsFrom(N:S)))) 0.019/0.019 t => natsFrom(cons(N:S,natsFrom(s(N:S)))) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 23 (l' :-> r') => sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> sel(N:S,XS:S)} 0.019/0.019 s => cons(sel(N:S,XS:S),natsFrom(s(sel(N:S,XS:S)))) 0.019/0.019 t => natsFrom(U41(tt,N:S,XS:S)) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => cons(snd(pair(X:S,Y:S)),natsFrom(s(snd(pair(X:S,Y:S))))) 0.019/0.019 t => natsFrom(U51(tt,Y:S)) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> splitAt(0,XS:S)} 0.019/0.019 s => cons(splitAt(0,XS:S),natsFrom(s(splitAt(0,XS:S)))) 0.019/0.019 t => natsFrom(pair(nil,XS:S)) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => cons(splitAt(s(N:S),cons(X:S,XS:S)),natsFrom(s(splitAt(s(N:S),cons(X:S,XS:S))))) 0.019/0.019 t => natsFrom(U61(tt,N:S,X:S,XS:S)) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => cons(tail(cons(N:S,XS:S)),natsFrom(s(tail(cons(N:S,XS:S))))) 0.019/0.019 t => natsFrom(U71(tt,XS:S)) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x45:S 0.019/0.019 Pos x45:S in l => [1] 0.019/0.019 Sigma => {x45:S -> take(N:S,XS:S)} 0.019/0.019 s => cons(take(N:S,XS:S),natsFrom(s(take(N:S,XS:S)))) 0.019/0.019 t => natsFrom(U81(tt,N:S,XS:S)) 0.019/0.019 NW => 0 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S) 0.019/0.019 Rule 23 (l' :-> r') => sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 Var => x46:S 0.019/0.019 Pos x46:S in l => [1] 0.019/0.019 Sigma => {x46:S -> sel(N:S,XS:S)} 0.019/0.019 s => U41(tt,sel(N:S,XS:S),x47:S) 0.019/0.019 t => sel(U41(tt,N:S,XS:S),x47:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x46:S 0.019/0.019 Pos x46:S in l => [1] 0.019/0.019 Sigma => {x46:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => U41(tt,snd(pair(X:S,Y:S)),x47:S) 0.019/0.019 t => sel(U51(tt,Y:S),x47:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x46:S 0.019/0.019 Pos x46:S in l => [1] 0.019/0.019 Sigma => {x46:S -> splitAt(0,XS:S)} 0.019/0.019 s => U41(tt,splitAt(0,XS:S),x47:S) 0.019/0.019 t => sel(pair(nil,XS:S),x47:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x46:S 0.019/0.019 Pos x46:S in l => [1] 0.019/0.019 Sigma => {x46:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => U41(tt,splitAt(s(N:S),cons(X:S,XS:S)),x47:S) 0.019/0.019 t => sel(U61(tt,N:S,X:S,XS:S),x47:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x46:S 0.019/0.019 Pos x46:S in l => [1] 0.019/0.019 Sigma => {x46:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => U41(tt,tail(cons(N:S,XS:S)),x47:S) 0.019/0.019 t => sel(U71(tt,XS:S),x47:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x46:S 0.019/0.019 Pos x46:S in l => [1] 0.019/0.019 Sigma => {x46:S -> take(N:S,XS:S)} 0.019/0.019 s => U41(tt,take(N:S,XS:S),x47:S) 0.019/0.019 t => sel(U81(tt,N:S,XS:S),x47:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => snd(pair(x48:S,x49:S)) -> U51(tt,x49:S) 0.019/0.019 Rule 24 (l' :-> r') => snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 Var => x49:S 0.019/0.019 Pos x49:S in l => [1,2] 0.019/0.019 Sigma => {x49:S -> snd(pair(X:S,Y:S))} 0.019/0.019 s => U51(tt,snd(pair(X:S,Y:S))) 0.019/0.019 t => snd(pair(x48:S,U51(tt,Y:S))) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => snd(pair(x48:S,x49:S)) -> U51(tt,x49:S) 0.019/0.019 Rule 25 (l' :-> r') => splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 Var => x49:S 0.019/0.019 Pos x49:S in l => [1,2] 0.019/0.019 Sigma => {x49:S -> splitAt(0,XS:S)} 0.019/0.019 s => U51(tt,splitAt(0,XS:S)) 0.019/0.019 t => snd(pair(x48:S,pair(nil,XS:S))) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => snd(pair(x48:S,x49:S)) -> U51(tt,x49:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x49:S 0.019/0.019 Pos x49:S in l => [1,2] 0.019/0.019 Sigma => {x49:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => U51(tt,splitAt(s(N:S),cons(X:S,XS:S))) 0.019/0.019 t => snd(pair(x48:S,U61(tt,N:S,X:S,XS:S))) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => snd(pair(x48:S,x49:S)) -> U51(tt,x49:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x49:S 0.019/0.019 Pos x49:S in l => [1,2] 0.019/0.019 Sigma => {x49:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => U51(tt,tail(cons(N:S,XS:S))) 0.019/0.019 t => snd(pair(x48:S,U71(tt,XS:S))) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => snd(pair(x48:S,x49:S)) -> U51(tt,x49:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x49:S 0.019/0.019 Pos x49:S in l => [1,2] 0.019/0.019 Sigma => {x49:S -> take(N:S,XS:S)} 0.019/0.019 s => U51(tt,take(N:S,XS:S)) 0.019/0.019 t => snd(pair(x48:S,U81(tt,N:S,XS:S))) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => splitAt(s(x51:S),cons(x52:S,x53:S)) -> U61(tt,x51:S,x52:S,x53:S) 0.019/0.019 Rule 26 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 Var => x51:S 0.019/0.019 Pos x51:S in l => [1,1] 0.019/0.019 Sigma => {x51:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.019/0.019 s => U61(tt,splitAt(s(N:S),cons(X:S,XS:S)),x52:S,x53:S) 0.019/0.019 t => splitAt(s(U61(tt,N:S,X:S,XS:S)),cons(x52:S,x53:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => splitAt(s(x51:S),cons(x52:S,x53:S)) -> U61(tt,x51:S,x52:S,x53:S) 0.019/0.019 Rule 27 (l' :-> r') => tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 Var => x51:S 0.019/0.019 Pos x51:S in l => [1,1] 0.019/0.019 Sigma => {x51:S -> tail(cons(N:S,XS:S))} 0.019/0.019 s => U61(tt,tail(cons(N:S,XS:S)),x52:S,x53:S) 0.019/0.019 t => splitAt(s(U71(tt,XS:S)),cons(x52:S,x53:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => splitAt(s(x51:S),cons(x52:S,x53:S)) -> U61(tt,x51:S,x52:S,x53:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x51:S 0.019/0.019 Pos x51:S in l => [1,1] 0.019/0.019 Sigma => {x51:S -> take(N:S,XS:S)} 0.019/0.019 s => U61(tt,take(N:S,XS:S),x52:S,x53:S) 0.019/0.019 t => splitAt(s(U81(tt,N:S,XS:S)),cons(x52:S,x53:S)) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 ->Extended u-Critical Pair: 0.019/0.019 Rule 1 (l :-> r) => take(x56:S,x57:S) -> U81(tt,x56:S,x57:S) 0.019/0.019 Rule 28 (l' :-> r') => take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 Var => x56:S 0.019/0.019 Pos x56:S in l => [1] 0.019/0.019 Sigma => {x56:S -> take(N:S,XS:S)} 0.019/0.019 s => U81(tt,take(N:S,XS:S),x57:S) 0.019/0.019 t => take(U81(tt,N:S,XS:S),x57:S) 0.019/0.019 NW => 1 0.019/0.019 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 Confluence Problem: 0.019/0.019 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S ZS:S) 0.019/0.019 (STRATEGY CONTEXTSENSITIVE 0.019/0.019 (U11 1) 0.019/0.019 (U12 1) 0.019/0.019 (U21 1) 0.019/0.019 (U22 1) 0.019/0.019 (U31 1) 0.019/0.019 (U32 1) 0.019/0.019 (U41 1) 0.019/0.019 (U42 1) 0.019/0.019 (U51 1) 0.019/0.019 (U52 1) 0.019/0.019 (U61 1) 0.019/0.019 (U62 1) 0.019/0.019 (U63 1) 0.019/0.019 (U64 1) 0.019/0.019 (U71 1) 0.019/0.019 (U72 1) 0.019/0.019 (U81 1) 0.019/0.019 (U82 1) 0.019/0.019 (afterNth 1 2) 0.019/0.019 (fst 1) 0.019/0.019 (head 1) 0.019/0.019 (natsFrom 1) 0.019/0.019 (sel 1 2) 0.019/0.019 (snd 1) 0.019/0.019 (splitAt 1 2) 0.019/0.019 (tail 1) 0.019/0.019 (take 1 2) 0.019/0.019 (0) 0.019/0.019 (cons 1) 0.019/0.019 (fSNonEmpty) 0.019/0.019 (nil) 0.019/0.019 (pair 1 2) 0.019/0.019 (s 1) 0.019/0.019 (tt) 0.019/0.019 ) 0.019/0.019 (RULES 0.019/0.019 U11(tt,N:S,XS:S) -> U12(tt,N:S,XS:S) 0.019/0.019 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.019/0.019 U21(tt,X:S) -> U22(tt,X:S) 0.019/0.019 U22(tt,X:S) -> X:S 0.019/0.019 U31(tt,N:S) -> U32(tt,N:S) 0.019/0.019 U32(tt,N:S) -> N:S 0.019/0.019 U41(tt,N:S,XS:S) -> U42(tt,N:S,XS:S) 0.019/0.019 U42(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.019/0.019 U51(tt,Y:S) -> U52(tt,Y:S) 0.019/0.019 U52(tt,Y:S) -> Y:S 0.019/0.019 U61(tt,N:S,X:S,XS:S) -> U62(tt,N:S,X:S,XS:S) 0.019/0.019 U62(tt,N:S,X:S,XS:S) -> U63(tt,N:S,X:S,XS:S) 0.019/0.019 U63(tt,N:S,X:S,XS:S) -> U64(splitAt(N:S,XS:S),X:S) 0.019/0.019 U64(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.019/0.019 U71(tt,XS:S) -> U72(tt,XS:S) 0.019/0.019 U72(tt,XS:S) -> XS:S 0.019/0.019 U81(tt,N:S,XS:S) -> U82(tt,N:S,XS:S) 0.019/0.019 U82(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.019/0.019 afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 ) 0.019/0.019 Critical Pairs: 0.019/0.019 => Not trivial, Not overlay, NW1, N1 0.019/0.019 => Not trivial, Not overlay, NW1, N2 0.019/0.019 => Not trivial, Not overlay, NW1, N3 0.019/0.019 => Not trivial, Not overlay, NW1, N4 0.019/0.019 => Not trivial, Not overlay, NW1, N5 0.019/0.019 => Not trivial, Not overlay, NW1, N6 0.019/0.019 => Not trivial, Not overlay, NW1, N7 0.019/0.019 => Not trivial, Not overlay, NW1, N8 0.019/0.019 => Not trivial, Not overlay, NW1, N9 0.019/0.019 => Not trivial, Not overlay, NW1, N10 0.019/0.019 => Not trivial, Not overlay, NW1, N11 0.019/0.019 => Not trivial, Not overlay, NW1, N12 0.019/0.019 => Not trivial, Not overlay, NW1, N13 0.019/0.019 => Not trivial, Not overlay, NW1, N14 0.019/0.019 => Not trivial, Not overlay, NW1, N15 0.019/0.019 => Not trivial, Not overlay, NW1, N16 0.019/0.019 => Not trivial, Not overlay, NW1, N17 0.019/0.019 => Not trivial, Not overlay, NW1, N18 0.019/0.019 => Not trivial, Not overlay, NW1, N19 0.019/0.019 => Not trivial, Not overlay, NW1, N20 0.019/0.019 => Not trivial, Not overlay, NW1, N21 0.019/0.019 => Not trivial, Not overlay, NW1, N22 0.019/0.019 => Not trivial, Not overlay, NW1, N23 0.019/0.019 => Not trivial, Not overlay, NW1, N24 0.019/0.019 => Not trivial, Not overlay, NW1, N25 0.019/0.019 => Not trivial, Not overlay, NW1, N26 0.019/0.019 => Not trivial, Not overlay, NW1, N27 0.019/0.019 => Not trivial, Not overlay, NW1, N28 0.019/0.019 => Not trivial, Not overlay, NW1, N29 0.019/0.019 => Not trivial, Not overlay, NW1, N30 0.019/0.019 => Not trivial, Not overlay, NW1, N31 0.019/0.019 => Not trivial, Not overlay, NW1, N32 0.019/0.019 => Not trivial, Not overlay, NW1, N33 0.019/0.019 => Not trivial, Not overlay, NW1, N34 0.019/0.019 => Not trivial, Not overlay, NW1, N35 0.019/0.019 => Not trivial, Not overlay, NW1, N36 0.019/0.019 => Not trivial, Not overlay, NW1, N37 0.019/0.019 => Not trivial, Not overlay, NW1, N38 0.019/0.019 => Not trivial, Not overlay, NW1, N39 0.019/0.019 => Not trivial, Not overlay, NW1, N40 0.019/0.019 => Not trivial, Not overlay, NW1, N41 0.019/0.019 => Not trivial, Not overlay, NW1, N42 0.019/0.019 => Not trivial, Not overlay, NW0, N43 0.019/0.019 => Not trivial, Not overlay, NW0, N44 0.019/0.019 => Not trivial, Not overlay, NW0, N45 0.019/0.019 => Not trivial, Not overlay, NW0, N46 0.019/0.019 => Not trivial, Not overlay, NW0, N47 0.019/0.019 => Not trivial, Not overlay, NW0, N48 0.019/0.019 => Not trivial, Not overlay, NW0, N49 0.019/0.019 => Not trivial, Not overlay, NW1, N50 0.019/0.019 => Not trivial, Not overlay, NW1, N51 0.019/0.019 => Not trivial, Not overlay, NW1, N52 0.019/0.019 => Not trivial, Not overlay, NW1, N53 0.019/0.019 => Not trivial, Not overlay, NW1, N54 0.019/0.019 => Not trivial, Not overlay, NW1, N55 0.019/0.019 => Not trivial, Not overlay, NW1, N56 0.019/0.019 => Not trivial, Not overlay, NW1, N57 0.019/0.019 => Not trivial, Not overlay, NW1, N58 0.019/0.019 => Not trivial, Not overlay, NW1, N59 0.019/0.019 => Not trivial, Not overlay, NW1, N60 0.019/0.019 => Not trivial, Not overlay, NW1, N61 0.019/0.019 => Not trivial, Not overlay, NW1, N62 0.019/0.019 => Not trivial, Not overlay, NW1, N63 0.019/0.019 => Not trivial, Not overlay, NW1, N64 0.019/0.019 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.019/0.019 0.019/0.019 Huet Levy Processor: 0.019/0.019 -> Rules: 0.019/0.019 U11(tt,N:S,XS:S) -> U12(tt,N:S,XS:S) 0.019/0.019 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.019/0.019 U21(tt,X:S) -> U22(tt,X:S) 0.019/0.019 U22(tt,X:S) -> X:S 0.019/0.019 U31(tt,N:S) -> U32(tt,N:S) 0.019/0.019 U32(tt,N:S) -> N:S 0.019/0.019 U41(tt,N:S,XS:S) -> U42(tt,N:S,XS:S) 0.019/0.019 U42(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.019/0.019 U51(tt,Y:S) -> U52(tt,Y:S) 0.019/0.019 U52(tt,Y:S) -> Y:S 0.019/0.019 U61(tt,N:S,X:S,XS:S) -> U62(tt,N:S,X:S,XS:S) 0.019/0.019 U62(tt,N:S,X:S,XS:S) -> U63(tt,N:S,X:S,XS:S) 0.019/0.019 U63(tt,N:S,X:S,XS:S) -> U64(splitAt(N:S,XS:S),X:S) 0.019/0.019 U64(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.019/0.019 U71(tt,XS:S) -> U72(tt,XS:S) 0.019/0.019 U72(tt,XS:S) -> XS:S 0.019/0.019 U81(tt,N:S,XS:S) -> U82(tt,N:S,XS:S) 0.019/0.019 U82(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.019/0.019 afterNth(N:S,XS:S) -> U11(tt,N:S,XS:S) 0.019/0.019 fst(pair(X:S,Y:S)) -> U21(tt,X:S) 0.019/0.019 head(cons(N:S,XS:S)) -> U31(tt,N:S) 0.019/0.019 natsFrom(N:S) -> cons(N:S,natsFrom(s(N:S))) 0.019/0.019 sel(N:S,XS:S) -> U41(tt,N:S,XS:S) 0.019/0.019 snd(pair(X:S,Y:S)) -> U51(tt,Y:S) 0.019/0.019 splitAt(0,XS:S) -> pair(nil,XS:S) 0.019/0.019 splitAt(s(N:S),cons(X:S,XS:S)) -> U61(tt,N:S,X:S,XS:S) 0.019/0.019 tail(cons(N:S,XS:S)) -> U71(tt,XS:S) 0.019/0.019 take(N:S,XS:S) -> U81(tt,N:S,XS:S) 0.019/0.019 -> Vars: 0.019/0.019 N, XS, N, XS, X, X, N, N, N, XS, N, XS, Y, Y, N, X, XS, N, X, XS, N, X, XS, X, YS, ZS, XS, XS, N, XS, N, XS, N, XS, X, Y, N, XS, N, N, XS, X, Y, XS, N, X, XS, N, XS, N, XS 0.019/0.019 -> UVars: 0.019/0.019 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.019/0.019 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X], UV-RFrozen: [X]) 0.019/0.019 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N], UV-RFrozen: [N]) 0.019/0.019 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.019/0.019 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [Y], UV-RFrozen: [Y]) 0.019/0.019 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [Y], UV-LFrozen: [Y], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, X, XS], UV-RFrozen: [N, X, XS]) 0.019/0.019 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, X, XS], UV-RFrozen: [N, X, XS]) 0.019/0.019 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, X, XS], UV-RFrozen: [X]) 0.019/0.019 (UV-RuleId: 14, UV-LActive: [YS, ZS], UV-RActive: [X, ZS], UV-LFrozen: [X], UV-RFrozen: [YS]) 0.019/0.019 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [XS]) 0.019/0.019 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [XS], UV-LFrozen: [XS], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.019/0.019 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 19, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS]) 0.019/0.019 (UV-RuleId: 20, UV-LActive: [X, Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X]) 0.019/0.019 (UV-RuleId: 21, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N]) 0.019/0.019 (UV-RuleId: 22, UV-LActive: [N], UV-RActive: [N], UV-LFrozen: [], UV-RFrozen: [N]) 0.019/0.019 (UV-RuleId: 23, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS]) 0.019/0.019 (UV-RuleId: 24, UV-LActive: [X, Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [Y]) 0.019/0.019 (UV-RuleId: 25, UV-LActive: [XS], UV-RActive: [XS], UV-LFrozen: [], UV-RFrozen: []) 0.019/0.019 (UV-RuleId: 26, UV-LActive: [N, X], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, X, XS]) 0.019/0.019 (UV-RuleId: 27, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [XS]) 0.019/0.019 (UV-RuleId: 28, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS]) 0.019/0.019 -> FVars: 0.019/0.019 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, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57 0.019/0.019 -> PVars: 0.019/0.019 N: [x7, x9, x13, x14, x15, x17, x21, x24, x27, x35, x37, x39, x43, x45, x46, x51, x54, x56], XS: [x8, x10, x16, x18, x23, x26, x29, x33, x34, x36, x38, x40, x44, x47, x50, x53, x55, x57], X: [x11, x12, x22, x25, x28, x30, x41, x48, x52], Y: [x19, x20, x42, x49], YS: [x31], ZS: [x32] 0.019/0.019 0.019/0.019 -> Rlps: 0.019/0.019 (rule: U11(tt,x7:S,x8:S) -> U12(tt,x7:S,x8:S), id: 1, possubterms: U11(tt,x7:S,x8:S)->[], tt->[1]) 0.019/0.019 (rule: U12(tt,x9:S,x10:S) -> snd(splitAt(x9:S,x10:S)), id: 2, possubterms: U12(tt,x9:S,x10:S)->[], tt->[1]) 0.019/0.019 (rule: U21(tt,x11:S) -> U22(tt,x11:S), id: 3, possubterms: U21(tt,x11:S)->[], tt->[1]) 0.019/0.019 (rule: U22(tt,x12:S) -> x12:S, id: 4, possubterms: U22(tt,x12:S)->[], tt->[1]) 0.019/0.019 (rule: U31(tt,x13:S) -> U32(tt,x13:S), id: 5, possubterms: U31(tt,x13:S)->[], tt->[1]) 0.019/0.019 (rule: U32(tt,x14:S) -> x14:S, id: 6, possubterms: U32(tt,x14:S)->[], tt->[1]) 0.019/0.019 (rule: U41(tt,x15:S,x16:S) -> U42(tt,x15:S,x16:S), id: 7, possubterms: U41(tt,x15:S,x16:S)->[], tt->[1]) 0.019/0.019 (rule: U42(tt,x17:S,x18:S) -> head(afterNth(x17:S,x18:S)), id: 8, possubterms: U42(tt,x17:S,x18:S)->[], tt->[1]) 0.019/0.019 (rule: U51(tt,x19:S) -> U52(tt,x19:S), id: 9, possubterms: U51(tt,x19:S)->[], tt->[1]) 0.019/0.019 (rule: U52(tt,x20:S) -> x20:S, id: 10, possubterms: U52(tt,x20:S)->[], tt->[1]) 0.019/0.019 (rule: U61(tt,x21:S,x22:S,x23:S) -> U62(tt,x21:S,x22:S,x23:S), id: 11, possubterms: U61(tt,x21:S,x22:S,x23:S)->[], tt->[1]) 0.019/0.019 (rule: U62(tt,x24:S,x25:S,x26:S) -> U63(tt,x24:S,x25:S,x26:S), id: 12, possubterms: U62(tt,x24:S,x25:S,x26:S)->[], tt->[1]) 0.019/0.019 (rule: U63(tt,x27:S,x28:S,x29:S) -> U64(splitAt(x27:S,x29:S),x28:S), id: 13, possubterms: U63(tt,x27:S,x28:S,x29:S)->[], tt->[1]) 0.019/0.019 (rule: U64(pair(x31:S,x32:S),x30:S) -> pair(cons(x30:S,x31:S),x32:S), id: 14, possubterms: U64(pair(x31:S,x32:S),x30:S)->[], pair(x31:S,x32:S)->[1]) 0.019/0.019 (rule: U71(tt,x33:S) -> U72(tt,x33:S), id: 15, possubterms: U71(tt,x33:S)->[], tt->[1]) 0.019/0.019 (rule: U72(tt,x34:S) -> x34:S, id: 16, possubterms: U72(tt,x34:S)->[], tt->[1]) 0.019/0.019 (rule: U81(tt,x35:S,x36:S) -> U82(tt,x35:S,x36:S), id: 17, possubterms: U81(tt,x35:S,x36:S)->[], tt->[1]) 0.019/0.019 (rule: U82(tt,x37:S,x38:S) -> fst(splitAt(x37:S,x38:S)), id: 18, possubterms: U82(tt,x37:S,x38:S)->[], tt->[1]) 0.019/0.019 (rule: afterNth(x39:S,x40:S) -> U11(tt,x39:S,x40:S), id: 19, possubterms: afterNth(x39:S,x40:S)->[]) 0.019/0.019 (rule: fst(pair(x41:S,x42:S)) -> U21(tt,x41:S), id: 20, possubterms: fst(pair(x41:S,x42:S))->[], pair(x41:S,x42:S)->[1]) 0.019/0.019 (rule: head(cons(x43:S,x44:S)) -> U31(tt,x43:S), id: 21, possubterms: head(cons(x43:S,x44:S))->[], cons(x43:S,x44:S)->[1]) 0.019/0.019 (rule: natsFrom(x45:S) -> cons(x45:S,natsFrom(s(x45:S))), id: 22, possubterms: natsFrom(x45:S)->[]) 0.019/0.019 (rule: sel(x46:S,x47:S) -> U41(tt,x46:S,x47:S), id: 23, possubterms: sel(x46:S,x47:S)->[]) 0.019/0.019 (rule: snd(pair(x48:S,x49:S)) -> U51(tt,x49:S), id: 24, possubterms: snd(pair(x48:S,x49:S))->[], pair(x48:S,x49:S)->[1]) 0.019/0.019 (rule: splitAt(0,x50:S) -> pair(nil,x50:S), id: 25, possubterms: splitAt(0,x50:S)->[], 0->[1]) 0.019/0.019 (rule: splitAt(s(x51:S),cons(x52:S,x53:S)) -> U61(tt,x51:S,x52:S,x53:S), id: 26, possubterms: splitAt(s(x51:S),cons(x52:S,x53:S))->[], s(x51:S)->[1], cons(x52:S,x53:S)->[2]) 0.019/0.019 (rule: tail(cons(x54:S,x55:S)) -> U71(tt,x55:S), id: 27, possubterms: tail(cons(x54:S,x55:S))->[], cons(x54:S,x55:S)->[1]) 0.019/0.019 (rule: take(x56:S,x57:S) -> U81(tt,x56:S,x57:S), id: 28, possubterms: take(x56:S,x57:S)->[]) 0.019/0.019 0.019/0.019 -> Unifications: 0.019/0.019 0.019/0.019 0.019/0.019 -> Critical pairs info: 0.019/0.019 => Not trivial, Not overlay, NW1, N1 0.019/0.019 => Not trivial, Not overlay, NW0, N2 0.019/0.019 => Not trivial, Not overlay, NW0, N3 0.019/0.019 => Not trivial, Not overlay, NW1, N4 0.019/0.019 => Not trivial, Not overlay, NW1, N5 0.019/0.019 => Not trivial, Not overlay, NW1, N6 0.019/0.019 => Not trivial, Not overlay, NW0, N7 0.019/0.019 => Not trivial, Not overlay, NW1, N8 0.019/0.019 => Not trivial, Not overlay, NW1, N9 0.019/0.019 => Not trivial, Not overlay, NW1, N10 0.019/0.019 => Not trivial, Not overlay, NW1, N11 0.019/0.019 => Not trivial, Not overlay, NW0, N12 0.019/0.019 => Not trivial, Not overlay, NW1, N13 0.019/0.019 => Not trivial, Not overlay, NW1, N14 0.019/0.019 => Not trivial, Not overlay, NW1, N15 0.019/0.019 => Not trivial, Not overlay, NW1, N16 0.019/0.019 => Not trivial, Not overlay, NW1, N17 0.019/0.019 => Not trivial, Not overlay, NW1, N18 0.019/0.019 => Not trivial, Not overlay, NW1, N19 0.019/0.019 => Not trivial, Not overlay, NW1, N20 0.019/0.019 => Not trivial, Not overlay, NW1, N21 0.019/0.019 => Not trivial, Not overlay, NW1, N22 0.019/0.019 => Not trivial, Not overlay, NW1, N23 0.019/0.019 => Not trivial, Not overlay, NW1, N24 0.019/0.019 => Not trivial, Not overlay, NW1, N25 0.019/0.019 => Not trivial, Not overlay, NW1, N26 0.019/0.019 => Not trivial, Not overlay, NW1, N27 0.019/0.019 => Not trivial, Not overlay, NW1, N28 0.019/0.019 => Not trivial, Not overlay, NW1, N29 0.019/0.019 => Not trivial, Not overlay, NW1, N30 0.019/0.019 => Not trivial, Not overlay, NW1, N31 0.019/0.019 => Not trivial, Not overlay, NW1, N32 0.019/0.019 => Not trivial, Not overlay, NW1, N33 0.019/0.019 => Not trivial, Not overlay, NW1, N34 0.019/0.019 => Not trivial, Not overlay, NW1, N35 0.019/0.019 => Not trivial, Not overlay, NW1, N36 0.019/0.019 => Not trivial, Not overlay, NW1, N37 0.019/0.019 => Not trivial, Not overlay, NW0, N38 0.019/0.019 => Not trivial, Not overlay, NW1, N39 0.019/0.019 => Not trivial, Not overlay, NW1, N40 0.019/0.019 => Not trivial, Not overlay, NW1, N41 0.019/0.019 => Not trivial, Not overlay, NW1, N42 0.019/0.019 => Not trivial, Not overlay, NW1, N43 0.019/0.019 => Not trivial, Not overlay, NW1, N44 0.019/0.019 => Not trivial, Not overlay, NW0, N45 0.019/0.019 => Not trivial, Not overlay, NW1, N46 0.019/0.019 => Not trivial, Not overlay, NW1, N47 0.019/0.019 => Not trivial, Not overlay, NW0, N48 0.019/0.019 => Not trivial, Not overlay, NW1, N49 0.019/0.019 => Not trivial, Not overlay, NW1, N50 0.019/0.019 => Not trivial, Not overlay, NW1, N51 0.019/0.019 => Not trivial, Not overlay, NW1, N52 0.019/0.019 => Not trivial, Not overlay, NW1, N53 0.019/0.019 => Not trivial, Not overlay, NW1, N54 0.019/0.019 => Not trivial, Not overlay, NW1, N55 0.019/0.019 => Not trivial, Not overlay, NW1, N56 0.019/0.019 => Not trivial, Not overlay, NW1, N57 0.019/0.019 => Not trivial, Not overlay, NW1, N58 0.019/0.019 => Not trivial, Not overlay, NW1, N59 0.019/0.019 => Not trivial, Not overlay, NW1, N60 0.019/0.019 => Not trivial, Not overlay, NW1, N61 0.019/0.019 => Not trivial, Not overlay, NW1, N62 0.019/0.019 => Not trivial, Not overlay, NW1, N63 0.019/0.019 => Not trivial, Not overlay, NW1, N64 0.019/0.019 0.019/0.019 -> Problem conclusions: 0.019/0.019 Left linear, Not right linear, Not linear 0.019/0.019 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.019/0.019 Not Huet-Levy confluent, Not Newman confluent 0.019/0.019 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.019/0.019 0.019/0.019 0.019/0.019 Problem 1: 0.019/0.019 No Convergence Brute Force Processor: 0.019/0.019 -> Rewritings: 0.019/0.019 s: cons(sel(N:S,XS:S),natsFrom(s(sel(N:S,XS:S)))) 0.019/0.019 Nodes: [0,1,2,3,4,5,6] 0.019/0.019 Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6)] 0.019/0.019 ID: 0 => ('cons(sel(N:S,XS:S),natsFrom(s(sel(N:S,XS:S))))', D0) 0.019/0.019 ID: 1 => ('cons(U41(tt,N:S,XS:S),natsFrom(s(sel(N:S,XS:S))))', D1, R23, P[1], S{x46:S -> N:S, x47:S -> XS:S}), NR: 'U41(tt,N:S,XS:S)' 0.019/0.019 ID: 2 => ('cons(U42(tt,N:S,XS:S),natsFrom(s(sel(N:S,XS:S))))', D2, R7, P[1], S{x15:S -> N:S, x16:S -> XS:S}), NR: 'U42(tt,N:S,XS:S)' 0.019/0.019 ID: 3 => ('cons(head(afterNth(N:S,XS:S)),natsFrom(s(sel(N:S,XS:S))))', D3, R8, P[1], S{x17:S -> N:S, x18:S -> XS:S}), NR: 'head(afterNth(N:S,XS:S))' 0.019/0.019 ID: 4 => ('cons(head(U11(tt,N:S,XS:S)),natsFrom(s(sel(N:S,XS:S))))', D4, R19, P[1, 1], S{x39:S -> N:S, x40:S -> XS:S}), NR: 'U11(tt,N:S,XS:S)' 0.019/0.019 ID: 5 => ('cons(head(U12(tt,N:S,XS:S)),natsFrom(s(sel(N:S,XS:S))))', D5, R1, P[1, 1], S{x7:S -> N:S, x8:S -> XS:S}), NR: 'U12(tt,N:S,XS:S)' 0.019/0.019 ID: 6 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(sel(N:S,XS:S))))', D6, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 t: natsFrom(U41(tt,N:S,XS:S)) 0.019/0.019 Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26] 0.019/0.019 Edges: [(0,1),(0,2),(1,3),(1,4),(2,5),(3,6),(3,7),(4,8),(5,9),(6,10),(6,11),(7,12),(8,13),(9,14),(10,15),(10,16),(11,17),(12,18),(13,19),(14,20),(15,21),(16,22),(17,23),(18,24),(19,25),(20,26)] 0.019/0.019 ID: 0 => ('natsFrom(U41(tt,N:S,XS:S))', D0) 0.019/0.019 ID: 1 => ('natsFrom(U42(tt,N:S,XS:S))', D1, R7, P[1], S{x15:S -> N:S, x16:S -> XS:S}), NR: 'U42(tt,N:S,XS:S)' 0.019/0.019 ID: 2 => ('cons(U41(tt,N:S,XS:S),natsFrom(s(U41(tt,N:S,XS:S))))', D1, R22, P[], S{x45:S -> U41(tt,N:S,XS:S)}), NR: 'cons(U41(tt,N:S,XS:S),natsFrom(s(U41(tt,N:S,XS:S))))' 0.019/0.019 ID: 3 => ('natsFrom(head(afterNth(N:S,XS:S)))', D2, R8, P[1], S{x17:S -> N:S, x18:S -> XS:S}), NR: 'head(afterNth(N:S,XS:S))' 0.019/0.019 ID: 4 => ('cons(U42(tt,N:S,XS:S),natsFrom(s(U42(tt,N:S,XS:S))))', D2, R22, P[], S{x45:S -> U42(tt,N:S,XS:S)}), NR: 'cons(U42(tt,N:S,XS:S),natsFrom(s(U42(tt,N:S,XS:S))))' 0.019/0.019 ID: 5 => ('cons(U42(tt,N:S,XS:S),natsFrom(s(U41(tt,N:S,XS:S))))', D2, R7, P[1], S{x15:S -> N:S, x16:S -> XS:S}), NR: 'U42(tt,N:S,XS:S)' 0.019/0.019 ID: 6 => ('natsFrom(head(U11(tt,N:S,XS:S)))', D3, R19, P[1, 1], S{x39:S -> N:S, x40:S -> XS:S}), NR: 'U11(tt,N:S,XS:S)' 0.019/0.019 ID: 7 => ('cons(head(afterNth(N:S,XS:S)),natsFrom(s(head(afterNth(N:S,XS:S)))))', D3, R22, P[], S{x45:S -> head(afterNth(N:S,XS:S))}), NR: 'cons(head(afterNth(N:S,XS:S)),natsFrom(s(head(afterNth(N:S,XS:S)))))' 0.019/0.019 ID: 8 => ('cons(head(afterNth(N:S,XS:S)),natsFrom(s(U42(tt,N:S,XS:S))))', D3, R8, P[1], S{x17:S -> N:S, x18:S -> XS:S}), NR: 'head(afterNth(N:S,XS:S))' 0.019/0.019 ID: 9 => ('cons(head(afterNth(N:S,XS:S)),natsFrom(s(U41(tt,N:S,XS:S))))', D3, R8, P[1], S{x17:S -> N:S, x18:S -> XS:S}), NR: 'head(afterNth(N:S,XS:S))' 0.019/0.019 ID: 10 => ('natsFrom(head(U12(tt,N:S,XS:S)))', D4, R1, P[1, 1], S{x7:S -> N:S, x8:S -> XS:S}), NR: 'U12(tt,N:S,XS:S)' 0.019/0.019 ID: 11 => ('cons(head(U11(tt,N:S,XS:S)),natsFrom(s(head(U11(tt,N:S,XS:S)))))', D4, R22, P[], S{x45:S -> head(U11(tt,N:S,XS:S))}), NR: 'cons(head(U11(tt,N:S,XS:S)),natsFrom(s(head(U11(tt,N:S,XS:S)))))' 0.019/0.019 ID: 12 => ('cons(head(U11(tt,N:S,XS:S)),natsFrom(s(head(afterNth(N:S,XS:S)))))', D4, R19, P[1, 1], S{x39:S -> N:S, x40:S -> XS:S}), NR: 'U11(tt,N:S,XS:S)' 0.019/0.019 ID: 13 => ('cons(head(U11(tt,N:S,XS:S)),natsFrom(s(U42(tt,N:S,XS:S))))', D4, R19, P[1, 1], S{x39:S -> N:S, x40:S -> XS:S}), NR: 'U11(tt,N:S,XS:S)' 0.019/0.019 ID: 14 => ('cons(head(U11(tt,N:S,XS:S)),natsFrom(s(U41(tt,N:S,XS:S))))', D4, R19, P[1, 1], S{x39:S -> N:S, x40:S -> XS:S}), NR: 'U11(tt,N:S,XS:S)' 0.019/0.019 ID: 15 => ('natsFrom(head(snd(splitAt(N:S,XS:S))))', D5, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 ID: 16 => ('cons(head(U12(tt,N:S,XS:S)),natsFrom(s(head(U12(tt,N:S,XS:S)))))', D5, R22, P[], S{x45:S -> head(U12(tt,N:S,XS:S))}), NR: 'cons(head(U12(tt,N:S,XS:S)),natsFrom(s(head(U12(tt,N:S,XS:S)))))' 0.019/0.019 ID: 17 => ('cons(head(U12(tt,N:S,XS:S)),natsFrom(s(head(U11(tt,N:S,XS:S)))))', D5, R1, P[1, 1], S{x7:S -> N:S, x8:S -> XS:S}), NR: 'U12(tt,N:S,XS:S)' 0.019/0.019 ID: 18 => ('cons(head(U12(tt,N:S,XS:S)),natsFrom(s(head(afterNth(N:S,XS:S)))))', D5, R1, P[1, 1], S{x7:S -> N:S, x8:S -> XS:S}), NR: 'U12(tt,N:S,XS:S)' 0.019/0.019 ID: 19 => ('cons(head(U12(tt,N:S,XS:S)),natsFrom(s(U42(tt,N:S,XS:S))))', D5, R1, P[1, 1], S{x7:S -> N:S, x8:S -> XS:S}), NR: 'U12(tt,N:S,XS:S)' 0.019/0.019 ID: 20 => ('cons(head(U12(tt,N:S,XS:S)),natsFrom(s(U41(tt,N:S,XS:S))))', D5, R1, P[1, 1], S{x7:S -> N:S, x8:S -> XS:S}), NR: 'U12(tt,N:S,XS:S)' 0.019/0.019 ID: 21 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(head(snd(splitAt(N:S,XS:S))))))', D6, R22, P[], S{x45:S -> head(snd(splitAt(N:S,XS:S)))}), NR: 'cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(head(snd(splitAt(N:S,XS:S))))))' 0.019/0.019 ID: 22 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(head(U12(tt,N:S,XS:S)))))', D6, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 ID: 23 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(head(U11(tt,N:S,XS:S)))))', D6, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 ID: 24 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(head(afterNth(N:S,XS:S)))))', D6, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 ID: 25 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(U42(tt,N:S,XS:S))))', D6, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 ID: 26 => ('cons(head(snd(splitAt(N:S,XS:S))),natsFrom(s(U41(tt,N:S,XS:S))))', D6, R2, P[1, 1], S{x9:S -> N:S, x10:S -> XS:S}), NR: 'snd(splitAt(N:S,XS:S))' 0.019/0.019 cons(sel(N:S,XS:S),natsFrom(s(sel(N:S,XS:S)))) ->* no union *<- natsFrom(U41(tt,N:S,XS:S)) 0.019/0.019 "Not joinable" 0.019/0.019 0.019/0.019 The problem is not joinable. 0.019/0.019 0.19user 0.00system 0:00.19elapsed 104%CPU (0avgtext+0avgdata 16216maxresident)k 0.019/0.019 56inputs+0outputs (0major+7713minor)pagefaults 0swaps