(1) DirectTerminationProof (EQUIVALENT transformation)
We use [DIRECT_TERMINATION] with the following order to prove termination.
Knuth-Bendix order [KBO] with precedence:
g1 > 0 > f1 > s1
and weight map:
0=1
g_1=0
s_1=1
f_1=1
The variable weight is 1