--- eprover-1.0.004.orig/Makefile
+++ eprover-1.0.004/Makefile
@@ -18,9 +18,9 @@
 #
 #------------------------------------------------------------------------
 
-.PHONY: all depend remove_links clean cleandist default_config debug_config distrib fulldistrib top links tags tools rebuild install config remake documentation E
+.PHONY: all depend cleandist distrib fulldistrib top tags tools rebuild install test config remake documentation E
 
- include Makefile.vars
+include Makefile.vars
 
 # Project specific variables
 
@@ -37,39 +37,24 @@
 
 # Generate dependencies
 
-depend: 
-	for subdir in $(CODE); do\
-	   cd $$subdir; touch Makefile.dependencies; $(MAKE) depend; cd ..;\
-	done;
+depend: ;
+# automatic now
 
 # Remove all automatically generated files
 
-remove_links:
-	cd include; touch does_exist.h; rm *.h
-	cd lib; touch does_exist.a; rm *.a
-
 
-clean: remove_links
+clean:
 	for subdir in $(PARTS); do\
-	   cd $$subdir; touch Makefile.dependencies;$(MAKE) clean; cd ..;\
+	    $(MAKE) -C $$subdir clean ; \
 	done;
 
 cleandist: clean
-	@touch dummy~ PROVER/dummy~
-	rm *~ */*~
+	rm -f *~ */*~ Makefile.cfg */*.d
 
 
-default_config:
-	sed -e 's/CC         = kgcc/CC         = gcc/' Makefile.vars| \
-	awk '/^NODEBUG/{print "NODEBUG    = -DNDEBUG -DFAST_EXIT";next}/^MEMDEBUG/{print "MEMDEBUG   = # -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2";next}/^DEBUGGER/{print "DEBUGGER   = # -g -ggdb";next}{print}' > __tmpmake__;mv __tmpmake__ Makefile.vars
-
-debug_config:
-	cat Makefile.vars| \
-	awk '/^NODEBUG/{print "NODEBUG    = # -DNDEBUG -DFAST_EXIT";next}/^MEMDEBUG/{print "MEMDEBUG   = -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2";next}{print}' > __tmpmake__;mv __tmpmake__ Makefile.vars
-
 # Build a distribution
 
-distrib: cleandist default_config
+distrib: cleandist
 	@echo "Did you think about: "
 	@echo " - Changing the bibliographies to local version"
 	@echo "    ??? "
@@ -80,7 +65,7 @@
 # Include proprietary code not part of the GPL'ed version, 
 # as well as CVS subdirecctories
 
-fulldistrib: cleandist default_config
+fulldistrib: cleandist
 	@echo "Warning: You are building a full archive!"
 	@echo "Did you remember to increase the dev version number and commit to CVS?"
 	cd ..; $(TAR) cf - $(PROJECT)|$(GZIP) - -c > $(PROJECT)_FULL.tgz
@@ -108,8 +93,8 @@
 	cd PYTHON; make tags
 
 tools:
-	cd development_tools;$(MAKE) tools
-	cd PYTHON; $(MAKE) tools
+	$(MAKE) -C development_tools tools
+	$(MAKE) -C PYTHON tools
 
 # Rebuilding from scratch
 
@@ -117,16 +102,14 @@
 	echo 'Rebuilding with debug options $(DEBUGFLAGS)'	
 	$(MAKE) clean
 	$(MAKE) config
-	$(MAKE) depend
-	$(MAKE)
+	$(MAKE) all
 
 # Configure the whole package
 
-config: 
-	echo 'Configuring build system and tools'
-	$(MAKE) links
-	$(MAKE) tools
-	$(MAKE) depend
+config: ;
+# Tools target modifies local source files, which is unsuitable for
+# automatic packaging.
+#	$(MAKE) tools
 
 
 # Configure and copy executables to the installation directory
@@ -140,25 +123,36 @@
 #	@mv tmpfile PROVER/eproof
 
 
+# $(DESTDIR) is used for Debian packaging - it is a build
+# directory into which everything is copied.
+# Normally it expands to just an empty string.
 install: E
-	-sh -c 'mkdir -p $(EXECPATH)'
-	-sh -c 'cp PROVER/eprover $(EXECPATH)'
-	-sh -c 'cp PROVER/epclextract $(EXECPATH)'
-	-sh -c 'cp PROVER/eproof $(EXECPATH)'
-	-sh -c 'cp  PROVER/eground $(EXECPATH)'	
+	sh -c 'mkdir -p $(DESTDIR)$(EXECPATH)'
+	sh -c 'cp PROVER/eprover $(DESTDIR)$(EXECPATH)'
+	sh -c 'cp PROVER/epclextract $(DESTDIR)$(EXECPATH)'
+	sh -c 'sed -e "/^EXECPATH=.*/s|.*|EXECPATH=$(EXECPATH)|" PROVER/eproof > $(DESTDIR)$(EXECPATH)/eproof'
+	sh -c 'chmod 0755 $(DESTDIR)$(EXECPATH)/eproof'
+	sh -c 'cp PROVER/eground $(DESTDIR)$(EXECPATH)'	
+
+test: E
+	PROVER/eprover --output-level=0 --tptp-format -xAuto EXAMPLE_PROBLEMS/TPTP/BOO006-1+rm_eq_rstfp.tptp | grep -q 'Unsatisfiable'
 
 # Also remake documentation
 
 remake: config rebuild documentation
 
 documentation:
-	cd DOC; $(MAKE)
+	$(MAKE) -C DOC all
 
 # Build the single libraries
 
 E:
+	@if [ "$(EXECPATH)" = "" ] ; then \
+	    echo ">>>> EXECPATH undefined, please run './configure' first!" ; \
+	    exit 1 ; \
+	fi
 	for subdir in $(CODE); do\
-	   cd $$subdir;touch Makefile.dependencies;$(MAKE);cd ..;\
+	    $(MAKE) -C $$subdir all ; \
 	done;
 
 
--- eprover-1.0.004.orig/configure
+++ eprover-1.0.004/configure
@@ -75,6 +75,7 @@
 #
 
 EXECPATH=`pwd`/PROVER
+DEBUG=""
 
 
 for argument in  "$@"; do
@@ -90,6 +91,8 @@
         echo "  Equivalent to --bindir=<path>/bin".
         echo "--prefix=<path>"
         echo "  Equivalent to --bindir=<path>/bin".
+        echo "--debug"
+        echo "  Configure Makefile for debugging.".
         exit 0
     else
         opt=`echo "$argument"|cut -d= -f1`
@@ -98,6 +101,8 @@
            EXECPATH=$arg
         elif [ "$opt" = "--exec-prefix" -o "$opt" = "--prefix" ] ; then
            EXECPATH=$arg/bin 
+	elif [ "$opt" = "--debug" ] ; then
+	   DEBUG="1" 
         else
            echo "Unknown option " $argument
            exit 1
@@ -107,11 +112,9 @@
 
 echo "Configuring with executable path "$EXECPATH
 
-sed -e "/^EXECPATH =.*/s|.*|EXECPATH = $EXECPATH|" Makefile.vars > tmpfile
-mv tmpfile Makefile.vars
-
-sed -e "/^EXECPATH=.*/s|.*|EXECPATH=$EXECPATH|" PROVER/eproof > tmpfile
-mv tmpfile PROVER/eproof
-chmod ugo+x PROVER/eproof
+echo "EXECPATH = $EXECPATH" >Makefile.cfg
+if [ "$DEBUG" = "" ] ; then
+    echo "DEBUG = 1" >>Makefile.cfg
+fi
 
 make config
--- eprover-1.0.004.orig/Makefile.vars
+++ eprover-1.0.004/Makefile.vars
@@ -16,10 +16,11 @@
 .PHONY: warn depend links tags remove_links tags rebuild install install_exec distrib fulldistrib top tools remake documentation
 
 
-# EXECPATH is where make install-exec will move the more important
-# executables. Edit it to point to wherever you want them to live.
-
-EXECPATH = /home/schulzs/tmp/tmp/E/PROVER
+# '-' before 'include' means that 'make' won't complain if the target is
+# missing. This is needed for targets like 'cleandist'.
+# We check later in the main Makefile that EXECPATH is defined.
+# (Some older 'make' implementations may use 'sinclude'.)
+-include Makefile.cfg
 
 # Makefile special variables
 #
@@ -34,8 +35,6 @@
 TAR        = tar       # Optional, for building distributions
 GZIP       = gzip
 MCOPY      = mcopy     # Optional, for building floppy disks
-LN         = ln -s     # You can use cp or hard links if your
-                       # system does not support symbolic links
 LATEX      = latex     # Optional if you don't want or need the
                        # documentation. This needs to be latex2e (or
                        # perhaps later), latex 2.09 wont work.
@@ -57,7 +56,13 @@
 
 # System libraries:
 
-LIBS = -lm
+SYSLIBS = -lm
+
+# Look for all *.h files, then keep just the directory names, sort and remove
+# duplicates, and add '-I'.
+INCLUDES   = $(addprefix -I, $(sort $(dir $(wildcard ../*/*.h))))
+# Similarly for *.c.
+LIBS	   = $(addprefix -I, $(sort $(dir $(wildcard ../*/*.c))))
 
 # BUILDFLAGS:
 #
@@ -100,8 +105,13 @@
 
 # The next two flags are dependend - you can only have CLB_MEMORY_DEBUG
 # if you don't have NDEBUG!
+ifdef DEBUG
+MEMDEBUG   = -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2
+NODEBUG    = # -DNDEBUG -DFAST_EXIT
+else
 MEMDEBUG   = # -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2
 NODEBUG    = -DNDEBUG -DFAST_EXIT
+endif
 DEBUGFLAGS = $(PROFFLAGS) $(MEMDEBUG) $(DEBUGGER) $(NODEBUG)
 
 ARCHFLAGS  =  # -mdynamic-no-pic # Helps a tiny bit on Mac
@@ -118,42 +128,42 @@
 # Solaris/Linux with gcc
 #
 #CFLAGS     = -O6 -Wall -Wno-char-subscripts -Wshadow -ansi \
-#             -pedantic -I../include $(DEBUGFLAGS) \
+#             -pedantic $(INCLUDES) $(DEBUGFLAGS) \
 #             $(BUILDFLAGS) $(ARCHFLAGS)
 
 CFLAGS     = -O6 -fomit-frame-pointer -Wall -Wno-char-subscripts -std=gnu99 \
-             -I../include $(DEBUGFLAGS) \
+             $(INCLUDES) $(DEBUGFLAGS) \
              $(BUILDFLAGS) $(ARCHFLAGS)
 
 # Version for profiling
 
 CFLAGS     = -O6 -Wall -Wno-char-subscripts -ansi -std=gnu99 \
-             -I../include $(DEBUGFLAGS) \
+             $(INCLUDES) $(DEBUGFLAGS) \
              $(BUILDFLAGS) $(ARCHFLAGS)
 
 # Version for debugging
 #
 # CFLAGS     = -Wall -Wno-char-subscripts -std=c99 \
-#              -I../include $(DEBUGFLAGS) \
+#              $(INCLUDES) $(DEBUGFLAGS) \
 #              $(BUILDFLAGS) $(ARCHFLAGS)
 
 # Workaround for broken Red Hat gcc 2.96 (hah!)
 
 # CFLAGS     = -O6 -fno-strength-reduce -Wall -Wno-char-subscripts -Wshadow -ansi \
