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 X:S)
0.001/0.001	(STRATEGY CONTEXTSENSITIVE
0.001/0.001	(and 1)
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	and(tt,X:S) -> X:S
0.001/0.001	length(cons(N:S,L:S)) -> s(length(L:S))
0.001/0.001	length(nil) -> 0
0.001/0.001	take(0,IL:S) -> nil
0.001/0.001	take(s(M:S),cons(N:S,IL:S)) -> cons(N:S,take(M:S,IL: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 X:S)
0.001/0.001	(STRATEGY CONTEXTSENSITIVE
0.001/0.001	(and 1)
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	and(tt,X:S) -> X:S
0.001/0.001	length(cons(N:S,L:S)) -> s(length(L:S))
0.001/0.001	length(nil) -> 0
0.001/0.001	take(0,IL:S) -> nil
0.001/0.001	take(s(M:S),cons(N:S,IL:S)) -> cons(N:S,take(M:S,IL: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 X:S)
0.001/0.001	(STRATEGY CONTEXTSENSITIVE
0.001/0.001	(and 1)
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	and(tt,X:S) -> X:S
0.001/0.001	length(cons(N:S,L:S)) -> s(length(L:S))
0.001/0.001	length(nil) -> 0
0.001/0.001	take(0,IL:S) -> nil
0.001/0.001	take(s(M:S),cons(N:S,IL:S)) -> cons(N:S,take(M:S,IL: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	Extended u-Critical Pairs NonLHRV Processor [JLAMP21]:
0.001/0.001	->Extended u-Critical Pair:
0.001/0.001	 Rule 1 (l :-> r) => take(s(x11:S),cons(x12:S,x10:S)) -> cons(x12:S,take(x11:S,x10:S))
0.001/0.001	 Rule 5 (l' :-> r') => take(s(M:S),cons(N:S,IL:S)) -> cons(N:S,take(M:S,IL:S))
0.001/0.001	 Var => x11:S
0.001/0.001	 Pos x11:S in l => [1,1]
0.001/0.001	 Sigma => {x11:S -> take(s(M:S),cons(N:S,IL:S))}
0.001/0.001	 s => cons(x12:S,take(take(s(M:S),cons(N:S,IL:S)),x10:S))
0.001/0.001	 t => take(s(cons(N:S,take(M:S,IL:S))),cons(x12:S,x10:S))
0.001/0.001	 NW => 1
0.001/0.001	
0.001/0.001	
0.001/0.001	->Extended u-Critical Pair:
0.001/0.001	 Rule 1 (l :-> r) => take(s(x11:S),cons(x12:S,x10:S)) -> cons(x12:S,take(x11:S,x10:S))
0.001/0.001	 Rule 6 (l' :-> r') => zeros -> cons(0,zeros)
0.001/0.001	 Var => x11:S
0.001/0.001	 Pos x11:S in l => [1,1]
0.001/0.001	 Sigma => {x11:S -> zeros}
0.001/0.001	 s => cons(x12:S,take(zeros,x10:S))
0.001/0.001	 t => take(s(cons(0,zeros)),cons(x12:S,x10:S))
0.001/0.001	 NW => 1
0.001/0.001	
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 X:S)
0.001/0.001	(STRATEGY CONTEXTSENSITIVE
0.001/0.001	(and 1)
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	and(tt,X:S) -> X:S
0.001/0.001	length(cons(N:S,L:S)) -> s(length(L:S))
0.001/0.001	length(nil) -> 0
0.001/0.001	take(0,IL:S) -> nil
0.001/0.001	take(s(M:S),cons(N:S,IL:S)) -> cons(N:S,take(M:S,IL:S))
0.001/0.001	zeros -> cons(0,zeros)
0.001/0.001	)
0.001/0.001	Critical Pairs:
0.001/0.001	<cons(x12:S,take(take(s(M:S),cons(N:S,IL:S)),x10:S)),take(s(cons(N:S,take(M:S,IL:S))),cons(x12:S,x10:S))>   =>  Not trivial, Not overlay, NW1, N1
0.001/0.001	<cons(x12:S,take(zeros,x10:S)),take(s(cons(0,zeros)),cons(x12:S,x10:S))>   =>  Not trivial, Not overlay, NW1, N2
0.001/0.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.001/0.001	
0.001/0.001	Huet Levy Processor:
0.001/0.001	-> Rules:
0.001/0.001	 and(tt,X:S) -> X:S
0.001/0.001	 length(cons(N:S,L:S)) -> s(length(L:S))
0.001/0.001	 length(nil) -> 0
0.001/0.001	 take(0,IL:S) -> nil
0.001/0.001	 take(s(M:S),cons(N:S,IL:S)) -> cons(N:S,take(M:S,IL:S))
0.001/0.001	 zeros -> cons(0,zeros)
0.001/0.001	-> Vars:
0.001/0.001	 X, L, N, IL, IL, M, N
0.001/0.001	-> UVars:
0.001/0.001	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 2, UV-LActive: [N], UV-RActive: [L], UV-LFrozen: [L], 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: [IL], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	 (UV-RuleId: 5, UV-LActive: [M, N], UV-RActive: [N], UV-LFrozen: [IL], UV-RFrozen: [IL, M])
0.001/0.001	 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.001/0.001	-> FVars:
0.001/0.001	 x6, x7, x8, x9, x10, x11, x12
0.001/0.001	-> PVars:
0.001/0.001	 X: [x6], L: [x7], N: [x8, x12], IL: [x9, x10], M: [x11]
0.001/0.001	
0.001/0.001	-> Rlps:
0.001/0.001	 (rule: and(tt,x6:S) -> x6:S, id: 1, possubterms: and(tt,x6:S)->[], tt->[1])
0.001/0.001	 (rule: length(cons(x8:S,x7:S)) -> s(length(x7:S)), id: 2, possubterms: length(cons(x8:S,x7:S))->[], cons(x8:S,x7:S)->[1])
0.001/0.001	 (rule: length(nil) -> 0, id: 3, possubterms: length(nil)->[], nil->[1])
0.001/0.001	 (rule: take(0,x9:S) -> nil, id: 4, possubterms: take(0,x9:S)->[], 0->[1])
0.001/0.001	 (rule: take(s(x11:S),cons(x12:S,x10:S)) -> cons(x12:S,take(x11:S,x10:S)), id: 5, possubterms: take(s(x11:S),cons(x12:S,x10:S))->[], s(x11:S)->[1], cons(x12:S,x10:S)->[2])
0.001/0.001	 (rule: zeros -> cons(0,zeros), id: 6, possubterms: zeros->[])
0.001/0.001	
0.001/0.001	-> Unifications:
0.001/0.001	
0.001/0.001	
0.001/0.001	-> Critical pairs info:
0.001/0.001	<cons(N:S,take(take(s(M:S),cons(N:S,IL:S)),IL:S)),take(s(cons(N:S,take(M:S,IL:S))),cons(N:S,IL:S))>   =>  Not trivial, Not overlay, NW1, N1
0.001/0.001	<cons(N:S,take(zeros,IL:S)),take(s(cons(0,zeros)),cons(N:S,IL:S))>   =>  Not trivial, Not overlay, NW1, N2
0.001/0.001	
0.001/0.001	-> Problem conclusions:
0.001/0.001	 Left linear, Right linear, 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	No Convergence Brute Force Processor:
0.001/0.001	-> Rewritings:
0.001/0.001	s: cons(N:S,take(take(s(M:S),cons(N:S,IL:S)),IL:S))
0.001/0.001	Nodes: [0]
0.001/0.001	Edges: []
0.001/0.001	ID: 0 => ('cons(N:S,take(take(s(M:S),cons(N:S,IL:S)),IL:S))', D0)
0.001/0.001	t: take(s(cons(N:S,take(M:S,IL:S))),cons(N:S,IL:S))
0.001/0.001	Nodes: [0,1]
0.001/0.001	Edges: [(0,1)]
0.001/0.001	ID: 0 => ('take(s(cons(N:S,take(M:S,IL:S))),cons(N:S,IL:S))', D0)
0.001/0.001	ID: 1 => ('cons(N:S,take(cons(N:S,take(M:S,IL:S)),IL:S))', D1, R5, P[], S{x10:S -> IL:S, x11:S -> cons(N:S,take(M:S,IL:S)), x12:S -> N:S}), NR: 'cons(N:S,take(cons(N:S,take(M:S,IL:S)),IL:S))'
0.001/0.001	cons(N:S,take(take(s(M:S),cons(N:S,IL:S)),IL:S)) ->* no union *<- take(s(cons(N:S,take(M:S,IL:S))),cons(N:S,IL:S))
0.001/0.001	"Not joinable"
0.001/0.001	
0.001/0.001	The problem is not joinable.
0.001/0.001	0.00user 0.00system 0:00.01elapsed 50%CPU (0avgtext+0avgdata 9800maxresident)k
0.001/0.001	0inputs+0outputs (0major+791minor)pagefaults 0swaps