Re: [isabelle] Isabelle2013-RC1 Sledge output finicky



The remote provers tend to only work when used in a Sledgehammer command by themselves.

This command finishes after a few seconds with no results from either ATP.

sledgehammer[minimize=smart,preplay_timeout=3,timeout=30,verbose,max_relevant=smart,provers="
  remote_vampire z3_tptp
  "]

This command finishes after a few seconds with a proof.

sledgehammer[minimize=smart,preplay_timeout=3,timeout=30,verbose,max_relevant=smart,provers="
  remote_vampire
  "]

The ATP remote_satallax is predictable in the same exact way. By itself, it returns a proof. With z3_tptp, it doesn't.

In general, the ATPs are only working if they're run by themselves.

They're still very useful.

Regards,
GB





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.