-#             -pedantic -I../include $(DEBUGFLAGS) \
+#             -pedantic $(INCLUDES) $(DEBUGFLAGS) \
 #             $(BUILDFLAGS) $(ARCHFLAGS)
 #
 # Solaris with SUN's SUNPro cc
-# CFLAGS     = -fast -I../include $(BUILDFLAGS) $(DEBUGFLAGS) -D__inline__=""
+# CFLAGS     = -fast $(INCLUDES) $(BUILDFLAGS) $(DEBUGFLAGS) -D__inline__=""
 #
 # HPUX with gcc - someone please hurt an HP employee for me!
 #
 # CFLAGS     = -O6 -Wall -Wno-char-subscripts -Wshadow \
-#             -I../include $(DEBUGFLAGS) \
+#             $(INCLUDES) $(DEBUGFLAGS) \
 #             $(BUILDFLAGS) $(ARCHFLAGS) -DHP_UX
 
 
-LDFLAGS    = $(PROFFLAGS) $(DEBUGGER) $(LIBS) 
+LDFLAGS    = $(PROFFLAGS) $(DEBUGGER) $(SYSLIBS) $(LIBS)
 CC         = gcc
 # CC         = cc
 LD         = $(CC) $(LDFLAGS)
@@ -162,9 +172,13 @@
 # dependencies. gcc does a better job than makedepend, so it is the
 # default. 
 #
-# MAKEDEPEND = echo "" > Makefile.dependencies; makedepend -- $(CFLAGS) -- -f Makefile.dependencies *.c
-MAKEDEPEND = gcc -M $(CFLAGS) *.c > Makefile.dependencies
-
-
-
 
+ifneq ($(MAKECMDGOALS),clean)
+include $(patsubst %.c,%.d,$(wildcard *.c))
+endif
+
+%.d: %.c
+	@echo Computing dependencies for $<
+	@set -e; rm -f $@; \
+	    $(CC) -M $(CFLAGS) $< | \
+	    sed 's,\($*\)\.o[ :]*,\1.o $@ : ,g' > $@
--- eprover-1.0.004.orig/PROVER/Makefile
+++ eprover-1.0.004/PROVER/Makefile
@@ -22,8 +22,6 @@
 LIB     = $(PROJECT)
 all: $(LIB)
 
-depend: *.c
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -38,121 +36,120 @@
 
 # Build the programs
 
-EPROVER = eprover.o ../lib/CONTROL.a ../lib/HEURISTICS.a\
-            ../lib/LEARN.a\
-            ../lib/CLAUSES.a ../lib/ORDERINGS.a ../lib/TERMS.a\
-            ../lib/INOUT.a ../lib/BASICS.a
+EPROVER = eprover.o ../CONTROL/CONTROL.a ../HEURISTICS/HEURISTICS.a\
+            ../LEARN/LEARN.a\
+            ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a ../TERMS/TERMS.a\
+            ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 eprover: $(EPROVER)
 	$(LD) -o eprover $(EPROVER)
 
-EGROUND = eground.o ../lib/HEURISTICS.a\
-            ../lib/CLAUSES.a ../lib/ORDERINGS.a ../lib/TERMS.a\
-            ../lib/INOUT.a ../lib/BASICS.a
+EGROUND = eground.o ../HEURISTICS/HEURISTICS.a\
+            ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a ../TERMS/TERMS.a\
+            ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 eground: $(EGROUND)
 	$(LD) -o eground $(EGROUND)
 
-EDPLL = edpll.o ../lib/PROPOSITIONAL.a ../lib/CLAUSES.a\
-        ../lib/ORDERINGS.a ../lib/TERMS.a ../lib/INOUT.a\
-	../lib/BASICS.a 
+EDPLL = edpll.o ../PROPOSITIONAL/PROPOSITIONAL.a ../CLAUSES/CLAUSES.a\
+        ../ORDERINGS/ORDERINGS.a ../TERMS/TERMS.a ../INOUT/INOUT.a\
+	../BASICS/BASICS.a 
 
 edpll: $(EDPLL)
 	$(LD) -o edpll $(EDPLL)
 
-CLASSIFY = classify_problem.o ../lib/HEURISTICS.a\
-            ../lib/CLAUSES.a ../lib/ORDERINGS.a ../lib/TERMS.a\
-            ../lib/INOUT.a ../lib/BASICS.a
+CLASSIFY = classify_problem.o ../HEURISTICS/HEURISTICS.a\
+            ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a ../TERMS/TERMS.a\
+            ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 classify_problem: $(CLASSIFY)
 	$(LD) -o classify_problem $(CLASSIFY)
 
-TERMPROPS = termprops.o ../lib/TERMS.a\
-            ../lib/INOUT.a ../lib/BASICS.a
+TERMPROPS = termprops.o ../TERMS/TERMS.a\
+            ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 termprops: $(TERMPROPS)
 	$(LD) -o termprops $(TERMPROPS)
 
 DIRECT_EXAMPLES = direct_examples.o \
-            ../lib/PCL2.a ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-            ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+            ../PCL2/PCL2.a ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+            ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 direct_examples: $(DIRECT_EXAMPLES)
 	$(LD) -o direct_examples $(DIRECT_EXAMPLES)
 
 
 EPCLANALYSE = epclanalyse.o \
-        ../lib/PCL2.a ../lib/HEURISTICS.a ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-        ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+        ../PCL2/PCL2.a ../HEURISTICS/HEURISTICS.a ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+        ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 epclanalyse: $(EPCLANALYSE)
 	$(LD) -o epclanalyse $(EPCLANALYSE)
 
 
 EPCLLEMMA = epcllemma.o \
-        ../lib/PCL2.a ../lib/HEURISTICS.a ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-        ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+        ../PCL2/PCL2.a ../HEURISTICS/HEURISTICS.a ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+        ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 epcllemma: $(EPCLLEMMA)
 	$(LD) -o epcllemma $(EPCLLEMMA)
 
 
 EPCLEXTRACT = epclextract.o \
-        ../lib/PCL2.a ../lib/HEURISTICS.a ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-        ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+        ../PCL2/PCL2.a ../HEURISTICS/HEURISTICS.a ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+        ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 epclextract: $(EPCLEXTRACT)
 	$(LD) -o epclextract $(EPCLEXTRACT)
 
 CHECKPROOF = checkproof.o \
-        ../lib/PCL2.a ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-        ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+        ../PCL2/PCL2.a ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+        ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 checkproof: $(CHECKPROOF)
 	$(LD) -o checkproof $(CHECKPROOF)
 
 EKB_CREATE = ekb_create.o \
-            ../lib/LEARN.a ../lib/ANALYSIS.a ../lib/CLAUSES.a \
-            ../lib/ORDERINGS.a \
-            ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+            ../LEARN/LEARN.a ../ANALYSIS/ANALYSIS.a ../CLAUSES/CLAUSES.a \
+            ../ORDERINGS/ORDERINGS.a \
+            ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 ekb_create: $(EKB_CREATE)
 	$(LD) -o ekb_create $(EKB_CREATE)
 
 EKB_INSERT = ekb_insert.o \
-            ../lib/LEARN.a ../lib/ANALYSIS.a ../lib/CLAUSES.a \
-            ../lib/ORDERINGS.a \
-            ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+            ../LEARN/LEARN.a ../ANALYSIS/ANALYSIS.a ../CLAUSES/CLAUSES.a \
+            ../ORDERINGS/ORDERINGS.a \
+            ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 ekb_insert: $(EKB_INSERT)
 	$(LD) -o ekb_insert $(EKB_INSERT)
 
 EKB_GINSERT = ekb_ginsert.o \
-	    ../lib/PCL2.a ../lib/LEARN.a ../lib/ANALYSIS.a ../lib/CLAUSES.a \
-            ../lib/ORDERINGS.a \
-            ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+	    ../PCL2/PCL2.a ../LEARN/LEARN.a ../ANALYSIS/ANALYSIS.a ../CLAUSES/CLAUSES.a \
+            ../ORDERINGS/ORDERINGS.a \
+            ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 ekb_ginsert: $(EKB_GINSERT)
 	$(LD) -o ekb_ginsert $(EKB_GINSERT)
 
 EKB_DELETE = ekb_delete.o \
-            ../lib/LEARN.a ../lib/ANALYSIS.a ../lib/CLAUSES.a \
-            ../lib/ORDERINGS.a \
-            ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+            ../LEARN/LEARN.a ../ANALYSIS/ANALYSIS.a ../CLAUSES/CLAUSES.a \
+            ../ORDERINGS/ORDERINGS.a \
+            ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 ekb_delete: $(EKB_DELETE)
 	$(LD) -o ekb_delete $(EKB_DELETE)
 
 TSM_CLASSIFY = tsm_classify.o \
-            ../lib/LEARN.a ../lib/ANALYSIS.a ../lib/CLAUSES.a \
-            ../lib/ORDERINGS.a \
-            ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+            ../LEARN/LEARN.a ../ANALYSIS/ANALYSIS.a ../CLAUSES/CLAUSES.a \
+            ../ORDERINGS/ORDERINGS.a \
+            ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 tsm_classify: $(TSM_CLASSIFY)
 	$(LD) -o tsm_classify $(TSM_CLASSIFY)
 
 
-include Makefile.dependencies
 
 
 
--- eprover-1.0.004.orig/TEST/Makefile
+++ eprover-1.0.004/TEST/Makefile
@@ -19,8 +19,6 @@
 LIB     = $(PROJECT)
 all: $(LIB) patterntest
 
-depend: *.c
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -37,29 +35,28 @@
 
 # Build the test program
 
-TEST_PROG = cl_test.o ../lib/CONTROL.a ../lib/HEURISTICS.a\
-            ../lib/CLAUSES.a ../lib/ORDERINGS.a ../lib/TERMS.a\
-            ../lib/INOUT.a ../lib/BASICS.a
+TEST_PROG = cl_test.o ../CONTROL/CONTROL.a ../HEURISTICS/HEURISTICS.a\
+            ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a ../TERMS/TERMS.a\
+            ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 $(LIB): $(TEST_PROG)
 	$(LD) -o $(PROJECT) $(TEST_PROG)
 
 
-PATTERN_TEST = patterntest.o ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-	    ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a ../lib/LEARN.a
+PATTERN_TEST = patterntest.o ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+	    ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a ../LEARN/LEARN.a
 
 patterntest: $(PATTERN_TEST)
 	$(LD) -o patterntest $(PATTERN_TEST)
 
 
-PCL_TEST = cl_pcltest.o ../lib/PCL2.a ../lib/CLAUSES.a ../lib/ORDERINGS.a \
-	../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+PCL_TEST = cl_pcltest.o ../PCL2/PCL2.a ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a \
+	../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 cl_pcltest: $(PCL_TEST)
 	$(LD) -o cl_pcltest $(PCL_TEST)
 
 
-include Makefile.dependencies
 
 
 
