--- a/src/HOL/SMT_Examples/SMT_Examples.certs Wed Nov 24 08:51:48 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Wed Nov 24 10:39:58 2010 +0100
@@ -16193,3 +16193,101 @@
#223 := [asserted]: #31
[unit-resolution #223 #592]: false
unsat
+030f06ff279b2b609c311e25ffea5c845380fd2c 97 0
+#2 := false
+decl f1 :: S1
+#4 := f1
+decl f2 :: S1
+#5 := f2
+#9 := 3::int
+decl f3 :: int
+#8 := f3
+#46 := (>= f3 3::int)
+#51 := (ite #46 f2 f1)
+#73 := (= f1 #51)
+#58 := (ite #46 f1 f2)
+#69 := (= f1 #58)
+#115 := (iff #69 #73)
+#113 := (iff #73 #69)
+#61 := (= #51 #58)
+#12 := (<= 3::int f3)
+#13 := (ite #12 f1 f2)
+#10 := (< f3 3::int)
+#11 := (ite #10 f1 f2)
+#14 := (distinct #11 #13)
+#15 := (not #14)
+#64 := (iff #15 #61)
+#33 := (= #11 #13)
+#62 := (iff #33 #61)
+#59 := (= #13 #58)
+#56 := (iff #12 #46)
+#57 := [rewrite]: #56
+#60 := [monotonicity #57]: #59
+#54 := (= #11 #51)
+#44 := (not #46)
+#48 := (ite #44 f1 f2)
+#52 := (= #48 #51)
+#53 := [rewrite]: #52
+#49 := (= #11 #48)
+#45 := (iff #10 #44)
+#47 := [rewrite]: #45
+#50 := [monotonicity #47]: #49
+#55 := [trans #50 #53]: #54
+#63 := [monotonicity #55 #60]: #62
+#42 := (iff #15 #33)
+#34 := (not #33)
+#37 := (not #34)
+#40 := (iff #37 #33)
+#41 := [rewrite]: #40
+#38 := (iff #15 #37)
+#35 := (iff #14 #34)
+#36 := [rewrite]: #35
+#39 := [monotonicity #36]: #38
+#43 := [trans #39 #41]: #42
+#65 := [trans #43 #63]: #64
+#32 := [asserted]: #15
+#66 := [mp #32 #65]: #61
+#114 := [monotonicity #66]: #113
+#116 := [symm #114]: #115
+#109 := (not #73)
+#6 := (= f1 f2)
+#67 := (= f2 #58)
+#105 := (iff #67 #6)
+#103 := (iff #6 #67)
+#98 := (= #58 f2)
+#101 := (iff #98 #67)
+#102 := [commutativity]: #101
+#99 := (iff #6 #98)
+#96 := [hypothesis]: #73
+#97 := [trans #96 #66]: #69
+#100 := [monotonicity #97]: #99
+#104 := [trans #100 #102]: #103
+#106 := [symm #104]: #105
+#72 := (= f2 #51)
+#84 := (iff #72 #67)
+#85 := [monotonicity #66]: #84
+#80 := (not #67)
+#81 := [hypothesis]: #80
+#78 := (or #46 #67)
+#79 := [def-axiom]: #78
+#82 := [unit-resolution #79 #81]: #46
+#74 := (or #44 #72)
+#75 := [def-axiom]: #74
+#83 := [unit-resolution #75 #82]: #72
+#86 := [mp #83 #85]: #67
+#87 := [unit-resolution #81 #86]: false
+#88 := [lemma #87]: #67
+#107 := [mp #88 #106]: #6
+#7 := (not #6)
+#31 := [asserted]: #7
+#108 := [unit-resolution #31 #107]: false
+#110 := [lemma #108]: #109
+#70 := (or #46 #73)
+#71 := [def-axiom]: #70
+#111 := [unit-resolution #71 #110]: #46
+#76 := (or #44 #69)
+#77 := [def-axiom]: #76
+#112 := [unit-resolution #77 #111]: #69
+#117 := [mp #112 #116]: #73
+[unit-resolution #110 #117]: false
+unsat