Input TRS:
    1: active(f(x)) -> mark(f(f(x)))
    2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
    3: mat(f(x),f(y())) -> f(mat(x,y()))
    4: chk(no(c())) -> active(c())
    5: mat(f(x),c()) -> no(c())
    6: f(active(x)) -> active(f(x))
    7: f(no(x)) -> no(f(x))
    8: f(mark(x)) -> mark(f(x))
    9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #chk(no(f(x))) -> #f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
   #2: #chk(no(f(x))) -> #chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))
   #3: #chk(no(f(x))) -> #mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)
   #4: #chk(no(f(x))) -> #f(f(f(f(f(f(f(f(f(f(X()))))))))))
   #5: #chk(no(f(x))) -> #f(f(f(f(f(f(f(f(f(X())))))))))
   #6: #chk(no(f(x))) -> #f(f(f(f(f(f(f(f(X()))))))))
   #7: #chk(no(f(x))) -> #f(f(f(f(f(f(f(X())))))))
   #8: #chk(no(f(x))) -> #f(f(f(f(f(f(X()))))))
   #9: #chk(no(f(x))) -> #f(f(f(f(f(X())))))
   #10: #chk(no(f(x))) -> #f(f(f(f(X()))))
   #11: #chk(no(f(x))) -> #f(f(f(X())))
   #12: #chk(no(f(x))) -> #f(f(X()))
   #13: #chk(no(f(x))) -> #f(X())
   #14: #f(active(x)) -> #active(f(x))
   #15: #f(active(x)) -> #f(x)
   #16: #tp(mark(x)) -> #tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
   #17: #tp(mark(x)) -> #chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))
   #18: #tp(mark(x)) -> #mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)
   #19: #tp(mark(x)) -> #f(f(f(f(f(f(f(f(f(f(X()))))))))))
   #20: #tp(mark(x)) -> #f(f(f(f(f(f(f(f(f(X())))))))))
   #21: #tp(mark(x)) -> #f(f(f(f(f(f(f(f(X()))))))))
   #22: #tp(mark(x)) -> #f(f(f(f(f(f(f(X())))))))
   #23: #tp(mark(x)) -> #f(f(f(f(f(f(X()))))))
   #24: #tp(mark(x)) -> #f(f(f(f(f(X())))))
   #25: #tp(mark(x)) -> #f(f(f(f(X()))))
   #26: #tp(mark(x)) -> #f(f(f(X())))
   #27: #tp(mark(x)) -> #f(f(X()))
   #28: #tp(mark(x)) -> #f(X())
   #29: #f(no(x)) -> #f(x)
   #30: #mat(f(x),f(y())) -> #f(mat(x,y()))
   #31: #mat(f(x),f(y())) -> #mat(x,y())
   #32: #active(f(x)) -> #f(f(x))
   #33: #f(mark(x)) -> #f(x)
   #34: #chk(no(c())) -> #active(c())
Number of SCCs: 1, DPs: 5, edges: 17
	SCC { #14 #15 #29 #32 #33 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
    tp(x1)	weight: 0
     y()	weight: 0
    no(x1)	weight: (/ 1 4) + x1
 #mat(x1,x2)	weight: 0
   chk(x1)	weight: 0
     c()	weight: 0
     f(x1)	weight: (/ 1 4) + x1
  mark(x1)	weight: (/ 1 4) + x1
   #f(x1)	weight: x1
  #tp(x1)	weight: 0
active(x1)	weight: (/ 3 4) + x1
   mat(x1,x2)	weight: 0
#active(x1)	weight: (/ 1 4) + x1
     X()	weight: 0
 #chk(x1)	weight: 0
    Usable rules: { 1 6..8 }
    Removed DPs: #14 #15 #29 #32 #33
Number of SCCs: 0, DPs: 0, edges: 0
YES