nick8325 / equinox Goto Github PK

View Code? Open in Web Editor NEW

19.0 19.0 4.0 3.41 MB

Paradox model finder and equinox theorem prover for first-order logic.

License: MIT License

Haskell 77.53% OpenEdge ABL 4.26% Shell 0.65% C++ 4.26% C 1.30% Makefile 0.01% TeX 11.99%

equinox's People

Contributors

Stargazers

Watchers

Forkers

jessealama asr carmenchui andreasabel

equinox's Issues

paradox feature request: specify minimum and maximum domain cardinality

When searching for models with paradox, I find that I often want to compare different models of a theory, specifically, models of different cardinalities. As it stands, though, this appears not to be possible with paradox without either (1) modifying the paradox sources, or (2) adding a premise to the theory saying that the domain size is at least N. Both of these are rather awkward; it seems better to me to support a minimum (and perhaps also maximum) domain size as a commandline parameter for paradox, similar to -n and -N for mace4.

Unable to build smellysox

$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory /Users/alama/sources/equinox/minisat/current-base' make[1]:Solver.or' is up to date.
make[1]: Leaving directory /Users/alama/sources/equinox/minisat/current-base' make Prop.or -C minisat/current-base make[1]: Entering directory/Users/alama/sources/equinox/minisat/current-base'
make[1]: Prop.or' is up to date. make[1]: Leaving directory/Users/alama/sources/equinox/minisat/current-base'
make MiniSatWrapper.or -C instantiate
make[1]: Entering directory /Users/alama/sources/equinox/instantiate' make[1]:MiniSatWrapper.or' is up to date.
make[1]: Leaving directory /Users/alama/sources/equinox/instantiate' make MiniSatInstantiateClause.or -C instantiate make[1]: Entering directory/Users/alama/sources/equinox/instantiate'
make[1]: MiniSatInstantiateClause.or' is up to date. make[1]: Leaving directory/Users/alama/sources/equinox/instantiate'
make -C Haskell
make[1]: Entering directory `/Users/alama/sources/equinox/Haskell'
ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded --make SmellySox/Main -o smellysox.exe

on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
[ 2 of 19] Compiling SmellySox.Parser.Lextff ( SmellySox/Parser/Lextff.hs, SmellySox/Parser/Lextff.o )

templates/GenericTemplate.hs:119:22: Not in scope: `alexGetByte'

templates/GenericTemplate.hs:153:8: Not in scope: alexGetByte' make[1]: *** [smellysox.exe] Error 1 make[1]: Leaving directory/Users/alama/sources/equinox/Haskell'
make: *** [mk-haskell] Error 2

Infinox does not build

Using equinox (commit cf20d54) I am unable to build Infinox. Here's a build log:

$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
make[1]: `Solver.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make Prop.or   -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
make[1]: `Prop.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make MiniSatWrapper.or           -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
make[1]: `MiniSatWrapper.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make MiniSatInstantiateClause.or -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
make[1]: `MiniSatInstantiateClause.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make -C Haskell
make[1]: Entering directory `/Users/alama/sources/equinox/Haskell'
ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded --make Paradox/Main.hs -o paradox

on the commandline:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead

Parsek.hs:1:12:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead
ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded -threaded --make Equinox/Main.hs -o equinox

on the commandline:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead

Parsek.hs:1:12:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead
ghc -fglasgow-exts -O2 -static -threaded -main-is Infinox.Main.main --make Infinox.Main -o infinox

on the commandline:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead

Infinox/Timeout.hs:1:12:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead

Infinox/Timeout.hs:36:8:
    Could not find module `System'
    It is a member of the hidden package `haskell98-2.0.0.1'.
    Use -v to see a list of the files searched for.
make[1]: *** [infinox.exe] Error 1
make[1]: Leaving directory `/Users/alama/sources/equinox/Haskell'
make: *** [mk-haskell] Error 2

unable to build with ghc 7.4.2 on mac os x 10.8

