1.71/0.92	YES
1.71/0.92	
1.71/0.92	Proof:
1.71/0.92	This system is confluent.
1.71/0.92	By \cite{SMI95}, Corollary 4.7 or 5.3.
1.71/0.92	This system is oriented.
1.71/0.92	This system is of type 3 or smaller.
1.71/0.92	This system is right-stable.
1.71/0.92	This system is properly oriented.
1.71/0.92	This is an overlay system.
1.71/0.92	This system is left-linear.
1.71/0.92	All 2 critical pairs are trivial or infeasible.
1.71/0.92	Overlap: (rule1: filter(z', $1, cons(y', z)) -> pair($2, cons(y', ys)) <= filter(z', $1, z) = pair($2, ys), eq(div(y', z'), pair(x', $1)) = false, rule2: filter($3, $5, cons($4, y)) -> pair($4, y) <= eq(div($4, $3), pair($6, $5)) = true, pos: ε, mgu: {($3,z'), ($5,$1), ($4,y'), (y,z)})
1.71/0.92	CP: pair(y', z) = pair($2, cons(y', ys)) <= filter(z', $1, z) = pair($2, ys), eq(div(y', z'), pair(x', $1)) = false, eq(div(y', z'), pair($6, $1)) = true
1.71/0.92	This critical pair is infeasible.
1.71/0.92	This critical pair is conditional.
1.71/0.92	This critical pair has some non-trivial conditions.
1.71/0.92	'tcap_{R_u}(conds(filter(z', $1, z), eq(div(y', z'), pair(x', $1)), eq(div(y', z'), pair($6, $1))))' and 'conds(pair($2, ys), false, true)' are not unifiable.
1.71/0.92	Overlap: (rule1: filter(z', y, cons(y', z)) -> pair(y', z) <= eq(div(y', z'), pair(x', y)) = true, rule2: filter($3, $5, cons($4, $1)) -> pair($2, cons($4, ys)) <= filter($3, $5, $1) = pair($2, ys), eq(div($4, $3), pair($6, $5)) = false, pos: ε, mgu: {($3,z'), ($5,y), ($4,y'), ($1,z)})
1.71/0.92	CP: pair($2, cons(y', ys)) = pair(y', z) <= eq(div(y', z'), pair(x', y)) = true, filter(z', y, z) = pair($2, ys), eq(div(y', z'), pair($6, y)) = false
1.71/0.92	This critical pair is infeasible.
1.71/0.92	This critical pair is conditional.
1.71/0.92	This critical pair has some non-trivial conditions.
1.71/0.92	'(true,pair($2, ys),false)' is not reachable from '(eq(div(y', z'), pair(x', y)),filter(z', y, z),eq(div(y', z'), pair($6, y)))' by generalized tcap using root-symbol analysis.
1.71/0.92	
1.73/0.95	EOF