Constrained REwriting Sortware Tool version 0.8.3.0 for analyzing LCTRSs.

Usage: crest-cr-benchmark BENCHMARKPATH [-t|--timeout TIMEOUT] 
                          [-j|--threads THREADS] [--z3] [--cvc5] [--yices] 
                          [--seq] [-m|--methods [Int]] [--html]

  (Non-)Confluence analysis benchmarking executable of the Constrained REwriting
  Sortware Tool version 0.8.3.0. 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.
  -m,--methods [Int]       Specify an integer list of methods (if not set, all
                           are used): 1 = Orthogonality, 2 = Weak Orthogonality,
                           3 = Strongly Closedness, 4 = Parallel Closedness, 5 =
                           Almost Parallel Closedness (both sequences parallel
                           steps), 6 = Almost Parallel Closedness (heuristic), 7
                           = Development Closedness, 8 = Almost Development
                           Closedness (both sequences multi-steps), 9 = Almost
                           Development Closedness (heuristic), 10 = Non
                           Confluence, 11 = Newmans Lemma, 12 = Toyama81
  --html                   Print proofs to files and produce a
                           "crest-benchmark.html".