Usage
-----

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

Synthesize one or more systems with property FORMULA.

OPTIONS
-------

  -h, -?     --help                print usage information
             --verbose, --history  activate additional history output
  -l         --lv                  search for linear variable separated ES
  -n NUM     --num=NUM             number of systems to synthesise, default: 1
  -S STRING  --signature=STRING    signature, default: creates sig with sigstep (-s)
  -a STRING  --arity=STRING        signature with arities, default: creates sig with
                                   sigstep (-s)
  -s NUM     --sigStep=NUM         steps to generate default signature, default: 2
  -A NUM     --maxArity=NUM        maximal arity in generated signature, default: 3
  -D NUM     --maxDepth=NUM        maximum depth, default: 3
  -r NUM     --minNumRules=NUM     minimum number of rules, default: 0
  -R NUM     --maxNumRules=NUM     maximum number of rules, default: 3
  -v NUM     --vars=NUM            maximum number of variables, default: 1
  -j NUM     --jobs=NUM            set number of jobs to run in parallel, default: 1

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

The TRS file syntax follows the format used by COPS
  TRS format: http://project-coco.uibk.ac.at/problems/trs.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.