YES

Proof:
This system is confluent.
By \cite{SMI95}, Corollary 4.7 or 5.3.
This system is not normal.
This system is oriented.
This system is of type 3 or smaller.
This system is right-stable.
This system is properly oriented.
This is an overlay system.
This system is left-linear.
All 2 critical pairs are trivial or infeasible.
tp2(nil, x) = tp2(cons(x, y), z') <= isnoc(nil) = tp2(y, z'):
This critical pair is not trivial.
This critical pair is conditional.
This critical pair has some non-trivial conditions.
'tcap(?1(isnoc(nil)))' is not unifiable with '?1(tp2(y, z'))'.
tp2(cons(y, z), z') = tp2(nil, y) <= isnoc(nil) = tp2(z, z'):
This critical pair is not trivial.
This critical pair is conditional.
This critical pair has some non-trivial conditions.
'tcap(?1(isnoc(nil)))' is not unifiable with '?1(tp2(z, z'))'.
This system is conditional.