ところが．．．

HOL Light には Prover9 という頼もしい友がいます．

# #use "Examples/prover9.ml" ;;
val prover9 : string = "prover9"
val prover9_debugging : bool ref = {contents = false}
val prover9_options : string ref =
  {contents =
    "clear(auto_inference).\nclear(auto_denials).\nclear(auto_limits).
\nset(neg_binary_resolution).\nset(binary_resolution).\nset(paramodula
tion).\n"}
val functions :
  term list ->
  term -> term list * term list * 'a -> term list * term list * 'a = <
fun>
...

# time PROVER9 (mk_imp(concl(CONJ(CONJ DIVIDES_LE_STRONG  DIVIDES_MOD)lem),`(mdivides 9 ==> m=1 \/ m=3 \/ m=9)`));;
-------- Proof 1 --------

THEOREM PROVED

------ process 7836 exit (max_proofs) ------
CPU time (user): 0.347
val it : thm =
  |- ((!m n. m divides n ==> 1 <= m /\ m <= n \/ n = 0) /\
      (!m n. ~(m = 0) ==> (m divides n <=> n MOD m = 0))) /\
     ~(9 = 0) /\
     ~(2 = 0) /\
     ~(4 = 0) /\
     ~(5 = 0) /\
     ~(6 = 0) /\
     ~(7 = 0) /\
     ~(8 = 0) /\
     (!m. 1 <= m /\ m <= 9
          ==> m = 1 \/
              m = 2 \/
              m = 3 \/
              m = 4 \/
              m = 5 \/
              m = 6 \/
              m = 7 \/
              m = 8 \/
              m = 9) /\
     ~(9 MOD 2 = 0) /\
     ~(9 MOD 4 = 0) /\
     ~(9 MOD 5 = 0) /\
     ~(9 MOD 6 = 0) /\
     ~(9 MOD 7 = 0) /\
     ~(9 MOD 8 = 0)
     ==> m divides 9
     ==> m = 1 \/ m = 3 \/ m = 9