33010
|
1 |
#2 := false
|
|
2 |
decl up_1 :: (-> T1 T2 bool)
|
|
3 |
#5 := (:var 0 T2)
|
|
4 |
decl uf_4 :: T1
|
|
5 |
#18 := uf_4
|
|
6 |
#19 := (up_1 uf_4 #5)
|
|
7 |
#635 := (pattern #19)
|
|
8 |
#116 := (not #19)
|
|
9 |
#636 := (forall (vars (?x6 T2)) (:pat #635) #116)
|
|
10 |
decl uf_3 :: T2
|
|
11 |
#14 := uf_3
|
|
12 |
#21 := (up_1 uf_4 uf_3)
|
|
13 |
decl uf_2 :: T1
|
|
14 |
#7 := uf_2
|
|
15 |
#195 := (= uf_2 uf_4)
|
|
16 |
#602 := (iff #21 #195)
|
|
17 |
#4 := (:var 1 T1)
|
|
18 |
#6 := (up_1 #4 #5)
|
|
19 |
#612 := (pattern #6)
|
|
20 |
#8 := (= #4 uf_2)
|
|
21 |
#9 := (iff #6 #8)
|
|
22 |
#613 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #612) #9)
|
|
23 |
#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
|
|
24 |
#616 := (iff #10 #613)
|
|
25 |
#614 := (iff #9 #9)
|
|
26 |
#615 := [refl]: #614
|
|
27 |
#617 := [quant-intro #615]: #616
|
|
28 |
#56 := (~ #10 #10)
|
|
29 |
#54 := (~ #9 #9)
|
|
30 |
#55 := [refl]: #54
|
|
31 |
#57 := [nnf-pos #55]: #56
|
|
32 |
#39 := [asserted]: #10
|
|
33 |
#58 := [mp~ #39 #57]: #10
|
|
34 |
#618 := [mp #58 #617]: #613
|
|
35 |
#286 := (not #613)
|
|
36 |
#244 := (or #286 #602)
|
|
37 |
#194 := (= uf_4 uf_2)
|
|
38 |
#264 := (iff #21 #194)
|
|
39 |
#587 := (or #286 #264)
|
|
40 |
#249 := (iff #587 #244)
|
|
41 |
#251 := (iff #244 #244)
|
|
42 |
#589 := [rewrite]: #251
|
|
43 |
#260 := (iff #264 #602)
|
|
44 |
#282 := (iff #194 #195)
|
|
45 |
#196 := [rewrite]: #282
|
|
46 |
#603 := [monotonicity #196]: #260
|
|
47 |
#250 := [monotonicity #603]: #249
|
|
48 |
#590 := [trans #250 #589]: #249
|
|
49 |
#248 := [quant-inst]: #587
|
|
50 |
#591 := [mp #248 #590]: #244
|
|
51 |
#598 := [unit-resolution #591 #618]: #602
|
|
52 |
decl ?x6!3 :: T2
|
|
53 |
#63 := ?x6!3
|
|
54 |
#64 := (up_1 uf_4 ?x6!3)
|
|
55 |
#283 := (iff #64 #195)
|
|
56 |
#214 := (or #286 #283)
|
|
57 |
#281 := (iff #64 #194)
|
|
58 |
#287 := (or #286 #281)
|
|
59 |
#288 := (iff #287 #214)
|
|
60 |
#604 := (iff #214 #214)
|
|
61 |
#606 := [rewrite]: #604
|
|
62 |
#274 := (iff #281 #283)
|
|
63 |
#285 := [monotonicity #196]: #274
|
|
64 |
#267 := [monotonicity #285]: #288
|
|
65 |
#261 := [trans #267 #606]: #288
|
|
66 |
#284 := [quant-inst]: #287
|
|
67 |
#393 := [mp #284 #261]: #214
|
|
68 |
#596 := [unit-resolution #393 #618]: #283
|
|
69 |
#600 := (not #283)
|
|
70 |
#586 := (or #600 #195)
|
|
71 |
#122 := (not #21)
|
|
72 |
#599 := [hypothesis]: #122
|
|
73 |
#127 := (or #21 #64)
|
|
74 |
#119 := (forall (vars (?x6 T2)) #116)
|
|
75 |
#128 := (or #122 #119)
|
|
76 |
#135 := (and #127 #128)
|
|
77 |
#129 := (and #128 #127)
|
|
78 |
#136 := (iff #129 #135)
|
|
79 |
#137 := [rewrite]: #136
|
|
80 |
#20 := (exists (vars (?x6 T2)) #19)
|
|
81 |
#42 := (not #20)
|
|
82 |
#43 := (iff #21 #42)
|
|
83 |
#130 := (~ #43 #129)
|
|
84 |
#120 := (~ #42 #119)
|
|
85 |
#117 := (~ #116 #116)
|
|
86 |
#118 := [refl]: #117
|
|
87 |
#121 := [nnf-neg #118]: #120
|
|
88 |
#113 := (not #42)
|
|
89 |
#114 := (~ #113 #64)
|
|
90 |
#88 := (~ #20 #64)
|
|
91 |
#89 := [sk]: #88
|
|
92 |
#115 := [nnf-neg #89]: #114
|
|
93 |
#125 := (~ #21 #21)
|
|
94 |
#126 := [refl]: #125
|
|
95 |
#123 := (~ #122 #122)
|
|
96 |
#124 := [refl]: #123
|
|
97 |
#131 := [nnf-pos #124 #126 #115 #121]: #130
|
|
98 |
#22 := (iff #20 #21)
|
|
99 |
#23 := (not #22)
|
|
100 |
#44 := (iff #23 #43)
|
|
101 |
#45 := [rewrite]: #44
|
|
102 |
#41 := [asserted]: #23
|
|
103 |
#48 := [mp #41 #45]: #43
|
|
104 |
#132 := [mp~ #48 #131]: #129
|
|
105 |
#133 := [mp #132 #137]: #135
|
|
106 |
#134 := [and-elim #133]: #127
|
|
107 |
#585 := [unit-resolution #134 #599]: #64
|
|
108 |
#608 := (not #64)
|
|
109 |
#609 := (or #600 #608 #195)
|
|
110 |
#610 := [def-axiom]: #609
|
|
111 |
#292 := [unit-resolution #610 #585]: #586
|
|
112 |
#308 := [unit-resolution #292 #596]: #195
|
|
113 |
#272 := (not #195)
|
|
114 |
#592 := (not #602)
|
|
115 |
#309 := (or #592 #272)
|
|
116 |
#593 := (or #592 #21 #272)
|
|
117 |
#588 := [def-axiom]: #593
|
|
118 |
#310 := [unit-resolution #588 #599]: #309
|
|
119 |
#296 := [unit-resolution #310 #308 #598]: false
|
|
120 |
#311 := [lemma #296]: #21
|
|
121 |
#641 := (or #122 #636)
|
|
122 |
#642 := (iff #128 #641)
|
|
123 |
#639 := (iff #119 #636)
|
|
124 |
#637 := (iff #116 #116)
|
|
125 |
#638 := [refl]: #637
|
|
126 |
#640 := [quant-intro #638]: #639
|
|
127 |
#643 := [monotonicity #640]: #642
|
|
128 |
#138 := [and-elim #133]: #128
|
|
129 |
#644 := [mp #138 #643]: #641
|
|
130 |
#594 := [unit-resolution #644 #311]: #636
|
|
131 |
#595 := (not #636)
|
|
132 |
#597 := (or #595 #122)
|
|
133 |
#235 := [quant-inst]: #597
|
|
134 |
[unit-resolution #235 #311 #594]: false
|
|
135 |
unsat
|