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
+
−)