|
1 #2 := false |
|
2 #4 := 0::int |
|
3 decl ?x2!1 :: int |
|
4 #91 := ?x2!1 |
|
5 #98 := (<= ?x2!1 0::int) |
|
6 #99 := (not #98) |
|
7 #7 := 0::real |
|
8 decl ?x3!0 :: real |
|
9 #93 := ?x3!0 |
|
10 #96 := (<= ?x3!0 0::real) |
|
11 #97 := (not #96) |
|
12 #111 := (and #97 #99) |
|
13 #114 := (not #111) |
|
14 #33 := -1::int |
|
15 #94 := (<= ?x2!1 -1::int) |
|
16 #95 := (not #94) |
|
17 #120 := (or #95 #114) |
|
18 #125 := (not #120) |
|
19 #100 := (and #99 #97) |
|
20 #101 := (not #100) |
|
21 #102 := (or #101 #95) |
|
22 #103 := (not #102) |
|
23 #126 := (iff #103 #125) |
|
24 #123 := (iff #102 #120) |
|
25 #117 := (or #114 #95) |
|
26 #121 := (iff #117 #120) |
|
27 #122 := [rewrite]: #121 |
|
28 #118 := (iff #102 #117) |
|
29 #115 := (iff #101 #114) |
|
30 #112 := (iff #100 #111) |
|
31 #113 := [rewrite]: #112 |
|
32 #116 := [monotonicity #113]: #115 |
|
33 #119 := [monotonicity #116]: #118 |
|
34 #124 := [trans #119 #122]: #123 |
|
35 #127 := [monotonicity #124]: #126 |
|
36 #5 := (:var 1 int) |
|
37 #75 := (<= #5 -1::int) |
|
38 #76 := (not #75) |
|
39 #8 := (:var 0 real) |
|
40 #65 := (<= #8 0::real) |
|
41 #66 := (not #65) |
|
42 #61 := (<= #5 0::int) |
|
43 #62 := (not #61) |
|
44 #69 := (and #62 #66) |
|
45 #72 := (not #69) |
|
46 #79 := (or #72 #76) |
|
47 #82 := (forall (vars (?x2 int) (?x3 real)) #79) |
|
48 #85 := (not #82) |
|
49 #104 := (~ #85 #103) |
|
50 #105 := [sk]: #104 |
|
51 #11 := 1::int |
|
52 #12 := (- 1::int) |
|
53 #13 := (< #12 #5) |
|
54 #9 := (< 0::real #8) |
|
55 #6 := (< 0::int #5) |
|
56 #10 := (and #6 #9) |
|
57 #14 := (implies #10 #13) |
|
58 #15 := (forall (vars (?x2 int) (?x3 real)) #14) |
|
59 #16 := (exists (vars (?x1 int)) #15) |
|
60 #17 := (not #16) |
|
61 #88 := (iff #17 #85) |
|
62 #36 := (< -1::int #5) |
|
63 #42 := (not #10) |
|
64 #43 := (or #42 #36) |
|
65 #48 := (forall (vars (?x2 int) (?x3 real)) #43) |
|
66 #58 := (not #48) |
|
67 #86 := (iff #58 #85) |
|
68 #83 := (iff #48 #82) |
|
69 #80 := (iff #43 #79) |
|
70 #77 := (iff #36 #76) |
|
71 #78 := [rewrite]: #77 |
|
72 #73 := (iff #42 #72) |
|
73 #70 := (iff #10 #69) |
|
74 #67 := (iff #9 #66) |
|
75 #68 := [rewrite]: #67 |
|
76 #63 := (iff #6 #62) |
|
77 #64 := [rewrite]: #63 |
|
78 #71 := [monotonicity #64 #68]: #70 |
|
79 #74 := [monotonicity #71]: #73 |
|
80 #81 := [monotonicity #74 #78]: #80 |
|
81 #84 := [quant-intro #81]: #83 |
|
82 #87 := [monotonicity #84]: #86 |
|
83 #59 := (iff #17 #58) |
|
84 #56 := (iff #16 #48) |
|
85 #51 := (exists (vars (?x1 int)) #48) |
|
86 #54 := (iff #51 #48) |
|
87 #55 := [elim-unused]: #54 |
|
88 #52 := (iff #16 #51) |
|
89 #49 := (iff #15 #48) |
|
90 #46 := (iff #14 #43) |
|
91 #39 := (implies #10 #36) |
|
92 #44 := (iff #39 #43) |
|
93 #45 := [rewrite]: #44 |
|
94 #40 := (iff #14 #39) |
|
95 #37 := (iff #13 #36) |
|
96 #34 := (= #12 -1::int) |
|
97 #35 := [rewrite]: #34 |
|
98 #38 := [monotonicity #35]: #37 |
|
99 #41 := [monotonicity #38]: #40 |
|
100 #47 := [trans #41 #45]: #46 |
|
101 #50 := [quant-intro #47]: #49 |
|
102 #53 := [quant-intro #50]: #52 |
|
103 #57 := [trans #53 #55]: #56 |
|
104 #60 := [monotonicity #57]: #59 |
|
105 #89 := [trans #60 #87]: #88 |
|
106 #32 := [asserted]: #17 |
|
107 #90 := [mp #32 #89]: #85 |
|
108 #108 := [mp~ #90 #105]: #103 |
|
109 #109 := [mp #108 #127]: #125 |
|
110 #128 := [not-or-elim #109]: #111 |
|
111 #130 := [and-elim #128]: #99 |
|
112 #110 := [not-or-elim #109]: #94 |
|
113 #186 := (or #95 #98) |
|
114 #187 := [th-lemma]: #186 |
|
115 #188 := [unit-resolution #187 #110]: #98 |
|
116 [unit-resolution #188 #130]: false |
|
117 unsat |