search

nick8325 / equinox

Paradox model finder and equinox theorem prover for first-order logic.
MIT License
20 stars 4 forks source link

Regression #13

Open asr opened 7 years ago

asr commented 7 years ago

Using Equinox version 5.0alpha 2010-06-29 (commit 9151a09, compiled with GHC 6.10.4), the attached problem is proved instantly:

$ time equinox regression.fof 
Equinox, version 5.0alpha, 2010-06-29.
+++ PROBLEM: regression.fof
Reading 'regression.fof' ... OK
+++ SOLVING: regression.fof
#elt|m|#instances
  12|P|....
  12|L|1.>.
  99|P|....
  99|L|.L.1
 190|P|L13.
+++ RESULT: Theorem

real    0m0.150s
user    0m0.142s
sys 0m0.008s

but using the upstream version the same problem is not proved in 10 minutes:

$ equinox --time 600 regression.fof
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
+++ PROBLEM: regression.fof
Reading 'regression.fof' ... OK
+++ SOLVING: regression.fof
...
*** TIMEOUT (600 seconds)
+++ RESULT: Timeout

Actually, I found the same kind of regression (proved in 5.0alpha 2010-06-29, not proved in upstream) in others TPTP problems, but the attached one is the simplest.

regression.fof.txt

asr commented 7 years ago

In this branch, there is a version of Equinox 5.0alpha 2010-06-29 which should compile with recent versions of GHC.

CC'ing @jonaprieto.