The package rpms/prover9.git has added or updated architecture specific content in its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/prover9.git/commit/?id=172bd8841c....
Change:
-ExcludeArch: ppc64
Thanks.
Full change:
============
commit 172bd8841cced4143170b5017f704c042cc27eed
Author: Miro Hronok <miro(a)hroncok.cz>
Date: Mon May 20 11:32:01 2019 +0200
Orphaned for 6+ weeks
diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index 95d79a7..0000000
--- a/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-LADR-2008-05A.tar.gz
-prover9-manual-2008-05A.tar.gz
-LADR-2009-11A.tar.gz
-prover9-manual-2009-11A.tar.gz
diff --git a/dead.package b/dead.package
new file mode 100644
index 0000000..5204a84
--- /dev/null
+++ b/dead.package
@@ -0,0 +1 @@
+Orphaned for 6+ weeks
diff --git a/format-fix.patch b/format-fix.patch
deleted file mode 100644
index e880d4c..0000000
--- a/format-fix.patch
+++ /dev/null
@@ -1,48 +0,0 @@
---- ladr/fastparse.c.orig 2015-07-27 10:15:11.423522124 -0500
-+++ ladr/fastparse.c 2015-07-27 10:16:48.745891297 -0500
-@@ -183,8 +183,8 @@
- Pos = 0;
- t = fast_parse(s);
- if (s[Pos] != '.') {
-- fprintf(stderr, s);
-- fprintf(stdout, s);
-+ fprintf(stderr, "%s", s);
-+ fprintf(stdout, "%s", s);
- fatal_error("fast_read_term, term ends before period.");
- }
- return t;
---- mace4.src/print.c.orig 2015-07-27 10:23:08.719183948 -0500
-+++ mace4.src/print.c 2015-07-27 10:25:31.202292819 -0500
-@@ -111,12 +111,12 @@
- printf(s1, i);
- printf("\n ---");
- for (i = 0; i < n; i++)
-- printf(s2);
-+ printf("%s", s2);
- printf("\n ");
- for (i = 0; i < n; i++) {
- int v = f1_val(p->base, i);
- if (v < 0)
-- printf(s3);
-+ printf("%s", s3);
- else
- printf(s1, v);
- }
-@@ -134,7 +134,7 @@
- printf(s1, i);
- printf("\n --+");
- for (i = 0; i < n; i++)
-- printf(s2);
-+ printf("%s", s2);
- printf("\n");
-
- for (i = 0; i < n; i++) {
-@@ -142,7 +142,7 @@
- for (j = 0; j < n; j++) {
- int v = f2_val(p->base, i, j);
- if (v < 0)
-- printf(s3);
-+ printf("%s", s3);
- else
- printf(s1, v);
- }
diff --git a/prover9-fedora.patch b/prover9-fedora.patch
deleted file mode 100644
index 5e78ea6..0000000
--- a/prover9-fedora.patch
+++ /dev/null
@@ -1,191 +0,0 @@
---- utilities/attack 2007-02-09 23:19:40.000000000 +0000
-+++ utilities/attack.fedora 2008-01-31 14:48:50.000000000 +0000
-@@ -1,5 +1,22 @@
- #!/usr/bin/python
-
-+# Copyright (C) 2006, 2007 William McCune
-+#
-+# This file is part of the LADR Deduction Library.
-+#
-+# 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.
-+
- # This script takes a Mace4 input file (the head) and a stream of
- # candidates. It builds a list of models (M) of the candidates w.r.t.
- # the clauses in the head.
---- utilities/looper 2007-05-30 20:04:08.000000000 +0100
-+++ utilities/looper.fedora 2008-01-31 14:48:56.000000000 +0000
-@@ -1,5 +1,22 @@
- #!/usr/bin/python
-
-+# Copyright (C) 2006, 2007 William McCune
-+#
-+# This file is part of the LADR Deduction Library.
-+#
-+# 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.
-+
- # This script takes a (Prover9|Mace4) input file (the head), and
- # a stream of candidates. For each candidate, it appends the
- # candidate to the head, and then runs (Prover9|Mace4).
---- utilities/prover9-mace4 2007-09-03 21:02:36.000000000 +0100
-+++ utilities/prover9-mace4.fedora 2008-01-31 14:49:00.000000000 +0000
-@@ -1,5 +1,22 @@
- #!/usr/bin/python
-
-+# Copyright (C) 2006, 2007 William McCune
-+#
-+# This file is part of the LADR Deduction Library.
-+#
-+# 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.
-+
- # This script takes a Prover9 input file and runs Prover9 and Mace4
- # in parallel. If the one that finishes first finished with success,
- # its output is sent to stdout of this process.
---- README.first 2008-01-11 23:36:28.000000000 +0000
-+++ README.first.fedora 2008-06-18 14:58:41.000000000 +0100
-@@ -8,3 +8,58 @@
-
- for the HTML manual, examples, and updates.
-
-+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 provers.src/white_black.h, provers.src/giv_select.c,
-+provers.src/white_black.c, provers.src/giv_select.h, ladr/clause_eval.c,
-+ladr/tmp/definitions.c, ladr/tmp/multiset.c, ladr/clause_eval.h,
-+ladr/definitions.c, ladr/definitions.h, ladr/multiset.c, ladr/multiset.h:
-+
-+ The LADR Deduction Library 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.
-+
-+ 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.
-+
-+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.
-+
---- copyright 1970-01-01 01:00:00.000000000 +0100
-+++ copyright.fedora 2008-06-18 15:06:17.000000000 +0100
-@@ -0,0 +1,52 @@
-+This package was debianized by Peter Collingbourne <pcc03(a)doc.ic.ac.uk> on
-+Sat, 11 Aug 2007 23:22:34 +0100. It was converted for Fedora by Tim Colles
-+<timc(a)inf.ed.ac.uk> on 18/06/2008.
-+
-+It was downloaded from <
http://www.cs.unm.edu/~mccune/mace4/download/>
-+
-+Upstream Authors:
-+
-+ William McCune <mccune(a)cs.unm.edu>
-+ David A. Wheeler <dwheeler(a)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(a)doc.ic.ac.uk> and
-+is licensed under the GPL, see `/usr/share/common-licenses/GPL'.
diff --git a/prover9-manpages.patch b/prover9-manpages.patch
deleted file mode 100644
index 1e3e89b..0000000
--- a/prover9-manpages.patch
+++ /dev/null
@@ -1,470 +0,0 @@
-diff -Naur LADR-2008-04A.upstream/manpages/clausefilter.1
LADR-2008-04A/manpages/clausefilter.1
---- LADR-2008-04A.upstream/manpages/clausefilter.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/clausefilter.1 2008-06-18 10:26:17.000000000 +0100
-@@ -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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/clausetester.1
LADR-2008-04A/manpages/clausetester.1
---- LADR-2008-04A.upstream/manpages/clausetester.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/clausetester.1 2008-06-18 10:26:16.000000000 +0100
-@@ -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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/interpfilter.1
LADR-2008-04A/manpages/interpfilter.1
---- LADR-2008-04A.upstream/manpages/interpfilter.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/interpfilter.1 2008-06-18 10:26:17.000000000 +0100
-@@ -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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/interpformat.1
LADR-2008-04A/manpages/interpformat.1
---- LADR-2008-04A.upstream/manpages/interpformat.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/interpformat.1 2008-06-18 10:26:17.000000000 +0100
-@@ -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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/isofilter.1
LADR-2008-04A/manpages/isofilter.1
---- LADR-2008-04A.upstream/manpages/isofilter.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/isofilter.1 2008-06-18 10:26:16.000000000 +0100
-@@ -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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/mace4.1 LADR-2008-04A/manpages/mace4.1
---- LADR-2008-04A.upstream/manpages/mace4.1 2007-12-31 04:43:54.000000000 +0000
-+++ LADR-2008-04A/manpages/mace4.1 2008-06-18 10:26:16.000000000 +0100
-@@ -80,7 +80,7 @@
- .br
- The original \fBmace4\fP manual, which can be downloaded at
http://www.cs.unm.edu/~mccune/prover9/mace4.pdf
- .SH AUTHOR
--\fBmace4\fP ws written by William McCune <mccune(a)cs.unm.edu>
-+\fBmace4\fP was written by William McCune <mccune(a)cs.unm.edu>
- .PP
- This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
- for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/prooftrans.1
LADR-2008-04A/manpages/prooftrans.1
---- LADR-2008-04A.upstream/manpages/prooftrans.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/prooftrans.1 2008-06-18 10:26:16.000000000 +0100
-@@ -0,0 +1,73 @@
-+.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]
-+.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 \-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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/prover9.1 LADR-2008-04A/manpages/prover9.1
---- LADR-2008-04A.upstream/manpages/prover9.1 2007-12-31 04:43:54.000000000 +0000
-+++ LADR-2008-04A/manpages/prover9.1 2008-06-18 10:26:17.000000000 +0100
-@@ -11,7 +11,7 @@
- .br
- .B prover9
- .RI [ options ]
---f
-+\-f
- .I input-file
- >
- .I output-file
-@@ -38,15 +38,15 @@
- .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 \fIfiles
--Take input from \fIfiles\fP instead of from standard input.
-+.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 ws written by William McCune <mccune(a)cs.unm.edu>
-+\fBprover9\fP was written by William McCune <mccune(a)cs.unm.edu>
- .PP
- This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
- for the Debian project (but may be used by others).
-diff -Naur LADR-2008-04A.upstream/manpages/prover9-apps.1
LADR-2008-04A/manpages/prover9-apps.1
---- LADR-2008-04A.upstream/manpages/prover9-apps.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/prover9-apps.1 2008-06-18 11:40:34.000000000 +0100
-@@ -0,0 +1,17 @@
-+.TH PROVER9-APPS 1 "June 18, 2008"
-+.SH NAME
-+prover9-apps \- undocumented Prover9 applications
-+.SH DESCRIPTION
-+Some programs in the \fBprover9-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 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(a)cs.unm.edu>.
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others) and modified for Fedora
-+by Tim Colles <timc(a)inf.ed.ac.uk>.
-diff -Naur LADR-2008-04A.upstream/manpages/rewriter.1 LADR-2008-04A/manpages/rewriter.1
---- LADR-2008-04A.upstream/manpages/rewriter.1 1970-01-01 01:00:00.000000000 +0100
-+++ LADR-2008-04A/manpages/rewriter.1 2008-06-18 10:26:17.000000000 +0100
-@@ -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(a)cs.unm.edu>
-+.PP
-+This manual page was written by Peter Collingbourne <pcc03(a)doc.ic.ac.uk>,
-+for the Debian project (but may be used by others).
diff --git a/prover9-no-2.5isms.patch b/prover9-no-2.5isms.patch
deleted file mode 100644
index e439f99..0000000
--- a/prover9-no-2.5isms.patch
+++ /dev/null
@@ -1,15 +0,0 @@
-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 != "":
diff --git a/prover9.spec b/prover9.spec
deleted file mode 100644
index 7e4e570..0000000
--- a/prover9.spec
+++ /dev/null
@@ -1,289 +0,0 @@
-%define upstreamname LADR
-%define upstreamver 2009-11A
-
-Name: prover9
-Version: 200911a
-Release: 17%{?dist}
-Summary: Theorem Prover and Countermodel Generator
-
-# All files are GPLv2 except utilities/gvizify which is GPLv2+
-License: GPLv2 and GPLv2+
-URL:
http://www.cs.unm.edu/~mccune/prover9/
-Source0:
http://www.cs.unm.edu/~mccune/prover9/download/%{upstreamname}-%{upstream...
-Source1:
http://www.cs.unm.edu/~mccune/prover9/manual/%{name}-manual-%{upstreamver...
-Patch0: %{name}-no-2.5isms.patch
-Patch1: %{name}-manpages.patch
-Patch2: %{name}-fedora.patch
-Patch3: format-fix.patch
-BuildRequires: libtool
-
-# Fails test2 in check section on ppc64 architecture
-ExcludeArch: ppc64
-
-%description
-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 devel
-Summary: LADR Deduction Library - Development Files
-Requires: %{name} = %{version}-%{release}
-Provides: %{name}-static = %{version}-%{release}
-
-%description devel
-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 and static development
-libraries for LADR.
-
-
-%package apps
-Summary: LADR Deduction Library - Miscellaneous Applications
-Requires: %{name} = %{version}-%{release}
-
-%description apps
-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.
-
-
-%package doc
-Summary: LADR Deduction Library - Documentation
-Requires: %{name} = %{version}-%{release}
-
-%description doc
-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.
-
-This package provides documentation for Prover9, Mace4 and other associated
-programs.
-
-
-%prep
-%setup -q -n %{upstreamname}-%{upstreamver} -a 1
-%patch0 -p1
-%patch1 -p1
-%patch2 -p0
-%patch3 -p0
-
-
-%build
-make all CFLAGS="%{optflags}"
-
-
-%install
-%{__rm} -rf %{buildroot}
-%{__install} -p -d -m 0755 %{buildroot}%{_bindir}
-for f in bin/*; do
- %{__install} -p -m 0755 $f %{buildroot}%{_bindir}/%{name}-`basename $f`
-done
-%{__rm} %{buildroot}%{_bindir}/%{name}-proof3fo.xsl
-%{__rm} %{buildroot}%{_bindir}/%{name}-prover9-mace4
-%{__rm} %{buildroot}%{_bindir}/%{name}-test_clause_eval
-%{__mv} %{buildroot}%{_bindir}/%{name}-mace4 %{buildroot}%{_bindir}/mace4
-%{__mv} %{buildroot}%{_bindir}/%{name}-prover9 %{buildroot}%{_bindir}/prover9
-# manpages
-%{__install} -p -d -m 0755 %{buildroot}%{_mandir}/man1
-%{__install} -p -m 0644 manpages/interpformat.1
%{buildroot}%{_mandir}/man1/%{name}-interpformat.1
-%{__install} -p -m 0644 manpages/isofilter.1
%{buildroot}%{_mandir}/man1/%{name}-isofilter.1
-%{__ln_s} %{name}-isofilter.1.gz %{buildroot}%{_mandir}/man1/%{name}-isofilter0.1.gz
-%{__ln_s} %{name}-isofilter.1.gz %{buildroot}%{_mandir}/man1/%{name}-isofilter2.1.gz
-%{__install} -p -m 0644 manpages/prooftrans.1
%{buildroot}%{_mandir}/man1/%{name}-prooftrans.1
-%{__install} -p -m 0644 manpages/mace4.1 %{buildroot}%{_mandir}/man1
-%{__install} -p -m 0644 manpages/prover9.1 %{buildroot}%{_mandir}/man1
-# header files and libraries for devel package
-%{__install} -p -d -m 0755 %{buildroot}%{_includedir}/ladr
-%{__install} -p -m 0644 ladr/*.h %{buildroot}%{_includedir}/ladr
-%{__install} -p -d -m 0755 %{buildroot}%{_libdir}
-%{__install} -p -m 0644 ladr/lib*.a %{buildroot}%{_libdir}
-# manpages for apps package
-%{__install} -p -m 0644 manpages/clausefilter.1
%{buildroot}%{_mandir}/man1/%{name}-clausefilter.1
-%{__install} -p -m 0644 manpages/clausetester.1
%{buildroot}%{_mandir}/man1/%{name}-clausetester.1
-%{__install} -p -m 0644 manpages/interpfilter.1
%{buildroot}%{_mandir}/man1/%{name}-interpfilter.1
-%{__install} -p -m 0644 manpages/rewriter.1
%{buildroot}%{_mandir}/man1/%{name}-rewriter.1
-%{__install} -p -m 0644 manpages/prover9-apps.1 %{buildroot}%{_mandir}/man1
-# fix incorrect permission on one of the example scripts
-chmod 0644 apps.examples/run-all
-
-
-
-%check
-make test1 test2 test3
-
-
-%files
-%doc Changelog COPYING TODO copyright mace4.examples prover9.examples
-%{_bindir}/mace4
-%{_bindir}/prover9
-%{_bindir}/%{name}-interpformat
-%{_bindir}/%{name}-isofilter
-%{_bindir}/%{name}-isofilter0
-%{_bindir}/%{name}-isofilter2
-%{_bindir}/%{name}-prooftrans
-%{_mandir}/man1/mace4.1.gz
-%{_mandir}/man1/prover9.1.gz
-%{_mandir}/man1/%{name}-interpformat.1.gz
-%{_mandir}/man1/%{name}-isofilter.1.gz
-%{_mandir}/man1/%{name}-isofilter0.1.gz
-%{_mandir}/man1/%{name}-isofilter2.1.gz
-%{_mandir}/man1/%{name}-prooftrans.1.gz
-
-
-%files devel
-%doc ladr/html
-%{_includedir}/ladr
-%{_libdir}/lib*.a
-
-
-%files apps
-%doc apps.examples apps.src/README.directproof
-%{_bindir}/%{name}-attack
-%{_bindir}/%{name}-autosketches4
-%{_bindir}/%{name}-clausefilter
-%{_bindir}/%{name}-clausetester
-%{_bindir}/%{name}-complex
-%{_bindir}/%{name}-directproof
-%{_bindir}/%{name}-dprofiles
-%{_bindir}/%{name}-fof-prover9
-%{_bindir}/%{name}-gen_trc_defs
-%{_bindir}/%{name}-get_givens
-%{_bindir}/%{name}-get_interps
-%{_bindir}/%{name}-get_kept
-%{_bindir}/%{name}-gvizify
-%{_bindir}/%{name}-idfilter
-%{_bindir}/%{name}-interpfilter
-%{_bindir}/%{name}-ladr_to_tptp
-%{_bindir}/%{name}-latfilter
-%{_bindir}/%{name}-looper
-%{_bindir}/%{name}-miniscope
-%{_bindir}/%{name}-mirror-flip
-%{_bindir}/%{name}-newauto
-%{_bindir}/%{name}-newsax
-%{_bindir}/%{name}-olfilter
-%{_bindir}/%{name}-perm3
-%{_bindir}/%{name}-renamer
-%{_bindir}/%{name}-rewriter
-%{_bindir}/%{name}-sigtest
-%{_bindir}/%{name}-test_complex
-%{_bindir}/%{name}-tptp_to_ladr
-%{_bindir}/%{name}-unfast
-%{_bindir}/%{name}-upper-covers
-%{_mandir}/man1/prover9-apps.1.gz
-%{_mandir}/man1/%{name}-clausefilter.1.gz
-%{_mandir}/man1/%{name}-clausetester.1.gz
-%{_mandir}/man1/%{name}-interpfilter.1.gz
-%{_mandir}/man1/%{name}-rewriter.1.gz
-
-
-%files doc
-%doc %{name}-manual-%{upstreamver}/*.{html,css,gif}
-
-
-%changelog
-* Sat Feb 02 2019 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-17
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Fri Jul 13 2018 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-16
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Fri Feb 09 2018 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-15
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Thu Aug 03 2017 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-14
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
-
-* Thu Jul 27 2017 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-13
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
-
-* Sat Feb 11 2017 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-12
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
-
-* Thu Feb 04 2016 Fedora Release Engineering <releng(a)fedoraproject.org> -
200911a-11
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
-
-* Mon Jul 27 2015 Bruno Wolff III <bruno(a)wolff.to> - 200911a-10
-- Fix format string warning
-
-* Thu Jun 18 2015 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-9
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
-
-* Sun Aug 17 2014 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-8
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
-
-* Sat Jun 07 2014 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-7
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
-
-* Sun Aug 04 2013 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-6
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
-
-* Thu Feb 14 2013 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-5
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
-
-* Sat Jul 21 2012 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-4
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
-
-* Sat Jan 14 2012 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-3
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_17_Mass_Rebuild
-
-* Wed Feb 09 2011 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200911a-2
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
-
-* Sat Jul 24 2010 David A. Wheeler <dwheeler(a)dwheeler.com> - 200911a-1
-- Update to upstream version 200911a.
-- Adds prover9-complex, prover9-gen_trc_defs, prover9-test_complex.
-- Fix spelling in RPM summary.
-
-* Sun Jul 26 2009 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200805a-6
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
-
-* Thu Feb 26 2009 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
200805a-5
-- Rebuilt for
https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
-
-* Wed Jul 09 2008 Tim Colles <timc(a)inf.ed.ac.uk> - 200805a-4
-- exclude ppc64 architecture as test2 fails
-
-* Tue Jul 08 2008 Tim Colles <timc(a)inf.ed.ac.uk> - 200805a-3
-- make -apps require base package instead of other way around
-- added check section to run built-in tests
-- fix perms on static library
-- fix perms on example script
-- use name prefix and install all binaries in /usr/bin
-- add name prefix to manpages, drop symlinks for missing manpages
-
-* Fri Jun 06 2008 Tim Colles <timc(a)inf.ed.ac.uk> - 200805a-2
-- dropped libtoolize patch and stopped shipping shared libraries
-- changed build to use rpm optflags
-- added -p flag to preserve timestamps
-- install all binaries except mace4/prover9 to /usr/lib/prover9/bin
-
-* Fri Jun 06 2008 Tim Colles <timc(a)inf.ed.ac.uk> - 200805a-1
-- renamed as prover9
-- redesigned borrowing heavily from the Debian package by Peter Collingbourne
-- included patches from Debian package by Peter Collingbourne
-- added documentation source/package
-- updated version
-
-* Thu Jan 10 2008 Tim Colles <timc(a)inf.ed.ac.uk> - 200712-1
-- initial version
diff --git a/sources b/sources
deleted file mode 100644
index 68ed5f1..0000000
--- a/sources
+++ /dev/null
@@ -1,2 +0,0 @@
-ab409f31ecbb4410b1c7d75deadea2c6 LADR-2009-11A.tar.gz
-23fbb9c6b3cbfbb2b893fb788e248a29 prover9-manual-2009-11A.tar.gz