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