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