8.73/3.02	YES
8.73/3.02	
8.73/3.02	Proof:
8.73/3.02	This system is confluent.
8.73/3.02	By \cite{SMI95}, Corollary 4.7 or 5.3.
8.73/3.02	This system is oriented.
8.73/3.02	This system is of type 3 or smaller.
8.73/3.02	This system is right-stable.
8.73/3.02	This system is properly oriented.
8.73/3.02	This is an overlay system.
8.73/3.02	This system is left-linear.
8.73/3.02	All 2 critical pairs are trivial or infeasible.
8.73/3.02	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: {(z,x), (z',nil)})
8.73/3.02	CP: tp2(nil, x) = tp2(cons(x, x'), y') <= isnoc(nil) = tp2(x', y')
8.73/3.02	This critical pair is infeasible.
8.73/3.02	This critical pair is conditional.
8.73/3.02	This critical pair has some non-trivial conditions.
8.73/3.02	Call external tool:
8.73/3.02	./waldmeister
8.73/3.02	Input:
8.73/3.02	  isnoc(cons(y, nil)) -> tp2(nil, y)
8.73/3.02	  isnoc(cons(x, ys)) -> tp2(cons(x, xs), y) <= isnoc(ys) = tp2(xs, y)
8.73/3.02	
8.73/3.02	By Waldmeister.
8.73/3.02	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: {(x,z), (z',nil)})
8.73/3.02	CP: tp2(cons(z, x'), y') = tp2(nil, z) <= isnoc(nil) = tp2(x', y')
8.73/3.02	This critical pair is infeasible.
8.73/3.02	This critical pair is conditional.
8.73/3.02	This critical pair has some non-trivial conditions.
8.73/3.02	Call external tool:
8.73/3.02	./waldmeister
8.73/3.02	Input:
8.73/3.02	  isnoc(cons(y, nil)) -> tp2(nil, y)
8.73/3.02	  isnoc(cons(x, ys)) -> tp2(cons(x, xs), y) <= isnoc(ys) = tp2(xs, y)
8.73/3.02	
8.73/3.02	By Waldmeister.
8.73/3.02	
9.10/3.17	EOF