Using ecc947c on Mac OS X 10.8, using GHC 7.4.2 coming from a fresh install of the Haskell Platform:

$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
Compiling: Solver.or ( Solver.C )
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make Prop.or   -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
Compiling: Prop.or ( Prop.C )
Prop.C: In function ‘void logBinOp(FILE*, Var, Lit, Lit, char*)’:
Prop.C:29: warning: format not a string literal and no format arguments
Prop.C:29: warning: format not a string literal and no format arguments
Prop.C: In member function ‘Lit PropSolver::mkAnd(Lit, Lit)’:
Prop.C:93: warning: deprecated conversion from string constant to ‘char*’
Prop.C: In member function ‘Lit PropSolver::mkEqu(Lit, Lit)’:
Prop.C:140: warning: deprecated conversion from string constant to ‘char*’
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make MiniSatWrapper.or           -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
Making dependencies ...
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
Compiling: MiniSatWrapper.or ( MiniSatWrapper.C )
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make MiniSatInstantiateClause.or -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
Compiling: MiniSatInstantiateClause.or ( MiniSatInstantiateClause.C )
MiniSatInstantiateClause.C: In member function ‘bool FOClause::instantiate(Solver&, int)’:
MiniSatInstantiateClause.C:239: warning: unused variable ‘ret’
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make -C Haskell
make[1]: Entering directory `/Users/alama/sources/equinox/Haskell'
ghc -fglasgow-exts --make Sat.hs

on the commandline:
    Warning: -fglasgow-exts is deprecated: Use individual extensions instead

Form.hs:32:8:
    Could not find module `Control.Monad.State'
    Perhaps you meant
      Control.Monad.ST (from base)
      Control.Monad.ST.Safe (from base)
      Control.Monad.Fix (from base)
    Use -v to see a list of the files searched for.
