%==============================================================================
%----The tptp2X  utility is used  to make transformations on the 
%----clauses in TPTP problem, and to output the clauses in formats 
%----accepted  by existing ATP systems. 
%----
%----Written by Geoff Sutcliffe, July 1992.
%----Updated by Geoff Sutcliffe, November 1992.
%----Updated by Geoff Sutcliffe, March 1993.
%----Revised by Geoff Sutcliffe, January, 1994.
%----Updated by Geoff Sutcliffe, April, 1994.
%----Revised by Geoff Sutcliffe, May-August 1994, with ideas from
%----    Gerd Neugebauer
%----Revised by Geoff Sutcliffe, May, 1995.
%----Extensions for FOF by Geoff Sutcliffe, October 1996.
%==============================================================================
%------------------------------------------------------------------------------
%----Load the configuration file
:-consult('tptp2X.config').
%------------------------------------------------------------------------------
%----These are used in the TPTP and need to exist before the 
%----transformations and formats are loaded. They are also declared at 
%----runtime in tptp2X/4.
:-op(70,fx,'$$').
:-op(80,fx,'$').
:-op(85,fx,'&').    %----DLF dereference 
:-op(90,xfx,/).     %----Rationals need to bind tighter than =
:-op(100,fx,++).
:-op(100,fx,--).
%----Postfix for !=
:-op(100,xf,'!').
%---- .. used for range in tptp2X. Needs to be stronger than :
:-op(400,xfx,'..').
%----! and ? are of higher precedence than : so ![X]:p(X) is :(![X],p(X))
%----Otherwise ![X]:![Y]:p(X,Y) cannot be parsed.
%----! is fy so Prolog can read !! (blah) as !(!(blah)) and it gets fixed
:-op(400,fy,!).
:-op(400,fx,?).
:-op(400,fx,^).
:-op(400,fx,'!>').
:-op(400,fx,'?*').
:-op(400,fx,'@-').
:-op(400,fx,'@+').
:-op(401,fx,'@@-').
:-op(401,fx,'@@+').
:-op(402,fx,'!!').
:-op(402,fx,'??').
:-op(403,yfx,*).     %----X product
:-op(403,yfx,+).     %----Union
%----DLF ++ and ** and <+> and -= stronger than = and << and >>
:-op(403,yfx,'**').  %----DLF intersection
:-op(403,yfx,'++').  %----DLF union
:-op(403,yfx,'<+>'). %----DLF disjoint union
%----= must bind more tightly than : for ! [X] : a = X. = must binder looser
%----than quantifiers for otherwise X = ! [Y] : ... is a syntax error (the =
%----grabs the quantifier). That means for THF it is necessary to bracket 
%----formula terms, e.g., a = (! [X] : p(X))
:-op(405,xfx,'=').
%---!= not possible because ! is special - see postfix cheat :-op(405,xfx,'!=').
:-op(440,xfy,>).     %----Type arrow
:-op(450,xfx,'-=').  %----DLF role inverse_of
:-op(450,xfx,'<>').  %----DLF class disjoint
:-op(450,xfx,'<<').  %----DLF subclass, Subtype arrow
:-op(450,xfx,'>>').  %----DLF superclass
%----Need : stronger than binary connectives for ! [X] : p(X) <=> !Y ...
%----Need ~ and : equal and right-assoc for ![X] : ~p and for ~![X] : ...
:-op(450,fy,~).      %----Logical negation
:-op(450,xfy,:).
:-op(501,yfx,@).
% :-op(502,xfy,'|').
:-(system_mode(true),op(502,xfy,'|'),system_mode(false)).
:-op(502,xfx,'~|').
:-op(503,xfy,&).
:-op(503,xfx,~&).
:-op(504,xfx,=>).
:-op(504,xfx,<=).
:-op(505,xfx,<=>).
:-op(505,xfx,<~>).
:-op(510,xfx,-->).

