and(and(u, some(r, implies(not(not(implies(u, not(u)))), and(not(u), u)))), not(and(u, some(r, implies(not(not(implies(u, not(u)))), and(not(u), u)))))