Checking LCTRSs for confluence on a given benchmark.

Usage: crest-benchmark BENCHMARKPATH [-t|--timeout TIMEOUT] 
                       [-j|--threads THREADS] [--z3] [--cvc5] [--yices] [--its] 
                       [--seq] [-m|--method INT] [--html]

  Analyzing LCTRSs on a benchmark directory (searches for files with ".lctrs"
  file extension).

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 (default is 1)
  --z3                     Use Z3 (default)
  --cvc5                   Use CVC5
  --yices                  Use Yices
  --its                    Parse an ITS and looks for files with ".koat"
                           extension (Note: not everything is supported)
  --seq                    Uses the sequential mode of crest without any
                           concurrency.
  -m,--method INT          Specify method (if not set, all are used): 1 =
                           Orthogonality, 2 = Weak Orthogonality, 3 = Strongly
                           Closedness, 4 = Parallel Closedness, 5 = Almost
                           Parallel Closedness
  --html                   Print proofs to files and produce a
                           "crest-benchmark.html".