Usage
-----

./fort-h [OPTION...] FORMULA FILE.trs...

OPTIONS
-------

  -h, -?   --help              print usage information
  -v       --verbose           verbose output
  -w       --witness           enable witness generation
  -c FILE  --certificate=FILE  write certificate to FILE
  -i       --info              enable additional information in the certificate
           --json              outputs information in JSON-format
                               implies -v and --only-info
           --only-info         only output information on the problem
                               makes FILE.trs optional (useful together with -v)

FILE Syntax
-----------

The TRS file syntax follows the format used by COPS
  TRS format:   http://project-coco.uibk.ac.at/problems/trs.php
  MSTRS format: http://project-coco.uibk.ac.at/problems/mstrs.php

It also support two TRSs per FILE with the COM format
  COM format:   http://project-coco.uibk.ac.at/2019/categories/commutation.php

FORMULA Syntax
--------------

The syntax for <formula> is given by the following BNF:

<formula>        = <formula> <connective> <formula>
                 | '~' <formula>
                 | <quantifier> <varlist> ( <formula> )
	         | <property>
                 | <var> <relation> <var>
                 | <indices> <formula>
                 | {+ <nat> } <formula>
                 | ( <formula> )
<connective>     = '&' | '|' | '=>' | '<=>'
<quantifier>     = forall | exists
<relation>       = '->' | '->=' | '->+' | '->*' | '->!' | '-||->'
                 | '->e' | '->be' | '->e+' | '->be+' | '->e*' | '->be*'
                 | '<->' | '<->*' | 'join' | 'meet' | '='
                 | '<-' | '=<-' | '+<-' | '*<-' | '<-!' | '<-||-'
                 | 'e<-' | 'be<-' | '+e<-' | '+be<-' | '*e<-' | '*be<-'
                 | '->e=' | '->be=' | '=e<-' | '=be<-'
<property>       = <prop_of_system> | <prop_of_term>
<prop_of_system> = CR | WCR | SCR | NFP | UNC | UNR | WN | SN 
	         | GCR | GWCR | GSCR | GNFP | GUNC | GUNR
	         | <binary_prop> ( <indices>, <indices> )
<binary_prop>    = COM | GCOM | CE | GCE | NE | GNE
<prop_of_term>   = <prop> ( <var> ) | <finiteness> (<binrel>, <var>)
<prop>           = CR | WCR | WN | NFP | SN | NF | SCR | UNR
<finiteness>     = INF | FIN
<binrel>         = <relation> | '~' <binrel> | <binrel> <connective> <binrel>
                 | ( <binrel> )
<indices>        = '['<nat_list>']'

Here <nat> denotes a natural number, and <var> any nonempty sequence of
alphanumeric symbols starting with a letter. <nat_list> and <var_list> are comma
separated lists of <nat>s or <var>s.

Any <relation> denotes the expected rewrite relation. The addition of 'e' (as in
'->e') denotes rewriting at the root, 'be' ('->be') below the root.