The Unused Sequents

• Serge Autexier requested

  that the TPTP syntax include sequents

• In the TPTP syntax

       <thf_sequent>          ::= <thf_tuple> <gentzen_arrow> <thf_tuple>
       <tfx_sequent>          ::= <tfx_tuple> <gentzen_arrow> <tfx_tuple>
       <fof_sequent>          ::= <fof_formula_tuple> <gentzen_arrow>
                                  <fof_formula_tuple> | (<fof_sequent>)
       <gentzen_arrow>        ::= --> 

• Should sequents be

  retained, removed, ignored?