|
1 #2 := false |
|
2 decl up_35 :: (-> int bool) |
|
3 #112 := 1::int |
|
4 #113 := (up_35 1::int) |
|
5 #114 := (not #113) |
|
6 #297 := [asserted]: #114 |
|
7 #103 := (:var 0 int) |
|
8 #104 := (up_35 #103) |
|
9 #911 := (pattern #104) |
|
10 #912 := (forall (vars (?x12 int)) (:pat #911) #104) |
|
11 #294 := (forall (vars (?x12 int)) #104) |
|
12 #915 := (iff #294 #912) |
|
13 #913 := (iff #104 #104) |
|
14 #914 := [refl]: #913 |
|
15 #916 := [quant-intro #914]: #915 |
|
16 #320 := (~ #294 #294) |
|
17 #361 := (~ #104 #104) |
|
18 #362 := [refl]: #361 |
|
19 #321 := [nnf-pos #362]: #320 |
|
20 decl up_32 :: (-> T13 bool) |
|
21 decl uf_36 :: (-> int T13 T13) |
|
22 decl uf_37 :: T13 |
|
23 #105 := uf_37 |
|
24 #106 := (uf_36 #103 uf_37) |
|
25 #107 := (up_32 #106) |
|
26 #108 := (not #107) |
|
27 #109 := (or #107 #108) |
|
28 #110 := (and #104 #109) |
|
29 #111 := (forall (vars (?x12 int)) #110) |
|
30 #295 := (iff #111 #294) |
|
31 #292 := (iff #110 #104) |
|
32 #1 := true |
|
33 #287 := (and #104 true) |
|
34 #290 := (iff #287 #104) |
|
35 #291 := [rewrite]: #290 |
|
36 #288 := (iff #110 #287) |
|
37 #284 := (iff #109 true) |
|
38 #286 := [rewrite]: #284 |
|
39 #289 := [monotonicity #286]: #288 |
|
40 #293 := [trans #289 #291]: #292 |
|
41 #296 := [quant-intro #293]: #295 |
|
42 #283 := [asserted]: #111 |
|
43 #299 := [mp #283 #296]: #294 |
|
44 #363 := [mp~ #299 #321]: #294 |
|
45 #917 := [mp #363 #916]: #912 |
|
46 #418 := (not #912) |
|
47 #504 := (or #418 #113) |
|
48 #419 := [quant-inst]: #504 |
|
49 [unit-resolution #419 #917 #297]: false |
|
50 unsat |