Cdiprover can be executed with the command

$ ./cdiprover <options> <file>.trs <timeout>

- <timeout> specifies the number of seconds until cdiprover stops
  looking for a polynomial interpretation and context-dependent interpretation
  stubs.
- <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. Legal values
    for <class> are "linear", "simple", "simplemixed", "quadratic".
--- -b <bound>: sets the upper bound for the coefficient variables
    to <bound>.

In addition to the normal output, cdiprover also outputs stubs of
context-dependent interpretations into files 

<filename>.solution<n>.con

where <n> is a running number. These files can be directly used as input
for cdisolver. The grammar of the .con files is given in Table 6.1 of the
master thesis.
A specification consists of four parts. The first part declares a list of
variables that is going to be used in the parts below. Otherwise, it would
not be possible to differentiate between variables and constant function
symbols when parsing a file. The second part declares the rewrite rules of
the considered TRS. The third part declares the stub of the context-dependent
interpretation. The last part declares a list of pairs (a,b), which means
that the Delta-monotonicity constraint has to be checked for the function
symbol "a" and argument position "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
\texttt{http://www.lri.fr/~marche/tpdb/format.html}.