0.001/0.001 NO 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S IL:S L:S M:S N:S V:S V1:S V2:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (U11 1) 0.001/0.001 (U21 1) 0.001/0.001 (U31 1) 0.001/0.001 (U41 1) 0.001/0.001 (U42 1) 0.001/0.001 (U51 1) 0.001/0.001 (U52 1) 0.001/0.001 (U61 1) 0.001/0.001 (U62 1) 0.001/0.001 (U71 1) 0.001/0.001 (U72 1) 0.001/0.001 (U81 1) 0.001/0.001 (U91 1) 0.001/0.001 (U92 1) 0.001/0.001 (U93 1) 0.001/0.001 (isNat) 0.001/0.001 (isNatIList) 0.001/0.001 (isNatList) 0.001/0.001 (length 1) 0.001/0.001 (take 1 2) 0.001/0.001 (zeros) 0.001/0.001 (0) 0.001/0.001 (cons 1) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (nil) 0.001/0.001 (s 1) 0.001/0.001 (tt) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 U11(tt) -> tt 0.001/0.001 U21(tt) -> tt 0.001/0.001 U31(tt) -> tt 0.001/0.001 U41(tt,V2:S) -> U42(isNatIList(V2:S)) 0.001/0.001 U42(tt) -> tt 0.001/0.001 U51(tt,V2:S) -> U52(isNatList(V2:S)) 0.001/0.001 U52(tt) -> tt 0.001/0.001 U61(tt,V2:S) -> U62(isNatIList(V2:S)) 0.001/0.001 U62(tt) -> tt 0.001/0.001 U71(tt,L:S,N:S) -> U72(isNat(N:S),L:S) 0.001/0.001 U72(tt,L:S) -> s(length(L:S)) 0.001/0.001 U81(tt) -> nil 0.001/0.001 U91(tt,IL:S,M:S,N:S) -> U92(isNat(M:S),IL:S,M:S,N:S) 0.001/0.001 U92(tt,IL:S,M:S,N:S) -> U93(isNat(N:S),IL:S,M:S,N:S) 0.001/0.001 U93(tt,IL:S,M:S,N:S) -> cons(N:S,take(M:S,IL:S)) 0.001/0.001 isNat(length(V1:S)) -> U11(isNatList(V1:S)) 0.001/0.001 isNat(0) -> tt 0.001/0.001 isNat(s(V1:S)) -> U21(isNat(V1:S)) 0.001/0.001 isNatIList(zeros) -> tt 0.001/0.001 isNatIList(cons(V1:S,V2:S)) -> U41(isNat(V1:S),V2:S) 0.001/0.001 isNatIList(V:S) -> U31(isNatList(V:S)) 0.001/0.001 isNatList(take(V1:S,V2:S)) -> U61(isNat(V1:S),V2:S) 0.001/0.001 isNatList(cons(V1:S,V2:S)) -> U51(isNat(V1:S),V2:S) 0.001/0.001 isNatList(nil) -> tt 0.001/0.001 length(cons(N:S,L:S)) -> U71(isNatList(L:S),L:S,N:S) 0.001/0.001 length(nil) -> 0 0.001/0.001 take(0,IL:S) -> U81(isNatIList(IL:S)) 0.001/0.001 take(s(M:S),cons(N:S,IL:S)) -> U91(isNatIList(IL:S),IL:S,M:S,N:S) 0.001/0.001 zeros -> cons(0,zeros) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 CleanTRS Processor: 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S IL:S L:S M:S N:S V:S V1:S V2:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (U11 1) 0.001/0.001 (U21 1) 0.001/0.001 (U31 1) 0.001/0.001 (U41 1) 0.001/0.001 (U42 1) 0.001/0.001 (U51 1) 0.001/0.001 (U52 1) 0.001/0.001 (U61 1) 0.001/0.001 (U62 1) 0.001/0.001 (U71 1) 0.001/0.001 (U72 1) 0.001/0.001 (U81 1) 0.001/0.001 (U91 1) 0.001/0.001 (U92 1) 0.001/0.001 (U93 1) 0.001/0.001 (isNat) 0.001/0.001 (isNatIList) 0.001/0.001 (isNatList) 0.001/0.001 (length 1) 0.001/0.001 (take 1 2) 0.001/0.001 (zeros) 0.001/0.001 (0) 0.001/0.001 (cons 1) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (nil) 0.001/0.001 (s 1) 0.001/0.001 (tt) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 U11(tt) -> tt 0.001/0.001 U21(tt) -> tt 0.001/0.001 U31(tt) -> tt 0.001/0.001 U41(tt,V2:S) -> U42(isNatIList(V2:S)) 0.001/0.001 U42(tt) -> tt 0.001/0.001 U51(tt,V2:S) -> U52(isNatList(V2:S)) 0.001/0.001 U52(tt) -> tt 0.001/0.001 U61(tt,V2:S) -> U62(isNatIList(V2:S)) 0.001/0.001 U62(tt) -> tt 0.001/0.001 U71(tt,L:S,N:S) -> U72(isNat(N:S),L:S) 0.001/0.001 U72(tt,L:S) -> s(length(L:S)) 0.001/0.001 U81(tt) -> nil 0.001/0.001 U91(tt,IL:S,M:S,N:S) -> U92(isNat(M:S),IL:S,M:S,N:S) 0.001/0.001 U92(tt,IL:S,M:S,N:S) -> U93(isNat(N:S),IL:S,M:S,N:S) 0.001/0.001 U93(tt,IL:S,M:S,N:S) -> cons(N:S,take(M:S,IL:S)) 0.001/0.001 isNat(length(V1:S)) -> U11(isNatList(V1:S)) 0.001/0.001 isNat(0) -> tt 0.001/0.001 isNat(s(V1:S)) -> U21(isNat(V1:S)) 0.001/0.001 isNatIList(zeros) -> tt 0.001/0.001 isNatIList(cons(V1:S,V2:S)) -> U41(isNat(V1:S),V2:S) 0.001/0.001 isNatIList(V:S) -> U31(isNatList(V:S)) 0.001/0.001 isNatList(take(V1:S,V2:S)) -> U61(isNat(V1:S),V2:S) 0.001/0.001 isNatList(cons(V1:S,V2:S)) -> U51(isNat(V1:S),V2:S) 0.001/0.001 isNatList(nil) -> tt 0.001/0.001 length(cons(N:S,L:S)) -> U71(isNatList(L:S),L:S,N:S) 0.001/0.001 length(nil) -> 0 0.001/0.001 take(0,IL:S) -> U81(isNatIList(IL:S)) 0.001/0.001 take(s(M:S),cons(N:S,IL:S)) -> U91(isNatIList(IL:S),IL:S,M:S,N:S) 0.001/0.001 zeros -> cons(0,zeros) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 Modular Confluence Combinations Decomposition Processor: 0.001/0.001 It is a CTRS -> No modular confluence 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 CS-TRS Processor: 0.001/0.001 R is a CS-TRS 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S IL:S L:S M:S N:S V:S V1:S V2:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (U11 1) 0.001/0.001 (U21 1) 0.001/0.001 (U31 1) 0.001/0.001 (U41 1) 0.001/0.001 (U42 1) 0.001/0.001 (U51 1) 0.001/0.001 (U52 1) 0.001/0.001 (U61 1) 0.001/0.001 (U62 1) 0.001/0.001 (U71 1) 0.001/0.001 (U72 1) 0.001/0.001 (U81 1) 0.001/0.001 (U91 1) 0.001/0.001 (U92 1) 0.001/0.001 (U93 1) 0.001/0.001 (isNat) 0.001/0.001 (isNatIList) 0.001/0.001 (isNatList) 0.001/0.001 (length 1) 0.001/0.001 (take 1 2) 0.001/0.001 (zeros) 0.001/0.001 (0) 0.001/0.001 (cons 1) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (nil) 0.001/0.001 (s 1) 0.001/0.001 (tt) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 U11(tt) -> tt 0.001/0.001 U21(tt) -> tt 0.001/0.001 U31(tt) -> tt 0.001/0.001 U41(tt,V2:S) -> U42(isNatIList(V2:S)) 0.001/0.001 U42(tt) -> tt 0.001/0.001 U51(tt,V2:S) -> U52(isNatList(V2:S)) 0.001/0.001 U52(tt) -> tt 0.001/0.001 U61(tt,V2:S) -> U62(isNatIList(V2:S)) 0.001/0.001 U62(tt) -> tt 0.001/0.001 U71(tt,L:S,N:S) -> U72(isNat(N:S),L:S) 0.001/0.001 U72(tt,L:S) -> s(length(L:S)) 0.001/0.001 U81(tt) -> nil 0.001/0.001 U91(tt,IL:S,M:S,N:S) -> U92(isNat(M:S),IL:S,M:S,N:S) 0.001/0.001 U92(tt,IL:S,M:S,N:S) -> U93(isNat(N:S),IL:S,M:S,N:S) 0.001/0.001 U93(tt,IL:S,M:S,N:S) -> cons(N:S,take(M:S,IL:S)) 0.001/0.001 isNat(length(V1:S)) -> U11(isNatList(V1:S)) 0.001/0.001 isNat(0) -> tt 0.001/0.001 isNat(s(V1:S)) -> U21(isNat(V1:S)) 0.001/0.001 isNatIList(zeros) -> tt 0.001/0.001 isNatIList(cons(V1:S,V2:S)) -> U41(isNat(V1:S),V2:S) 0.001/0.001 isNatIList(V:S) -> U31(isNatList(V:S)) 0.001/0.001 isNatList(take(V1:S,V2:S)) -> U61(isNat(V1:S),V2:S) 0.001/0.001 isNatList(cons(V1:S,V2:S)) -> U51(isNat(V1:S),V2:S) 0.001/0.001 isNatList(nil) -> tt 0.001/0.001 length(cons(N:S,L:S)) -> U71(isNatList(L:S),L:S,N:S) 0.001/0.001 length(nil) -> 0 0.001/0.001 take(0,IL:S) -> U81(isNatIList(IL:S)) 0.001/0.001 take(s(M:S),cons(N:S,IL:S)) -> U91(isNatIList(IL:S),IL:S,M:S,N:S) 0.001/0.001 zeros -> cons(0,zeros) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 Huet Levy Processor: 0.001/0.001 -> Rules: 0.001/0.001 U11(tt) -> tt 0.001/0.001 U21(tt) -> tt 0.001/0.001 U31(tt) -> tt 0.001/0.001 U41(tt,V2:S) -> U42(isNatIList(V2:S)) 0.001/0.001 U42(tt) -> tt 0.001/0.001 U51(tt,V2:S) -> U52(isNatList(V2:S)) 0.001/0.001 U52(tt) -> tt 0.001/0.001 U61(tt,V2:S) -> U62(isNatIList(V2:S)) 0.001/0.001 U62(tt) -> tt 0.001/0.001 U71(tt,L:S,N:S) -> U72(isNat(N:S),L:S) 0.001/0.001 U72(tt,L:S) -> s(length(L:S)) 0.001/0.001 U81(tt) -> nil 0.001/0.001 U91(tt,IL:S,M:S,N:S) -> U92(isNat(M:S),IL:S,M:S,N:S) 0.001/0.001 U92(tt,IL:S,M:S,N:S) -> U93(isNat(N:S),IL:S,M:S,N:S) 0.001/0.001 U93(tt,IL:S,M:S,N:S) -> cons(N:S,take(M:S,IL:S)) 0.001/0.001 isNat(length(V1:S)) -> U11(isNatList(V1:S)) 0.001/0.001 isNat(0) -> tt 0.001/0.001 isNat(s(V1:S)) -> U21(isNat(V1:S)) 0.001/0.001 isNatIList(zeros) -> tt 0.001/0.001 isNatIList(cons(V1:S,V2:S)) -> U41(isNat(V1:S),V2:S) 0.001/0.001 isNatIList(V:S) -> U31(isNatList(V:S)) 0.001/0.001 isNatList(take(V1:S,V2:S)) -> U61(isNat(V1:S),V2:S) 0.001/0.001 isNatList(cons(V1:S,V2:S)) -> U51(isNat(V1:S),V2:S) 0.001/0.001 isNatList(nil) -> tt 0.001/0.001 length(cons(N:S,L:S)) -> U71(isNatList(L:S),L:S,N:S) 0.001/0.001 length(nil) -> 0 0.001/0.001 take(0,IL:S) -> U81(isNatIList(IL:S)) 0.001/0.001 take(s(M:S),cons(N:S,IL:S)) -> U91(isNatIList(IL:S),IL:S,M:S,N:S) 0.001/0.001 zeros -> cons(0,zeros) 0.001/0.001 -> Vars: 0.001/0.001 V2, V2, V2, L, N, L, IL, M, N, IL, M, N, IL, M, N, V1, V1, V1, V2, V, V1, V2, V1, V2, L, N, IL, IL, M, N 0.001/0.001 -> UVars: 0.001/0.001 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.001/0.001 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.001/0.001 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.001/0.001 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [L, N], UV-RFrozen: [L, N]) 0.001/0.001 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [L], UV-LFrozen: [L], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [IL, M, N], UV-RFrozen: [IL, M, N]) 0.001/0.001 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [IL, M, N], UV-RFrozen: [IL, M, N]) 0.001/0.001 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [IL, M, N], UV-RFrozen: [IL, M]) 0.001/0.001 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.001/0.001 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.001/0.001 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.001/0.001 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.001/0.001 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.001/0.001 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.001/0.001 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 25, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [L], UV-RFrozen: [L, N]) 0.001/0.001 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 27, UV-LActive: [IL], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [IL]) 0.001/0.001 (UV-RuleId: 28, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [IL], UV-RFrozen: [IL, M, N]) 0.001/0.001 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 -> FVars: 0.001/0.001 x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37 0.001/0.001 -> PVars: 0.001/0.001 V2: [x8, x9, x10, x26, x29, x31], L: [x11, x13, x32], N: [x12, x16, x19, x22, x33, x37], IL: [x14, x17, x20, x34, x35], M: [x15, x18, x21, x36], V1: [x23, x24, x25, x28, x30], V: [x27] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 (rule: U11(tt) -> tt, id: 1, possubterms: U11(tt)->[], tt->[1]) 0.001/0.001 (rule: U21(tt) -> tt, id: 2, possubterms: U21(tt)->[], tt->[1]) 0.001/0.001 (rule: U31(tt) -> tt, id: 3, possubterms: U31(tt)->[], tt->[1]) 0.001/0.001 (rule: U41(tt,x8:S) -> U42(isNatIList(x8:S)), id: 4, possubterms: U41(tt,x8:S)->[], tt->[1]) 0.001/0.001 (rule: U42(tt) -> tt, id: 5, possubterms: U42(tt)->[], tt->[1]) 0.001/0.001 (rule: U51(tt,x9:S) -> U52(isNatList(x9:S)), id: 6, possubterms: U51(tt,x9:S)->[], tt->[1]) 0.001/0.001 (rule: U52(tt) -> tt, id: 7, possubterms: U52(tt)->[], tt->[1]) 0.001/0.001 (rule: U61(tt,x10:S) -> U62(isNatIList(x10:S)), id: 8, possubterms: U61(tt,x10:S)->[], tt->[1]) 0.001/0.001 (rule: U62(tt) -> tt, id: 9, possubterms: U62(tt)->[], tt->[1]) 0.001/0.001 (rule: U71(tt,x11:S,x12:S) -> U72(isNat(x12:S),x11:S), id: 10, possubterms: U71(tt,x11:S,x12:S)->[], tt->[1]) 0.001/0.001 (rule: U72(tt,x13:S) -> s(length(x13:S)), id: 11, possubterms: U72(tt,x13:S)->[], tt->[1]) 0.001/0.001 (rule: U81(tt) -> nil, id: 12, possubterms: U81(tt)->[], tt->[1]) 0.001/0.001 (rule: U91(tt,x14:S,x15:S,x16:S) -> U92(isNat(x15:S),x14:S,x15:S,x16:S), id: 13, possubterms: U91(tt,x14:S,x15:S,x16:S)->[], tt->[1]) 0.001/0.001 (rule: U92(tt,x17:S,x18:S,x19:S) -> U93(isNat(x19:S),x17:S,x18:S,x19:S), id: 14, possubterms: U92(tt,x17:S,x18:S,x19:S)->[], tt->[1]) 0.001/0.001 (rule: U93(tt,x20:S,x21:S,x22:S) -> cons(x22:S,take(x21:S,x20:S)), id: 15, possubterms: U93(tt,x20:S,x21:S,x22:S)->[], tt->[1]) 0.001/0.001 (rule: isNat(length(x23:S)) -> U11(isNatList(x23:S)), id: 16, possubterms: isNat(length(x23:S))->[]) 0.001/0.001 (rule: isNat(0) -> tt, id: 17, possubterms: isNat(0)->[]) 0.001/0.001 (rule: isNat(s(x24:S)) -> U21(isNat(x24:S)), id: 18, possubterms: isNat(s(x24:S))->[]) 0.001/0.001 (rule: isNatIList(zeros) -> tt, id: 19, possubterms: isNatIList(zeros)->[]) 0.001/0.001 (rule: isNatIList(cons(x25:S,x26:S)) -> U41(isNat(x25:S),x26:S), id: 20, possubterms: isNatIList(cons(x25:S,x26:S))->[]) 0.001/0.001 (rule: isNatIList(x27:S) -> U31(isNatList(x27:S)), id: 21, possubterms: isNatIList(x27:S)->[]) 0.001/0.001 (rule: isNatList(take(x28:S,x29:S)) -> U61(isNat(x28:S),x29:S), id: 22, possubterms: isNatList(take(x28:S,x29:S))->[]) 0.001/0.001 (rule: isNatList(cons(x30:S,x31:S)) -> U51(isNat(x30:S),x31:S), id: 23, possubterms: isNatList(cons(x30:S,x31:S))->[]) 0.001/0.001 (rule: isNatList(nil) -> tt, id: 24, possubterms: isNatList(nil)->[]) 0.001/0.001 (rule: length(cons(x33:S,x32:S)) -> U71(isNatList(x32:S),x32:S,x33:S), id: 25, possubterms: length(cons(x33:S,x32:S))->[], cons(x33:S,x32:S)->[1]) 0.001/0.001 (rule: length(nil) -> 0, id: 26, possubterms: length(nil)->[], nil->[1]) 0.001/0.001 (rule: take(0,x34:S) -> U81(isNatIList(x34:S)), id: 27, possubterms: take(0,x34:S)->[], 0->[1]) 0.001/0.001 (rule: take(s(x36:S),cons(x37:S,x35:S)) -> U91(isNatIList(x35:S),x35:S,x36:S,x37:S), id: 28, possubterms: take(s(x36:S),cons(x37:S,x35:S))->[], s(x36:S)->[1], cons(x37:S,x35:S)->[2]) 0.001/0.001 (rule: zeros -> cons(0,zeros), id: 29, possubterms: zeros->[]) 0.001/0.001 0.001/0.001 -> Unifications: 0.001/0.001 (R21 unifies with R19 at p: [], l: isNatIList(x27:S), lp: isNatIList(x27:S), sig: {x27:S -> zeros}, l': isNatIList(zeros), r: U31(isNatList(x27:S)), r': tt) 0.001/0.001 (R21 unifies with R20 at p: [], l: isNatIList(x27:S), lp: isNatIList(x27:S), sig: {x27:S -> cons(V1:S,V2:S)}, l': isNatIList(cons(V1:S,V2:S)), r: U31(isNatList(x27:S)), r': U41(isNat(V1:S),V2:S)) 0.001/0.001 0.001/0.001 -> Critical pairs info: 0.001/0.001 => Not trivial, Overlay, NW0, N1 0.001/0.001 => Not trivial, Overlay, NW0, N2 0.001/0.001 0.001/0.001 -> Problem conclusions: 0.001/0.001 Left linear, Not right linear, Not linear 0.001/0.001 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.001/0.001 Not Huet-Levy confluent, Not Newman confluent 0.001/0.001 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 Different Normal CP Terms Processor: 0.001/0.001 => Not trivial, Overlay, NW0, N1, Normal and not trivial cp 0.001/0.001 0.001/0.001 The problem is not joinable. 0.001/0.001 0.00user 0.00system 0:00.01elapsed 78%CPU (0avgtext+0avgdata 11204maxresident)k 0.001/0.001 0inputs+0outputs (0major+1020minor)pagefaults 0swaps