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