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