%----DLF separators, very weak, but stronger than :=
:-op(525,xfx,#).
:-op(525,xf,#).

:-op(550,xfx,:=).

%----DLF == is built in, precedence 700 - weak!
%------------------------------------------------------------------------------
%----Runtime version of operators
declare_TPTP_operators:-
    op(70,fx,'$$'),
    op(80,fx,'$'),
    op(85,fx,'&'),
    op(90,xfx,/),
    op(100,fx,++),
    op(100,fx,--),
    op(100,xf,'!'),
    op(400,xfx,'..'),
    op(400,fy,!),
    op(400,fx,?),
    op(400,fx,^),
    op(400,fx,'!>'),
    op(400,fx,'?*'),
    op(400,fx,'@-'),
    op(400,fx,'@+'),
    op(400,fx,'@@-'),
    op(400,fx,'@@+'),
    op(402,fx,'!!'),
    op(402,fx,'??'),
    op(403,yfx,*),
    op(403,yfx,+),
    op(403,yfx,'**'),
    op(403,yfx,'++'),
    op(403,yfx,'<+>'),
    op(405,xfx,'='),
    op(440,xfy,>),
    op(450,yfx,'-='),
    op(450,yfx,'<>'),
    op(450,xfx,'<<'),
    op(450,xfx,'>>'),
    op(450,fy,~),
    op(450,xfy,:),
    op(501,yfx,@),
%    op(502,xfy,'|'),
    (system_mode(true),op(502,xfy,'|'),system_mode(false)),
    op(502,xfx,'~|'),
    op(503,xfy,&),
    op(503,xfx,~&),
    op(504,xfx,=>),
    op(504,xfx,<=),
    op(505,xfx,<=>),
    op(505,xfx,<~>),
    op(510,xfx,-->),
    op(525,xfx,#),
    op(525,xf,#),
    op(550,xfx,':=').
%------------------------------------------------------------------------------
%----This specifies the transformations that will be loaded. Currently
%----all are loaded, but you comment out any you don't want. Always keep
%----transform.arrange for none transformation.
:-['transform.arrange'].
:-['transform.equality'].
:-['transform.expand'].
:-['transform.fofify'].
:-['transform.magic'].
:-['transform.reform'].
:-['transform.shorten'].
:-['transform.xdb'].
%------------------------------------------------------------------------------
%----This specifies the output formats that will be loaded. Currently
%----all are loaded, but you comment out any you don't want. Don't
%----leave a space between the comment % and the command, as that will
%----confuse tptp2X_install
:-['format.bliksem'].
% NO LONGER USED :-['format.carine'].
% NO LONGER USED ['format.clif'].
% NO LONGER USED ['format.code'].
:-['format.dedam'].
:-['format.dfg'].
:-['format.dimacs'].
:-['format.eqp'].
% NO LONGER USED ['format.finder'].
:-['format.geo'].
% NO LONGER USED ['format.ilf'].
% NO LONGER USED :-['format.isabelle'].
% NO LONGER USED ['format.kif'].
:-['format.leancop'].
:-['format.lf'].
% NO LONGER USED ['format.tap'].
% NO LONGER USED :-['format.leantap'].
:-['format.metitarski'].
% NO LONGER USED ['format.omdoc'].
% NO LONGER USED ['format.oscar'].
:-['format.otter'].
% NO LONGER USED :-['format.protein'].
:-['format.prover9'].
% NO LONGER USED ['format.pttp'].
% NO LONGER USED ['format.satchmo'].
% NO LONGER USED ['format.scott'].
% NO LONGER USED ['format.sem'].
% NO LONGER USED :-['format.setheo'].
% NO LONGER USED :-['format.sex'].
:-['format.smt'].
% NO LONGER USED ['format.sprfn'].
% NO LONGER USED ['format.thinker'].
:-['format.tps'].
% NO LONGER USED :-['format.oldtptp'].
:-['format.tptp'].
% NO LONGER USED :-['format.prefix'].
:-['format.waldmeister'].
%------------------------------------------------------------------------------
%----Use the standard TPTP read code. 
:-['tptp2X.read'].
:-['tptp2X.generate'].
:-['tptp2X.syntax'].
:-['tptp2X.format'].
%------------------------------------------------------------------------------
%----Invert sign 
tptp2X_invert_sign(++,--).

tptp2X_invert_sign(--,++).
%------------------------------------------------------------------------------
%----Invert the sign of a TPTP literal
tptp2X_invert_literal(++Atom,--Atom).

tptp2X_invert_literal(--Atom,++Atom).
%------------------------------------------------------------------------------
%----Used by generator files to include others. When Prolog is standard
%----this can be improved to use ensure_loaded.
tptp2X_include(TPTPFileName):-
    assertz(tptp2X_file_to_include(TPTPFileName)).
%------------------------------------------------------------------------------
%----Load a single file (used for loading generators)
%----Check if already loaded not possible with a call, due to existence
%----errors. Not possible with clause/2 as it's not dynamic. Shit.
% tptp2X_load_one_file(TPTPFileName):-
%----Can't find a portable way!
%     !.

%----Use consult for BinProlog, which has a different compiling attitude.
tptp2X_load_one_file(TPTPFileName):-
    prolog_dialect(PrologDialect),
    tptp2X_member(PrologDialect,[binprolog,gnu,generic]),
    !,
    tptp_path_name(TPTPFileName,TPTPPathName),
    consult(TPTPPathName).

tptp2X_load_one_file(TPTPFileName):-
    tptp_path_name(TPTPFileName,TPTPPathName),
    compile(TPTPPathName).
%------------------------------------------------------------------------------
%----Load a file, and those which are tptp2X_included
tptp2X_load(TPTPFileName):-
    tptp2X_load_one_file(TPTPFileName),
    (retract(tptp2X_file_to_include(FileToInclude)) ->
        tptp2X_load(FileToInclude)
    ;   true).
%------------------------------------------------------------------------------
%----Make a subset of a list
tptp2X_subset([],[]).

tptp2X_subset([_|T],Subset):-
    tptp2X_subset(T,Subset).

tptp2X_subset([H|T],[H|RestOfSubset]):-
    tptp2X_subset(T,RestOfSubset).
%------------------------------------------------------------------------------
%----Simple append, required in tptpread. Renamed to avoid confusion 
%----with builtins.
tptp2X_append([],List,List).

tptp2X_append([Head|Tail],List,[Head|TailList]):-
    tptp2X_append(Tail,List,TailList).
%------------------------------------------------------------------------------
%----Simple select. Renamed to avoid confusion with builtins.
tptp2X_select(Element,[Element|Tail],Tail).

tptp2X_select(Element,[Head|Tail],[Head|SelectedTail]):-
    tptp2X_select(Element,Tail,SelectedTail).
%------------------------------------------------------------------------------
%----Select the Nth element.
tptp2X_select_Nth(Element,[Element|Tail],1,Tail).

tptp2X_select_Nth(Element,[Head|Tail],N,[Head|SelectedTail]):-
    integer(N),
    N > 1,
    NewN is N - 1,
    tptp2X_select_Nth(Element,Tail,NewN,SelectedTail).

tptp2X_select_Nth(Element,[Head|Tail],N,[Head|SelectedTail]):-
    var(N),
    tptp2X_select_Nth(Element,Tail,NewN,SelectedTail),
    N is NewN + 1.
%------------------------------------------------------------------------------
%----List difference
tptp2X_list_difference(Remainder,[],Remainder).

tptp2X_list_difference(List,[FirstToRemove|RestToRemove],Remainder):-
    tptp2X_select(FirstToRemove,List,OthersInList),
    !,
    tptp2X_list_difference(OthersInList,RestToRemove,Remainder).

tptp2X_list_difference(List,[_|RestToRemove],Remainder):-
    tptp2X_list_difference(List,RestToRemove,Remainder).
%------------------------------------------------------------------------------
%----Simple member. Renamed to avoid confusion with builtins.
tptp2X_member(Element,[Element|_]).

tptp2X_member(Element,[_|Tail]):-
    tptp2X_member(Element,Tail).
%------------------------------------------------------------------------------
%----Exact member without unification. Only a test, not for extraction
tptp2X_exact_member(Element,[Head|_]):-
    Element == Head.

tptp2X_exact_member(Element,[_|Tail]):-
    tptp2X_exact_member(Element,Tail).
%------------------------------------------------------------------------------
%----Simple length. Renamed to avoid confusion with builtins.
tptp2X_length([],0).

tptp2X_length([_|Tail],Length):-
    tptp2X_length(Tail,TailLength),
    Length is TailLength + 1.
%------------------------------------------------------------------------------
tptp2X_atom_length(Atom,AtomLength):-
     name(Atom,AtomASCII),
     tptp2X_length(AtomASCII,AtomLength).
%------------------------------------------------------------------------------
%----Setof1 does setof, but allows empty list to be returned
tptp2X_setof1(Variable,Goal,List):-
    setof(Variable,Goal,List),
    !.

tptp2X_setof1(_,_,[]).
%------------------------------------------------------------------------------
%----bagof1 does bagof, but allows empty list to be returned
tptp2X_bagof1(Variable,Goal,List):-
    bagof(Variable,Goal,List),
    !.

tptp2X_bagof1(_,_,[]).
%------------------------------------------------------------------------------
%----setof that ignores other variables and returns an empty list rather
%----than failing.
tptp2X_findall_setof1(Variable,Predicate,UniqueValues):-
    findall(Variable,Predicate,AllValues),
    tptp2X_setof1(Member,tptp2X_member(Member,AllValues),UniqueValues).
%------------------------------------------------------------------------------
%----Doing an occurs check
tptp2X_occurs_check_list(_,[]).

tptp2X_occurs_check_list(Variable,[H|T]):-
    tptp2X_occurs_check(Variable,H),
    tptp2X_occurs_check_list(Variable,T).
%------------------------------------------------------------------------------
tptp2X_occurs_check(Variable,Term):-
    var(Term),
    !,
    Variable \== Term.

tptp2X_occurs_check(Variable,Term):-
    Term =.. [_|Arguments],
    tptp2X_occurs_check_list(Variable,Arguments).
%------------------------------------------------------------------------------
%----Remove all elements upto the last delimiter
tptp2X_list_tail([],_,[],not_found):-
    !.
    
%----Check if the delimiter is further down the list
tptp2X_list_tail([_|ListTail],Delimiter,TailTail,found):-
    tptp2X_list_tail(ListTail,Delimiter,TailTail,found),
    !.

%----Check if this is the delimiter
tptp2X_list_tail([Delimiter|ListTail],Delimiter,ListTail,found):-
    !.

%----Otherwise pass back this list
tptp2X_list_tail(List,_,List,not_found).
%------------------------------------------------------------------------------
%----Choose the maximum of two values
tptp2X_choose_maximum(FirstNumber,SecondNumber,FirstNumber):-
    FirstNumber >= SecondNumber,
    !.

tptp2X_choose_maximum(_,SecondNumber,SecondNumber).
%------------------------------------------------------------------------------
%----Find the maximal value in a list of positive numbers
tptp2X_maximal_in_list([],0).

tptp2X_maximal_in_list([H|T],Maximum):-
    tptp2X_maximal_in_list(T,TMaximum),
    tptp2X_choose_maximum(H,TMaximum,Maximum).
%------------------------------------------------------------------------------
%----Add vectors of numbers
tptp2X_list_add([],[],[]).

tptp2X_list_add([H1|T1],[H2|T2],[ResultH|ResultT]):-
    tptp2X_list_add(T1,T2,ResultT),
    ResultH is H1 + H2.
%------------------------------------------------------------------------------
%----Product of all values in a list
tptp2X_sum_logs([],0):-
    !.

tptp2X_sum_logs([H|T],SumLogs):-
    tptp2X_sum_logs(T,TSumLogs),
    SumLogs is log(H) + TSumLogs.
%------------------------------------------------------------------------------
%----Compute geometric average
tptp2X_geometric_average([],0):-
    !.

tptp2X_geometric_average(List,Average):-
    tptp2X_sum_logs(List,SumLogs),
    tptp2X_length(List,Length),
%----This is not currently in use because Eclipse rounds to an integer
    Average is round(exp(SumLogs / Length)).
%------------------------------------------------------------------------------
%----Sum a list
tptp2X_sum([],0).

tptp2X_sum([H|T],Sum):-
    tptp2X_sum(T,TSum),
    Sum is H + TSum.
%------------------------------------------------------------------------------
%----Compute arithmetic average
tptp2X_arithmetic_average([],0):-
    !.

tptp2X_arithmetic_average(List,Average):-
    tptp2X_sum(List,Sum),
    tptp2X_length(List,Length),
    Average is Sum // Length.
%------------------------------------------------------------------------------
%----Generating random integers in a given range
%----Generic version - Integers in range 0 to 4095 (may not be adequate
%----for all uses).
tptp2X_random_integer_for_dialect(generic,Lowest,Highest,Random):-
%----Seed already saved, use it.
    retract(seed(BigRandom)),
    !,
    NewSeed is (125 * BigRandom + 1) mod 4096,
    asserta(seed(NewSeed)),
    Random is Lowest + (BigRandom mod (Highest - Lowest + 1)).

%----First time - make seed from Lowest and Highest
tptp2X_random_integer_for_dialect(generic,Lowest,Highest,Random):-
    Seed is Highest - Lowest,
    asserta(seed(Seed)),
    tptp2X_random_integer_for_dialect(generic,Lowest,Highest,Random).

%----BinProlog version
tptp2X_random_integer_for_dialect(binprolog,Lowest,Highest,Random):-
%----Integer in some range (not in manual)
    random(BigRandom),
    Random is Lowest + (BigRandom mod (Highest - Lowest + 1)).

%----SWI prolog
tptp2X_random_integer_for_dialect(swi,Lowest,Highest,Random):-
    Range is (Highest-Lowest) + 1,
    RandomInRange is random(Range),
    Random is Lowest + RandomInRange.

%----YAP prolog
tptp2X_random_integer_for_dialect(yap,Lowest,Highest,Random):-
    Random is Lowest + integer(random * (Highest-Lowest+1)).

%----SICStus 2.1 version.
tptp2X_random_integer_for_dialect(sicstus,Lowest,Highest,Random):-
    HighestPlus1 is Highest + 1,
    random(Lowest,HighestPlus1,Random).

%----GNU Prolog version.
tptp2X_random_integer_for_dialect(gnu,Lowest,Highest,Random):-
    HighestPlus1 is Highest + 1,
    random(Lowest,HighestPlus1,Random).

%----Eclipse version
tptp2X_random_integer_for_dialect(eclipse,Lowest,Highest,Random):-
%----Integer in range 0 to (2^32 - 1)
    random(BigRandom),
    Random is Lowest + (BigRandom mod (1+ Highest - Lowest)).

%----Quintus version - Integer in specified range
tptp2X_random_integer_for_dialect(quintus,Lowest,Highest,Random):-
    use_module(library(random)),
    HighestPlus1 is Highest + 1,
    random(Lowest,HighestPlus1,Random).

tptp2X_random_integer(Lowest,Highest,Random):-
    prolog_dialect(Dialect),
    tptp2X_random_integer_for_dialect(Dialect,Lowest,Highest,Random).
%------------------------------------------------------------------------------
%----Extracts the .XXX from a filename
tptp2X_extension(FullName,Extension):-
    name(FullName,FullASCII),
    tptp2X_append(_,[46|ExtensionASCII],FullASCII),
%----Force the last . to be taken
    \+ tptp2X_member(46,ExtensionASCII),
    !,
    name(Extension,[46|ExtensionASCII]).

%----No extension
tptp2X_extension(_,'').
%------------------------------------------------------------------------------
%----Procedure to do the same as the UNIX basename command
tptp2X_basename(FullName,Suffix,Basename):-
    name(FullName,FullNameList),
    name(Suffix,SuffixList),
%----Delete upto last / (ASCII 47)
    tptp2X_list_tail(FullNameList,47,FullNameTailList,_),
%----Try to delete suffix from list
    (tptp2X_append(BasenameList,SuffixList,FullNameTailList) ->
        name(Basename,BasenameList);
%----If not possible, then ignore the suffix
        name(Basename,FullNameTailList)).
%------------------------------------------------------------------------------
%----Procedure to do the same as the UNIX dirname command
tptp2X_dirname(FullName,Dirname):-
    name(FullName,FullNameList),
%----Remove the tptp2X_basename
    tptp2X_basename(FullName,'',Basename),
    name(Basename,BasenameList),
%----Find what is before the tptp2X_basename, if anything
    (tptp2X_append(DirnameList,[47|BasenameList],FullNameList) ->
        name(Dirname,DirnameList);
%----If no directory then it's the current one
        Dirname = '.').
%------------------------------------------------------------------------------
%----Provide a range of integers through backtracking
tptp2X_integer_in_range(Low,High,Low):-
    Low =< High.

tptp2X_integer_in_range(Low,High,Integer):-
    Low < High,
    NewLow is Low + 1,
    tptp2X_integer_in_range(NewLow,High,Integer).
%------------------------------------------------------------------------------
%-----Convert from an integer to a list of characters
tptp2X_integer_name(Integer,FinalString):-
    tptp2X_integer_name(Integer,[],FinalString).

tptp2X_integer_name(Integer,StringSoFar,[Character|StringSoFar]):-
    Integer < 10,
    !,
    Character is Integer + 48.

tptp2X_integer_name(Integer,StringSoFar,FinalString):-
    TopHalf is Integer // 10,
    BottomHalf is Integer mod 10,
    Character is BottomHalf + 48,
    tptp2X_integer_name(TopHalf,[Character|StringSoFar],FinalString).
%------------------------------------------------------------------------------
%----Do text substitution in a list
replace_in_list(SearchFor,OldList,ReplaceWith,NewList):-
    tptp2X_append(SearchFor,EndOfOldList,OldTail),
    tptp2X_append(StartOfOldList,OldTail,OldList),
    !,
    tptp2X_append(ReplaceWith,EndOfOldList,NewTail),
    tptp2X_append(StartOfOldList,NewTail,MiddleList),
    replace_in_list(SearchFor,MiddleList,ReplaceWith,NewList).

replace_in_list(_,List,_,List).
%------------------------------------------------------------------------------
%----Replace bits of atoms - this is a shitty way of updating the
%----header which is maintained as a list of atoms, one atom per line.
replace_in_atoms([],Atoms,Atoms):-
%----Not sure if this cut is needed really (fuck)
    !.

replace_in_atoms([FirstPair|RestOfPairs],Atoms,ReplacedAtoms):-
    !,
    replace_in_atoms(FirstPair,Atoms,Atoms1),
    replace_in_atoms(RestOfPairs,Atoms1,ReplacedAtoms).

replace_in_atoms(_,[],[]).

replace_in_atoms(SearchForAtom-ReplaceWithAtom,[FirstAtom|RestOfAtoms],
[FirstReplacedAtom|RestOfReplacedAtoms]):-
%----These two could be abstracted, but it's out of the way here
    name(SearchForAtom,SearchForList),
    name(ReplaceWithAtom,ReplaceWithList),
%----Convert to ASCII list
    name(FirstAtom,FirstAtomList),
    replace_in_list(SearchForList,FirstAtomList,ReplaceWithList,
FirstReplacedAtomList),
    name(FirstReplacedAtom,FirstReplacedAtomList),
    replace_in_atoms(SearchForAtom-ReplaceWithAtom,RestOfAtoms,
RestOfReplacedAtoms).
%------------------------------------------------------------------------------
%----Any name for lists
list_name([OneElement],OneElementList):-
    !,
    any_name(OneElement,OneElementList).

list_name([H|T],ListList):-
    any_name(H,HList),
    list_name(T,TList),
    tptp2X_append(HList,[44|TList],ListList).
%------------------------------------------------------------------------------
%----Do name for anything
any_name(Variable,"_"):-
    var(Variable),
    !.

any_name([],"[]"):-
    !.

any_name([H|T],ListList):-
    !,
    list_name([H|T],InteriorList),
%----91 = [ and 93 = ]
    tptp2X_append([91|InteriorList],"]",ListList).

any_name(Atom,AtomList):-
    atomic(Atom),
    !,
    name(Atom,AtomList).

any_name(Integer,IntegerList):-
    integer(Integer),
    !,
    tptp2X_integer_name(Integer,IntegerList).

%----Operators (hacks for special cases)
%---- : = 58
any_name(Operand1:Operand2,ColonList):-
    !,
    any_name(Operand1,OperandList1),
    any_name(Operand2,OperandList2),
    tptp2X_append(OperandList1,[58|OperandList2],ColonList).

%---- .. = 46 46
any_name(Operand1..Operand2,DotDotList):-
    !,
    any_name(Operand1,OperandList1),
    any_name(Operand2,OperandList2),
    tptp2X_append(OperandList1,[46,46|OperandList2],DotDotList).

%---- + = 43
any_name(Operand1+Operand2,PlusList):-
    !,
    any_name(Operand1,OperandList1),
    any_name(Operand2,OperandList2),
    tptp2X_append(OperandList1,[43|OperandList2],PlusList).

%----Functions
any_name(Function,FunctionList):-
    Function =.. [Functor|Arguments],
    name(Functor,FunctorList),
    list_name(Arguments,ArgumentsList),
%----40 = (
    tptp2X_append(FunctorList,[40|ArgumentsList],List1),
    tptp2X_append(List1,")",FunctionList).
%------------------------------------------------------------------------------
%----Append each list element's list
concatenate_atoms_list([],[]).

concatenate_atoms_list([H|T],ASCII):-
    any_name(H,HList),
    concatenate_atoms_list(T,TList),
    tptp2X_append(HList,TList,ASCII).
%------------------------------------------------------------------------------
%----Concatenate a list of terms into a big atom
concatenate_atoms(Atoms,Atom):-
    concatenate_atoms_list(Atoms,AtomsList),
    name(Atom,AtomsList).
%------------------------------------------------------------------------------
%-----Fast reverse a list
fast_reverse_list([],ReverseList,ReverseList):-
    !.

fast_reverse_list([Head|Tail],ReverseSoFar,ReverseList):-
    fast_reverse_list(Tail,[Head|ReverseSoFar],ReverseList).
%------------------------------------------------------------------------------
%----Put the header comment in a tptp2X line
%----Escape for suppressing when I do TPTP maintenance
add_tptp2X_comment_entry(_,CommentEntries,_,CommentEntries):-
    fail,
    !.

%----Already more than one tptp2X comments, and the one we want exists (old)
add_tptp2X_comment_entry(old,CommentEntries,CommentText,NewCommentEntries):-
%----Find first tptp2X comment
    tptp2X_append(FirstEntries,[TPTP2XEntry1|RestOfEntries],CommentEntries),
    name(TPTP2XEntry1,TPTP2XEntryASCII1),
    tptp2X_append("          : tptp2X ",_,TPTP2XEntryASCII1),
%----Find second tptp2X comment
    tptp2X_member(TPTP2XEntry2,RestOfEntries),
    name(TPTP2XEntry2,TPTP2XEntryASCII2),
    tptp2X_append("          : tptp2X ",_,TPTP2XEntryASCII2),
    !,
%----Insert comment on rest of entries
    add_tptp2X_comment_entry(old,RestOfEntries,CommentText,
NewRestOfCommentEntries),
    tptp2X_append(FirstEntries,[TPTP2XEntry1|NewRestOfCommentEntries],
NewCommentEntries).

%----Already a tptp2X comment that we want (old)
add_tptp2X_comment_entry(old,CommentEntries,CommentText,NewCommentEntries):-
%----Find the tptp2X comment
    tptp2X_append(FirstEntries,[CommentEntry|RestOfEntries],CommentEntries),
    name(CommentEntry,CommentASCII),
    tptp2X_append("          : tptp2X ",TPTP2XCommentASCII,CommentASCII),
    !,
%----Add the new text in front
    name(CommentText,CommentTextASCII),
    tptp2X_append("          : tptp2X ",CommentTextASCII,ASCII1),
    tptp2X_append(ASCII1,[32|TPTP2XCommentASCII],ASCII2),
    name(NewEntry,ASCII2),
    tptp2X_append(FirstEntries,[NewEntry|RestOfEntries],NewCommentEntries).

%----If no tptp2X comment then do nothing for old
add_tptp2X_comment_entry(old,CommentEntries,_,CommentEntries).

%----Make the tptp2X entry (new)
add_tptp2X_comment_entry(new,CommentEntries,CommentText,NewCommentEntries):-
    concatenate_atoms(['          : tptp2X ',CommentText],CommentEntry),
    tptp2X_append(CommentEntries,[CommentEntry],NewCommentEntries).
%------------------------------------------------------------------------------
%----Add a comment explaining how this was all created
add_tptp2X_comment(OldOrNew,FileHeader,CommentText,CommentedFileHeader):-
    tptp2X_append(EarlierFields,['Comments'-CommentEntries|RestOfFields],
FileHeader),
    !,
    add_tptp2X_comment_entry(OldOrNew,CommentEntries,CommentText,
NewCommentEntries),
    tptp2X_append(EarlierFields,['Comments'-NewCommentEntries|RestOfFields],
CommentedFileHeader).

%----If the comment fields is missing, then do nothing
add_tptp2X_comment(_,FileHeader,_,FileHeader).
%------------------------------------------------------------------------------
extract_formulae_of_type([],_,[],[]).

extract_formulae_of_type([FirstFormula|RestOfFormulae],Type,
[FirstFormula|RestOfType],NotOfType):-
    FirstFormula =.. [_,_,Type|_],
    !,
    extract_formulae_of_type(RestOfFormulae,Type,RestOfType,NotOfType).

extract_formulae_of_type([FirstFormula|RestOfFormulae],Type,OfType,
[FirstFormula|RestNotOfType]):-
    extract_formulae_of_type(RestOfFormulae,Type,OfType,RestNotOfType).
%------------------------------------------------------------------------------
%----Get information about this tptp2X file for generators
get_tptp2X_file_information(BaseInputName,generator,GenerationFormat,
GenerationConstraints,SOTAGenerations):-
    concatenate_atoms([BaseInputName,'_file_information'],
InformationQueryPredicate),
    InformationQuery =.. [InformationQueryPredicate,generator,
sizes(GenerationFormat,GenerationConstraints),SOTATerm],
    InformationQuery,
    SOTATerm =.. [sota|SOTAGenerations].

get_tptp2X_file_information(BaseInputName,format,ListOfFormats):-
    concatenate_atoms([BaseInputName,'_file_information'],
InformationQueryPredicate),
    InformationQuery =.. [InformationQueryPredicate,format,AFormat,_],
    findall(AFormat,InformationQuery,ListOfFormats).

get_tptp2X_file_information(BaseInputName,transform,ListOfFormats):-
    concatenate_atoms([BaseInputName,'_file_information'],
InformationQueryPredicate),
    InformationQuery =.. [InformationQueryPredicate,transform,AFormat,_],
    findall(AFormat,InformationQuery,ListOfFormats).
%------------------------------------------------------------------------------
%----If no comment atom then suppress
output_comment_line(_,''):-
    !.

output_comment_line(Content,Start-End):-
    !,
    write(Start),
    write(Content),
    write(End),
    nl.

output_comment_line(Content,Start):-
    write(Start),
    write(Content),
    nl.
%------------------------------------------------------------------------------
comment_atom_length(Start-End,Length):-
    !,
    tptp2X_atom_length(Start,StartLength),
    tptp2X_atom_length(End,EndLength),
    Length is StartLength + EndLength.

comment_atom_length(Start,Length):-
    tptp2X_atom_length(Start,Length).
%------------------------------------------------------------------------------
generate_separator_list(0,[]).

generate_separator_list(Length,[45|RestOfSeparatorList]):-
    Length > 0,
    Length1 is Length - 1,
    generate_separator_list(Length1,RestOfSeparatorList).
%------------------------------------------------------------------------------
generate_separator(Length,Separator):-
    generate_separator_list(Length,SeparatorList),
    name(Separator,SeparatorList).
%------------------------------------------------------------------------------
%----Write a comment line
output_separator_line(CommentAtom):-
    comment_atom_length(CommentAtom,CommentAtomLength),
    SeparatorLength is 79 - CommentAtomLength,
    generate_separator(SeparatorLength,Separator),
    output_comment_line(Separator,CommentAtom).
%------------------------------------------------------------------------------
%----Output field lines one by one.
output_field_lines([],_).

output_field_lines([FirstLine|RestOfLines],CommentAtom):-
    output_comment_line(FirstLine,CommentAtom),
    output_field_lines(RestOfLines,CommentAtom).
%------------------------------------------------------------------------------
%----Output the file header using the given comment atom
output_file_header([],_):-
    !.

%----Suppress if no comment atom
output_file_header([_|RestOfHeaderLines],''):-
    !,
    output_file_header(RestOfHeaderLines,'').

%----No leading comment char for empty lines
output_file_header(['Blank'-_|RestOfHeaderLines],CommentAtom):-
    !,
    nl,
    output_file_header(RestOfHeaderLines,CommentAtom).

output_file_header([_-FieldLines|RestOfHeaderLines],CommentAtom):-
    output_field_lines(FieldLines,CommentAtom),
    output_file_header(RestOfHeaderLines,CommentAtom).
%------------------------------------------------------------------------------
%----If no header then nothing
possibly_output_file_header([],_):-
    !.

%----If some header then header and separator line
possibly_output_file_header(Header,CommentAtom):-
    output_file_header(Header,CommentAtom),
    output_separator_line(CommentAtom).
%------------------------------------------------------------------------------
%----Output each of the include directives
output_each_include_directive([]).

output_each_include_directive([include(FileName)|RestOfDirectives]):-
    write('include('),
%----Portable writing of a ' for the filename (a Prolog atom here)
    put_code(39),
    write(FileName),
    put_code(39),
    write(').'),
    nl,
    output_each_include_directive(RestOfDirectives).
%------------------------------------------------------------------------------
%----Output include directives for other files. Only in tptp format.
output_include_directives([],_,tptp):-
    !.

output_include_directives(IncludeDirectives,CommentAtom,tptp):-
    !,
    output_each_include_directive(IncludeDirectives),
    output_separator_line(CommentAtom).

%----Other formats only if no directives
output_include_directives([],_,_).
%------------------------------------------------------------------------------
%----Output the formulae in the required format
%----If none, then do nothing.
output_formulae([],_,_,_):-
    !.

%----Otherwise build a query and execute it
output_formulae(OutputFormulae,FileHeader,OutputFormat,FormatName):-
    FormatQuery =.. [FormatName,OutputFormat,OutputFormulae,FileHeader],
    FormatQuery.
%------------------------------------------------------------------------------
%----Make the output file name
%----If the output directory is user, then output to stdout
make_output_file_name(user,_,_,user):-
    !.

make_output_file_name(OutputDirectory,OutputName,FileNameExtension,
OutputFileName):-
    concatenate_atoms([OutputDirectory,'/',OutputName,FileNameExtension],
OutputFileName).
%------------------------------------------------------------------------------
%----Extract the first part, and whole parts of : separated terms
get_format_or_transform_name(Name:Arguments,Name,WholeAtom):-
    !,
    any_name(Name:Arguments,ASCII),
    name(WholeAtom,ASCII).

%----Simple ones without :s
get_format_or_transform_name(Name,Name,Name).
%------------------------------------------------------------------------------
%----Extract the format information from the file
get_format_information(FormatName,CommentAtom,FileNameExtension):-
    concatenate_atoms([FormatName,'_format_information'],
InformationQueryPredicate),
    InformationQuery =.. [InformationQueryPredicate,CommentAtom,
FileNameExtension],
    InformationQuery,
    !.

%----Error case
get_format_information(FormatName,_,_):-
    write('%----ERROR : Cannot get the format information for '),
    write(FormatName),
    nl,
    fail.
%------------------------------------------------------------------------------
%----Do the output, file is already open
%----If no clauses or header, then do nothing (used for emptying files).
output_formulae_in_format([],[],[],_,_,_):-
    !.

output_formulae_in_format(FileHeader,IncludeDirectives,OutputFormulae,
OutputFormat,FormatName,CommentAtom):-
    output_separator_line(CommentAtom),
    possibly_output_file_header(FileHeader,CommentAtom),
    output_include_directives(IncludeDirectives,CommentAtom,FormatName),
    output_formulae(OutputFormulae,FileHeader,OutputFormat,FormatName),
%----Put a comment line
    output_separator_line(CommentAtom),
    !.

%----Error case. Don't fail - the file still has to be closed.
output_formulae_in_format(_,_,_,OutputFormat,_,_):-
%----Close the file so output goes to user
%----Hmmm, it might be stdout, should I close that?
%----Output error message
    write('%----ERROR : Output in '),
    write(OutputFormat),
    write(' format failed.'),
    nl.
%------------------------------------------------------------------------------
%----Reject variable formats
output_formulae_in_format_to_file(_,_,_,Variable,_,_,_,_):-
    var(Variable),
    !,
    write(
'%----ERROR : The output format is invalid (it looks like a variable).'),nl,
    fail.

%----Allow multiple output formats (useful for the competition). Done
%----by backtracking over formats specified.
output_formulae_in_format_to_file(FileHeader,IncludeDirectives,
OutputFormulae,[FirstFormat|RestOfFormats],OutputName,OutputDirectory,
OutputFormatUsed,OutputFileName):-
    !,
    tptp2X_member(OutputFormatUsed,[FirstFormat|RestOfFormats]),
    output_formulae_in_format_to_file(FileHeader,IncludeDirectives,
OutputFormulae,OutputFormatUsed,OutputName,OutputDirectory,
OutputFormatUsed,OutputFileName).

%----Format the clauses and write to file
output_formulae_in_format_to_file(FileHeader,IncludeDirectives,
OutputFormulae,OutputFormat,OutputName,OutputDirectory,OutputFormat,
OutputFileName):-
%----Extract the main name of the output format.
    get_format_or_transform_name(OutputFormat,FormatName,FormatAtom),
%----Get the format information (Not a nice way, really).
    get_format_information(FormatName,CommentAtom,FileNameExtension),
%----Make indicator of output format
    concatenate_atoms(['-f ',FormatAtom],OutputFormatText),
    add_tptp2X_comment(old,FileHeader,OutputFormatText,CommentedFileHeader),
%----Make the output file name
    make_output_file_name(OutputDirectory,OutputName,FileNameExtension,
BasicOutputFileName),
    tptp_path_name(BasicOutputFileName,OutputFileName),
%----Redirect the output, opening and closing in case of previous errors
    (OutputFileName \== user -> (
        current_output(CurrentOutput),
        open(OutputFileName,write,OutputFileStream),
        set_output(OutputFileStream))
    ;   true),
%----Do the output
    output_formulae_in_format(CommentedFileHeader,IncludeDirectives,
OutputFormulae,OutputFormat,FormatName,CommentAtom),
%----Restore output direction
    (OutputFileName \== user -> (
        close(OutputFileStream),
        set_output(CurrentOutput))
    ;   true).
%------------------------------------------------------------------------------
%----Delete a file, however the dialect does it
%----Generic simply makes the file 0 bytes, and prays for cleanup later
tptp2X_delete_file_for_dialect(generic,FileName):-
    telling(CurrentOutput),
    tell(FileName),
    told,
    tell(CurrentOutput).

tptp2X_delete_file_for_dialect(binprolog,FileName):-
    tptp2X_delete_file_for_dialect(generic,FileName).

tptp2X_delete_file_for_dialect(yap,FileName):-
    delete_file(FileName).

tptp2X_delete_file_for_dialect(swi,FileName):-
    delete_file(FileName).

tptp2X_delete_file_for_dialect(quintus,FileName):-
    delete_file(FileName).

tptp2X_delete_file_for_dialect(gnu,FileName):-
    delete_file(FileName).

tptp2X_delete_file_for_dialect(sicstus,FileName):-
    delete_file(FileName).

tptp2X_delete_file_for_dialect(eclipse,FileName):-
    delete(FileName).

tptp2X_delete_file(FileName):-
    prolog_dialect(Dialect),
    tptp2X_delete_file_for_dialect(Dialect,FileName).
%------------------------------------------------------------------------------
%----Get a unique value. 
%----Get from a fact that was asserted by the tptp2X script
get_tptp2X_unique_value(UniqueValue):-
%----Use clause to avoid BinProlog error - this means it must be
%----dynamic, which it is if asserted.
    clause(tptp2X_unique_value(UniqueValue),_),
    !.

%----Otherwise give a default
get_tptp2X_unique_value(tptp2X).
%------------------------------------------------------------------------------
%----Make a unique file name for this process, for temporary file
temporary_file_name(TaskForFileName,FileName):-
    get_tptp2X_unique_value(UniqueForProcess),
%----Cut to avoid using other unique values
    !,
    concatenate_atoms(['TemporaryFile',TaskForFileName,UniqueForProcess],
FileName).
%------------------------------------------------------------------------------
%----Write out and reload the clauses, to make real variables
reload_formulae(Formulae,IncludeDirectives,ReloadedFormulae,
ReloadedDictionary):-
    temporary_file_name('ForReload',TemporaryFileName),
    output_formulae_in_format_to_file([],IncludeDirectives,Formulae,tptp,
TemporaryFileName,'/tmp',_OutputFormatUsed,OutputFileName),
    read_formulae_from_file(OutputFileName,ReloadedFormulae,
ReloadedDictionary),
%----Delete the temporary file
    tptp2X_delete_file(OutputFileName).
%------------------------------------------------------------------------------
%----Reject variable transformations
transform_formulae(_,_,_,_,Variable,_,_,_,_,_):-
    var(Variable),
    !,
    write(
'%----ERROR : The transformation is invalid (it looks like a variable).'),nl,
    fail.

%----If a list of transformations, then do each one. Use member due
%----to backtracking approach
transform_formulae(FileHeader,InputFormulae,InputName,Dictionary,
[OneTransformation|OtherTransformations],TransformedFileHeader,
OutputFormulae,OutputName,NewDictionary,TransformationDone):-
    !,
    tptp2X_member(Transformation,[OneTransformation|OtherTransformations]),
    transform_formulae(FileHeader,InputFormulae,InputName,Dictionary,
Transformation,TransformedFileHeader,OutputFormulae,OutputName,NewDictionary,
TransformationDone).

%----If a sequence of transformations, do first then rest
transform_formulae(FileHeader,InputFormulae,InputName,Dictionary,
FirstTransformation + RestOfTransformations,TransformedFileHeader,
OutputFormulae,OutputName,NewDictionary,
FirstTransformationDone+RestOfTransformationsDone):-
    !,
%DEBUG write('DO TRANFORM '),write(FirstTransformation),nl,
%DEBUG write('InputFormulae'),nl,write(InputFormulae),nl,
%DEBUG write('Dictionary'),nl,write(Dictionary),nl,
    transform_formulae(FileHeader,InputFormulae,InputName,Dictionary,
FirstTransformation,IntermediateFileHeader,IntermediateFormulae,
IntermediateName,IntermediateDictionary,FirstTransformationDone),
%DEBUG write('DONE TRANFORM '),write(FirstTransformation),nl,
%DEBUG write('IntermediateFormulae'),nl,write(IntermediateFormulae),nl,
%DEBUG write('IntermediateDictionary'),nl,write(IntermediateDictionary),nl,
    transform_formulae(IntermediateFileHeader,IntermediateFormulae,
IntermediateName,IntermediateDictionary,RestOfTransformations,
TransformedFileHeader,OutputFormulae,OutputName,NewDictionary,
RestOfTransformationsDone).

%----The syntax transformation is internal, to force recomputing syntax
transform_formulae(FileHeader,Formulae,Name,Dictionary,syntax,FileHeader,
Formulae,Name,Dictionary,syntax):-
    !.

%----If a backtrackable transformation, then do them
transform_formulae(FileHeader,InputFormulae,InputName,Dictionary,
Transformation,FileHeader,OutputFormulae,OutputName,NewDictionary,
TransformationAtom):-
    tptp2X_member(Transformation,[expand:conjectures]),
    !,
%----Extract the main name of the transformation
    get_format_or_transform_name(Transformation,TransformationName,
TransformationAtom),
%----Make the transformation query
    TransformationQuery =.. [TransformationName,InputFormulae,Dictionary,
Transformation,OutputFormulae,NewDictionary,FileNameSuffix],
%----Do the transformation
    TransformationQuery,
    concatenate_atoms([InputName,FileNameSuffix],OutputName).

%----If a single transformation, then do it
transform_formulae(FileHeader,InputFormulae,InputName,Dictionary,
Transformation,FileHeader,OutputFormulae,OutputName,NewDictionary,
TransformationAtom):-
%----Extract the main name of the transformation
    get_format_or_transform_name(Transformation,TransformationName,
TransformationAtom),
%----Make the transformation query
    TransformationQuery =.. [TransformationName,InputFormulae,Dictionary,
Transformation,OutputFormulae,NewDictionary,FileNameSuffix],
%----Do the transformation
    TransformationQuery,
    !,
    concatenate_atoms([InputName,FileNameSuffix],OutputName).

%----Error message
transform_formulae(_,_,_,_,Transformation,_,_,_,_,_):-
    write('%----ERROR : The transformation '),
    write(Transformation),
    write(' failed.'),
    nl,
    fail.
%------------------------------------------------------------------------------
%----If shorten transformation, then clobber the header
shorten_header(TransformationsDone,_,
['File'-[' File     : Shortened file, so there is no header']]):-
    any_name(TransformationsDone,ASCII),
%----ASCII for shorten (aaargh, crap code)
    tptp2X_append(_,[115,104,111,114,116,101,110|_],ASCII),
    !.

%----Others do nothing right now
shorten_header(_,FileHeader,FileHeader).
%------------------------------------------------------------------------------
%----Make the Syntax field from the values given
%----CNF case
make_syntax_header_field(SyntaxReplacements,[ClausesLine,LiteralsLine,
ClauseSizeLine,PredicateLine,FunctionLine,VariablesLine,TermDepthLine]):-
    tptp2X_member('CNFF'-Clauses,SyntaxReplacements),
    !,
    tptp2X_member('NNHN'-NonHornClauses,SyntaxReplacements),
    tptp2X_member('UNIT'-UnitClauses,SyntaxReplacements),
    tptp2X_member('RARE'-RangeRestrictedClauses,SyntaxReplacements),
    concatenate_atoms([' Syntax   : Number of clauses    : ',
Clauses,' (',NonHornClauses,' non-Horn;',UnitClauses,' unit;',
RangeRestrictedClauses,' RR)'],ClausesLine),
%----Make literals line
    tptp2X_member('LITS'-Literals,SyntaxReplacements),
    tptp2X_member('EQLS'-EqualityLiterals,SyntaxReplacements),
    concatenate_atoms(['            Number of literals   : ',
Literals,' (',EqualityLiterals,' equality)'],LiteralsLine),
%----Make clause size line
    tptp2X_member('CLSZ'-MaximalClauseSize,SyntaxReplacements),
    tptp2X_member('CLAS'-AverageClauseSize,SyntaxReplacements),
    concatenate_atoms(['            Maximal clause size  : ',
MaximalClauseSize,' (',AverageClauseSize,' average)'],ClauseSizeLine),
%----Make predicate symbols line
    tptp2X_member('PRED'-PredicateSymbols,SyntaxReplacements),
    tptp2X_member('PROP'-PropositionalSymbols,SyntaxReplacements),
    tptp2X_member('MINP'-MinimalPredicateArity,SyntaxReplacements),
    tptp2X_member('MAXP'-MaximalPredicateArity,SyntaxReplacements),
    concatenate_atoms(['            Number of predicates : ',
PredicateSymbols,' (',PropositionalSymbols,' propositional; ',
MinimalPredicateArity,'-',MaximalPredicateArity,' arity)'],PredicateLine),
%----Make function symbols line
    tptp2X_member('FUNC'-FunctionSymbols,SyntaxReplacements),
    tptp2X_member('CNST'-ConstantSymbols,SyntaxReplacements),
    tptp2X_member('MINF'-MinimalFunctorArity,SyntaxReplacements),
    tptp2X_member('MAXF'-MaximalFunctorArity,SyntaxReplacements),
    concatenate_atoms(['            Number of functors   : ',
FunctionSymbols,' (',ConstantSymbols,' constant; ',MinimalFunctorArity,
'-',MaximalFunctorArity,' arity)'],FunctionLine),
%----Make variables line
    tptp2X_member('VARS'-Variables,SyntaxReplacements),
    tptp2X_member('SGTN'-Singletons,SyntaxReplacements),
    concatenate_atoms(['            Number of variables  : ',
Variables,' (',Singletons,' sgn)'],VariablesLine),
%----Make term depth line
    tptp2X_member('TMDP'-MaximalTermDepth,SyntaxReplacements),
    tptp2X_member('TMAD'-AverageTermDepth,SyntaxReplacements),
    concatenate_atoms(['            Maximal term depth   : ',
MaximalTermDepth,' (',AverageTermDepth,' average)'],TermDepthLine).

%----FOF case
make_syntax_header_field(SyntaxReplacements,[FormulaeLine,AtomsLine,
FormulaDepthLine,ConnectivesLine1,ConnectivesLine2,ConnectivesLine3,
PredicateLine,FunctionLine,VariablesLine,TermDepthLine]):-
%----Make formulae line. Leave the CommentAtom off the front as that is
%----added on output.
    tptp2X_member('FOFF'-NumberOfFormulae,SyntaxReplacements),
    !,
    tptp2X_member('UNIT'-NumberOfUnitFormulae,SyntaxReplacements),
    concatenate_atoms([' Syntax   : Number of formulae    : ',
NumberOfFormulae,' (',NumberOfUnitFormulae,' unit)'],FormulaeLine),
%----Atoms line
    tptp2X_member('ATOM'-NumberOfAtoms,SyntaxReplacements),
    tptp2X_member('EQAT'-NumberOfEqualityAtoms,SyntaxReplacements),
    concatenate_atoms(['            Number of atoms       : ',
NumberOfAtoms,' (',NumberOfEqualityAtoms,' equality)'],AtomsLine),
%----Formula depth line
    tptp2X_member('FMDP'-MaximalFormulaDepth,SyntaxReplacements),
    tptp2X_member('FMAD'-AverageFormulaDepth,SyntaxReplacements),
    concatenate_atoms(['            Maximal formula depth : ',
MaximalFormulaDepth,' (',AverageFormulaDepth,' average)'],FormulaDepthLine),
%----1st connectives line
    tptp2X_member('CONN'-NumberOfConnectives,SyntaxReplacements),
    tptp2X_member('NOTS'-NumberOfNOTs,SyntaxReplacements),
    tptp2X_member('ORSS'-NumberOfORs,SyntaxReplacements),
    tptp2X_member('ANDS'-NumberOfANDs,SyntaxReplacements),
    concatenate_atoms(['            Number of connectives : ',
NumberOfConnectives,' (',NumberOfNOTs,'   ~;',NumberOfORs,'   |;',
NumberOfANDs,'   &)'],ConnectivesLine1),
%----2nd connectives line
    tptp2X_member('EQVS'-NumberOfEQUIVs,SyntaxReplacements),
    tptp2X_member('IMPS'-NumberOfIMPLYs,SyntaxReplacements),
    tptp2X_member('PMIS'-NumberOfIMPLIEDs,SyntaxReplacements),
    tptp2X_member('XORS'-NumberOfXORs,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfEQUIVs,' <=>;',NumberOfIMPLYs,'  =>;',NumberOfIMPLIEDs,'  <=;',
NumberOfXORs,' <~>)'],ConnectivesLine2),
%----3rd connectives line
    tptp2X_member('NORS'-NumberOfNORs,SyntaxReplacements),
    tptp2X_member('NANS'-NumberOfNANDs,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfNORs,'  ~|;',NumberOfNANDs,'  ~&)'],ConnectivesLine3),
%----Predicates line
    tptp2X_member('PRED'-NumberOfPredicateSymbols,SyntaxReplacements),
    tptp2X_member('PROP'-NumberOfPropositions,SyntaxReplacements),
    tptp2X_member('MINP'-MinimalPredicateArity,SyntaxReplacements),
    tptp2X_member('MAXP'-MaximalPredicateArity,SyntaxReplacements),
    concatenate_atoms(['            Number of predicates  : ',
NumberOfPredicateSymbols,' (',NumberOfPropositions,' propositional; ',
MinimalPredicateArity,'-',MaximalPredicateArity,' arity)'],PredicateLine),
%----Functors line
    tptp2X_member('FUNC'-NumberOfFunctors,SyntaxReplacements),
    tptp2X_member('CNST'-NumberOfConstants,SyntaxReplacements),
    tptp2X_member('MINF'-MinimalFunctorArity,SyntaxReplacements),
    tptp2X_member('MAXF'-MaximalFunctorArity,SyntaxReplacements),
    concatenate_atoms(['            Number of functors    : ',
NumberOfFunctors,' (',NumberOfConstants,' constant; ',MinimalFunctorArity,
'-',MaximalFunctorArity,' arity)'],FunctionLine),
%----Variables line
    tptp2X_member('VARS'-NumberOfVariables,SyntaxReplacements),
    tptp2X_member('SGTN'-NumberOfSingletons,SyntaxReplacements),
    tptp2X_member('UNIV'-NumberOfUniversals,SyntaxReplacements),
    tptp2X_member('EXIS'-NumberOfExistentials,SyntaxReplacements),
    concatenate_atoms(['            Number of variables   : ',
NumberOfVariables,' (',NumberOfSingletons,' sgn;',NumberOfUniversals,
'   !;',NumberOfExistentials,'   ?)'],VariablesLine),
%----Term depth line
    tptp2X_member('TMDP'-MaximalTermDepth,SyntaxReplacements),
    tptp2X_member('TMAD'-AverageTermDepth,SyntaxReplacements),
    concatenate_atoms(['            Maximal term depth    : ',
MaximalTermDepth,' (',AverageTermDepth,' average)'],TermDepthLine).

%----TFF case
make_syntax_header_field(SyntaxReplacements,[FormulaeLine,AtomsLine,
FormulaDepthLine,ConnectivesLine1,ConnectivesLine2,ConnectivesLine3,
TypeConnectivesLine,PredicateLine,FunctionLine,VariablesLine,TermDepthLine|
ArithmeticList]):-
%----Make formulae line. Leave the CommentAtom off the front as that is
%----added on output.
    tptp2X_member('TFFF'-NumberOfFormulae,SyntaxReplacements),
    !,
    tptp2X_member('UNIT'-NumberOfUnitFormulae,SyntaxReplacements),
    tptp2X_member('TFRM'-NumberOfTypeDecs,SyntaxReplacements),
    concatenate_atoms([' Syntax   : Number of formulae    : ',
NumberOfFormulae,' (',NumberOfUnitFormulae,' unit;',NumberOfTypeDecs,' type)'],
FormulaeLine),
%----Atoms line
    tptp2X_member('ATOM'-NumberOfAtoms,SyntaxReplacements),
    tptp2X_member('EQAT'-NumberOfEqualityAtoms,SyntaxReplacements),
    concatenate_atoms(['            Number of atoms       : ',
NumberOfAtoms,' (',NumberOfEqualityAtoms,' equality)'],AtomsLine),
%----Formula depth line
    tptp2X_member('FMDP'-MaximalFormulaDepth,SyntaxReplacements),
    tptp2X_member('FMAD'-AverageFormulaDepth,SyntaxReplacements),
    concatenate_atoms(['            Maximal formula depth : ',
MaximalFormulaDepth,' (',AverageFormulaDepth,' average)'],FormulaDepthLine),
%----1st connectives line
    tptp2X_member('CONN'-NumberOfConnectives,SyntaxReplacements),
    tptp2X_member('NOTS'-NumberOfNOTs,SyntaxReplacements),
    tptp2X_member('ORSS'-NumberOfORs,SyntaxReplacements),
    tptp2X_member('ANDS'-NumberOfANDs,SyntaxReplacements),
    concatenate_atoms(['            Number of connectives : ',
NumberOfConnectives,' (',NumberOfNOTs,'   ~;',NumberOfORs,'   |;',
NumberOfANDs,'   &)'],ConnectivesLine1),
%----2nd connectives line
    tptp2X_member('EQVS'-NumberOfEQUIVs,SyntaxReplacements),
    tptp2X_member('IMPS'-NumberOfIMPLYs,SyntaxReplacements),
    tptp2X_member('PMIS'-NumberOfIMPLIEDs,SyntaxReplacements),
    tptp2X_member('XORS'-NumberOfXORs,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfEQUIVs,' <=>;',NumberOfIMPLYs,'  =>;',NumberOfIMPLIEDs,'  <=;',
NumberOfXORs,' <~>)'],ConnectivesLine2),
%----3rd connectives line
    tptp2X_member('NORS'-NumberOfNORs,SyntaxReplacements),
    tptp2X_member('NANS'-NumberOfNANDs,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfNORs,'  ~|;',NumberOfNANDs,'  ~&)'],ConnectivesLine3),
%----Type connectives line
    tptp2X_member('TCON'-NumberOfTypeConnectives,SyntaxReplacements),
    tptp2X_member('MAPS'-NumberOfMaps,SyntaxReplacements),
    tptp2X_member('XPRO'-NumberOfXProds,SyntaxReplacements),
    tptp2X_member('UNIO'-NumberOfUnions,SyntaxReplacements),
    tptp2X_member('SUBT'-NumberOfSubtypes,SyntaxReplacements),
    concatenate_atoms(['            Number of type conns  : ',
NumberOfTypeConnectives,' (',NumberOfMaps,'   >;',NumberOfXProds,'   *;',
NumberOfUnions,'   +;',NumberOfSubtypes,'  <<)'],TypeConnectivesLine),
%----Predicates line
    tptp2X_member('PRED'-NumberOfPredicateSymbols,SyntaxReplacements),
    tptp2X_member('PROP'-NumberOfPropositions,SyntaxReplacements),
    tptp2X_member('MINP'-MinimalPredicateArity,SyntaxReplacements),
    tptp2X_member('MAXP'-MaximalPredicateArity,SyntaxReplacements),
    concatenate_atoms(['            Number of predicates  : ',
NumberOfPredicateSymbols,' (',NumberOfPropositions,' propositional; ',
MinimalPredicateArity,'-',MaximalPredicateArity,' arity)'],PredicateLine),
%----Functors line
    tptp2X_member('FUNC'-NumberOfFunctors,SyntaxReplacements),
    tptp2X_member('CNST'-NumberOfConstants,SyntaxReplacements),
    tptp2X_member('MINF'-MinimalFunctorArity,SyntaxReplacements),
    tptp2X_member('MAXF'-MaximalFunctorArity,SyntaxReplacements),
    concatenate_atoms(['            Number of functors    : ',
NumberOfFunctors,' (',NumberOfConstants,' constant; ',MinimalFunctorArity,
'-',MaximalFunctorArity,' arity)'],FunctionLine),
%----Variables line
    tptp2X_member('VARS'-NumberOfVariables,SyntaxReplacements),
    tptp2X_member('SGTN'-NumberOfSingletons,SyntaxReplacements),
    tptp2X_member('UNIV'-NumberOfUniversals,SyntaxReplacements),
    tptp2X_member('EXIS'-NumberOfExistentials,SyntaxReplacements),
    concatenate_atoms(['            Number of variables   : ',
NumberOfVariables,' (',NumberOfSingletons,' sgn;',NumberOfUniversals,
'   !;',NumberOfExistentials,'   ?)'],VariablesLine),
%----Term depth line
    tptp2X_member('TMDP'-MaximalTermDepth,SyntaxReplacements),
    tptp2X_member('TMAD'-AverageTermDepth,SyntaxReplacements),
    concatenate_atoms(['            Maximal term depth    : ',
MaximalTermDepth,' (',AverageTermDepth,' average)'],TermDepthLine),
    tptp2X_member('MATT'-NumberOfArithmeticSymbols,SyntaxReplacements),
    (   NumberOfArithmeticSymbols == '   0'
   ->   ArithmeticList = []
    ;   (   tptp2X_member('MATP'-NumberOfMathPredicates,SyntaxReplacements),
            tptp2X_member('MATF'-NumberOfMathFunctions,SyntaxReplacements),
            tptp2X_member('MATN'-NumberOfNumbers,SyntaxReplacements),
            concatenate_atoms(['            Arithmetic symbols    : ',
NumberOfArithmeticSymbols,' (',NumberOfMathPredicates,' pred;',
NumberOfMathFunctions,' func;',NumberOfNumbers,' numbers)'],
ArithmeticLine),
            ArithmeticList = [ArithmeticLine]
        )
    ).

%----THF case
make_syntax_header_field(SyntaxReplacements,[FormulaeLine,AtomsLine,
FormulaDepthLine,ConnectivesLine1,ConnectivesLine2,ConnectivesLine3,
TypeConnectivesLine,SymbolsLine,VariablesLine1,VariablesLine2]):-
%----Make formulae line. Leave the CommentAtom off the front as that is
%----added on output.
    tptp2X_member('THFF'-NumberOfFormulae,SyntaxReplacements),
    !,
    tptp2X_member('UNIT'-NumberOfUnitFormulae,SyntaxReplacements),
    tptp2X_member('TFRM'-NumberOfTypeFormulae,SyntaxReplacements),
    tptp2X_member('DFRM'-NumberOfDefnFormulae,SyntaxReplacements),
    concatenate_atoms([' Syntax   : Number of formulae    : ',
NumberOfFormulae,' (',NumberOfUnitFormulae,' unit;',NumberOfTypeFormulae,
' type;',NumberOfDefnFormulae,' defn)'],FormulaeLine),
%----Atoms line
    tptp2X_member('ATOM'-NumberOfAtoms,SyntaxReplacements),
    tptp2X_member('EQAT'-NumberOfEqualityAtoms,SyntaxReplacements),
    tptp2X_member('VAAT'-NumberOfVariableAtoms,SyntaxReplacements),
    concatenate_atoms(['            Number of atoms       : ',
NumberOfAtoms,' (',NumberOfEqualityAtoms,' equality;',NumberOfVariableAtoms,
' variable)'],AtomsLine),
%----Formula depth line
    tptp2X_member('FMDP'-MaximalFormulaDepth,SyntaxReplacements),
    tptp2X_member('FMAD'-AverageFormulaDepth,SyntaxReplacements),
    concatenate_atoms(['            Maximal formula depth : ',
MaximalFormulaDepth,' (',AverageFormulaDepth,' average)'],FormulaDepthLine),
%----1st connectives line
    tptp2X_member('CONN'-NumberOfConnectives,SyntaxReplacements),
    tptp2X_member('NOTS'-NumberOfNOTs,SyntaxReplacements),
    tptp2X_member('ORSS'-NumberOfORs,SyntaxReplacements),
    tptp2X_member('ANDS'-NumberOfANDs,SyntaxReplacements),
    tptp2X_member('APPY'-NumberOfAPPLYs,SyntaxReplacements),
    concatenate_atoms(['            Number of connectives : ',
NumberOfConnectives,' (',NumberOfNOTs,'   ~;',NumberOfORs,'   |;',
NumberOfANDs,'   &;',NumberOfAPPLYs,'   @)'],ConnectivesLine1),
%----2nd connectives line
    tptp2X_member('EQVS'-NumberOfEQUIVs,SyntaxReplacements),
    tptp2X_member('IMPS'-NumberOfIMPLYs,SyntaxReplacements),
    tptp2X_member('PMIS'-NumberOfIMPLIEDs,SyntaxReplacements),
    tptp2X_member('XORS'-NumberOfXORs,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfEQUIVs,' <=>;',NumberOfIMPLYs,'  =>;',NumberOfIMPLIEDs,'  <=;',
NumberOfXORs,' <~>)'],ConnectivesLine2),
%----3rd connectives line
    tptp2X_member('NORS'-NumberOfNORs,SyntaxReplacements),
    tptp2X_member('NANS'-NumberOfNANDs,SyntaxReplacements),
    tptp2X_member('PIPI'-NumberOfPis,SyntaxReplacements),
    tptp2X_member('SIGM'-NumberOfSigmas,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfNORs,'  ~|;',NumberOfNANDs,'  ~&;',NumberOfPis,'  !!;',
NumberOfSigmas,'  ??)'],ConnectivesLine3),
%----Type connectives line
    tptp2X_member('TCON'-NumberOfTypeConnectives,SyntaxReplacements),
    tptp2X_member('MAPS'-NumberOfMaps,SyntaxReplacements),
    tptp2X_member('XPRO'-NumberOfXProds,SyntaxReplacements),
    tptp2X_member('UNIO'-NumberOfUnions,SyntaxReplacements),
    tptp2X_member('SUBT'-NumberOfSubtypes,SyntaxReplacements),
    concatenate_atoms(['            Number of type conns  : ',
NumberOfTypeConnectives,' (',NumberOfMaps,'   >;',NumberOfXProds,'   *;',
NumberOfUnions,'   +;',NumberOfSubtypes,'  <<)'],TypeConnectivesLine),
%----Symbols line
    tptp2X_member('FUNC'-NumberOfSymbols,SyntaxReplacements),
    tptp2X_member('GTYP'-NumberOfGlobalTypeDecs,SyntaxReplacements),
