academic/ladr: Updated for version 2008_09A

3 files changed, 607 insertions, 13 deletions

diff --git a/academic/ladr/ladr-libtoolize.diff b/academic/ladr/ladr-libtoolize.diff
new file mode 100644
index 000000000000..9eddee96d94b
--- /dev/null
+++ b/academic/ladr/ladr-libtoolize.diff
@@ -0,0 +1,571 @@
+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
+@@ -2,7 +2,7 @@
+ 	@echo See README.make
+ 
+ all:
+-	cd ladr         && $(MAKE) lib
++	cd ladr         && $(MAKE) lib XFLAGS+=-D_REENTRANT
+ 	cd mace4.src    && $(MAKE) all
+ 	cd provers.src  && $(MAKE) all
+ 	cd apps.src     && $(MAKE) all
+@@ -12,7 +12,7 @@
+ 	@echo ""
+ 
+ ladr lib:
+-	cd ladr         && $(MAKE) lib
++	cd ladr         && $(MAKE) lib XFLAGS+=-D_REENTRANT
+ 
+ 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
+@@ -16,16 +16,16 @@
+ all: ladr apps install realclean
+ 
+ ladr:
+-	cd ../ladr && $(MAKE) libladr.a
++	cd ../ladr && $(MAKE) libladr.la
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o $(PROGRAMS)
++	libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
+ 
+ install:
+-	/bin/mv $(PROGRAMS) ../bin
++	libtool --mode=install /bin/cp $(PROGRAMS) `pwd`/../bin
+ 
+ tags:
+ 	etags *.c ../ladr/*.c
+@@ -33,73 +33,73 @@
+ apps: $(PROGRAMS)
+ 
+ test: test.o
+-	$(CC) $(CFLAGS) -o test test.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o test test.o ../ladr/libladr.la
+ 
+ interpformat: interpformat.o
+-	$(CC) $(CFLAGS) -o interpformat interpformat.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o interpformat interpformat.o ../ladr/libladr.la
+ 
+ prooftrans: prooftrans.o
+-	$(CC) $(CFLAGS) -o prooftrans prooftrans.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o prooftrans prooftrans.o ../ladr/libladr.la
+ 
+ directproof: directproof.o
+-	$(CC) $(CFLAGS) -o directproof directproof.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o directproof directproof.o ../ladr/libladr.la
+ 
+ test_clause_eval: test_clause_eval.o
+-	$(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
+ 
+ latfilter: latfilter.o
+-	$(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.la
+ 
+ olfilter: olfilter.o
+-	$(CC) $(CFLAGS) -o olfilter olfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o olfilter olfilter.o ../ladr/libladr.la
+ 
+ unfast: unfast.o
+-	$(CC) $(CFLAGS) -o unfast unfast.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o unfast unfast.o ../ladr/libladr.la
+ 
+ upper-covers: upper-covers.o
+-	$(CC) $(CFLAGS) -o upper-covers upper-covers.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o upper-covers upper-covers.o ../ladr/libladr.la
+ 
+ miniscope: miniscope.o
+-	$(CC) $(CFLAGS) -o miniscope miniscope.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o miniscope miniscope.o ../ladr/libladr.la
+ 
+ isofilter0: isofilter0.o
+-	$(CC) $(CFLAGS) -o isofilter0 isofilter0.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o isofilter0 isofilter0.o ../ladr/libladr.la
+ 
+ isofilter: isofilter.o
+-	$(CC) $(CFLAGS) -o isofilter isofilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o isofilter isofilter.o ../ladr/libladr.la
+ 
+ isofilter2: isofilter2.o
+-	$(CC) $(CFLAGS) -o isofilter2 isofilter2.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o isofilter2 isofilter2.o ../ladr/libladr.la
+ 
+ dprofiles: dprofiles.o
+-	$(CC) $(CFLAGS) -o dprofiles dprofiles.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o dprofiles dprofiles.o ../ladr/libladr.la
+ 
+ renamer: renamer.o
+-	$(CC) $(CFLAGS) -o renamer renamer.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o renamer renamer.o ../ladr/libladr.la
+ 
+ rewriter: rewriter.o
+-	$(CC) $(CFLAGS) -o rewriter rewriter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o rewriter rewriter.o ../ladr/libladr.la
+ 
+ idfilter: idfilter.o
+-	$(CC) $(CFLAGS) -o idfilter idfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o idfilter idfilter.o ../ladr/libladr.la
+ 
+ clausefilter: clausefilter.o
+-	$(CC) $(CFLAGS) -o clausefilter clausefilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o clausefilter clausefilter.o ../ladr/libladr.la
+ 
+ interpfilter: interpfilter.o
+-	$(CC) $(CFLAGS) -o interpfilter interpfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o interpfilter interpfilter.o ../ladr/libladr.la
+ 
+ clausetester: clausetester.o
+-	$(CC) $(CFLAGS) -o clausetester clausetester.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o clausetester clausetester.o ../ladr/libladr.la
+ 
+ mirror-flip: mirror-flip.o
+-	$(CC) $(CFLAGS) -o mirror-flip mirror-flip.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o mirror-flip mirror-flip.o ../ladr/libladr.la
+ 
+ perm3: perm3.o
+-	$(CC) $(CFLAGS) -o perm3 perm3.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o perm3 perm3.o ../ladr/libladr.la
+ 
+ sigtest: sigtest.o
+-	$(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o sigtest sigtest.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
+@@ -11,46 +11,49 @@
+ # CFLAGS = $(XFLAGS) -pg -O -Wall
+ # CFLAGS = $(XFLAGS)  -Wall -pedantic
+ 
+-BASE_OBJ = order.o clock.o nonport.o\
+-	   fatal.o ibuffer.o memory.o hash.o string.o strbuf.o\
+-           glist.o options.o symbols.o avltree.o
+-TERM_OBJ = term.o termflag.o listterm.o tlist.o flatterm.o multiset.o\
+-	   termorder.o parse.o accanon.o
+-UNIF_OBJ = unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o\
+-           dioph.o btu.o btm.o mindex.o basic.o attrib.o
+-CLAS_OBJ = formula.o definitions.o literals.o topform.o clist.o\
+-	   clauseid.o clauses.o\
+-	   just.o cnf.o clausify.o parautil.o\
+-           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\
+-           backdemod.o\
+-           hints.o ac_redun.o xproofs.o ivy.o
+-MODL_OBJ = interp.o
+-MISC_OBJ = std_options.o banner.o ioutil.o tptp_trans.o top_input.o
++BASE_OBJ = order.lo clock.lo nonport.lo\
++	   fatal.lo ibuffer.lo memory.lo hash.lo string.lo strbuf.lo\
++           glist.lo options.lo symbols.lo avltree.lo
++TERM_OBJ = term.lo termflag.lo listterm.lo tlist.lo flatterm.lo multiset.lo\
++	   termorder.lo parse.lo accanon.lo
++UNIF_OBJ = unify.lo fpalist.lo fpa.lo discrim.lo discrimb.lo discrimw.lo\
++           dioph.lo btu.lo btm.lo mindex.lo basic.lo attrib.lo
++CLAS_OBJ = formula.lo definitions.lo literals.lo topform.lo clist.lo\
++	   clauseid.lo clauses.lo\
++	   just.lo cnf.lo clausify.lo parautil.lo\
++           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\
++           backdemod.lo\
++           hints.lo ac_redun.lo xproofs.lo ivy.lo
++MODL_OBJ = interp.lo
++MISC_OBJ = std_options.lo banner.lo ioutil.lo tptp_trans.lo top_input.lo
+ 
+ 
+ OBJECTS = $(BASE_OBJ) $(TERM_OBJ) $(UNIF_OBJ) $(CLAS_OBJ)\
+           $(INFE_OBJ) $(MODL_OBJ) $(MISC_OBJ)
+ 
+-libladr.a: $(OBJECTS)
+-	$(AR) rs libladr.a $(OBJECTS)
++libladr.la: $(OBJECTS)
++	libtool --mode=link gcc -shared -rpath /usr/lib -version-info 4:0:0 -o libladr.la $(OBJECTS) -lm
++
++%.lo: %.c
++	libtool --mode=compile gcc -c $(CFLAGS) $(XFLAGS) -o $@ $<
+ 
+ ##############################################################################
+ 
+ lib ladr libladr:
+-	$(MAKE) libladr.a
++	$(MAKE) libladr.la
+ 
+ dep:
+ 	util/make_dep $(OBJECTS)
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.lo
+ 
+ realclean:
+-	/bin/rm -f *.o *.a
++	libtool --mode=clean /bin/rm -f *.lo *.la
+ 
+ protos:
+ 	util/make_protos $(OBJECTS)
+@@ -67,150 +70,150 @@
+ 
+ # The rest of the file is generated automatically by util/make_dep
+ 
+-order.o:   	order.h 
++order.lo:   	order.h 
+ 
+-clock.o:   	clock.h string.h memory.h fatal.h header.h
++clock.lo:   	clock.h string.h memory.h fatal.h header.h
+ 
+-nonport.o:   	nonport.h 
++nonport.lo:   	nonport.h 
+ 
+-fatal.o:   	fatal.h header.h
++fatal.lo:   	fatal.h header.h
+ 
+-ibuffer.o:   	ibuffer.h fatal.h header.h
++ibuffer.lo:   	ibuffer.h fatal.h header.h
+ 
+-memory.o:   	memory.h fatal.h header.h
++memory.lo:   	memory.h fatal.h header.h
+ 
+-hash.o:   	hash.h memory.h fatal.h header.h
++hash.lo:   	hash.h memory.h fatal.h header.h
+ 
+-string.o:   	string.h memory.h fatal.h header.h
++string.lo:   	string.h memory.h fatal.h header.h
+ 
+-strbuf.o:   	strbuf.h string.h memory.h fatal.h header.h
++strbuf.lo:   	strbuf.h string.h memory.h fatal.h header.h
+ 
+-glist.o:   	glist.h order.h string.h memory.h fatal.h header.h
++glist.lo:   	glist.h order.h string.h memory.h fatal.h header.h
+ 
+-options.o:   	options.h string.h memory.h fatal.h header.h
++options.lo:   	options.h string.h memory.h fatal.h header.h
+ 
+-symbols.o:   	symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++symbols.lo:   	symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-avltree.o:   	avltree.h memory.h order.h fatal.h header.h
++avltree.lo:   	avltree.h memory.h order.h fatal.h header.h
+ 
+-term.o:   	term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++term.lo:   	term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-termflag.o:   	termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++termflag.lo:   	termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-listterm.o:   	listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++listterm.lo:   	listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-tlist.o:   	tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++tlist.lo:   	tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-flatterm.o:   	flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++flatterm.lo:   	flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-multiset.o:   	multiset.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++multiset.lo:   	multiset.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-termorder.o:   	termorder.h flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++termorder.lo:   	termorder.h flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-parse.o:   	parse.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++parse.lo:   	parse.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-topform.o:   	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
++topform.lo:   	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
+ 
+-clist.o:   	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
++clist.lo:   	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
+ 
+-clauseid.o:   	clauseid.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
++clauseid.lo:   	clauseid.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
+ 
+-clauses.o:   	clauses.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
++clauses.lo:   	clauses.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.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
+ 
+-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
+ 
+-parautil.o:   	parautil.h 
++parautil.lo:   	parautil.h 
+ 
+-pindex.o:   	pindex.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
++pindex.lo:   	pindex.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
+ 
+-compress.o:   	compress.h parautil.h
++compress.lo:   	compress.h parautil.h
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-features.o:   	features.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++features.lo:   	features.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-di_tree.o:   	di_tree.h features.h topform.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h attrib.h formula.h maximal.h unify.h listterm.h termorder.h hash.h flatterm.h
++di_tree.lo:   	di_tree.h features.h topform.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h attrib.h formula.h maximal.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-fastparse.o:   	fastparse.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
++fastparse.lo:   	fastparse.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.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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-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
+ 
+-xproofs.o:   	xproofs.h clauses.h clause_misc.h paramod.h subsume.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 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 parse.h resolve.h clash.h lindex.h parautil.h features.h
++xproofs.lo:   	xproofs.h clauses.h clause_misc.h paramod.h subsume.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 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 parse.h resolve.h clash.h lindex.h parautil.h features.h
+ 
+-ivy.o:   	ivy.h xproofs.h clauses.h clause_misc.h paramod.h subsume.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 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 parse.h resolve.h clash.h lindex.h parautil.h features.h
++ivy.lo:   	ivy.h xproofs.h clauses.h clause_misc.h paramod.h subsume.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 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 parse.h resolve.h clash.h lindex.h parautil.h features.h
+ 
+-interp.o:   	interp.h parse.h topform.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h
++interp.lo:   	interp.h parse.h topform.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h
+ 
+-std_options.o:   	std_options.h options.h symbols.h clock.h string.h memory.h fatal.h header.h strbuf.h glist.h order.h
++std_options.lo:   	std_options.h options.h symbols.h clock.h string.h memory.h fatal.h header.h strbuf.h glist.h order.h
+ 
+-banner.o:   	banner.h nonport.h clock.h string.h memory.h fatal.h header.h
++banner.lo:   	banner.h nonport.h clock.h string.h memory.h fatal.h header.h
+ 
+-ioutil.o:   	ioutil.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
++ioutil.lo:   	ioutil.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
+ 
+-tptp_trans.o:   	tptp_trans.h ioutil.h clausify.h parse.h fastparse.h ivy.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
++tptp_trans.lo:   	tptp_trans.h ioutil.h clausify.h parse.h fastparse.h ivy.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
+ 
+-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 @@
+ 	$(MAKE) libmace4.a
+ 
+ ladr:
+-	cd ../ladr && $(MAKE) libladr.a
++	cd ../ladr && $(MAKE) libladr.la
+ 	$(MAKE) clean
+ 
+ mace4: libmace4.a mace4.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.la
+ 
+ $(OBJECTS): estack.h syms.h ground.h propagate.h mstate.h msearch.h
+ 
+@@ -37,10 +37,10 @@
+ 	etags *.c ../ladr/*.c
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o *.a mace4
++	libtool --mode=clean /bin/rm -f *.o *.a mace4
+ 
+ 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
+@@ -41,13 +41,13 @@
+ 	$(MAKE) clean
+ 
+ install:
+-	/bin/cp -p $(PROGRAMS) ../bin
++	libtool --mode=install /bin/cp -p $(PROGRAMS) `pwd`/../bin
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o $(PROGRAMS)
++	libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
+ 
+ protos:
+ 	util/make_protos $(OBJECTS)
+@@ -63,34 +63,34 @@
+ 	$(MAKE) prover9
+ 
+ prover9: prover9.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.la
+ 
+ fof-prover9: fof-prover9.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.la
+ 
+ ladr_to_tptp: ladr_to_tptp.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.la
+ 
+ tptp_to_ladr: tptp_to_ladr.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.la
+ 
+ autosketches4: autosketches4.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.la
+ 
+ newauto: newauto.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o newauto newauto.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o newauto newauto.o $(OBJECTS) ../ladr/libladr.la
+ 
+ newsax: newsax.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o newsax newsax.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o newsax newsax.o $(OBJECTS) ../ladr/libladr.la
+ 
+ cgrep: cgrep.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.la
+ 
+ mprover: mprover.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.a ../mace4.src/libmace4.a
++	libtool --mode=link $(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.la ../mace4.src/libmace4.la
+ 
+ iterate4: iterate4.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.la
+ 
+ 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
+@@ -17,13 +17,13 @@
+ 
+ ladr:
+ 	make clean
+-	cd ../ladr && $(MAKE) libladr.a
++	cd ../ladr && $(MAKE) libladr.la
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o $(PROGRAMS)
++	libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
+ 
+ tags:
+ 	etags *.c ../ladr/*.c
+@@ -31,8 +31,8 @@
+ apps: $(PROGRAMS)
+ 
+ avltest: avltest.o
+-	$(CC) $(CFLAGS) -o avltest avltest.o ../ladr/libladr.a -lm
++	libtool --mode=link $(CC) $(CFLAGS) -o avltest avltest.o ../ladr/libladr.la -lm
+ 
+ tptp_test: tptp_test.o
+-	$(CC) $(CFLAGS) -o tptp_test tptp_test.o ../ladr/libladr.a -lm
++	libtool --mode=link $(CC) $(CFLAGS) -o tptp_test tptp_test.o ../ladr/libladr.la -lm
+ 
diff --git a/academic/ladr/ladr.SlackBuild b/academic/ladr/ladr.SlackBuild
index 4aa915f80955..2b88462210ac 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 <hmwiesinger@gmx.at>
+# Copyright 2007-2008 Heinz Wiesinger <pprkut@liwjatan.at>
 # 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=Dec_2007
+VERSION=2008_09A
 ARCH=${ARCH:-i486}
 BUILD=${BUILD:-1}
 TAG=${TAG:-_SBo}
@@ -40,6 +40,8 @@ if [ "$ARCH" = "i486" ]; then
   SLKCFLAGS="-O2 -march=i486 -mtune=i686"
 elif [ "$ARCH" = "i686" ]; then
   SLKCFLAGS="-O2 -march=i686 -mtune=i686"
+elif [ "$ARCH" = "x86_64" ]; then
+  SLKCFLAGS="-O2 -fPIC"
 fi
 
 set -e
@@ -51,16 +53,37 @@ rm -rf $SRCNAM-$SRC_VERSION
 tar xvf $CWD/$SRCNAM-$SRC_VERSION.tar.gz
 cd $SRCNAM-$SRC_VERSION
 chown -R root:root .
-chmod -R u+w,go+r-w,a-s .
+find . \
+ \( -perm 777 -o -perm 775 -o -perm 711 -o -perm 555 -o -perm 511 \) \
+ -exec chmod 755 {} \; -o \
+ \( -perm 666 -o -perm 664 -o -perm 600 -o -perm 444 -o -perm 440 -o -perm 400 \) \
+ -exec chmod 644 {} \;
 
-CFLAGS="$SLKCFLAGS" CXXFLAGS="$SLKCFLAGS" make all
+# build and use shared library instead of a static one. Modified version
+# of the patch already included in the upstream package
+patch -p1 -i $CWD/ladr-libtoolize.diff
 
-mkdir -p $PKG/usr/bin
+XFLAGS="$SLKCFLAGS" make all MAKEFLAGS="-j1"
+
+mkdir -p $PKG/usr/{bin,lib}
 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
+
+rm -f $PKG/usr/bin/proof3fo.xsl
+chmod 755 $PKG/usr/bin/gvizify
+
+mkdir -p $PKG/usr/man/man1
+cp -f ./manpages/*.1 $PKG/usr/man/man1/
+
+find $PKG | xargs file | grep -e "executable" -e "shared object" | grep ELF \
+  | cut -f 1 -d : | xargs strip --strip-unneeded 2> /dev/null || true
 
-( cd $PKG
-  find . | xargs file | grep "executable" | grep ELF | cut -f 1 -d : | xargs strip --strip-unneeded 2> /dev/null || true
-  find . | xargs file | grep "shared object" | grep ELF | cut -f 1 -d : | xargs strip --strip-unneeded 2> /dev/null
+( cd $PKG/usr/man
+  find . -type f -exec gzip -9 {} \;
+  for i in $( find . -type l ) ; do ln -s $( readlink $i ).gz $i.gz ; rm $i ; done
 )
 
 mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION
diff --git a/academic/ladr/ladr.info b/academic/ladr/ladr.info
index 5c14a17f1333..8c7a1ae4cdc2 100644
--- a/academic/ladr/ladr.info
+++ b/academic/ladr/ladr.info
@@ -1,8 +1,8 @@
 PRGNAM="ladr"
-VERSION="Dec_2007"
+VERSION="2008_09A"
 HOMEPAGE="http://www.cs.unm.edu/~mccune/prover9/"
-DOWNLOAD="http://www.cs.unm.edu/~mccune/prover9/download/LADR-Dec-2007.tar.gz"
-MD5SUM="6e2896ed4cce4556bfcc321778df5dfe"
+DOWNLOAD="http://www.cs.unm.edu/~mccune/prover9/download/LADR-2008-09A.tar.gz"
+MD5SUM="96cc67eae8f485c22d01449fd2639dae"
 MAINTAINER="ppr:kut"
-EMAIL="HMWiesinger@gmx.at"
-APPROVED="David Somero"
+EMAIL="pprkut@liwjatan.at"
+APPROVED="Michiel"