0.003/0.003 NO 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (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) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U105 1) 0.003/0.003 (U106 1) 0.003/0.003 (U11 1) 0.003/0.003 (U111 1) 0.003/0.003 (U112 1) 0.003/0.003 (U113 1) 0.003/0.003 (U114 1) 0.003/0.003 (U12 1) 0.003/0.003 (U121 1) 0.003/0.003 (U122 1) 0.003/0.003 (U13 1) 0.003/0.003 (U131 1) 0.003/0.003 (U132 1) 0.003/0.003 (U133 1) 0.003/0.003 (U134 1) 0.003/0.003 (U135 1) 0.003/0.003 (U136 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U44 1) 0.003/0.003 (U45 1) 0.003/0.003 (U46 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U81 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (U93 1) 0.003/0.003 (U94 1) 0.003/0.003 (U95 1) 0.003/0.003 (U96 1) 0.003/0.003 (isNat 1) 0.003/0.003 (isNatIList 1) 0.003/0.003 (isNatIListKind 1) 0.003/0.003 (isNatKind 1) 0.003/0.003 (isNatList 1) 0.003/0.003 (length 1) 0.003/0.003 (take 1 2) 0.003/0.003 (zeros) 0.003/0.003 (cons) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (nil) 0.003/0.003 (num0) 0.003/0.003 (s) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U102(tt,V1:S:S,V2:S:S) -> U103(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U103(tt,V1:S:S,V2:S:S) -> U104(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U104(tt,V1:S:S,V2:S:S) -> U105(isNat(V1:S:S),V2:S:S) 0.003/0.003 U105(tt,V2:S:S) -> U106(isNatIList(V2:S:S)) 0.003/0.003 U106(tt) -> tt 0.003/0.003 U11(tt,V1:S:S) -> U12(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 U111(tt,L:S:S,N:S:S) -> U112(isNatIListKind(L:S:S),L:S:S,N:S:S) 0.003/0.003 U112(tt,L:S:S,N:S:S) -> U113(isNat(N:S:S),L:S:S,N:S:S) 0.003/0.003 U113(tt,L:S:S,N:S:S) -> U114(isNatKind(N:S:S),L:S:S) 0.003/0.003 U114(tt,L:S:S) -> s(length(L:S:S)) 0.003/0.003 U12(tt,V1:S:S) -> U13(isNatList(V1:S:S)) 0.003/0.003 U121(tt,IL:S:S) -> U122(isNatIListKind(IL:S:S)) 0.003/0.003 U122(tt) -> nil 0.003/0.003 U13(tt) -> tt 0.003/0.003 U131(tt,IL:S:S,M:S:S,N:S:S) -> U132(isNatIListKind(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U132(tt,IL:S:S,M:S:S,N:S:S) -> U133(isNat(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U133(tt,IL:S:S,M:S:S,N:S:S) -> U134(isNatKind(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U134(tt,IL:S:S,M:S:S,N:S:S) -> U135(isNat(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U135(tt,IL:S:S,M:S:S,N:S:S) -> U136(isNatKind(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U136(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.003/0.003 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 U32(tt,V:S:S) -> U33(isNatList(V:S:S)) 0.003/0.003 U33(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U42(tt,V1:S:S,V2:S:S) -> U43(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U43(tt,V1:S:S,V2:S:S) -> U44(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U44(tt,V1:S:S,V2:S:S) -> U45(isNat(V1:S:S),V2:S:S) 0.003/0.003 U45(tt,V2:S:S) -> U46(isNatIList(V2:S:S)) 0.003/0.003 U46(tt) -> tt 0.003/0.003 U51(tt,V2:S:S) -> U52(isNatIListKind(V2:S:S)) 0.003/0.003 U52(tt) -> tt 0.003/0.003 U61(tt,V2:S:S) -> U62(isNatIListKind(V2:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt) -> tt 0.003/0.003 U81(tt) -> tt 0.003/0.003 U91(tt,V1:S:S,V2:S:S) -> U92(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U92(tt,V1:S:S,V2:S:S) -> U93(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U93(tt,V1:S:S,V2:S:S) -> U94(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U94(tt,V1:S:S,V2:S:S) -> U95(isNat(V1:S:S),V2:S:S) 0.003/0.003 U95(tt,V2:S:S) -> U96(isNatList(V2:S:S)) 0.003/0.003 U96(tt) -> tt 0.003/0.003 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 isNat(num0) -> tt 0.003/0.003 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatIList(zeros) -> tt 0.003/0.003 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 isNatIListKind(take(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(zeros) -> tt 0.003/0.003 isNatIListKind(cons(V1:S:S,V2:S:S)) -> U51(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(nil) -> tt 0.003/0.003 isNatKind(length(V1:S:S)) -> U71(isNatIListKind(V1:S:S)) 0.003/0.003 isNatKind(num0) -> tt 0.003/0.003 isNatKind(s(V1:S:S)) -> U81(isNatKind(V1:S:S)) 0.003/0.003 isNatList(take(V1:S:S,V2:S:S)) -> U101(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(cons(V1:S:S,V2:S:S)) -> U91(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(nil) -> tt 0.003/0.003 length(cons(N:S:S,L:S:S)) -> U111(isNatList(L:S:S),L:S:S,N:S:S) 0.003/0.003 length(nil) -> num0 0.003/0.003 take(num0,IL:S:S) -> U121(isNatIList(IL:S:S),IL:S:S) 0.003/0.003 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 zeros -> cons(num0,zeros) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 CleanTRS Processor: 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (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) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U105 1) 0.003/0.003 (U106 1) 0.003/0.003 (U11 1) 0.003/0.003 (U111 1) 0.003/0.003 (U112 1) 0.003/0.003 (U113 1) 0.003/0.003 (U114 1) 0.003/0.003 (U12 1) 0.003/0.003 (U121 1) 0.003/0.003 (U122 1) 0.003/0.003 (U13 1) 0.003/0.003 (U131 1) 0.003/0.003 (U132 1) 0.003/0.003 (U133 1) 0.003/0.003 (U134 1) 0.003/0.003 (U135 1) 0.003/0.003 (U136 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U44 1) 0.003/0.003 (U45 1) 0.003/0.003 (U46 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U81 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (U93 1) 0.003/0.003 (U94 1) 0.003/0.003 (U95 1) 0.003/0.003 (U96 1) 0.003/0.003 (isNat 1) 0.003/0.003 (isNatIList 1) 0.003/0.003 (isNatIListKind 1) 0.003/0.003 (isNatKind 1) 0.003/0.003 (isNatList 1) 0.003/0.003 (length 1) 0.003/0.003 (take 1 2) 0.003/0.003 (zeros) 0.003/0.003 (cons) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (nil) 0.003/0.003 (num0) 0.003/0.003 (s) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U102(tt,V1:S:S,V2:S:S) -> U103(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U103(tt,V1:S:S,V2:S:S) -> U104(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U104(tt,V1:S:S,V2:S:S) -> U105(isNat(V1:S:S),V2:S:S) 0.003/0.003 U105(tt,V2:S:S) -> U106(isNatIList(V2:S:S)) 0.003/0.003 U106(tt) -> tt 0.003/0.003 U11(tt,V1:S:S) -> U12(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 U111(tt,L:S:S,N:S:S) -> U112(isNatIListKind(L:S:S),L:S:S,N:S:S) 0.003/0.003 U112(tt,L:S:S,N:S:S) -> U113(isNat(N:S:S),L:S:S,N:S:S) 0.003/0.003 U113(tt,L:S:S,N:S:S) -> U114(isNatKind(N:S:S),L:S:S) 0.003/0.003 U114(tt,L:S:S) -> s(length(L:S:S)) 0.003/0.003 U12(tt,V1:S:S) -> U13(isNatList(V1:S:S)) 0.003/0.003 U121(tt,IL:S:S) -> U122(isNatIListKind(IL:S:S)) 0.003/0.003 U122(tt) -> nil 0.003/0.003 U13(tt) -> tt 0.003/0.003 U131(tt,IL:S:S,M:S:S,N:S:S) -> U132(isNatIListKind(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U132(tt,IL:S:S,M:S:S,N:S:S) -> U133(isNat(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U133(tt,IL:S:S,M:S:S,N:S:S) -> U134(isNatKind(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U134(tt,IL:S:S,M:S:S,N:S:S) -> U135(isNat(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U135(tt,IL:S:S,M:S:S,N:S:S) -> U136(isNatKind(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U136(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.003/0.003 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 U32(tt,V:S:S) -> U33(isNatList(V:S:S)) 0.003/0.003 U33(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U42(tt,V1:S:S,V2:S:S) -> U43(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U43(tt,V1:S:S,V2:S:S) -> U44(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U44(tt,V1:S:S,V2:S:S) -> U45(isNat(V1:S:S),V2:S:S) 0.003/0.003 U45(tt,V2:S:S) -> U46(isNatIList(V2:S:S)) 0.003/0.003 U46(tt) -> tt 0.003/0.003 U51(tt,V2:S:S) -> U52(isNatIListKind(V2:S:S)) 0.003/0.003 U52(tt) -> tt 0.003/0.003 U61(tt,V2:S:S) -> U62(isNatIListKind(V2:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt) -> tt 0.003/0.003 U81(tt) -> tt 0.003/0.003 U91(tt,V1:S:S,V2:S:S) -> U92(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U92(tt,V1:S:S,V2:S:S) -> U93(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U93(tt,V1:S:S,V2:S:S) -> U94(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U94(tt,V1:S:S,V2:S:S) -> U95(isNat(V1:S:S),V2:S:S) 0.003/0.003 U95(tt,V2:S:S) -> U96(isNatList(V2:S:S)) 0.003/0.003 U96(tt) -> tt 0.003/0.003 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 isNat(num0) -> tt 0.003/0.003 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatIList(zeros) -> tt 0.003/0.003 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 isNatIListKind(take(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(zeros) -> tt 0.003/0.003 isNatIListKind(cons(V1:S:S,V2:S:S)) -> U51(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(nil) -> tt 0.003/0.003 isNatKind(length(V1:S:S)) -> U71(isNatIListKind(V1:S:S)) 0.003/0.003 isNatKind(num0) -> tt 0.003/0.003 isNatKind(s(V1:S:S)) -> U81(isNatKind(V1:S:S)) 0.003/0.003 isNatList(take(V1:S:S,V2:S:S)) -> U101(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(cons(V1:S:S,V2:S:S)) -> U91(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(nil) -> tt 0.003/0.003 length(cons(N:S:S,L:S:S)) -> U111(isNatList(L:S:S),L:S:S,N:S:S) 0.003/0.003 length(nil) -> num0 0.003/0.003 take(num0,IL:S:S) -> U121(isNatIList(IL:S:S),IL:S:S) 0.003/0.003 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 zeros -> cons(num0,zeros) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 Modular Confluence Combinations Decomposition Processor: 0.003/0.003 It is a CTRS -> No modular confluence 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 CS-TRS Processor: 0.003/0.003 R is a CS-TRS 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (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) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U105 1) 0.003/0.003 (U106 1) 0.003/0.003 (U11 1) 0.003/0.003 (U111 1) 0.003/0.003 (U112 1) 0.003/0.003 (U113 1) 0.003/0.003 (U114 1) 0.003/0.003 (U12 1) 0.003/0.003 (U121 1) 0.003/0.003 (U122 1) 0.003/0.003 (U13 1) 0.003/0.003 (U131 1) 0.003/0.003 (U132 1) 0.003/0.003 (U133 1) 0.003/0.003 (U134 1) 0.003/0.003 (U135 1) 0.003/0.003 (U136 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U44 1) 0.003/0.003 (U45 1) 0.003/0.003 (U46 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U81 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (U93 1) 0.003/0.003 (U94 1) 0.003/0.003 (U95 1) 0.003/0.003 (U96 1) 0.003/0.003 (isNat 1) 0.003/0.003 (isNatIList 1) 0.003/0.003 (isNatIListKind 1) 0.003/0.003 (isNatKind 1) 0.003/0.003 (isNatList 1) 0.003/0.003 (length 1) 0.003/0.003 (take 1 2) 0.003/0.003 (zeros) 0.003/0.003 (cons) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (nil) 0.003/0.003 (num0) 0.003/0.003 (s) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U102(tt,V1:S:S,V2:S:S) -> U103(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U103(tt,V1:S:S,V2:S:S) -> U104(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U104(tt,V1:S:S,V2:S:S) -> U105(isNat(V1:S:S),V2:S:S) 0.003/0.003 U105(tt,V2:S:S) -> U106(isNatIList(V2:S:S)) 0.003/0.003 U106(tt) -> tt 0.003/0.003 U11(tt,V1:S:S) -> U12(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 U111(tt,L:S:S,N:S:S) -> U112(isNatIListKind(L:S:S),L:S:S,N:S:S) 0.003/0.003 U112(tt,L:S:S,N:S:S) -> U113(isNat(N:S:S),L:S:S,N:S:S) 0.003/0.003 U113(tt,L:S:S,N:S:S) -> U114(isNatKind(N:S:S),L:S:S) 0.003/0.003 U114(tt,L:S:S) -> s(length(L:S:S)) 0.003/0.003 U12(tt,V1:S:S) -> U13(isNatList(V1:S:S)) 0.003/0.003 U121(tt,IL:S:S) -> U122(isNatIListKind(IL:S:S)) 0.003/0.003 U122(tt) -> nil 0.003/0.003 U13(tt) -> tt 0.003/0.003 U131(tt,IL:S:S,M:S:S,N:S:S) -> U132(isNatIListKind(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U132(tt,IL:S:S,M:S:S,N:S:S) -> U133(isNat(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U133(tt,IL:S:S,M:S:S,N:S:S) -> U134(isNatKind(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U134(tt,IL:S:S,M:S:S,N:S:S) -> U135(isNat(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U135(tt,IL:S:S,M:S:S,N:S:S) -> U136(isNatKind(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U136(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.003/0.003 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 U32(tt,V:S:S) -> U33(isNatList(V:S:S)) 0.003/0.003 U33(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U42(tt,V1:S:S,V2:S:S) -> U43(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U43(tt,V1:S:S,V2:S:S) -> U44(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U44(tt,V1:S:S,V2:S:S) -> U45(isNat(V1:S:S),V2:S:S) 0.003/0.003 U45(tt,V2:S:S) -> U46(isNatIList(V2:S:S)) 0.003/0.003 U46(tt) -> tt 0.003/0.003 U51(tt,V2:S:S) -> U52(isNatIListKind(V2:S:S)) 0.003/0.003 U52(tt) -> tt 0.003/0.003 U61(tt,V2:S:S) -> U62(isNatIListKind(V2:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt) -> tt 0.003/0.003 U81(tt) -> tt 0.003/0.003 U91(tt,V1:S:S,V2:S:S) -> U92(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U92(tt,V1:S:S,V2:S:S) -> U93(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U93(tt,V1:S:S,V2:S:S) -> U94(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U94(tt,V1:S:S,V2:S:S) -> U95(isNat(V1:S:S),V2:S:S) 0.003/0.003 U95(tt,V2:S:S) -> U96(isNatList(V2:S:S)) 0.003/0.003 U96(tt) -> tt 0.003/0.003 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 isNat(num0) -> tt 0.003/0.003 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatIList(zeros) -> tt 0.003/0.003 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 isNatIListKind(take(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(zeros) -> tt 0.003/0.003 isNatIListKind(cons(V1:S:S,V2:S:S)) -> U51(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(nil) -> tt 0.003/0.003 isNatKind(length(V1:S:S)) -> U71(isNatIListKind(V1:S:S)) 0.003/0.003 isNatKind(num0) -> tt 0.003/0.003 isNatKind(s(V1:S:S)) -> U81(isNatKind(V1:S:S)) 0.003/0.003 isNatList(take(V1:S:S,V2:S:S)) -> U101(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(cons(V1:S:S,V2:S:S)) -> U91(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(nil) -> tt 0.003/0.003 length(cons(N:S:S,L:S:S)) -> U111(isNatList(L:S:S),L:S:S,N:S:S) 0.003/0.003 length(nil) -> num0 0.003/0.003 take(num0,IL:S:S) -> U121(isNatIList(IL:S:S),IL:S:S) 0.003/0.003 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 zeros -> cons(num0,zeros) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 Huet Levy Processor: 0.003/0.003 -> Rules: 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U102(tt,V1:S:S,V2:S:S) -> U103(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U103(tt,V1:S:S,V2:S:S) -> U104(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U104(tt,V1:S:S,V2:S:S) -> U105(isNat(V1:S:S),V2:S:S) 0.003/0.003 U105(tt,V2:S:S) -> U106(isNatIList(V2:S:S)) 0.003/0.003 U106(tt) -> tt 0.003/0.003 U11(tt,V1:S:S) -> U12(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 U111(tt,L:S:S,N:S:S) -> U112(isNatIListKind(L:S:S),L:S:S,N:S:S) 0.003/0.003 U112(tt,L:S:S,N:S:S) -> U113(isNat(N:S:S),L:S:S,N:S:S) 0.003/0.003 U113(tt,L:S:S,N:S:S) -> U114(isNatKind(N:S:S),L:S:S) 0.003/0.003 U114(tt,L:S:S) -> s(length(L:S:S)) 0.003/0.003 U12(tt,V1:S:S) -> U13(isNatList(V1:S:S)) 0.003/0.003 U121(tt,IL:S:S) -> U122(isNatIListKind(IL:S:S)) 0.003/0.003 U122(tt) -> nil 0.003/0.003 U13(tt) -> tt 0.003/0.003 U131(tt,IL:S:S,M:S:S,N:S:S) -> U132(isNatIListKind(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U132(tt,IL:S:S,M:S:S,N:S:S) -> U133(isNat(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U133(tt,IL:S:S,M:S:S,N:S:S) -> U134(isNatKind(M:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U134(tt,IL:S:S,M:S:S,N:S:S) -> U135(isNat(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U135(tt,IL:S:S,M:S:S,N:S:S) -> U136(isNatKind(N:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 U136(tt,IL:S:S,M:S:S,N:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S)) 0.003/0.003 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 U32(tt,V:S:S) -> U33(isNatList(V:S:S)) 0.003/0.003 U33(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U42(tt,V1:S:S,V2:S:S) -> U43(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U43(tt,V1:S:S,V2:S:S) -> U44(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U44(tt,V1:S:S,V2:S:S) -> U45(isNat(V1:S:S),V2:S:S) 0.003/0.003 U45(tt,V2:S:S) -> U46(isNatIList(V2:S:S)) 0.003/0.003 U46(tt) -> tt 0.003/0.003 U51(tt,V2:S:S) -> U52(isNatIListKind(V2:S:S)) 0.003/0.003 U52(tt) -> tt 0.003/0.003 U61(tt,V2:S:S) -> U62(isNatIListKind(V2:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt) -> tt 0.003/0.003 U81(tt) -> tt 0.003/0.003 U91(tt,V1:S:S,V2:S:S) -> U92(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 U92(tt,V1:S:S,V2:S:S) -> U93(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U93(tt,V1:S:S,V2:S:S) -> U94(isNatIListKind(V2:S:S),V1:S:S,V2:S:S) 0.003/0.003 U94(tt,V1:S:S,V2:S:S) -> U95(isNat(V1:S:S),V2:S:S) 0.003/0.003 U95(tt,V2:S:S) -> U96(isNatList(V2:S:S)) 0.003/0.003 U96(tt) -> tt 0.003/0.003 isNat(length(V1:S:S)) -> U11(isNatIListKind(V1:S:S),V1:S:S) 0.003/0.003 isNat(num0) -> tt 0.003/0.003 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatIList(zeros) -> tt 0.003/0.003 isNatIList(cons(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatIList(V:S:S) -> U31(isNatIListKind(V:S:S),V:S:S) 0.003/0.003 isNatIListKind(take(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(zeros) -> tt 0.003/0.003 isNatIListKind(cons(V1:S:S,V2:S:S)) -> U51(isNatKind(V1:S:S),V2:S:S) 0.003/0.003 isNatIListKind(nil) -> tt 0.003/0.003 isNatKind(length(V1:S:S)) -> U71(isNatIListKind(V1:S:S)) 0.003/0.003 isNatKind(num0) -> tt 0.003/0.003 isNatKind(s(V1:S:S)) -> U81(isNatKind(V1:S:S)) 0.003/0.003 isNatList(take(V1:S:S,V2:S:S)) -> U101(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(cons(V1:S:S,V2:S:S)) -> U91(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.003/0.003 isNatList(nil) -> tt 0.003/0.003 length(cons(N:S:S,L:S:S)) -> U111(isNatList(L:S:S),L:S:S,N:S:S) 0.003/0.003 length(nil) -> num0 0.003/0.003 take(num0,IL:S:S) -> U121(isNatIList(IL:S:S),IL:S:S) 0.003/0.003 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S) 0.003/0.003 zeros -> cons(num0,zeros) 0.003/0.003 -> Vars: 0.003/0.003 V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V1:S, L:S, N:S, L:S, N:S, L:S, N:S, L:S, V1:S, IL:S, IL:S, M:S, N:S, IL:S, M:S, N:S, IL:S, M:S, N:S, IL:S, M:S, N:S, IL:S, M:S, N:S, IL:S, M:S, N:S, V1:S, V1:S, V:S, V:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V2:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2: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.003/0.003 -> UVars: 0.003/0.003 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [L:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S, N:S]) 0.003/0.003 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S, N:S]) 0.003/0.003 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S]) 0.003/0.003 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [L:S], UV-RFrozen: [L:S]) 0.003/0.003 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [IL:S], UV-LFrozen: [IL:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [IL:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [V:S], UV-LFrozen: [V:S], UV-RFrozen: [V:S]) 0.003/0.003 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [V:S], UV-LFrozen: [V:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 46, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 49, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 50, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 51, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: [V:S]) 0.003/0.003 (UV-RuleId: 52, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 56, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 57, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 58, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 59, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 62, UV-LActive: [], UV-RActive: [L:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S, N:S]) 0.003/0.003 (UV-RuleId: 63, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 64, UV-LActive: [IL:S], UV-RActive: [IL:S], UV-LFrozen: [], UV-RFrozen: [IL:S]) 0.003/0.003 (UV-RuleId: 65, UV-LActive: [], UV-RActive: [IL:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S]) 0.003/0.003 (UV-RuleId: 66, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 -> FVars: 0.003/0.003 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, x58, x59, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x72, x73, x74, x75, x76, x77, x78, x79, x80, x81, x82, x83, x84, x85, x86, x87, x88, x89, x90 0.003/0.003 -> PVars: 0.003/0.003 V1:S: [x9, x11, x13, x15, x18, x26, x46, x47, x50, x52, x54, x56, x61, x63, x65, x67, x70, x71, x72, x75, x77, x79, x80, x81, x83], V2:S: [x10, x12, x14, x16, x17, x51, x53, x55, x57, x58, x59, x60, x62, x64, x66, x68, x69, x73, x76, x78, x82, x84], L:S: [x19, x21, x23, x25, x85], N:S: [x20, x22, x24, x30, x33, x36, x39, x42, x45, x86, x90], IL:S: [x27, x28, x31, x34, x37, x40, x43, x87, x88], M:S: [x29, x32, x35, x38, x41, x44, x89], V:S: [x48, x49, x74] 0.003/0.003 0.003/0.003 -> Rlps: 0.003/0.003 (rule: U101(tt,x9:S,x10:S) -> U102(isNatKind(x9:S),x9:S,x10:S), id: 1, possubterms: U101(tt,x9:S,x10:S)->[], tt->[1]) 0.003/0.003 (rule: U102(tt,x11:S,x12:S) -> U103(isNatIListKind(x12:S),x11:S,x12:S), id: 2, possubterms: U102(tt,x11:S,x12:S)->[], tt->[1]) 0.003/0.003 (rule: U103(tt,x13:S,x14:S) -> U104(isNatIListKind(x14:S),x13:S,x14:S), id: 3, possubterms: U103(tt,x13:S,x14:S)->[], tt->[1]) 0.003/0.003 (rule: U104(tt,x15:S,x16:S) -> U105(isNat(x15:S),x16:S), id: 4, possubterms: U104(tt,x15:S,x16:S)->[], tt->[1]) 0.003/0.003 (rule: U105(tt,x17:S) -> U106(isNatIList(x17:S)), id: 5, possubterms: U105(tt,x17:S)->[], tt->[1]) 0.003/0.003 (rule: U106(tt) -> tt, id: 6, possubterms: U106(tt)->[], tt->[1]) 0.003/0.003 (rule: U11(tt,x18:S) -> U12(isNatIListKind(x18:S),x18:S), id: 7, possubterms: U11(tt,x18:S)->[], tt->[1]) 0.003/0.003 (rule: U111(tt,x19:S,x20:S) -> U112(isNatIListKind(x19:S),x19:S,x20:S), id: 8, possubterms: U111(tt,x19:S,x20:S)->[], tt->[1]) 0.003/0.003 (rule: U112(tt,x21:S,x22:S) -> U113(isNat(x22:S),x21:S,x22:S), id: 9, possubterms: U112(tt,x21:S,x22:S)->[], tt->[1]) 0.003/0.003 (rule: U113(tt,x23:S,x24:S) -> U114(isNatKind(x24:S),x23:S), id: 10, possubterms: U113(tt,x23:S,x24:S)->[], tt->[1]) 0.003/0.003 (rule: U114(tt,x25:S) -> s(length(x25:S)), id: 11, possubterms: U114(tt,x25:S)->[], tt->[1]) 0.003/0.003 (rule: U12(tt,x26:S) -> U13(isNatList(x26:S)), id: 12, possubterms: U12(tt,x26:S)->[], tt->[1]) 0.003/0.003 (rule: U121(tt,x27:S) -> U122(isNatIListKind(x27:S)), id: 13, possubterms: U121(tt,x27:S)->[], tt->[1]) 0.003/0.003 (rule: U122(tt) -> nil, id: 14, possubterms: U122(tt)->[], tt->[1]) 0.003/0.003 (rule: U13(tt) -> tt, id: 15, possubterms: U13(tt)->[], tt->[1]) 0.003/0.003 (rule: U131(tt,x28:S,x29:S,x30:S) -> U132(isNatIListKind(x28:S),x28:S,x29:S,x30:S), id: 16, possubterms: U131(tt,x28:S,x29:S,x30:S)->[], tt->[1]) 0.003/0.003 (rule: U132(tt,x31:S,x32:S,x33:S) -> U133(isNat(x32:S),x31:S,x32:S,x33:S), id: 17, possubterms: U132(tt,x31:S,x32:S,x33:S)->[], tt->[1]) 0.003/0.003 (rule: U133(tt,x34:S,x35:S,x36:S) -> U134(isNatKind(x35:S),x34:S,x35:S,x36:S), id: 18, possubterms: U133(tt,x34:S,x35:S,x36:S)->[], tt->[1]) 0.003/0.003 (rule: U134(tt,x37:S,x38:S,x39:S) -> U135(isNat(x39:S),x37:S,x38:S,x39:S), id: 19, possubterms: U134(tt,x37:S,x38:S,x39:S)->[], tt->[1]) 0.003/0.003 (rule: U135(tt,x40:S,x41:S,x42:S) -> U136(isNatKind(x42:S),x40:S,x41:S,x42:S), id: 20, possubterms: U135(tt,x40:S,x41:S,x42:S)->[], tt->[1]) 0.003/0.003 (rule: U136(tt,x43:S,x44:S,x45:S) -> cons(x45:S,take(x44:S,x43:S)), id: 21, possubterms: U136(tt,x43:S,x44:S,x45:S)->[], tt->[1]) 0.003/0.003 (rule: U21(tt,x46:S) -> U22(isNatKind(x46:S),x46:S), id: 22, possubterms: U21(tt,x46:S)->[], tt->[1]) 0.003/0.003 (rule: U22(tt,x47:S) -> U23(isNat(x47:S)), id: 23, possubterms: U22(tt,x47:S)->[], tt->[1]) 0.003/0.003 (rule: U23(tt) -> tt, id: 24, possubterms: U23(tt)->[], tt->[1]) 0.003/0.003 (rule: U31(tt,x48:S) -> U32(isNatIListKind(x48:S),x48:S), id: 25, possubterms: U31(tt,x48:S)->[], tt->[1]) 0.003/0.003 (rule: U32(tt,x49:S) -> U33(isNatList(x49:S)), id: 26, possubterms: U32(tt,x49:S)->[], tt->[1]) 0.003/0.003 (rule: U33(tt) -> tt, id: 27, possubterms: U33(tt)->[], tt->[1]) 0.003/0.003 (rule: U41(tt,x50:S,x51:S) -> U42(isNatKind(x50:S),x50:S,x51:S), id: 28, possubterms: U41(tt,x50:S,x51:S)->[], tt->[1]) 0.003/0.003 (rule: U42(tt,x52:S,x53:S) -> U43(isNatIListKind(x53:S),x52:S,x53:S), id: 29, possubterms: U42(tt,x52:S,x53:S)->[], tt->[1]) 0.003/0.003 (rule: U43(tt,x54:S,x55:S) -> U44(isNatIListKind(x55:S),x54:S,x55:S), id: 30, possubterms: U43(tt,x54:S,x55:S)->[], tt->[1]) 0.003/0.003 (rule: U44(tt,x56:S,x57:S) -> U45(isNat(x56:S),x57:S), id: 31, possubterms: U44(tt,x56:S,x57:S)->[], tt->[1]) 0.003/0.003 (rule: U45(tt,x58:S) -> U46(isNatIList(x58:S)), id: 32, possubterms: U45(tt,x58:S)->[], tt->[1]) 0.003/0.003 (rule: U46(tt) -> tt, id: 33, possubterms: U46(tt)->[], tt->[1]) 0.003/0.003 (rule: U51(tt,x59:S) -> U52(isNatIListKind(x59:S)), id: 34, possubterms: U51(tt,x59:S)->[], tt->[1]) 0.003/0.003 (rule: U52(tt) -> tt, id: 35, possubterms: U52(tt)->[], tt->[1]) 0.003/0.003 (rule: U61(tt,x60:S) -> U62(isNatIListKind(x60:S)), id: 36, possubterms: U61(tt,x60:S)->[], tt->[1]) 0.003/0.003 (rule: U62(tt) -> tt, id: 37, possubterms: U62(tt)->[], tt->[1]) 0.003/0.003 (rule: U71(tt) -> tt, id: 38, possubterms: U71(tt)->[], tt->[1]) 0.003/0.003 (rule: U81(tt) -> tt, id: 39, possubterms: U81(tt)->[], tt->[1]) 0.003/0.003 (rule: U91(tt,x61:S,x62:S) -> U92(isNatKind(x61:S),x61:S,x62:S), id: 40, possubterms: U91(tt,x61:S,x62:S)->[], tt->[1]) 0.003/0.003 (rule: U92(tt,x63:S,x64:S) -> U93(isNatIListKind(x64:S),x63:S,x64:S), id: 41, possubterms: U92(tt,x63:S,x64:S)->[], tt->[1]) 0.003/0.003 (rule: U93(tt,x65:S,x66:S) -> U94(isNatIListKind(x66:S),x65:S,x66:S), id: 42, possubterms: U93(tt,x65:S,x66:S)->[], tt->[1]) 0.003/0.003 (rule: U94(tt,x67:S,x68:S) -> U95(isNat(x67:S),x68:S), id: 43, possubterms: U94(tt,x67:S,x68:S)->[], tt->[1]) 0.003/0.003 (rule: U95(tt,x69:S) -> U96(isNatList(x69:S)), id: 44, possubterms: U95(tt,x69:S)->[], tt->[1]) 0.003/0.003 (rule: U96(tt) -> tt, id: 45, possubterms: U96(tt)->[], tt->[1]) 0.003/0.003 (rule: isNat(length(x70:S)) -> U11(isNatIListKind(x70:S),x70:S), id: 46, possubterms: isNat(length(x70:S))->[], length(x70:S)->[1]) 0.003/0.003 (rule: isNat(num0) -> tt, id: 47, possubterms: isNat(num0)->[], num0->[1]) 0.003/0.003 (rule: isNat(s(x71:S)) -> U21(isNatKind(x71:S),x71:S), id: 48, possubterms: isNat(s(x71:S))->[], s(x71:S)->[1]) 0.003/0.003 (rule: isNatIList(zeros) -> tt, id: 49, possubterms: isNatIList(zeros)->[], zeros->[1]) 0.003/0.003 (rule: isNatIList(cons(x72:S,x73:S)) -> U41(isNatKind(x72:S),x72:S,x73:S), id: 50, possubterms: isNatIList(cons(x72:S,x73:S))->[], cons(x72:S,x73:S)->[1]) 0.003/0.003 (rule: isNatIList(x74:S) -> U31(isNatIListKind(x74:S),x74:S), id: 51, possubterms: isNatIList(x74:S)->[]) 0.003/0.003 (rule: isNatIListKind(take(x75:S,x76:S)) -> U61(isNatKind(x75:S),x76:S), id: 52, possubterms: isNatIListKind(take(x75:S,x76:S))->[], take(x75:S,x76:S)->[1]) 0.003/0.003 (rule: isNatIListKind(zeros) -> tt, id: 53, possubterms: isNatIListKind(zeros)->[], zeros->[1]) 0.003/0.003 (rule: isNatIListKind(cons(x77:S,x78:S)) -> U51(isNatKind(x77:S),x78:S), id: 54, possubterms: isNatIListKind(cons(x77:S,x78:S))->[], cons(x77:S,x78:S)->[1]) 0.003/0.003 (rule: isNatIListKind(nil) -> tt, id: 55, possubterms: isNatIListKind(nil)->[], nil->[1]) 0.003/0.003 (rule: isNatKind(length(x79:S)) -> U71(isNatIListKind(x79:S)), id: 56, possubterms: isNatKind(length(x79:S))->[], length(x79:S)->[1]) 0.003/0.003 (rule: isNatKind(num0) -> tt, id: 57, possubterms: isNatKind(num0)->[], num0->[1]) 0.003/0.003 (rule: isNatKind(s(x80:S)) -> U81(isNatKind(x80:S)), id: 58, possubterms: isNatKind(s(x80:S))->[], s(x80:S)->[1]) 0.003/0.003 (rule: isNatList(take(x81:S,x82:S)) -> U101(isNatKind(x81:S),x81:S,x82:S), id: 59, possubterms: isNatList(take(x81:S,x82:S))->[], take(x81:S,x82:S)->[1]) 0.003/0.003 (rule: isNatList(cons(x83:S,x84:S)) -> U91(isNatKind(x83:S),x83:S,x84:S), id: 60, possubterms: isNatList(cons(x83:S,x84:S))->[], cons(x83:S,x84:S)->[1]) 0.003/0.003 (rule: isNatList(nil) -> tt, id: 61, possubterms: isNatList(nil)->[], nil->[1]) 0.003/0.003 (rule: length(cons(x86:S,x85:S)) -> U111(isNatList(x85:S),x85:S,x86:S), id: 62, possubterms: length(cons(x86:S,x85:S))->[], cons(x86:S,x85:S)->[1]) 0.003/0.003 (rule: length(nil) -> num0, id: 63, possubterms: length(nil)->[], nil->[1]) 0.003/0.003 (rule: take(num0,x87:S) -> U121(isNatIList(x87:S),x87:S), id: 64, possubterms: take(num0,x87:S)->[], num0->[1]) 0.003/0.003 (rule: take(s(x89:S),cons(x90:S,x88:S)) -> U131(isNatIList(x88:S),x88:S,x89:S,x90:S), id: 65, possubterms: take(s(x89:S),cons(x90:S,x88:S))->[], s(x89:S)->[1], cons(x90:S,x88:S)->[2]) 0.003/0.003 (rule: zeros -> cons(num0,zeros), id: 66, possubterms: zeros->[]) 0.003/0.003 0.003/0.003 -> Unifications: 0.003/0.003 (R46 unifies with R62 at p: [1], l: isNat(length(x70:S)), lp: length(x70:S), sig: {x70:S -> cons(N:S:S,L:S:S)}, l': length(cons(N:S:S,L:S:S)), r: U11(isNatIListKind(x70:S),x70:S), r': U111(isNatList(L:S:S),L:S:S,N:S:S)) 0.003/0.003 (R46 unifies with R63 at p: [1], l: isNat(length(x70:S)), lp: length(x70:S), sig: {x70:S -> nil}, l': length(nil), r: U11(isNatIListKind(x70:S),x70:S), r': num0) 0.003/0.003 (R49 unifies with R66 at p: [1], l: isNatIList(zeros), lp: zeros, sig: {}, l': zeros, r: tt, r': cons(num0,zeros)) 0.003/0.003 (R51 unifies with R49 at p: [], l: isNatIList(x74:S), lp: isNatIList(x74:S), sig: {x74:S -> zeros}, l': isNatIList(zeros), r: U31(isNatIListKind(x74:S),x74:S), r': tt) 0.003/0.003 (R51 unifies with R50 at p: [], l: isNatIList(x74:S), lp: isNatIList(x74:S), sig: {x74:S -> cons(V1:S:S,V2:S:S)}, l': isNatIList(cons(V1:S:S,V2:S:S)), r: U31(isNatIListKind(x74:S),x74:S), r': U41(isNatKind(V1:S:S),V1:S:S,V2:S:S)) 0.003/0.003 (R52 unifies with R64 at p: [1], l: isNatIListKind(take(x75:S,x76:S)), lp: take(x75:S,x76:S), sig: {x75:S -> num0,x76:S -> IL:S:S}, l': take(num0,IL:S:S), r: U61(isNatKind(x75:S),x76:S), r': U121(isNatIList(IL:S:S),IL:S:S)) 0.003/0.003 (R52 unifies with R65 at p: [1], l: isNatIListKind(take(x75:S,x76:S)), lp: take(x75:S,x76:S), sig: {x75:S -> s(M:S:S),x76:S -> cons(N:S:S,IL:S:S)}, l': take(s(M:S:S),cons(N:S:S,IL:S:S)), r: U61(isNatKind(x75:S),x76:S), r': U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S)) 0.003/0.003 (R53 unifies with R66 at p: [1], l: isNatIListKind(zeros), lp: zeros, sig: {}, l': zeros, r: tt, r': cons(num0,zeros)) 0.003/0.003 (R56 unifies with R62 at p: [1], l: isNatKind(length(x79:S)), lp: length(x79:S), sig: {x79:S -> cons(N:S:S,L:S:S)}, l': length(cons(N:S:S,L:S:S)), r: U71(isNatIListKind(x79:S)), r': U111(isNatList(L:S:S),L:S:S,N:S:S)) 0.003/0.003 (R56 unifies with R63 at p: [1], l: isNatKind(length(x79:S)), lp: length(x79:S), sig: {x79:S -> nil}, l': length(nil), r: U71(isNatIListKind(x79:S)), r': num0) 0.003/0.003 (R59 unifies with R64 at p: [1], l: isNatList(take(x81:S,x82:S)), lp: take(x81:S,x82:S), sig: {x81:S -> num0,x82:S -> IL:S:S}, l': take(num0,IL:S:S), r: U101(isNatKind(x81:S),x81:S,x82:S), r': U121(isNatIList(IL:S:S),IL:S:S)) 0.003/0.003 (R59 unifies with R65 at p: [1], l: isNatList(take(x81:S,x82:S)), lp: take(x81:S,x82:S), sig: {x81:S -> s(M:S:S),x82:S -> cons(N:S:S,IL:S:S)}, l': take(s(M:S:S),cons(N:S:S,IL:S:S)), r: U101(isNatKind(x81:S),x81:S,x82:S), r': U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S)) 0.003/0.003 0.003/0.003 -> Critical pairs info: 0.003/0.003 => Not trivial, Not overlay, NW0, N1 0.003/0.003 => Not trivial, Not overlay, NW0, N2 0.003/0.003 => Not trivial, Not overlay, NW0, N3 0.003/0.003 => Not trivial, Not overlay, NW0, N4 0.003/0.003 => Not trivial, Not overlay, NW0, N5 0.003/0.003 => Not trivial, Overlay, NW0, N6 0.003/0.003 => Not trivial, Not overlay, NW0, N7 0.003/0.003 => Not trivial, Not overlay, NW0, N8 0.003/0.003 => Not trivial, Not overlay, NW0, N9 0.003/0.003 => Not trivial, Not overlay, NW0, N10 0.003/0.003 => Not trivial, Not overlay, NW0, N11 0.003/0.003 => Not trivial, Overlay, NW0, N12 0.003/0.003 0.003/0.003 -> Problem conclusions: 0.003/0.003 Left linear, Not right linear, Not linear 0.003/0.003 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.003/0.003 Not Huet-Levy confluent, Not Newman confluent 0.003/0.003 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 No Convergence Brute Force Processor: 0.003/0.003 -> Rewritings: 0.003/0.003 s: isNatIListKind(U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S)) 0.003/0.003 Nodes: [0,1] 0.003/0.003 Edges: [(0,1)] 0.003/0.003 ID: 0 => ('isNatIListKind(U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S))', D0) 0.003/0.003 ID: 1 => ('isNatIListKind(U131(U31(isNatIListKind(IL:S:S),IL:S:S),IL:S:S,M:S:S,N:S:S))', D1, R51, P[1, 1], S{x74:S -> IL:S:S}), NR: 'U31(isNatIListKind(IL:S:S),IL:S:S)' 0.003/0.003 t: U61(isNatKind(s(M:S:S)),cons(N:S:S,IL:S:S)) 0.003/0.003 Nodes: [0,1] 0.003/0.003 Edges: [(0,1)] 0.003/0.003 ID: 0 => ('U61(isNatKind(s(M:S:S)),cons(N:S:S,IL:S:S))', D0) 0.003/0.003 ID: 1 => ('U61(U81(isNatKind(M:S:S)),cons(N:S:S,IL:S:S))', D1, R58, P[1], S{x80:S -> M:S:S}), NR: 'U81(isNatKind(M:S:S))' 0.003/0.003 isNatIListKind(U131(isNatIList(IL:S:S),IL:S:S,M:S:S,N:S:S)) ->* no union *<- U61(isNatKind(s(M:S:S)),cons(N:S:S,IL:S:S)) 0.003/0.003 "Not joinable" 0.003/0.003 0.003/0.003 The problem is not joinable. 0.003/0.003 0.02user 0.00system 0:00.03elapsed 81%CPU (0avgtext+0avgdata 12316maxresident)k 0.003/0.003 8inputs+0outputs (0major+1324minor)pagefaults 0swaps