summaryrefslogtreecommitdiff
path: root/academic/ladr
diff options
context:
space:
mode:
Diffstat (limited to 'academic/ladr')
-rw-r--r--academic/ladr/ladr-libtoolize.diff161
-rw-r--r--academic/ladr/ladr.SlackBuild19
-rw-r--r--academic/ladr/ladr.info12
-rw-r--r--academic/ladr/slack-desc4
4 files changed, 113 insertions, 83 deletions
diff --git a/academic/ladr/ladr-libtoolize.diff b/academic/ladr/ladr-libtoolize.diff
index 9eddee96d9..015de6d830 100644
--- a/academic/ladr/ladr-libtoolize.diff
+++ b/academic/ladr/ladr-libtoolize.diff
@@ -1,6 +1,6 @@
-diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/Makefile LADR-2008-09A/Makefile
---- LADR-2008-09A-orig/Makefile 2007-10-22 23:33:12.000000000 +0200
-+++ LADR-2008-09A/Makefile 2008-10-19 15:55:32.270034513 +0200
+diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/Makefile LADR-2009-11A/Makefile
+--- LADR-2009-11A.orig/Makefile 2007-10-22 23:33:12.000000000 +0200
++++ LADR-2009-11A/Makefile 2009-12-26 13:50:32.285406118 +0100
@@ -2,7 +2,7 @@
@echo See README.make
@@ -19,9 +19,9 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/Makefile LADR-2008-09A/Make
test1:
bin/prover9 -f prover9.examples/x2.in | bin/prooftrans parents_only
-diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008-09A/apps.src/Makefile
---- LADR-2008-09A-orig/apps.src/Makefile 2008-07-10 00:45:29.000000000 +0200
-+++ LADR-2008-09A/apps.src/Makefile 2008-10-19 15:55:32.330034747 +0200
+diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/apps.src/Makefile LADR-2009-11A/apps.src/Makefile
+--- LADR-2009-11A.orig/apps.src/Makefile 2009-04-17 16:46:39.000000000 +0200
++++ LADR-2009-11A/apps.src/Makefile 2009-12-26 13:50:32.335405804 +0100
@@ -16,16 +16,16 @@
all: ladr apps install realclean
@@ -43,7 +43,7 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008
tags:
etags *.c ../ladr/*.c
-@@ -33,73 +33,73 @@
+@@ -33,85 +33,85 @@
apps: $(PROGRAMS)
test: test.o
@@ -66,6 +66,14 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008
- $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.la
+ test_complex: test_complex.o
+- $(CC) $(CFLAGS) -o test_complex test_complex.o ../ladr/libladr.a
++ libtool --mode=link $(CC) $(CFLAGS) -o test_complex test_complex.o ../ladr/libladr.la
+
+ complex: complex.o
+- $(CC) $(CFLAGS) -o complex complex.o ../ladr/libladr.a
++ libtool --mode=link $(CC) $(CFLAGS) -o complex complex.o ../ladr/libladr.la
+
latfilter: latfilter.o
- $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.la
@@ -138,11 +146,19 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/apps.src/Makefile LADR-2008
- $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.la
+ rewriter2: rewriter2.o
+- $(CC) $(CFLAGS) -o rewriter2 rewriter2.o ../ladr/libladr.a
++ libtool --mode=link $(CC) $(CFLAGS) -o rewriter2 rewriter2.o ../ladr/libladr.la
+
+ gen_trc_defs: gen_trc_defs.o
+- $(CC) $(CFLAGS) -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.a
++ libtool --mode=link $(CC) $(CFLAGS) -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.la
+
-diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A/ladr/Makefile
---- LADR-2008-09A-orig/ladr/Makefile 2008-08-15 02:11:36.000000000 +0200
-+++ LADR-2008-09A/ladr/Makefile 2008-10-19 15:55:32.435034921 +0200
+diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/ladr/Makefile LADR-2009-11A/ladr/Makefile
+--- LADR-2009-11A.orig/ladr/Makefile 2009-10-28 15:22:04.000000000 +0100
++++ LADR-2009-11A/ladr/Makefile 2009-12-26 13:50:32.453408456 +0100
@@ -11,46 +11,49 @@
# CFLAGS = $(XFLAGS) -pg -O -Wall
# CFLAGS = $(XFLAGS) -Wall -pedantic
@@ -160,8 +176,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
- pindex.o compress.o\
- maximal.o lindex.o weight.o weight2.o\
- int_code.o features.o di_tree.o fastparse.o\
-- random.o subsume.o clause_misc.o clause_eval.o
--INFE_OBJ = flatdemod.o demod.o clash.o resolve.o paramod.o\
+- random.o subsume.o clause_misc.o clause_eval.o complex.o
+-INFE_OBJ = dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o\
- backdemod.o\
- hints.o ac_redun.o xproofs.o ivy.o
-MODL_OBJ = interp.o
@@ -179,8 +195,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
+ pindex.lo compress.lo\
+ maximal.lo lindex.lo weight.lo weight2.lo\
+ int_code.lo features.lo di_tree.lo fastparse.lo\
-+ random.lo subsume.lo clause_misc.lo clause_eval.lo
-+INFE_OBJ = flatdemod.lo demod.lo clash.lo resolve.lo paramod.lo\
++ random.lo subsume.lo clause_misc.lo clause_eval.lo complex.lo
++INFE_OBJ = dollar.lo flatdemod.lo demod.lo clash.lo resolve.lo paramod.lo\
+ backdemod.lo\
+ hints.lo ac_redun.lo xproofs.lo ivy.lo
+MODL_OBJ = interp.lo
@@ -217,7 +233,7 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
protos:
util/make_protos $(OBJECTS)
-@@ -67,150 +70,150 @@
+@@ -67,156 +70,156 @@
# The rest of the file is generated automatically by util/make_dep
@@ -287,47 +303,47 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
-accanon.o: accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+accanon.lo: accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
--unify.o: unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+unify.lo: unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-unify.o: unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++unify.lo: unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-fpalist.o: fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+fpalist.lo: fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--fpa.o: fpa.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+fpa.lo: fpa.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-fpa.o: fpa.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++fpa.lo: fpa.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--discrim.o: discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+discrim.lo: discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-discrim.o: discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++discrim.lo: discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--discrimb.o: discrimb.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+discrimb.lo: discrimb.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-discrimb.o: discrimb.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++discrimb.lo: discrimb.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--discrimw.o: discrimw.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+discrimw.lo: discrimw.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-discrimw.o: discrimw.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++discrimw.lo: discrimw.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-dioph.o: dioph.h
+dioph.lo: dioph.h
--btu.o: btu.h dioph.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+btu.lo: btu.h dioph.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-btu.o: btu.h dioph.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++btu.lo: btu.h dioph.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--btm.o: btm.h unify.h accanon.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termflag.h termorder.h flatterm.h
-+btm.lo: btm.h unify.h accanon.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termflag.h termorder.h flatterm.h
+-btm.o: btm.h unify.h accanon.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termorder.h flatterm.h
++btm.lo: btm.h unify.h accanon.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termorder.h flatterm.h
--mindex.o: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
-+mindex.lo: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+-mindex.o: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
++mindex.lo: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
-basic.o: basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+basic.lo: basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--attrib.o: attrib.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-+attrib.lo: attrib.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+-attrib.o: attrib.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++attrib.lo: attrib.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
--formula.o: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-+formula.lo: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+-formula.o: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++formula.lo: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
--definitions.o: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h termflag.h parse.h
-+definitions.lo: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h termflag.h parse.h
+-definitions.o: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h parse.h
++definitions.lo: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h parse.h
-literals.o: literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+literals.lo: literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
@@ -347,8 +363,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
-just.o: just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+just.lo: just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
--cnf.o: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-+cnf.lo: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+-cnf.o: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++cnf.lo: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-clausify.o: clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h
+clausify.lo: clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h
@@ -365,12 +381,15 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
-maximal.o: maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+maximal.lo: maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
--lindex.o: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
-+lindex.lo: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
+-lindex.o: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
++lindex.lo: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
-weight.o: weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h
+weight.lo: weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h
+-weight2.o: weight2.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++weight2.lo: weight2.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+
-int_code.o: int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+int_code.lo: int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
@@ -386,8 +405,8 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
-random.o: random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+random.lo: random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
--subsume.o: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
-+subsume.lo: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
+-subsume.o: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
++subsume.lo: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
-clause_misc.o: clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h
+clause_misc.lo: clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h
@@ -395,26 +414,32 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
-clause_eval.o: clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+clause_eval.lo: clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
--flatdemod.o: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
-+flatdemod.lo: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+-complex.o: complex.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++complex.lo: complex.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+
+-dollar.o: dollar.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++dollar.lo: dollar.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+
+-flatdemod.o: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
++flatdemod.lo: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
--demod.o: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
-+demod.lo: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+-demod.o: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
++demod.lo: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
--clash.o: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
-+clash.lo: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+-clash.o: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
++clash.lo: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
--resolve.o: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
-+resolve.lo: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
+-resolve.o: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
++resolve.lo: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
--paramod.o: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
-+paramod.lo: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
+-paramod.o: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
++paramod.lo: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
--backdemod.o: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
-+backdemod.lo: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
+-backdemod.o: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
++backdemod.lo: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
--hints.o: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
-+hints.lo: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
+-hints.o: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
++hints.lo: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
-ac_redun.o: ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ac_redun.lo: ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
@@ -442,10 +467,10 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/ladr/Makefile LADR-2008-09A
-top_input.o: top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h
+top_input.lo: top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h
-diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/mace4.src/Makefile LADR-2008-09A/mace4.src/Makefile
---- LADR-2008-09A-orig/mace4.src/Makefile 2008-07-10 00:38:20.000000000 +0200
-+++ LADR-2008-09A/mace4.src/Makefile 2008-10-19 15:55:32.376034420 +0200
-@@ -25,11 +25,11 @@
+diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/mace4.src/Makefile LADR-2009-11A/mace4.src/Makefile
+--- LADR-2009-11A.orig/mace4.src/Makefile 2009-04-17 16:46:46.000000000 +0200
++++ LADR-2009-11A/mace4.src/Makefile 2009-12-26 13:50:32.373406096 +0100
+@@ -26,11 +26,11 @@
$(MAKE) libmace4.a
ladr:
@@ -459,7 +484,7 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/mace4.src/Makefile LADR-200
$(OBJECTS): estack.h syms.h ground.h propagate.h mstate.h msearch.h
-@@ -37,10 +37,10 @@
+@@ -38,10 +38,10 @@
etags *.c ../ladr/*.c
clean:
@@ -473,9 +498,9 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/mace4.src/Makefile LADR-200
install:
- /bin/mv mace4 ../bin
+ libtool --mode=install /bin/cp mace4 `pwd`/../bin
-diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/provers.src/Makefile LADR-2008-09A/provers.src/Makefile
---- LADR-2008-09A-orig/provers.src/Makefile 2008-08-18 21:12:56.000000000 +0200
-+++ LADR-2008-09A/provers.src/Makefile 2008-10-19 15:55:32.434034496 +0200
+diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/provers.src/Makefile LADR-2009-11A/provers.src/Makefile
+--- LADR-2009-11A.orig/provers.src/Makefile 2009-10-28 15:22:15.000000000 +0100
++++ LADR-2009-11A/provers.src/Makefile 2009-12-26 13:50:32.420530288 +0100
@@ -41,13 +41,13 @@
$(MAKE) clean
@@ -538,9 +563,9 @@ diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/provers.src/Makefile LADR-2
prover9.o mprover.o iterate4.o autosketches4.o fof-prover9.o: search.h utilities.h forward_subsume.h giv_select.h white_black.h demodulate.h actions.h index_lits.h pred_elim.h unfold.h provers.h
-diff -U 3 -H -b -w -B -d -r -N -- LADR-2008-09A-orig/test.src/Makefile LADR-2008-09A/test.src/Makefile
---- LADR-2008-09A-orig/test.src/Makefile 2007-03-06 21:27:59.000000000 +0100
-+++ LADR-2008-09A/test.src/Makefile 2008-10-19 15:55:32.425034393 +0200
+diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/test.src/Makefile LADR-2009-11A/test.src/Makefile
+--- LADR-2009-11A.orig/test.src/Makefile 2007-03-06 21:27:59.000000000 +0100
++++ LADR-2009-11A/test.src/Makefile 2009-12-26 13:50:32.416531165 +0100
@@ -17,13 +17,13 @@
ladr:
diff --git a/academic/ladr/ladr.SlackBuild b/academic/ladr/ladr.SlackBuild
index 2b88462210..352f01c14d 100644
--- a/academic/ladr/ladr.SlackBuild
+++ b/academic/ladr/ladr.SlackBuild
@@ -2,7 +2,7 @@
# Slackware build script for ladr
-# Copyright 2007-2008 Heinz Wiesinger <pprkut@liwjatan.at>
+# Copyright 2007-2010 Heinz Wiesinger, Amsterdam, The Netherlands
# All rights reserved.
#
# Redistribution and use of this script, with or without modification, is
@@ -23,7 +23,7 @@
# ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
PRGNAM=ladr
-VERSION=2008_09A
+VERSION=2009_11A
ARCH=${ARCH:-i486}
BUILD=${BUILD:-1}
TAG=${TAG:-_SBo}
@@ -38,10 +38,13 @@ SRC_VERSION=$(echo $VERSION | tr _ -)
if [ "$ARCH" = "i486" ]; then
SLKCFLAGS="-O2 -march=i486 -mtune=i686"
+ LIBDIRSUFFIX=""
elif [ "$ARCH" = "i686" ]; then
SLKCFLAGS="-O2 -march=i686 -mtune=i686"
+ LIBDIRSUFFIX=""
elif [ "$ARCH" = "x86_64" ]; then
SLKCFLAGS="-O2 -fPIC"
+ LIBDIRSUFFIX="64"
fi
set -e
@@ -65,12 +68,12 @@ patch -p1 -i $CWD/ladr-libtoolize.diff
XFLAGS="$SLKCFLAGS" make all MAKEFLAGS="-j1"
-mkdir -p $PKG/usr/{bin,lib}
+mkdir -p $PKG/usr/{bin,lib$LIBDIRSUFFIX}
install -m 0755 ./bin/* $PKG/usr/bin/
-install -m 0755 ./ladr/libladr.la $PKG/usr/lib/
-install -m 0755 ./ladr/.libs/libladr.so.4.0.0 $PKG/usr/lib/
-ln -s /usr/lib/libladr.so.4.0.0 $PKG/usr/lib/libladr.so.4
-ln -s /usr/lib/libladr.so.4.0.0 $PKG/usr/lib/libladr.so
+install -m 0755 ./ladr/libladr.la $PKG/usr/lib$LIBDIRSUFFIX/
+install -m 0755 ./ladr/.libs/libladr.so.4.0.0 $PKG/usr/lib$LIBDIRSUFFIX/
+ln -s /usr/lib$LIBDIRSUFFIX/libladr.so.4.0.0 $PKG/usr/lib$LIBDIRSUFFIX/libladr.so.4
+ln -s /usr/lib$LIBDIRSUFFIX/libladr.so.4.0.0 $PKG/usr/lib$LIBDIRSUFFIX/libladr.so
rm -f $PKG/usr/bin/proof3fo.xsl
chmod 755 $PKG/usr/bin/gvizify
@@ -94,4 +97,4 @@ mkdir -p $PKG/install
cat $CWD/slack-desc > $PKG/install/slack-desc
cd $PKG
-/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.tgz
+/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.${PKGTYPE:-tgz}
diff --git a/academic/ladr/ladr.info b/academic/ladr/ladr.info
index 8c7a1ae4cd..e3b7be7be0 100644
--- a/academic/ladr/ladr.info
+++ b/academic/ladr/ladr.info
@@ -1,8 +1,10 @@
PRGNAM="ladr"
-VERSION="2008_09A"
+VERSION="2009_11A"
HOMEPAGE="http://www.cs.unm.edu/~mccune/prover9/"
-DOWNLOAD="http://www.cs.unm.edu/~mccune/prover9/download/LADR-2008-09A.tar.gz"
-MD5SUM="96cc67eae8f485c22d01449fd2639dae"
-MAINTAINER="ppr:kut"
+DOWNLOAD="http://www.cs.unm.edu/~mccune/prover9/download/LADR-2009-11A.tar.gz"
+MD5SUM="ab409f31ecbb4410b1c7d75deadea2c6"
+DOWNLOAD_x86_64=""
+MD5SUM_x86_64=""
+MAINTAINER="Heinz Wiesinger"
EMAIL="pprkut@liwjatan.at"
-APPROVED="Michiel"
+APPROVED="Erik Hanson"
diff --git a/academic/ladr/slack-desc b/academic/ladr/slack-desc
index 0e9a2a4d73..7939499621 100644
--- a/academic/ladr/slack-desc
+++ b/academic/ladr/slack-desc
@@ -5,11 +5,11 @@
# make exactly 11 lines for the formatting to be correct. It's also
# customary to leave one space after the ':'.
- |-----handy-ruler------------------------------------------------------|
+ |-----handy-ruler-------------------------------------------------------|
ladr: ladr (Mathematical Programs)
ladr:
ladr: LADR includes some mathematical programs like
-ladr: - prover 9 (automated theorem prover for first-order and equational
+ladr: - prover 9 (automated theorem prover for first-order and equational
ladr: logic)
ladr: - mace4 (search for finite models and counterexamples)
ladr: