blob: aad2a4691e5f6c76abc02a7f18f5eef6f7e97775 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
(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)
|
