{ unsatisfiable } conj ( down x [][]<~>x, { transitive } down x [][]-x, { asymmetric } down x <>x { reflexive } )