Constrained REwriting Sortware Tool version 0.8.7.1 for analyzing LCTRSs.

Usage: crest-cr-benchmark BENCHMARKPATH [-t|--timeout TIMEOUT] 
                          [-j|--threads THREADS] [--z3] [--cvc5] [--yices] 
                          [--seq] [-s|--strategy STRING] [--html]

  (Non-)Confluence analysis benchmarking executable of the Constrained REwriting
  Sortware Tool version 0.8.7.1. Searches for files with ".ari" file extension
  in the given directory.

Available options:
  -h,--help                Show this help text
  BENCHMARKPATH            Path to directory containing benchmarks
  -t,--timeout TIMEOUT     Timeout of the analysis
  -j,--threads THREADS     Number of threads for the analysis
  --z3                     Use Z3 (default)
  --cvc5                   Use CVC5
  --yices                  Use Yices
  --seq                    Uses the sequential mode of crest without any
                           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}
  --html                   Print proofs to files and produce a
                           "crest-benchmark.html".