Skip to content


Subversion checkout URL

You can clone with
Download ZIP
tree: 17ba8dd92b
Fetching contributors…

Cannot retrieve contributors at this time

executable file 31 lines (25 sloc) 0.879 kB
#!/bin/bash -
# TPTP theories that have multiple formulas with identical names are
# invalid, even if the contents of the two formulas are identical.
# This script removes such duplicate formulas from an input TPTP
# theory. The output of this script is not guaranteed to be a TPTP
# theory with non-duplicate names. One case where this can occur is
# when distinct formulas are assigned the same name, e.g.,
# fof(my_formula,axiom,$true).
# fof(my_formula,axiom,$false).
# or when a single formula is assigned distinct statuses, e.g.,
# fof(my_formula,axiom,$true).
# fof(my_formula,theorem,$false).
if [ -z $theory ]; then
echo "Usage: `basename $0` TPTP-THEORY";
exit 1;
if [ ! -r $theory ]; then
echo "Error: the supplied TPTP theory file '$theory' is not readable."
exit 1;
tptp4X -N -c -x -umachine $theory | sort -u | uniq -u
Jump to Line
Something went wrong with that request. Please try again.