--- a/src/HOL/SMT_Examples/SMT_Tests.certs Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs Tue Mar 27 17:11:02 2012 +0200
@@ -67232,3 +67232,280 @@
unsat
26a6ebeac1bb75693d61408e7c0984072dfbd2df 1 0
unsat
+2f894a623075d62f46fa0487301d3cff02b03b4d 123 0
+#2 := false
+decl f4 :: S2
+#8 := f4
+decl f3 :: S2
+#7 := f3
+#9 := (= f3 f4)
+decl inj!0 :: (-> S3 S2)
+decl f6 :: (-> S2 S3)
+#28 := (f6 f4)
+#179 := (inj!0 #28)
+#265 := (= #179 f4)
+#18 := (:var 0 S2)
+#19 := (f6 #18)
+#112 := (pattern #19)
+#111 := (inj!0 #19)
+#108 := (= #111 #18)
+#594 := (forall (vars (k!0 S2)) (:pat #112) #108)
+#113 := (forall (vars (k!0 S2)) (:pat #112) #108)
+#595 := (iff #113 #594)
+#597 := (iff #594 #594)
+#598 := [rewrite]: #597
+#596 := [rewrite]: #595
+#599 := [trans #596 #598]: #595
+#16 := (:var 1 S2)
+#21 := (= #18 #16)
+#17 := (f6 #16)
+#20 := (= #17 #19)
+#54 := (not #20)
+#55 := (or #54 #21)
+#58 := (forall (vars (?v0 S2) (?v1 S2)) #55)
+#114 := (iff #58 #113)
+#115 := [rewrite]: #114
+#118 := (~ #58 #58)
+#116 := (~ #55 #55)
+#117 := [refl]: #116
+#119 := [nnf-pos #117]: #118
+decl f5 :: S2
+#11 := f5
+#14 := (= f4 f5)
+#15 := (not #14)
+#12 := (= f3 f5)
+#13 := (not #12)
+#10 := (not #9)
+#82 := (and #10 #13 #15 #58)
+#27 := (f6 f3)
+#29 := (= #27 #28)
+#30 := (not #29)
+#85 := (not #82)
+#88 := (or #85 #30)
+#91 := (not #88)
+#22 := (implies #20 #21)
+#23 := (forall (vars (?v0 S2) (?v1 S2)) #22)
+#24 := (and #15 #23)
+#25 := (and #13 #24)
+#26 := (and #10 #25)
+#31 := (implies #26 #30)
+#32 := (not #31)
+#94 := (iff #32 #91)
+#61 := (and #15 #58)
+#64 := (and #13 #61)
+#67 := (and #10 #64)
+#73 := (not #67)
+#74 := (or #73 #30)
+#79 := (not #74)
+#92 := (iff #79 #91)
+#89 := (iff #74 #88)
+#86 := (iff #73 #85)
+#83 := (iff #67 #82)
+#84 := [rewrite]: #83
+#87 := [monotonicity #84]: #86
+#90 := [monotonicity #87]: #89
+#93 := [monotonicity #90]: #92
+#80 := (iff #32 #79)
+#77 := (iff #31 #74)
+#70 := (implies #67 #30)
+#75 := (iff #70 #74)
+#76 := [rewrite]: #75
+#71 := (iff #31 #70)
+#68 := (iff #26 #67)
+#65 := (iff #25 #64)
+#62 := (iff #24 #61)
+#59 := (iff #23 #58)
+#56 := (iff #22 #55)
+#57 := [rewrite]: #56
+#60 := [quant-intro #57]: #59
+#63 := [monotonicity #60]: #62
+#66 := [monotonicity #63]: #65
+#69 := [monotonicity #66]: #68
+#72 := [monotonicity #69]: #71
+#78 := [trans #72 #76]: #77
+#81 := [monotonicity #78]: #80
+#95 := [trans #81 #93]: #94
+#53 := [asserted]: #32
+#96 := [mp #53 #95]: #91
+#97 := [not-or-elim #96]: #82
+#101 := [and-elim #97]: #58
+#110 := [mp~ #101 #119]: #58
+#109 := [mp #110 #115]: #113
+#600 := [mp #109 #599]: #594
+#180 := (not #594)
+#270 := (or #180 #265)
+#267 := [quant-inst #8]: #270
+#250 := [unit-resolution #267 #600]: #265
+#590 := (= f3 #179)
+#178 := (inj!0 #27)
+#256 := (= #178 #179)
+#244 := (= #179 #178)
+#269 := (= #28 #27)
+#102 := [not-or-elim #96]: #29
+#271 := [symm #102]: #269
+#375 := [monotonicity #271]: #244
+#589 := [symm #375]: #256
+#582 := (= f3 #178)
+#264 := (= #178 f3)
+#266 := (or #180 #264)
+#257 := [quant-inst #7]: #266
+#268 := [unit-resolution #257 #600]: #264
+#255 := [symm #268]: #582
+#591 := [trans #255 #589]: #590
+#592 := [trans #591 #250]: #9
+#98 := [and-elim #97]: #10
+[unit-resolution #98 #592]: false
+unsat
+dbb5533c26f60f0a5c965d87e1dfccfd73b06e07 152 0
+#2 := false
+decl f3 :: (-> S2 S3 S4)
+decl f10 :: S3
+#34 := f10
+decl f11 :: S2
+#41 := f11
+#51 := (f3 f11 f10)
+decl f4 :: (-> S5 S4 S2)
+decl f12 :: S4
+#44 := f12
+decl f5 :: (-> S6 S3 S5)
+decl f8 :: S3
+#30 := f8
+decl f6 :: (-> S7 S2 S6)
+decl f7 :: S7
+#7 := f7
+#42 := (f6 f7 f11)
+#43 := (f5 #42 f8)
+#45 := (f4 #43 f12)
+#281 := (f3 #45 f10)
+#282 := (= #281 #51)
+#568 := (= #281 f12)
+#567 := (= f10 f8)
+#565 := (if #567 #568 #282)
+#23 := (:var 0 S3)
+#21 := (:var 1 S4)
+#19 := (:var 2 S3)
+#17 := (:var 3 S2)
+#18 := (f6 f7 #17)
+#20 := (f5 #18 #19)
+#22 := (f4 #20 #21)
+#24 := (f3 #22 #23)
+#611 := (pattern #24)
+#26 := (f3 #17 #23)
+#128 := (= #24 #26)
+#127 := (= #24 #21)
+#25 := (= #23 #19)
+#111 := (if #25 #127 #128)
+#612 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4) (?v3 S3)) (:pat #611) #111)
+#120 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4) (?v3 S3)) #111)
+#615 := (iff #120 #612)
+#613 := (iff #111 #111)
+#614 := [refl]: #613
+#616 := [quant-intro #614]: #615
+#27 := (if #25 #21 #26)
+#28 := (= #24 #27)
+#29 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4) (?v3 S3)) #28)
+#117 := (iff #29 #120)
+#112 := (iff #28 #111)
+#119 := [rewrite]: #112
+#118 := [quant-intro #119]: #117
+#109 := (~ #29 #29)
+#108 := (~ #28 #28)
+#125 := [refl]: #108
+#110 := [nnf-pos #125]: #109
+#76 := [asserted]: #29
+#126 := [mp~ #76 #110]: #29
+#115 := [mp #126 #118]: #120
+#617 := [mp #115 #616]: #612
+#385 := (not #612)
+#570 := (or #385 #565)
+#559 := [quant-inst #41 #30 #44 #34]: #570
+#569 := [unit-resolution #559 #617]: #565
+#561 := (not #567)
+#35 := (= f8 f10)
+#36 := (not #35)
+#546 := (iff #36 #561)
+#551 := (iff #35 #567)
+#566 := (iff #567 #35)
+#550 := [commutativity]: #566
+#552 := [symm #550]: #551
+#547 := [monotonicity #552]: #546
+decl f9 :: S3
+#31 := f9
+#37 := (= f9 f10)
+#38 := (not #37)
+#32 := (= f8 f9)
+#33 := (not #32)
+#85 := (and #33 #36 #38)
+decl f13 :: S4
+#48 := f13
+#46 := (f6 f7 #45)
+#47 := (f5 #46 f9)
+#49 := (f4 #47 f13)
+#50 := (f3 #49 f10)
+#52 := (= #50 #51)
+#88 := (not #85)
+#91 := (or #88 #52)
+#94 := (not #91)
+#39 := (and #36 #38)
+#40 := (and #33 #39)
+#53 := (implies #40 #52)
+#54 := (not #53)
+#97 := (iff #54 #94)
+#78 := (not #40)
+#79 := (or #78 #52)
+#82 := (not #79)
+#95 := (iff #82 #94)
+#92 := (iff #79 #91)
+#89 := (iff #78 #88)
+#86 := (iff #40 #85)
+#87 := [rewrite]: #86
+#90 := [monotonicity #87]: #89
+#93 := [monotonicity #90]: #92
+#96 := [monotonicity #93]: #95
+#83 := (iff #54 #82)
+#80 := (iff #53 #79)
+#81 := [rewrite]: #80
+#84 := [monotonicity #81]: #83
+#98 := [trans #84 #96]: #97
+#77 := [asserted]: #54
+#99 := [mp #77 #98]: #94
+#100 := [not-or-elim #99]: #85
+#102 := [and-elim #100]: #36
+#553 := [mp #102 #547]: #561
+#406 := (not #282)
+#104 := (not #52)
+#388 := (iff #104 #406)
+#428 := (iff #52 #282)
+#545 := (iff #282 #52)
+#544 := (= #281 #50)
+#260 := (= #50 #281)
+#279 := (= #50 f13)
+#278 := (= f10 f9)
+#596 := (if #278 #279 #260)
+#592 := (or #385 #596)
+#265 := [quant-inst #45 #31 #48 #34]: #592
+#554 := [unit-resolution #265 #617]: #596
+#599 := (not #278)
+#387 := (iff #38 #599)
+#384 := (iff #37 #278)
+#548 := (iff #278 #37)
+#555 := [commutativity]: #548
+#386 := [symm #555]: #384
+#540 := [monotonicity #386]: #387
+#103 := [and-elim #100]: #38
+#541 := [mp #103 #540]: #599
+#266 := (not #596)
+#602 := (or #266 #278 #260)
+#597 := [def-axiom]: #602
+#543 := [unit-resolution #597 #541 #554]: #260
+#542 := [symm #543]: #544
+#427 := [monotonicity #542]: #545
+#429 := [symm #427]: #428
+#536 := [monotonicity #429]: #388
+#105 := [not-or-elim #99]: #104
+#438 := [mp #105 #536]: #406
+#560 := (not #565)
+#562 := (or #560 #567 #282)
+#563 := [def-axiom]: #562
+[unit-resolution #563 #438 #553 #569]: false
+unsat