Checking LCTRSs for confluence.

Usage: prototype-cade FILEPATH [-t|--timeout TIMEOUT] [-a|--ARI] [--cps] 
                      [-v|--verb] [--debug] [--result] [--z3] [--cvc5] [--yices]
                      [--its] [--seq] [-m|--method INT]

  Analyzing LCTRSs.

Available options:
  -h,--help                Show this help text
  FILEPATH                 Path to the source file
  -t,--timeout TIMEOUT     Timeout of the analysis
  -a,--ARI                 Transform a standard WST format TRS into ARI format
  --cps                    Compute the critical pairs
  -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
  --yices                  Use Yices as SMT solver
  --its                    Parse an ITS (Note: not everything is supported)
  --seq                    Uses sequential mode of crest without concurrency
  -m,--method INT          Specify method (if not set, all are used): 1 =
                           Orthogonality, 2 = Weak Orhtogonality, 3 = Strongly
                           Closedness, 4 = Parallel Closedness, 5 = Almost
                           Parallel Closedness