YES Termination: (Ranking Functions Found) ------------ f1543_0_clear_EQ: < < arg3 > > method 1