%NOT USED    tptp2X_member('GDEF'-NumberOfGlobalDefns,SyntaxReplacements),
    concatenate_atoms(['            Number of symbols     : ',
NumberOfSymbols,' (',NumberOfGlobalTypeDecs,'   :)'],SymbolsLine),
%NOT USED (printing definitions) ;',NumberOfGlobalDefns,'  :=)'],SymbolsLine),
%NOT USED tptp2X_member('CNST'-NumberOfConstants,SyntaxReplacements),
%NOT USED tptp2X_member('MINF'-MinimalSymbolArity,SyntaxReplacements),
%NOT USED tptp2X_member('MAXF'-MaximalSymbolArity,SyntaxReplacements),
%NOT USED ,' (',NumberOfConstants,' constant; ',MinimalSymbolArity,
%NOT USED '-',MaximalSymbolArity,' arity)'],SymbolsLine),
%----1st variables line
    tptp2X_member('VARS'-NumberOfVariables,SyntaxReplacements),
    tptp2X_member('SGTN'-NumberOfSingletons,SyntaxReplacements),
    tptp2X_member('UNIV'-NumberOfUniversals,SyntaxReplacements),
    tptp2X_member('EXIS'-NumberOfExistentials,SyntaxReplacements),
    tptp2X_member('LMDA'-NumberOfLambdas,SyntaxReplacements),
    concatenate_atoms(['            Number of variables   : ',
NumberOfVariables,' (',NumberOfSingletons,' sgn;',NumberOfUniversals,
'   !;',NumberOfExistentials,'   ?;',NumberOfLambdas,'   ^)'],VariablesLine1),
%----2nd variables line
    tptp2X_member('TYPE'-NumberOfTypeDecs,SyntaxReplacements),
