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 v_NonEmpty:S:S M:S:S N:S:S V1:S:S V2:S:S X:S:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (U11 1) 0.001/0.001 (U12 1) 0.001/0.001 (U13 1) 0.001/0.001 (U21 1) 0.001/0.001 (U22 1) 0.001/0.001 (U31 1) 0.001/0.001 (U32 1) 0.001/0.001 (U33 1) 0.001/0.001 (U41 1) 0.001/0.001 (U51 1) 0.001/0.001 (U61 1) 0.001/0.001 (U71 1) 0.001/0.001 (and 1) 0.001/0.001 (isNat 1) 0.001/0.001 (isNatKind 1) 0.001/0.001 (plus 2) 0.001/0.001 (x 2) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (num0) 0.001/0.001 (s) 0.001/0.001 (tt) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 U11(tt,V1:S:S,V2:S:S) -> U12(isNat(V1:S:S),V2:S:S) 0.001/0.001 U12(tt,V2:S:S) -> U13(isNat(V2:S:S)) 0.001/0.001 U13(tt) -> tt 0.001/0.001 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.001/0.001 U22(tt) -> tt 0.001/0.001 U31(tt,V1:S:S,V2:S:S) -> U32(isNat(V1:S:S),V2:S:S) 0.001/0.001 U32(tt,V2:S:S) -> U33(isNat(V2:S:S)) 0.001/0.001 U33(tt) -> tt 0.001/0.001 U41(tt,N:S:S) -> N:S:S 0.001/0.001 U51(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.001/0.001 U61(tt) -> num0 0.001/0.001 U71(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.001/0.001 and(tt,X:S:S) -> X:S:S 0.001/0.001 isNat(plus(V1:S:S,V2:S:S)) -> U11(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(x(V1:S:S,V2:S:S)) -> U31(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(num0) -> tt 0.001/0.001 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.001/0.001 isNatKind(plus(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(x(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(num0) -> tt 0.001/0.001 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.001/0.001 plus(N:S:S,num0) -> U41(and(isNat(N:S:S),isNatKind(N:S:S)),N:S:S) 0.001/0.001 plus(N:S:S,s(M:S:S)) -> U51(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 0.001/0.001 x(N:S:S,num0) -> U61(and(isNat(N:S:S),isNatKind(N:S:S))) 0.001/0.001 x(N:S:S,s(M:S:S)) -> U71(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 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 v_NonEmpty:S:S M:S:S N:S:S V1:S:S V2:S:S X:S:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (U11 1) 0.001/0.001 (U12 1) 0.001/0.001 (U13 1) 0.001/0.001 (U21 1) 0.001/0.001 (U22 1) 0.001/0.001 (U31 1) 0.001/0.001 (U32 1) 0.001/0.001 (U33 1) 0.001/0.001 (U41 1) 0.001/0.001 (U51 1) 0.001/0.001 (U61 1) 0.001/0.001 (U71 1) 0.001/0.001 (and 1) 0.001/0.001 (isNat 1) 0.001/0.001 (isNatKind 1) 0.001/0.001 (plus 2) 0.001/0.001 (x 2) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (num0) 0.001/0.001 (s) 0.001/0.001 (tt) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 U11(tt,V1:S:S,V2:S:S) -> U12(isNat(V1:S:S),V2:S:S) 0.001/0.001 U12(tt,V2:S:S) -> U13(isNat(V2:S:S)) 0.001/0.001 U13(tt) -> tt 0.001/0.001 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.001/0.001 U22(tt) -> tt 0.001/0.001 U31(tt,V1:S:S,V2:S:S) -> U32(isNat(V1:S:S),V2:S:S) 0.001/0.001 U32(tt,V2:S:S) -> U33(isNat(V2:S:S)) 0.001/0.001 U33(tt) -> tt 0.001/0.001 U41(tt,N:S:S) -> N:S:S 0.001/0.001 U51(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.001/0.001 U61(tt) -> num0 0.001/0.001 U71(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.001/0.001 and(tt,X:S:S) -> X:S:S 0.001/0.001 isNat(plus(V1:S:S,V2:S:S)) -> U11(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(x(V1:S:S,V2:S:S)) -> U31(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(num0) -> tt 0.001/0.001 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.001/0.001 isNatKind(plus(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(x(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(num0) -> tt 0.001/0.001 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.001/0.001 plus(N:S:S,num0) -> U41(and(isNat(N:S:S),isNatKind(N:S:S)),N:S:S) 0.001/0.001 plus(N:S:S,s(M:S:S)) -> U51(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 0.001/0.001 x(N:S:S,num0) -> U61(and(isNat(N:S:S),isNatKind(N:S:S))) 0.001/0.001 x(N:S:S,s(M:S:S)) -> U71(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 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 v_NonEmpty:S:S M:S:S N:S:S V1:S:S V2:S:S X:S:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (U11 1) 0.001/0.001 (U12 1) 0.001/0.001 (U13 1) 0.001/0.001 (U21 1) 0.001/0.001 (U22 1) 0.001/0.001 (U31 1) 0.001/0.001 (U32 1) 0.001/0.001 (U33 1) 0.001/0.001 (U41 1) 0.001/0.001 (U51 1) 0.001/0.001 (U61 1) 0.001/0.001 (U71 1) 0.001/0.001 (and 1) 0.001/0.001 (isNat 1) 0.001/0.001 (isNatKind 1) 0.001/0.001 (plus 2) 0.001/0.001 (x 2) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (num0) 0.001/0.001 (s) 0.001/0.001 (tt) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 U11(tt,V1:S:S,V2:S:S) -> U12(isNat(V1:S:S),V2:S:S) 0.001/0.001 U12(tt,V2:S:S) -> U13(isNat(V2:S:S)) 0.001/0.001 U13(tt) -> tt 0.001/0.001 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.001/0.001 U22(tt) -> tt 0.001/0.001 U31(tt,V1:S:S,V2:S:S) -> U32(isNat(V1:S:S),V2:S:S) 0.001/0.001 U32(tt,V2:S:S) -> U33(isNat(V2:S:S)) 0.001/0.001 U33(tt) -> tt 0.001/0.001 U41(tt,N:S:S) -> N:S:S 0.001/0.001 U51(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.001/0.001 U61(tt) -> num0 0.001/0.001 U71(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.001/0.001 and(tt,X:S:S) -> X:S:S 0.001/0.001 isNat(plus(V1:S:S,V2:S:S)) -> U11(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(x(V1:S:S,V2:S:S)) -> U31(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(num0) -> tt 0.001/0.001 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.001/0.001 isNatKind(plus(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(x(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(num0) -> tt 0.001/0.001 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.001/0.001 plus(N:S:S,num0) -> U41(and(isNat(N:S:S),isNatKind(N:S:S)),N:S:S) 0.001/0.001 plus(N:S:S,s(M:S:S)) -> U51(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 0.001/0.001 x(N:S:S,num0) -> U61(and(isNat(N:S:S),isNatKind(N:S:S))) 0.001/0.001 x(N:S:S,s(M:S:S)) -> U71(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 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,V1:S:S,V2:S:S) -> U12(isNat(V1:S:S),V2:S:S) 0.001/0.001 U12(tt,V2:S:S) -> U13(isNat(V2:S:S)) 0.001/0.001 U13(tt) -> tt 0.001/0.001 U21(tt,V1:S:S) -> U22(isNat(V1:S:S)) 0.001/0.001 U22(tt) -> tt 0.001/0.001 U31(tt,V1:S:S,V2:S:S) -> U32(isNat(V1:S:S),V2:S:S) 0.001/0.001 U32(tt,V2:S:S) -> U33(isNat(V2:S:S)) 0.001/0.001 U33(tt) -> tt 0.001/0.001 U41(tt,N:S:S) -> N:S:S 0.001/0.001 U51(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.001/0.001 U61(tt) -> num0 0.001/0.001 U71(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.001/0.001 and(tt,X:S:S) -> X:S:S 0.001/0.001 isNat(plus(V1:S:S,V2:S:S)) -> U11(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(x(V1:S:S,V2:S:S)) -> U31(and(isNatKind(V1:S:S),isNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.001/0.001 isNat(num0) -> tt 0.001/0.001 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.001/0.001 isNatKind(plus(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(x(V1:S:S,V2:S:S)) -> and(isNatKind(V1:S:S),isNatKind(V2:S:S)) 0.001/0.001 isNatKind(num0) -> tt 0.001/0.001 isNatKind(s(V1:S:S)) -> isNatKind(V1:S:S) 0.001/0.001 plus(N:S:S,num0) -> U41(and(isNat(N:S:S),isNatKind(N:S:S)),N:S:S) 0.001/0.001 plus(N:S:S,s(M:S:S)) -> U51(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 0.001/0.001 x(N:S:S,num0) -> U61(and(isNat(N:S:S),isNatKind(N:S:S))) 0.001/0.001 x(N:S:S,s(M:S:S)) -> U71(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S) 0.001/0.001 -> Vars: 0.001/0.001 V1:S, V2:S, V2:S, V1:S, V1:S, V2:S, V2:S, N:S, M:S, N:S, M:S, N:S, X:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, N:S, M:S, N:S, N:S, M:S, N:S 0.001/0.001 -> UVars: 0.001/0.001 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.001/0.001 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], 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: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 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: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.001/0.001 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.001/0.001 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.001/0.001 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 14, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S, V2:S]) 0.001/0.001 (UV-RuleId: 15, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S, V2:S]) 0.001/0.001 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.001/0.001 (UV-RuleId: 18, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V2:S]) 0.001/0.001 (UV-RuleId: 19, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V2:S]) 0.001/0.001 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.001/0.001 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.001/0.001 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.001/0.001 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.001/0.001 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.001/0.001 -> FVars: 0.001/0.001 x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35 0.001/0.001 -> PVars: 0.001/0.001 V1:S: [x7, x10, x11, x20, x22, x24, x25, x27, x29], V2:S: [x8, x9, x12, x13, x21, x23, x26, x28], N:S: [x14, x16, x18, x30, x32, x33, x35], M:S: [x15, x17, x31, x34], X:S: [x19] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 (rule: U11(tt,x7:S,x8:S) -> U12(isNat(x7:S),x8:S), id: 1, possubterms: U11(tt,x7:S,x8:S)->[], tt->[1]) 0.001/0.001 (rule: U12(tt,x9:S) -> U13(isNat(x9:S)), id: 2, possubterms: U12(tt,x9:S)->[], tt->[1]) 0.001/0.001 (rule: U13(tt) -> tt, id: 3, possubterms: U13(tt)->[], tt->[1]) 0.001/0.001 (rule: U21(tt,x10:S) -> U22(isNat(x10:S)), id: 4, possubterms: U21(tt,x10:S)->[], tt->[1]) 0.001/0.001 (rule: U22(tt) -> tt, id: 5, possubterms: U22(tt)->[], tt->[1]) 0.001/0.001 (rule: U31(tt,x11:S,x12:S) -> U32(isNat(x11:S),x12:S), id: 6, possubterms: U31(tt,x11:S,x12:S)->[], tt->[1]) 0.001/0.001 (rule: U32(tt,x13:S) -> U33(isNat(x13:S)), id: 7, possubterms: U32(tt,x13:S)->[], tt->[1]) 0.001/0.001 (rule: U33(tt) -> tt, id: 8, possubterms: U33(tt)->[], tt->[1]) 0.001/0.001 (rule: U41(tt,x14:S) -> x14:S, id: 9, possubterms: U41(tt,x14:S)->[], tt->[1]) 0.001/0.001 (rule: U51(tt,x15:S,x16:S) -> s(plus(x16:S,x15:S)), id: 10, possubterms: U51(tt,x15:S,x16:S)->[], tt->[1]) 0.001/0.001 (rule: U61(tt) -> num0, id: 11, possubterms: U61(tt)->[], tt->[1]) 0.001/0.001 (rule: U71(tt,x17:S,x18:S) -> plus(x(x18:S,x17:S),x18:S), id: 12, possubterms: U71(tt,x17:S,x18:S)->[], tt->[1]) 0.001/0.001 (rule: and(tt,x19:S) -> x19:S, id: 13, possubterms: and(tt,x19:S)->[], tt->[1]) 0.001/0.001 (rule: isNat(plus(x20:S,x21:S)) -> U11(and(isNatKind(x20:S),isNatKind(x21:S)),x20:S,x21:S), id: 14, possubterms: isNat(plus(x20:S,x21:S))->[], plus(x20:S,x21:S)->[1]) 0.001/0.001 (rule: isNat(x(x22:S,x23:S)) -> U31(and(isNatKind(x22:S),isNatKind(x23:S)),x22:S,x23:S), id: 15, possubterms: isNat(x(x22:S,x23:S))->[], x(x22:S,x23:S)->[1]) 0.001/0.001 (rule: isNat(num0) -> tt, id: 16, possubterms: isNat(num0)->[], num0->[1]) 0.001/0.001 (rule: isNat(s(x24:S)) -> U21(isNatKind(x24:S),x24:S), id: 17, possubterms: isNat(s(x24:S))->[], s(x24:S)->[1]) 0.001/0.001 (rule: isNatKind(plus(x25:S,x26:S)) -> and(isNatKind(x25:S),isNatKind(x26:S)), id: 18, possubterms: isNatKind(plus(x25:S,x26:S))->[], plus(x25:S,x26:S)->[1]) 0.001/0.001 (rule: isNatKind(x(x27:S,x28:S)) -> and(isNatKind(x27:S),isNatKind(x28:S)), id: 19, possubterms: isNatKind(x(x27:S,x28:S))->[], x(x27:S,x28:S)->[1]) 0.001/0.001 (rule: isNatKind(num0) -> tt, id: 20, possubterms: isNatKind(num0)->[], num0->[1]) 0.001/0.001 (rule: isNatKind(s(x29:S)) -> isNatKind(x29:S), id: 21, possubterms: isNatKind(s(x29:S))->[], s(x29:S)->[1]) 0.001/0.001 (rule: plus(x30:S,num0) -> U41(and(isNat(x30:S),isNatKind(x30:S)),x30:S), id: 22, possubterms: plus(x30:S,num0)->[], num0->[2]) 0.001/0.001 (rule: plus(x32:S,s(x31:S)) -> U51(and(and(isNat(x31:S),isNatKind(x31:S)),and(isNat(x32:S),isNatKind(x32:S))),x31:S,x32:S), id: 23, possubterms: plus(x32:S,s(x31:S))->[], s(x31:S)->[2]) 0.001/0.001 (rule: x(x33:S,num0) -> U61(and(isNat(x33:S),isNatKind(x33:S))), id: 24, possubterms: x(x33:S,num0)->[], num0->[2]) 0.001/0.001 (rule: x(x35:S,s(x34:S)) -> U71(and(and(isNat(x34:S),isNatKind(x34:S)),and(isNat(x35:S),isNatKind(x35:S))),x34:S,x35:S), id: 25, possubterms: x(x35:S,s(x34:S))->[], s(x34:S)->[2]) 0.001/0.001 0.001/0.001 -> Unifications: 0.001/0.001 (R14 unifies with R22 at p: [1], l: isNat(plus(x20:S,x21:S)), lp: plus(x20:S,x21:S), sig: {x20:S -> N:S:S,x21:S -> num0}, l': plus(N:S:S,num0), r: U11(and(isNatKind(x20:S),isNatKind(x21:S)),x20:S,x21:S), r': U41(and(isNat(N:S:S),isNatKind(N:S:S)),N:S:S)) 0.001/0.001 (R14 unifies with R23 at p: [1], l: isNat(plus(x20:S,x21:S)), lp: plus(x20:S,x21:S), sig: {x20:S -> N:S:S,x21:S -> s(M:S:S)}, l': plus(N:S:S,s(M:S:S)), r: U11(and(isNatKind(x20:S),isNatKind(x21:S)),x20:S,x21:S), r': U51(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S)) 0.001/0.001 (R15 unifies with R24 at p: [1], l: isNat(x(x22:S,x23:S)), lp: x(x22:S,x23:S), sig: {x22:S -> N:S:S,x23:S -> num0}, l': x(N:S:S,num0), r: U31(and(isNatKind(x22:S),isNatKind(x23:S)),x22:S,x23:S), r': U61(and(isNat(N:S:S),isNatKind(N:S:S)))) 0.001/0.001 (R15 unifies with R25 at p: [1], l: isNat(x(x22:S,x23:S)), lp: x(x22:S,x23:S), sig: {x22:S -> N:S:S,x23:S -> s(M:S:S)}, l': x(N:S:S,s(M:S:S)), r: U31(and(isNatKind(x22:S),isNatKind(x23:S)),x22:S,x23:S), r': U71(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S)) 0.001/0.001 (R18 unifies with R22 at p: [1], l: isNatKind(plus(x25:S,x26:S)), lp: plus(x25:S,x26:S), sig: {x25:S -> N:S:S,x26:S -> num0}, l': plus(N:S:S,num0), r: and(isNatKind(x25:S),isNatKind(x26:S)), r': U41(and(isNat(N:S:S),isNatKind(N:S:S)),N:S:S)) 0.001/0.001 (R18 unifies with R23 at p: [1], l: isNatKind(plus(x25:S,x26:S)), lp: plus(x25:S,x26:S), sig: {x25:S -> N:S:S,x26:S -> s(M:S:S)}, l': plus(N:S:S,s(M:S:S)), r: and(isNatKind(x25:S),isNatKind(x26:S)), r': U51(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S)) 0.001/0.001 (R19 unifies with R24 at p: [1], l: isNatKind(x(x27:S,x28:S)), lp: x(x27:S,x28:S), sig: {x27:S -> N:S:S,x28:S -> num0}, l': x(N:S:S,num0), r: and(isNatKind(x27:S),isNatKind(x28:S)), r': U61(and(isNat(N:S:S),isNatKind(N:S:S)))) 0.001/0.001 (R19 unifies with R25 at p: [1], l: isNatKind(x(x27:S,x28:S)), lp: x(x27:S,x28:S), sig: {x27:S -> N:S:S,x28:S -> s(M:S:S)}, l': x(N:S:S,s(M:S:S)), r: and(isNatKind(x27:S),isNatKind(x28:S)), r': U71(and(and(isNat(M:S:S),isNatKind(M:S:S)),and(isNat(N:S:S),isNatKind(N:S:S))),M:S:S,N:S:S)) 0.001/0.001 0.001/0.001 -> Critical pairs info: 0.001/0.001 => Not trivial, Not overlay, NW0, N1 0.001/0.001 => Not trivial, Not overlay, NW0, N2 0.001/0.001 => Not trivial, Not overlay, NW0, N3 0.001/0.001 => Not trivial, Not overlay, NW0, N4 0.001/0.001 => Not trivial, Not overlay, NW0, N5 0.001/0.001 => Not trivial, Not overlay, NW0, N6 0.001/0.001 => Not trivial, Not overlay, NW0, N7 0.001/0.001 => Not trivial, Not overlay, NW0, N8 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, Not 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.01system 0:00.01elapsed 83%CPU (0avgtext+0avgdata 11384maxresident)k 0.001/0.001 8inputs+0outputs (0major+1093minor)pagefaults 0swaps