(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)