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