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 IL:S:S L:S:S M:S:S N:S:S V:S:S V1:S:S V2:S:S X:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U43 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U53 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U63 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U91 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat 1) 0.002/0.002 (isNatIList 1) 0.002/0.002 (isNatIListKind 1) 0.002/0.002 (isNatKind 1) 0.002/0.002 (isNatList 1) 0.002/0.002 (length 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zeros) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S:S) -> U12(isNatList(V1:S:S)) 0.002/0.002 U12(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V:S:S) -> U32(isNatList(V:S:S)) 0.002/0.002 U32(tt) -> tt 0.002/0.002 U41(tt,V1:S:S,V2:S:S) -> U42(isNat(V1:S:S),V2:S:S) 0.002/0.002 U42(tt,V2:S:S) -> U43(isNatIList(V2:S:S)) 0.002/0.002 U43(tt) -> tt 0.002/0.002 U51(tt,V1:S:S,V2:S:S) -> U52(isNat(V1:S:S),V2:S:S) 0.002/0.002 U52(tt,V2:S:S) -> U53(isNatList(V2:S:S)) 0.002/0.002 U53(tt) -> tt 0.002/0.002 U61(tt,V1:S:S,V2:S:S) -> U62(isNat(V1:S:S),V2:S:S) 0.002/0.002 U62(tt,V2:S:S) -> U63(isNatIList(V2:S:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,L:S:S) -> s(length(L:S:S)) 0.002/0.002 U81(tt) -> nil 0.002/0.002 U91(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatIList(zeros) -> tt 0.002/0.002 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.002/0.002 isNatIListKind(take(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(zeros) -> tt 0.002/0.002 isNatIListKind(cons(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(nil) -> tt 0.002/0.002 isNatKind(length(V1:S:S)) -> isNatIListKind(V1:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.002/0.002 isNatList(take(V1:S:S,V2:S:S)) -> U61(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(cons(V1:S:S,V2:S:S)) -> U51(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(nil) -> tt 0.002/0.002 length(cons(N:S:S,L:S:S)) -> U71(and(and(isNatList(L:S:S),isNatIListKind(L:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),L:S:S) 0.002/0.002 length(nil) -> num0 0.002/0.002 take(num0,IL:S:S) -> U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S))) 0.002/0.002 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U91(and(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)),and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S)))),IL:S:S,M:S:S,N:S:S) 0.002/0.002 zeros -> cons(num0,zeros) 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 IL:S:S L:S:S M:S:S N:S:S V:S:S V1:S:S V2:S:S X:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U43 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U53 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U63 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U91 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat 1) 0.002/0.002 (isNatIList 1) 0.002/0.002 (isNatIListKind 1) 0.002/0.002 (isNatKind 1) 0.002/0.002 (isNatList 1) 0.002/0.002 (length 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zeros) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S:S) -> U12(isNatList(V1:S:S)) 0.002/0.002 U12(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V:S:S) -> U32(isNatList(V:S:S)) 0.002/0.002 U32(tt) -> tt 0.002/0.002 U41(tt,V1:S:S,V2:S:S) -> U42(isNat(V1:S:S),V2:S:S) 0.002/0.002 U42(tt,V2:S:S) -> U43(isNatIList(V2:S:S)) 0.002/0.002 U43(tt) -> tt 0.002/0.002 U51(tt,V1:S:S,V2:S:S) -> U52(isNat(V1:S:S),V2:S:S) 0.002/0.002 U52(tt,V2:S:S) -> U53(isNatList(V2:S:S)) 0.002/0.002 U53(tt) -> tt 0.002/0.002 U61(tt,V1:S:S,V2:S:S) -> U62(isNat(V1:S:S),V2:S:S) 0.002/0.002 U62(tt,V2:S:S) -> U63(isNatIList(V2:S:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,L:S:S) -> s(length(L:S:S)) 0.002/0.002 U81(tt) -> nil 0.002/0.002 U91(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatIList(zeros) -> tt 0.002/0.002 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.002/0.002 isNatIListKind(take(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(zeros) -> tt 0.002/0.002 isNatIListKind(cons(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(nil) -> tt 0.002/0.002 isNatKind(length(V1:S:S)) -> isNatIListKind(V1:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.002/0.002 isNatList(take(V1:S:S,V2:S:S)) -> U61(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(cons(V1:S:S,V2:S:S)) -> U51(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(nil) -> tt 0.002/0.002 length(cons(N:S:S,L:S:S)) -> U71(and(and(isNatList(L:S:S),isNatIListKind(L:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),L:S:S) 0.002/0.002 length(nil) -> num0 0.002/0.002 take(num0,IL:S:S) -> U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S))) 0.002/0.002 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U91(and(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)),and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S)))),IL:S:S,M:S:S,N:S:S) 0.002/0.002 zeros -> cons(num0,zeros) 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 IL:S:S L:S:S M:S:S N:S:S V:S:S V1:S:S V2:S:S X:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U43 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U53 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U63 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U91 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat 1) 0.002/0.002 (isNatIList 1) 0.002/0.002 (isNatIListKind 1) 0.002/0.002 (isNatKind 1) 0.002/0.002 (isNatList 1) 0.002/0.002 (length 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zeros) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S:S) -> U12(isNatList(V1:S:S)) 0.002/0.002 U12(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V:S:S) -> U32(isNatList(V:S:S)) 0.002/0.002 U32(tt) -> tt 0.002/0.002 U41(tt,V1:S:S,V2:S:S) -> U42(isNat(V1:S:S),V2:S:S) 0.002/0.002 U42(tt,V2:S:S) -> U43(isNatIList(V2:S:S)) 0.002/0.002 U43(tt) -> tt 0.002/0.002 U51(tt,V1:S:S,V2:S:S) -> U52(isNat(V1:S:S),V2:S:S) 0.002/0.002 U52(tt,V2:S:S) -> U53(isNatList(V2:S:S)) 0.002/0.002 U53(tt) -> tt 0.002/0.002 U61(tt,V1:S:S,V2:S:S) -> U62(isNat(V1:S:S),V2:S:S) 0.002/0.002 U62(tt,V2:S:S) -> U63(isNatIList(V2:S:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,L:S:S) -> s(length(L:S:S)) 0.002/0.002 U81(tt) -> nil 0.002/0.002 U91(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatIList(zeros) -> tt 0.002/0.002 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.002/0.002 isNatIListKind(take(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(zeros) -> tt 0.002/0.002 isNatIListKind(cons(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(nil) -> tt 0.002/0.002 isNatKind(length(V1:S:S)) -> isNatIListKind(V1:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.002/0.002 isNatList(take(V1:S:S,V2:S:S)) -> U61(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(cons(V1:S:S,V2:S:S)) -> U51(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(nil) -> tt 0.002/0.002 length(cons(N:S:S,L:S:S)) -> U71(and(and(isNatList(L:S:S),isNatIListKind(L:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),L:S:S) 0.002/0.002 length(nil) -> num0 0.002/0.002 take(num0,IL:S:S) -> U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S))) 0.002/0.002 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U91(and(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)),and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S)))),IL:S:S,M:S:S,N:S:S) 0.002/0.002 zeros -> cons(num0,zeros) 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 U11(tt,V1:S:S) -> U12(isNatList(V1:S:S)) 0.002/0.002 U12(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V:S:S) -> U32(isNatList(V:S:S)) 0.002/0.002 U32(tt) -> tt 0.002/0.002 U41(tt,V1:S:S,V2:S:S) -> U42(isNat(V1:S:S),V2:S:S) 0.002/0.002 U42(tt,V2:S:S) -> U43(isNatIList(V2:S:S)) 0.002/0.002 U43(tt) -> tt 0.002/0.002 U51(tt,V1:S:S,V2:S:S) -> U52(isNat(V1:S:S),V2:S:S) 0.002/0.002 U52(tt,V2:S:S) -> U53(isNatList(V2:S:S)) 0.002/0.002 U53(tt) -> tt 0.002/0.002 U61(tt,V1:S:S,V2:S:S) -> U62(isNat(V1:S:S),V2:S:S) 0.002/0.002 U62(tt,V2:S:S) -> U63(isNatIList(V2:S:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,L:S:S) -> s(length(L:S:S)) 0.002/0.002 U81(tt) -> nil 0.002/0.002 U91(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.002/0.002 and(tt,X:S:S) -> X:S:S 0.002/0.002 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatIList(zeros) -> tt 0.002/0.002 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.002/0.002 isNatIListKind(take(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(zeros) -> tt 0.002/0.002 isNatIListKind(cons(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)) 0.002/0.002 isNatIListKind(nil) -> tt 0.002/0.002 isNatKind(length(V1:S:S)) -> isNatIListKind(V1:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.002/0.002 isNatList(take(V1:S:S,V2:S:S)) -> U61(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(cons(V1:S:S,V2:S:S)) -> U51(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S) 0.002/0.002 isNatList(nil) -> tt 0.002/0.002 length(cons(N:S:S,L:S:S)) -> U71(and(and(isNatList(L:S:S),isNatIListKind(L:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),L:S:S) 0.002/0.002 length(nil) -> num0 0.002/0.002 take(num0,IL:S:S) -> U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S))) 0.002/0.002 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U91(and(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)),and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S)))),IL:S:S,M:S:S,N:S:S) 0.002/0.002 zeros -> cons(num0,zeros) 0.002/0.002 -> Vars: 0.002/0.002 V1:S, V1:S, V:S, V1:S, V2:S, V2:S, V1:S, V2:S, V2:S, V1:S, V2:S, V2:S, L:S, IL:S, M:S, N:S, X:S, V1:S, V1:S, V1:S, V2:S, V:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, L:S, N:S, IL:S, IL:S, M:S, N:S 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [V:S], UV-LFrozen: [V:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [L:S], UV-RFrozen: [L:S]) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1: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: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: [V:S]) 0.002/0.002 (UV-RuleId: 26, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 30, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 33, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [L:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S, N:S]) 0.002/0.002 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 38, UV-LActive: [IL:S], UV-RActive: [IL:S], UV-LFrozen: [], UV-RFrozen: [IL:S]) 0.002/0.002 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [IL:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.002/0.002 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 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 0.002/0.002 -> PVars: 0.002/0.002 V1:S: [x10, x11, x13, x16, x19, x27, x28, x29, x32, x34, x36, x37, x38, x40], V:S: [x12, x31], V2:S: [x14, x15, x17, x18, x20, x21, x30, x33, x35, x39, x41], L:S: [x22, x42], IL:S: [x23, x44, x45], M:S: [x24, x46], N:S: [x25, x43, x47], X:S: [x26] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U11(tt,x10:S) -> U12(isNatList(x10:S)), id: 1, possubterms: U11(tt,x10:S)->[], tt->[1]) 0.002/0.002 (rule: U12(tt) -> tt, id: 2, possubterms: U12(tt)->[], tt->[1]) 0.002/0.002 (rule: U21(tt,x11:S) -> U22(isNat(x11:S)), id: 3, possubterms: U21(tt,x11:S)->[], tt->[1]) 0.002/0.002 (rule: U22(tt) -> tt, id: 4, possubterms: U22(tt)->[], tt->[1]) 0.002/0.002 (rule: U31(tt,x12:S) -> U32(isNatList(x12:S)), id: 5, possubterms: U31(tt,x12:S)->[], tt->[1]) 0.002/0.002 (rule: U32(tt) -> tt, id: 6, possubterms: U32(tt)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x13:S,x14:S) -> U42(isNat(x13:S),x14:S), id: 7, possubterms: U41(tt,x13:S,x14:S)->[], tt->[1]) 0.002/0.002 (rule: U42(tt,x15:S) -> U43(isNatIList(x15:S)), id: 8, possubterms: U42(tt,x15:S)->[], tt->[1]) 0.002/0.002 (rule: U43(tt) -> tt, id: 9, possubterms: U43(tt)->[], tt->[1]) 0.002/0.002 (rule: U51(tt,x16:S,x17:S) -> U52(isNat(x16:S),x17:S), id: 10, possubterms: U51(tt,x16:S,x17:S)->[], tt->[1]) 0.002/0.002 (rule: U52(tt,x18:S) -> U53(isNatList(x18:S)), id: 11, possubterms: U52(tt,x18:S)->[], tt->[1]) 0.002/0.002 (rule: U53(tt) -> tt, id: 12, possubterms: U53(tt)->[], tt->[1]) 0.002/0.002 (rule: U61(tt,x19:S,x20:S) -> U62(isNat(x19:S),x20:S), id: 13, possubterms: U61(tt,x19:S,x20:S)->[], tt->[1]) 0.002/0.002 (rule: U62(tt,x21:S) -> U63(isNatIList(x21:S)), id: 14, possubterms: U62(tt,x21:S)->[], tt->[1]) 0.002/0.002 (rule: U63(tt) -> tt, id: 15, possubterms: U63(tt)->[], tt->[1]) 0.002/0.002 (rule: U71(tt,x22:S) -> s(length(x22:S)), id: 16, possubterms: U71(tt,x22:S)->[], tt->[1]) 0.002/0.002 (rule: U81(tt) -> nil, id: 17, possubterms: U81(tt)->[], tt->[1]) 0.002/0.002 (rule: U91(tt,x23:S,x24:S,x25:S) -> cons(x25:S,take(x24:S,x23:S)), id: 18, possubterms: U91(tt,x23:S,x24:S,x25:S)->[], tt->[1]) 0.002/0.002 (rule: and(tt,x26:S) -> x26:S, id: 19, possubterms: and(tt,x26:S)->[], tt->[1]) 0.002/0.002 (rule: isNat(length(x27:S)) -> U11(isNatIListKind(x27:S),x27:S), id: 20, possubterms: isNat(length(x27:S))->[], length(x27:S)->[1]) 0.002/0.002 (rule: isNat(num0) -> tt, id: 21, possubterms: isNat(num0)->[], num0->[1]) 0.002/0.002 (rule: isNat(s(x28:S)) -> U21(isNatKind(x28:S),x28:S), id: 22, possubterms: isNat(s(x28:S))->[], s(x28:S)->[1]) 0.002/0.002 (rule: isNatIList(zeros) -> tt, id: 23, possubterms: isNatIList(zeros)->[], zeros->[1]) 0.002/0.002 (rule: isNatIList(cons(x29:S,x30:S)) -> U41(and(isNatKind(x29:S),isNatIListKind(x30:S)),x29:S,x30:S), id: 24, possubterms: isNatIList(cons(x29:S,x30:S))->[], cons(x29:S,x30:S)->[1]) 0.002/0.002 (rule: isNatIList(x31:S) -> U31(isNatIListKind(x31:S),x31:S), id: 25, possubterms: isNatIList(x31:S)->[]) 0.002/0.002 (rule: isNatIListKind(take(x32:S,x33:S)) -> and(isNatKind(x32:S),isNatIListKind(x33:S)), id: 26, possubterms: isNatIListKind(take(x32:S,x33:S))->[], take(x32:S,x33:S)->[1]) 0.002/0.002 (rule: isNatIListKind(zeros) -> tt, id: 27, possubterms: isNatIListKind(zeros)->[], zeros->[1]) 0.002/0.002 (rule: isNatIListKind(cons(x34:S,x35:S)) -> and(isNatKind(x34:S),isNatIListKind(x35:S)), id: 28, possubterms: isNatIListKind(cons(x34:S,x35:S))->[], cons(x34:S,x35:S)->[1]) 0.002/0.002 (rule: isNatIListKind(nil) -> tt, id: 29, possubterms: isNatIListKind(nil)->[], nil->[1]) 0.002/0.002 (rule: isNatKind(length(x36:S)) -> isNatIListKind(x36:S), id: 30, possubterms: isNatKind(length(x36:S))->[], length(x36:S)->[1]) 0.002/0.002 (rule: isNatKind(num0) -> tt, id: 31, possubterms: isNatKind(num0)->[], num0->[1]) 0.002/0.002 (rule: isNatKind(s(x37:S)) -> isNatKind(x37:S), id: 32, possubterms: isNatKind(s(x37:S))->[], s(x37:S)->[1]) 0.002/0.002 (rule: isNatList(take(x38:S,x39:S)) -> U61(and(isNatKind(x38:S),isNatIListKind(x39:S)),x38:S,x39:S), id: 33, possubterms: isNatList(take(x38:S,x39:S))->[], take(x38:S,x39:S)->[1]) 0.002/0.002 (rule: isNatList(cons(x40:S,x41:S)) -> U51(and(isNatKind(x40:S),isNatIListKind(x41:S)),x40:S,x41:S), id: 34, possubterms: isNatList(cons(x40:S,x41:S))->[], cons(x40:S,x41:S)->[1]) 0.002/0.002 (rule: isNatList(nil) -> tt, id: 35, possubterms: isNatList(nil)->[], nil->[1]) 0.002/0.002 (rule: length(cons(x43:S,x42:S)) -> U71(and(and(isNatList(x42:S),isNatIListKind(x42:S)),and(isNat(x43:S),isNatKind(x43:S))),x42:S), id: 36, possubterms: length(cons(x43:S,x42:S))->[], cons(x43:S,x42:S)->[1]) 0.002/0.002 (rule: length(nil) -> num0, id: 37, possubterms: length(nil)->[], nil->[1]) 0.002/0.002 (rule: take(num0,x44:S) -> U81(and(isNatIList(x44:S),isNatIListKind(x44:S))), id: 38, possubterms: take(num0,x44:S)->[], num0->[1]) 0.002/0.002 (rule: take(s(x46:S),cons(x47:S,x45:S)) -> U91(and(and(isNatIList(x45:S),isNatIListKind(x45:S)),and(and(isNat(x46:S),isNatKind(x46:S)),and(isNat(x47:S),isNatKind(x47:S)))),x45:S,x46:S,x47:S), id: 39, possubterms: take(s(x46:S),cons(x47:S,x45:S))->[], s(x46:S)->[1], cons(x47:S,x45:S)->[2]) 0.002/0.002 (rule: zeros -> cons(num0,zeros), id: 40, possubterms: zeros->[]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R20 unifies with R36 at p: [1], l: isNat(length(x27:S)), lp: length(x27:S), sig: {x27:S -> cons(N:S:S,L:S:S)}, l': length(cons(N:S:S,L:S:S)), r: U11(isNatIListKind(x27:S),x27:S), r': U71(and(and(isNatList(L:S:S),isNatIListKind(L:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),L:S:S)) 0.002/0.002 (R20 unifies with R37 at p: [1], l: isNat(length(x27:S)), lp: length(x27:S), sig: {x27:S -> nil}, l': length(nil), r: U11(isNatIListKind(x27:S),x27:S), r': num0) 0.002/0.002 (R23 unifies with R40 at p: [1], l: isNatIList(zeros), lp: zeros, sig: {}, l': zeros, r: tt, r': cons(num0,zeros)) 0.002/0.002 (R25 unifies with R23 at p: [], l: isNatIList(x31:S), lp: isNatIList(x31:S), sig: {x31:S -> zeros}, l': isNatIList(zeros), r: U31(isNatIListKind(x31:S),x31:S), r': tt) 0.002/0.002 (R25 unifies with R24 at p: [], l: isNatIList(x31:S), lp: isNatIList(x31:S), sig: {x31:S -> cons(V1:S:S,V2:S:S)}, l': isNatIList(cons(V1:S:S,V2:S:S)), r: U31(isNatIListKind(x31:S),x31:S), r': U41(and(isNatKind(V1:S:S),isNatIListKind(V2:S:S)),V1:S:S,V2:S:S)) 0.002/0.002 (R26 unifies with R38 at p: [1], l: isNatIListKind(take(x32:S,x33:S)), lp: take(x32:S,x33:S), sig: {x32:S -> num0,x33:S -> IL:S:S}, l': take(num0,IL:S:S), r: and(isNatKind(x32:S),isNatIListKind(x33:S)), r': U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)))) 0.002/0.002 (R26 unifies with R39 at p: [1], l: isNatIListKind(take(x32:S,x33:S)), lp: take(x32:S,x33:S), sig: {x32:S -> s(M:S:S),x33:S -> cons(N:S:S,IL:S:S)}, l': take(s(M:S:S),cons(N:S:S,IL:S:S)), r: and(isNatKind(x32:S),isNatIListKind(x33:S)), r': U91(and(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)),and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S)))),IL:S:S,M:S:S,N:S:S)) 0.002/0.002 (R27 unifies with R40 at p: [1], l: isNatIListKind(zeros), lp: zeros, sig: {}, l': zeros, r: tt, r': cons(num0,zeros)) 0.002/0.002 (R30 unifies with R36 at p: [1], l: isNatKind(length(x36:S)), lp: length(x36:S), sig: {x36:S -> cons(N:S:S,L:S:S)}, l': length(cons(N:S:S,L:S:S)), r: isNatIListKind(x36:S), r': U71(and(and(isNatList(L:S:S),isNatIListKind(L:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),L:S:S)) 0.002/0.002 (R30 unifies with R37 at p: [1], l: isNatKind(length(x36:S)), lp: length(x36:S), sig: {x36:S -> nil}, l': length(nil), r: isNatIListKind(x36:S), r': num0) 0.002/0.002 (R33 unifies with R38 at p: [1], l: isNatList(take(x38:S,x39:S)), lp: take(x38:S,x39:S), sig: {x38:S -> num0,x39:S -> IL:S:S}, l': take(num0,IL:S:S), r: U61(and(isNatKind(x38:S),isNatIListKind(x39:S)),x38:S,x39:S), r': U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)))) 0.002/0.002 (R33 unifies with R39 at p: [1], l: isNatList(take(x38:S,x39:S)), lp: take(x38:S,x39:S), sig: {x38:S -> s(M:S:S),x39:S -> cons(N:S:S,IL:S:S)}, l': take(s(M:S:S),cons(N:S:S,IL:S:S)), r: U61(and(isNatKind(x38:S),isNatIListKind(x39:S)),x38:S,x39:S), r': U91(and(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)),and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S)))),IL:S:S,M:S:S,N: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, 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 => Not trivial, Not overlay, NW0, N11 0.002/0.002 => Not trivial, Overlay, NW0, N12 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: isNatIListKind(U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)))) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('isNatIListKind(U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S))))', D0) 0.002/0.002 ID: 1 => ('isNatIListKind(U81(and(U31(isNatIListKind(IL:S:S),IL:S:S),isNatIListKind(IL:S:S))))', D1, R25, P[1, 1, 1], S{x31:S -> IL:S:S}), NR: 'U31(isNatIListKind(IL:S:S),IL:S:S)' 0.002/0.002 t: and(isNatKind(num0),isNatIListKind(IL:S:S)) 0.002/0.002 Nodes: [0,1,2] 0.002/0.002 Edges: [(0,1),(1,2)] 0.002/0.002 ID: 0 => ('and(isNatKind(num0),isNatIListKind(IL:S:S))', D0) 0.002/0.002 ID: 1 => ('and(tt,isNatIListKind(IL:S:S))', D1, R31, P[1], S{}), NR: 'tt' 0.002/0.002 ID: 2 => ('isNatIListKind(IL:S:S)', D2, R19, P[], S{x26:S -> isNatIListKind(IL:S:S)}), NR: 'isNatIListKind(IL:S:S)' 0.002/0.002 isNatIListKind(U81(and(isNatIList(IL:S:S),isNatIListKind(IL:S:S)))) ->* no union *<- and(isNatKind(num0),isNatIListKind(IL: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 63%CPU (0avgtext+0avgdata 12016maxresident)k 0.002/0.002 8inputs+0outputs (0major+1210minor)pagefaults 0swaps