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