33010
|
1 |
#2 := false
|
|
2 |
#5 := (:var 0 int)
|
|
3 |
#7 := 0::int
|
|
4 |
#9 := (<= 0::int #5)
|
|
5 |
#8 := (< #5 0::int)
|
|
6 |
#10 := (or #8 #9)
|
|
7 |
#4 := (:var 1 int)
|
|
8 |
#6 := (< #4 #5)
|
|
9 |
#11 := (implies #6 #10)
|
|
10 |
#12 := (forall (vars (?x2 int)) #11)
|
|
11 |
#13 := (exists (vars (?x1 int)) #12)
|
|
12 |
#14 := (not #13)
|
|
13 |
#95 := (iff #14 false)
|
|
14 |
#31 := (not #6)
|
|
15 |
#32 := (or #31 #10)
|
|
16 |
#35 := (forall (vars (?x2 int)) #32)
|
|
17 |
#38 := (exists (vars (?x1 int)) #35)
|
|
18 |
#41 := (not #38)
|
|
19 |
#93 := (iff #41 false)
|
|
20 |
#1 := true
|
|
21 |
#88 := (not true)
|
|
22 |
#91 := (iff #88 false)
|
|
23 |
#92 := [rewrite]: #91
|
|
24 |
#89 := (iff #41 #88)
|
|
25 |
#86 := (iff #38 true)
|
|
26 |
#81 := (exists (vars (?x1 int)) true)
|
|
27 |
#84 := (iff #81 true)
|
|
28 |
#85 := [elim-unused]: #84
|
|
29 |
#82 := (iff #38 #81)
|
|
30 |
#79 := (iff #35 true)
|
|
31 |
#74 := (forall (vars (?x2 int)) true)
|
|
32 |
#77 := (iff #74 true)
|
|
33 |
#78 := [elim-unused]: #77
|
|
34 |
#75 := (iff #35 #74)
|
|
35 |
#72 := (iff #32 true)
|
|
36 |
#46 := (>= #5 0::int)
|
|
37 |
#44 := (not #46)
|
|
38 |
#64 := (or #44 #46)
|
|
39 |
#50 := -1::int
|
|
40 |
#53 := (* -1::int #5)
|
|
41 |
#54 := (+ #4 #53)
|
|
42 |
#52 := (>= #54 0::int)
|
|
43 |
#67 := (or #52 #64)
|
|
44 |
#70 := (iff #67 true)
|
|
45 |
#71 := [rewrite]: #70
|
|
46 |
#68 := (iff #32 #67)
|
|
47 |
#65 := (iff #10 #64)
|
|
48 |
#48 := (iff #9 #46)
|
|
49 |
#49 := [rewrite]: #48
|
|
50 |
#45 := (iff #8 #44)
|
|
51 |
#47 := [rewrite]: #45
|
|
52 |
#66 := [monotonicity #47 #49]: #65
|
|
53 |
#62 := (iff #31 #52)
|
|
54 |
#51 := (not #52)
|
|
55 |
#57 := (not #51)
|
|
56 |
#60 := (iff #57 #52)
|
|
57 |
#61 := [rewrite]: #60
|
|
58 |
#58 := (iff #31 #57)
|
|
59 |
#55 := (iff #6 #51)
|
|
60 |
#56 := [rewrite]: #55
|
|
61 |
#59 := [monotonicity #56]: #58
|
|
62 |
#63 := [trans #59 #61]: #62
|
|
63 |
#69 := [monotonicity #63 #66]: #68
|
|
64 |
#73 := [trans #69 #71]: #72
|
|
65 |
#76 := [quant-intro #73]: #75
|
|
66 |
#80 := [trans #76 #78]: #79
|
|
67 |
#83 := [quant-intro #80]: #82
|
|
68 |
#87 := [trans #83 #85]: #86
|
|
69 |
#90 := [monotonicity #87]: #89
|
|
70 |
#94 := [trans #90 #92]: #93
|
|
71 |
#42 := (iff #14 #41)
|
|
72 |
#39 := (iff #13 #38)
|
|
73 |
#36 := (iff #12 #35)
|
|
74 |
#33 := (iff #11 #32)
|
|
75 |
#34 := [rewrite]: #33
|
|
76 |
#37 := [quant-intro #34]: #36
|
|
77 |
#40 := [quant-intro #37]: #39
|
|
78 |
#43 := [monotonicity #40]: #42
|
|
79 |
#96 := [trans #43 #94]: #95
|
|
80 |
#30 := [asserted]: #14
|
|
81 |
[mp #30 #96]: false
|
|
82 |
unsat
|