Constrained REwriting Sortware Tool version 0.8.7.0 for analyzing LCTRSs.

Usage: crest-cr FILEPATH [-t|--timeout TIMEOUT] [-j|--threads THREADS] [--cps] 
                [--pcps] [--wcr] [-v|--verb] [--debug] [--result] [--z3] 
                [--cvc5] [--yices] [--seq] [-s|--strategy STRING] [--ari]

  (Non-)Confluence analysis executable of the Constrained REwriting Sortware
  Tool version 0.8.7.0.

Available options:
  -h,--help                Show this help text
  FILEPATH                 Path to the source file
  -t,--timeout TIMEOUT     Timeout of the analysis
  -j,--threads THREADS     Number of Threads for the analysis
  --cps                    Compute the constrained critical pairs
  --pcps                   Compute the constrained parallel critical pairs
  --wcr                    Show local confluence (Note: termination is not
                           shown!)
  -v,--verb                Get more verbose output
  --debug                  Debug mode which shows also internal errors
  --result                 Suppress any output except result and time
  --z3                     Use Z3 as SMT solver (default)
  --cvc5                   Use CVC5 as SMT solver (experimental)
  --yices                  Use Yices as SMT solver (experimental)
  --seq                    Uses sequential mode of crest without concurrency
  -s,--strategy STRING     Specify a comma-separated list of methods (if not
                           set, all are used): {'o' = Orthogonality 'wo' = Weak
                           Orthogonality 'sc' = Strongly Closedness 'pc' =
                           Parallel Closedness 'apc' = Almost Parallel
                           Closedness (both sequences parallel steps) 'apch' =
                           Almost Parallel Closedness (heuristic) 'dc' =
                           Development Closedness 'adc' = Almost Development
                           Closedness (both sequences multi-steps) 'adch' =
                           Almost Development Closedness (heuristic) 'dnfs' =
                           Non Confluence 'kbc' = Knuth-Bendix Criterion 'pcp' =
                           Toyama 81 based on PCPs}
  --ari                    Prints the LCTRS fully sorted in the ARI format.