src/HOL/SMT/Examples/cert/z3_fol_03.proof

+#2 := false
+decl up_1 :: (-> T1 T2 bool)
+#5 := (:var 0 T2)
+decl uf_4 :: T1
+#18 := uf_4
+#19 := (up_1 uf_4 #5)
+#635 := (pattern #19)
+#116 := (not #19)
+#636 := (forall (vars (?x6 T2)) (:pat #635) #116)
+decl uf_3 :: T2
+#14 := uf_3
+#21 := (up_1 uf_4 uf_3)
+decl uf_2 :: T1
+#7 := uf_2
+#195 := (= uf_2 uf_4)
+#602 := (iff #21 #195)
+#4 := (:var 1 T1)
+#6 := (up_1 #4 #5)
+#612 := (pattern #6)
+#8 := (= #4 uf_2)
+#9 := (iff #6 #8)
+#613 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #612) #9)
+#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
+#616 := (iff #10 #613)
+#614 := (iff #9 #9)
+#615 := [refl]: #614
+#617 := [quant-intro #615]: #616
+#56 := (~ #10 #10)
+#54 := (~ #9 #9)
+#55 := [refl]: #54
+#57 := [nnf-pos #55]: #56
+#39 := [asserted]: #10
+#58 := [mp~ #39 #57]: #10
+#618 := [mp #58 #617]: #613
+#286 := (not #613)
+#244 := (or #286 #602)
+#194 := (= uf_4 uf_2)
+#264 := (iff #21 #194)
+#587 := (or #286 #264)
+#249 := (iff #587 #244)
+#251 := (iff #244 #244)
+#589 := [rewrite]: #251
+#260 := (iff #264 #602)
+#282 := (iff #194 #195)
+#196 := [rewrite]: #282
+#603 := [monotonicity #196]: #260
+#250 := [monotonicity #603]: #249
+#590 := [trans #250 #589]: #249
+#248 := [quant-inst]: #587
+#591 := [mp #248 #590]: #244
+#598 := [unit-resolution #591 #618]: #602
+decl ?x6!3 :: T2
+#63 := ?x6!3
+#64 := (up_1 uf_4 ?x6!3)
+#283 := (iff #64 #195)
+#214 := (or #286 #283)
+#281 := (iff #64 #194)
+#287 := (or #286 #281)
+#288 := (iff #287 #214)
+#604 := (iff #214 #214)
+#606 := [rewrite]: #604
+#274 := (iff #281 #283)
+#285 := [monotonicity #196]: #274
+#267 := [monotonicity #285]: #288
+#261 := [trans #267 #606]: #288
+#284 := [quant-inst]: #287
+#393 := [mp #284 #261]: #214
+#596 := [unit-resolution #393 #618]: #283
+#600 := (not #283)
+#586 := (or #600 #195)
+#122 := (not #21)
+#599 := [hypothesis]: #122
+#127 := (or #21 #64)
+#119 := (forall (vars (?x6 T2)) #116)
+#128 := (or #122 #119)
+#135 := (and #127 #128)
+#129 := (and #128 #127)
+#136 := (iff #129 #135)
+#137 := [rewrite]: #136
+#20 := (exists (vars (?x6 T2)) #19)
+#42 := (not #20)
+#43 := (iff #21 #42)
+#130 := (~ #43 #129)
+#120 := (~ #42 #119)
+#117 := (~ #116 #116)
+#118 := [refl]: #117
+#121 := [nnf-neg #118]: #120
+#113 := (not #42)
+#114 := (~ #113 #64)
+#88 := (~ #20 #64)
+#89 := [sk]: #88
+#115 := [nnf-neg #89]: #114
+#125 := (~ #21 #21)
+#126 := [refl]: #125
+#123 := (~ #122 #122)
+#124 := [refl]: #123
+#131 := [nnf-pos #124 #126 #115 #121]: #130
+#22 := (iff #20 #21)
+#23 := (not #22)
+#44 := (iff #23 #43)
+#45 := [rewrite]: #44
+#41 := [asserted]: #23
+#48 := [mp #41 #45]: #43
+#132 := [mp~ #48 #131]: #129
+#133 := [mp #132 #137]: #135
+#134 := [and-elim #133]: #127
+#585 := [unit-resolution #134 #599]: #64
+#608 := (not #64)
+#609 := (or #600 #608 #195)
+#610 := [def-axiom]: #609
+#292 := [unit-resolution #610 #585]: #586
+#308 := [unit-resolution #292 #596]: #195
+#272 := (not #195)
+#592 := (not #602)
+#309 := (or #592 #272)
+#593 := (or #592 #21 #272)
+#588 := [def-axiom]: #593
+#310 := [unit-resolution #588 #599]: #309
+#296 := [unit-resolution #310 #308 #598]: false
+#311 := [lemma #296]: #21
+#641 := (or #122 #636)
+#642 := (iff #128 #641)
+#639 := (iff #119 #636)
+#637 := (iff #116 #116)
+#638 := [refl]: #637
+#640 := [quant-intro #638]: #639
+#643 := [monotonicity #640]: #642
+#138 := [and-elim #133]: #128
+#644 := [mp #138 #643]: #641
+#594 := [unit-resolution #644 #311]: #636
+#595 := (not #636)
+#597 := (or #595 #122)
+#235 := [quant-inst]: #597
+[unit-resolution #235 #311 #594]: false
+unsat