### XML-Format

From version 1.12 onwards, CeTA uses the CPF format, version 2.x as input. CeTA versions 1.06 - 1.11 use CPF version 1.0 as input. Older versions of CeTA use this proof format.

Since most elements of CPF are fully supported, we just list some items which might be useful to know when creating proofs that should be read by CeTA.

- As input, only TRSs and relative TRSs are supported, where an arbitrary innermost strategy can be defined. However, no equations may be present.
- The technique
*argumentFilterProc*is unsupported. - The technique
*unlabel*is no longer supported. One can use*split*instead. - One can use linear
*polynomial*interpretations with*matrices*over*naturals*,*rationals*,*arctic*, or*arcticBelowZero*as possible*domain*s. Here, in the*function*s, everything has to be a*matrix*, even the constant parts. Non-linear polynomial interpretations are only supported for rationals and naturals. Make sure that the*degree*element is at least 2 if you want to use non-linear interpretations.

Also*matrixInterpretation*s where the constants are vectors are supported. These are automatically extended to matrices by filling in zeros. - Polynomials with negative constants are supported using Pleft and Pright approximations for linear interpretations. Here, one must not use
*max*-elements (to indicate that*Pol(f(x)) = x - 1*means*Pol(f(x)) = max(0, x-1)*, but one just has to encode*x - 1*. - Any set of usable rules can be used (ren/cap or tcap or icap, with or without regarding argument filter). However, the given set of usable rules must be closed under usable rules of right-hand sides.
- For match- and roof-bounds only left-linear TRSs are supported, and the automata have to satisfy the compatibility condition of Geser et al., not quasi-compatibility of Korp et al.
- Any dependency graph estimation can be used that is subsumed by E(I)DG
^{***}(root-symbol-comparison, ren/cap, tcap, icap, looking both forward and backward).

The archive containing the sources of IsaFoR/CeTA contains a number of examples in the CPF format.