--- eprover-1.0.004.orig/TERMS/Makefile
+++ eprover-1.0.004/TERMS/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -47,5 +45,4 @@
 $(LIB): $(TERM_LIB)
 	$(AR) $(LIB) $(TERM_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/HEURISTICS/Makefile
+++ eprover-1.0.004/HEURISTICS/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -56,5 +54,4 @@
 $(LIB): $(HEURISTICS_LIB)
 	$(AR) $(LIB) $(HEURISTICS_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/PROPOSITIONAL/Makefile
+++ eprover-1.0.004/PROPOSITIONAL/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -41,5 +39,4 @@
 $(LIB): $(PROP_LIB)
 	$(AR) $(LIB) $(PROP_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/INOUT/Makefile
+++ eprover-1.0.004/INOUT/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -41,5 +39,4 @@
 $(LIB): $(IO_LIB)
 	$(AR) $(LIB) $(IO_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/PCL2/Makefile
+++ eprover-1.0.004/PCL2/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -40,5 +38,4 @@
 $(LIB): $(PCL2_LIB)
 	$(AR) $(LIB) $(PCL2_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/DOC/Makefile
+++ eprover-1.0.004/DOC/Makefile
@@ -24,10 +24,14 @@
 	@touch does_exist.aux does_exist.log does_exist.dvi does_exist.ps;
 	@rm *.aux *.log *.dvi *.ps;
 	@echo Removed compiled files
+	# added for tex4ht
+	rm -rf html
+	rm -f *.4tc *.4ct *.lg *.idv *.tmp *.xref eprover*.css eprover*.html
 
 depend:
 	echo "No dependencies for LaTeX documentation"
 
+
 # Services (provided by the master Makefile)
 
 include ../Makefile.services
@@ -45,3 +49,12 @@
 	$(LATEX) eprover.tex
 	$(PDFLATEX) eprover.tex
 	$(DVIPS) -o eprover.ps eprover.dvi
+
+
+html: html/eprover.html
+
+html/eprover.html: eprover.tex
+	mkdir -p html
+	htlatex $< "xhtml,2,info,sections+,fn-in" unicode -d./html/
+
+.PHONY: html
--- eprover-1.0.004.orig/BASICS/Makefile
+++ eprover-1.0.004/BASICS/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -47,7 +45,6 @@
 $(LIB): $(BASIC_LIB)
 	$(AR) $(LIB) $(BASIC_LIB)
 
-include Makefile.dependencies
 
 
 
--- eprover-1.0.004.orig/LEARN/Makefile
+++ eprover-1.0.004/LEARN/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -46,5 +44,4 @@
 $(LIB): $(LEARN_LIB)
 	$(AR) $(LIB) $(LEARN_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/debian/eprover-doc-html.links
+++ eprover-1.0.004/debian/eprover-doc-html.links
@@ -0,0 +1 @@
+usr/share/doc/eprover/html usr/share/doc/eprover-doc-html/html
--- eprover-1.0.004.orig/debian/eground.1
+++ eprover-1.0.004/debian/eground.1
@@ -0,0 +1,260 @@
+.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.36.
+.TH E "1" "February 2009" "E 0.4" "User Commands"
+.SH NAME
+E \- The Equational Theorem Prover User Manual
+.SH SYNOPSIS
+.B eground
+[\fIoptions\fR] [\fIfiles\fR]
+.SH DESCRIPTION
+eground 0.4
+.PP
+Read a set of clauses and determine if it can be grounded (i.e. is
+either already ground or has no non\-constant function symbols). If
+this is the case, print sufficiently many ground instances of the
+clauses to guarantee that a ground refutation can be found for
+unsatisfiable clause sets.
+.HP
+\fB\-h\fR
+.HP
+\fB\-\-help\fR
+.IP
+Print a short description of program usage and options.
+.HP
+\fB\-\-version\fR
+.IP
+Print the version number of the program.
+.HP
+\fB\-v\fR
+.HP
+\fB\-\-verbose[=\fR<arg>]
+.IP
+Verbose comments on the progress of the program by printing technical
+information to stderr. The short form or the long form without the
+optional argument is equivalent to \fB\-\-verbose\fR=\fI1\fR.
+.HP
+\fB\-o\fR <arg>
+.HP
+\fB\-\-output\-file=\fR<arg>
+.IP
+Redirect output into the named file.
+.HP
+\fB\-s\fR
+.HP
+\fB\-\-silent\fR
+.IP
+Equivalent to \fB\-\-output\-level\fR=\fI0\fR.
+.HP
+\fB\-l\fR <arg>
+.HP
+\fB\-\-output\-level=\fR<arg>
+.IP
+Select an output level, greater values imply more verbose output. Level 0
+produces nearly no output except for the final clauses, level 1 produces
+minimal additional output. Higher levels are without meaning in eground
+(I think).
+.HP
+\fB\-\-print\-statistics\fR
+.IP
+Print a short statistical summary of clauses read and generated.
+.HP
+\fB\-R\fR
+.HP
+\fB\-\-resources\-info\fR
+.IP
+Give some information about the resources used by the system. You will
+usually get CPU time information. On systems returning more information
+with the rusage() system call, you will also get information about memory
+consumption.
+.HP
+\fB\-\-suppress\-result\fR
+.IP
+Supress actual printing of the result, just give a short message about
+success. Useful mainly for test runs.
+.HP
+\fB\-\-tptp\-in\fR
+.IP
+Parse TPTP\-2 format instead of E\-LOP (except includes, which are handles
+as in TPTP\-3, as TPTP\-2 include syntax is considered harmful).
+.HP
+\fB\-\-tptp\-out\fR
+.IP
+Print TPTP\-2 format instead of E\-LOP.
+.HP
+\fB\-\-tptp\-format\fR
+.IP
+Equivalent to \fB\-\-tptp\-in\fR and \fB\-\-tptp\-out\fR.
+.HP
+\fB\-\-tptp2\-in\fR
+.IP
+Synonymous with \fB\-\-tptp\-in\fR.
+.HP
+\fB\-\-tptp2\-out\fR
+.IP
+Synonymous with \fB\-\-tptp\-out\fR.
+.HP
+\fB\-\-tptp2\-format\fR
+.IP
+Synonymous with \fB\-\-tptp\-format\fR.
+.HP
+\fB\-\-tstp\-in\fR
+.IP
+Parse TPTP\-3 format instead of E\-LOP (Note that TPTP\-3 syntax is still
+under development, and the version implemented may not be fully
+conformant at all times. It works on all TPTP 3.0.1 input files
+(including includes).
+.HP
+\fB\-\-tstp\-out\fR
+.IP
+Print output clauses in TPTP\-3 syntax.
+.HP
+\fB\-\-tstp\-format\fR
+.IP
+Equivalent to \fB\-\-tstp\-in\fR and \fB\-\-tstp\-out\fR.
+.HP
+\fB\-\-tptp3\-in\fR
+.IP
+Synonymous with \fB\-\-tstp\-in\fR.
+.HP
+\fB\-\-tptp3\-out\fR
+.IP
+Synonymous with \fB\-\-tstp\-out\fR.
+.HP
+\fB\-\-tptp3\-format\fR
+.IP
+Synonymous with \fB\-\-tstp\-format\fR.
+.HP
+\fB\-d\fR
+.HP
+\fB\-\-dimacs\fR
+.IP
+Print output in the DIMACS format suitable for many propositional
+provers.
+.HP
+\fB\-\-split\-tries[=\fR<arg>]
+.IP
+Determine the number of tries for splitting. If 0, no splitting is
+performed. If 1, only variable\-disjoint splits are done. Otherwise, up to
+the desired number of variable permutations is tried to find a splitting
+subset. The option without the optional argument is equivalent to
+\fB\-\-split\-tries\fR=\fI1\fR.
+.HP
+\fB\-U\fR
+.HP
+\fB\-\-no\-unit\-subsumption\fR
+.IP
+Do not check if clauses are subsumed by previously encountered unit
+clauses.
+.HP
+\fB\-r\fR
+.HP
+\fB\-\-no\-unit\-resolution\fR
+.IP
+Do not perform forward\-unit\-resolution on new clauses.
+.HP
+\fB\-t\fR
+.HP
+\fB\-\-no\-tautology\-detection\fR
+.IP
+Do not perform tautology deletion on new clauses.
+.HP
+\fB\-m\fR <arg>
+.HP
+\fB\-\-memory\-limit=\fR<arg>
+.IP
+Limit the memory the system may use. The argument is the allowed amount
+of memory in MB. This option may not work everywhere, due to broken
+and/or strange behaviour of setrlimit() in some UNIX implementations. It
+does work under all tested versions of Solaris and GNU/Linux.
+.HP
+\fB\-\-cpu\-limit[=\fR<arg>]
+.IP
+Limit the cpu time the program should run. The optional argument is the
+CPU time in seconds. The program will terminate immediately after
+reaching the time limit, regardless of internal state. This option may
+not work everywhere, due to broken and/or strange behaviour of
+setrlimit() in some UNIX implementations. It does work under all tested
+versions of Solaris, HP\-UX and GNU/Linux. As a side effect, this option
+will inhibit core file writing. The option without the optional argument
+is equivalent to \fB\-\-cpu\-limit\fR=\fI300\fR.
+.HP
+\fB\-\-soft\-cpu\-limit[=\fR<arg>]
+.IP
+Limit the cpu time spend in grounding. After the time expires, the prover
+will print an partial system. The option without the optional argument is
+equivalent to \fB\-\-soft\-cpu\-limit\fR=\fI310\fR.
+.HP
+\fB\-i\fR
+.HP
+\fB\-\-add\-one\-instance\fR
+.IP
+If the grounding procedure runs out of time or memory, try to add at
+least one instance of each clause to the set. This might fail for  really
+large clause sets, since the reserve memory kept for this purpose may be
+insufficient.
+.HP
+\fB\-g\fR <arg>
+.HP
+\fB\-\-give\-up=\fR<arg>
+.IP
+Give up early if the problem is unlikely to be reasonably small. If run
+without constraints, the programm will give up if the clause with the
+largest number of instances will be expanded into more than this number
+of instances. If run with contraints, the program keeps a running count
+and will terminate if the estimated total number of clauses would exceed
+this value . A value of 0 will leave this test disabled.
+.HP
+\fB\-c\fR
+.HP
+\fB\-\-constraints\fR
+.IP
+Use global purity constraints to restrict the number of instantiations
+done.
+.HP
+\fB\-C\fR
+.HP
+\fB\-\-local\-constraints\fR
+.IP
+Use local purity constraints to further restrict the number of
+instantiations done. Implies the previous option. Not yet implemented!
+Note to self: Split clauses need to get fresh variables if this is to
+work!
+.SH AUTHOR
+Stephan Schulz <schulz@eprover.org>
+.SH COPYRIGHT
+Copyright 1998\-2006 by Stephan Schulz <schulz@eprover.org>
+.PP
+You can find the latest version of E and additional information at
+http://www.eprover.org
+.PP
+This program is free software; you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 2 of the License, or
+(at your option) any later version.
+.PP
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+.PP
+You should have received a copy of the GNU General Public License
+along with this program (it should be contained in the top level
+directory of the distribution in the file COPYING); if not, write to
+the Free Software Foundation, Inc., 59 Temple Place, Suite 330,
+Boston, MA  02111\-1307 USA
+.PP
+The original copyright holder can be contacted as
+.PP
+Stephan Schulz (I4)
+.br
+Technische Universitaet Muenchen
+.br
+Institut fuer Informatik
+.br
+Boltzmannstrasse 3
+.br
+85748 Garching bei Muenchen
+.br
+Germany
+.SH "SEE ALSO"
+.BR epclextract (1).
+.BR eprover (1),
--- eprover-1.0.004.orig/debian/eprover.doc-base
+++ eprover-1.0.004/debian/eprover.doc-base
@@ -0,0 +1,11 @@
+Document: eprover
+Title: User Manual for E - the equational theorem prover
+Author: Stephan Schulz
+Abstract: E is an equational theorem prover for full clausal logic, based on
+ superposition and rewriting. In this very preliminary manual we first give a
+ short introduction for impatient new users, and then cover calculus, control,
+ options and input/output of the prover in some more detail.
+Section: Science/Mathematics
+
+Format: pdf
+Files: /usr/share/doc/eprover/eprover.pdf.gz
--- eprover-1.0.004.orig/debian/epclextract.1
+++ eprover-1.0.004/debian/epclextract.1
@@ -0,0 +1,107 @@
+.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.36.
+.TH E "1" "February 2009" "E 0.41" "User Commands"
+.SH NAME
+E \- The Equational Theorem Prover User Manual
+.SH SYNOPSIS
+.B epclextract
+[\fIoptions\fR] [\fIfiles\fR]
+.SH DESCRIPTION
+epclextract 0.41
+.PP
+Read an PCL2 protocol and print the steps necessary for proving the clauses in "proof", "final", or "extract" steps.
+.HP
+\fB\-h\fR
+.HP
+\fB\-\-help\fR
+.IP
+Print a short description of program usage and options.
+.HP
+\fB\-\-version\fR
+.IP
+Print the version number of the program.
+.HP
+\fB\-v\fR
+.HP
+\fB\-\-verbose[=\fR<arg>]
+.IP
+Verbose comments on the progress of the program. The short form or the
+long form without the optional argument is equivalent to \fB\-\-verbose\fR=\fI1\fR.
+.HP
+\fB\-f\fR
+.HP
+\fB\-\-fast\-extract\fR
+.IP
+Do a fast extract. With this option the program understands only a subset
+of PCL and assumes that all "proof" and "final" steps are at the end of
+the protokoll.
+.HP
+\fB\-c\fR
+.HP
+\fB\-\-competition\-framing\fR
+.IP
+Print special "begin" and "end"comments around the proof object, as
+requiered by the CASC MIX* class.
+.HP
+\fB\-n\fR
+.HP
+\fB\-\-no\-extract\fR
+.IP
+Don't extract, print back all steps (actually, it treats all steps as
+proof steps). Useful as a syntax checker, or if you want to convert PCL
+to TSTP with the next option.
+.HP
+\fB\-\-tstp\-out\fR
+.IP
+Print proof protocol in TSTP syntax (default is PCL).
+.HP
+\fB\-o\fR <arg>
+.HP
+\fB\-\-output\-file=\fR<arg>
+.IP
+Redirect output into the named file.
+.HP
+\fB\-s\fR
+.HP
+\fB\-\-silent\fR
+.IP
+Equivalent to \fB\-\-output\-level\fR=\fI0\fR.
+.SH AUTHOR
+Stephan Schulz <schulz@eprover.org>
+.SH COPYRIGHT
+Copyright 1998\-2006 by Stephan Schulz <schulz@eprover.org>
+.PP
+You can find the latest version of E and additional information at
+http://www.eprover.org
+.PP
+This program is free software; you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 2 of the License, or
+(at your option) any later version.
+.PP
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+.PP
+You should have received a copy of the GNU General Public License
+along with this program (it should be contained in the top level
+directory of the distribution in the file COPYING); if not, write to
+the Free Software Foundation, Inc., 59 Temple Place, Suite 330,
+Boston, MA  02111\-1307 USA
+.PP
+The original copyright holder can be contacted as
+.PP
+Stephan Schulz (I4)
+.br
+Technische Universitaet Muenchen
+.br
+Institut fuer Informatik
+.br
+Boltzmannstrasse 3
+.br
+85748 Garching bei Muenchen
+.br
+Germany
+.SH "SEE ALSO"
+.BR eground (1),
+.BR eprover (1).
--- eprover-1.0.004.orig/debian/eprover-examples.README.Debian
+++ eprover-1.0.004/debian/eprover-examples.README.Debian
@@ -0,0 +1,11 @@
+README.Debian for eprover
+-------------------------
+
+This package contains several sample inputs for automated theorem prover E.
+These examples are installed into the doc directory of the eprover package
+/usr/share/doc/eprover/examples.
+
+For more problems you may check The TPTP (Thousands of Problems for Theorem
+Provers) Problem Library at http://www.tptp.org/
+
+ -- Petr Pudlak <deb@pudlak.name>  Tue, 03 Mar 2009 15:03:06 +0100
--- eprover-1.0.004.orig/debian/dirs
+++ eprover-1.0.004/debian/dirs
@@ -0,0 +1 @@
+usr/bin
--- eprover-1.0.004.orig/debian/rules
+++ eprover-1.0.004/debian/rules
@@ -0,0 +1,157 @@
+#!/usr/bin/make -f
+# -*- makefile -*-
+# Sample debian/rules that uses debhelper.
+# This file was originally written by Joey Hess and Craig Small.
+# As a special exception, when this file is copied by dh-make into a
+# dh-make output file, you may use that output file without restriction.
+# This special exception was added by Craig Small in version 0.37 of dh-make.
+
+# Uncomment this to turn on verbose mode.
+#export DH_VERBOSE=1
+
+
+# These are used for cross-compiling and for saving the configure script
+# from having to guess our platform (since we know it already)
+DEB_HOST_GNU_TYPE   ?= $(shell dpkg-architecture -qDEB_HOST_GNU_TYPE)
+DEB_BUILD_GNU_TYPE  ?= $(shell dpkg-architecture -qDEB_BUILD_GNU_TYPE)
+ifneq ($(DEB_HOST_GNU_TYPE),$(DEB_BUILD_GNU_TYPE))
+CROSS= --build $(DEB_BUILD_GNU_TYPE) --host $(DEB_HOST_GNU_TYPE)
+else
+CROSS= --build $(DEB_BUILD_GNU_TYPE)
+endif
+
+PKGNAME=eprover
+DESTDIR=$(CURDIR)/debian/$(PKGNAME)
+
+
+
+config.status: configure
+	dh_testdir
+	# Add here commands to configure the package.
+ifneq "$(wildcard /usr/share/misc/config.sub)" ""
+	cp -f /usr/share/misc/config.sub config.sub
+endif
+ifneq "$(wildcard /usr/share/misc/config.guess)" ""
+	cp -f /usr/share/misc/config.guess config.guess
+endif
+	#CFLAGS="$(CFLAGS)" ./configure $(CROSS) --prefix=/usr
+	CFLAGS="$(CFLAGS)" ./configure --prefix=/usr
+
+
+build: build-arch
+
+build-arch: build-stamp-arch
+
+build-stamp-arch:  config.status 
+	dh_testdir
+
+	# Add here commands to compile the package.
+	$(MAKE)
+	#docbook-to-man debian/eprover.sgml > eprover.1
+	# test that the prover really compiled and works
+	$(MAKE) test
+
+	touch $@
+
+build-manpages: debian/eprover.1
+
+
+build-indep: build-stamp-indep
+
+build-stamp-indep:  config.status build-manpages
+	dh_testdir
+	$(MAKE) -C DOC html
+	touch $@
+
+#debian/%.1: debian/%.1.xml
+#	xsltproc --nonet \
+#	    --param make.year.ranges 1 \
+#	    --param make.single.year.ranges 1 \
+#	    --param man.charmap.use.subset 0 \
+#	    -o debian/ \
+#	    /usr/share/xml/docbook/stylesheet/nwalsh/manpages/docbook.xsl \
+#	    $<
+
+clean:
+	dh_testdir
+	dh_testroot
+	rm -f build-stamp-arch build-stamp-indep
+
+	# Add here commands to clean up after the build process.
+	[ ! -f Makefile ] || $(MAKE) cleandist
+	rm -f config.sub config.guess
+
+	dh_clean 
+
+install-arch: build-arch
+	dh_testdir
+	dh_testroot
+	dh_prep  
+	dh_installdirs
+	# Add here commands to install the package into debian/eprover.
+	$(MAKE) DESTDIR=$(DESTDIR) install
+
+install-indep: build-indep
+	dh_testdir
+	dh_testroot
+	dh_prep  
+	dh_installdirs
+	# Add here commands to install the package into debian/eprover.
+
+
+# Build architecture-independent files here.
+# We have nothing to do by default.
+binary-indep: export DH_OPTIONS=-i
+binary-indep: install-indep
+	dh_testdir
+	dh_testroot
+	dh_installchangelogs DOC/NEWS
+	dh_installdocs
+	dh_installexamples
+	dh_install
+	dh_installman
+	dh_link
+	dh_compress
+	dh_fixperms
+	dh_installdeb
+	dh_shlibdeps
+	dh_gencontrol
+	dh_md5sums
+	dh_builddeb
+
+# Build architecture-dependent files here.
+binary-arch: export DH_OPTIONS=-a
+binary-arch: install-arch
+	dh_testdir
+	dh_testroot
+	dh_installchangelogs DOC/NEWS
+	dh_installdocs
+	dh_installexamples
+	dh_install
+#	dh_installmenu
+#	dh_installdebconf
+#	dh_installlogrotate
+#	dh_installemacsen
+#	dh_installpam
+#	dh_installmime
+#	dh_python
+#	dh_installinit
+#	dh_installcron
+#	dh_installinfo
+	dh_installman
+	dh_link
+	dh_strip
+	dh_compress
+	dh_fixperms
+#	dh_perl
+#	dh_makeshlibs
+	dh_installdeb
+	dh_shlibdeps
+	dh_gencontrol
+	dh_md5sums
+	dh_builddeb
+
+
+binary: binary-indep binary-arch
+
+.PHONY: build clean binary-indep binary-arch binary install
--- eprover-1.0.004.orig/debian/eprover-examples.links
+++ eprover-1.0.004/debian/eprover-examples.links
@@ -0,0 +1 @@
+usr/share/doc/eprover/examples usr/share/doc/eprover-examples/examples
--- eprover-1.0.004.orig/debian/eprover.docs
+++ eprover-1.0.004/debian/eprover.docs
@@ -0,0 +1,12 @@
+README
+DOC/ANNOUNCE
+DOC/CREDITS
+DOC/DONE
+DOC/E-REMARKS.english
+DOC/NEWS
+DOC/PORTING
+DOC/TODO
+DOC/TSTP_Syntax.txt
+DOC/WISHLIST
+DOC/eprover.pdf
+DOC/grammar.txt
--- eprover-1.0.004.orig/debian/eprover-doc-html.install
+++ eprover-1.0.004/debian/eprover-doc-html.install
@@ -0,0 +1 @@
+DOC/html  usr/share/doc/eprover
--- eprover-1.0.004.orig/debian/control
+++ eprover-1.0.004/debian/control
@@ -0,0 +1,89 @@
+Source: eprover
+Section: science
+Priority: extra
+Maintainer: Ubuntu MOTU Developers <ubuntu-motu@lists.ubuntu.com>
+XSBC-Original-Maintainer: Debian Science Maintainers <debian-science-maintainers@lists.alioth.debian.org>
+Uploaders: Petr Pudlak <deb@pudlak.name>
+Build-Depends: debhelper (>= 7), autotools-dev, sed (>= 4.1), mawk (>= 1.3) | gawk (>= 3.1) | awk
+Build-Depends-Indep: tex4ht, texlive-latex-base, texlive-latex-extra, dvipng
+Standards-Version: 3.8.0
+Homepage: http://www.eprover.org/
+DM-Upload-Allowed: yes
+Vcs-Git: git://git.debian.org/git/debian-science/packages/eprover.git
+Vcs-Browser: http://git.debian.org/?p=debian-science/packages/eprover.git
+
+Package: eprover
+Architecture: any
+Depends: ${shlibs:Depends}, ${misc:Depends}
+Recommends: eprover-doc-html
+Suggests: eprover-examples
+Description: Theorem prover for first-order logic with equality
+ E is a fully automatic theorem prover for full first-order logic with
+ equality. It accepts a mathematical specification and, optionally, a
+ hypothesis, and tries to prove the hypothesis and/or find a
+ saturation representing a (counter-)model for the specification.
+ .
+ E is based on a purely equational problem representation and
+ implements a variant of the superposition calculus. Proof search can
+ be guided with a multitude of options or a powerful automatic
+ configuration mode. The system can process input in a number of
+ different formats, including the standard TPTP-2 and TPTP-3
+ formats. It can generate proof objects in PCL2 or TPTP-3/TSTP
+ format.
+ .
+ E is considered one of the most powerful and friendly automated
+ theorem provers for first-order logic. It has consistently been among
+ the top system in the major categories of the CASC system competition,
+ and usually been the strongest free software system.
+
+Package: eprover-examples
+Architecture: all
+Depends: eprover, ${shlibs:Depends}, ${misc:Depends}
+Recommends:
+Suggests:
+Description: Theorem prover for first-order logic with equality - examples
+ E is a fully automatic theorem prover for full first-order logic with
+ equality. It accepts a mathematical specification and, optionally, a
+ hypothesis, and tries to prove the hypothesis and/or find a
+ saturation representing a (counter-)model for the specification.
+ .
+ E is based on a purely equational problem representation and
+ implements a variant of the superposition calculus. Proof search can
+ be guided with a multitude of options or a powerful automatic
+ configuration mode. The system can process input in a number of
+ different formats, including the standard TPTP-2 and TPTP-3
+ formats. It can generate proof objects in PCL2 or TPTP-3/TSTP
+ format.
+ .
+ E is considered one of the most powerful and friendly automated
+ theorem provers for first-order logic. It has consistently been among
+ the top system in the major categories of the CASC system competition,
+ and usually been the strongest free software system.
+ .
+ This package contains several sample inputs to try E on.
+
+Package: eprover-doc-html
+Architecture: all
+Depends: eprover, ${shlibs:Depends}, ${misc:Depends}
+Recommends:
+Suggests:
+Description: Theorem prover for first-order logic with equality - HTML doc
+ E is a fully automatic theorem prover for full first-order logic with
+ equality. It accepts a mathematical specification and, optionally, a
+ hypothesis, and tries to prove the hypothesis and/or find a
+ saturation representing a (counter-)model for the specification.
+ .
+ E is based on a purely equational problem representation and
+ implements a variant of the superposition calculus. Proof search can
+ be guided with a multitude of options or a powerful automatic
+ configuration mode. The system can process input in a number of
+ different formats, including the standard TPTP-2 and TPTP-3
+ formats. It can generate proof objects in PCL2 or TPTP-3/TSTP
+ format.
+ .
+ E is considered one of the most powerful and friendly automated
+ theorem provers for first-order logic. It has consistently been among
+ the top system in the major categories of the CASC system competition,
+ and usually been the strongest free software system.
+ .
+ This package contains E's documentation in HTML format.
--- eprover-1.0.004.orig/debian/changelog
+++ eprover-1.0.004/debian/changelog
@@ -0,0 +1,31 @@
+eprover (1.0.004-1ubuntu1) karmic; urgency=low
+
+  * debian/rules: fix FTBFS in all archs except i386.  (LP: #381092)
+    changed "build:" target as it makes build documentation for all archs.
+
+ -- Andrea Gasparini <gaspa@yattaweb.it>  Wed, 27 May 2009 22:48:37 +0200
+
+eprover (1.0.004-1) unstable; urgency=low
+
+  * Initial Debian release.
+    Closes: #516545
+  * Created man pages using help2man.
+  * Adjusted the Makefiles to
+    - install into $(DESTDIR) directory;
+    - to handle dependencies between source files in a more transparent and
+      efficient way - instead of generating Makefile.dependencies by the build
+      scripts, let 'make' generate .d file for each .c file as needed;
+    - not to modify source files in place - instead of modifying Makefile.vars,
+      put configuration into a new file Makefile.cfg;
+    - not to build development tools - the build scripts modify them in place
+      and they are not needed anyway for the package.
+  * Added 'test' target to Makefile to test that eprover binary was sucessfully
+    compiled and works on a sample problem.
+  * Added 'html' target to DOC/Makefile that builds HTML documentation using
+    tex4ht.
+  * Adjusted for the DebianScience GIT repository.
+  * Refined dependencies in debian/control, checked with pbuilder.
+  * Update 'clear' target in DOC/Makefile to clean some files left after
+    tex4ht.
+
+ -- Petr Pudlak <deb@pudlak.name>  Tue, 03 Mar 2009 15:03:06 +0100
--- eprover-1.0.004.orig/debian/eprover-doc-html.doc-base
+++ eprover-1.0.004/debian/eprover-doc-html.doc-base
@@ -0,0 +1,12 @@
+Document: eprover-doc-html
+Title: User Manual for E - the equational theorem prover
+Author: Stephan Schulz
+Abstract: E is an equational theorem prover for full clausal logic, based on
+ superposition and rewriting. In this very preliminary manual we first give a
+ short introduction for impatient new users, and then cover calculus, control,
+ options and input/output of the prover in some more detail.
+Section: Science/Mathematics
+
+Format: HTML
+Index: /usr/share/doc/eprover/html/eprover.html
+Files: /usr/share/doc/eprover/html/*.html /usr/share/doc/eprover/html/*.png /usr/share/doc/eprover/html/*.css
--- eprover-1.0.004.orig/debian/eprover-examples.install
+++ eprover-1.0.004/debian/eprover-examples.install
@@ -0,0 +1,2 @@
+EXAMPLE_PROBLEMS/LOP   usr/share/doc/eprover/examples
+EXAMPLE_PROBLEMS/TPTP  usr/share/doc/eprover/examples
--- eprover-1.0.004.orig/debian/eprover.help2man
+++ eprover-1.0.004/debian/eprover.help2man
@@ -0,0 +1,13 @@
+[NAME]
+E \- The Equational Theorem Prover User Manual
+
+/^ *$^ *$/m
+.SH COPYRIGHT
+
+[SEE ALSO]
+.BR eground (1),
+.BR epclextract (1),
+.br
+PDF manual 
+.IR /usr/share/doc/eprover/eprover.pdf.gz
+for a more detailed description.
--- eprover-1.0.004.orig/debian/eprover.manpages
+++ eprover-1.0.004/debian/eprover.manpages
@@ -0,0 +1,3 @@
+debian/eprover.1
+debian/epclextract.1
+debian/eground.1
--- eprover-1.0.004.orig/debian/eprover.links
+++ eprover-1.0.004/debian/eprover.links
@@ -0,0 +1 @@
+usr/share/man/man1/eprover.1.gz usr/share/man/man1/eproof.1.gz
--- eprover-1.0.004.orig/debian/compat
+++ eprover-1.0.004/debian/compat
@@ -0,0 +1 @@
+7
--- eprover-1.0.004.orig/debian/watch
+++ eprover-1.0.004/debian/watch
@@ -0,0 +1,10 @@
+version=3
+# This is a variant HTTP format which allows direct specification of
+# the homepage:
+# Homepage  Pattern  [Version  [Action]]
+#http://www.dataway.ch/~lukasl/amph/amph.html \
+# files/amphetamine-([\d\.]*).tar.bz2
+
+# http://www.eprover.org/ would need redirection
+http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html \
+    E_DOWNLOAD/V_(\d+)\.(\d+)-(\d+)/E.tgz
--- eprover-1.0.004.orig/debian/eprover.1
+++ eprover-1.0.004/debian/eprover.1
@@ -0,0 +1,832 @@
+.TH E "1" "February 2009" "E 1.0-004 Temi" "User Commands"
+.SH NAME
+E \- The Equational Theorem Prover User Manual
+.SH SYNOPSIS
+.B eprover
+[\fIoptions\fR] [\fIfiles\fR]
+.br
+.B eproof
+[\fIoptions\fR] [\fIfiles\fR]
+.SH DESCRIPTION
+E 1.0\-004 "Temi"
+.PP
+.I eprover
+reads a set of first\-order clauses and formulae and tries to refute it.
+.PP
+.I eproof
+is a wrapper script that calls
+.I eprover
+and then runs
+.I epclextract
+on its output to construct a proof.
+.HP
+\fB\-h\fR
+.HP
+\fB\-\-help\fR
+.IP
+Print a short description of program usage and options.
+.HP
+\fB\-V\fR
+.HP
+\fB\-\-version\fR
+.IP
+Print the version number of the prover. Please include this with all bug
+reports (if any).
+.HP
+\fB\-v\fR
+.HP
+\fB\-\-verbose[=\fR<arg>]
+.IP
+Verbose comments on the progress of the program. This differs from the
+output level (below) in that technical information is printed to stderr,
+while the output level determines which logical manipulations of the
+clauses are printed to stdout. The short form or the long form without
+the optional argument is equivalent to \fB\-\-verbose\fR=\fI1\fR.
+.HP
+\fB\-o\fR <arg>
+.HP
+\fB\-\-output\-file=\fR<arg>
+.IP
+Redirect output into the named file.
+.HP
+\fB\-s\fR
+.HP
+\fB\-\-silent\fR
+.IP
+Equivalent to \fB\-\-output\-level\fR=\fI0\fR.
+.HP
+\fB\-l\fR <arg>
+.HP
+\fB\-\-output\-level=\fR<arg>
+.IP
+Select an output level, greater values imply more verbose output. Level 0
+produces nearly no output, level 1 will output each clause as it is
+processed, level 2 will output generating inferences, level 3 will give a
+full protocol including rewrite steps and level 4 will include some
+internal clause renamings. Levels >= 2 also imply PCL2 or TSTP formats
+(which can be post\-processed with suitable tools).
+.HP
+\fB\-\-pcl\-terms\-compressed\fR
+.IP
+Print terms in the PCL output in shared representation.
+.HP
+\fB\-\-pcl\-compact\fR
+.IP
+Print PCL steps without additional spaces for formatting (safes disk
+space for large protocols).
+.HP
+\fB\-\-print\-statistics\fR
+.IP
+Print the inference statistics (only relevant for output level 0,
+otherwise they are printed automatically.
+.HP
+\fB\-\-print\-detailed\-statistics\fR
+.IP
+Print data about the proof state that is potentially expensive to
+collect. Includes number of term cells and number of rewrite steps.
+.HP
+\fB\-S\fR
+.HP
+\fB\-\-print\-saturated[=\fR<arg>]
+.IP
+Print the (semi\-) saturated clause sets after terminating the saturation
+process. The argument given describes which parts should be printed in
+which order. Legal characters are 'eigEIGaA', standing for processed
+positive units, processed negative units, processed non\-units,
+unprocessed positive units, unprocessed negative units, unprocessed
+non\-units, and two types of additional equality axioms, respectively.
+Equality axioms will only be printed if the original specification
+contained real equality. In this case, 'a' requests axioms in which a
+separate substitutivity axiom is given for each argument position of a
+function or predicate symbol, while 'A' requests a single substitutivity
+axiom (covering all positions) for each symbol. The short form or the
+long form without the optional argument is equivalent to
+\fB\-\-print\-saturated\fR=\fIeigEIG\fR.
+.HP
+\fB\-\-print\-sat\-info\fR
+.IP
+Print additional information (clause number, weight, etc) as a comment
+for clauses from the semi\-saturated end system.
+.HP
+\fB\-\-filter\-saturated[=\fR<arg>]
+.IP
+Filter the (semi\-) saturated clause sets after terminating the
+saturation process. The argument is a string describing which operations
+to take (and in which order). Options are 'u' (remove all clauses with
+more than one literal), 'c' (delete all but one copy of identical
+clauses, 'n', 'r', 'f' (forward contraction, unit\-subsumption only, no
+rewriting, rewriting with rules only, full rewriting, respectively), and
+\&'N', 'R' and 'F' (as their lower case counterparts, but with
+non\-unit\-subsumption enabled as well). The option without the optional
+argument is equivalent to \fB\-\-filter\-saturated\fR=\fIFc\fR.
+.HP
+\fB\-\-cnf\fR
+.IP
+Convert the input problem into clause normal form and print it. This is
+(nearly) equivalent to '\-\-print\-saturated=eigEIG
+\fB\-\-processed\-clauses\-limit\fR=\fI0\fR' and will by default perform some usually
+useful simplifications. You can additionally specify e.g.
+\&'\-\-no\-preprocessing' if you want just the result of CNF translation.
+.HP
+\fB\-\-print\-pid\fR
+.IP
+Print the process id of the prover as a comment after option processing.
+.HP
+\fB\-\-error\-on\-empty\fR
+.IP
+Return with an error code if the input file contains no clauses.
+Formally, the empty clause set (as an empty conjunction of clauses) is
+trivially satisfiable, and E will treat any empty input set as
+satisfiable. However, in composite systems this is more often a sign that
+something went wrong. Use this option to catch such bugs.
+.HP
+\fB\-m\fR <arg>
+.HP
+\fB\-\-memory\-limit=\fR<arg>
+.IP
+Limit the memory the prover may use. The argument is the allowed amount
+of memory in MB. If you use the argument 'Auto', the system will try to
+figure out the amount of physical memory of your machine and claim most
+of it. This option may not work everywhere, due to broken and/or strange
+behaviour of setrlimit() in some UNIX implementations, and due to the
+fact that I know of no portable way to figure out the physical memory in
+a machine. Both the option and the 'Auto' version do work under all
+tested versions of Solaris and GNU/Linux. Due to problems with limit
+datatypes, it is currently impossible to set a limit of more than 2 GB
+(2048 MB).
+.HP
+\fB\-\-cpu\-limit[=\fR<arg>]
+.IP
+Limit the cpu time the prover should run. The optional argument is the
+CPU time in seconds. The prover will terminate immediately after reaching
+the time limit, regardless of internal state. This option may not work
+everywhere, due to broken and/or strange behaviour of setrlimit() in some
+UNIX implementations. It does work under all tested versions of Solaris,
+HP\-UX, MacOS\-X, and GNU/Linux. As a side effect, this option will inhibit
+core file writing. Please note that if you use both \fB\-\-cpu\-limit\fR and
+\fB\-\-soft\-cpu\-limit\fR, the soft limit has to be smaller than the hard limit to
+have any effect.  The option without the optional argument is equivalent
+to \fB\-\-cpu\-limit\fR=\fI300\fR.
+.HP
+\fB\-\-soft\-cpu\-limit[=\fR<arg>]
+.IP
+Limit the cpu time the prover should spend in the main saturation phase.
+The prover will then terminate gracefully, i.e. it will perform
+post\-processing, filtering and printing of unprocessed clauses, if these
+options are selected. Note that for some filtering options (in particular
+those which perform full subsumption), the postprocessing time may well
+be larger than the saturation time. This option is particularly useful if
+you want to use E as a preprocessor or lemma generator in a larger
+system. The option without the optional argument is equivalent to
+\fB\-\-soft\-cpu\-limit\fR=\fI290\fR.
+.HP
+\fB\-R\fR
+.HP
+\fB\-\-resources\-info\fR
+.IP
+Give some information about the resources used by the prover. You will
+usually get CPU time information. On systems returning more information
+with the rusage() system call, you will also get information about memory
+consumption.
+.HP
+\fB\-C\fR <arg>
+.HP
+\fB\-\-processed\-clauses\-limit=\fR<arg>
+.IP
+Set the maximal number of clauses to process (i.e. the number of
+traversals of the main\-loop).
+.HP
+\fB\-P\fR <arg>
+.HP
+\fB\-\-processed\-set\-limit=\fR<arg>
+.IP
+Set the maximal size of the set of processed clauses. This differs from
+the previous option in that redundant and back\-simplified processed
+clauses are not counted.
+.HP
+\fB\-U\fR <arg>
+.HP
+\fB\-\-unprocessed\-limit=\fR<arg>
+.IP
+Set the maximal size of the set of unprocessed clauses. This is a
+termination condition, not something to use to control the deletion of
+bad clauses. Compare \fB\-\-delete\-bad\-limit\fR.
+.HP
+\fB\-T\fR <arg>
+.HP
+\fB\-\-total\-clause\-set\-limit=\fR<arg>
+.IP
+Set the maximal size of the set of all clauses. See previous option.
+.HP
+\fB\-n\fR
+.HP
+\fB\-\-eqn\-no\-infix\fR
+.IP
+In LOP, print equations in prefix notation equal(x,y).
+.HP
+\fB\-e\fR
+.HP
+\fB\-\-full\-equational\-rep\fR
+.IP
+In LOP. print all literals as equations, even non\-equational ones.
+.HP
+\fB\-\-tptp\-in\fR
+.IP
+Parse TPTP\-2 format instead of E\-LOP (but note that includes are handled
+according to TPTP\-3 semantics).
+.HP
+\fB\-\-tptp\-out\fR
+.IP
+Print TPTP format instead of E\-LOP. Implies \fB\-\-eqn\-no\-infix\fR and will
+ignore \fB\-\-full\-equational\-rep\fR.
+.HP
+\fB\-\-tptp\-format\fR
+.IP
+Equivalent to \fB\-\-tptp\-in\fR and \fB\-\-tptp\-out\fR.
+.HP
+\fB\-\-tptp2\-in\fR
+.IP
+Synonymous with \fB\-\-tptp\-in\fR.
+.HP
+\fB\-\-tptp2\-out\fR
+.IP
+Synonymous with \fB\-\-tptp\-out\fR.
+.HP
+\fB\-\-tptp2\-format\fR
+.IP
+Synonymous with \fB\-\-tptp\-format\fR.
+.HP
+\fB\-\-tstp\-in\fR
+.IP
+Parse TPTP\-3 format instead of E\-LOP (Note that TPTP\-3 syntax is still
+under development, and the version in E may not be fully conforming at
+all times. E works on all TPTP 3.0.1 input files (including includes).
+.HP
+\fB\-\-tstp\-out\fR
+.IP
+Print output clauses in TPTP\-3 syntax. In particular, for output levels
+>=2, write derivations as TPTP\-3 derivations (default is PCL).
+.HP
+\fB\-\-tstp\-format\fR
+.IP
+Equivalent to \fB\-\-tstp\-in\fR and \fB\-\-tstp\-out\fR.
+.HP
+\fB\-\-tptp3\-in\fR
+.IP
+Synonymous with \fB\-\-tstp\-in\fR.
+.HP
+\fB\-\-tptp3\-out\fR
+.IP
+Synonymous with \fB\-\-tstp\-out\fR.
+.HP
+\fB\-\-tptp3\-format\fR
+.IP
+Synonymous with \fB\-\-tstp\-format\fR.
+.HP
+\fB\-\-no\-preprocessing\fR
+.IP
+Do not perform preprocessing on the initial clause set. Preprocessing
+currently removes tautologies and orders terms, literals and clauses in a
+certain ("canonical") way before anything else happens. Unless the next
+option is set, it will also unfold equational definitions.
+.HP
+\fB\-\-no\-eq\-unfolding\fR
+.IP
+During preprocessing, abstain from unfolding (and removing) equational
+definitions.
+.HP
+\fB\-\-ac\-handling[=\fR<arg>]
+.IP
+Select AC handling mode. Preselected is 'DiscardAll', other options are
+\&'None' to disable AC handling, 'KeepUnits', and 'KeepOrientable'. The
+option without the optional argument is equivalent to
+\fB\-\-ac\-handling\fR=\fIKeepUnits\fR.
+.HP
+\fB\-\-ac\-non\-aggressive\fR
+.IP
+Do AC resolution on negative literals only on processing (by default, AC
+resolution is done after clause creation). Only effective if AC handling
+is not disabled.
+.HP
+\fB\-W\fR <arg>
+.HP
+\fB\-\-literal\-selection\-strategy=\fR<arg>
+.IP
+Choose a strategy for selection of negative literals. There are two
+special values for this option: NoSelection will select no literal (i.e.
+perform normal superposition) and NoGeneration will inhibit all
+generating inferences. For a list of the other (hopefully
+self\-documenting) values run 'eprover \fB\-W\fR none'. There are two variants of
+each strategy. The one prefixed with 'P' will allow paramodulation into
+maximal positive literals in addition to paramodulation into maximal
+selected negative literals.
+.HP
+\fB\-\-no\-generation\fR
+.IP
+Don't perform any generating inferences (equivalent to
+\fB\-\-literal\-selection\-strategy\fR=\fINoGeneration\fR).
+.HP
+\fB\-\-select\-on\-processing\-only\fR
+.IP
+Perform literal selection at processing time only (i.e. select only in
+the _given clause_), not before clause evaluation. This is relevant
+because many clause selection heuristics give special consideration to
+maximal or selected literals.
+.HP
+\fB\-i\fR
+.HP
+\fB\-\-inherit\-paramod\-literals\fR
+.IP
+Always select the negative literals a previous inference paramodulated
+into (if possible). If no such literal exists, select as dictated by the
+selection strategy.
+.HP
+\fB\-j\fR
+.HP
+\fB\-\-inherit\-goal\-pm\-literals\fR
+.IP
+In a goal (all negative clause), always select the negative literals a
+previous inference paramodulated into (if possible). If no such literal
+exists, select as dictated by the selection strategy.
+.HP
+\fB\-j\fR
+.HP
+\fB\-\-inherit\-conjecture\-pm\-literals\fR
+.IP
+In a conjecture\-derived clause), always select the negative literals a
+previous inference paramodulated into (if possible). If no such literal
+exists, select as dictated by the selection strategy.
+.HP
+\fB\-\-selection\-pos\-min=\fR<arg>
+.IP
+Set a lower limit for the number of positive literals a clause must have
+to be eligible for literal selection.
+.HP
+\fB\-\-selection\-pos\-max=\fR<arg>
+.IP
+Set a upper limit for the number of positive literals a clause can have
+to be eligible for literal selection.
+.HP
+\fB\-\-selection\-neg\-min=\fR<arg>
+.IP
+Set a lower limit for the number of negative literals a clause must have
+to be eligible for literal selection.
+.HP
+\fB\-\-selection\-neg\-max=\fR<arg>
+.IP
+Set a upper limit for the number of negative literals a clause can have
+to be eligible for literal selection.
+.HP
+\fB\-\-selection\-all\-min=\fR<arg>
+.IP
+Set a lower limit for the number of literals a clause must have to be
+eligible for literal selection.
+.HP
+\fB\-\-selection\-all\-max=\fR<arg>
+.IP
+Set an upper limit for the number of literals a clause must have to be
+eligible for literal selection.
+.HP
+\fB\-\-selection\-weight\-min=\fR<arg>
+.IP
+Set the minimum weight a clause must have to be eligible for literal
+selection.
+.HP
+\fB\-\-prefer\-initial\-clauses\fR
+.IP
+Always process all initial clauses first.
+.HP
+\fB\-x\fR <arg>
+.HP
+\fB\-\-expert\-heuristic=\fR<arg>
+.IP
+Select one of the clause selection heuristics. Currently at least
+available: Auto, Weight, StandardWeight, RWeight, FIFO, LIFO, Uniq,
+UseWatchlist. For a full list check HEURISTICS/che_proofcontrol.c. Auto
+is recommended if you only want to find a proof. It is special in that it
+will also set some additional options. To have optimal performance, you
+also should specify \fB\-tAuto\fR to select a good term ordering. LIFO is unfair
+and will make the prover incomplete. Uniq is used internally and is not
+very useful in most cases. You can define more heuristics using the
+option \fB\-H\fR (see below).
+.HP
+\fB\-\-filter\-limit[=\fR<arg>]
+.IP
+Set the limit on the number of 'storage units' in the proof state, after
+which the set of unprocessed clauses will be filtered against the
+processed clauses to eliminate redundant clauses. As of E 0.7, a 'storage
+unit' is approximately one byte, however, storage is estimated in an
+abstract way, independent of hardware or memory allocation library, and
+the storage estimate is only an approximation. The option without the
+optional argument is equivalent to \fB\-\-filter\-limit\fR=\fI1000000\fR.
+.HP
+\fB\-\-filter\-copies\-limit[=\fR<arg>]
+.IP
+Set the number of storage units in new unprocessed clauses after which
+the set of unprocessed clauses will be filtered for equivalent copies of
+clauses (see above). As this operation is cheaper, you may want to set
+this limit lower than \fB\-\-filter\-limit\fR. The option without the optional
+argument is equivalent to \fB\-\-filter\-copies\-limit\fR=\fI800000\fR.
+.HP
+\fB\-\-delete\-bad\-limit[=\fR<arg>]
+.IP
+Set the number of storage units after which bad clauses are deleted
+without further consideration. This causes the prover to be potentially
+incomplete, but will allow you to limit the maximum amount of memory used
+fairly well. The prover will tell you if a proof attempt failed due to
+the incompleteness introduced by this option. It is recommended to set
+this limit significantly higher than \fB\-\-filter\-limit\fR or
+\fB\-\-filter\-copies\-limit\fR. If you select \fB\-xAuto\fR and set a memory limit, the
+prover will determine a good value automatically. The option without the
+optional argument is equivalent to \fB\-\-delete\-bad\-limit\fR=\fI1500000\fR.
+.HP
+\fB\-\-assume\-completeness\fR
+.IP
+There are various way (e.g. the next few options) to configure the prover
+to be strongly incomplete in the general case. E will detect when such an
+option is selected and return corresponding exit states (i.e. it will not
+claim satisfiability just because it ran out of unprocessed clauses). If
+you _know_ that for your class of problems the selected strategy is still
+complete, use this option to tell the system that this is the case.
+.HP
+\fB\-\-disable\-eq\-factoring\fR
+.IP
+Disable equality factoring. This makes the prover incomplete for general
+non\-Horn problems, but helps for some specialized classes. It is not
+necessary to disable equality factoring for Horn problems, as Horn
+clauses are not factored anyways.
+.HP
+\fB\-\-disable\-paramod\-into\-neg\-units\fR
+.IP
+Disable paramodulation into negative unit clause. This makes the prover
+incomplete in the general case, but helps for some specialized classes.
+.HP
+\fB\-\-disable\-given\-clause\-fw\-contraction\fR
+.IP
+Disable simplification and subsumption of the newly selected given clause
+(clauses are still simplified when they are generated). In general, this
+breaks some basic assumptions of the DISCOUNT loop proof search
+procedure. However, there are some problem classes in which  this
+simplifications empirically never occurs. In such cases, we can save
+significant overhead. The option _should_ work in all cases, but is not
+expected to improve things in most cases.
+.HP
+\fB\-\-simul\-paramod\fR
+.IP
+Use simultaneous paramodulation to implement superposition. Default is to
+use plain paramodulation. This is an experimental feature.
+.HP
+\fB\-\-oriented\-simul\-paramod\fR
+.IP
+Use simultaneous paramodulation for oriented from\-literals. This is an
+experimental feature.
+.HP
+\fB\-\-split\-clauses[=\fR<arg>]
+.IP
+Determine which clauses should be subject to splitting. The argument is
+the binary 'OR' of values for the desired classes:
+.RS 8
+.TP
+1:
+Horn clauses
+.TP
+2:
+Non\-Horn clauses
+.TP
+4:
+Negative clauses
+.TP
+8:
+Positive clauses
+.TP
+16:
+Clauses with both positive and negative literals
+.RE
+.IP
+Each set bit adds that class to the set of clauses which will be split.
+The option without the optional argument is equivalent to
+\fB\-\-split\-clauses\fR=\fI7\fR.
+.HP
+\fB\-\-split\-method=\fR<arg>
+.IP
+Determine how to treat ground literals in splitting. The argument is
+either '0' to denote no splitting of ground literals (they are all
+assigned to the first split clause produced), '1' to denote that all
+ground literals should form a single new clause, or '2', in which case
+ground literals are treated as usual and are all split off into
+individual clauses.
+.HP
+\fB\-\-split\-aggressive\fR
+.IP
+Apply splitting to new clauses (after simplification) and before
+evaluation. By default, splitting (if activated) is only performed on
+selected clauses.
+.HP
+\fB\-\-split\-reuse\-defs\fR
+.IP
+If possible, reuse previous definitions for splitting.
+.HP
+\fB\-\-reweight\-limit[=\fR<arg>]
+.IP
+Set the number of new unprocessed clauses after which the set of
+unprocessed clauses will be reevaluated. The option without the optional
+argument is equivalent to \fB\-\-reweight\-limit\fR=\fI30000\fR.
+.HP
+\fB\-t\fR <arg>
+.HP
+\fB\-\-term\-ordering=\fR<arg>
+.IP
+Select an ordering type (currently Auto, LPO, LPO4, KBO or KBO1). \fB\-tAuto\fR
+is suggested, in particular with \fB\-xAuto\fR. KBO and KBO1 are different
+implementations of the same ordering, KBO is usually faster and has had
+more testing. Similarly, LPO4 is an new, equivalent but superior
+implementation of LPO.
+.HP
+\fB\-w\fR <arg>
+.HP
+\fB\-\-order\-weight\-generation=\fR<arg>
+.IP
+Select a method for the generation of weights for use with the term
+ordering. Run 'eprover \fB\-w\fR none' for a list of options.
+.HP
+\fB\-\-order\-weights=\fR<arg>
+.IP
+Describe a (partial) assignments of weights to function symbols for term
+orderings (in particular, KBO). You can specify a list of weights of the
+form 'f1:w1,f2:w2, ...'. Since a total weight assignment is needed, E
+will _first_ apply any weight generation scheme specified (or the default
+one), and then modify the weights as specified. Note that E performs only
+very basic sanity checks, so you probably can specify weights that break
+KBO constraints.
+.HP
+\fB\-G\fR <arg>
+.HP
+\fB\-\-order\-precedence\-generation=\fR<arg>
+.IP
+Select a method for the generation of a precedence for use with the term
+ordering. Run 'eprover \fB\-G\fR none' for a list of options.
+.HP
+\fB\-c\fR <arg>
+.HP
+\fB\-\-order\-constant\-weight=\fR<arg>
+.IP
+Set a special weight > 0 for constants in the term ordering. By default,
+constants are treated like other function symbols.
+.HP
+\fB\-\-precedence[=\fR<arg>]
+.IP
+Describe a (partial) precedence for the term ordering used for the proof
+attempt. You can specify a comma\-separated list of precedence chains,
+where a precedence chain is a list of function symbols (which all have to
+appear in the proof problem), connected by >, <, or =. If this option is
+used in connection with \fB\-\-order\-precedence\-generation\fR, the partial
+ordering will be completed using the selected method, otherwise the
+prover runs with a non\-ground\-total ordering. The option without the
+optional argument is equivalent to \fB\-\-precedence=\fR.
+.HP
+\fB\-\-lpo\-recursion\-limit[=\fR<arg>]
+.IP
+Set a depth limit for LPO comparisons. Most comparisons do not need more
+than 10 or 20 levels of recursion. By default, recursion depth is limited
+to 1000 to avoid stack overflow problems. If the limit is reached, the
+prover assumes that the terms are uncomparable. Smaller values make the
+comparison attempts faster, but less exact. Larger values have the
+opposite effect. Values up to 20000 should be save on most operating
+systems. If you run into segmentation faults while using LPO or LPO4,
+first try to set this limit to a reasonable value. If the problem
+persists, send a bug report ;\-) The option without the optional argument
+is equivalent to \fB\-\-lpo\-recursion\-limit\fR=\fI100\fR.
+.HP
+\fB\-\-restrict\-literal\-comparisons\fR
+.IP
+Make all literals uncomparable in the term ordering (i.e. do not use the
+term ordering to restrict paramodulation, equality resolution and
+factoring to certain literals. This is necessary to make
+Set\-of\-Support\-strategies complete for the non\-equational case (It still
+is incomplete for the equational case, but pretty useless anyways).
+.HP
+\fB\-\-sos\-uses\-input\-types\fR
+.IP
+If input is TPTP format, use TPTP conjectures for initializing the Set of
+Support. If not in TPTP format, use E\-LOP queries (clauses of the form
+?\-l(X),...,m(Y)). Normally, all negative clauses are used. Please note
+that most E heuristics do not use this information at all, it is
+currently only useful for certain parameter settings (including the
+SimulateSOS priority function).
+.HP
+\fB\-\-destructive\-er\fR
+.IP
+Allow destructive equality resolution inferences on pure\-variable
+literals of the form X!=Y, i.e. replace the original clause with the
+result of an equality resolution inference on this literal.
+.HP
+\fB\-\-strong\-destructive\-er\fR
+.IP
+Allow destructive equality resolution inferences on literals of the form
+X!=t (where X does not occur in t), i.e. replace the original clause with
+the result of an equality resolution inference on this literal. Unless I
+am brain\-dead, this maintains completeness, although the proof is rather
+tricky.
+.HP
+\fB\-\-destructive\-er\-aggressive\fR
+.IP
+Apply destructive equality resolution to all newly generated clauses, not
+just to selected clauses. Implies \fB\-\-destructive\-er\fR.
+.HP
+\fB\-\-forward\-context\-sr\fR
+.IP
+Apply contextual simplify\-reflect with processed clauses to the given
+clause.
+.HP
+\fB\-\-forward\-context\-sr\-aggressive\fR
+.IP
+Apply contextual simplify\-reflect with processed clauses to new clauses.
+Implies \fB\-\-forward\-context\-sr\fR.
+.HP
+\fB\-\-backward\-context\-sr\fR
+.IP
+Apply contextual simplify\-reflect with the given clause to processed
+clauses.
+.HP
+\fB\-g\fR
+.HP
+\fB\-\-prefer\-general\-demodulators\fR
+.IP
+Prefer general demodulators. By default, E prefers specialized
+demodulators. This affects in which order the rewrite  index is
+traversed.
+.HP
+\fB\-F\fR <arg>
+.HP
+\fB\-\-forward_demod_level=\fR<arg>
+.IP
+Set the desired level for rewriting of unprocessed clauses. A value of 0
+means no rewriting, 1 indicates to use rules (orientable equations) only,
+2 indicates full rewriting with rules and instances of unorientable
+equations. Default behavior is 2.
+.HP
+\fB\-\-strong\-rw\-inst\fR
+.IP
+Instantiate unbound variables in matching potential demodulators with a
+small constant terms.
+.HP
+\fB\-u\fR
+.HP
+\fB\-\-strong\-forward\-subsumption\fR
+.IP
+Try multiple positions and unit\-equations to try to equationally subsume
+a single new clause. Default is to search for a single position.
+.HP
+\fB\-\-watchlist[=\fR<arg>]
+.IP
+Give the name for a file containing clauses to be watched for during the
+saturation process. If a clause is generated that subsumes a watchlist
+clause, the subsumed clause is removed from the watchlist. The prover
+will terminate when the watchlist is empty. If you want to use the
+watchlist for guiding the proof, put the empty clause onto the list and
+use the built\-in clause selection heuristic 'UseWatchlist' (or build a
+heuristic yourself using the priority functions 'PreferWatchlist' and
+\&'DeferWatchlist'). Use the argument 'Use inline watchlist type' (or no
+argument) and the special clause type 'watchlist' if you want to put
+watchlist clauses into the normal input stream. This is only supported
+for TPTP input formats. The option without the optional argument is
+equivalent to \fB\-\-watchlist=\fR'Use inline watchlist type'.
+.HP
+\fB\-\-no\-watchlist\-simplification\fR
+.IP
+Normally, that watchlist is brought into normal form with respect to the
+current processed clause set and certain simplifications. This option
+disables this behaviour.
+.HP
+\fB\-\-conventional\-subsumption\fR
+.IP
+Equivalent to \fB\-\-subsumption\-indexing\fR=\fINone\fR.
+.HP
+\fB\-\-subsumption\-indexing=\fR<arg>
+.IP
+Determine choice of indexing for (most) subsumption operations. Choices
+are 'None' for naive subsumption, 'Direct' for direct mapped FV\-Indexing,
+\&'Perm' for permuted FV\-Indexing and 'PermOpt' for permuted FV\-Indexing
+with deletion of (suspected) non\-informative features. Default behaviour
+is 'Perm'.
+.HP
+\fB\-\-fvindex\-featuretypes=\fR<arg>
+.IP
+Select the feature types used for indexing. Choices are "None" to disable
+FV\-indexing, "AC" for AC compatible features (the default) (literal
+number and symbol counts), "SS" for set subsumption compatible features
+(symbol depth), and "All" for all features.Unless you want to measure the
+effects of the different features, I suggest you stick with the default.
+.HP
+\fB\-\-fvindex\-maxfeatures[=\fR<arg>]
+.IP
+Set the maximum initial number of symbols for feature computation.
+Depending on the feature selection, a value of X here will convert into
+2X+2 features (for set subsumption features), 2X+4 features (for
+AC\-compatible features) or 4X+6 features (if all features are used, the
+default). Note that the actually used set of features may be smaller than
+this if the signature does not contain enough symbols.For the Perm and
+PermOpt version, this is _also_ used to set the maximum depth of the
+feature vector index. Yes, I should probably make this into two separate
+options. If you select a small value here, you should probably not use
+"Direct" for the \fB\-\-subsumption\-indexing\fR option. The option without the
+optional argument is equivalent to \fB\-\-fvindex\-maxfeatures\fR=\fI200\fR.
+.HP
+\fB\-\-fvindex\-slack[=\fR<arg>]
+.IP
+Set the number of slots reserved in the index for function symbols that
+may be introduced into the signature later, e.g. by splitting. If no new
+symbols are introduced, this just wastes time and memory. If PermOpt is
+chosen, the slackness slots will be deleted from the index anyways, but
+will still waste (a little) time in computing feature vectors. The option
+without the optional argument is equivalent to \fB\-\-fvindex\-slack\fR=\fI0\fR.
+.HP
+\fB\-\-simplify\-with\-unprocessed\-units[=\fR<arg>]
+.IP
+Determine whether to use unprocessed unit clauses for simplify\-reflect
+(unit\-cutting) and unit subsumption. Possible values are 'NoSimplify' for
+strict DISCOUNT loop, 'TopSimplify' to use unprocessed units at the top
+level only, or 'FullSimplify' to use positive units even within
+equations. The option without the optional argument is equivalent to
+\fB\-\-simplify\-with\-unprocessed\-units\fR=\fITopSimplify\fR.
+.HP
+\fB\-D\fR <arg>
+.HP
+\fB\-\-define\-weight\-function=\fR<arg>
+.IP
+Define a weight function (see manual for details). Later definitions
+override previous definitions.
+.HP
+\fB\-H\fR <arg>
+.HP
+\fB\-\-define\-heuristic=\fR<arg>
+.IP
+Define a clause selection heuristic (see manual for details). Later
+definitions override previous definitions.
+.HP
+\fB\-\-free\-numbers\fR
+.IP
+Treat numbers (strings of decimal digits) as normal free function symbols
+in the input. By default, number now are supposed to denote domain
+constants and to be implicitly different from each other.
+.HP
+\fB\-\-free\-objects\fR
+.IP
+Treat object identifiers (strings in double quotes) as normal free
+function symbols in the input. By default, object identifiers now
+represent domain objects and are implicitly different from each other
+(and from numbers, unless those are declared to be free).
+.HP
+\fB\-\-definitional\-cnf[=\fR<arg>]
+.IP
+Use the new clausification algorithm that possibly introduces definitions
+for subformulas to avoid exponential blow\-up. This is now the default.
+The optional argument is a fudge factor that determines when a definition
+is introduced. 0 disables definitions, the default works well. The option
+without the optional argument is equivalent to \fB\-\-definitional\-cnf\fR=\fI24\fR.
+
+.SH AUTHOR
+Stephan Schulz <schulz@eprover.org>
+.SH COPYRIGHT
+Copyright 1998\-2006 by Stephan Schulz <schulz@eprover.org>
+.PP
+You can find the latest version of E and additional information at
+http://www.eprover.org
+.PP
+This program is free software; you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 2 of the License, or
+(at your option) any later version.
+.PP
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+.PP
+You should have received a copy of the GNU General Public License
+along with this program (it should be contained in the top level
+directory of the distribution in the file COPYING); if not, write to
+the Free Software Foundation, Inc., 59 Temple Place, Suite 330,
+Boston, MA  02111\-1307 USA
+.PP
+The original copyright holder can be contacted as
+.PP
+Stephan Schulz (I4)
+.br
+Technische Universitaet Muenchen
+.br
+Institut fuer Informatik
+.br
+Boltzmannstrasse 3
+.br
+85748 Garching bei Muenchen
+.br
+Germany
+
+.SH "SEE ALSO"
+.BR eground (1),
+.BR epclextract (1),
+.br
+PDF manual 
+.IR /usr/share/doc/eprover/eprover.pdf.gz
+for a more detailed description.
--- eprover-1.0.004.orig/debian/copyright
+++ eprover-1.0.004/debian/copyright
@@ -0,0 +1,29 @@
+This package was downloaded from http://www.eprover.org/
+
+Files: debian/*
+Author: Petr Pudlak <deb@pudlak.name>
+Copyright: Copyright  2009 Petr Pudlak <deb@pudlak.name>
+License: GPL-2+
+ The Debian packaging is licensed under the GPL, version 2 or later,
+ see below.
+
+Files: *
+Author: Stephan Schulz <schulz@eprover.org>
+Copyright: Copyright  2007-2008 Stephan Schulz <schulz@eprover.org>
+License: GPL-2+
+    This package is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This package is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this package; if not, write to the Free Software
+    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301 USA
+
+On Debian systems, the complete text of the GNU General
+Public License can be found in `/usr/share/common-licenses/GPL-2'.
--- eprover-1.0.004.orig/CLAUSES/Makefile
+++ eprover-1.0.004/CLAUSES/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -50,5 +48,4 @@
 $(LIB): $(CLAUSE_LIB)
 	$(AR) $(LIB) $(CLAUSE_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/ANALYSIS/Makefile
+++ eprover-1.0.004/ANALYSIS/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -39,7 +37,6 @@
 $(LIB): $(ANALYSIS_LIB)
 	$(AR) $(LIB) $(ANALYSIS_LIB)
 
-include Makefile.dependencies
 
 
 
--- eprover-1.0.004.orig/EXTERNAL/Makefile
+++ eprover-1.0.004/EXTERNAL/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -35,11 +33,10 @@
 include ../Makefile.services
 
 CSSCPA = CSSCPA_filter.o cex_csscpa.o \
-            ../lib/CLAUSES.a ../lib/ORDERINGS.a ../lib/TERMS.a\
-            ../lib/INOUT.a ../lib/BASICS.a
+            ../CLAUSES/CLAUSES.a ../ORDERINGS/ORDERINGS.a ../TERMS/TERMS.a\
+            ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 $(LIB): $(CSSCPA)
 	$(LD) -o CSSCPA_filter $(CSSCPA)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/ORDERINGS/Makefile
+++ eprover-1.0.004/ORDERINGS/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -39,7 +37,6 @@
 $(LIB): $(ORDER_LIB)
 	$(AR) $(LIB) $(ORDER_LIB)
 
-include Makefile.dependencies
 
 
 
--- eprover-1.0.004.orig/CONTROL/Makefile
+++ eprover-1.0.004/CONTROL/Makefile
@@ -20,8 +20,6 @@
 
 all: $(LIB)
 
-depend: *.c *.h
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -41,5 +39,4 @@
 $(LIB): $(CONTROL_LIB)
 	$(AR) $(LIB) $(CONTROL_LIB)
 
-include Makefile.dependencies
 
--- eprover-1.0.004.orig/SIMPLE_APPS/Makefile
+++ eprover-1.0.004/SIMPLE_APPS/Makefile
@@ -20,8 +20,6 @@
 LIB     = $(PROJECT)
 all: $(LIB)
 
-depend: *.c
-	$(MAKEDEPEND)
 
 # Remove all automatically generated files
 
@@ -35,16 +33,15 @@
 
 # Build the test programs
 
-TERM2DAG = term2dag.o ../lib/TERMS.a ../lib/INOUT.a ../lib/BASICS.a
+TERM2DAG = term2dag.o ../TERMS/TERMS.a ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 term2dag: $(TERM2DAG)
 	$(LD) -o term2dag $(TERM2DAG)
 
-EX_COMMANDLINE = ex_commandline.o ../lib/INOUT.a ../lib/BASICS.a
+EX_COMMANDLINE = ex_commandline.o ../INOUT/INOUT.a ../BASICS/BASICS.a
 
 ex_commandline: $(EX_COMMANDLINE)
 	$(LD) -o ex_commandline $(EX_COMMANDLINE)
 
-include Makefile.dependencies