The usage of cdiprover2 is

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

- <timeout> specifies the maximum number of seconds until cdiprover2 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 cdiprover2 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 bound is not
    immediately used fully. Instead, first, the program looks for
    solutions using the bounds (2^n)-1 starting from n=1 until the bound
    exceeds the bound given in the option -b.

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.