Re: [isabelle] Automating the auto-tools
With a 480 second timeout, these are provers which found the
inconsistency due to the trivial mistake in the axiom:
Of note is that z3_tptp found it but not z3. Note to self: Leave z3_tptp in.
Provers that attempted it:
metis smt dummy_thf e spass spass_new spass_old
z3_tptp cvc3 yices z3 remote_e_sine remote_e_tofof
remote_iprover remote_iprover_eq remote_leo2 remote_satallax
remote_snark remote_vampire remote_waldmeister
Note to self: Put the remote provers in that were successful. They
shouldn't add too much of a burden on my CPU.
With a 480 second timeout, the right axiom in, and me waiting much
longer than 480 seconds, sledgehammer didn't find a proof for the
I ran with a 480 second timeout, with these provers:
e metis spass spass_new z3 z3_tptp remote_e_sine remote_iprover
remote_iprover_eq remote_leo2 remote_satallax remote_vampire
At 480 seconds, e, metis, spass, and spass_new timed out. They had all
been sucking up 25% of my CPU processing. At that point z3 kicked in
using 25% of my CPU until it got an error after 2 minutes. Sledgehammer
was still running, so I figured it was waiting on the remote provers to
signal that they had timed out after 480 seconds of processing, which,
it appears, was going to be spread out over however many minutes it
would take for me to get my 480 seconds of processing, the remote
servers also trying to prove theorems for the rest of the world, trying
in vain, at least for the negation of mine, I hope.
And those prover processes don't terminate very well. You have to help
them out, and kill them sometimes. For Windows, it helps to have the
process explorer utility:
However, killing them seems to cause problems, so I think it's best to
let them terminate normally.
I learned something important here. Every prover's going to get its 480
seconds to try and do something.
But every time I do a keystroke in a file that the tester file is
importing, the continuous prover starts over, so I need to change my
script to accommodate for that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and