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