%NOT USED    tptp2X_member('DEFN'-NumberOfDefns,SyntaxReplacements),
    tptp2X_member('BIPI'-NumberOfPIs,SyntaxReplacements),
    tptp2X_member('BISI'-NumberOfSIGMAs,SyntaxReplacements),
    concatenate_atoms(['                                         (',
NumberOfTypeDecs,'   :;',
%NOT USED (printing definitions) NumberOfDefns,'  :=;',
NumberOfPIs,'  !>;',NumberOfSIGMAs,'  ?*)'],VariablesLine2).
%------------------------------------------------------------------------------
%----Put leading blanks to get an atom in a field of 4
integer_to_4_digit_atom(Number,Atom):-
    tptp2X_integer_name(Number,NumberASCII),
    (   [D1,D2,D3,D4] = NumberASCII ;
        [D1,D2,D3,D4] = [32|NumberASCII] ;
        [D1,D2,D3,D4] = [32,32|NumberASCII] ;
        [D1,D2,D3,D4] = [32,32,32|NumberASCII]),
    !,
    name(Atom,[D1,D2,D3,D4]).

%----Case where the number is more than 4 characters
integer_to_4_digit_atom(Number,Number).
%------------------------------------------------------------------------------
%----Convert integers to 4 digit atoms for layout
make_syntax_replacement_list([],[]).

