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