3.48/1.52	YES
3.48/1.52	
3.48/1.52	Proof:
3.48/1.52	This system is confluent.
3.48/1.52	By \cite{SMI95}, Corollary 4.7 or 5.3.
3.48/1.52	This system is oriented.
3.48/1.52	This system is of type 3 or smaller.
3.48/1.52	This system is right-stable.
3.48/1.52	This system is properly oriented.
3.48/1.52	This is an overlay system.
3.48/1.52	This system is left-linear.
3.48/1.52	All 2 critical pairs are trivial or infeasible.
3.48/1.52	Overlap: (rule1: isnoc(cons(z, z')) -> tp2(cons(z, x'), y') <= isnoc(z') = tp2(x', y'), rule2: isnoc(cons(x, nil)) -> tp2(nil, x), pos: ε, mgu: {(x,z), (z',nil)})
3.48/1.52	CP: tp2(nil, z) = tp2(cons(z, x'), y') <= isnoc(nil) = tp2(x', y')
3.48/1.52	This critical pair is infeasible.
3.48/1.52	This critical pair is conditional.
3.48/1.52	This critical pair has some non-trivial conditions.
3.48/1.52	'tcap_{R_u}(isnoc(nil))' and 'tp2(x', y')' are not unifiable.
3.48/1.52	Overlap: (rule1: isnoc(cons(x, nil)) -> tp2(nil, x), rule2: isnoc(cons(z, z')) -> tp2(cons(z, x'), y') <= isnoc(z') = tp2(x', y'), pos: ε, mgu: {(z,x), (z',nil)})
3.48/1.52	CP: tp2(cons(x, x'), y') = tp2(nil, x) <= isnoc(nil) = tp2(x', y')
3.48/1.52	This critical pair is infeasible.
3.48/1.52	This critical pair is conditional.
3.48/1.52	This critical pair has some non-trivial conditions.
3.48/1.52	'(tp2(x', y'))' is not reachable from '(isnoc(nil))' by generalized tcap using root-symbol analysis.
3.48/1.52	
5.68/2.01	EOF