%---Minimal and maximal arities are excluded
make_syntax_replacement_list([FirstLabel-FirstValue|RestOfLabelledValues],
[FirstLabel-FirstValue|RestOfLabelledValue4s]):-
    tptp2X_member(FirstLabel,['MINP','MAXP','MINF','MAXF']),
    !,
    make_syntax_replacement_list(RestOfLabelledValues,RestOfLabelledValue4s).

make_syntax_replacement_list([FirstLabel-FirstValue|RestOfLabelledValues],
[FirstLabel-FirstValue4|RestOfLabelledValue4s]):-
    integer_to_4_digit_atom(FirstValue,FirstValue4),
    make_syntax_replacement_list(RestOfLabelledValues,RestOfLabelledValue4s).
%------------------------------------------------------------------------------
%----Update the header with the syntactic information.
%----Clausal case
update_syntax_field(changed,Formulae,FileHeader,UpdatedFileHeader):-
%----Put in a fail here to avoid updating the syntax field
%----Check there's a header
    tptp2X_append(EarlierFields,['Syntax'-_|RestOfFields],FileHeader),
    !,
%----Compute the syntactic information. It's easiest to write it all
%----out to a file and read again, as variables in generated clauses
%----are typically atoms in reality. Other cases too, from transformations.
    reload_formulae(Formulae,[],ReloadedFormulae,_),
