The benchmarks result from termination analyses of term rewriting systems from the Termination Problem Data Base, which is used for the annual International Termination Competition. Its current version 3.2 can be downloaded from: http://www.lri.fr/~marche/tpdb/tpdb-3.2.tgz Most of the benchmarks were generated by using extensions of the techniques described in the paper "SAT Solving for Termination Analysis with Polynomial Interpretations" that has been submitted to SAT 2007. SRS/Marche/turing_copy.srs : AProVE07-17 SRS/Marche/turing_mult.srs : AProVE07-13 AProVE07-14 TRS/AG01/#3.39.trs : AProVE07-20 AProVE07-21 TRS/AG01/#3.40.trs : AProVE07-04 AProVE07-12 TRS/AProVE/AAECC-ring.trs : AProVE07-10 AProVE07-18 AProVE07-19 TRS/AProVE/AAECC.trs : AProVE07-15 TRS/AProVE/JFP_Ex31.trs : AProVE07-25 AProVE07-27 TRS/AProVE/Liveness_WRS.trs : AProVE07-16 TRS/HM/t008.trs : AProVE07-22 TRS/HM/t009.trs : AProVE07-01 AProVE07-02 AProVE07-03 AProVE07-08 AProVE07-09 AProVE07-26 TRS/TRCSR/Ex49_GM04_C.trs : AProVE07-23 TRS/TRCSR/Ex4_7_15_Bor03_C.trs : AProVE07-05 AProVE07-06 AProVE07-07 TRS/TRCSR/Ex6_15_AEL02_GM.trs : AProVE07-24 TRS/secret05/cime3.trs : AProVE07-11