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 N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U11 1) 0.002/0.002 (U21 1) 0.002/0.002 (U31 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U91 1) 0.002/0.002 (afterNth) 0.002/0.002 (and 1) 0.002/0.002 (fst 1) 0.002/0.002 (head 1) 0.002/0.002 (isLNat 1) 0.002/0.002 (isNatural 1) 0.002/0.002 (isPLNat 1) 0.002/0.002 (natsFrom) 0.002/0.002 (sel) 0.002/0.002 (snd 1) 0.002/0.002 (splitAt 1 2) 0.002/0.002 (tail 1) 0.002/0.002 (take) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (pair) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U21(tt,X:S:S) -> X:S:S 0.002/0.002 U31(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U51(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U61(tt,Y:S:S) -> Y:S:S 0.002/0.002 U71(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U81(tt,N:S:S,X:S:S,XS:S:S) -> U82(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U82(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U91(tt,XS:S:S) -> XS:S:S 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(and(isLNat(X:S:S),isLNat(Y:S:S)),X:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(fst(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isLNat(snd(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(tail(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> and(isLNat(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 natsFrom(N:S:S) -> U41(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U51(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U61(and(isLNat(X:S:S),isLNat(Y:S:S)),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U71(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U91(and(isNatural(N:S:S),isLNat(XS:S:S)),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U101(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 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 N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U11 1) 0.002/0.002 (U21 1) 0.002/0.002 (U31 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U91 1) 0.002/0.002 (afterNth) 0.002/0.002 (and 1) 0.002/0.002 (fst 1) 0.002/0.002 (head 1) 0.002/0.002 (isLNat 1) 0.002/0.002 (isNatural 1) 0.002/0.002 (isPLNat 1) 0.002/0.002 (natsFrom) 0.002/0.002 (sel) 0.002/0.002 (snd 1) 0.002/0.002 (splitAt 1 2) 0.002/0.002 (tail 1) 0.002/0.002 (take) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (pair) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U21(tt,X:S:S) -> X:S:S 0.002/0.002 U31(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U51(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U61(tt,Y:S:S) -> Y:S:S 0.002/0.002 U71(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U81(tt,N:S:S,X:S:S,XS:S:S) -> U82(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U82(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U91(tt,XS:S:S) -> XS:S:S 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(and(isLNat(X:S:S),isLNat(Y:S:S)),X:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(fst(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isLNat(snd(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(tail(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> and(isLNat(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 natsFrom(N:S:S) -> U41(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U51(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U61(and(isLNat(X:S:S),isLNat(Y:S:S)),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U71(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U91(and(isNatural(N:S:S),isLNat(XS:S:S)),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U101(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 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 v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U11 1) 0.002/0.002 (U21 1) 0.002/0.002 (U31 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U91 1) 0.002/0.002 (afterNth) 0.002/0.002 (and 1) 0.002/0.002 (fst 1) 0.002/0.002 (head 1) 0.002/0.002 (isLNat 1) 0.002/0.002 (isNatural 1) 0.002/0.002 (isPLNat 1) 0.002/0.002 (natsFrom) 0.002/0.002 (sel) 0.002/0.002 (snd 1) 0.002/0.002 (splitAt 1 2) 0.002/0.002 (tail 1) 0.002/0.002 (take) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (pair) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U21(tt,X:S:S) -> X:S:S 0.002/0.002 U31(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U51(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U61(tt,Y:S:S) -> Y:S:S 0.002/0.002 U71(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U81(tt,N:S:S,X:S:S,XS:S:S) -> U82(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U82(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U91(tt,XS:S:S) -> XS:S:S 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(and(isLNat(X:S:S),isLNat(Y:S:S)),X:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(fst(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isLNat(snd(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(tail(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> and(isLNat(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 natsFrom(N:S:S) -> U41(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U51(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U61(and(isLNat(X:S:S),isLNat(Y:S:S)),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U71(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U91(and(isNatural(N:S:S),isLNat(XS:S:S)),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U101(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 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 U101(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U21(tt,X:S:S) -> X:S:S 0.002/0.002 U31(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U51(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U61(tt,Y:S:S) -> Y:S:S 0.002/0.002 U71(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U81(tt,N:S:S,X:S:S,XS:S:S) -> U82(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U82(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U91(tt,XS:S:S) -> XS:S:S 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(and(isLNat(X:S:S),isLNat(Y:S:S)),X:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(fst(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isLNat(snd(V1:S:S)) -> isPLNat(V1:S:S) 0.002/0.002 isLNat(tail(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> isLNat(V1:S:S) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> isNatural(V1:S:S) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> and(isNatural(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> and(isLNat(V1:S:S),isLNat(V2:S:S)) 0.002/0.002 natsFrom(N:S:S) -> U41(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U51(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U61(and(isLNat(X:S:S),isLNat(Y:S:S)),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U71(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U91(and(isNatural(N:S:S),isLNat(XS:S:S)),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U101(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S) 0.002/0.002 -> Vars: 0.002/0.002 N:S, XS:S, N:S, XS:S, X:S, N:S, N:S, N:S, XS:S, Y:S, XS:S, N:S, X:S, XS:S, X:S, YS:S, ZS:S, XS:S, N:S, XS:S, X:S, X:S, Y:S, N:S, XS:S, V1:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V2:S, N:S, N:S, XS:S, X:S, Y:S, XS:S, N:S, X:S, XS:S, N:S, XS:S, N:S, XS:S 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [X:S]) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, YS:S, ZS:S], UV-RFrozen: [X:S, YS:S, ZS:S]) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 24, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 28, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [Y:S]) 0.002/0.002 (UV-RuleId: 33, UV-LActive: [XS:S], UV-RActive: [XS:S], UV-LFrozen: [], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.002/0.002 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 -> FVars: 0.002/0.002 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, x58, x59, x60, x61, x62, x63, x64, x65 0.002/0.002 -> PVars: 0.002/0.002 N:S: [x10, x12, x15, x16, x17, x21, x28, x33, x53, x54, x59, x62, x64], XS:S: [x11, x13, x18, x20, x23, x27, x29, x34, x55, x58, x61, x63, x65], X:S: [x14, x22, x24, x30, x31, x56, x60], Y:S: [x19, x32, x57], YS:S: [x25], ZS:S: [x26], V1:S: [x35, x37, x38, x39, x40, x41, x43, x45, x46, x48, x49, x51], V2:S: [x36, x42, x44, x47, x50, x52] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U101(tt,x10:S,x11:S) -> fst(splitAt(x10:S,x11:S)), id: 1, possubterms: U101(tt,x10:S,x11:S)->[], tt->[1]) 0.002/0.002 (rule: U11(tt,x12:S,x13:S) -> snd(splitAt(x12:S,x13:S)), id: 2, possubterms: U11(tt,x12:S,x13:S)->[], tt->[1]) 0.002/0.002 (rule: U21(tt,x14:S) -> x14:S, id: 3, possubterms: U21(tt,x14:S)->[], tt->[1]) 0.002/0.002 (rule: U31(tt,x15:S) -> x15:S, id: 4, possubterms: U31(tt,x15:S)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x16:S) -> cons(x16:S,natsFrom(s(x16:S))), id: 5, possubterms: U41(tt,x16:S)->[], tt->[1]) 0.002/0.002 (rule: U51(tt,x17:S,x18:S) -> head(afterNth(x17:S,x18:S)), id: 6, possubterms: U51(tt,x17:S,x18:S)->[], tt->[1]) 0.002/0.002 (rule: U61(tt,x19:S) -> x19:S, id: 7, possubterms: U61(tt,x19:S)->[], tt->[1]) 0.002/0.002 (rule: U71(tt,x20:S) -> pair(nil,x20:S), id: 8, possubterms: U71(tt,x20:S)->[], tt->[1]) 0.002/0.002 (rule: U81(tt,x21:S,x22:S,x23:S) -> U82(splitAt(x21:S,x23:S),x22:S), id: 9, possubterms: U81(tt,x21:S,x22:S,x23:S)->[], tt->[1]) 0.002/0.002 (rule: U82(pair(x25:S,x26:S),x24:S) -> pair(cons(x24:S,x25:S),x26:S), id: 10, possubterms: U82(pair(x25:S,x26:S),x24:S)->[], pair(x25:S,x26:S)->[1]) 0.002/0.002 (rule: U91(tt,x27:S) -> x27:S, id: 11, possubterms: U91(tt,x27:S)->[], tt->[1]) 0.002/0.002 (rule: afterNth(x28:S,x29:S) -> U11(and(isNatural(x28:S),isLNat(x29:S)),x28:S,x29:S), id: 12, possubterms: afterNth(x28:S,x29:S)->[]) 0.002/0.002 (rule: and(tt,x30:S) -> x30:S, id: 13, possubterms: and(tt,x30:S)->[], tt->[1]) 0.002/0.002 (rule: fst(pair(x31:S,x32:S)) -> U21(and(isLNat(x31:S),isLNat(x32:S)),x31:S), id: 14, possubterms: fst(pair(x31:S,x32:S))->[], pair(x31:S,x32:S)->[1]) 0.002/0.002 (rule: head(cons(x33:S,x34:S)) -> U31(and(isNatural(x33:S),isLNat(x34:S)),x33:S), id: 15, possubterms: head(cons(x33:S,x34:S))->[], cons(x33:S,x34:S)->[1]) 0.002/0.002 (rule: isLNat(afterNth(x35:S,x36:S)) -> and(isNatural(x35:S),isLNat(x36:S)), id: 16, possubterms: isLNat(afterNth(x35:S,x36:S))->[], afterNth(x35:S,x36:S)->[1]) 0.002/0.002 (rule: isLNat(fst(x37:S)) -> isPLNat(x37:S), id: 17, possubterms: isLNat(fst(x37:S))->[], fst(x37:S)->[1]) 0.002/0.002 (rule: isLNat(natsFrom(x38:S)) -> isNatural(x38:S), id: 18, possubterms: isLNat(natsFrom(x38:S))->[], natsFrom(x38:S)->[1]) 0.002/0.002 (rule: isLNat(snd(x39:S)) -> isPLNat(x39:S), id: 19, possubterms: isLNat(snd(x39:S))->[], snd(x39:S)->[1]) 0.002/0.002 (rule: isLNat(tail(x40:S)) -> isLNat(x40:S), id: 20, possubterms: isLNat(tail(x40:S))->[], tail(x40:S)->[1]) 0.002/0.002 (rule: isLNat(take(x41:S,x42:S)) -> and(isNatural(x41:S),isLNat(x42:S)), id: 21, possubterms: isLNat(take(x41:S,x42:S))->[], take(x41:S,x42:S)->[1]) 0.002/0.002 (rule: isLNat(cons(x43:S,x44:S)) -> and(isNatural(x43:S),isLNat(x44:S)), id: 22, possubterms: isLNat(cons(x43:S,x44:S))->[], cons(x43:S,x44:S)->[1]) 0.002/0.002 (rule: isLNat(nil) -> tt, id: 23, possubterms: isLNat(nil)->[], nil->[1]) 0.002/0.002 (rule: isNatural(head(x45:S)) -> isLNat(x45:S), id: 24, possubterms: isNatural(head(x45:S))->[], head(x45:S)->[1]) 0.002/0.002 (rule: isNatural(sel(x46:S,x47:S)) -> and(isNatural(x46:S),isLNat(x47:S)), id: 25, possubterms: isNatural(sel(x46:S,x47:S))->[], sel(x46:S,x47:S)->[1]) 0.002/0.002 (rule: isNatural(num0) -> tt, id: 26, possubterms: isNatural(num0)->[], num0->[1]) 0.002/0.002 (rule: isNatural(s(x48:S)) -> isNatural(x48:S), id: 27, possubterms: isNatural(s(x48:S))->[], s(x48:S)->[1]) 0.002/0.002 (rule: isPLNat(splitAt(x49:S,x50:S)) -> and(isNatural(x49:S),isLNat(x50:S)), id: 28, possubterms: isPLNat(splitAt(x49:S,x50:S))->[], splitAt(x49:S,x50:S)->[1]) 0.002/0.002 (rule: isPLNat(pair(x51:S,x52:S)) -> and(isLNat(x51:S),isLNat(x52:S)), id: 29, possubterms: isPLNat(pair(x51:S,x52:S))->[], pair(x51:S,x52:S)->[1]) 0.002/0.002 (rule: natsFrom(x53:S) -> U41(isNatural(x53:S),x53:S), id: 30, possubterms: natsFrom(x53:S)->[]) 0.002/0.002 (rule: sel(x54:S,x55:S) -> U51(and(isNatural(x54:S),isLNat(x55:S)),x54:S,x55:S), id: 31, possubterms: sel(x54:S,x55:S)->[]) 0.002/0.002 (rule: snd(pair(x56:S,x57:S)) -> U61(and(isLNat(x56:S),isLNat(x57:S)),x57:S), id: 32, possubterms: snd(pair(x56:S,x57:S))->[], pair(x56:S,x57:S)->[1]) 0.002/0.002 (rule: splitAt(num0,x58:S) -> U71(isLNat(x58:S),x58:S), id: 33, possubterms: splitAt(num0,x58:S)->[], num0->[1]) 0.002/0.002 (rule: splitAt(s(x59:S),cons(x60:S,x61:S)) -> U81(and(isNatural(x59:S),and(isNatural(x60:S),isLNat(x61:S))),x59:S,x60:S,x61:S), id: 34, possubterms: splitAt(s(x59:S),cons(x60:S,x61:S))->[], s(x59:S)->[1], cons(x60:S,x61:S)->[2]) 0.002/0.002 (rule: tail(cons(x62:S,x63:S)) -> U91(and(isNatural(x62:S),isLNat(x63:S)),x63:S), id: 35, possubterms: tail(cons(x62:S,x63:S))->[], cons(x62:S,x63:S)->[1]) 0.002/0.002 (rule: take(x64:S,x65:S) -> U101(and(isNatural(x64:S),isLNat(x65:S)),x64:S,x65:S), id: 36, possubterms: take(x64:S,x65:S)->[]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R16 unifies with R12 at p: [1], l: isLNat(afterNth(x35:S,x36:S)), lp: afterNth(x35:S,x36:S), sig: {x35:S -> N:S:S,x36:S -> XS:S:S}, l': afterNth(N:S:S,XS:S:S), r: and(isNatural(x35:S),isLNat(x36:S)), r': U11(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S)) 0.002/0.002 (R17 unifies with R14 at p: [1], l: isLNat(fst(x37:S)), lp: fst(x37:S), sig: {x37:S -> pair(X:S:S,Y:S:S)}, l': fst(pair(X:S:S,Y:S:S)), r: isPLNat(x37:S), r': U21(and(isLNat(X:S:S),isLNat(Y:S:S)),X:S:S)) 0.002/0.002 (R18 unifies with R30 at p: [1], l: isLNat(natsFrom(x38:S)), lp: natsFrom(x38:S), sig: {x38:S -> N:S:S}, l': natsFrom(N:S:S), r: isNatural(x38:S), r': U41(isNatural(N:S:S),N:S:S)) 0.002/0.002 (R19 unifies with R32 at p: [1], l: isLNat(snd(x39:S)), lp: snd(x39:S), sig: {x39:S -> pair(X:S:S,Y:S:S)}, l': snd(pair(X:S:S,Y:S:S)), r: isPLNat(x39:S), r': U61(and(isLNat(X:S:S),isLNat(Y:S:S)),Y:S:S)) 0.002/0.002 (R20 unifies with R35 at p: [1], l: isLNat(tail(x40:S)), lp: tail(x40:S), sig: {x40:S -> cons(N:S:S,XS:S:S)}, l': tail(cons(N:S:S,XS:S:S)), r: isLNat(x40:S), r': U91(and(isNatural(N:S:S),isLNat(XS:S:S)),XS:S:S)) 0.002/0.002 (R21 unifies with R36 at p: [1], l: isLNat(take(x41:S,x42:S)), lp: take(x41:S,x42:S), sig: {x41:S -> N:S:S,x42:S -> XS:S:S}, l': take(N:S:S,XS:S:S), r: and(isNatural(x41:S),isLNat(x42:S)), r': U101(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S)) 0.002/0.002 (R24 unifies with R15 at p: [1], l: isNatural(head(x45:S)), lp: head(x45:S), sig: {x45:S -> cons(N:S:S,XS:S:S)}, l': head(cons(N:S:S,XS:S:S)), r: isLNat(x45:S), r': U31(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S)) 0.002/0.002 (R25 unifies with R31 at p: [1], l: isNatural(sel(x46:S,x47:S)), lp: sel(x46:S,x47:S), sig: {x46:S -> N:S:S,x47:S -> XS:S:S}, l': sel(N:S:S,XS:S:S), r: and(isNatural(x46:S),isLNat(x47:S)), r': U51(and(isNatural(N:S:S),isLNat(XS:S:S)),N:S:S,XS:S:S)) 0.002/0.002 (R28 unifies with R33 at p: [1], l: isPLNat(splitAt(x49:S,x50:S)), lp: splitAt(x49:S,x50:S), sig: {x49:S -> num0,x50:S -> XS:S:S}, l': splitAt(num0,XS:S:S), r: and(isNatural(x49:S),isLNat(x50:S)), r': U71(isLNat(XS:S:S),XS:S:S)) 0.002/0.002 (R28 unifies with R34 at p: [1], l: isPLNat(splitAt(x49:S,x50:S)), lp: splitAt(x49:S,x50:S), sig: {x49:S -> s(N:S:S),x50:S -> cons(X:S:S,XS:S:S)}, l': splitAt(s(N:S:S),cons(X:S:S,XS:S:S)), r: and(isNatural(x49:S),isLNat(x50:S)), r': U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS: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 => Not trivial, Not 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, 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 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: isPLNat(U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S)) 0.002/0.002 Nodes: [0] 0.002/0.002 Edges: [] 0.002/0.002 ID: 0 => ('isPLNat(U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S))', D0) 0.002/0.002 t: and(isNatural(s(N:S:S)),isLNat(cons(X:S:S,XS:S:S))) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('and(isNatural(s(N:S:S)),isLNat(cons(X:S:S,XS:S:S)))', D0) 0.002/0.002 ID: 1 => ('and(isNatural(N:S:S),isLNat(cons(X:S:S,XS:S:S)))', D1, R27, P[1], S{x48:S -> N:S:S}), NR: 'isNatural(N:S:S)' 0.002/0.002 isPLNat(U81(and(isNatural(N:S:S),and(isNatural(X:S:S),isLNat(XS:S:S))),N:S:S,X:S:S,XS:S:S)) ->* no union *<- and(isNatural(s(N:S:S)),isLNat(cons(X:S:S,XS: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.01user 0.00system 0:00.02elapsed 86%CPU (0avgtext+0avgdata 12052maxresident)k 0.002/0.002 8inputs+0outputs (0major+1205minor)pagefaults 0swaps