%------------------------------------------------------------------------------
% File     : <For TPTP use only>
% Domain   : <The domain of the problem, from the TPTP domains>
% Problem  : <A one line description of the problem>
% Version  : <If this is a different form of an existing problem, why it is 
%             different>
% English  : <A full description of the problem>

% Refs     : <Relevant references>
% Source   : <The Ref where the formulae originate from>
% Names    : <The name(s) of this problem in the literature>

% Status   : <A value from the SZS ontology>
% Rating   : <Don't worry about this one - we'll do it automatically>
% Syntax   : <Don't worry about this one - we'll do it automatically>
% SPC      : <Don't worry about this one - we'll do it automatically>

% Comments : <Anything else that might be useful>
%------------------------------------------------------------------------------
<Any unambiguous representation of the formulae>
%------------------------------------------------------------------------------