and(implies(implies(v, w), implies(or(or(or(or(w, u), not(some(r, u))), not(and(not(some(r, v)), all(r, all(r, u))))), u), some(r, all(r, some(r, v))))), not(implies(implies(v, w), implies(or(or(or(or(w, u), not(some(r, u))), not(and(not(some(r, v)), all(r, all(r, u))))), u), some(r, all(r, some(r, v))))))