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

+#2 := false
+decl up_1 :: (-> T1 T2 bool)
+#5 := (:var 0 T2)
+decl uf_3 :: T1
+#11 := uf_3
+#12 := (up_1 uf_3 #5)
+#560 := (pattern #12)
+#57 := (not #12)
+#561 := (forall (vars (?x3 T2)) (:pat #560) #57)
+decl uf_4 :: T2
+#14 := uf_4
+#15 := (up_1 uf_3 uf_4)
+decl uf_2 :: T1
+#7 := uf_2
+#136 := (= uf_2 uf_3)
+#543 := (iff #15 #136)
+#4 := (:var 1 T1)
+#6 := (up_1 #4 #5)
+#553 := (pattern #6)
+#8 := (= #4 uf_2)
+#9 := (iff #6 #8)
+#554 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #553) #9)
+#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
+#557 := (iff #10 #554)
+#555 := (iff #9 #9)
+#556 := [refl]: #555
+#558 := [quant-intro #556]: #557
+#47 := (~ #10 #10)
+#45 := (~ #9 #9)
+#46 := [refl]: #45
+#48 := [nnf-pos #46]: #47
+#33 := [asserted]: #10
+#49 := [mp~ #33 #48]: #10
+#559 := [mp #49 #558]: #554
+#227 := (not #554)
+#185 := (or #227 #543)
+#135 := (= uf_3 uf_2)
+#205 := (iff #15 #135)
+#528 := (or #227 #205)
+#190 := (iff #528 #185)
+#192 := (iff #185 #185)
+#530 := [rewrite]: #192
+#201 := (iff #205 #543)
+#223 := (iff #135 #136)
+#137 := [rewrite]: #223
+#544 := [monotonicity #137]: #201
+#191 := [monotonicity #544]: #190
+#531 := [trans #191 #530]: #190
+#189 := [quant-inst]: #528
+#532 := [mp #189 #531]: #185
+#539 := [unit-resolution #532 #559]: #543
+decl ?x3!0 :: T2
+#50 := ?x3!0
+#51 := (up_1 uf_3 ?x3!0)
+#224 := (iff #51 #136)
+#155 := (or #227 #224)
+#222 := (iff #51 #135)
+#228 := (or #227 #222)
+#229 := (iff #228 #155)
+#545 := (iff #155 #155)
+#547 := [rewrite]: #545
+#215 := (iff #222 #224)
+#226 := [monotonicity #137]: #215
+#208 := [monotonicity #226]: #229
+#202 := [trans #208 #547]: #229
+#225 := [quant-inst]: #228
+#334 := [mp #225 #202]: #155
+#537 := [unit-resolution #334 #559]: #224
+#541 := (not #224)
+#527 := (or #541 #136)
+#63 := (not #15)
+#540 := [hypothesis]: #63
+#68 := (or #15 #51)
+#60 := (forall (vars (?x3 T2)) #57)
+#69 := (or #63 #60)
+#76 := (and #68 #69)
+#70 := (and #69 #68)
+#77 := (iff #70 #76)
+#78 := [rewrite]: #77
+#13 := (exists (vars (?x3 T2)) #12)
+#35 := (not #13)
+#36 := (iff #15 #35)
+#71 := (~ #36 #70)
+#61 := (~ #35 #60)
+#58 := (~ #57 #57)
+#59 := [refl]: #58
+#62 := [nnf-neg #59]: #61
+#54 := (not #35)
+#55 := (~ #54 #51)
+#42 := (~ #13 #51)
+#39 := [sk]: #42
+#56 := [nnf-neg #39]: #55
+#66 := (~ #15 #15)
+#67 := [refl]: #66
+#64 := (~ #63 #63)
+#65 := [refl]: #64
+#72 := [nnf-pos #65 #67 #56 #62]: #71
+#16 := (iff #13 #15)
+#17 := (not #16)
+#37 := (iff #17 #36)
+#38 := [rewrite]: #37
+#34 := [asserted]: #17
+#41 := [mp #34 #38]: #36
+#73 := [mp~ #41 #72]: #70
+#74 := [mp #73 #78]: #76
+#75 := [and-elim #74]: #68
+#526 := [unit-resolution #75 #540]: #51
+#549 := (not #51)
+#550 := (or #541 #549 #136)
+#551 := [def-axiom]: #550
+#233 := [unit-resolution #551 #526]: #527
+#249 := [unit-resolution #233 #537]: #136
+#213 := (not #136)
+#533 := (not #543)
+#250 := (or #533 #213)
+#534 := (or #533 #15 #213)
+#529 := [def-axiom]: #534
+#251 := [unit-resolution #529 #540]: #250
+#237 := [unit-resolution #251 #249 #539]: false
+#252 := [lemma #237]: #15
+#566 := (or #63 #561)
+#567 := (iff #69 #566)
+#564 := (iff #60 #561)
+#562 := (iff #57 #57)
+#563 := [refl]: #562
+#565 := [quant-intro #563]: #564
+#568 := [monotonicity #565]: #567
+#79 := [and-elim #74]: #69
+#569 := [mp #79 #568]: #566
+#535 := [unit-resolution #569 #252]: #561
+#536 := (not #561)
+#538 := (or #536 #63)
+#176 := [quant-inst]: #538
+[unit-resolution #176 #252 #535]: false
+unsat