Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT/Examples/cert/z3_prop_10
changeset 33010 39f73a59e855 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_prop_10	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,251 @@
+(benchmark Isabelle
+:extrasorts ( T1)
+:extrapreds (
+  (up_1)
+  (up_5)
+  (up_7)
+  (up_9)
+  (up_11)
+  (up_14)
+  (up_16)
+  (up_18)
+  (up_20)
+  (up_22)
+  (up_25)
+  (up_27)
+  (up_29)
+  (up_31)
+  (up_33)
+  (up_36)
+  (up_38)
+  (up_40)
+  (up_42)
+  (up_44)
+  (up_47)
+  (up_49)
+  (up_51)
+  (up_53)
+  (up_55)
+  (up_57)
+  (up_58)
+  (up_59)
+  (up_60)
+  (up_3)
+  (up_2)
+  (up_6)
+  (up_8)
+  (up_10)
+  (up_12)
+  (up_13)
+  (up_15)
+  (up_17)
+  (up_19)
+  (up_21)
+  (up_23)
+  (up_24)
+  (up_26)
+  (up_28)
+  (up_30)
+  (up_32)
+  (up_34)
+  (up_35)
+  (up_37)
+  (up_39)
+  (up_41)
+  (up_43)
+  (up_45)
+  (up_46)
+  (up_48)
+  (up_50)
+  (up_52)
+  (up_54)
+  (up_56)
+  (up_4)
+ )
+:assumption (not up_1)
+:assumption (not up_2)
+:assumption (not up_3)
+:assumption (not up_4)
+:assumption (or up_5 (or up_6 up_1))
+:assumption (or up_7 (or up_8 up_5))
+:assumption (or up_9 (or up_10 up_7))
+:assumption (or up_11 (or up_12 up_9))
+:assumption (or up_13 up_11)
+:assumption (or up_14 (or up_15 up_2))
+:assumption (or up_16 (or up_17 (or up_14 up_6)))
+:assumption (or up_18 (or up_19 (or up_16 up_8)))
+:assumption (or up_20 (or up_21 (or up_18 up_10)))
+:assumption (or up_22 (or up_23 (or up_20 up_12)))
+:assumption (or up_24 (or up_22 up_13))
+:assumption (or up_25 (or up_26 up_15))
+:assumption (or up_27 (or up_28 (or up_25 up_17)))
+:assumption (or up_29 (or up_30 (or up_27 up_19)))
+:assumption (or up_31 (or up_32 (or up_29 up_21)))
+:assumption (or up_33 (or up_34 (or up_31 up_23)))
+:assumption (or up_35 (or up_33 up_24))
+:assumption (or up_36 (or up_37 up_26))
+:assumption (or up_38 (or up_39 (or up_36 up_28)))
+:assumption (or up_40 (or up_41 (or up_38 up_30)))
+:assumption (or up_42 (or up_43 (or up_40 up_32)))
+:assumption (or up_44 (or up_45 (or up_42 up_34)))
+:assumption (or up_46 (or up_44 up_35))
+:assumption (or up_47 (or up_48 up_37))
+:assumption (or up_49 (or up_50 (or up_47 up_39)))
+:assumption (or up_51 (or up_52 (or up_49 up_41)))
+:assumption (or up_53 (or up_54 (or up_51 up_43)))
+:assumption (or up_55 (or up_56 (or up_53 up_45)))
+:assumption (or up_4 (or up_55 up_46))
+:assumption (or up_57 up_48)
+:assumption (or up_58 (or up_57 up_50))
+:assumption (or up_59 (or up_58 up_52))
+:assumption (or up_60 (or up_59 up_54))
+:assumption (or up_3 (or up_60 up_56))
+:assumption (or (not up_5) (not up_6))
+:assumption (or (not up_5) (not up_1))
+:assumption (or (not up_6) (not up_1))
+:assumption (or (not up_7) (not up_8))
+:assumption (or (not up_7) (not up_5))
+:assumption (or (not up_8) (not up_5))
+:assumption (or (not up_9) (not up_10))
+:assumption (or (not up_9) (not up_7))
+:assumption (or (not up_10) (not up_7))
+:assumption (or (not up_11) (not up_12))
+:assumption (or (not up_11) (not up_9))
+:assumption (or (not up_12) (not up_9))
+:assumption (or (not up_13) (not up_11))
+:assumption (or (not up_14) (not up_15))
+:assumption (or (not up_14) (not up_2))
+:assumption (or (not up_15) (not up_2))
+:assumption (or (not up_16) (not up_17))
+:assumption (or (not up_16) (not up_14))
+:assumption (or (not up_16) (not up_6))
+:assumption (or (not up_17) (not up_14))
+:assumption (or (not up_17) (not up_6))
+:assumption (or (not up_14) (not up_6))
+:assumption (or (not up_18) (not up_19))
+:assumption (or (not up_18) (not up_16))
+:assumption (or (not up_18) (not up_8))
+:assumption (or (not up_19) (not up_16))
+:assumption (or (not up_19) (not up_8))
+:assumption (or (not up_16) (not up_8))
+:assumption (or (not up_20) (not up_21))
+:assumption (or (not up_20) (not up_18))
+:assumption (or (not up_20) (not up_10))
+:assumption (or (not up_21) (not up_18))
+:assumption (or (not up_21) (not up_10))
+:assumption (or (not up_18) (not up_10))
+:assumption (or (not up_22) (not up_23))
+:assumption (or (not up_22) (not up_20))
+:assumption (or (not up_22) (not up_12))
+:assumption (or (not up_23) (not up_20))
+:assumption (or (not up_23) (not up_12))
+:assumption (or (not up_20) (not up_12))
+:assumption (or (not up_24) (not up_22))
+:assumption (or (not up_24) (not up_13))
+:assumption (or (not up_22) (not up_13))
+:assumption (or (not up_25) (not up_26))
+:assumption (or (not up_25) (not up_15))
+:assumption (or (not up_26) (not up_15))
+:assumption (or (not up_27) (not up_28))
+:assumption (or (not up_27) (not up_25))
+:assumption (or (not up_27) (not up_17))
+:assumption (or (not up_28) (not up_25))
+:assumption (or (not up_28) (not up_17))
+:assumption (or (not up_25) (not up_17))
+:assumption (or (not up_29) (not up_30))
+:assumption (or (not up_29) (not up_27))
+:assumption (or (not up_29) (not up_19))
+:assumption (or (not up_30) (not up_27))
+:assumption (or (not up_30) (not up_19))
+:assumption (or (not up_27) (not up_19))
+:assumption (or (not up_31) (not up_32))
+:assumption (or (not up_31) (not up_29))
+:assumption (or (not up_31) (not up_21))
+:assumption (or (not up_32) (not up_29))
+:assumption (or (not up_32) (not up_21))
+:assumption (or (not up_29) (not up_21))
+:assumption (or (not up_33) (not up_34))
+:assumption (or (not up_33) (not up_31))
+:assumption (or (not up_33) (not up_23))
+:assumption (or (not up_34) (not up_31))
+:assumption (or (not up_34) (not up_23))
+:assumption (or (not up_31) (not up_23))
+:assumption (or (not up_35) (not up_33))
+:assumption (or (not up_35) (not up_24))
+:assumption (or (not up_33) (not up_24))
+:assumption (or (not up_36) (not up_37))
+:assumption (or (not up_36) (not up_26))
+:assumption (or (not up_37) (not up_26))
+:assumption (or (not up_38) (not up_39))
+:assumption (or (not up_38) (not up_36))
+:assumption (or (not up_38) (not up_28))
+:assumption (or (not up_39) (not up_36))
+:assumption (or (not up_39) (not up_28))
+:assumption (or (not up_36) (not up_28))
+:assumption (or (not up_40) (not up_41))
+:assumption (or (not up_40) (not up_38))
+:assumption (or (not up_40) (not up_30))
+:assumption (or (not up_41) (not up_38))
+:assumption (or (not up_41) (not up_30))
+:assumption (or (not up_38) (not up_30))
+:assumption (or (not up_42) (not up_43))
+:assumption (or (not up_42) (not up_40))
+:assumption (or (not up_42) (not up_32))
+:assumption (or (not up_43) (not up_40))
+:assumption (or (not up_43) (not up_32))
+:assumption (or (not up_40) (not up_32))
+:assumption (or (not up_44) (not up_45))
+:assumption (or (not up_44) (not up_42))
+:assumption (or (not up_44) (not up_34))
+:assumption (or (not up_45) (not up_42))
+:assumption (or (not up_45) (not up_34))
+:assumption (or (not up_42) (not up_34))
+:assumption (or (not up_46) (not up_44))
+:assumption (or (not up_46) (not up_35))
+:assumption (or (not up_44) (not up_35))
+:assumption (or (not up_47) (not up_48))
+:assumption (or (not up_47) (not up_37))
+:assumption (or (not up_48) (not up_37))
+:assumption (or (not up_49) (not up_50))
+:assumption (or (not up_49) (not up_47))
+:assumption (or (not up_49) (not up_39))
+:assumption (or (not up_50) (not up_47))
+:assumption (or (not up_50) (not up_39))
+:assumption (or (not up_47) (not up_39))
+:assumption (or (not up_51) (not up_52))
+:assumption (or (not up_51) (not up_49))
+:assumption (or (not up_51) (not up_41))
+:assumption (or (not up_52) (not up_49))
+:assumption (or (not up_52) (not up_41))
+:assumption (or (not up_49) (not up_41))
+:assumption (or (not up_53) (not up_54))
+:assumption (or (not up_53) (not up_51))
+:assumption (or (not up_53) (not up_43))
+:assumption (or (not up_54) (not up_51))
+:assumption (or (not up_54) (not up_43))
+:assumption (or (not up_51) (not up_43))
+:assumption (or (not up_55) (not up_56))
+:assumption (or (not up_55) (not up_53))
+:assumption (or (not up_55) (not up_45))
+:assumption (or (not up_56) (not up_53))
+:assumption (or (not up_56) (not up_45))
+:assumption (or (not up_53) (not up_45))
+:assumption (or (not up_4) (not up_55))
+:assumption (or (not up_4) (not up_46))
+:assumption (or (not up_55) (not up_46))
+:assumption (or (not up_57) (not up_48))
+:assumption (or (not up_58) (not up_57))
+:assumption (or (not up_58) (not up_50))
+:assumption (or (not up_57) (not up_50))
+:assumption (or (not up_59) (not up_58))
+:assumption (or (not up_59) (not up_52))
+:assumption (or (not up_58) (not up_52))
+:assumption (or (not up_60) (not up_59))
+:assumption (or (not up_60) (not up_54))
+:assumption (or (not up_59) (not up_54))
+:assumption (or (not up_3) (not up_60))
+:assumption (or (not up_3) (not up_56))
+:assumption (or (not up_60) (not up_56))
+:assumption (not false)
+:formula true
+)
isabelle