Input TRS:
    1: c(z,x,a()) -> f(b(b(f(z),z),x))
    2: b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
    3: f(c(c(z,a(),a()),x,a())) -> z
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #b(y,b(z,a())) -> #f(b(c(f(a()),y,z),z))
   #2: #b(y,b(z,a())) -> #b(c(f(a()),y,z),z)
   #3: #b(y,b(z,a())) -> #c(f(a()),y,z)
   #4: #b(y,b(z,a())) -> #f(a())
   #5: #c(z,x,a()) -> #f(b(b(f(z),z),x))
   #6: #c(z,x,a()) -> #b(b(f(z),z),x)
   #7: #c(z,x,a()) -> #b(f(z),z)
   #8: #c(z,x,a()) -> #f(z)
Number of SCCs: 1, DPs: 4, edges: 8
	SCC { #2 #3 #6 #7 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
     a()	weight: (/ 33 2)
     b(x1,x2)	weight: max{0, (/ 21 2) + x1, (/ 19 2) + x2}
     c(x1,x2,x3)	weight: max{0, 7 + x1, -4 + x2}
     f(x1)	weight: max{0, -14 + x1}
   #f(x1)	weight: 0
   #c(x1,x2,x3)	weight: max{0, -2 + x1, -12 + x2, -17 + x3}
   #b(x1,x2)	weight: max{0, (- (/ 23 2)) + x1, -12 + x2}
    Usable rules: { 1..3 }
    Removed DPs: #2 #3
Number of SCCs: 0, DPs: 0, edges: 0
YES