%----Do detailed syntactic analysis
    examine_input_syntactics(ReloadedFormulae,SyntacticValues),
%----Make 4 character atoms from values
    make_syntax_replacement_list(SyntacticValues,SyntaxReplacements),
%----Replace in the header
    make_syntax_header_field(SyntaxReplacements,SyntaxFieldLines),
    tptp2X_append(EarlierFields,['Syntax'-SyntaxFieldLines|RestOfFields],
UpdatedFileHeader).

%----Default, do nothing
update_syntax_field(_,_,FileHeader,FileHeader).
%------------------------------------------------------------------------------
%----Extract the base name and type, one of clauses or generator
base_filename_and_type(TPTPFileName,BaseInputName,_FormulaFormat,
TPTPExtension):-
%----Strip off the .Type from the file name
    tptp2X_extension(TPTPFileName,Extension),
%----Get the base name
    tptp2X_basename(TPTPFileName,Extension,BaseInputName),
    !,
%----Need to check the extension. Used to differentiate between problems
%----and generators. Default to .p (erg)
    (tptp2X_member(Extension,['.p','.ax','.eq','.g']) ->
        TPTPExtension = Extension
    ;   TPTPExtension = '.p').

%----In case something goes wrong with the filename, give error message
base_filename_and_type(TPTPFileName,_,_,_):-
    write('%----ERROR : '),
    write(TPTPFileName),
    write(' is not a valid TPTP file name, and has been ignored.'),
    nl,
    fail.
