0.00/0.00	YES
0.00/0.00	
0.00/0.00	Problem 1: 
0.00/0.00	
0.00/0.00	
0.00/0.00	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.00	Confluence Problem:
0.00/0.00	(VAR vNonEmpty L N X)
0.00/0.00	(REPLACEMENT-MAP
0.00/0.00	(and 1)
0.00/0.00	(length 1)
0.00/0.00	(zeros)
0.00/0.00	(0)
0.00/0.00	(cons 1)
0.00/0.00	(fSNonEmpty)
0.00/0.00	(nil)
0.00/0.00	(s 1)
0.00/0.00	(tt)
0.00/0.00	)
0.00/0.00	(RULES
0.00/0.00	and(tt,X) -> X
0.00/0.00	length(cons(N,L)) -> s(length(L))
0.00/0.00	length(nil) -> 0
0.00/0.00	zeros -> cons(0,zeros)
0.00/0.00	)
0.00/0.00	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.00	
0.00/0.00	
0.00/0.00	Problem 1: 
0.00/0.00	
0.00/0.00	Problem 1: 
0.00/0.00	Left-Homogeneous u-Replacing Variables Procedure:
0.00/0.00	R satisfies LHRV condition
0.00/0.00	
0.00/0.00	Problem 1: 
0.00/0.00	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.00	Confluence Problem:
0.00/0.00	(VAR vNonEmpty L N X)
0.00/0.00	(REPLACEMENT-MAP
0.00/0.00	(and 1)
0.00/0.00	(length 1)
0.00/0.00	(zeros)
0.00/0.00	(0)
0.00/0.00	(cons 1)
0.00/0.00	(fSNonEmpty)
0.00/0.00	(nil)
0.00/0.00	(s 1)
0.00/0.00	(tt)
0.00/0.00	)
0.00/0.00	(RULES
0.00/0.00	and(tt,X) -> X
0.00/0.00	length(cons(N,L)) -> s(length(L))
0.00/0.00	length(nil) -> 0
0.00/0.00	zeros -> cons(0,zeros)
0.00/0.00	)
0.00/0.00	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.00	
0.00/0.00	Huet Levy Procedure:
0.00/0.00	-> Rules:
0.00/0.00	 and(tt,X) -> X
0.00/0.00	 length(cons(N,L)) -> s(length(L))
0.00/0.00	 length(nil) -> 0
0.00/0.00	 zeros -> cons(0,zeros)
0.00/0.00	-> Vars:
0.00/0.00	 X, L, N
0.00/0.00	-> UVars:
0.00/0.00	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: [])
0.00/0.00	 (UV-RuleId: 2, UV-LActive: [N], UV-RActive: [L], UV-LFrozen: [L], UV-RFrozen: [])
0.00/0.00	 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.00/0.00	 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.00/0.00	
0.00/0.00	-> Rlps:
0.00/0.00	 (rule: and(tt,X) -> X, id: 1, possubterms: and(tt,X)->[], tt->[1])
0.00/0.00	 (rule: length(cons(N,L)) -> s(length(L)), id: 2, possubterms: length(cons(N,L))->[], cons(N,L)->[1])
0.00/0.00	 (rule: length(nil) -> 0, id: 3, possubterms: length(nil)->[], nil->[1])
0.00/0.00	 (rule: zeros -> cons(0,zeros), id: 4, possubterms: zeros->[])
0.00/0.00	
0.00/0.00	-> Unifications:
0.00/0.00	
0.00/0.00	
0.00/0.00	-> Critical pairs info:
0.00/0.00	
0.00/0.00	
0.00/0.00	-> Problem conclusions:
0.00/0.00	 Left linear, Right linear, Linear
0.00/0.00	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.00/0.00	 Huet-Levy confluent, Not Newman confluent
0.00/0.00	 R is a CS-TRS, Left-homogeneous u-replacing variables
0.00/0.00	
0.00/0.00	
0.00/0.00	The problem is confluent.
0.00/0.01	EOF