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.
pair(x, $3) = pair($7, cons(x, ys)) <= filter($5, $8, $3) = pair($7, ys), eq(div(x, $5), pair(y, $8)) = false, eq(div(x, $5), pair($4, $8)) = true:
This critical pair is not trivial.
This critical pair is conditional.
This critical pair has some non-trivial conditions.
'tcap(?1(filter($5, $8, $3), eq(div(x, $5), pair(y, $8)), eq(div(x, $5), pair($4, $8))))' is not unifiable with '?1(pair($7, ys), false, true)'.
pair($3, cons($1, ys)) = pair($1, $8) <= eq(div($1, x), pair($4, $5)) = true, filter(x, $5, $8) = pair($3, ys), eq(div($1, x), pair($7, $5)) = false:
This critical pair is not trivial.
This critical pair is conditional.
This critical pair has some non-trivial conditions.
'tcap(?1(eq(div($1, x), pair($4, $5)), filter(x, $5, $8), eq(div($1, x), pair($7, $5))))' is not unifiable with '?1(true, pair($3, ys), false)'.
This system is conditional.