{ satisfiable, but engine gets into a loop 
  while building an infinite model         }

@c 
  conj (
         <>T, 
         [][]<~>c, 
         [] conj (<>T,
                  down x []-x, 
                  down x [][]-x, 
                  down x [][]<~>x )
       )