(set-logic AUFNIRA) (set-info :status unsat) (declare-sort S1 0) (declare-sort S2 0) (declare-sort S3 0) (declare-sort S4 0) (declare-sort S5 0) (declare-sort S6 0) (declare-sort S7 0) (declare-sort S8 0) (declare-sort S9 0) (declare-sort S10 0) (declare-sort S11 0) (declare-sort S12 0) (declare-sort S13 0) (declare-fun f1 () S1) (declare-fun f2 () S1) (declare-fun f3 (S2 Real) Real) (declare-fun f4 (S3 Real) S2) (declare-fun f5 () S3) (declare-fun f6 (S4 Int) Int) (declare-fun f7 (S5 Int) S4) (declare-fun f8 () S5) (declare-fun f9 () S2) (declare-fun f10 () Real) (declare-fun f11 () Real) (declare-fun f12 () S2) (declare-fun f13 (S7 S6) Real) (declare-fun f14 () S7) (declare-fun f15 () S2) (declare-fun f16 () S2) (declare-fun f17 (S8 Int) S6) (declare-fun f18 () S8) (declare-fun f19 (S9 S6) Int) (declare-fun f20 () S9) (declare-fun f21 (S10 Real) S7) (declare-fun f22 () S10) (declare-fun f23 () S2) (declare-fun f24 (S11 S6) S6) (declare-fun f25 (S12 S6) S11) (declare-fun f26 () S12) (declare-fun f27 () S12) (declare-fun f28 (S13 Int) S9) (declare-fun f29 () S13) (declare-fun f30 () S2) (declare-fun f31 () S4) (assert (not (= f1 f2))) (assert (forall ((?v0 Real) (?v1 Real)) (= (f3 (f4 f5 ?v0) ?v1) (* ?v0 ?v1)))) (assert (forall ((?v0 Int) (?v1 Int)) (= (f6 (f7 f8 ?v0) ?v1) (* ?v0 ?v1)))) (assert (not (= (f3 f9 (- f10 f11)) (- (f3 f9 f10))))) (assert (= (f3 f9 f11) 0.0)) (assert (forall ((?v0 Real)) (= (f3 f9 (+ f11 ?v0)) (- (f3 f9 ?v0))))) (assert (= (f3 f9 (/ f11 2.0)) 1.0)) (assert (= (f3 f9 (/ f11 6.0)) (/ 1.0 2.0))) (assert (= (f3 f9 (* 2.0 f11)) 0.0)) (assert (= (f3 f9 (* (/ 3.0 2.0) f11)) (- 1.0))) (assert (let ((?v_0 2.0)) (<= (/ f11 ?v_0) ?v_0))) (assert (let ((?v_0 2.0)) (< (/ f11 ?v_0) ?v_0))) (assert (< (- (* 2.0 f11)) f11)) (assert (< (- (/ f11 2.0)) 0.0)) (assert (<= 2.0 f11)) (assert (<= 0.0 (/ f11 2.0))) (assert (< 0.0 (/ f11 2.0))) (assert (< f11 4.0)) (assert (<= 0.0 f11)) (assert (< 0.0 f11)) (assert (let ((?v_0 2.0)) (not (= (/ f11 ?v_0) ?v_0)))) (assert (not (= (/ f11 2.0) 0.0))) (assert (not (< f11 0.0))) (assert (not (= f11 0.0))) (assert (forall ((?v0 S6) (?v1 S6)) (= (= (f13 f14 ?v0) (f13 f14 ?v1)) (= ?v0 ?v1)))) (assert (forall ((?v0 S6) (?v1 S6)) (= (< (f13 f14 ?v0) (f13 f14 ?v1)) (< (f19 f20 ?v0) (f19 f20 ?v1))))) (assert (forall ((?v0 S6) (?v1 S6)) (= (<= (f13 f14 ?v0) (f13 f14 ?v1)) (<= (f19 f20 ?v0) (f19 f20 ?v1))))) (assert (forall ((?v0 S6) (?v1 S6)) (let ((?v_0 (f19 f20 ?v1)) (?v_1 (f19 f20 ?v0))) (=> (<= ?v_1 ?v_0) (= (f13 f14 (f17 f18 (- ?v_0 ?v_1))) (- (f13 f14 ?v1) (f13 f14 ?v0))))))) (assert (forall ((?v0 Real) (?v1 Real)) (exists ((?v2 Real) (?v3 Real)) (and (= ?v0 (* ?v2 (f3 f15 ?v3))) (= ?v1 (* ?v2 (f3 f9 ?v3))))))) (assert (< 1.0 (f3 f16 2.0))) (assert (< 0.0 (f3 f16 2.0))) (assert (<= 0.0 (f3 f16 2.0))) (assert (forall ((?v0 Real) (?v1 Real)) (<= 0.0 (f3 f16 (+ (* ?v0 ?v0) (* ?v1 ?v1)))))) (assert (forall ((?v0 Real) (?v1 Real)) (=> (<= ?v0 ?v1) (<= (f3 f16 ?v0) (f3 f16 ?v1))))) (assert (forall ((?v0 Real) (?v1 Real)) (=> (< ?v0 ?v1) (< (f3 f16 ?v0) (f3 f16 ?v1))))) (assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (=> (= (f3 f16 ?v0) ?v_0) (= ?v0 ?v_0)))))) (assert (forall ((?v0 Real)) (=> (< 0.0 ?v0) (< (/ ?v0 (f3 f16 2.0)) ?v0)))) (assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0)))))) (assert (forall ((?v0 Real)) (let ((?v_0 1.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0)))))) (check-sat) (exit)