%------------------------------------------------------------------------------
%----Get the clauses from file or by generation
get_header_and_formulae(TPTPFileName,BaseInputName,FileHeader,Extension,_,
BaseInputName,CommentedFileHeader,Formulae,Dictionary):-
%----Check for problem and axiom files
    tptp2X_member(Extension,['.p','.ax','.eq']),
%----Read in the formulae
    read_formulae_from_file(TPTPFileName,Formulae,Dictionary),
%----Make indicator of source
    concatenate_atoms([BaseInputName,Extension],ReadingText),
    add_tptp2X_comment(old,FileHeader,ReadingText,CommentedFileHeader).

get_header_and_formulae(TPTPFileName,BaseInputName,RawFileHeader,'.g',
GenerationSpecification,BaseOutputName,CommentedFileHeader,ReloadedFormulae,
ReloadedDictionary):-
%----Load the file with its code
    tptp2X_load(TPTPFileName),
%----Generate the clauses and make output name
    generate_clauses_and_header(BaseInputName,RawFileHeader,
GenerationSpecification,BaseOutputName,UpdatedFileHeader,Formulae,Generation),
%----Reload the clauses to get real variables. Numbervars to give them names.
    numbervars_each_formula(Formulae),
    reload_formulae(Formulae,[],ReloadedFormulae,ReloadedDictionary),
