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 M:S N:S V1:S V2:S X:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(U11 1)
0.002/0.002	(U12 1)
0.002/0.002	(U13 1)
0.002/0.002	(U21 1)
0.002/0.002	(U22 1)
0.002/0.002	(U31 1)
0.002/0.002	(U41 1)
0.002/0.002	(and 1)
0.002/0.002	(isNat)
0.002/0.002	(isNatKind)
0.002/0.002	(plus 1 2)
0.002/0.002	(0)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(s 1)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S)
0.002/0.002	U12(tt,V2:S) -> U13(isNat(V2:S))
0.002/0.002	U13(tt) -> tt
0.002/0.002	U21(tt,V1:S) -> U22(isNat(V1:S))
0.002/0.002	U22(tt) -> tt
0.002/0.002	U31(tt,N:S) -> N:S
0.002/0.002	U41(tt,M:S,N:S) -> s(plus(N:S,M:S))
0.002/0.002	and(tt,X:S) -> X:S
0.002/0.002	isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S)
0.002/0.002	isNat(0) -> tt
0.002/0.002	isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S)
0.002/0.002	isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S))
0.002/0.002	isNatKind(0) -> tt
0.002/0.002	isNatKind(s(V1:S)) -> isNatKind(V1:S)
0.002/0.002	plus(N:S,0) -> U31(and(isNat(N:S),isNatKind(N:S)),N:S)
0.002/0.002	plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	CleanTRS Processor:
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty:S M:S N:S V1:S V2:S X:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(U11 1)
0.002/0.002	(U12 1)
0.002/0.002	(U13 1)
0.002/0.002	(U21 1)
0.002/0.002	(U22 1)
0.002/0.002	(U31 1)
0.002/0.002	(U41 1)
0.002/0.002	(and 1)
0.002/0.002	(isNat)
0.002/0.002	(isNatKind)
0.002/0.002	(plus 1 2)
0.002/0.002	(0)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(s 1)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S)
0.002/0.002	U12(tt,V2:S) -> U13(isNat(V2:S))
0.002/0.002	U13(tt) -> tt
0.002/0.002	U21(tt,V1:S) -> U22(isNat(V1:S))
0.002/0.002	U22(tt) -> tt
0.002/0.002	U31(tt,N:S) -> N:S
0.002/0.002	U41(tt,M:S,N:S) -> s(plus(N:S,M:S))
0.002/0.002	and(tt,X:S) -> X:S
0.002/0.002	isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S)
0.002/0.002	isNat(0) -> tt
0.002/0.002	isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S)
0.002/0.002	isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S))
0.002/0.002	isNatKind(0) -> tt
0.002/0.002	isNatKind(s(V1:S)) -> isNatKind(V1:S)
0.002/0.002	plus(N:S,0) -> U31(and(isNat(N:S),isNatKind(N:S)),N:S)
0.002/0.002	plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	Modular Confluence Combinations Decomposition Processor:
0.002/0.002	It is a CTRS -> No modular confluence
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	CS-TRS Processor:
0.002/0.002	R is a CS-TRS
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty:S M:S N:S V1:S V2:S X:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(U11 1)
0.002/0.002	(U12 1)
0.002/0.002	(U13 1)
0.002/0.002	(U21 1)
0.002/0.002	(U22 1)
0.002/0.002	(U31 1)
0.002/0.002	(U41 1)
0.002/0.002	(and 1)
0.002/0.002	(isNat)
0.002/0.002	(isNatKind)
0.002/0.002	(plus 1 2)
0.002/0.002	(0)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(s 1)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S)
0.002/0.002	U12(tt,V2:S) -> U13(isNat(V2:S))
0.002/0.002	U13(tt) -> tt
0.002/0.002	U21(tt,V1:S) -> U22(isNat(V1:S))
0.002/0.002	U22(tt) -> tt
0.002/0.002	U31(tt,N:S) -> N:S
0.002/0.002	U41(tt,M:S,N:S) -> s(plus(N:S,M:S))
0.002/0.002	and(tt,X:S) -> X:S
0.002/0.002	isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S)
0.002/0.002	isNat(0) -> tt
0.002/0.002	isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S)
0.002/0.002	isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S))
0.002/0.002	isNatKind(0) -> tt
0.002/0.002	isNatKind(s(V1:S)) -> isNatKind(V1:S)
0.002/0.002	plus(N:S,0) -> U31(and(isNat(N:S),isNatKind(N:S)),N:S)
0.002/0.002	plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	Extended u-Critical Pairs NonLHRV Processor [JLAMP21]:
0.002/0.002	->Extended u-Critical Pair:
0.002/0.002	 Rule 1 (l :-> r) => plus(x20:S,0) -> U31(and(isNat(x20:S),isNatKind(x20:S)),x20:S)
0.002/0.002	 Rule 15 (l' :-> r') => plus(N:S,0) -> U31(and(isNat(N:S),isNatKind(N:S)),N:S)
0.002/0.002	 Var => x20:S
0.002/0.002	 Pos x20:S in l => [1]
0.002/0.002	 Sigma => {x20:S -> plus(N:S,0)}
0.002/0.002	 s => U31(and(isNat(plus(N:S,0)),isNatKind(plus(N:S,0))),plus(N:S,0))
0.002/0.002	 t => plus(U31(and(isNat(N:S),isNatKind(N:S)),N:S),0)
0.002/0.002	 NW => 1
0.002/0.002	
0.002/0.002	
0.002/0.002	->Extended u-Critical Pair:
0.002/0.002	 Rule 1 (l :-> r) => plus(x20:S,0) -> U31(and(isNat(x20:S),isNatKind(x20:S)),x20:S)
0.002/0.002	 Rule 16 (l' :-> r') => plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	 Var => x20:S
0.002/0.002	 Pos x20:S in l => [1]
0.002/0.002	 Sigma => {x20:S -> plus(N:S,s(M:S))}
0.002/0.002	 s => U31(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S)))
0.002/0.002	 t => plus(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0)
0.002/0.002	 NW => 1
0.002/0.002	
0.002/0.002	
0.002/0.002	->Extended u-Critical Pair:
0.002/0.002	 Rule 1 (l :-> r) => plus(x22:S,s(x21:S)) -> U41(and(and(isNat(x21:S),isNatKind(x21:S)),and(isNat(x22:S),isNatKind(x22:S))),x21:S,x22:S)
0.002/0.002	 Rule 16 (l' :-> r') => plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	 Var => x21:S
0.002/0.002	 Pos x21:S in l => [2,1]
0.002/0.002	 Sigma => {x21:S -> plus(N:S,s(M:S))}
0.002/0.002	 s => U41(and(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),and(isNat(x22:S),isNatKind(x22:S))),plus(N:S,s(M:S)),x22:S)
0.002/0.002	 t => plus(x22:S,s(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)))
0.002/0.002	 NW => 1
0.002/0.002	
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 M:S N:S V1:S V2:S X:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(U11 1)
0.002/0.002	(U12 1)
0.002/0.002	(U13 1)
0.002/0.002	(U21 1)
0.002/0.002	(U22 1)
0.002/0.002	(U31 1)
0.002/0.002	(U41 1)
0.002/0.002	(and 1)
0.002/0.002	(isNat)
0.002/0.002	(isNatKind)
0.002/0.002	(plus 1 2)
0.002/0.002	(0)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(s 1)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S)
0.002/0.002	U12(tt,V2:S) -> U13(isNat(V2:S))
0.002/0.002	U13(tt) -> tt
0.002/0.002	U21(tt,V1:S) -> U22(isNat(V1:S))
0.002/0.002	U22(tt) -> tt
0.002/0.002	U31(tt,N:S) -> N:S
0.002/0.002	U41(tt,M:S,N:S) -> s(plus(N:S,M:S))
0.002/0.002	and(tt,X:S) -> X:S
0.002/0.002	isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S)
0.002/0.002	isNat(0) -> tt
0.002/0.002	isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S)
0.002/0.002	isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S))
0.002/0.002	isNatKind(0) -> tt
0.002/0.002	isNatKind(s(V1:S)) -> isNatKind(V1:S)
0.002/0.002	plus(N:S,0) -> U31(and(isNat(N:S),isNatKind(N:S)),N:S)
0.002/0.002	plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	)
0.002/0.002	Critical Pairs:
0.002/0.002	<U31(and(isNat(plus(N:S,0)),isNatKind(plus(N:S,0))),plus(N:S,0)),plus(U31(and(isNat(N:S),isNatKind(N:S)),N:S),0)>   =>  Not trivial, Not overlay, NW1, N1
0.002/0.002	<U31(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S))),plus(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0)>   =>  Not trivial, Not overlay, NW1, N2
0.002/0.002	<U41(and(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),and(isNat(x22:S),isNatKind(x22:S))),plus(N:S,s(M:S)),x22:S),plus(x22:S,s(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)))>   =>  Not trivial, Not overlay, NW1, N3
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,V2:S) -> U12(isNat(V1:S),V2:S)
0.002/0.002	 U12(tt,V2:S) -> U13(isNat(V2:S))
0.002/0.002	 U13(tt) -> tt
0.002/0.002	 U21(tt,V1:S) -> U22(isNat(V1:S))
0.002/0.002	 U22(tt) -> tt
0.002/0.002	 U31(tt,N:S) -> N:S
0.002/0.002	 U41(tt,M:S,N:S) -> s(plus(N:S,M:S))
0.002/0.002	 and(tt,X:S) -> X:S
0.002/0.002	 isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S)
0.002/0.002	 isNat(0) -> tt
0.002/0.002	 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S)
0.002/0.002	 isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S))
0.002/0.002	 isNatKind(0) -> tt
0.002/0.002	 isNatKind(s(V1:S)) -> isNatKind(V1:S)
0.002/0.002	 plus(N:S,0) -> U31(and(isNat(N:S),isNatKind(N:S)),N:S)
0.002/0.002	 plus(N:S,s(M:S)) -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)
0.002/0.002	-> Vars:
0.002/0.002	 V1, V2, V2, V1, N, M, N, X, V1, V2, V1, V1, V2, V1, N, M, N
0.002/0.002	-> UVars:
0.002/0.002	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.002/0.002	 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2])
0.002/0.002	 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.002/0.002	 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [M, N], UV-LFrozen: [M, N], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.002/0.002	 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.002/0.002	 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.002/0.002	 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.002/0.002	 (UV-RuleId: 15, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N])
0.002/0.002	 (UV-RuleId: 16, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [M, N])
0.002/0.002	-> FVars:
0.002/0.002	 x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22
0.002/0.002	-> PVars:
0.002/0.002	 V1: [x6, x9, x14, x16, x17, x19], V2: [x7, x8, x15, x18], N: [x10, x12, x20, x22], M: [x11, x21], X: [x13]
0.002/0.002	
0.002/0.002	-> Rlps:
0.002/0.002	 (rule: U11(tt,x6:S,x7:S) -> U12(isNat(x6:S),x7:S), id: 1, possubterms: U11(tt,x6:S,x7:S)->[], tt->[1])
0.002/0.002	 (rule: U12(tt,x8:S) -> U13(isNat(x8:S)), id: 2, possubterms: U12(tt,x8:S)->[], tt->[1])
0.002/0.002	 (rule: U13(tt) -> tt, id: 3, possubterms: U13(tt)->[], tt->[1])
0.002/0.002	 (rule: U21(tt,x9:S) -> U22(isNat(x9:S)), id: 4, possubterms: U21(tt,x9:S)->[], tt->[1])
0.002/0.002	 (rule: U22(tt) -> tt, id: 5, possubterms: U22(tt)->[], tt->[1])
0.002/0.002	 (rule: U31(tt,x10:S) -> x10:S, id: 6, possubterms: U31(tt,x10:S)->[], tt->[1])
0.002/0.002	 (rule: U41(tt,x11:S,x12:S) -> s(plus(x12:S,x11:S)), id: 7, possubterms: U41(tt,x11:S,x12:S)->[], tt->[1])
0.002/0.002	 (rule: and(tt,x13:S) -> x13:S, id: 8, possubterms: and(tt,x13:S)->[], tt->[1])
0.002/0.002	 (rule: isNat(plus(x14:S,x15:S)) -> U11(and(isNatKind(x14:S),isNatKind(x15:S)),x14:S,x15:S), id: 9, possubterms: isNat(plus(x14:S,x15:S))->[])
0.002/0.002	 (rule: isNat(0) -> tt, id: 10, possubterms: isNat(0)->[])
0.002/0.002	 (rule: isNat(s(x16:S)) -> U21(isNatKind(x16:S),x16:S), id: 11, possubterms: isNat(s(x16:S))->[])
0.002/0.002	 (rule: isNatKind(plus(x17:S,x18:S)) -> and(isNatKind(x17:S),isNatKind(x18:S)), id: 12, possubterms: isNatKind(plus(x17:S,x18:S))->[])
0.002/0.002	 (rule: isNatKind(0) -> tt, id: 13, possubterms: isNatKind(0)->[])
0.002/0.002	 (rule: isNatKind(s(x19:S)) -> isNatKind(x19:S), id: 14, possubterms: isNatKind(s(x19:S))->[])
0.002/0.002	 (rule: plus(x20:S,0) -> U31(and(isNat(x20:S),isNatKind(x20:S)),x20:S), id: 15, possubterms: plus(x20:S,0)->[], 0->[2])
0.002/0.002	 (rule: plus(x22:S,s(x21:S)) -> U41(and(and(isNat(x21:S),isNatKind(x21:S)),and(isNat(x22:S),isNatKind(x22:S))),x21:S,x22:S), id: 16, possubterms: plus(x22:S,s(x21:S))->[], s(x21:S)->[2])
0.002/0.002	
0.002/0.002	-> Unifications:
0.002/0.002	
0.002/0.002	
0.002/0.002	-> Critical pairs info:
0.002/0.002	<U31(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S))),plus(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0)>   =>  Not trivial, Not overlay, NW1, N1
0.002/0.002	<U31(and(isNat(plus(N:S,0)),isNatKind(plus(N:S,0))),plus(N:S,0)),plus(U31(and(isNat(N:S),isNatKind(N:S)),N:S),0)>   =>  Not trivial, Not overlay, NW1, N2
0.002/0.002	<U41(and(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),and(isNat(N:S),isNatKind(N:S))),plus(N:S,s(M:S)),N:S),plus(N:S,s(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)))>   =>  Not trivial, Not overlay, NW1, N3
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: U31(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S)))
0.002/0.002	Nodes: [0,1]
0.002/0.002	Edges: [(0,1)]
0.002/0.002	ID: 0 => ('U31(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S)))', D0)
0.002/0.002	ID: 1 => ('U31(and(U11(and(isNatKind(N:S),isNatKind(s(M:S))),N:S,s(M:S)),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S)))', D1, R9, P[1, 1], S{x14:S -> N:S, x15:S -> s(M:S)}), NR: 'U11(and(isNatKind(N:S),isNatKind(s(M:S))),N:S,s(M:S))'
0.002/0.002	t: plus(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0)
0.002/0.002	Nodes: [0,1]
0.002/0.002	Edges: [(0,1)]
0.002/0.002	ID: 0 => ('plus(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0)', D0)
0.002/0.002	ID: 1 => ('U31(and(isNat(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)),isNatKind(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))),U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))', D1, R15, P[], S{x20:S -> U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)}), NR: 'U31(and(isNat(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S)),isNatKind(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))),U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))'
0.002/0.002	U31(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S))) ->* no union *<- plus(U41(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0)
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 59%CPU (0avgtext+0avgdata 10832maxresident)k
0.002/0.002	0inputs+0outputs (0major+1050minor)pagefaults 0swaps