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