0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
a(b(x)) → b(a(x)) a(c(x)) → x
a1 > b1 > c1
a_1=1 b_1=2 c_1=1