make[1]: *** [Sat.o] Error 1
make[1]: Leaving directory `/Users/alama/sources/equinox/Haskell'
make: *** [mk-haskell] Error 2

paradox segfaults on Mac OS X 10.7

Paradox segfaults on Mac OS X 10.7, even with the latest ghc. The difficulty arises when dealing with "non-trivial" problems whose smallest countermodel has size, say, 5 or more. I don't know how to characterize the TPTP problems on which paradox crashes. All I can say is that when theories start to get a little complex, paradox becomes more likely to crash on Mac OS X. Even more strange, with a single theory paradox sometimes crashes and sometimes terminates.

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.4.1
$ paradox theorem36.p
Paradox, version 4.0, 2010-06-29.
+++ PROBLEM: theorem36.p
Reading 'theorem36.p' ... OK
+++ SOLVING: theorem36.p
domain size 1
domain size 2
domain size 3
domain size 4
domain size 5
domain size 6
domain size 7
Segmentation fault: 11
$ paradox theorem36.p 
Paradox, version 4.0, 2010-06-29.
+++ PROBLEM: theorem36.p
Reading 'theorem36.p' ... OK
+++ SOLVING: theorem36.p
domain size 1
domain size 2
domain size 3
domain size 4
domain size 5
domain size 6
domain size 7
+++ RESULT: CounterSatisfiable

I attach the TPTP problem on which paradox exhibits this strange behavior.

% IndCon(x) -> Complete(x)
fof(individual_concepts_are_complete,conjecture,
  (! [X,D] : ((object(X) & point(D)) =>
    (individual_concept_wrt(X,D) => complete_wrt(X,D))))).

fof(tentative,axiom,
  (? [X] : object(X))).

fof(pauls_principle,axiom,
  (! [X] : (property(X) => ~(a_property_negation_of(X,X))))).

fof(theorem36_lemma1,lemma,
  (! [D,X,F,G] : ((point(D) & object(X) & property(F) & property(G)) =>
     (a_property_negation_of(G,F) =>
        (ex1_wrt(F,X,D) | ex1_wrt(G,X,D)))))).

fof(theorem36_lemma2,lemma,
  (! [D,X,F,G] : ((point(D) & object(X) & property(F) & property(G)) =>
     (a_property_negation_of(G,F) => (ex1_wrt(G,X,D) <=> ~ex1_wrt(F,X,D)))))).

fof(theorem36_lemma3,lemma,
  (! [X,F,G,Q,R,S]: ((object(X) & property(F) & property(G) & proposition(Q) & proposition(R) & proposition(S)) =>
     ((plug1(Q,F,X) & a_property_negation_of(G,F) & plug1(R,G,X) & is_a_disjunction_of(S,Q,R)) =>
       ( ( ! [D] : (point(D) =>  true_wrt(S,D))) => (! [W] : (object(W) => (world_wrt(W,d) => true_in_wrt(S,W,d))))))))).

fof(theorem36_lemma4,lemma,
  (! [U,F,G,P,Q,W,X] : ((object(X) & object(U) & property(F) & object(W) & property(G) & proposition(P) & proposition(Q)) =>
     ((a_property_negation_of(G,F) & plug1(P,F,U) & plug1(Q,G,U) & ex1_wrt(o,U,d) & world_wrt(W,d) & ex1_wrt(c,X,d)) =>
       (((true_in_wrt(P,W,d) | true_in_wrt(Q,W,d)) & realizes_in_wrt(U,X,W,d)) =>
              (enc_wrt(X,F,d) | enc_wrt(X,G,d))))))).

%          (! [X,H,R] : ((object(X) & property(H) & proposition(R)) =>
%              ((ex1_wrt(c,X,d) & plug1(R,H,U)) => (true_in_wrt(R,W,D) <=> enc_wrt(X,H,D))))))  =>

fof(sort_realizes_in_wrt,axiom,
 ( ! [U,X,W,D] : ( realizes_in_wrt(U,X,W,D) => (object(U) & object(X) & object(W) & point(D))))).

fof(sort_individual_concept,axiom,
  ( ! [X,D] : (individual_concept_wrt(X,D) => (point(D) & object(X))))).

fof(sort_appears_in_wrt,axiom,
  (! [X,W,D] : (appears_in_wrt(X,W,D) => (point(D) & object(X) & object(W))))).

% Definition of IndividualConcept(x)
fof(def_individual_concept_wrt,axiom,
    (! [X,D] : ((object(X) & point(D)) => (individual_concept_wrt(X,D) <=>
         (ex1_wrt(c,X,D) & (? [W] : (object(W) & world_wrt(W,D) & appears_in_wrt(X,W,D)))))))).

% Definition of AppearanceAt
fof(def_appears_in_wrt,axiom,
  (! [D,X,W] : ((point(D) & object(X) & object(W)) =>
    (appears_in_wrt(X,W,D) <=>  (ex1_wrt(c,X,D) & world_wrt(W,D) &
     (? [U] : (object(U) & ex1_wrt(o,U,D) & realizes_in_wrt(U,X,W,D)))))))).

% Definition of RealizesInAt
fof(def_realizes_in_wrt,axiom,
     (! [D,U,X,W,P] : ((point(D) & object(U) & object(X) & object(W) & proposition(P)) =>
          (realizes_in_wrt(U,X,W,D) <=> (ex1_wrt(o,U,D)  & ex1_wrt(c,X,D) & world_wrt(W,D) &
               (! [F] : ((property(F) =>
                  (plug1(P,F,U) =>
                     (true_in_wrt(P,W,D) <=> enc_wrt(X,F,D))))))))))).

fof(existence_proposition_plug1,axiom,
  (! [X,F] : ((object(X) & property(F))  => (? [P] : (proposition(P) & plug1(P,F,X)))))).

% from principia/includes/propositions.ax
fof(proposition_plug1_truth,axiom,
  (! [X,F,P] : ((object(X) & property(F) & proposition(P)) =>
    (plug1(P,F,X) =>
      (! [D] : (point(D) => (true_wrt(P,D) <=> ex1_wrt(F,X,D)))))))).

% Definition of Complete(x)
fof(def_complete,axiom,
  ( ! [X,D] : ((object(X) & point(D)) =>
    (complete_wrt(X,D)  <=> (! [F,G] : ((property(F) & property(G) & a_property_negation_of(G,F)) =>
       (enc_wrt(X,F,D) | enc_wrt(X,G,D)))))))).

% There is at least one negation of each property.
fof(property_negation,axiom,
  (! [F] : (property(F)  => (? [G] : (property(G) & a_property_negation_of(G,F)))))).

% Axiom for property negation
fof(meaning_postulate_a_property_negation_of,axiom,
   (! [F,G] : ((property(F) & property(G)) =>
      (a_property_negation_of(G,F) <=>
        (! [X,D] : ((object(X) & point(D)) =>
           (ex1_wrt(G,X,D) <=> ~ex1_wrt(F,X,D)))))))).

fof(property_negation_sorting,axiom,
  (! [G,F] : (a_property_negation_of(G,F) => (property(G) & property(F))))).

% Principle from World Theory (Kripke Principle)
fof(necessary_truth_implies_truth_at_every_world,lemma,
  (! [P] : ((proposition(P) =>
    (! [D] : (point(D) => true_wrt(P,D)) =>
      (! [W]: (object(W) => (world_wrt(W,d) => true_in_wrt(P,W,d))))))))).


fof(existence_a_disjunction_of,axiom,
  (! [P,Q] : ((proposition(P) & proposition(Q)) =>
    (? [R] : (proposition(R) & is_a_disjunction_of(R,P,Q)))))).

fof(axiom_is_a_disjunction_of,axiom,
  (! [P,Q,R] : ((proposition(P) & proposition(Q) & proposition(R)) =>
    (is_a_disjunction_of(R,P,Q) <=>
        (! [D] : (point(D) => (true_wrt(R,D) <=> (true_wrt(P,D) | true_wrt(Q,D))))))))).

fof(is_a_disjunction_of_sorting,axiom,
  (! [P,Q,R] : (is_a_disjunction_of(R,P,Q) => (proposition(P) & proposition(Q) & proposition(R))))).

fof(is_a_disjunction_of_distributes,axiom,
  (! [P,Q,R] : ((proposition(P) & proposition(Q) & proposition(R)) =>
    (is_a_disjunction_of(R,P,Q) =>
      (! [W] : (object(W) =>
        (world_wrt(W,d) =>
          (true_in_wrt(R,W,d) <=> (true_in_wrt(P,W,d) | true_in_wrt(Q,W,d)))))))))).
%                             ^ we may need to turn this into a biconditional

% Distinguished Elements.

fof(distinguished_property_e,axiom,property(e)).
fof(being_a_concept_is_being_abstract,axiom,c=a).

fof(distinctness_o_e,axiom,o!=e).
fof(distinctness_a_e,axiom,a!=e).
fof(distinctness_o_a,axiom,o!=a).

% Defined Notions

fof(def_o_wrt,axiom,
  (! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).

fof(def_a_wrt,axiom,
  (! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~(? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).


fof(def_encp_wrt,axiom,
  (! [X,P,D] : ((object(X) & proposition(P) & point(D)) =>
    (encp_wrt(X,P,D) <=> (? [F] : (property(F) & vac(F,P) & enc_wrt(X,F,D))))))).

fof(def_true_in_wrt,axiom,
  (! [P,X,D] : ((proposition(P) & object(X) & point(D)) =>
    (true_in_wrt(P,X,D) <=> encp_wrt(X,P,D))))).

% Sorting Principles

fof(sort_o,axiom,property(o)).
fof(sort_a,axiom,property(a)).

fof(sort_true_in_wrt,axiom,
 (! [P,X,D] : (true_in_wrt(P,X,D) => (proposition(P) & object(X) & point(D))))).



% Distinguished Elements

fof(distinguished_point_d,axiom,point(d)).

% Sorting on Primitive Notions
fof(sort_properties_not_points,axiom,
  (! [X] : (property(X) => ~point(X)))).
fof(sort_properties_not_objects,axiom,
  (! [X] : (property(X) => ~object(X)))).
fof(sort_objects_not_points,axiom,
 (! [X] : (object(X) => ~point(X)))).
%% fof(sort_propositions_not_points_objects_or_properties,axiom,
%%   (! [X] : (proposition(X) => ~(point(X) | object(X) | property(X))))).
 fof(sort_ex1_wrt,axiom,
  (! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & object(X) & point(D))))).
fof(sort_enc_wrt,axiom,
  (! [X,F,D] : (enc_wrt(X,F,D) => (object(X) & property(F) & point(D))))).
fof(sort_true_wrt,axiom,
  (! [P,D] : (true_wrt(P,D) => (proposition(P) & point(D))))).
fof(sort_true_in_wrt,axiom,
  (! [P,W,D] : (true_in_wrt(P,W,D) => (proposition(P) & object(W) & point(D))))).
fof(sort_individual_concept_wrt,axiom,
  (! [X,D] : (individual_concept_wrt(X,D) => (object(X) & point(D))))).

% Logical Axioms

fof(rigidity_of_encoding,axiom,
  (! [X,F] : ((object(X) & property(F)) =>
    ((? [D] : (point(D) & enc_wrt(X,F,D))) =>
      (! [D] : (point(D) => enc_wrt(X,F,D))))))).

Equinox generates <<loops>> when using any command-line option

For example, given the file refl.fof:

fof(refl, conjecture, ! [X] : X = X).

Works:

$ equinox refl.fof
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
+++ PROBLEM: refl.fof
Reading 'refl.fof' ... OK
+++ SOLVING: refl.fof
#elt|#instances
+++ RESULT: Theorem

Fails:

$ equinox --time 10 refl.fof
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
equinox: <<loop>>

Even the --help option fails:

$ equinox --help
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
Usage: equinox <option>* <file>*

<file> should be in TPTP format.

<option> can be any of the following:

equinox: <<loop>>

Tested with GHC 7.10.3 and 8.0.1.

CCing @jonaprieto

Failed assertions in Paradox

Some problems cause assertions to fail in MiniSatInstantiateClause.cc:

bug_clausify.tptp
incomplete4.tptp
incomplete5.tptp

The instantiation code was previously compiled with -DNDEBUG which meant that the failures were ignored.

cannot build minisat on Mac OS X 10.10 and g++

On Mac OS X 10.10 with GCC (that is, not Apple's own compiler, but GNU C++), I'm not able to build equinox:

$ CXX=/sw/lib/gcc4.9/bin/g++-4 make
make Solver.or -C minisat/current-base
make[1]: Entering directory '/Users/alama/sources/equinox/minisat/current-base'
make[1]: 'Solver.or' is up to date.
make[1]: Leaving directory '/Users/alama/sources/equinox/minisat/current-base'
make Prop.or   -C minisat/current-base
make[1]: Entering directory '/Users/alama/sources/equinox/minisat/current-base'
Compiling: Prop.or ( Prop.C )
In file included from Prop.h:23:0,
                 from Prop.C:20:
../mtl/Map.h: In constructor ‘Map<K, D, H, E>::Map(const H&, const E&)’:
../mtl/Map.h:87:41: warning: delegating constructors only available with -std=c++11 or -std=gnu++11
      Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
                                         ^
../mtl/Map.h:87:50: error: mem-initializer for ‘Map<K, D, H, E>::hash’ follows constructor delegation
      Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
                                                  ^
../mtl/Map.h:87:61: error: mem-initializer for ‘Map<K, D, H, E>::equals’ follows constructor delegation
      Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
                                                             ^
Prop.C: In member function ‘Lit PropSolver::mkAnd(Lit, Lit)’:
Prop.C:93:45: warning: deprecated conversion from string constant to ‘char*’ [-Wwrite-strings]
             logBinOp(logfile, v, f, g, " & ");
                                             ^
Prop.C: In member function ‘Lit PropSolver::mkEqu(Lit, Lit)’:
Prop.C:140:46: warning: deprecated conversion from string constant to ‘char*’ [-Wwrite-strings]
             logBinOp(logfile, v, f, g, " == ");
                                              ^
../mtl/template.mk:61: recipe for target 'Prop.or' failed
make[1]: *** [Prop.or] Error 1
make[1]: Leaving directory '/Users/alama/sources/equinox/minisat/current-base'
Makefile:18: recipe for target 'mk-minisat' failed
make: *** [mk-minisat] Error 2

Here, /sw/lib/gcc4.9/bin/g++-4 is GNU G++ coming from the Fink project; it isn't the Apple-supplied C++ compiler.

Error build `FolSat.hs`

[17 of 18] Compiling Equinox.FolSat   ( Equinox/FolSat.hs, Equinox/FolSat.o )

Equinox/FolSat.hs:317:22: error:
    • Could not deduce (Control.Monad.Fail.MonadFail Sat.S)
        arising from a do statement
        with the failable pattern ‘Left subs’
      from the context: (Ord a, Num a, Show a)
        bound by the inferred type of
                   findAllSubs :: (Ord a, Num a, Show a) =>
                                  a -> Sat.S (Either [Map Symbol Con] (Bool, Set Symbol))
        at Equinox/FolSat.hs:(305,12)-(327,42)
    • In a stmt of a 'do' block: Left subs <- findAllSubs (i + 1)
      In the expression:
        do Sat.lift (showOne send (i + 1))
           cs <- sequence [getModelValueValue v | v <- vs]
           let sub = M.fromList (xs `zip` cs)
           Sat.addClause [Sat.neg (v =? c) | (v, c) <- vs `zip` cs, c /= st]
           ....
      In a stmt of a 'do' block:
        if b then
            do Sat.lift (showOne send (i + 1))
               cs <- sequence [getModelValueValue v | v <- vs]
               let sub = ...
               ....
        else
            do if i == 0 then do ... else do ...
    |
317 |                      Left subs <- findAllSubs (i+1)
    |                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
make[1]: *** [Makefile:42: ../equinox] Error 1

Not sure what to do

Regression

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

Paradox and equinox not on system on TPTP?

I wanted to see a paradox model today!

error building minisat with clang

Building equinox/paradox/etc. using the clang C++ compiler on Mac OS X 10.8 results in an error:

$ make
make Solver.or -C minisat/current-base
Compiling: Solver.or ( Solver.C )
clang: warning: argument unused during compilation: '-ffloat-store'
In file included from Solver.C:20:
In file included from ./Solver.h:65:
./VarOrder.h:88:1: warning: 'VarFilter' defined as a struct here but previously declared as a class [-Wmismatched-tags]
struct VarFilter {
^
./VarOrder.h:70:12: note: did you mean struct here?
    friend class VarFilter;
           ^~~~~
           struct
In file included from Solver.C:20:
./Solver.h:265:38: error: use of undeclared identifier 'Clause_new'
                propagate_tmpbin   = Clause_new(dummy);
                                     ^
./Solver.h:266:38: error: use of undeclared identifier 'Clause_new'
                analyze_tmpbin     = Clause_new(dummy);
                                     ^
./Solver.h:268:38: error: use of undeclared identifier 'Clause_new'
                bwdsub_tmpunit     = Clause_new(dummy);
                                     ^
./Solver.h:270:38: error: use of undeclared identifier 'Clause_new'
                propagate_tmpempty = Clause_new(dummy);
                                     ^
Solver.C:89:23: error: use of undeclared identifier 'Clause_new'
        Clause* c   = Clause_new(ps, learnt);
                      ^
Solver.C:879:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
                    else
                    ^
Solver.C:910:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
                    else
                    ^
3 warnings and 5 errors generated.
make[1]: *** [Solver.or] Error 1
make: *** [mk-minisat] Error 2

A solution it to use g++:

CXX=g++ make
[proceeds as expected]