(define <<::(-> int int bool)) (assert (forall (x::int y::int z::int) (implies (and (<< x y) (<< y z)) (<< x z)))) (assert (forall (x::int y::int) (implies (<< x y) (/= x y)))) (define x1::int) (define x2::int) (define x3::int) (define x4::int) (assert (<< x1 x2)) (assert (<< x2 x3)) (assert (<< x3 x4)) (assert (not (<< x1 x4))) (check)