(REWRITE (forall ($@vars $t $u $v) $dummy1 
    (or (not (and (<: $t $u) (<: $u $v))) (<: $t $v))) true)
  (REWRITE (forall ($@vars $t $u) $dummy1 
    (or (not (and (<: $t $u) (<: $u $t))) (= $t $u))) true)