leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
BSD 3-Clause "New" or "Revised" License
42 stars 10 forks source link

problem causes LEO to hang #74

Open apease opened 1 year ago

apease commented 1 year ago

Chad Brown semi-automatically created some problems based on SUMO. One appears to hang LEO-III. It could just be a problem on our end, but similar such problems either succeed or timeout so I thought I'd send it along. I'm still new to THF so apologies if I've messed up, but it seems like LEO-III should at least time out. I've attached the output from the problem (.txt), the process info below and the problem (zipped .p) file.

p$ ps -aux | grep leo apease 65942 103 1.3 3945964 884668 pts/1 Sl+ 08:54 193:26 /home/apease/Programs/java/jdk1.8.0_111/bin/java -Xss32m -Xmx1g -jar /home/apease/workspace/Leo-III/Leo-III-1.6/bin/leo3 TQG20bushytop.9076.th0.p -t 600 -p

It should have timed out in 10 minutes but is still running three hours later.

TQG20bushytop.9076.th0.p.txt TQG20bushytop.9076.th0.zip