[Termtools] New elements in CPF

[René Thiemann]

Dear all,

some elements have been added to the certification problem format (CPF) in the area of
complexity proofs, nontermination proofs, and termination proofs.

- complexity:
  - input problem ((relative) TRS + strategy + complexity measure (RC/DC) + complexity class)
  - rule shifting from strict to relative using orders
  - trivial (no strict rules)

- nontermination:  
  - switch to termination
  - switch to innermost termination
  - reduce innermost strategy component
  - instantiation
  - non-looping non-termination

- termination:
  - KBO with weight-function, smallest weight w0, and (quasi)-precedence
  
Comments are welcome, and if there are none, then these elements will be fixed by May 1, 2012 and they
will be used in the upcoming termination competition.

See http://cl-informatik.uibk.ac.at/software/cpf/#devel for more details.

Best regards,
René