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