Constrained REwriting Sortware Tool version 0.8.3.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] [-m|--methods [Int]] [--ari]

  (Non-)Confluence analysis executable of the Constrained REwriting Sortware
  Tool version 0.8.3.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
  -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 = Toyama 81 based
                           on PCPs
  --ari                    Prints the LCTRS fully sorted in the ARI format.