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