Constrained REwriting Sortware Tool version 0.8.7.1 for analyzing LCTRSs.

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

  (Non-)Termination 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
  -s,--strategy STRING     Specify a comma-separated list of methods (if not
                           set, all are used): {'dpg' = DP graph with no SCCs
                           'crodp' = Constrained Reduction Order on DP problem
                           'cro' = Constrained Reduction Order 'vc' = Value
                           Criterion 'vclin' = Value Criterion with linear
                           combination projection 'sc' = Subterm Criterion
                           'rpair' = Reduction Pair (using some of 'cro', 'vc',
                           'sc', 'vclin'); e.g.: 'rpair[cro,vclin]'}
  --html                   Print proofs to files and produce a
                           "crest-sn-benchmark.html".