--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_pair_01.proof Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,50 @@
+#2 := false
+decl uf_6 :: T2
+#23 := uf_6
+decl uf_4 :: T2
+#19 := uf_4
+#25 := (= uf_4 uf_6)
+decl uf_2 :: (-> T1 T2)
+decl uf_1 :: (-> T2 T3 T1)
+decl uf_5 :: T3
+#20 := uf_5
+#21 := (uf_1 uf_4 uf_5)
+#22 := (uf_2 #21)
+#24 := (= #22 uf_6)
+#65 := [asserted]: #24
+#143 := (= uf_4 #22)
+#11 := (:var 0 T3)
+#10 := (:var 1 T2)
+#12 := (uf_1 #10 #11)
+#567 := (pattern #12)
+#16 := (uf_2 #12)
+#58 := (= #10 #16)
+#574 := (forall (vars (?x4 T2) (?x5 T3)) (:pat #567) #58)
+#62 := (forall (vars (?x4 T2) (?x5 T3)) #58)
+#577 := (iff #62 #574)
+#575 := (iff #58 #58)
+#576 := [refl]: #575
+#578 := [quant-intro #576]: #577
+#71 := (~ #62 #62)
+#87 := (~ #58 #58)
+#88 := [refl]: #87
+#72 := [nnf-pos #88]: #71
+#17 := (= #16 #10)
+#18 := (forall (vars (?x4 T2) (?x5 T3)) #17)
+#63 := (iff #18 #62)
+#60 := (iff #17 #58)
+#61 := [rewrite]: #60
+#64 := [quant-intro #61]: #63
+#57 := [asserted]: #18
+#67 := [mp #57 #64]: #62
+#89 := [mp~ #67 #72]: #62
+#579 := [mp #89 #578]: #574
+#214 := (not #574)
+#551 := (or #214 #143)
+#553 := [quant-inst]: #551
+#233 := [unit-resolution #553 #579]: #143
+#235 := [trans #233 #65]: #25
+#26 := (not #25)
+#66 := [asserted]: #26
+[unit-resolution #66 #235]: false
+unsat