0.002/0.002	NO
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty:S v_NonEmpty:S:S IL:S:S L:S:S M:S:S N:S:S T:S:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(and 1)
0.002/0.002	(isNat 1)
0.002/0.002	(isNatIList 1)
0.002/0.002	(isNatList 1)
0.002/0.002	(length 1)
0.002/0.002	(take 1 2)
0.002/0.002	(uLength 1)
0.002/0.002	(uTake1 1)
0.002/0.002	(uTake2 1)
0.002/0.002	(zeros)
0.002/0.002	(cons)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(nil)
0.002/0.002	(num0)
0.002/0.002	(s)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	and(tt,T:S:S) -> T:S:S
0.002/0.002	isNat(length(L:S:S)) -> isNatList(L:S:S)
0.002/0.002	isNat(num0) -> tt
0.002/0.002	isNat(s(N:S:S)) -> isNat(N:S:S)
0.002/0.002	isNatIList(zeros) -> tt
0.002/0.002	isNatIList(cons(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	isNatIList(IL:S:S) -> isNatList(IL:S:S)
0.002/0.002	isNatList(take(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	isNatList(cons(N:S:S,L:S:S)) -> and(isNat(N:S:S),isNatList(L:S:S))
0.002/0.002	isNatList(nil) -> tt
0.002/0.002	length(cons(N:S:S,L:S:S)) -> uLength(and(isNat(N:S:S),isNatList(L:S:S)),L:S:S)
0.002/0.002	take(num0,IL:S:S) -> uTake1(isNatIList(IL:S:S))
0.002/0.002	take(s(M:S:S),cons(N:S:S,IL:S:S)) -> uTake2(and(isNat(M:S:S),and(isNat(N:S:S),isNatIList(IL:S:S))),M:S:S,N:S:S,IL:S:S)
0.002/0.002	uLength(tt,L:S:S) -> s(length(L:S:S))
0.002/0.002	uTake1(tt) -> nil
0.002/0.002	uTake2(tt,M:S:S,N:S:S,IL:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S))
0.002/0.002	zeros -> cons(num0,zeros)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	CleanTRS Processor:
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty:S v_NonEmpty:S:S IL:S:S L:S:S M:S:S N:S:S T:S:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(and 1)
0.002/0.002	(isNat 1)
0.002/0.002	(isNatIList 1)
0.002/0.002	(isNatList 1)
0.002/0.002	(length 1)
0.002/0.002	(take 1 2)
0.002/0.002	(uLength 1)
0.002/0.002	(uTake1 1)
0.002/0.002	(uTake2 1)
0.002/0.002	(zeros)
0.002/0.002	(cons)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(nil)
0.002/0.002	(num0)
0.002/0.002	(s)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	and(tt,T:S:S) -> T:S:S
0.002/0.002	isNat(length(L:S:S)) -> isNatList(L:S:S)
0.002/0.002	isNat(num0) -> tt
0.002/0.002	isNat(s(N:S:S)) -> isNat(N:S:S)
0.002/0.002	isNatIList(zeros) -> tt
0.002/0.002	isNatIList(cons(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	isNatIList(IL:S:S) -> isNatList(IL:S:S)
0.002/0.002	isNatList(take(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	isNatList(cons(N:S:S,L:S:S)) -> and(isNat(N:S:S),isNatList(L:S:S))
0.002/0.002	isNatList(nil) -> tt
0.002/0.002	length(cons(N:S:S,L:S:S)) -> uLength(and(isNat(N:S:S),isNatList(L:S:S)),L:S:S)
0.002/0.002	take(num0,IL:S:S) -> uTake1(isNatIList(IL:S:S))
0.002/0.002	take(s(M:S:S),cons(N:S:S,IL:S:S)) -> uTake2(and(isNat(M:S:S),and(isNat(N:S:S),isNatIList(IL:S:S))),M:S:S,N:S:S,IL:S:S)
0.002/0.002	uLength(tt,L:S:S) -> s(length(L:S:S))
0.002/0.002	uTake1(tt) -> nil
0.002/0.002	uTake2(tt,M:S:S,N:S:S,IL:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S))
0.002/0.002	zeros -> cons(num0,zeros)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	Modular Confluence Combinations Decomposition Processor:
0.002/0.002	It is a CTRS -> No modular confluence
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	CS-TRS Processor:
0.002/0.002	R is a CS-TRS
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty:S v_NonEmpty:S:S IL:S:S L:S:S M:S:S N:S:S T:S:S)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(and 1)
0.002/0.002	(isNat 1)
0.002/0.002	(isNatIList 1)
0.002/0.002	(isNatList 1)
0.002/0.002	(length 1)
0.002/0.002	(take 1 2)
0.002/0.002	(uLength 1)
0.002/0.002	(uTake1 1)
0.002/0.002	(uTake2 1)
0.002/0.002	(zeros)
0.002/0.002	(cons)
0.002/0.002	(fSNonEmpty)
0.002/0.002	(nil)
0.002/0.002	(num0)
0.002/0.002	(s)
0.002/0.002	(tt)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	and(tt,T:S:S) -> T:S:S
0.002/0.002	isNat(length(L:S:S)) -> isNatList(L:S:S)
0.002/0.002	isNat(num0) -> tt
0.002/0.002	isNat(s(N:S:S)) -> isNat(N:S:S)
0.002/0.002	isNatIList(zeros) -> tt
0.002/0.002	isNatIList(cons(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	isNatIList(IL:S:S) -> isNatList(IL:S:S)
0.002/0.002	isNatList(take(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	isNatList(cons(N:S:S,L:S:S)) -> and(isNat(N:S:S),isNatList(L:S:S))
0.002/0.002	isNatList(nil) -> tt
0.002/0.002	length(cons(N:S:S,L:S:S)) -> uLength(and(isNat(N:S:S),isNatList(L:S:S)),L:S:S)
0.002/0.002	take(num0,IL:S:S) -> uTake1(isNatIList(IL:S:S))
0.002/0.002	take(s(M:S:S),cons(N:S:S,IL:S:S)) -> uTake2(and(isNat(M:S:S),and(isNat(N:S:S),isNatIList(IL:S:S))),M:S:S,N:S:S,IL:S:S)
0.002/0.002	uLength(tt,L:S:S) -> s(length(L:S:S))
0.002/0.002	uTake1(tt) -> nil
0.002/0.002	uTake2(tt,M:S:S,N:S:S,IL:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S))
0.002/0.002	zeros -> cons(num0,zeros)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	Huet Levy Processor:
0.002/0.002	-> Rules:
0.002/0.002	 and(tt,T:S:S) -> T:S:S
0.002/0.002	 isNat(length(L:S:S)) -> isNatList(L:S:S)
0.002/0.002	 isNat(num0) -> tt
0.002/0.002	 isNat(s(N:S:S)) -> isNat(N:S:S)
0.002/0.002	 isNatIList(zeros) -> tt
0.002/0.002	 isNatIList(cons(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	 isNatIList(IL:S:S) -> isNatList(IL:S:S)
0.002/0.002	 isNatList(take(N:S:S,IL:S:S)) -> and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	 isNatList(cons(N:S:S,L:S:S)) -> and(isNat(N:S:S),isNatList(L:S:S))
0.002/0.002	 isNatList(nil) -> tt
0.002/0.002	 length(cons(N:S:S,L:S:S)) -> uLength(and(isNat(N:S:S),isNatList(L:S:S)),L:S:S)
0.002/0.002	 take(num0,IL:S:S) -> uTake1(isNatIList(IL:S:S))
0.002/0.002	 take(s(M:S:S),cons(N:S:S,IL:S:S)) -> uTake2(and(isNat(M:S:S),and(isNat(N:S:S),isNatIList(IL:S:S))),M:S:S,N:S:S,IL:S:S)
0.002/0.002	 uLength(tt,L:S:S) -> s(length(L:S:S))
0.002/0.002	 uTake1(tt) -> nil
0.002/0.002	 uTake2(tt,M:S:S,N:S:S,IL:S:S) -> cons(N:S:S,take(M:S:S,IL:S:S))
0.002/0.002	 zeros -> cons(num0,zeros)
0.002/0.002	-> Vars:
0.002/0.002	 T:S, L:S, N:S, IL:S, N:S, IL:S, IL:S, N:S, L:S, N:S, L:S, N:S, IL:S, IL:S, M:S, N:S, L:S, IL:S, M:S, N:S
0.002/0.002	-> UVars:
0.002/0.002	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [T:S], UV-LFrozen: [T:S], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 2, UV-LActive: [L:S], UV-RActive: [L:S], UV-LFrozen: [], UV-RFrozen: [])
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: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [])
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:S], UV-LFrozen: [IL:S, N:S], UV-RFrozen: [IL:S])
0.002/0.002	 (UV-RuleId: 7, UV-LActive: [IL:S], UV-RActive: [IL:S], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 8, UV-LActive: [IL:S, N:S], UV-RActive: [N:S], UV-LFrozen: [], UV-RFrozen: [IL:S])
0.002/0.002	 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S])
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: [N:S], UV-LFrozen: [L:S, N:S], UV-RFrozen: [L:S])
0.002/0.002	 (UV-RuleId: 12, UV-LActive: [IL:S], UV-RActive: [IL:S], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S])
0.002/0.002	 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [L:S], UV-RFrozen: [L:S])
0.002/0.002	 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [IL:S, M:S, N:S], UV-RFrozen: [IL:S, M:S, N:S])
0.002/0.002	 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.002/0.002	-> FVars:
0.002/0.002	 x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26
0.002/0.002	-> PVars:
0.002/0.002	 T:S: [x7], L:S: [x8, x15, x17, x23], N:S: [x9, x11, x14, x16, x18, x22, x26], IL:S: [x10, x12, x13, x19, x20, x24], M:S: [x21, x25]
0.002/0.002	
0.002/0.002	-> Rlps:
0.002/0.002	 (rule: and(tt,x7:S) -> x7:S, id: 1, possubterms: and(tt,x7:S)->[], tt->[1])
0.002/0.002	 (rule: isNat(length(x8:S)) -> isNatList(x8:S), id: 2, possubterms: isNat(length(x8:S))->[], length(x8:S)->[1])
0.002/0.002	 (rule: isNat(num0) -> tt, id: 3, possubterms: isNat(num0)->[], num0->[1])
0.002/0.002	 (rule: isNat(s(x9:S)) -> isNat(x9:S), id: 4, possubterms: isNat(s(x9:S))->[], s(x9:S)->[1])
0.002/0.002	 (rule: isNatIList(zeros) -> tt, id: 5, possubterms: isNatIList(zeros)->[], zeros->[1])
0.002/0.002	 (rule: isNatIList(cons(x11:S,x10:S)) -> and(isNat(x11:S),isNatIList(x10:S)), id: 6, possubterms: isNatIList(cons(x11:S,x10:S))->[], cons(x11:S,x10:S)->[1])
0.002/0.002	 (rule: isNatIList(x12:S) -> isNatList(x12:S), id: 7, possubterms: isNatIList(x12:S)->[])
0.002/0.002	 (rule: isNatList(take(x14:S,x13:S)) -> and(isNat(x14:S),isNatIList(x13:S)), id: 8, possubterms: isNatList(take(x14:S,x13:S))->[], take(x14:S,x13:S)->[1])
0.002/0.002	 (rule: isNatList(cons(x16:S,x15:S)) -> and(isNat(x16:S),isNatList(x15:S)), id: 9, possubterms: isNatList(cons(x16:S,x15:S))->[], cons(x16:S,x15:S)->[1])
0.002/0.002	 (rule: isNatList(nil) -> tt, id: 10, possubterms: isNatList(nil)->[], nil->[1])
0.002/0.002	 (rule: length(cons(x18:S,x17:S)) -> uLength(and(isNat(x18:S),isNatList(x17:S)),x17:S), id: 11, possubterms: length(cons(x18:S,x17:S))->[], cons(x18:S,x17:S)->[1])
0.002/0.002	 (rule: take(num0,x19:S) -> uTake1(isNatIList(x19:S)), id: 12, possubterms: take(num0,x19:S)->[], num0->[1])
0.002/0.002	 (rule: take(s(x21:S),cons(x22:S,x20:S)) -> uTake2(and(isNat(x21:S),and(isNat(x22:S),isNatIList(x20:S))),x21:S,x22:S,x20:S), id: 13, possubterms: take(s(x21:S),cons(x22:S,x20:S))->[], s(x21:S)->[1], cons(x22:S,x20:S)->[2])
0.002/0.002	 (rule: uLength(tt,x23:S) -> s(length(x23:S)), id: 14, possubterms: uLength(tt,x23:S)->[], tt->[1])
0.002/0.002	 (rule: uTake1(tt) -> nil, id: 15, possubterms: uTake1(tt)->[], tt->[1])
0.002/0.002	 (rule: uTake2(tt,x25:S,x26:S,x24:S) -> cons(x26:S,take(x25:S,x24:S)), id: 16, possubterms: uTake2(tt,x25:S,x26:S,x24:S)->[], tt->[1])
0.002/0.002	 (rule: zeros -> cons(num0,zeros), id: 17, possubterms: zeros->[])
0.002/0.002	
0.002/0.002	-> Unifications:
0.002/0.002	(R2 unifies with R11 at p: [1], l: isNat(length(x8:S)), lp: length(x8:S), sig: {x8:S -> cons(N:S:S,L:S:S)}, l': length(cons(N:S:S,L:S:S)), r: isNatList(x8:S), r': uLength(and(isNat(N:S:S),isNatList(L:S:S)),L:S:S))
0.002/0.002	(R5 unifies with R17 at p: [1], l: isNatIList(zeros), lp: zeros, sig: {}, l': zeros, r: tt, r': cons(num0,zeros))
0.002/0.002	(R7 unifies with R5 at p: [], l: isNatIList(x12:S), lp: isNatIList(x12:S), sig: {x12:S -> zeros}, l': isNatIList(zeros), r: isNatList(x12:S), r': tt)
0.002/0.002	(R7 unifies with R6 at p: [], l: isNatIList(x12:S), lp: isNatIList(x12:S), sig: {x12:S -> cons(N:S:S,IL:S:S)}, l': isNatIList(cons(N:S:S,IL:S:S)), r: isNatList(x12:S), r': and(isNat(N:S:S),isNatIList(IL:S:S)))
0.002/0.002	(R8 unifies with R12 at p: [1], l: isNatList(take(x14:S,x13:S)), lp: take(x14:S,x13:S), sig: {x13:S -> IL:S:S,x14:S -> num0}, l': take(num0,IL:S:S), r: and(isNat(x14:S),isNatIList(x13:S)), r': uTake1(isNatIList(IL:S:S)))
0.002/0.002	(R8 unifies with R13 at p: [1], l: isNatList(take(x14:S,x13:S)), lp: take(x14:S,x13:S), sig: {x13:S -> cons(N:S:S,IL:S:S),x14:S -> s(M:S:S)}, l': take(s(M:S:S),cons(N:S:S,IL:S:S)), r: and(isNat(x14:S),isNatIList(x13:S)), r': uTake2(and(isNat(M:S:S),and(isNat(N:S:S),isNatIList(IL:S:S))),M:S:S,N:S:S,IL:S:S))
0.002/0.002	
0.002/0.002	-> Critical pairs info:
0.002/0.002	<isNatIList(cons(num0,zeros)),tt>   =>  Not trivial, Not overlay, NW0, N1
0.002/0.002	<and(isNat(N:S:S),isNatIList(IL:S:S)),isNatList(cons(N:S:S,IL:S:S))>   =>  Not trivial, Overlay, NW0, N2
0.002/0.002	<isNatList(uTake1(isNatIList(IL:S:S))),and(isNat(num0),isNatIList(IL:S:S))>   =>  Not trivial, Not overlay, NW0, N3
0.002/0.002	<isNat(uLength(and(isNat(N:S:S),isNatList(L:S:S)),L:S:S)),isNatList(cons(N:S:S,L:S:S))>   =>  Not trivial, Not overlay, NW0, N4
0.002/0.002	<tt,isNatList(zeros)>   =>  Not trivial, Overlay, NW0, N5
0.002/0.002	<isNatList(uTake2(and(isNat(M:S:S),and(isNat(N:S:S),isNatIList(IL:S:S))),M:S:S,N:S:S,IL:S:S)),and(isNat(s(M:S:S)),isNatIList(cons(N:S:S,IL:S:S)))>   =>  Not trivial, Not overlay, NW0, N6
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: and(isNat(N:S:S),isNatIList(IL:S:S))
0.002/0.002	Nodes: [0]
0.002/0.002	Edges: []
0.002/0.002	ID: 0 => ('and(isNat(N:S:S),isNatIList(IL:S:S))', D0)
0.002/0.002	t: isNatList(cons(N:S:S,IL:S:S))
0.002/0.002	Nodes: [0,1]
0.002/0.002	Edges: [(0,1)]
0.002/0.002	ID: 0 => ('isNatList(cons(N:S:S,IL:S:S))', D0)
0.002/0.002	ID: 1 => ('and(isNat(N:S:S),isNatList(IL:S:S))', D1, R9, P[], S{x15:S -> IL:S:S, x16:S -> N:S:S}), NR: 'and(isNat(N:S:S),isNatList(IL:S:S))'
0.002/0.002	and(isNat(N:S:S),isNatIList(IL:S:S)) ->* no union *<- isNatList(cons(N:S:S,IL:S:S))
0.002/0.002	"Not joinable"
0.002/0.002	
0.002/0.002	The problem is not joinable.
0.002/0.002	0.00user 0.00system 0:00.02elapsed 59%CPU (0avgtext+0avgdata 10880maxresident)k
0.002/0.002	8inputs+0outputs (0major+995minor)pagefaults 0swaps