added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML)
(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
)