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:

e
metis
spass
spass_new
z3_tptp
remote_e_sine
remote_iprover
remote_iprover_eq
remote_leo2
remote_satallax
remote_vampire

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 negated theorem.

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:

http://technet.microsoft.com/en-us/sysinternals/bb896653.aspx

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.

Regards,
GB





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