The usage of cdiprover3 is

$ ./cdiprover3 <options> <filename> <timeout>

- <timeout> specifies the maximum number of seconds until cdiprover3 stops
  looking for a suitable polynomial or context-dependent interpretation.
- <filename> specifies the path to the file which contains the TRS that
  shall be considered.
- For <options>, the following switches are available:
--- -o <filename2>: specifies that the output should go to a file with the
    path <filename>/<filename2>.txt instead of standard output.
--- -c <class>: sets the parametric polynomial that is used for searching
    a suitable polynomial interpretation. The possible values
    for <class> are "linear", "simple", "simplemixed", "quadratic",
    "additive", "pizerolinear", "pizerosimple", "pizerosimplemixed",
    "pizeroquadratic", "deltasimple", and "restricteddeltasimple". If this
    switch is not specified, then cdiprover3 first looks for a polynomial
    interpretation with additive polynomials. If that is not successful,
    then real context-dependent interpretations with restricted
    delta-simple polynomials are searched.
--- -b <bound> sets the upper bound for the coefficient variables to
    bound.
--- -i: If this switch is activated, then the given number of bits is not
    immediately used fully. Instead, first, the program starts by looking
    for solutions which use only one bit per variable. Upon each failure,
    the number of bits is increased by 1 until a timeout occurs, or the
    bound specified in the option -b is fully covered.

The input files have to follow the same syntax as the files in the termination
problems database. The format specification for this database is available at
http://www.lri.fr/~marche/tpdb/format.html.