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