CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria: * Dependency pairs: o plain/marks, o graphs refinements with or without sub-term criterion, as well as various orderings: * Polynomial interpretations, * Matrix interpretations, * Full RPO with status, with AFS refinements. CiME 3 may be used alone (searching for proofs and producing certificates) or in conjunction with your own prover via xml input/output and translation to .v files. Note that in addition to its own xml format, CiME 3 now supports CPF for the aformentioned techniques.