%----Make indicator of source. Do hack to make two parameters use infix :
    concatenate_atoms(['-s',Generation,' ',BaseInputName,'.g'],GenerationText),
    add_tptp2X_comment(old,UpdatedFileHeader,GenerationText,
CommentedFileHeader).
%------------------------------------------------------------------------------
%----Numbervars each of the axioms
numbervars_each_formula([]).

numbervars_each_formula([FirstFormula|RestOfFormulae]):-
    FirstFormula =.. [_,_,_,Formula|_],
    numbervars(Formula,0,_),
    numbervars_each_formula(RestOfFormulae).
%------------------------------------------------------------------------------
%----Check if the formulae have changed, in which case statistics are computed
%----This one for dubugging - forces it to happen
%DEBUG has_changed_for_syntax(_,_,_,_,changed):-!.

%----Needed if specified as the transformation
has_changed_for_syntax(_,_,syntax,_,changed):-
    !.

%----Not needed if existing syntax field is unchanged
has_changed_for_syntax(Formulae,OutputFormulae,_,_,unchanged):-
    Formulae == OutputFormulae,
    !.

%----For problems that never had any syntax - do nothing
has_changed_for_syntax(_,_,_,FileHeader,unchanged):-
    \+ tptp2X_member('Syntax'-_,FileHeader),
    !.

has_changed_for_syntax(_,_,_,_,changed).
%------------------------------------------------------------------------------
%----Do this in all possible ways by backtracking
make_all_outputs(TPTPFileName,BaseInputName,Extension,GenerationSpecification,
Transformation,OutputFormat,OutputDirectory):-
%----Read in the file header
    read_header_from_file(TPTPFileName,BaseInputName,FileHeader),
%----Add a new tptp2X line to the comments
    add_tptp2X_comment(new,FileHeader,'',CommentedFileHeader),
%----Get the formulae
    get_header_and_formulae(TPTPFileName,BaseInputName,CommentedFileHeader,
Extension,GenerationSpecification,UpdatedBaseInputName,FormulaeFileHeader,
Formulae,Dictionary),
%----Do a transformation by combination from the transformation list.
    transform_formulae(FormulaeFileHeader,Formulae,UpdatedBaseInputName,
Dictionary,Transformation,TransformedFileHeader,OutputFormulae,BaseOutputName,
NewDictionary,TransformationDone),
%----Add comment about transformations done if not none
    (TransformationDone == none
    ->  TransformCommentedFileHeader = TransformedFileHeader
    ;   (   concatenate_atoms(['-t ',TransformationDone],TransformationText),
            add_tptp2X_comment(old,TransformedFileHeader,TransformationText,
TransformCommentedFileHeader)
        )
    ),
%----If shorten transformation, then clobber the header
    shorten_header(TransformationDone,TransformCommentedFileHeader,
ShortenedFileHeader),
%----Instantiate variables to their names. First use the names picked
%----up from reading, then use numbervars to catch any new unnamed variables
%----that may have been added during transformation. Note: This is done
%----before update_syntax_field because there's a reload in there, and
%----Eclipse has some problems with variables when they become singleton.
    instantiate_variables_from_dictionary(NewDictionary),
    numbervars_each_formula(OutputFormulae),
%----Check if header needs syntax update (avoid where possible)
    has_changed_for_syntax(Formulae,OutputFormulae,TransformationDone,
ShortenedFileHeader,ChangedOrNot),
%----Update the Syntax field in the header for the new formulae
    update_syntax_field(ChangedOrNot,OutputFormulae,ShortenedFileHeader,
SyntaxFileHeader),
%----Do the output
    output_formulae_in_format_to_file(SyntaxFileHeader,[],OutputFormulae,
OutputFormat,BaseOutputName,OutputDirectory,_OutputFormatUsed,
OutputFileName),
    (OutputDirectory \== user ->
        (   write(TPTPFileName),
%----Need the full name for SystemOnTPTP processing
%----        (   write(BaseInputName),
            write(' -> '),
            write(OutputFileName),
            nl)
        ;   true),
    fail.

make_all_outputs(_,_,_,_,_,_,_).
%------------------------------------------------------------------------------
%----Check that a Prolog dialect and a tptp_directory exist
check_tptp2X_installation:-
    prolog_dialect(_),
    get_tptp_directory(_),
    !.

check_tptp2X_installation:-
    write('The tptp2X utility has not been installed correctly'),
    nl,
    write('Please check that a Prolog dialect and the TPTP directory'),
    nl,
    write('have been specified in the tptp2X.config file.'),
    nl,
    fail.
%------------------------------------------------------------------------------
%----The entry point 
tptp2X(TPTPFileName,GenerationSpecification,Transformation,OutputFormat,
OutputDirectory):-
%----Check that tptp2X has been installed
    check_tptp2X_installation,
%----Declare the operators used in the TPTP. They must be declared here
%----so that they are declared at run, rather than compile time. If 
%----they are only done as :-op(100,fx,++)., then compiled versions of 
%----this code will not work
    declare_TPTP_operators,
%----Extract the base file name
    base_filename_and_type(TPTPFileName,BaseInputName,_,Extension),
%----Get header and the clauses from file or by generation. There is 
%----backtracking to do all combinations here.
    make_all_outputs(TPTPFileName,BaseInputName,Extension,
GenerationSpecification,Transformation,OutputFormat,OutputDirectory).
%------------------------------------------------------------------------------
%----The old entry point, for backwards compatibility
tptp2X(TPTPFileName,Transformation,OutputFormat,OutputDirectory):-
    tptp2X(TPTPFileName,none,Transformation,OutputFormat,OutputDirectory).
%------------------------------------------------------------------------------