(set-logic QF_RDL)
(set-info :status unsat)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-sort U 0)
(declare-sort A 2)
(define-sort F (x) (A Real Real))
(declare-fun x2 () (F Real))
(define-fun minus ((x Real) (z Real)) Real (- x z))
(define-fun less ((x Real) (z Real)) Real (< x z))
(define-fun foo ((x Real) (z Real)) Bool (less x z))
(assert (not (=> (foo (minus x y) 0) (less x y))))
(check-sat)
(exit)