academic/ladr: Updated for version 2009_11A

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: