src/HOL/SMT/Examples/cert/z3_prop_10

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
)