CeTA (2.15) rejected this (in TRS relative certified): http://nfa.imn.htwk-leipzig.de/termcomp/display_proof/26938788 actual certifier output is: $ ceta-2.15 rt2-4.cpf REJECTED relative termination proof not accepted 1: the proof contains a termination assumption or unknown proof