--- ladr-0.0.200806a.orig/debian/changelog
+++ ladr-0.0.200806a/debian/changelog
@@ -0,0 +1,55 @@
+ladr (0.0.200806a-1) unstable; urgency=low
+
+  * New upstream release.
+  * debian/patches/01-libtoolise.dpatch: new source file weight2.c
+  * debian/libladr4.symbols: updated
+  * debian/control: new Standards-Version, updated for new prover9-doc
+  * debian/prooftrans.1: documented new tagged format
+
+ -- Peter Collingbourne <pcc03@doc.ic.ac.uk>  Sun, 29 Jun 2008 03:23:16 +0100
+
+ladr (0.0.200805a-1) unstable; urgency=low
+
+  * New upstream release.
+  * debian/libladr4.symbols: added new symbols
+  * debian/control
+    - updated for new prover9-doc
+    - added DM-Upload-Allowed: yes
+  * debian/copyright: give correct license information
+
+ -- Peter Collingbourne <pcc03@doc.ic.ac.uk>  Mon, 12 May 2008 18:07:55 +0100
+
+ladr (0.0.200804a-1) unstable; urgency=low
+
+  * New upstream release.
+  * debian/patches/01-libtoolise.dpatch: updated for new Makefiles
+  * debian/patches/02-shebangs.dpatch: deleted, applied upstream
+  * debian/ladr4-apps.install, debian/ladr4-apps.links, debian/ladr4-apps.docs:
+    added new application directproof
+  * debian/watch: added support for new version numbering scheme
+  * debian/interpformat.1, debian/prover9.1: replaced hyphens with minus
+    signs
+  * debian/libladr4.symbols: updated
+  * debian/control: updated for new prover9-doc
+  * debian/copyright: give correct license information
+
+ -- Peter Collingbourne <pcc03@doc.ic.ac.uk>  Tue, 08 Apr 2008 23:44:14 +0100
+
+ladr (0.0.200712-2) unstable; urgency=low
+
+  * debian/ladr4-apps.links: symlink usr/share/man/man1/prover9-mace4.1.gz
+    removed, as it does not refer to an installed application and conflicts
+    with the prover9-mace4 package
+
+ -- Peter Collingbourne <pcc03@doc.ic.ac.uk>  Sun, 10 Feb 2008 20:34:47 +0000
+
+ladr (0.0.200712-1) unstable; urgency=low
+
+  * Initial release (Closes: #437936)
+  * Fixed and libtoolized Makefiles
+  * Wrote man pages
+  * utilities/get_givens, utilities/get_interps, utilities/get_kept:
+    now use Bourne shell to avoid unneccessary dependencies
+
+ -- Peter Collingbourne <pcc03@doc.ic.ac.uk>  Tue, 22 Jan 2008 17:39:05 +0000
+
--- ladr-0.0.200806a.orig/debian/clausefilter.1
+++ ladr-0.0.200806a/debian/clausefilter.1
@@ -0,0 +1,43 @@
+.TH CLAUSEFILTER 1 "January 20, 2007"
+.SH NAME
+clausefilter - filter formulas with models
+.SH SYNOPSIS
+.B clausefilter
+.RI < interpretations-file >
+.RI < test >
+<
+.RI < formulas-file >
+>
+.RI < passing-formulas-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B clausefilter
+command.
+.PP
+Given a set of \fIinterpretations\fP, a \fItest\fP to perform, and a
+stream of \fIformulas\fP, \fBclausefilter\fP outputs the formulas
+that pass the test.
+.SH TESTS
+The following tests are available.
+.TP
+.B true_in_all
+Formula true in all interpretations.
+.TP
+.B true_in_some
+Formula true in some interpretation.
+.TP
+.B false_in_all
+Formula false in all interpretations.
+.TP
+.B false_in_some
+Formula false in some interpretation.
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBclausefilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBclausefilter\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/clausetester.1
+++ ladr-0.0.200806a/debian/clausetester.1
@@ -0,0 +1,29 @@
+.TH CLAUSETESTER 1 "January 20, 2007"
+.SH NAME
+clausetester - check formulas in models
+.SH SYNOPSIS
+.B clausetester
+.RI < interpretations-file >
+<
+.RI < formulas-file >
+>
+.RI < annotated-formulas-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B clausetester
+command.
+.PP
+This program takes a set of \fIinterpretations\fP and stream of
+\fIformulas\fP. For each formula, the interpretations in which the
+formula is true are shown, and at the end the number of formulas true
+in each interpretation is shown.
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBclausetester\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBclausetester\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/compat
+++ ladr-0.0.200806a/debian/compat
@@ -0,0 +1 @@
+5
--- ladr-0.0.200806a.orig/debian/control
+++ ladr-0.0.200806a/debian/control
@@ -0,0 +1,72 @@
+Source: ladr
+Priority: optional
+Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
+Build-Depends: debhelper (>= 5), libtool, dpatch
+Standards-Version: 3.8.0
+Section: math
+Vcs-Bzr: http://bzr.debian.org/collab-maint/ladr/unstable/
+DM-Upload-Allowed: yes
+Homepage: http://www.cs.unm.edu/~mccune/mace4/
+
+Package: libladr-dev
+Section: libdevel
+Architecture: any
+Depends: libladr4 (= ${binary:Version})
+Description: the LADR deduction library, development files
+ LADR (Library for Automated Deduction Research) is a library for
+ use in constructing theorem provers.  Among other useful routines it
+ provides facilities for applying inference rules such as resolution
+ and paramodulation to clauses.  LADR is used by the prover9 theorem
+ prover, and by the mace4 countermodel generator.
+ .
+ This package provides development support files for LADR.
+
+Package: libladr4
+Section: libs
+Architecture: any
+Depends: ${shlibs:Depends}
+Description: the LADR deduction library
+ LADR (Library for Automated Deduction Research) is a library for
+ use in constructing theorem provers.  Among other useful routines it
+ provides facilities for applying inference rules such as resolution
+ and paramodulation to clauses.  LADR is used by the prover9 theorem
+ prover, and by the mace4 countermodel generator.
+
+Package: prover9
+Section: math
+Architecture: any
+Depends: ${shlibs:Depends}
+Suggests: ladr4-apps (= ${binary:Version}), prover9-doc (>> 0.0.200806a), prover9-doc (<< 0.0.200806b)
+Description: theorem prover and countermodel generator
+ This package provides the Prover9 resolution/paramodulation theorem
+ prover and the Mace4 countermodel generator.
+ .
+ Prover9 is an automated theorem prover for first-order and equational
+ logic. It is a successor of the Otter prover.  Prover9 uses the
+ inference techniques of ordered resolution and paramodulation with
+ literal selection.
+ .
+ The program Mace4 searches for finite structures satisfying first-order
+ and equational statements, the same kind of statement that Prover9
+ accepts. If the statement is the denial of some conjecture, any
+ structures found by Mace4 are counterexamples to the conjecture.
+ .
+ Mace4 can be a valuable complement to Prover9, looking for
+ counterexamples before (or at the same time as) using Prover9 to search
+ for a proof. It can also be used to help debug input clauses and formulas
+ for Prover9.
+
+Package: ladr4-apps
+Section: math
+Architecture: any
+Depends: ${shlibs:Depends}, python
+Recommends: prover9-doc (>> 0.0.200806a), prover9-doc (<< 0.0.200806b)
+Description: the LADR deduction library, miscellaneous applications
+ LADR (Library for Automated Deduction Research) is a library for
+ use in constructing theorem provers.  Among other useful routines it
+ provides facilities for applying inference rules such as resolution
+ and paramodulation to clauses.  LADR is used by the prover9 theorem
+ prover, and by the mace4 countermodel generator.
+ .
+ This package provides miscellaneous LADR applications.
+
--- ladr-0.0.200806a.orig/debian/copyright
+++ ladr-0.0.200806a/debian/copyright
@@ -0,0 +1,51 @@
+This package was debianized by Peter Collingbourne <pcc03@doc.ic.ac.uk> on
+Sat, 11 Aug 2007 23:22:34 +0100.
+
+It was downloaded from <http://www.cs.unm.edu/~mccune/mace4/download/>
+
+Upstream Authors: 
+
+    William McCune <mccune@cs.unm.edu>
+    David A. Wheeler <dwheeler@dwheeler.com>
+
+Copyright: 
+
+    utilities/gvizify: Copyright (C) 2007 David A. Wheeler
+    Other files: Copyright (C) 2006, 2007 William McCune
+
+License for utilities/gvizify:
+
+    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.
+
+    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.
+
+    You should have received a copy of the GNU General Public License
+    along with this program; if not, write to the Free Software
+    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+
+License for all other files:
+
+    The LADR Deduction Library is free software; you can redistribute it
+    and/or modify it under the terms of the GNU General Public License,
+    version 2.
+
+    The LADR Deduction Library 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 the LADR Deduction Library; 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, version 2 can be found in `/usr/share/common-licenses/GPL-2'.
+
+The Debian packaging is (C) 2008, Peter Collingbourne <pcc03@doc.ic.ac.uk> and
+is licensed under the GPL, see `/usr/share/common-licenses/GPL'.
--- ladr-0.0.200806a.orig/debian/dirs
+++ ladr-0.0.200806a/debian/dirs
@@ -0,0 +1,2 @@
+usr/bin
+usr/sbin
--- ladr-0.0.200806a.orig/debian/interpfilter.1
+++ ladr-0.0.200806a/debian/interpfilter.1
@@ -0,0 +1,43 @@
+.TH INTERPFILTER 1 "January 20, 2007"
+.SH NAME
+interpfilter - filter models with formulas
+.SH SYNOPSIS
+.B interpfilter
+.RI < formulas-file >
+.RI < test >
+<
+.RI < interpretations-file >
+>
+.RI < passing-interpretations-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B interpfilter
+command.
+.PP
+Given a set of \fIformulas\fP, a \fItest\fP to perform, and a
+stream of \fIinterpretations\fP, \fBinterpfilter\fP outputs the interpretations
+that pass the test.
+.SH TESTS
+The following tests are available.
+.TP
+.B all_true
+All formulas true in given interpretation.
+.TP
+.B some_true
+Some formula true in given interpretation.
+.TP
+.B all_false
+All formulas false in given interpretation.
+.TP
+.B some_false
+Some formula false in given interpretation.
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBinterpfilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBinterpfilter\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/interpformat.1
+++ ladr-0.0.200806a/debian/interpformat.1
@@ -0,0 +1,65 @@
+.TH INTERPFORMAT 1 "January 20, 2007"
+.SH NAME
+interpformat \- tool for transforming
+.BR mace4 (1)
+models
+.SH SYNOPSIS
+.B interpformat
+.RI [ options ]
+.RI < transformation >
+\-f
+.I input-file
+>
+.I output-file
+.br
+.B interpformat
+.RI [ options ]
+.RI < transformation >
+<
+.I input-file
+>
+.I output-file
+.SH DESCRIPTION
+The models (structures) in
+.BR mace4 (1)
+output files can be transformed in various ways with the program \fBinterpformat\fP.
+.SH TRANSFORMATIONS
+The transformations are listed here.
+.TP
+.B standard
+one line per operation
+.TP
+.B standard2
+standard, with binary operations in a square (default)
+.TP
+.B portable
+list of lists, suitable for parsing by Python, GAP, etc.
+.TP
+.B tabular
+as nice tables
+.TP
+.B raw
+similar to standard, but without punctuation
+.TP
+.B cooked
+as terms, e.g., f(0,1)=2
+.TP
+.B tex
+formatted for LaTeX
+.TP
+.B xml
+XML
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B output \fI<operations>
+Output only the listed \fIoperations\fP.
+.SH SEE ALSO
+.BR mace4 (1).
+.br
+Full documentation for \fBinterpformat\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBinterpformat\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/isofilter.1
+++ ladr-0.0.200806a/debian/isofilter.1
@@ -0,0 +1,65 @@
+.TH ISOFILTER 1 "January 20, 2007"
+.SH NAME
+isofilter - removes isomorphic structures from
+.BR mace4 (1)
+models
+.SH SYNOPSIS
+.B isofilter
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.br
+.B isofilter0
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.br
+.B isofilter2
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.SH DESCRIPTION
+This manual page documents briefly the \fBisofilter\fP, \fBisofilter0\fP and \fBisofilter2\fP commands.
+.PP
+If
+.BR mace4 (1)
+produces more than one structure, some of them are very likely to be
+isomorphic to others. The program \fBisofilter\fP can be used to remove isomorphic
+structures.
+.SH ALGORITHM
+There are multiple \fBisofilter\fP variants providing alternative algorithms.
+.TP
+.B isofilter
+Uses Occurrence Profiles algorithm.
+.TP
+.B isofilter2
+Uses Canonical Forms algorithm.
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B ignore_constants
+Ignore all constants during the isomorphism tests.
+.TP
+.B check \fI<operations>
+Consider only the listed \fIoperations\fP in the isomorphism tests.
+.TP
+.B output \fI<operations>
+Output only the listed \fIoperations\fP.
+.TP
+.B wrap
+Enclose the resulting structures in \fBlist(interpretations). ... end_of_list.\fP
+.SH SEE ALSO
+.BR mace4 (1).
+.br
+Full documentation for \fBisofilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBisofilter\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/ladr4-apps.1
+++ ladr-0.0.200806a/debian/ladr4-apps.1
@@ -0,0 +1,16 @@
+.TH LADR4-APPS 1 "August 12, 2007"
+.SH NAME
+ladr4-apps \- undocumented LADR4 applications
+.SH DESCRIPTION
+Some programs in the \fBladr4-apps\fP package currently have no manual
+pages.  You can obtain documentation on some of these applications via the
+\fBprover9\fP manual, which is available on Debian systems via the package
+\fIprover9-doc\fP, at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+Alternatively invoking the application with the \fB-help\fP option may
+produce documentation.  Patches to add manual pages are welcome, and may
+be sent to the Debian package maintainer, whose details are listed below.
+.SH AUTHOR
+The applications were written by William McCune <mccune@cs.unm.edu>.
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/ladr4-apps.README.Debian
+++ ladr-0.0.200806a/debian/ladr4-apps.README.Debian
@@ -0,0 +1,9 @@
+ladr4-apps for Debian
+---------------------
+
+Some of these applications do not yet have man pages.  You can obtain
+basic help for them using the -help flag, or by consulting the manual,
+which is available in the prover9-doc package in HTML format, at
+/usr/share/doc/prover9-doc/manual/index.html
+
+ -- Peter Collingbourne <pcc03@doc.ic.ac.uk>  Sun, 20 Jan 2008 20:47:42 +0000
--- ladr-0.0.200806a.orig/debian/ladr4-apps.dirs
+++ ladr-0.0.200806a/debian/ladr4-apps.dirs
@@ -0,0 +1 @@
+usr/bin
--- ladr-0.0.200806a.orig/debian/ladr4-apps.docs
+++ ladr-0.0.200806a/debian/ladr4-apps.docs
@@ -0,0 +1 @@
+apps.src/README.directproof
--- ladr-0.0.200806a.orig/debian/ladr4-apps.install
+++ ladr-0.0.200806a/debian/ladr4-apps.install
@@ -0,0 +1,28 @@
+bin/attack usr/bin
+bin/autosketches4 usr/bin
+bin/clausefilter usr/bin
+bin/clausetester usr/bin
+bin/directproof usr/bin
+bin/dprofiles usr/bin
+bin/fof-prover9 usr/bin
+bin/get_givens usr/bin
+bin/get_interps usr/bin
+bin/get_kept usr/bin
+bin/gvizify usr/bin
+bin/idfilter usr/bin
+bin/interpfilter usr/bin
+bin/ladr_to_tptp usr/bin
+bin/latfilter usr/bin
+bin/looper usr/bin
+bin/miniscope usr/bin
+bin/mirror-flip usr/bin
+bin/newauto usr/bin
+bin/newsax usr/bin
+bin/olfilter usr/bin
+bin/perm3 usr/bin
+bin/renamer usr/bin
+bin/rewriter usr/bin
+bin/sigtest usr/bin
+bin/tptp_to_ladr usr/bin
+bin/unfast usr/bin
+bin/upper-covers usr/bin
--- ladr-0.0.200806a.orig/debian/ladr4-apps.links
+++ ladr-0.0.200806a/debian/ladr4-apps.links
@@ -0,0 +1,24 @@
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/attack.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/autosketches4.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/directproof.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/dprofiles.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/fof-prover9.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/get_givens.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/get_interps.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/get_kept.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/gvizify.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/idfilter.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/ladr_to_tptp.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/latfilter.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/looper.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/miniscope.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/mirror-flip.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/newauto.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/newsax.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/olfilter.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/perm3.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/renamer.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/sigtest.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/tptp_to_ladr.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/unfast.1.gz
+usr/share/man/man1/ladr4-apps.1.gz usr/share/man/man1/upper-covers.1.gz
--- ladr-0.0.200806a.orig/debian/ladr4-apps.manpages
+++ ladr-0.0.200806a/debian/ladr4-apps.manpages
@@ -0,0 +1,5 @@
+debian/ladr4-apps.1
+debian/clausefilter.1
+debian/clausetester.1
+debian/interpfilter.1
+debian/rewriter.1
--- ladr-0.0.200806a.orig/debian/libladr-dev.dirs
+++ ladr-0.0.200806a/debian/libladr-dev.dirs
@@ -0,0 +1,2 @@
+usr/lib
+usr/include/ladr
--- ladr-0.0.200806a.orig/debian/libladr-dev.docs
+++ ladr-0.0.200806a/debian/libladr-dev.docs
@@ -0,0 +1 @@
+ladr/html
--- ladr-0.0.200806a.orig/debian/libladr-dev.install
+++ ladr-0.0.200806a/debian/libladr-dev.install
@@ -0,0 +1,4 @@
+ladr/*.h usr/include/ladr
+debian/tmp/usr/lib/lib*.a usr/lib
+debian/tmp/usr/lib/lib*.so usr/lib
+debian/tmp/usr/lib/*.la usr/lib
--- ladr-0.0.200806a.orig/debian/libladr4.dirs
+++ ladr-0.0.200806a/debian/libladr4.dirs
@@ -0,0 +1 @@
+usr/lib
--- ladr-0.0.200806a.orig/debian/libladr4.install
+++ ladr-0.0.200806a/debian/libladr4.install
@@ -0,0 +1 @@
+debian/tmp/usr/lib/lib*.so.* usr/lib
--- ladr-0.0.200806a.orig/debian/libladr4.symbols
+++ ladr-0.0.200806a/debian/libladr4.symbols
@@ -0,0 +1,1239 @@
+libladr.so.4 libladr4 #MINVER#
+ Maximal_flag@Base 0.0.200712
+ Maximal_signed_flag@Base 0.0.200712
+ Ordering_method@Base 0.0.200712
+ Oriented_flag@Base 0.0.200712
+ Renamable_flip_flag@Base 0.0.200712
+ Selected_flag@Base 0.0.200712
+ absolute_wallclock@Base 0.0.200712
+ ac_canonical@Base 0.0.200712
+ accept_list@Base 0.0.200712
+ add_new_symbols@Base 0.0.200712
+ add_skolems_to_preliminary_precedence@Base 0.0.200712
+ adjust_weight_with_hints@Base 0.0.200712
+ alist2_insert@Base 0.0.200712
+ alist2_remove@Base 0.0.200712
+ alist_insert@Base 0.0.200712
+ all_args_vars@Base 0.0.200712
+ all_clauses_horn@Base 0.0.200712
+ all_clauses_positive@Base 0.0.200712
+ all_clauses_unit@Base 0.0.200712
+ all_function_symbols@Base 0.0.200712
+ all_relation_symbols@Base 0.0.200712
+ all_sym@Base 0.0.200712
+ all_symbols_lrpo_status@Base 0.0.200712
+ and@Base 0.0.200712
+ and_sym@Base 0.0.200712
+ any_clause@Base 0.0.200712
+ append_clash@Base 0.0.200712
+ append_just@Base 0.0.200712
+ append_label_attribute@Base 0.0.200712
+ append_literal@Base 0.0.200712
+ apply@Base 0.0.200712
+ apply_basic@Base 0.0.200712
+ apply_basic_substitute@Base 0.0.200712
+ apply_lit@Base 0.0.200712
+ apply_substitute2@Base 0.0.200804a
+ apply_substitute@Base 0.0.200712
+ arg_position@Base 0.0.200712
+ args_distinct_vars@Base 0.0.200712
+ arity_check@Base 0.0.200712
+ assign_clause_id@Base 0.0.200712
+ assign_discriminator_counts@Base 0.0.200712
+ assign_greatest_precedence@Base 0.0.200712
+ assign_order_method@Base 0.0.200712
+ assign_parm@Base 0.0.200712
+ assign_stringparm@Base 0.0.200712
+ assoc2a@Base 0.0.200712
+ assoc2b@Base 0.0.200712
+ assoc@Base 0.0.200712
+ assoc_comm_symbols@Base 0.0.200712
+ associativity3@Base 0.0.200712
+ associativity4@Base 0.0.200712
+ associativity@Base 0.0.200712
+ at_parm_limit@Base 0.0.200712
+ atom_number@Base 0.0.200712
+ atom_to_literal@Base 0.0.200712
+ attrib_sym@Base 0.0.200712
+ attribute_name_to_id@Base 0.0.200712
+ attributes_contain_variables@Base 0.0.200712
+ attributes_to_term@Base 0.0.200712
+ avl_check@Base 0.0.200712
+ avl_delete@Base 0.0.200712
+ avl_find@Base 0.0.200712
+ avl_height@Base 0.0.200712
+ avl_insert@Base 0.0.200712
+ avl_item_at_position@Base 0.0.200712
+ avl_largest@Base 0.0.200712
+ avl_nth_item@Base 0.0.200712
+ avl_place@Base 0.0.200712
+ avl_position@Base 0.0.200712
+ avl_size@Base 0.0.200712
+ avl_smallest@Base 0.0.200712
+ avl_zap@Base 0.0.200712
+ back_demod_hints@Base 0.0.200712
+ back_demod_indexed@Base 0.0.200712
+ back_demod_just@Base 0.0.200712
+ back_demod_linear@Base 0.0.200712
+ back_feature_subsume@Base 0.0.200712
+ back_subsume@Base 0.0.200712
+ back_subsume_one@Base 0.0.200712
+ back_unit_del_by_index@Base 0.0.200712
+ back_unit_deletion_just@Base 0.0.200712
+ basic_paramod@Base 0.0.200712
+ basic_paramodulation_prunes@Base 0.0.200712
+ basic_term@Base 0.0.200712
+ bell@Base 0.0.200712
+ biggest_variable@Base 0.0.200712
+ binary_factors@Base 0.0.200712
+ binary_parse_type@Base 0.0.200712
+ binary_res_just@Base 0.0.200712
+ binary_res_just_by_id@Base 0.0.200712
+ binary_resolution@Base 0.0.200712
+ build_attr_term@Base 0.0.200712
+ build_binary_term@Base 0.0.200712
+ build_binary_term_safe@Base 0.0.200712
+ build_reflex_eq@Base 0.0.200712
+ build_unary_term@Base 0.0.200712
+ build_unary_term_safe@Base 0.0.200712
+ bytes_palloced@Base 0.0.200712
+ c_associativity@Base 0.0.200712
+ cac_redundancy@Base 0.0.200712
+ cac_tautology@Base 0.0.200712
+ call_weight@Base 0.0.200806a
+ canon_interp@Base 0.0.200712
+ cat_att@Base 0.0.200712
+ check_ac_canonical@Base 0.0.200712
+ check_ibuf_clause@Base 0.0.200712
+ check_parents_and_uplinks_in_proof@Base 0.0.200712
+ check_upward_clause_links@Base 0.0.200712
+ check_upward_term_links@Base 0.0.200712
+ cl_id_compare@Base 0.0.200804a
+ cl_wt_id_compare@Base 0.0.200804a
+ claim_term_flag@Base 0.0.200712
+ clash@Base 0.0.200712
+ clausal_formula@Base 0.0.200712
+ clause_depth@Base 0.0.200712
+ clause_ident@Base 0.0.200712
+ clause_ids_assigned@Base 0.0.200712
+ clause_level@Base 0.0.200712
+ clause_member_plist@Base 0.0.200712
+ clause_plist_member@Base 0.0.200712
+ clause_reader@Base 0.0.200712
+ clause_set_variables@Base 0.0.200712
+ clause_symbol_count@Base 0.0.200712
+ clause_to_formula@Base 0.0.200712
+ clause_weight@Base 0.0.200712
+ clause_writer@Base 0.0.200712
+ clauses_in_clist@Base 0.0.200712
+ clausify_formula@Base 0.0.200712
+ clausify_just@Base 0.0.200712
+ clausify_prepare@Base 0.0.200712
+ clear_all_nonbasic_marks@Base 0.0.200712
+ clear_flag@Base 0.0.200712
+ clear_parse_type@Base 0.0.200712
+ clear_parse_type_for_all_symbols@Base 0.0.200712
+ clist_append@Base 0.0.200712
+ clist_append_all@Base 0.0.200712
+ clist_append_plist@Base 0.0.200712
+ clist_check@Base 0.0.200712
+ clist_copy@Base 0.0.200712
+ clist_empty@Base 0.0.200712
+ clist_free@Base 0.0.200712
+ clist_init@Base 0.0.200712
+ clist_insert_after@Base 0.0.200712
+ clist_insert_before@Base 0.0.200712
+ clist_length@Base 0.0.200712
+ clist_member@Base 0.0.200712
+ clist_move_clauses@Base 0.0.200712
+ clist_number_of_weight@Base 0.0.200712
+ clist_prepend@Base 0.0.200712
+ clist_remove@Base 0.0.200712
+ clist_remove_all@Base 0.0.200712
+ clist_remove_all_clauses@Base 0.0.200712
+ clist_reverse@Base 0.0.200712
+ clist_swap@Base 0.0.200712
+ clist_zap@Base 0.0.200712
+ clock_init@Base 0.0.200712
+ clock_milliseconds@Base 0.0.200712
+ clock_reset@Base 0.0.200712
+ clock_running@Base 0.0.200712
+ clock_seconds@Base 0.0.200712
+ clock_start@Base 0.0.200712
+ clock_stop@Base 0.0.200712
+ clocks_enabled@Base 0.0.200712
+ clocks_id@Base 0.0.200712
+ closed_formula@Base 0.0.200712
+ cnf@Base 0.0.200712
+ cnf_max_clauses@Base 0.0.200712
+ comm_symbols@Base 0.0.200712
+ commutativity@Base 0.0.200712
+ compare_interp@Base 0.0.200712
+ compare_vecs@Base 0.0.200712
+ compile_clause_eval_rule@Base 0.0.200804a
+ compile_interp@Base 0.0.200712
+ compress_clause@Base 0.0.200712
+ compress_term@Base 0.0.200712
+ cons_term@Base 0.0.200712
+ constants_in_clause@Base 0.0.200712
+ constants_in_formula@Base 0.0.200712
+ constants_in_term@Base 0.0.200712
+ contains_eq@Base 0.0.200712
+ contains_pos_eq@Base 0.0.200712
+ contains_skolem_function@Base 0.0.200712
+ contains_skolem_term@Base 0.0.200712
+ context_to_pairs@Base 0.0.200712
+ copy_and_renumber_proof@Base 0.0.200712
+ copy_attributes@Base 0.0.200712
+ copy_clause@Base 0.0.200712
+ copy_clause_ija@Base 0.0.200712
+ copy_clause_with_flag@Base 0.0.200712
+ copy_clause_with_flags@Base 0.0.200712
+ copy_clauses_ija@Base 0.0.200712
+ copy_clauses_to_clist@Base 0.0.200712
+ copy_clist_to_plist_shallow@Base 0.0.200712
+ copy_flatterm@Base 0.0.200712
+ copy_i3list@Base 0.0.200712
+ copy_ilist@Base 0.0.200712
+ copy_inference@Base 0.0.200712
+ copy_int_attribute@Base 0.0.200712
+ copy_interp@Base 0.0.200712
+ copy_just@Base 0.0.200712
+ copy_justification@Base 0.0.200712
+ copy_literal@Base 0.0.200712
+ copy_literals@Base 0.0.200712
+ copy_literals_with_flag@Base 0.0.200712
+ copy_literals_with_flags@Base 0.0.200712
+ copy_plist@Base 0.0.200712
+ copy_plist_of_formulas@Base 0.0.200712
+ copy_plist_of_terms@Base 0.0.200712
+ copy_selected_literal_marks@Base 0.0.200712
+ copy_string_attribute@Base 0.0.200712
+ copy_term@Base 0.0.200712
+ copy_term_attribute@Base 0.0.200712
+ copy_term_with_flag@Base 0.0.200712
+ copy_term_with_flags@Base 0.0.200712
+ copy_vec@Base 0.0.200712
+ create_profile@Base 0.0.200712
+ current_fsym_precedence@Base 0.0.200712
+ current_rsym_precedence@Base 0.0.200712
+ declare_base_symbols@Base 0.0.200712
+ declare_functions_and_relations@Base 0.0.200712
+ declare_parse_type@Base 0.0.200712
+ declare_quantifier_precedence@Base 0.0.200712
+ declare_standard_parse_types@Base 0.0.200712
+ declare_term_attribute_inheritable@Base 0.0.200712
+ declare_tptp_parse_types@Base 0.0.200712
+ decommission_skolem_symbols@Base 0.0.200712
+ definite_clause@Base 0.0.200712
+ delete_attributes@Base 0.0.200712
+ delete_clause@Base 0.0.200712
+ delete_clauses@Base 0.0.200712
+ delete_clist@Base 0.0.200712
+ delete_pair_index@Base 0.0.200712
+ demod1@Base 0.0.200712
+ demod_attempts@Base 0.0.200712
+ demod_just@Base 0.0.200712
+ demod_rewrites@Base 0.0.200712
+ demodulate@Base 0.0.200712
+ demodulator_type@Base 0.0.200712
+ deny_just@Base 0.0.200712
+ destroy_discrim_tree@Base 0.0.200712
+ di_tree_delete@Base 0.0.200712
+ di_tree_insert@Base 0.0.200712
+ dio@Base 0.0.200712
+ disable_clocks@Base 0.0.200712
+ disable_max_megs@Base 0.0.200712
+ disable_option_dependencies@Base 0.0.200712
+ discrim_bind_cancel@Base 0.0.200712
+ discrim_bind_retrieve_first@Base 0.0.200712
+ discrim_bind_retrieve_next@Base 0.0.200712
+ discrim_bind_update@Base 0.0.200712
+ discrim_dealloc@Base 0.0.200712
+ discrim_empty@Base 0.0.200712
+ discrim_flat_cancel@Base 0.0.200712
+ discrim_flat_retrieve_first@Base 0.0.200712
+ discrim_flat_retrieve_leaf@Base 0.0.200712
+ discrim_flat_retrieve_next@Base 0.0.200712
+ discrim_init@Base 0.0.200712
+ discrim_wild_cancel@Base 0.0.200712
+ discrim_wild_retrieve_first@Base 0.0.200712
+ discrim_wild_retrieve_next@Base 0.0.200712
+ discrim_wild_update@Base 0.0.200712
+ dnf@Base 0.0.200712
+ done_with_hints@Base 0.0.200712
+ dual@Base 0.0.200712
+ dual_type@Base 0.0.200712
+ eliminate_rebinding@Base 0.0.200712
+ embed_formulas_in_topforms@Base 0.0.200712
+ empty_substitution@Base 0.0.200712
+ enable_clocks@Base 0.0.200712
+ enable_max_megs@Base 0.0.200712
+ enable_option_dependencies@Base 0.0.200712
+ end_of_commands_term@Base 0.0.200712
+ end_of_list_clause@Base 0.0.200712
+ end_of_list_formula@Base 0.0.200712
+ end_of_list_term@Base 0.0.200712
+ eq_removable_literal@Base 0.0.200712
+ eq_sym@Base 0.0.200712
+ eq_tautology@Base 0.0.200712
+ eq_term@Base 0.0.200712
+ equality_in_clauses@Base 0.0.200712
+ equality_in_clist@Base 0.0.200712
+ equational_def@Base 0.0.200712
+ equational_def_2@Base 0.0.200712
+ eval_clause_in_rule@Base 0.0.200804a
+ eval_formula@Base 0.0.200712
+ eval_literals@Base 0.0.200712
+ eval_literals_false_instances@Base 0.0.200712
+ eval_literals_true_instances@Base 0.0.200712
+ eval_term_ground@Base 0.0.200712
+ eval_topform@Base 0.0.200712
+ evaluable_atom@Base 0.0.200804a
+#MISSING: 0.0.200804a# evaluable_clause@Base 0.0.200712
+ evaluable_formula@Base 0.0.200804a
+ evaluable_literals@Base 0.0.200804a
+ evaluable_term@Base 0.0.200712
+ evaluable_topform@Base 0.0.200804a
+ exists_attribute@Base 0.0.200712
+ exists_preliminary_precedence@Base 0.0.200712
+ exists_selected_literal@Base 0.0.200712
+ exists_sym@Base 0.0.200712
+ expand_def_just@Base 0.0.200712
+ expand_proof@Base 0.0.200712
+ expand_proof_ivy@Base 0.0.200712
+ expand_with_definition@Base 0.0.200712
+ expand_with_definitions@Base 0.0.200712
+ f_clause@Base 0.0.200712
+ f_clauses@Base 0.0.200712
+ factor_just@Base 0.0.200712
+ factorial@Base 0.0.200712
+ false_sym@Base 0.0.200712
+ false_term@Base 0.0.200712
+ fapply_demod@Base 0.0.200712
+ fast_fwrite_clause@Base 0.0.200712
+ fast_fwrite_term_nl@Base 0.0.200712
+ fast_read_clause@Base 0.0.200712
+ fast_read_term@Base 0.0.200712
+ fast_set_defaults@Base 0.0.200712
+ fast_set_symbol@Base 0.0.200712
+ fatal_error@Base 0.0.200712
+ fd_read_to_ibuf@Base 0.0.200712
+ fdemod_attempts@Base 0.0.200712
+ fdemod_clause@Base 0.0.200712
+ fdemod_rewrites@Base 0.0.200712
+ fdemodulate@Base 0.0.200712
+ feature_length@Base 0.0.200712
+ features@Base 0.0.200712
+ features_less_or_equal@Base 0.0.200712
+ find_clause_by_id@Base 0.0.200712
+ first_fpos@Base 0.0.200712
+ first_literal_of_sign@Base 0.0.200712
+ first_negative_parent@Base 0.0.200712
+ flag@Base 0.0.200712
+ flag_default@Base 0.0.200804a
+ flag_flag_dep_default@Base 0.0.200804a   
+ flag_flag_dependency@Base 0.0.200712
+ flag_handler@Base 0.0.200712
+ flag_id_to_str@Base 0.0.200712
+ flag_parm_dep_default@Base 0.0.200804a   
+ flag_parm_dependency@Base 0.0.200712
+ flag_stringparm_dep_default@Base 0.0.200804a
+ flag_stringparm_dependency@Base 0.0.200712
+ flat_greater@Base 0.0.200712
+ flat_kbo_weight@Base 0.0.200712
+ flat_lrpo@Base 0.0.200712
+ flat_multiset_vars@Base 0.0.200712
+ flat_occurs_in@Base 0.0.200712
+ flat_variables_multisubset@Base 0.0.200712
+ flatten@Base 0.0.200712
+ flatten_top@Base 0.0.200712
+ flatterm_compare_vr@Base 0.0.200712
+ flatterm_count_without_vars@Base 0.0.200712
+ flatterm_ident@Base 0.0.200712
+ flatterm_symbol_count@Base 0.0.200712
+ flatterm_to_term@Base 0.0.200712
+ flip_eq@Base 0.0.200712
+ flip_just@Base 0.0.200712
+ fold_denial@Base 0.0.200712
+ formula_canon_eq@Base 0.0.200712
+ formula_contains_attributes@Base 0.0.200712
+ formula_copy@Base 0.0.200712
+ formula_copy_share@Base 0.0.200712
+ formula_flatten@Base 0.0.200712
+ formula_get@Base 0.0.200712
+ formula_ident@Base 0.0.200712
+ formula_ident_share@Base 0.0.200712
+ formula_megs@Base 0.0.200712
+ formula_set_variables@Base 0.0.200712
+ formula_size@Base 0.0.200712
+ formula_to_clause@Base 0.0.200712
+ formula_to_clauses@Base 0.0.200712
+ formula_to_literal@Base 0.0.200712
+ formula_to_literals@Base 0.0.200712
+ formula_to_term@Base 0.0.200712
+ formulas_to_conjunction@Base 0.0.200712
+ formulas_to_disjunction@Base 0.0.200712
+ forward_feature_subsume@Base 0.0.200712
+ forward_subsume@Base 0.0.200712
+ fpa_cancel@Base 0.0.200712
+ fpa_empty@Base 0.0.200712
+ fpa_first_answer@Base 0.0.200712
+ fpa_init_index@Base 0.0.200712
+ fpa_next_answer@Base 0.0.200712
+ fpa_update@Base 0.0.200712
+ fpalist_delete@Base 0.0.200712
+ fpalist_empty@Base 0.0.200712
+ fpalist_insert@Base 0.0.200712
+ fprint_attrib_mem@Base 0.0.200712
+ fprint_avltree_mem@Base 0.0.200712
+ fprint_btm_mem@Base 0.0.200712
+ fprint_btu_mem@Base 0.0.200712
+ fprint_clash_mem@Base 0.0.200712
+ fprint_clause@Base 0.0.200712
+ fprint_clause_clist@Base 0.0.200712
+ fprint_clause_id_tab@Base 0.0.200712
+ fprint_clist@Base 0.0.200712
+ fprint_clist_mem@Base 0.0.200712
+ fprint_clock@Base 0.0.200712
+ fprint_context@Base 0.0.200712
+ fprint_di_tree_mem@Base 0.0.200712
+ fprint_discrim_bind_index@Base 0.0.200712
+ fprint_discrim_mem@Base 0.0.200712
+ fprint_discrim_wild_index@Base 0.0.200712
+ fprint_discrimb_mem@Base 0.0.200712
+ fprint_discrimw_mem@Base 0.0.200712
+ fprint_flatterm_mem@Base 0.0.200712
+ fprint_formula@Base 0.0.200712
+ fprint_formula_mem@Base 0.0.200712
+ fprint_fpa_index@Base 0.0.200712
+ fprint_fpa_mem@Base 0.0.200712
+ fprint_fpa_state@Base 0.0.200712
+ fprint_fpalist_mem@Base 0.0.200712
+ fprint_glist_mem@Base 0.0.200712
+ fprint_hash_mem@Base 0.0.200712
+ fprint_ilist@Base 0.0.200712
+ fprint_interp_cooked@Base 0.0.200712
+ fprint_interp_mem@Base 0.0.200712
+ fprint_interp_portable@Base 0.0.200712
+ fprint_interp_raw@Base 0.0.200712
+ fprint_interp_standard2@Base 0.0.200712
+ fprint_interp_standard@Base 0.0.200712
+ fprint_interp_tabular@Base 0.0.200712
+ fprint_interp_tex@Base 0.0.200712
+ fprint_interp_xml@Base 0.0.200712
+ fprint_just_mem@Base 0.0.200712
+ fprint_lindex_mem@Base 0.0.200712
+ fprint_literals_mem@Base 0.0.200712
+ fprint_mindex@Base 0.0.200712
+ fprint_mindex_mem@Base 0.0.200712
+ fprint_options@Base 0.0.200712
+ fprint_options_mem@Base 0.0.200712
+ fprint_parse_mem@Base 0.0.200712
+ fprint_path@Base 0.0.200712
+ fprint_pindex_mem@Base 0.0.200712
+ fprint_sb@Base 0.0.200712
+ fprint_strbuf_mem@Base 0.0.200712
+ fprint_sym@Base 0.0.200712
+ fprint_syms@Base 0.0.200712
+ fprint_term@Base 0.0.200712
+ fprint_term_mem@Base 0.0.200712
+ fprint_top_input_mem@Base 0.0.200712
+ fprint_topform_mem@Base 0.0.200712
+ fprint_trail@Base 0.0.200712
+ fprint_unify_mem@Base 0.0.200712
+ free_clock@Base 0.0.200712
+ free_context@Base 0.0.200712
+ free_di_tree@Base 0.0.200712
+ free_discrim@Base 0.0.200712
+ free_discrim_pos@Base 0.0.200712
+ free_formula@Base 0.0.200712
+ free_i2list@Base 0.0.200712
+ free_i3list@Base 0.0.200712
+ free_ilist@Base 0.0.200712
+ free_literals@Base 0.0.200712
+ free_lits_to_term@Base 0.0.200712
+ free_mem@Base 0.0.200712
+ free_plist@Base 0.0.200712
+ free_term@Base 0.0.200712
+ free_variable@Base 0.0.200712
+ free_vars_term@Base 0.0.200712
+ fresh_symbol@Base 0.0.200712
+ fsym_set_in_term@Base 0.0.200712
+ fsym_set_in_topforms@Base 0.0.200712
+ function_or_relation_sn@Base 0.0.200712
+ function_or_relation_symbol@Base 0.0.200805a
+ function_symbol@Base 0.0.200712
+ function_symbols_in_formula@Base 0.0.200712
+ function_symbols_in_formulas@Base 0.0.200712
+ function_symbols_in_topform@Base 0.0.200712
+ function_symbols_in_topforms@Base 0.0.200712
+ fwrite_clause@Base 0.0.200712
+ fwrite_clause_clist@Base 0.0.200712
+ fwrite_clause_jmap@Base 0.0.200712
+ fwrite_clause_list@Base 0.0.200712
+ fwrite_demod_clist@Base 0.0.200712
+ fwrite_formula@Base 0.0.200712
+ fwrite_formula_list@Base 0.0.200712
+ fwrite_term@Base 0.0.200712
+ fwrite_term_list@Base 0.0.200712
+ fwrite_term_nl@Base 0.0.200712
+ gen_new_symbol@Base 0.0.200712
+ get_bits@Base 0.0.200712
+ get_clause_ancestors@Base 0.0.200712
+ get_clause_from_ibuf@Base 0.0.200712
+ get_cmem@Base 0.0.200712
+ get_cons_char@Base 0.0.200712
+ get_context@Base 0.0.200712
+ get_date@Base 0.0.200712
+ get_di_tree@Base 0.0.200712
+ get_discrim@Base 0.0.200712
+ get_discrim_pos@Base 0.0.200712
+ get_fatal_exit_code@Base 0.0.200712
+ get_flatterm@Base 0.0.200712
+ get_fpa_list@Base 0.0.200712
+ get_i2list@Base 0.0.200712
+ get_i3list@Base 0.0.200712
+ get_ilist@Base 0.0.200712
+ get_instancejust@Base 0.0.200712
+ get_int_attribute@Base 0.0.200712
+ get_just@Base 0.0.200712
+ get_literals@Base 0.0.200712
+ get_mem@Base 0.0.200712
+ get_nil_term@Base 0.0.200712
+ get_operation_symbol@Base 0.0.200712
+ get_parajust@Base 0.0.200712
+ get_parents@Base 0.0.200712
+ get_plist@Base 0.0.200712
+ get_quant_form@Base 0.0.200712
+ get_quote_char@Base 0.0.200712
+ get_rigid_term@Base 0.0.200712
+ get_rigid_term_dangerously@Base 0.0.200712
+ get_rigid_term_like@Base 0.0.200712
+ get_string_attribute@Base 0.0.200712
+ get_string_buf@Base 0.0.200712
+ get_symbol_type@Base 0.0.200712
+ get_term_attribute@Base 0.0.200712
+ get_term_attributes@Base 0.0.200806a
+ get_topform@Base 0.0.200712
+ get_variable_term@Base 0.0.200712
+ goal_just@Base 0.0.200712
+ greater_multiset@Base 0.0.200712
+ greater_multiset_current_ordering@Base 0.0.200712
+ greatest_id_in_proof@Base 0.0.200712
+ greatest_qvar@Base 0.0.200712
+ greatest_symnum@Base 0.0.200712
+ greatest_symnum_in_formula@Base 0.0.200712
+ greatest_symnum_in_term@Base 0.0.200712
+ greatest_variable@Base 0.0.200712
+ greatest_variable_in_clause@Base 0.0.200712
+ ground_clause@Base 0.0.200712
+ ground_term@Base 0.0.200712
+ has_copy_flip_just@Base 0.0.200804a
+ has_copy_just@Base 0.0.200712
+ has_greatest_precedence@Base 0.0.200712
+ has_input_just@Base 0.0.200712
+ hash_delete@Base 0.0.200712
+ hash_destroy@Base 0.0.200712
+ hash_formula@Base 0.0.200712
+ hash_info@Base 0.0.200712
+ hash_init@Base 0.0.200712
+ hash_insert@Base 0.0.200712
+ hash_lookup@Base 0.0.200712
+ hash_term@Base 0.0.200712
+ horn_clause@Base 0.0.200712
+ horn_clist@Base 0.0.200712
+ hostname@Base 0.0.200712
+ hyper_resolution@Base 0.0.200712
+ i2list_append@Base 0.0.200712
+ i2list_count@Base 0.0.200712
+ i2list_member@Base 0.0.200712
+ i2list_multimember@Base 0.0.200712
+ i2list_multisubset@Base 0.0.200712
+ i2list_prepend@Base 0.0.200712
+ i2list_removeall@Base 0.0.200712
+ i3list_append@Base 0.0.200712
+ i3list_count@Base 0.0.200712
+ i3list_prepend@Base 0.0.200712
+ ibuf_buffer@Base 0.0.200712
+ ibuf_free@Base 0.0.200712
+ ibuf_init@Base 0.0.200712
+ ibuf_length@Base 0.0.200712
+ ibuf_read@Base 0.0.200712
+ ibuf_rewind@Base 0.0.200712
+ ibuf_write@Base 0.0.200712
+ ibuf_write_block@Base 0.0.200712
+ ibuf_xread@Base 0.0.200712
+ ident_interp@Base 0.0.200712
+ ident_interp_perm@Base 0.0.200712
+ idx_demodulator@Base 0.0.200712
+ iff_sym@Base 0.0.200712
+ ilist_append@Base 0.0.200712
+ ilist_cat2@Base 0.0.200712
+ ilist_cat@Base 0.0.200712
+ ilist_copy@Base 0.0.200712
+ ilist_count@Base 0.0.200712
+ ilist_insert_up@Base 0.0.200712
+ ilist_intersect@Base 0.0.200712
+ ilist_is_set@Base 0.0.200712
+ ilist_last@Base 0.0.200804a
+ ilist_member@Base 0.0.200712
+ ilist_occurrences@Base 0.0.200712
+ ilist_pop@Base 0.0.200712
+ ilist_prepend@Base 0.0.200712
+ ilist_rem_dups@Base 0.0.200712
+ ilist_remove_last@Base 0.0.200712
+ ilist_removeall@Base 0.0.200712
+ ilist_set@Base 0.0.200712
+ ilist_subset@Base 0.0.200712
+ ilist_subtract@Base 0.0.200712
+ ilist_union@Base 0.0.200712
+ imp@Base 0.0.200712
+ imp_sym@Base 0.0.200712
+ impby@Base 0.0.200712
+ impby_sym@Base 0.0.200712
+ index_clause_back_demod@Base 0.0.200712
+ index_hint@Base 0.0.200712
+ inherit_attributes@Base 0.0.200712
+ inheritable_att_instances@Base 0.0.200712
+ init_basic_paramod@Base 0.0.200712
+ init_di_tree@Base 0.0.200712
+ init_features@Base 0.0.200712
+ init_flag@Base 0.0.200712
+ init_hints@Base 0.0.200712
+ init_kbo_weights@Base 0.0.200712
+ init_maximal@Base 0.0.200712
+ init_pair_index@Base 0.0.200712
+ init_paramod@Base 0.0.200712
+ init_parm@Base 0.0.200712
+ init_standard_ladr@Base 0.0.200712
+ init_standard_options@Base 0.0.200712
+ init_string_buf@Base 0.0.200712
+ init_stringparm@Base 0.0.200712
+ init_wallclock@Base 0.0.200712
+ init_weight@Base 0.0.200712
+ initial_clause@Base 0.0.200712
+ initial_substring@Base 0.0.200712
+ input_clauses@Base 0.0.200712
+ input_just@Base 0.0.200712
+ insert_clause_into_plist@Base 0.0.200712
+ insert_pair_index@Base 0.0.200712
+ instance_just@Base 0.0.200712
+ instantiate_clause@Base 0.0.200712
+ instantiate_inheritable_attributes@Base 0.0.200712
+ int_power@Base 0.0.200712
+ int_to_term@Base 0.0.200804a
+ interp_comments@Base 0.0.200712
+ interp_remove_constants@Base 0.0.200712
+ interp_remove_constants_recurse@Base 0.0.200712
+ interp_remove_others@Base 0.0.200712
+ interp_remove_others_recurse@Base 0.0.200712
+ interp_size@Base 0.0.200712
+ interp_table@Base 0.0.200712
+ intersect_clauses@Base 0.0.200712
+ is_assoc_comm@Base 0.0.200712
+ is_commutative@Base 0.0.200712
+ is_constant@Base 0.0.200712
+ is_definition@Base 0.0.200712
+ is_eq_symbol@Base 0.0.200712
+ is_skolem@Base 0.0.200712
+ is_symbol@Base 0.0.200712
+ is_term@Base 0.0.200712
+ is_unfold_symbol@Base 0.0.200712
+ iso_checks@Base 0.0.200712
+ iso_perms@Base 0.0.200712
+ isomorphic_interps@Base 0.0.200712
+ ith_in_plist@Base 0.0.200712
+ ith_literal@Base 0.0.200712
+ itoa@Base 0.0.200712
+ ivy_just@Base 0.0.200712
+ jmap1@Base 0.0.200712
+ jmap2@Base 0.0.200712
+ jstring@Base 0.0.200712
+ just_count@Base 0.0.200712
+ kbo@Base 0.0.200712
+ kbo_weight@Base 0.0.200712
+ label_att@Base 0.0.200712
+ ladr_list_to_tptp_list@Base 0.0.200712
+ lex_compare_arity_0123@Base 0.0.200712
+ lex_compare_arity_0213@Base 0.0.200712
+ lex_insert_after_initial_constants@Base 0.0.200712
+ lex_order@Base 0.0.200712
+ lindex_backtrack@Base 0.0.200712
+ lindex_destroy@Base 0.0.200712
+ lindex_empty@Base 0.0.200712
+ lindex_init@Base 0.0.200712
+ lindex_update@Base 0.0.200712
+ lindex_update_first@Base 0.0.200712
+ listterm_append@Base 0.0.200712
+ listterm_cons@Base 0.0.200712
+ listterm_i@Base 0.0.200712
+ listterm_length@Base 0.0.200712
+ listterm_member@Base 0.0.200712
+ listterm_reverse@Base 0.0.200712
+ listterm_to_tlist@Base 0.0.200712
+ listterm_zap@Base 0.0.200712
+ literal_flip@Base 0.0.200712
+ literal_formula@Base 0.0.200712
+ literal_number@Base 0.0.200712
+ literal_to_term@Base 0.0.200712
+ literals_depth@Base 0.0.200712
+ literals_to_term@Base 0.0.200712
+ lits_to_term@Base 0.0.200712
+ longest_string_in_plist@Base 0.0.200712
+ lrpo@Base 0.0.200712
+ lrpo_multiset@Base 0.0.200712
+ make_clause_basic@Base 0.0.200712
+ make_conjunction@Base 0.0.200712
+ make_disjunction@Base 0.0.200712
+ map_for_bad_tptp_syms@Base 0.0.200712
+ map_just@Base 0.0.200712
+ mark_all_nonbasic@Base 0.0.200712
+ mark_for_new_symbols@Base 0.0.200712
+ mark_maximal_literals@Base 0.0.200712
+ mark_oriented_eq@Base 0.0.200712
+ mark_parents_as_used@Base 0.0.200712
+ mark_renamable_flip@Base 0.0.200712
+ mark_selected_literal@Base 0.0.200712
+ mark_selected_literals@Base 0.0.200712
+ mark_term_nonbasic@Base 0.0.200712
+ match@Base 0.0.200712
+ match_bt_cancel@Base 0.0.200712
+ match_bt_first@Base 0.0.200712
+ match_bt_next@Base 0.0.200712
+ match_weight@Base 0.0.200712
+ max_clause_symbol_count@Base 0.0.200712
+ max_clause_weight@Base 0.0.200712
+ max_lit_test@Base 0.0.200712
+ max_signed_lit_test@Base 0.0.200712
+ max_wt_in_clist@Base 0.0.200712
+ maximal_literal@Base 0.0.200712
+ maximal_signed_literal@Base 0.0.200712
+ mega_mem_calls@Base 0.0.200712
+ mega_next_calls@Base 0.0.200712
+ mega_sub_calls@Base 0.0.200712
+ megs_malloced@Base 0.0.200712
+ memory_report@Base 0.0.200712
+ merge_just@Base 0.0.200712
+ merge_literals@Base 0.0.200712
+ merge_sort@Base 0.0.200712
+ merge_sort_recurse@Base 0.0.200712
+ min_depth@Base 0.0.200712
+ min_lex_val@Base 0.0.200712
+ mindex_destroy@Base 0.0.200712
+ mindex_empty@Base 0.0.200712
+ mindex_free@Base 0.0.200712
+ mindex_init@Base 0.0.200712
+ mindex_retrieve_cancel@Base 0.0.200712
+ mindex_retrieve_first@Base 0.0.200712
+ mindex_retrieve_next@Base 0.0.200712
+ mindex_update@Base 0.0.200712
+ miniscope@Base 0.0.200712
+ miniscope_formula@Base 0.0.200712
+ mixed_clause@Base 0.0.200712
+ most_literals@Base 0.0.200712
+ move_clauses_to_clist@Base 0.0.200712
+ move_clist_to_plist@Base 0.0.200712
+ multiset_add@Base 0.0.200712
+ multiset_add_n@Base 0.0.200712
+ multiset_occurrences@Base 0.0.200712
+ multiset_of_vars@Base 0.0.200712
+ multiset_to_set@Base 0.0.200712
+ multiset_union@Base 0.0.200712
+ multiset_vars@Base 0.0.200712
+ my_process_id@Base 0.0.200712
+ name_clist@Base 0.0.200712
+ nat_to_term@Base 0.0.200712
+ natural_constant_term@Base 0.0.200712
+ natural_string@Base 0.0.200712
+ neg_clauses_in_clist@Base 0.0.200712
+ neg_eq@Base 0.0.200712
+ neg_eq_unit@Base 0.0.200712
+ neg_nonunit_clauses@Base 0.0.200712
+ neg_nonunit_in_clist@Base 0.0.200712
+ negate@Base 0.0.200712
+ negative_clause@Base 0.0.200712
+ negative_clause_possibly_compressed@Base 0.0.200712
+ negative_clauses@Base 0.0.200712
+ negative_literals@Base 0.0.200712
+ neq_sym@Base 0.0.200712
+ new_constant@Base 0.0.200712
+ new_constant_properties@Base 0.0.200712
+ new_literal@Base 0.0.200712
+ new_str_copy@Base 0.0.200712
+ new_symbol_just@Base 0.0.200712
+ new_symbols_since_mark@Base 0.0.200712
+ next_combo_a@Base 0.0.200712
+ next_combo_b@Base 0.0.200712
+ next_combo_c@Base 0.0.200712
+ next_combo_ss@Base 0.0.200712
+ next_fpos@Base 0.0.200712
+ next_skolem_symbol@Base 0.0.200712
+ nil_term@Base 0.0.200712
+ nnf2@Base 0.0.200712
+ nnf@Base 0.0.200712
+ nonbasic_flag@Base 0.0.200712
+ nonbasic_term@Base 0.0.200712
+ nonneg_clauses@Base 0.0.200712
+ nonunit_bsub_tests@Base 0.0.200712
+ nonunit_fsub_tests@Base 0.0.200712
+ nonunit_subsumption_tests@Base 0.0.200712
+ normal3_interp@Base 0.0.200712
+ normal_interp@Base 0.0.200712
+ not_in_preliminary_precedence@Base 0.0.200712
+ not_sym@Base 0.0.200712
+ not_symnum@Base 0.0.200712
+ number_of_literals@Base 0.0.200712
+ number_of_maximal_literals@Base 0.0.200712
+ number_of_variables@Base 0.0.200712
+ number_of_vars_in_term@Base 0.0.200805a
+ occur_check@Base 0.0.200712
+ occurrences@Base 0.0.200712
+ occurs_in@Base 0.0.200712
+ only_eq@Base 0.0.200804a
+ option_dependencies_state@Base 0.0.200712
+ option_updates@Base 0.0.200712
+ or@Base 0.0.200712
+ or_sym@Base 0.0.200712
+ or_symnum@Base 0.0.200712
+ ordinary_constant_string@Base 0.0.200712
+ orient_equalities@Base 0.0.200712
+ oriented_eq@Base 0.0.200712
+ over_parm_limit@Base 0.0.200712
+ p_ac_basis@Base 0.0.200712
+ p_attrib_mem@Base 0.0.200712
+ p_avl@Base 0.0.200712
+ p_avltree_mem@Base 0.0.200712
+ p_bt_tree@Base 0.0.200712
+ p_btm_mem@Base 0.0.200712
+ p_btm_state@Base 0.0.200712
+ p_btu_mem@Base 0.0.200712
+ p_clash_mem@Base 0.0.200712
+ p_clause@Base 0.0.200712
+ p_clause_id_tab@Base 0.0.200712
+ p_clist@Base 0.0.200712
+ p_clist_mem@Base 0.0.200712
+ p_context@Base 0.0.200712
+ p_di_tree@Base 0.0.200712
+ p_di_tree_mem@Base 0.0.200712
+ p_discrim_bind_index@Base 0.0.200712
+ p_discrim_mem@Base 0.0.200712
+ p_discrim_wild_index@Base 0.0.200712
+ p_discrimb_mem@Base 0.0.200712
+ p_discrimw_mem@Base 0.0.200712
+ p_features@Base 0.0.200712
+ p_flat2@Base 0.0.200712
+ p_flat@Base 0.0.200712
+ p_flatterm@Base 0.0.200712
+ p_flatterm_mem@Base 0.0.200712
+ p_formula@Base 0.0.200712
+ p_formula_mem@Base 0.0.200712
+ p_fpa_density@Base 0.0.200712
+ p_fpa_index@Base 0.0.200712
+ p_fpa_list@Base 0.0.200804a
+ p_fpa_mem@Base 0.0.200712
+ p_fpa_query@Base 0.0.200712
+ p_fpa_state@Base 0.0.200712
+ p_fpalist_mem@Base 0.0.200712
+ p_glist_mem@Base 0.0.200712
+ p_hash_mem@Base 0.0.200712
+ p_i2list@Base 0.0.200712
+ p_ibuf@Base 0.0.200712
+ p_ilist@Base 0.0.200712
+ p_interp@Base 0.0.200712
+ p_interp_mem@Base 0.0.200712
+ p_interp_profile@Base 0.0.200712
+ p_just@Base 0.0.200712
+ p_just_mem@Base 0.0.200712
+ p_lindex_mem@Base 0.0.200712
+ p_literals_mem@Base 0.0.200712
+ p_mindex_mem@Base 0.0.200712
+ p_options@Base 0.0.200712
+ p_options_mem@Base 0.0.200712
+ p_pair_index@Base 0.0.200712
+ p_parse_mem@Base 0.0.200712
+ p_path@Base 0.0.200712
+ p_pindex_mem@Base 0.0.200712
+ p_sb@Base 0.0.200712
+ p_strbuf_mem@Base 0.0.200712
+ p_sym@Base 0.0.200712
+ p_syms@Base 0.0.200712
+ p_term@Base 0.0.200712
+ p_term_basic@Base 0.0.200712
+ p_term_mem@Base 0.0.200712
+ p_top_input_mem@Base 0.0.200712
+ p_topform_mem@Base 0.0.200712
+ p_trail@Base 0.0.200712
+ p_unify_mem@Base 0.0.200712
+ pair_already_used@Base 0.0.200712
+ pairs_exhausted@Base 0.0.200712
+ para_from_into@Base 0.0.200712
+ para_instance_prunes@Base 0.0.200712
+ para_just@Base 0.0.200712
+ para_just_rev_copy@Base 0.0.200712
+ para_pos2@Base 0.0.200804a
+ para_pos@Base 0.0.200712
+ paramodulate@Base 0.0.200712
+ paramodulation_options@Base 0.0.200712
+ parenthesize@Base 0.0.200712
+ parm@Base 0.0.200712
+ parm_default@Base 0.0.200804a
+ parm_flag_dependency@Base 0.0.200712
+ parm_handler@Base 0.0.200712
+ parm_id_to_str@Base 0.0.200712
+ parm_parm_dependency@Base 0.0.200712
+ parse_clause_from_string@Base 0.0.200712
+ parse_term_from_string@Base 0.0.200712
+ parse_type_to_str@Base 0.0.200712
+ particular_demod@Base 0.0.200712
+ perms_required@Base 0.0.200712
+ permute_interp@Base 0.0.200712
+ plist_append@Base 0.0.200712
+ plist_cat2@Base 0.0.200712
+ plist_cat@Base 0.0.200712
+ plist_count@Base 0.0.200712
+ plist_last@Base 0.0.200804a
+ plist_member@Base 0.0.200712
+ plist_of_subterms@Base 0.0.200712
+ plist_pop@Base 0.0.200712
+ plist_prepend@Base 0.0.200712
+ plist_remove@Base 0.0.200712
+ plist_remove_last@Base 0.0.200712
+ plist_subset@Base 0.0.200712
+ plist_subtract@Base 0.0.200712
+ plist_to_clist@Base 0.0.200712
+ pos_eq@Base 0.0.200712
+ pos_eq_unit@Base 0.0.200712
+ pos_equality_in_clauses@Base 0.0.200712
+ pos_in_clist@Base 0.0.200712
+ position_in_ilist@Base 0.0.200712
+ position_of_string_in_plist@Base 0.0.200712
+ position_of_subterm@Base 0.0.200712
+ position_of_term_in_tlist@Base 0.0.200712
+ positive_clause@Base 0.0.200712
+ positive_formula@Base 0.0.200712
+ positive_literals@Base 0.0.200712
+ preliminary_lex_compare@Base 0.0.200712
+ prepend_clist_to_plist@Base 0.0.200712
+ primary_just_type@Base 0.0.200804a
+ print_banner@Base 0.0.200712
+ print_flatterm@Base 0.0.200712
+ print_fsym_precedence@Base 0.0.200712
+ print_kbo_weights@Base 0.0.200712
+ print_rsym_precedence@Base 0.0.200712
+ print_separator@Base 0.0.200712
+ process_definitions@Base 0.0.200712
+ process_goal_formulas@Base 0.0.200712
+ process_input_formulas@Base 0.0.200712
+ process_lex_list@Base 0.0.200712
+ process_op@Base 0.0.200712
+ process_quoted_symbol@Base 0.0.200806a
+ process_redeclare@Base 0.0.200712
+ process_skolem_list@Base 0.0.200712
+ process_standard_options@Base 0.0.200712
+ prolog_style_variables_id@Base 0.0.200712
+ proof_id_to_clause@Base 0.0.200712
+ proof_length@Base 0.0.200712
+ proof_to_xproof@Base 0.0.200712
+ proper_listterm@Base 0.0.200712
+ propositional_just@Base 0.0.200712
+ put_clause_to_ibuf@Base 0.0.200712
+ quant_form@Base 0.0.200712
+ quant_sym@Base 0.0.200712
+ random_clause@Base 0.0.200712
+ random_complex_term@Base 0.0.200712
+ random_nonvariable_term@Base 0.0.200712
+ random_op_term@Base 0.0.200712
+ random_path@Base 0.0.200712
+ random_permutation@Base 0.0.200712
+ random_term@Base 0.0.200712
+ read_all_input@Base 0.0.200712
+ read_clause@Base 0.0.200712
+ read_clause_clist@Base 0.0.200712
+ read_clause_list@Base 0.0.200712
+ read_clause_or_formula@Base 0.0.200712
+ read_clause_or_formula_list@Base 0.0.200712
+ read_commands@Base 0.0.200712
+ read_formula@Base 0.0.200712
+ read_formula_list@Base 0.0.200712
+ read_from_file@Base 0.0.200712
+ read_term@Base 0.0.200712
+ read_term_list@Base 0.0.200712
+ redeclare_symbol_and_copy_parsetype@Base 0.0.200712
+ redundant_hints@Base 0.0.200712
+ register_attribute@Base 0.0.200712
+ relation_in_formula@Base 0.0.200712
+ relation_symbol@Base 0.0.200712
+ relation_symbols_in_formula@Base 0.0.200712
+ relation_symbols_in_formulas@Base 0.0.200712
+ relation_symbols_in_topform@Base 0.0.200712
+ relation_symbols_in_topforms@Base 0.0.200712
+ release_term_flag@Base 0.0.200712
+ remove_null_literals@Base 0.0.200712
+ remove_universal_quantifiers@Base 0.0.200712
+ remove_variable_symbols@Base 0.0.200712
+ renamable_flip_eq@Base 0.0.200712
+ renamable_flip_eq_test@Base 0.0.200712
+ rename_all_bound_vars@Base 0.0.200712
+ rename_these_bound_vars@Base 0.0.200712
+ renum_vars_map@Base 0.0.200712
+ renum_vars_recurse@Base 0.0.200712
+ renumber_proof@Base 0.0.200712
+ renumber_variables@Base 0.0.200712
+ renumber_vars_attributes@Base 0.0.200712
+ replace_bad_tptp_syms_form@Base 0.0.200712
+ replace_int_attribute@Base 0.0.200712
+ replace_term_attribute@Base 0.0.200712
+ res_instance_prunes@Base 0.0.200712
+ resolution_options@Base 0.0.200712
+ resolve2@Base 0.0.200712
+ resolve3@Base 0.0.200712
+ resolve_just@Base 0.0.200712
+ retrieve_pair@Base 0.0.200712
+ reverse_chars@Base 0.0.200712
+ reverse_i3list@Base 0.0.200712
+ reverse_ilist@Base 0.0.200712
+ reverse_plist@Base 0.0.200712
+ rewritable_clause@Base 0.0.200712
+ rsym_set_in_topforms@Base 0.0.200712
+ rule_contains_semantics@Base 0.0.200804a
+ same_discriminator_counts@Base 0.0.200712
+ same_profiles@Base 0.0.200712
+ same_structure@Base 0.0.200712
+ same_term_structure@Base 0.0.200712
+ same_top@Base 0.0.200712
+ sb_append@Base 0.0.200712
+ sb_append_char@Base 0.0.200712
+ sb_append_id@Base 0.0.200712
+ sb_append_int@Base 0.0.200712
+ sb_cat@Base 0.0.200712
+ sb_cat_copy@Base 0.0.200712
+ sb_char@Base 0.0.200712
+ sb_ivy_write_clause_jmap@Base 0.0.200712
+ sb_ivy_write_just@Base 0.0.200712
+ sb_replace_char@Base 0.0.200712
+ sb_size@Base 0.0.200712
+ sb_tagged_write_clause_jmap@Base 0.0.200806a
+ sb_tagged_write_just@Base 0.0.200806a
+ sb_to_malloc_char_array@Base 0.0.200712
+ sb_to_malloc_string@Base 0.0.200712
+ sb_write_clause@Base 0.0.200712
+ sb_write_clause_jmap@Base 0.0.200712
+ sb_write_ids@Base 0.0.200712
+ sb_write_just@Base 0.0.200712
+ sb_write_term@Base 0.0.200712
+ sb_xml_write_clause_jmap@Base 0.0.200712
+ sb_xml_write_just@Base 0.0.200712
+ selected_literal@Base 0.0.200712
+ separate_definitions@Base 0.0.200712
+ set_assoc_comm@Base 0.0.200712
+ set_basic_paramod@Base 0.0.200712
+ set_commutative@Base 0.0.200712
+ set_cons_char@Base 0.0.200712
+ set_fatal_exit_code@Base 0.0.200712
+ set_flag@Base 0.0.200712
+ set_int_attribute@Base 0.0.200712
+ set_kb_weight@Base 0.0.200712
+ set_lex_val@Base 0.0.200712
+ set_lrpo_status@Base 0.0.200712
+ set_max_megs@Base 0.0.200712
+ set_max_megs_proc@Base 0.0.200712
+ set_of_ivariables@Base 0.0.200712
+ set_of_ivars@Base 0.0.200712
+ set_of_variables@Base 0.0.200712
+ set_of_vars@Base 0.0.200712
+ set_operation_symbol@Base 0.0.200712
+ set_parse_type@Base 0.0.200712
+ set_program_name@Base 0.0.200712
+ set_quote_char@Base 0.0.200712
+ set_skolem@Base 0.0.200712
+ set_skolem_symbols@Base 0.0.200712
+ set_string_attribute@Base 0.0.200712
+ set_symbol_type@Base 0.0.200712
+ set_term_attribute@Base 0.0.200712
+ set_unfold_symbol@Base 0.0.200712
+ set_variable_style@Base 0.0.200712
+ set_vars_attributes@Base 0.0.200712
+ set_vars_recurse@Base 0.0.200712
+ simplify_literals2@Base 0.0.200712
+ simplify_literals@Base 0.0.200712
+ skip_to_nl@Base 0.0.200712
+ skolem_check@Base 0.0.200712
+ skolem_reset@Base 0.0.200712
+ skolem_symbols@Base 0.0.200712
+ skolem_term@Base 0.0.200712
+ skolemize@Base 0.0.200712
+ sn_to_arity@Base 0.0.200712
+ sn_to_kb_wt@Base 0.0.200712
+ sn_to_lex_val@Base 0.0.200712
+ sn_to_lrpo_status@Base 0.0.200712
+ sn_to_occurrences@Base 0.0.200712
+ sn_to_str@Base 0.0.200712
+ sort_by_lex_val@Base 0.0.200712
+ sort_clist_by_id@Base 0.0.200712
+ sort_plist@Base 0.0.200712
+ special_parse_type@Base 0.0.200712
+ split_string@Base 0.0.200712
+ sprint_sym@Base 0.0.200712
+ sprint_term@Base 0.0.200712
+ sread_term@Base 0.0.200712
+ str_exists@Base 0.0.200712
+ str_ident@Base 0.0.200712
+ str_to_flag_id@Base 0.0.200712
+ str_to_int@Base 0.0.200712
+ str_to_parm_id@Base 0.0.200712
+ str_to_sn@Base 0.0.200712
+ str_to_stringparm_id@Base 0.0.200712
+ string_attribute_member@Base 0.0.200712
+ string_member@Base 0.0.200712
+ string_member_plist@Base 0.0.200712
+ stringparm1@Base 0.0.200712
+ stringparm1_default@Base 0.0.200804a
+ stringparm@Base 0.0.200712
+ stringparm_id_to_str@Base 0.0.200712
+ subformula_contains_attributes@Base 0.0.200712
+ subst_changes_term@Base 0.0.200712
+ subst_free_var@Base 0.0.200712
+ subst_term@Base 0.0.200712
+ subst_var_term@Base 0.0.200712
+ substring@Base 0.0.200712
+ subsumes@Base 0.0.200712
+ subsumes_bt@Base 0.0.200712
+ sym_precedence@Base 0.0.200712
+ symbol_count@Base 0.0.200712
+ symbol_for_variable@Base 0.0.200712
+ symbol_in_term@Base 0.0.200712
+ symbol_in_use@Base 0.0.200712
+ symbol_occurrences@Base 0.0.200712
+ symbol_occurrences_in_clause@Base 0.0.200712
+ symbol_with_string@Base 0.0.200712
+ symbols_in_term@Base 0.0.200712
+ symnums_of_arity@Base 0.0.200712
+ syms_in_form@Base 0.0.200712
+ syms_with_lex_val@Base 0.0.200712
+ system_seconds@Base 0.0.200712
+ system_time@Base 0.0.200712
+ tautology@Base 0.0.200712
+ term0@Base 0.0.200712
+ term1@Base 0.0.200712
+ term2@Base 0.0.200712
+ term_at_pos@Base 0.0.200712
+ term_at_position@Base 0.0.200804a
+ term_compare_ncv@Base 0.0.200712
+ term_compare_vcp@Base 0.0.200712
+ term_compare_vr@Base 0.0.200712
+ term_depth@Base 0.0.200712
+ term_flag@Base 0.0.200712
+ term_flag_clear@Base 0.0.200712
+ term_flag_clear_recursively@Base 0.0.200712
+ term_flag_set@Base 0.0.200712
+ term_flags@Base 0.0.200712
+ term_greater@Base 0.0.200712
+ term_ident@Base 0.0.200712
+ term_order@Base 0.0.200712
+ term_reader@Base 0.0.200712
+ term_renumber_variables@Base 0.0.200712
+ term_set_variables@Base 0.0.200712
+ term_symbol@Base 0.0.200712
+ term_to_attributes@Base 0.0.200712
+ term_to_clause@Base 0.0.200712
+ term_to_flatterm@Base 0.0.200712
+ term_to_formula@Base 0.0.200712
+ term_to_int@Base 0.0.200712
+ term_to_just@Base 0.0.200712
+ term_to_literals@Base 0.0.200712
+ term_to_string@Base 0.0.200806a
+ term_to_topform2@Base 0.0.200712
+ term_to_topform@Base 0.0.200712
+ term_writer@Base 0.0.200712
+ tlist_copy@Base 0.0.200712
+ tlist_member@Base 0.0.200712
+ tlist_remove@Base 0.0.200712
+ tlist_set@Base 0.0.200712
+ tlist_subset@Base 0.0.200712
+ tlist_union@Base 0.0.200712
+ top_flip@Base 0.0.200712
+ topform_properties@Base 0.0.200712
+ topform_to_term@Base 0.0.200712
+ topform_to_term_without_attributes@Base 0.0.200712
+ tp_alloc@Base 0.0.200712
+ tptp_input_to_ladr_formula@Base 0.0.200712
+ translate_neg_equalities@Base 0.0.200712
+ transpose_binary@Base 0.0.200712
+ true_clause@Base 0.0.200712
+ true_sym@Base 0.0.200712
+ true_term@Base 0.0.200712
+ try_unit_conflict@Base 0.0.200804a
+ unary_parse_type@Base 0.0.200712
+ unassign_clause_id@Base 0.0.200712
+ uncompress_clause@Base 0.0.200712
+ uncompress_clauses@Base 0.0.200712
+ uncompress_term@Base 0.0.200712
+ undo_subst@Base 0.0.200712
+ undo_subst_2@Base 0.0.200712
+ unfold_order@Base 0.0.200712
+ unify@Base 0.0.200712
+ unify_bt_cancel@Base 0.0.200712
+ unify_bt_first@Base 0.0.200712
+ unify_bt_next@Base 0.0.200712
+ unindex_hint@Base 0.0.200712
+ unique_quantified_vars@Base 0.0.200712
+ unit_clause@Base 0.0.200712
+ unit_clist@Base 0.0.200712
+ unit_conflict_by_index@Base 0.0.200712
+ unit_del_just@Base 0.0.200712
+ unit_delete@Base 0.0.200712
+ universal_closure@Base 0.0.200712
+ update_flag@Base 0.0.200712
+ update_interp_with_constant@Base 0.0.200712
+ update_profile@Base 0.0.200712
+ upward_clause_links@Base 0.0.200712
+ upward_term_links@Base 0.0.200712
+ ur_resolution@Base 0.0.200712
+ user_seconds@Base 0.0.200712
+ user_time@Base 0.0.200712
+ username@Base 0.0.200712
+ variable_name@Base 0.0.200712
+ variable_style@Base 0.0.200712
+ variable_substitution@Base 0.0.200712
+ variable_symbols@Base 0.0.200804a
+ variables_multisubset@Base 0.0.200712
+ variables_subset@Base 0.0.200712
+ variant@Base 0.0.200712
+ varnums_in_clause@Base 0.0.200712
+ vars_in_attributes@Base 0.0.200712
+ vars_in_clause@Base 0.0.200712
+ vars_in_trail@Base 0.0.200712
+ wallclock@Base 0.0.200712
+ weight@Base 0.0.200712
+ which_string_member@Base 0.0.200712
+ xx_just@Base 0.0.200712
+ xx_resolve2@Base 0.0.200712
+ xxres_just@Base 0.0.200712
+ zap_attributes@Base 0.0.200712
+ zap_clash@Base 0.0.200712
+ zap_clause_eval_rule@Base 0.0.200804a
+ zap_di_tree@Base 0.0.200712
+ zap_flatterm@Base 0.0.200712
+ zap_formula@Base 0.0.200712
+ zap_formula_list@Base 0.0.200712
+ zap_fpa_chunks@Base 0.0.200712
+ zap_fpa_index@Base 0.0.200712
+ zap_fpalist@Base 0.0.200712
+ zap_i2list@Base 0.0.200712
+ zap_i3list@Base 0.0.200712
+ zap_ilist@Base 0.0.200712
+ zap_interp@Base 0.0.200712
+ zap_just@Base 0.0.200712
+ zap_literal@Base 0.0.200712
+ zap_literal_flip@Base 0.0.200712
+ zap_literals@Base 0.0.200712
+ zap_pair_index@Base 0.0.200712
+ zap_plist@Base 0.0.200712
+ zap_plist_of_terms@Base 0.0.200712
+ zap_string_buf@Base 0.0.200712
+ zap_term@Base 0.0.200712
+ zap_tlist@Base 0.0.200712
+ zap_top_flip@Base 0.0.200712
+ zap_topform@Base 0.0.200712
+ zero_wt_kb@Base 0.0.200712
--- ladr-0.0.200806a.orig/debian/mace4.1
+++ ladr-0.0.200806a/debian/mace4.1
@@ -0,0 +1,86 @@
+.TH MACE4 1 "August 12, 2007"
+.SH NAME
+mace4 \- searches for finite countermodels of first-order statements
+.SH SYNOPSIS
+.B mace4
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.SH DESCRIPTION
+This manual page documents briefly the
+.B mace4
+command.
+.PP
+The program \fBmace4\fP searches for finite structures satisfying first-order and equational statements, the same kind of statement that
+.BR prover9 (1)
+accepts. If the statement is the denial of some conjecture, any structures found by \fBmace4\fP are counterexamples to the conjecture.  \fBmace4\fP can be a valuable complement to
+.BR prover9 (1),
+looking for counterexamples before (or at the same time as) using
+.BR prover9 (1)
+to search for a proof. It can also be used to help debug input clauses and formulas for
+.BR prover9 (1).
+.SH OPTIONS
+A summary of options is included below.  Options override the equivalent settings given in the input file.  To set or clear a flag, you must give 1 or 0 as the value.
+.TP
+.B \-help
+This tells \fBmace4\fP to print a summary of these command-line options.
+.TP
+.B \-n \fIn
+This gives the starting domain size for the search. The default value is 2. If you also give an \fB-N\fP option, \fBmace4\fP will iterate domain sizes up through the \fB-N\fP value, using an increment given by the \fB-I\fP value. Otherwise, \fBmace4\fP will search only for the \fB-n\fP value.
+.TP
+.B \-N \fIn
+This gives the ending domain size for the search. The default is 10.
+.TP
+.B \-i \fIn
+This gives the domain size increment for the search. The default is 1.
+.TP
+.B \-q \fIn
+This flag overrides the parameter iterate. It says to try the sizes that are prime numbers, from \fB-n\fP up through \fB-N\fP.
+.TP
+.B \-m \fIn
+Stop searching when the \fIn\fPth structure has been found.  The default is 1.
+.TP
+.B \-t \fIn
+Stop searching after \fIn\fP seconds.
+.TP
+.B \-s \fIn
+Allow at most \fIn\fP seconds for each domain size. The parameter can be used (together with \fB-t\fP) to give an overall time limit.
+.TP
+.B \-b \fIn
+Stop searching when (about) \fIn\fP megabytes of memory have been used.
+.TP
+.B \-V \fIn
+A rule is needed for distinguishing variables from constants in clauses and formulas with free variables. If this flag is clear, variables start with (lower case) `u' through `z'. If this flag is set, variables in clauses start with (upper case) `A' through `Z' or `_'.
+.TP
+.B \-P \fIn
+If this flag is set, all structures that are found are printed in `standard' form, which means they are suitable as input to other LADR programs such as
+.BR isofilter (1)
+and
+.BR interpformat (1).
+.TP
+.B \-p \fIn
+If this flag is set, and if \fB-P\fP is clear, all structures that are found are printed in a tabular form.
+.TP
+.B \-R \fIn
+If this flag is set, a ring structure is is applied to the search. The operations {+,-,*} are assumed to be the ring of integers (mod domain_size). This method puts a tight constraint on the search, allowing much larger structures to be investigated.
+.TP
+.B \-v \fIn
+If this flag is set, the output file receives information about the search, including the initial partial model (the part of the model that can be determined before backtracking starts) and timing and other statistics for each domain size. (It does not give a trace of the backtracking, so it does not consume a lot of file space.) 
+.TP
+.B \-T \fIn
+If the trace flag is set, detailed information about the search, including a trace of all assignments and backtracking, is printed to the standard output. This flag causes a lot of output, so it should be used only on small searches.
+.PP
+There also exist a number of advanced options, which are used for experimentation with search methods. They can be ignored by nearly all users. For descriptions of these options, see the original \fBmace4\fP manual.
+.SH SEE ALSO
+.BR prover9 (1).
+.br
+Full documentation for \fBmace4\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.br
+The original \fBmace4\fP manual, which can be downloaded at http://www.cs.unm.edu/~mccune/prover9/mace4.pdf
+.SH AUTHOR
+\fBmace4\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/prooftrans.1
+++ ladr-0.0.200806a/debian/prooftrans.1
@@ -0,0 +1,80 @@
+.TH PROOFTRANS 1 "January 20, 2007"
+.SH NAME
+prooftrans - tool for transforming Prover9 proofs
+.SH SYNOPSIS
+.B prooftrans
+.RI [ parents_only ]
+.RI [ expand ]
+.RI [ renumber ]
+.RI [ striplabels ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+xml
+.RI [ expand ]
+.RI [ renumber ]
+.RI [ striplabels ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+ivy
+.RI [ renumber ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+hints
+[\fI-label label\fP]
+.RI [ expand ]
+.RI [ striplabels ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+tagged
+[\fI-f file\fP]
+.SH DESCRIPTION
+This manual page documents briefly the
+.B prooftrans
+command.
+.PP
+\fBprooftrans\fP can extract proofs from
+.BR prover9 (1)
+output files and transform them in various ways.
+
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B renumber
+Renumber steps.
+.TP
+.B parents_only
+Simplify justifications by listing only parents.
+.TP
+.B expand
+Expand all steps, turning secondary justifications into explicit steps.
+.TP
+.B xml
+Produce proofs in XML.
+.TP
+.B ivy
+Produce proofs for checking by the IVY proof checker.
+.TP
+.B hints
+Produce hints for guiding subsequent searches.
+.TP
+.B tagged
+Produce proofs in a structured tagged format.
+.TP
+.B \-label \fIlabel\fP
+Attach label attributes to the hint clauses consisting of the string \fIlabel\fP and a sequence number generated by prooftrans.
+.TP
+.B \-f \fIfile
+Take input from \fIfile\fP instead of from standard input.
+.SH SEE ALSO
+.BR prover9 (1).
+.br
+Full documentation for \fBprooftrans\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBprooftrans\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/prover9.1
+++ ladr-0.0.200806a/debian/prover9.1
@@ -0,0 +1,52 @@
+.TH PROVER9 1 "August 12, 2007"
+.SH NAME
+prover9 \- resolution/paramodulation theorem prover
+.SH SYNOPSIS
+.B prover9
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.br
+.B prover9
+.RI [ options ]
+\-f
+.I input-file
+>
+.I output-file
+.SH DESCRIPTION
+This manual page documents briefly the
+.B prover9
+command.
+.PP
+\fBprover9\fP is an automated theorem prover for first-order and equational logic. It is a successor of the
+.BR otter (1)
+prover.  \fBprover9\fP uses the inference techniques of ordered resolution and paramodulation with literal selection.
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B \-h
+View a list of command-line options.
+.TP
+.B \-x
+Enables an experimental enhanced auto-mode.  For more information consult the \fBprover9\fP manual.
+.TP
+.B \-p
+Fully parenthesize output.
+.TP
+.B \-t \fIn
+Constrain the search to last about \fIn\fP seconds.  For UNIX-like systems, the `user CPU' time is used.
+.TP
+.B \-f \fIfile
+Take input from \fIfile\fP instead of from standard input.
+.SH SEE ALSO
+.BR mace4 (1),
+.BR otter (1).
+.br
+On Debian systems, the manual is found in the \fIprover9-doc\fP package, at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBprover9\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/prover9.dirs
+++ ladr-0.0.200806a/debian/prover9.dirs
@@ -0,0 +1 @@
+usr/bin
--- ladr-0.0.200806a.orig/debian/prover9.examples
+++ ladr-0.0.200806a/debian/prover9.examples
@@ -0,0 +1,2 @@
+prover9.examples
+mace4.examples
--- ladr-0.0.200806a.orig/debian/prover9.install
+++ ladr-0.0.200806a/debian/prover9.install
@@ -0,0 +1,7 @@
+bin/prover9 usr/bin
+bin/prooftrans usr/bin
+bin/mace4 usr/bin
+bin/isofilter usr/bin
+bin/isofilter0 usr/bin
+bin/isofilter2 usr/bin
+bin/interpformat usr/bin
--- ladr-0.0.200806a.orig/debian/prover9.links
+++ ladr-0.0.200806a/debian/prover9.links
@@ -0,0 +1,2 @@
+usr/share/man/man1/isofilter.1.gz usr/share/man/man1/isofilter0.1.gz
+usr/share/man/man1/isofilter.1.gz usr/share/man/man1/isofilter2.1.gz
--- ladr-0.0.200806a.orig/debian/prover9.manpages
+++ ladr-0.0.200806a/debian/prover9.manpages
@@ -0,0 +1,5 @@
+debian/prover9.1
+debian/prooftrans.1
+debian/mace4.1
+debian/isofilter.1
+debian/interpformat.1
--- ladr-0.0.200806a.orig/debian/rewriter.1
+++ ladr-0.0.200806a/debian/rewriter.1
@@ -0,0 +1,60 @@
+.de Sp \" Vertical space (when we can't use .PP)
+.if t .sp .5v
+.if n .sp
+..
+.de Vb \" Begin verbatim text
+.ft CW
+.nf
+.ne \\$1
+..
+.de Ve \" End verbatim text
+.ft R
+.fi
+..
+.TH REWRITER 1 "January 20, 2007"
+.SH NAME
+rewriter - demodulate terms
+.SH SYNOPSIS
+.B rewriter
+.RI < demodulators-file >
+<
+.RI < terms-file >
+>
+.RI < rewritten-terms-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B rewriter
+command.
+.PP
+Rewrite a stream of \fIterms\fP with a list of \fIdemodulators\fP. The
+demodulators are used left-to-right as given, and they are not checked
+for termination.
+.SH SYNTAX
+The file of demodulators contains optional commands
+then a list of demodulators.  The commands can be used to
+declare infix operations and associativity/commutativity.
+Example file of demodulators:
+.Sp
+.Vb 10
+\&    op(400, infix, ^).
+\&    op(400, infix, v).
+\&    assoc_comm(^).
+\&    assoc_comm(v).
+\&    formulas(demodulators).
+\&    x ^ x = x.
+\&    x ^ (x v y) = x.
+\&    x v x = x.
+\&    x v (x ^ y) = x.
+\&    end_of_list.
+.Ve
+.Sp
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBrewriter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBrewriter\fP was written by William McCune <mccune@cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
--- ladr-0.0.200806a.orig/debian/rules
+++ ladr-0.0.200806a/debian/rules
@@ -0,0 +1,72 @@
+#!/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
+
+include /usr/share/dpatch/dpatch.make
+
+CFLAGS = -Wall -g
+
+ifneq (,$(findstring noopt,$(DEB_BUILD_OPTIONS)))
+	CFLAGS += -O0
+else
+	CFLAGS += -O2
+endif
+
+build: build-stamp
+build-stamp: patch
+	dh_testdir
+
+	$(MAKE) all CFLAGS="$(CFLAGS)"
+
+	touch $@
+
+clean: clean-patched unpatch
+clean-patched:
+	dh_testdir
+	dh_testroot
+	rm -f build-stamp
+
+	$(MAKE) realclean
+
+	dh_clean 
+
+install: build
+	dh_testdir
+	dh_testroot
+	dh_clean -k 
+	dh_installdirs
+
+	mkdir -p debian/tmp/usr/lib
+	libtool --mode=install cp -a ladr/libladr.la `pwd`/debian/tmp/usr/lib
+
+binary-indep: build install
+
+binary-arch: build install
+	dh_testdir
+	dh_testroot
+	dh_installchangelogs Changelog
+	dh_installdocs
+	dh_installexamples
+	find debian/*/usr/share/doc -size 0 -exec rm -f \{\} \;
+	dh_install
+	dh_installman
+	dh_link
+	dh_strip
+	dh_compress
+	dh_fixperms
+	dh_makeshlibs -V
+	dh_installdeb
+	dh_shlibdeps
+	dh_gencontrol
+	dh_md5sums
+	dh_builddeb
+
+binary: binary-indep binary-arch
+.PHONY: build clean binary-indep binary-arch binary install patch unpatch clean-patch
--- ladr-0.0.200806a.orig/debian/watch
+++ ladr-0.0.200806a/debian/watch
@@ -0,0 +1,4 @@
+version=3
+
+# Converts an LADR version number of the form March-2007A into the form 0.0.200703a, or 2008-04A into the form 0.0.200804a
+opts="uversionmangle=s/Jan[^-]*/01/;s/Feb[^-]*/02/;s/Mar[^-]*/03/;s/Apr[^-]*/04/;s/May/05/;s/Jun[^-]*/06/;s/Jul[^-]*/07/;s/Aug[^-]*/08/;s/Sep[^-]*/09/;s/Oct[^-]*/10/;s/Nov[^-]*/11/;s/Dec[^-]*/12/;s/([0-9]{2})-([0-9]{4})([A-Z]?)/'0.0.'.$2.$1.lc($3)/e;s/([0-9]{4})-([0-9]{2})([A-Z]?)/'0.0.'.$1.$2.lc($3)/e" http://www.cs.unm.edu/~mccune/mace4/download/ LADR-(.*).tar.gz
--- ladr-0.0.200806a.orig/debian/patches/00list
+++ ladr-0.0.200806a/debian/patches/00list
@@ -0,0 +1,2 @@
+01-libtoolise.dpatch
+03-no-2.5isms.dpatch
--- ladr-0.0.200806a.orig/debian/patches/01-libtoolise.dpatch
+++ ladr-0.0.200806a/debian/patches/01-libtoolise.dpatch
@@ -0,0 +1,579 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## 01-libtoolise.dpatch by  <pcc03@doc.ic.ac.uk>
+##
+## DP: Libtoolises the makefiles, corrects list of scripts,
+## DP: removes -lm where not necessary
+
+@DPATCH@
+diff -urNad ladr-0.0.200804a~/Makefile ladr-0.0.200804a/Makefile
+--- ladr-0.0.200804a~/Makefile	2007-10-22 22:33:12.000000000 +0100
++++ ladr-0.0.200804a/Makefile	2008-04-08 16:43:25.000000000 +0100
+@@ -2,11 +2,12 @@
+ 	@echo See README.make
+ 
+ all:
+-	cd ladr         && $(MAKE) lib
++	cd ladr         && $(MAKE) lib XFLAGS=-D_REENTRANT
+ 	cd mace4.src    && $(MAKE) all
+ 	cd provers.src  && $(MAKE) all
+ 	cd apps.src     && $(MAKE) all
+-	/bin/cp -p utilities/* bin
++	/bin/cp -p utilities/attack utilities/get_givens utilities/get_interps utilities/get_kept utilities/gvizify utilities/looper utilities/prover9-mace4 bin
++	chmod 755 bin/gvizify
+ 	@echo ""
+ 	@echo "**** Now try 'make test1'. ****"
+ 	@echo ""
+diff -urNad ladr-0.0.200804a~/apps.src/Makefile ladr-0.0.200804a/apps.src/Makefile
+--- ladr-0.0.200804a~/apps.src/Makefile	2008-03-11 15:44:18.000000000 +0000
++++ ladr-0.0.200804a/apps.src/Makefile	2008-04-08 16:52:31.000000000 +0100
+@@ -16,16 +16,16 @@
+ all: ladr apps install realclean
+ 
+ ladr:
+-	cd ../ladr && $(MAKE) libladr.a
++	cd ../ladr && $(MAKE) libladr.la
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o $(PROGRAMS)
++	libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
+ 
+ install:
+-	/bin/mv $(PROGRAMS) ../bin
++	libtool --mode=install /bin/cp $(PROGRAMS) `pwd`/../bin
+ 
+ tags:
+ 	etags *.c ../ladr/*.c
+@@ -33,73 +33,73 @@
+ apps: $(PROGRAMS)
+ 
+ test: test.o
+-	$(CC) $(CFLAGS) -o test test.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o test test.o ../ladr/libladr.la
+ 
+ interpformat: interpformat.o
+-	$(CC) $(CFLAGS) -o interpformat interpformat.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o interpformat interpformat.o ../ladr/libladr.la
+ 
+ prooftrans: prooftrans.o
+-	$(CC) $(CFLAGS) -o prooftrans prooftrans.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o prooftrans prooftrans.o ../ladr/libladr.la
+ 
+ directproof: directproof.o
+-	$(CC) $(CFLAGS) -o directproof directproof.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o directproof directproof.o ../ladr/libladr.la
+ 
+ test_clause_eval: test_clause_eval.o
+-	$(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.la
+ 
+ latfilter: latfilter.o
+-	$(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.la
+ 
+ olfilter: olfilter.o
+-	$(CC) $(CFLAGS) -o olfilter olfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o olfilter olfilter.o ../ladr/libladr.la
+ 
+ unfast: unfast.o
+-	$(CC) $(CFLAGS) -o unfast unfast.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o unfast unfast.o ../ladr/libladr.la
+ 
+ upper-covers: upper-covers.o
+-	$(CC) $(CFLAGS) -o upper-covers upper-covers.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o upper-covers upper-covers.o ../ladr/libladr.la
+ 
+ miniscope: miniscope.o
+-	$(CC) $(CFLAGS) -o miniscope miniscope.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o miniscope miniscope.o ../ladr/libladr.la
+ 
+ isofilter0: isofilter0.o
+-	$(CC) $(CFLAGS) -o isofilter0 isofilter0.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o isofilter0 isofilter0.o ../ladr/libladr.la
+ 
+ isofilter: isofilter.o
+-	$(CC) $(CFLAGS) -o isofilter isofilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o isofilter isofilter.o ../ladr/libladr.la
+ 
+ isofilter2: isofilter2.o
+-	$(CC) $(CFLAGS) -o isofilter2 isofilter2.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o isofilter2 isofilter2.o ../ladr/libladr.la
+ 
+ dprofiles: dprofiles.o
+-	$(CC) $(CFLAGS) -o dprofiles dprofiles.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o dprofiles dprofiles.o ../ladr/libladr.la
+ 
+ renamer: renamer.o
+-	$(CC) $(CFLAGS) -o renamer renamer.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o renamer renamer.o ../ladr/libladr.la
+ 
+ rewriter: rewriter.o
+-	$(CC) $(CFLAGS) -o rewriter rewriter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o rewriter rewriter.o ../ladr/libladr.la
+ 
+ idfilter: idfilter.o
+-	$(CC) $(CFLAGS) -o idfilter idfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o idfilter idfilter.o ../ladr/libladr.la
+ 
+ clausefilter: clausefilter.o
+-	$(CC) $(CFLAGS) -o clausefilter clausefilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o clausefilter clausefilter.o ../ladr/libladr.la
+ 
+ interpfilter: interpfilter.o
+-	$(CC) $(CFLAGS) -o interpfilter interpfilter.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o interpfilter interpfilter.o ../ladr/libladr.la
+ 
+ clausetester: clausetester.o
+-	$(CC) $(CFLAGS) -o clausetester clausetester.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o clausetester clausetester.o ../ladr/libladr.la
+ 
+ mirror-flip: mirror-flip.o
+-	$(CC) $(CFLAGS) -o mirror-flip mirror-flip.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o mirror-flip mirror-flip.o ../ladr/libladr.la
+ 
+ perm3: perm3.o
+-	$(CC) $(CFLAGS) -o perm3 perm3.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o perm3 perm3.o ../ladr/libladr.la
+ 
+ sigtest: sigtest.o
+-	$(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.la
+ 
+ 
+ 
+diff -urNad ladr-0.0.200804a~/ladr/Makefile ladr-0.0.200804a/ladr/Makefile
+--- ladr-0.0.200804a~/ladr/Makefile	2008-04-04 22:25:31.000000000 +0100
++++ ladr-0.0.200804a/ladr/Makefile	2008-04-08 16:49:19.000000000 +0100
+@@ -4,53 +4,56 @@
+ 
+ # XFLAGS can be specified on the command line (see XFLAGS below)
+ 
+-CFLAGS = $(XFLAGS) -O -Wall
+-# CFLAGS = $(XFLAGS) -O6 -Wall
+-# CFLAGS = $(XFLAGS) -g  -O -Wall
+-# CFLAGS = $(XFLAGS) -g -O0 -Wall
+-# CFLAGS = $(XFLAGS) -pg -O -Wall
+-# CFLAGS = $(XFLAGS)  -Wall -pedantic
++CFLAGS = -O -Wall
++# CFLAGS = -O6 -Wall
++# CFLAGS = -g  -O -Wall
++# CFLAGS = -g -O0 -Wall
++# CFLAGS = -pg -O -Wall
++# CFLAGS =  -Wall -pedantic
+ 
+-BASE_OBJ = order.o clock.o nonport.o\
+-	   fatal.o ibuffer.o memory.o hash.o string.o strbuf.o\
+-           glist.o options.o symbols.o avltree.o
+-TERM_OBJ = term.o termflag.o listterm.o tlist.o flatterm.o multiset.o\
+-	   termorder.o parse.o accanon.o
+-UNIF_OBJ = unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o\
+-           dioph.o btu.o btm.o mindex.o basic.o attrib.o
+-CLAS_OBJ = formula.o definitions.o literals.o topform.o clist.o\
+-	   clauseid.o clauses.o\
+-	   just.o cnf.o clausify.o parautil.o\
+-           pindex.o compress.o\
+-           maximal.o lindex.o weight.o weight2.o\
+-           int_code.o features.o di_tree.o fastparse.o\
+-           random.o subsume.o clause_misc.o clause_eval.o
+-INFE_OBJ = flatdemod.o demod.o clash.o resolve.o paramod.o\
+-           backdemod.o\
+-           hints.o ac_redun.o xproofs.o ivy.o
+-MODL_OBJ = interp.o
+-MISC_OBJ = std_options.o banner.o ioutil.o tptp_trans.o top_input.o
++BASE_OBJ = order.lo clock.lo nonport.lo\
++	   fatal.lo ibuffer.lo memory.lo hash.lo string.lo strbuf.lo\
++           glist.lo options.lo symbols.lo avltree.lo
++TERM_OBJ = term.lo termflag.lo listterm.lo tlist.lo flatterm.lo multiset.lo\
++	   termorder.lo parse.lo accanon.lo
++UNIF_OBJ = unify.lo fpalist.lo fpa.lo discrim.lo discrimb.lo discrimw.lo\
++           dioph.lo btu.lo btm.lo mindex.lo basic.lo attrib.lo
++CLAS_OBJ = formula.lo definitions.lo literals.lo topform.lo clist.lo\
++	   clauseid.lo clauses.lo\
++	   just.lo cnf.lo clausify.lo parautil.lo\
++           pindex.lo compress.lo\
++           maximal.lo lindex.lo weight.lo weight2.lo\
++           int_code.lo features.lo di_tree.lo fastparse.lo\
++           random.lo subsume.lo clause_misc.lo clause_eval.lo
++INFE_OBJ = flatdemod.lo demod.lo clash.lo resolve.lo paramod.lo\
++           backdemod.lo\
++           hints.lo ac_redun.lo xproofs.lo ivy.lo
++MODL_OBJ = interp.lo
++MISC_OBJ = std_options.lo banner.lo ioutil.lo tptp_trans.lo top_input.lo
+ 
+ 
+ OBJECTS = $(BASE_OBJ) $(TERM_OBJ) $(UNIF_OBJ) $(CLAS_OBJ)\
+           $(INFE_OBJ) $(MODL_OBJ) $(MISC_OBJ)
+ 
+-libladr.a: $(OBJECTS)
+-	$(AR) rs libladr.a $(OBJECTS)
++libladr.la: $(OBJECTS)
++	libtool --mode=link gcc -shared -rpath /usr/lib -version-info 4:0:0 -o libladr.la $(OBJECTS) -lm
++
++%.lo: %.c
++	libtool --mode=compile gcc -c $(CFLAGS) $(XFLAGS) -o $@ $<
+ 
+ ##############################################################################
+ 
+ lib ladr libladr:
+-	$(MAKE) libladr.a
++	$(MAKE) libladr.la
+ 
+ dep:
+ 	util/make_dep $(OBJECTS)
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.lo
+ 
+ realclean:
+-	/bin/rm -f *.o *.a
++	libtool --mode=clean /bin/rm -f *.lo *.la
+ 
+ protos:
+ 	util/make_protos $(OBJECTS)
+@@ -67,150 +70,150 @@
+ 
+ # The rest of the file is generated automatically by util/make_dep
+ 
+-order.o:   	order.h 
++order.lo:   	order.h 
+ 
+-clock.o:   	clock.h string.h memory.h fatal.h header.h
++clock.lo:   	clock.h string.h memory.h fatal.h header.h
+ 
+-nonport.o:   	nonport.h 
++nonport.lo:   	nonport.h 
+ 
+-fatal.o:   	fatal.h header.h
++fatal.lo:   	fatal.h header.h
+ 
+-ibuffer.o:   	ibuffer.h fatal.h header.h
++ibuffer.lo:   	ibuffer.h fatal.h header.h
+ 
+-memory.o:   	memory.h fatal.h header.h
++memory.lo:   	memory.h fatal.h header.h
+ 
+-hash.o:   	hash.h memory.h fatal.h header.h
++hash.lo:   	hash.h memory.h fatal.h header.h
+ 
+-string.o:   	string.h memory.h fatal.h header.h
++string.lo:   	string.h memory.h fatal.h header.h
+ 
+-strbuf.o:   	strbuf.h string.h memory.h fatal.h header.h
++strbuf.lo:   	strbuf.h string.h memory.h fatal.h header.h
+ 
+-glist.o:   	glist.h order.h string.h memory.h fatal.h header.h
++glist.lo:   	glist.h order.h string.h memory.h fatal.h header.h
+ 
+-options.o:   	options.h string.h memory.h fatal.h header.h
++options.lo:   	options.h string.h memory.h fatal.h header.h
+ 
+-symbols.o:   	symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++symbols.lo:   	symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-avltree.o:   	avltree.h memory.h order.h fatal.h header.h
++avltree.lo:   	avltree.h memory.h order.h fatal.h header.h
+ 
+-term.o:   	term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++term.lo:   	term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-termflag.o:   	termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++termflag.lo:   	termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-listterm.o:   	listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++listterm.lo:   	listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-tlist.o:   	tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++tlist.lo:   	tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-flatterm.o:   	flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++flatterm.lo:   	flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-multiset.o:   	multiset.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++multiset.lo:   	multiset.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-termorder.o:   	termorder.h flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++termorder.lo:   	termorder.h flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-parse.o:   	parse.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++parse.lo:   	parse.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-accanon.o:   	accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++accanon.lo:   	accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ 
+-unify.o:   	unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++unify.lo:   	unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-fpalist.o:   	fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++fpalist.lo:   	fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-fpa.o:   	fpa.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++fpa.lo:   	fpa.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-discrim.o:   	discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++discrim.lo:   	discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-discrimb.o:   	discrimb.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++discrimb.lo:   	discrimb.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-discrimw.o:   	discrimw.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++discrimw.lo:   	discrimw.h discrim.h unify.h index.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-dioph.o:   	dioph.h 
++dioph.lo:   	dioph.h 
+ 
+-btu.o:   	btu.h dioph.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++btu.lo:   	btu.h dioph.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-btm.o:   	btm.h unify.h accanon.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termflag.h termorder.h flatterm.h
++btm.lo:   	btm.h unify.h accanon.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termflag.h termorder.h flatterm.h
+ 
+-mindex.o:   	mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
++mindex.lo:   	mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+ 
+-basic.o:   	basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++basic.lo:   	basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-attrib.o:   	attrib.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++attrib.lo:   	attrib.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-formula.o:   	formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++formula.lo:   	formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ 
+-definitions.o:   	definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h termflag.h parse.h
++definitions.lo:   	definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h termflag.h parse.h
+ 
+-literals.o:   	literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++literals.lo:   	literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-topform.o:   	topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++topform.lo:   	topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-clist.o:   	clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++clist.lo:   	clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-clauseid.o:   	clauseid.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++clauseid.lo:   	clauseid.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-clauses.o:   	clauses.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++clauses.lo:   	clauses.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-just.o:   	just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++just.lo:   	just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-cnf.o:   	cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++cnf.lo:   	cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ 
+-clausify.o:   	clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h
++clausify.lo:   	clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h
+ 
+-parautil.o:   	parautil.h 
++parautil.lo:   	parautil.h 
+ 
+-pindex.o:   	pindex.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++pindex.lo:   	pindex.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-compress.o:   	compress.h parautil.h
++compress.lo:   	compress.h parautil.h
+ 
+-maximal.o:   	maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++maximal.lo:   	maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ 
+-lindex.o:   	lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
++lindex.lo:   	lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
+ 
+-weight.o:   	weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h
++weight.lo:   	weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h
+ 
+-int_code.o:   	int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++int_code.lo:   	int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-features.o:   	features.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
++features.lo:   	features.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+ 
+-di_tree.o:   	di_tree.h features.h topform.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h attrib.h formula.h maximal.h unify.h listterm.h termorder.h hash.h flatterm.h
++di_tree.lo:   	di_tree.h features.h topform.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h attrib.h formula.h maximal.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-fastparse.o:   	fastparse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++fastparse.lo:   	fastparse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-random.o:   	random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++random.lo:   	random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-subsume.o:   	subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
++subsume.lo:   	subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
+ 
+-clause_misc.o:   	clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h
++clause_misc.lo:   	clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h
+ 
+-clause_eval.o:   	clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
++clause_eval.lo:   	clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+ 
+-flatdemod.o:   	flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
++flatdemod.lo:   	flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+ 
+-demod.o:   	demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
++demod.lo:   	demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+ 
+-clash.o:   	clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
++clash.lo:   	clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h
+ 
+-resolve.o:   	resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
++resolve.lo:   	resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
+ 
+-paramod.o:   	paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
++paramod.lo:   	paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
+ 
+-backdemod.o:   	backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
++backdemod.lo:   	backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
+ 
+-hints.o:   	hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
++hints.lo:   	hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termflag.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
+ 
+-ac_redun.o:   	ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
++ac_redun.lo:   	ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ 
+-xproofs.o:   	xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
++xproofs.lo:   	xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
+ 
+-ivy.o:   	ivy.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
++ivy.lo:   	ivy.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
+ 
+-interp.o:   	interp.h parse.h topform.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h
++interp.lo:   	interp.h parse.h topform.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h
+ 
+-std_options.o:   	std_options.h options.h symbols.h clock.h string.h memory.h fatal.h header.h strbuf.h glist.h order.h
++std_options.lo:   	std_options.h options.h symbols.h clock.h string.h memory.h fatal.h header.h strbuf.h glist.h order.h
+ 
+-banner.o:   	banner.h nonport.h clock.h string.h memory.h fatal.h header.h
++banner.lo:   	banner.h nonport.h clock.h string.h memory.h fatal.h header.h
+ 
+-ioutil.o:   	ioutil.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
++ioutil.lo:   	ioutil.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
+ 
+-tptp_trans.o:   	tptp_trans.h ioutil.h clausify.h parse.h fastparse.h ivy.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
++tptp_trans.lo:   	tptp_trans.h ioutil.h clausify.h parse.h fastparse.h ivy.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
+ 
+-top_input.o:   	top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h
++top_input.lo:   	top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h
+diff -urNad ladr-0.0.200804a~/mace4.src/Makefile ladr-0.0.200804a/mace4.src/Makefile
+--- ladr-0.0.200804a~/mace4.src/Makefile	2007-10-05 05:00:39.000000000 +0100
++++ ladr-0.0.200804a/mace4.src/Makefile	2008-04-08 16:43:25.000000000 +0100
+@@ -25,11 +25,11 @@
+ 	$(MAKE) libmace4.a
+ 
+ ladr:
+-	cd ../ladr && $(MAKE) libladr.a
++	cd ../ladr && $(MAKE) libladr.la
+ 	$(MAKE) clean
+ 
+ mace4: libmace4.a mace4.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.la
+ 
+ $(OBJECTS): estack.h syms.h ground.h propagate.h mstate.h msearch.h
+ 
+@@ -37,10 +37,10 @@
+ 	etags *.c ../ladr/*.c
+ 
+ clean:
+-	/bin/rm -f *.o
++	libtool --mode=clean /bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o *.a mace4
++	libtool --mode=clean /bin/rm -f *.o *.a mace4
+ 
+ install:
+-	/bin/mv mace4 ../bin
++	libtool --mode=install /bin/cp mace4 `pwd`/../bin
+diff -urNad ladr-0.0.200804a~/provers.src/Makefile ladr-0.0.200804a/provers.src/Makefile
+--- ladr-0.0.200804a~/provers.src/Makefile	2008-04-04 22:27:24.000000000 +0100
++++ ladr-0.0.200804a/provers.src/Makefile	2008-04-08 16:43:25.000000000 +0100
+@@ -41,13 +41,13 @@
+ 	$(MAKE) clean
+ 
+ install:
+-	/bin/cp -p $(PROGRAMS) ../bin
++	libtool --mode=install /bin/cp -p $(PROGRAMS) `pwd`/../bin
+ 
+ clean:
+ 	/bin/rm -f *.o
+ 
+ realclean:
+-	/bin/rm -f *.o $(PROGRAMS)
++	libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
+ 
+ protos:
+ 	util/make_protos $(OBJECTS)
+@@ -63,34 +63,34 @@
+ 	$(MAKE) prover9
+ 
+ prover9: prover9.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.la
+ 
+ fof-prover9: fof-prover9.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.la
+ 
+ ladr_to_tptp: ladr_to_tptp.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.la
+ 
+ tptp_to_ladr: tptp_to_ladr.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.la
+ 
+ autosketches4: autosketches4.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.la
+ 
+ newauto: newauto.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o newauto newauto.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o newauto newauto.o $(OBJECTS) ../ladr/libladr.la
+ 
+ newsax: newsax.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -lm -o newsax newsax.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o newsax newsax.o $(OBJECTS) ../ladr/libladr.la
+ 
+ cgrep: cgrep.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.la
+ 
+ mprover: mprover.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.a ../mace4.src/libmace4.a
++	libtool --mode=link $(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.la ../mace4.src/libmace4.a
+ 
+ iterate4: iterate4.o $(OBJECTS)
+-	$(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.a
++	libtool --mode=link $(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.la
+ 
+ prover9.o mprover.o iterate4.o autosketches4.o fof-prover9.o: search.h utilities.h  forward_subsume.h giv_select.h white_black.h demodulate.h actions.h index_lits.h pred_elim.h unfold.h provers.h
+ 
+diff -urNad ladr-0.0.200804a~/test.src/Makefile ladr-0.0.200804a/test.src/Makefile
+--- ladr-0.0.200804a~/test.src/Makefile	2007-03-06 20:27:59.000000000 +0000
++++ ladr-0.0.200804a/test.src/Makefile	2008-04-08 16:43:25.000000000 +0100
+@@ -17,7 +17,7 @@
+ 
+ ladr:
+ 	make clean
+-	cd ../ladr && $(MAKE) libladr.a
++	cd ../ladr && $(MAKE) libladr.la
+ 
+ clean:
+ 	/bin/rm -f *.o
+@@ -31,8 +31,8 @@
+ apps: $(PROGRAMS)
+ 
+ avltest: avltest.o
+-	$(CC) $(CFLAGS) -o avltest avltest.o ../ladr/libladr.a -lm
++	libtool --mode=link $(CC) $(CFLAGS) -o avltest avltest.o ../ladr/libladr.la -lm
+ 
+ tptp_test: tptp_test.o
+-	$(CC) $(CFLAGS) -o tptp_test tptp_test.o ../ladr/libladr.a -lm
++	libtool --mode=link $(CC) $(CFLAGS) -o tptp_test tptp_test.o ../ladr/libladr.la -lm
+ 
--- ladr-0.0.200806a.orig/debian/patches/03-no-2.5isms.dpatch
+++ ladr-0.0.200806a/debian/patches/03-no-2.5isms.dpatch
@@ -0,0 +1,22 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## no-python2.5isms.dpatch by  <peter@xenon.peter.uk.to>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Removes Python 2.5isms from utility scripts, namely gvizify.
+
+@DPATCH@
+diff -urNad ladr-0.0.200712~/utilities/gvizify ladr-0.0.200712/utilities/gvizify
+--- ladr-0.0.200712~/utilities/gvizify	2008-01-24 20:57:07.000000000 +0000
++++ ladr-0.0.200712/utilities/gvizify	2008-01-24 20:58:24.000000000 +0000
+@@ -208,7 +208,10 @@
+   if options.multipage:
+     print " page=\"%s\";" % (options.size,)
+   else:
+-    force="" if options.relax else "!"
++    if options.relax:
++      force=""
++    else:
++      force="!"
+     print " size=\"%s%s\";" % (options.size, force)
+   print " margin=\"%s\";" % (options.margin,)
+   if options.command != "":