YES
TRS:
 {       f(mark(x)) -> mark(f(x)),
       f(active(x)) -> active(f(x)),
           f(no(x)) -> no(f(x)),
       active(f(x)) -> mark(f(f(x))),
      chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
       chk(no(c())) -> active(c()),
  mat(f(x), f(y())) -> f(mat(x, y())),
     mat(f(x), c()) -> no(c()),
        tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
 DP:
  Strict:
   {       f#(mark(x)) -> f#(x),
         f#(active(x)) -> f#(x),
         f#(active(x)) -> active#(f(x)),
             f#(no(x)) -> f#(x),
         active#(f(x)) -> f#(f(x)),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))),
        chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))),
        chk#(no(f(x))) -> f#(f(f(f(f(X()))))),
        chk#(no(f(x))) -> f#(f(f(f(X())))),
        chk#(no(f(x))) -> f#(f(f(X()))),
        chk#(no(f(x))) -> f#(f(X())),
        chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
        chk#(no(f(x))) -> f#(X()),
        chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)),
        chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x),
         chk#(no(c())) -> active#(c()),
    mat#(f(x), f(y())) -> f#(mat(x, y())),
    mat#(f(x), f(y())) -> mat#(x, y()),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))),
          tp#(mark(x)) -> f#(f(f(f(f(f(X())))))),
          tp#(mark(x)) -> f#(f(f(f(f(X()))))),
          tp#(mark(x)) -> f#(f(f(f(X())))),
          tp#(mark(x)) -> f#(f(f(X()))),
          tp#(mark(x)) -> f#(f(X())),
          tp#(mark(x)) -> f#(X()),
          tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)),
          tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x),
          tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
  Weak:
  {       f(mark(x)) -> mark(f(x)),
        f(active(x)) -> active(f(x)),
            f(no(x)) -> no(f(x)),
        active(f(x)) -> mark(f(f(x))),
       chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
        chk(no(c())) -> active(c()),
   mat(f(x), f(y())) -> f(mat(x, y())),
      mat(f(x), c()) -> no(c()),
         tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
  EDG:
   {(active#(f(x)) -> f#(f(x)), f#(no(x)) -> f#(x))
    (active#(f(x)) -> f#(f(x)), f#(active(x)) -> active#(f(x)))
    (active#(f(x)) -> f#(f(x)), f#(active(x)) -> f#(x))
    (active#(f(x)) -> f#(f(x)), f#(mark(x)) -> f#(x))
    (tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> mat#(x, y()))
    (tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> f#(mat(x, y())))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(X()))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(X())))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(X()))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(X())))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(X()))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(X())))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))))
    (tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))))
    (f#(mark(x)) -> f#(x), f#(no(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(active(x)) -> active#(f(x)))
    (f#(mark(x)) -> f#(x), f#(active(x)) -> f#(x))
    (f#(mark(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (f#(no(x)) -> f#(x), f#(no(x)) -> f#(x))
    (f#(no(x)) -> f#(x), f#(active(x)) -> active#(f(x)))
    (f#(no(x)) -> f#(x), f#(active(x)) -> f#(x))
    (f#(no(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(c())) -> active#(c()))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(X()))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(X())))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(X()))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(X())))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(X()))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))))
    (tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(f(X()))))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(f(X())))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(f(X()))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(f(X())))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> f#(X()))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))
    (chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)), chk#(no(c())) -> active#(c()))
    (f#(active(x)) -> f#(x), f#(mark(x)) -> f#(x))
    (f#(active(x)) -> f#(x), f#(active(x)) -> f#(x))
    (f#(active(x)) -> f#(x), f#(active(x)) -> active#(f(x)))
    (f#(active(x)) -> f#(x), f#(no(x)) -> f#(x))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(mark(x)) -> f#(x))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(active(x)) -> f#(x))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(active(x)) -> active#(f(x)))
    (chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))), f#(no(x)) -> f#(x))
    (chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> f#(mat(x, y())))
    (chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))), x), mat#(f(x), f(y())) -> mat#(x, y()))
    (f#(active(x)) -> active#(f(x)), active#(f(x)) -> f#(f(x)))}
   SCCS:
    Scc:
     {tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
    Scc:
     {chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))}
    Scc:
     {  f#(mark(x)) -> f#(x),
      f#(active(x)) -> f#(x),
      f#(active(x)) -> active#(f(x)),
          f#(no(x)) -> f#(x),
      active#(f(x)) -> f#(f(x))}
    SCC:
     Strict:
      {tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     Weak:
     {       f(mark(x)) -> mark(f(x)),
           f(active(x)) -> active(f(x)),
               f(no(x)) -> no(f(x)),
           active(f(x)) -> mark(f(f(x))),
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
           chk(no(c())) -> active(c()),
      mat(f(x), f(y())) -> f(mat(x, y())),
         mat(f(x), c()) -> no(c()),
            tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 1
      Automaton:
       {
            tp#_1(59) -> 12*
            tp#_0(46) -> 12*
             tp_0(46) -> 32*
             tp_0(45) -> 32*
             tp_0(44) -> 32*
             tp_0(43) -> 32*
             tp_0(42) -> 32*
             tp_0(41) -> 32*
             tp_0(40) -> 32*
             tp_0(39) -> 32*
             tp_0(38) -> 32*
             tp_0(37) -> 32*
             tp_0(36) -> 32*
             tp_0(35) -> 32*
             tp_0(34) -> 32*
             tp_0(33) -> 32*
             tp_0(32) -> 32*
             tp_0(31) -> 32*
             tp_0(30) -> 32*
             tp_0(29) -> 32*
             tp_0(28) -> 32*
             tp_0(27) -> 32*
             tp_0(26) -> 32*
             tp_0(25) -> 32*
                c_0() -> 35*
                y_1() -> 60*
                y_0() -> 34*
             no_0(46) -> 31*
             no_0(45) -> 31*
             no_0(44) -> 31 | 27
             no_0(43) -> 31 | 27
             no_0(42) -> 31 | 27
             no_0(41) -> 31 | 27
             no_0(40) -> 31 | 27
             no_0(39) -> 31 | 27
             no_0(38) -> 31 | 27
             no_0(37) -> 31 | 27
             no_0(36) -> 31 | 27
             no_0(35) -> 45 | 31 | 25
             no_0(34) -> 31*
             no_0(33) -> 31*
             no_0(32) -> 31*
             no_0(31) -> 31*
             no_0(30) -> 31*
             no_0(29) -> 31*
             no_0(28) -> 31 | 27
             no_0(27) -> 45 | 31 | 27 | 25
             no_0(26) -> 31*
             no_0(25) -> 31*
                X_1() -> 47*
                X_0() -> 33*
        mat_1(57, 27) -> 58*
        mat_1(57, 25) -> 58*
        mat_1(56, 60) -> 61*
        mat_0(46, 46) -> 25*
        mat_0(46, 45) -> 25*
        mat_0(46, 44) -> 25*
        mat_0(46, 43) -> 25*
        mat_0(46, 42) -> 25*
        mat_0(46, 41) -> 25*
        mat_0(46, 40) -> 25*
        mat_0(46, 39) -> 25*
        mat_0(46, 38) -> 25*
        mat_0(46, 37) -> 25*
        mat_0(46, 36) -> 25*
        mat_0(46, 35) -> 25*
        mat_0(46, 34) -> 25*
        mat_0(46, 33) -> 25*
        mat_0(46, 32) -> 25*
        mat_0(46, 31) -> 25*
        mat_0(46, 30) -> 25*
        mat_0(46, 29) -> 25*
        mat_0(46, 28) -> 25*
        mat_0(46, 27) -> 25*
        mat_0(46, 26) -> 25*
        mat_0(46, 25) -> 25*
        mat_0(45, 46) -> 25*
        mat_0(45, 45) -> 25*
        mat_0(45, 44) -> 25*
        mat_0(45, 43) -> 25*
        mat_0(45, 42) -> 25*
        mat_0(45, 41) -> 25*
        mat_0(45, 40) -> 25*
        mat_0(45, 39) -> 25*
        mat_0(45, 38) -> 25*
        mat_0(45, 37) -> 25*
        mat_0(45, 36) -> 25*
        mat_0(45, 35) -> 25*
        mat_0(45, 34) -> 25*
        mat_0(45, 33) -> 25*
        mat_0(45, 32) -> 25*
        mat_0(45, 31) -> 25*
        mat_0(45, 30) -> 25*
        mat_0(45, 29) -> 25*
        mat_0(45, 28) -> 25*
        mat_0(45, 27) -> 25*
        mat_0(45, 26) -> 25*
        mat_0(45, 25) -> 25*
        mat_0(44, 46) -> 45*
        mat_0(44, 45) -> 45*
        mat_0(44, 44) -> 45*
        mat_0(44, 43) -> 45*
        mat_0(44, 42) -> 45*
        mat_0(44, 41) -> 45*
        mat_0(44, 40) -> 45*
        mat_0(44, 39) -> 45*
        mat_0(44, 38) -> 45*
        mat_0(44, 37) -> 45*
        mat_0(44, 36) -> 45*
        mat_0(44, 35) -> 45*
        mat_0(44, 34) -> 45*
        mat_0(44, 33) -> 45*
        mat_0(44, 32) -> 45*
        mat_0(44, 31) -> 45*
        mat_0(44, 30) -> 45*
        mat_0(44, 29) -> 45*
        mat_0(44, 28) -> 45*
        mat_0(44, 27) -> 45*
        mat_0(44, 26) -> 45*
        mat_0(44, 25) -> 45*
        mat_0(43, 46) -> 25*
        mat_0(43, 45) -> 25*
        mat_0(43, 44) -> 25*
        mat_0(43, 43) -> 25*
        mat_0(43, 42) -> 25*
        mat_0(43, 41) -> 25*
        mat_0(43, 40) -> 25*
        mat_0(43, 39) -> 25*
        mat_0(43, 38) -> 25*
        mat_0(43, 37) -> 25*
        mat_0(43, 36) -> 25*
        mat_0(43, 35) -> 25*
        mat_0(43, 34) -> 25*
        mat_0(43, 33) -> 25*
        mat_0(43, 32) -> 25*
        mat_0(43, 31) -> 25*
        mat_0(43, 30) -> 25*
        mat_0(43, 29) -> 25*
        mat_0(43, 28) -> 25*
        mat_0(43, 27) -> 25*
        mat_0(43, 26) -> 25*
        mat_0(43, 25) -> 25*
        mat_0(42, 46) -> 25*
        mat_0(42, 45) -> 25*
        mat_0(42, 44) -> 25*
        mat_0(42, 43) -> 25*
        mat_0(42, 42) -> 25*
        mat_0(42, 41) -> 25*
        mat_0(42, 40) -> 25*
        mat_0(42, 39) -> 25*
        mat_0(42, 38) -> 25*
        mat_0(42, 37) -> 25*
        mat_0(42, 36) -> 25*
        mat_0(42, 35) -> 25*
        mat_0(42, 34) -> 25*
        mat_0(42, 33) -> 25*
        mat_0(42, 32) -> 25*
        mat_0(42, 31) -> 25*
        mat_0(42, 30) -> 25*
        mat_0(42, 29) -> 25*
        mat_0(42, 28) -> 25*
        mat_0(42, 27) -> 25*
        mat_0(42, 26) -> 25*
        mat_0(42, 25) -> 25*
        mat_0(41, 46) -> 25*
        mat_0(41, 45) -> 25*
        mat_0(41, 44) -> 25*
        mat_0(41, 43) -> 25*
        mat_0(41, 42) -> 25*
        mat_0(41, 41) -> 25*
        mat_0(41, 40) -> 25*
        mat_0(41, 39) -> 25*
        mat_0(41, 38) -> 25*
        mat_0(41, 37) -> 25*
        mat_0(41, 36) -> 25*
        mat_0(41, 35) -> 25*
        mat_0(41, 34) -> 25*
        mat_0(41, 33) -> 25*
        mat_0(41, 32) -> 25*
        mat_0(41, 31) -> 25*
        mat_0(41, 30) -> 25*
        mat_0(41, 29) -> 25*
        mat_0(41, 28) -> 25*
        mat_0(41, 27) -> 25*
        mat_0(41, 26) -> 25*
        mat_0(41, 25) -> 25*
        mat_0(40, 46) -> 25*
        mat_0(40, 45) -> 25*
        mat_0(40, 44) -> 25*
        mat_0(40, 43) -> 25*
        mat_0(40, 42) -> 25*
        mat_0(40, 41) -> 25*
        mat_0(40, 40) -> 25*
        mat_0(40, 39) -> 25*
        mat_0(40, 38) -> 25*
        mat_0(40, 37) -> 25*
        mat_0(40, 36) -> 25*
        mat_0(40, 35) -> 25*
        mat_0(40, 34) -> 25*
        mat_0(40, 33) -> 25*
        mat_0(40, 32) -> 25*
        mat_0(40, 31) -> 25*
        mat_0(40, 30) -> 25*
        mat_0(40, 29) -> 25*
        mat_0(40, 28) -> 25*
        mat_0(40, 27) -> 25*
        mat_0(40, 26) -> 25*
        mat_0(40, 25) -> 25*
        mat_0(39, 46) -> 25*
        mat_0(39, 45) -> 25*
        mat_0(39, 44) -> 25*
        mat_0(39, 43) -> 25*
        mat_0(39, 42) -> 25*
        mat_0(39, 41) -> 25*
        mat_0(39, 40) -> 25*
        mat_0(39, 39) -> 25*
        mat_0(39, 38) -> 25*
        mat_0(39, 37) -> 25*
        mat_0(39, 36) -> 25*
        mat_0(39, 35) -> 25*
        mat_0(39, 34) -> 25*
        mat_0(39, 33) -> 25*
        mat_0(39, 32) -> 25*
        mat_0(39, 31) -> 25*
        mat_0(39, 30) -> 25*
        mat_0(39, 29) -> 25*
        mat_0(39, 28) -> 25*
        mat_0(39, 27) -> 25*
        mat_0(39, 26) -> 25*
        mat_0(39, 25) -> 25*
        mat_0(38, 46) -> 25*
        mat_0(38, 45) -> 25*
        mat_0(38, 44) -> 25*
        mat_0(38, 43) -> 25*
        mat_0(38, 42) -> 25*
        mat_0(38, 41) -> 25*
        mat_0(38, 40) -> 25*
        mat_0(38, 39) -> 25*
        mat_0(38, 38) -> 25*
        mat_0(38, 37) -> 25*
        mat_0(38, 36) -> 25*
        mat_0(38, 35) -> 25*
        mat_0(38, 34) -> 25*
        mat_0(38, 33) -> 25*
        mat_0(38, 32) -> 25*
        mat_0(38, 31) -> 25*
        mat_0(38, 30) -> 25*
        mat_0(38, 29) -> 25*
        mat_0(38, 28) -> 25*
        mat_0(38, 27) -> 25*
        mat_0(38, 26) -> 25*
        mat_0(38, 25) -> 25*
        mat_0(37, 46) -> 25*
        mat_0(37, 45) -> 25*
        mat_0(37, 44) -> 25*
        mat_0(37, 43) -> 25*
        mat_0(37, 42) -> 25*
        mat_0(37, 41) -> 25*
        mat_0(37, 40) -> 25*
        mat_0(37, 39) -> 25*
        mat_0(37, 38) -> 25*
        mat_0(37, 37) -> 25*
        mat_0(37, 36) -> 25*
        mat_0(37, 35) -> 25*
        mat_0(37, 34) -> 25*
        mat_0(37, 33) -> 25*
        mat_0(37, 32) -> 25*
        mat_0(37, 31) -> 25*
        mat_0(37, 30) -> 25*
        mat_0(37, 29) -> 25*
        mat_0(37, 28) -> 25*
        mat_0(37, 27) -> 25*
        mat_0(37, 26) -> 25*
        mat_0(37, 25) -> 25*
        mat_0(36, 46) -> 25*
        mat_0(36, 45) -> 25*
        mat_0(36, 44) -> 25*
        mat_0(36, 43) -> 25*
        mat_0(36, 42) -> 25*
        mat_0(36, 41) -> 25*
        mat_0(36, 40) -> 25*
        mat_0(36, 39) -> 25*
        mat_0(36, 38) -> 25*
        mat_0(36, 37) -> 25*
        mat_0(36, 36) -> 25*
        mat_0(36, 35) -> 25*
        mat_0(36, 34) -> 25*
        mat_0(36, 33) -> 25*
        mat_0(36, 32) -> 25*
        mat_0(36, 31) -> 25*
        mat_0(36, 30) -> 25*
        mat_0(36, 29) -> 25*
        mat_0(36, 28) -> 25*
        mat_0(36, 27) -> 25*
        mat_0(36, 26) -> 25*
        mat_0(36, 25) -> 25*
        mat_0(35, 46) -> 25*
        mat_0(35, 45) -> 25*
        mat_0(35, 44) -> 25*
        mat_0(35, 43) -> 25*
        mat_0(35, 42) -> 25*
        mat_0(35, 41) -> 25*
        mat_0(35, 40) -> 25*
        mat_0(35, 39) -> 25*
        mat_0(35, 38) -> 25*
        mat_0(35, 37) -> 25*
        mat_0(35, 36) -> 25*
        mat_0(35, 35) -> 25*
        mat_0(35, 34) -> 25*
        mat_0(35, 33) -> 25*
        mat_0(35, 32) -> 25*
        mat_0(35, 31) -> 25*
        mat_0(35, 30) -> 25*
        mat_0(35, 29) -> 25*
        mat_0(35, 28) -> 25*
        mat_0(35, 27) -> 25*
        mat_0(35, 26) -> 25*
        mat_0(35, 25) -> 25*
        mat_0(34, 46) -> 25*
        mat_0(34, 45) -> 25*
        mat_0(34, 44) -> 25*
        mat_0(34, 43) -> 25*
        mat_0(34, 42) -> 25*
        mat_0(34, 41) -> 25*
        mat_0(34, 40) -> 25*
        mat_0(34, 39) -> 25*
        mat_0(34, 38) -> 25*
        mat_0(34, 37) -> 25*
        mat_0(34, 36) -> 25*
        mat_0(34, 35) -> 25*
        mat_0(34, 34) -> 25*
        mat_0(34, 33) -> 25*
        mat_0(34, 32) -> 25*
        mat_0(34, 31) -> 25*
        mat_0(34, 30) -> 25*
        mat_0(34, 29) -> 25*
        mat_0(34, 28) -> 25*
        mat_0(34, 27) -> 25*
        mat_0(34, 26) -> 25*
        mat_0(34, 25) -> 25*
        mat_0(33, 46) -> 25*
        mat_0(33, 45) -> 25*
        mat_0(33, 44) -> 25*
        mat_0(33, 43) -> 25*
        mat_0(33, 42) -> 25*
        mat_0(33, 41) -> 25*
        mat_0(33, 40) -> 25*
        mat_0(33, 39) -> 25*
        mat_0(33, 38) -> 25*
        mat_0(33, 37) -> 25*
        mat_0(33, 36) -> 25*
        mat_0(33, 35) -> 25*
        mat_0(33, 34) -> 25*
        mat_0(33, 33) -> 25*
        mat_0(33, 32) -> 25*
        mat_0(33, 31) -> 25*
        mat_0(33, 30) -> 25*
        mat_0(33, 29) -> 25*
        mat_0(33, 28) -> 25*
        mat_0(33, 27) -> 25*
        mat_0(33, 26) -> 25*
        mat_0(33, 25) -> 25*
        mat_0(32, 46) -> 25*
        mat_0(32, 45) -> 25*
        mat_0(32, 44) -> 25*
        mat_0(32, 43) -> 25*
        mat_0(32, 42) -> 25*
        mat_0(32, 41) -> 25*
        mat_0(32, 40) -> 25*
        mat_0(32, 39) -> 25*
        mat_0(32, 38) -> 25*
        mat_0(32, 37) -> 25*
        mat_0(32, 36) -> 25*
        mat_0(32, 35) -> 25*
        mat_0(32, 34) -> 25*
        mat_0(32, 33) -> 25*
        mat_0(32, 32) -> 25*
        mat_0(32, 31) -> 25*
        mat_0(32, 30) -> 25*
        mat_0(32, 29) -> 25*
        mat_0(32, 28) -> 25*
        mat_0(32, 27) -> 25*
        mat_0(32, 26) -> 25*
        mat_0(32, 25) -> 25*
        mat_0(31, 46) -> 25*
        mat_0(31, 45) -> 25*
        mat_0(31, 44) -> 25*
        mat_0(31, 43) -> 25*
        mat_0(31, 42) -> 25*
        mat_0(31, 41) -> 25*
        mat_0(31, 40) -> 25*
        mat_0(31, 39) -> 25*
        mat_0(31, 38) -> 25*
        mat_0(31, 37) -> 25*
        mat_0(31, 36) -> 25*
        mat_0(31, 35) -> 25*
        mat_0(31, 34) -> 25*
        mat_0(31, 33) -> 25*
        mat_0(31, 32) -> 25*
        mat_0(31, 31) -> 25*
        mat_0(31, 30) -> 25*
        mat_0(31, 29) -> 25*
        mat_0(31, 28) -> 25*
        mat_0(31, 27) -> 25*
        mat_0(31, 26) -> 25*
        mat_0(31, 25) -> 25*
        mat_0(30, 46) -> 25*
        mat_0(30, 45) -> 25*
        mat_0(30, 44) -> 25*
        mat_0(30, 43) -> 25*
        mat_0(30, 42) -> 25*
        mat_0(30, 41) -> 25*
        mat_0(30, 40) -> 25*
        mat_0(30, 39) -> 25*
        mat_0(30, 38) -> 25*
        mat_0(30, 37) -> 25*
        mat_0(30, 36) -> 25*
        mat_0(30, 35) -> 25*
        mat_0(30, 34) -> 25*
        mat_0(30, 33) -> 25*
        mat_0(30, 32) -> 25*
        mat_0(30, 31) -> 25*
        mat_0(30, 30) -> 25*
        mat_0(30, 29) -> 25*
        mat_0(30, 28) -> 25*
        mat_0(30, 27) -> 25*
        mat_0(30, 26) -> 25*
        mat_0(30, 25) -> 25*
        mat_0(29, 46) -> 25*
        mat_0(29, 45) -> 25*
        mat_0(29, 44) -> 25*
        mat_0(29, 43) -> 25*
        mat_0(29, 42) -> 25*
        mat_0(29, 41) -> 25*
        mat_0(29, 40) -> 25*
        mat_0(29, 39) -> 25*
        mat_0(29, 38) -> 25*
        mat_0(29, 37) -> 25*
        mat_0(29, 36) -> 25*
        mat_0(29, 35) -> 25*
        mat_0(29, 34) -> 25*
        mat_0(29, 33) -> 25*
        mat_0(29, 32) -> 25*
        mat_0(29, 31) -> 25*
        mat_0(29, 30) -> 25*
        mat_0(29, 29) -> 25*
        mat_0(29, 28) -> 25*
        mat_0(29, 27) -> 25*
        mat_0(29, 26) -> 25*
        mat_0(29, 25) -> 25*
        mat_0(28, 46) -> 25*
        mat_0(28, 45) -> 25*
        mat_0(28, 44) -> 25*
        mat_0(28, 43) -> 25*
        mat_0(28, 42) -> 25*
        mat_0(28, 41) -> 25*
        mat_0(28, 40) -> 25*
        mat_0(28, 39) -> 25*
        mat_0(28, 38) -> 25*
        mat_0(28, 37) -> 25*
        mat_0(28, 36) -> 25*
        mat_0(28, 35) -> 25*
        mat_0(28, 34) -> 25*
        mat_0(28, 33) -> 25*
        mat_0(28, 32) -> 25*
        mat_0(28, 31) -> 25*
        mat_0(28, 30) -> 25*
        mat_0(28, 29) -> 25*
        mat_0(28, 28) -> 25*
        mat_0(28, 27) -> 25*
        mat_0(28, 26) -> 25*
        mat_0(28, 25) -> 25*
        mat_0(27, 46) -> 25*
        mat_0(27, 45) -> 25*
        mat_0(27, 44) -> 25*
        mat_0(27, 43) -> 25*
        mat_0(27, 42) -> 25*
        mat_0(27, 41) -> 25*
        mat_0(27, 40) -> 25*
        mat_0(27, 39) -> 25*
        mat_0(27, 38) -> 25*
        mat_0(27, 37) -> 25*
        mat_0(27, 36) -> 25*
        mat_0(27, 35) -> 25*
        mat_0(27, 34) -> 25*
        mat_0(27, 33) -> 25*
        mat_0(27, 32) -> 25*
        mat_0(27, 31) -> 25*
        mat_0(27, 30) -> 25*
        mat_0(27, 29) -> 25*
        mat_0(27, 28) -> 25*
        mat_0(27, 27) -> 25*
        mat_0(27, 26) -> 25*
        mat_0(27, 25) -> 25*
        mat_0(26, 46) -> 25*
        mat_0(26, 45) -> 25*
        mat_0(26, 44) -> 25*
        mat_0(26, 43) -> 25*
        mat_0(26, 42) -> 25*
        mat_0(26, 41) -> 25*
        mat_0(26, 40) -> 25*
        mat_0(26, 39) -> 25*
        mat_0(26, 38) -> 25*
        mat_0(26, 37) -> 25*
        mat_0(26, 36) -> 25*
        mat_0(26, 35) -> 25*
        mat_0(26, 34) -> 25*
        mat_0(26, 33) -> 25*
        mat_0(26, 32) -> 25*
        mat_0(26, 31) -> 25*
        mat_0(26, 30) -> 25*
        mat_0(26, 29) -> 25*
        mat_0(26, 28) -> 25*
        mat_0(26, 27) -> 25*
        mat_0(26, 26) -> 25*
        mat_0(26, 25) -> 25*
        mat_0(25, 46) -> 25*
        mat_0(25, 45) -> 25*
        mat_0(25, 44) -> 25*
        mat_0(25, 43) -> 25*
        mat_0(25, 42) -> 25*
        mat_0(25, 41) -> 25*
        mat_0(25, 40) -> 25*
        mat_0(25, 39) -> 25*
        mat_0(25, 38) -> 25*
        mat_0(25, 37) -> 25*
        mat_0(25, 36) -> 25*
        mat_0(25, 35) -> 25*
        mat_0(25, 34) -> 25*
        mat_0(25, 33) -> 25*
        mat_0(25, 32) -> 25*
        mat_0(25, 31) -> 25*
        mat_0(25, 30) -> 25*
        mat_0(25, 29) -> 25*
        mat_0(25, 28) -> 25*
        mat_0(25, 27) -> 25*
        mat_0(25, 26) -> 25*
        mat_0(25, 25) -> 25*
            chk_1(58) -> 59*
            chk_0(46) -> 30*
            chk_0(45) -> 46*
            chk_0(44) -> 30*
            chk_0(43) -> 30*
            chk_0(42) -> 30*
            chk_0(41) -> 30*
            chk_0(40) -> 30*
            chk_0(39) -> 30*
            chk_0(38) -> 30*
            chk_0(37) -> 30*
            chk_0(36) -> 30*
            chk_0(35) -> 30*
            chk_0(34) -> 30*
            chk_0(33) -> 30*
            chk_0(32) -> 30*
            chk_0(31) -> 30*
            chk_0(30) -> 30*
            chk_0(29) -> 30*
            chk_0(28) -> 30*
            chk_0(27) -> 30*
            chk_0(26) -> 30*
            chk_0(25) -> 30*
         active_0(46) -> 29*
         active_0(45) -> 29*
         active_0(44) -> 29 | 27
         active_0(43) -> 29 | 27
         active_0(42) -> 29 | 27
         active_0(41) -> 29 | 27
         active_0(40) -> 29 | 27
         active_0(39) -> 29 | 27
         active_0(38) -> 29 | 27
         active_0(37) -> 29 | 27
         active_0(36) -> 29 | 27
         active_0(35) -> 46 | 30 | 29
         active_0(34) -> 29*
         active_0(33) -> 29*
         active_0(32) -> 29*
         active_0(31) -> 29*
         active_0(30) -> 29*
         active_0(29) -> 29*
         active_0(28) -> 29 | 27
         active_0(27) -> 46 | 30 | 29 | 27
         active_0(26) -> 29*
         active_0(25) -> 29*
              f_1(61) -> 58*
              f_1(56) -> 57*
              f_1(55) -> 56*
              f_1(54) -> 55*
              f_1(53) -> 54*
              f_1(52) -> 53*
              f_1(51) -> 52*
              f_1(50) -> 51*
              f_1(49) -> 50*
              f_1(48) -> 49*
              f_1(47) -> 48*
              f_0(46) -> 46 | 30 | 27
              f_0(45) -> 27 | 25
              f_0(44) -> 27*
              f_0(43) -> 44*
              f_0(42) -> 43*
              f_0(41) -> 42*
              f_0(40) -> 41*
              f_0(39) -> 40*
              f_0(38) -> 39*
              f_0(37) -> 38*
              f_0(36) -> 37*
              f_0(35) -> 27*
              f_0(34) -> 27*
              f_0(33) -> 28*
              f_0(32) -> 27*
              f_0(31) -> 27*
              f_0(30) -> 27*
              f_0(29) -> 27*
              f_0(28) -> 36*
              f_0(27) -> 27*
              f_0(26) -> 27*
              f_0(25) -> 45 | 27 | 25
           mark_0(46) -> 26*
           mark_0(45) -> 26*
           mark_0(44) -> 29 | 27 | 26
           mark_0(43) -> 29 | 27 | 26
           mark_0(42) -> 29 | 27 | 26
           mark_0(41) -> 29 | 27 | 26
           mark_0(40) -> 29 | 27 | 26
           mark_0(39) -> 29 | 27 | 26
           mark_0(38) -> 29 | 27 | 26
           mark_0(37) -> 29 | 27 | 26
           mark_0(36) -> 29 | 27 | 26
           mark_0(35) -> 26*
           mark_0(34) -> 26*
           mark_0(33) -> 26*
           mark_0(32) -> 26*
           mark_0(31) -> 26*
           mark_0(30) -> 26*
           mark_0(29) -> 26*
           mark_0(28) -> 27 | 26
           mark_0(27) -> 46 | 30 | 29 | 27 | 26
           mark_0(26) -> 26*
           mark_0(25) -> 46 | 30 | 26
       }
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))}
     Weak:
     {       f(mark(x)) -> mark(f(x)),
           f(active(x)) -> active(f(x)),
               f(no(x)) -> no(f(x)),
           active(f(x)) -> mark(f(f(x))),
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
           chk(no(c())) -> active(c()),
      mat(f(x), f(y())) -> f(mat(x, y())),
         mat(f(x), c()) -> no(c()),
            tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     POLY:
      Argument Filtering:
       pi(tp) = [], pi(c) = [], pi(y) = [], pi(no) = 0, pi(X) = [], pi(mat) = 1, pi(chk#) = 0, pi(chk) = [], pi(active) = [], pi(f) = [0], pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [f](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {       f(mark(x)) -> mark(f(x)),
             f(active(x)) -> active(f(x)),
                 f(no(x)) -> no(f(x)),
             active(f(x)) -> mark(f(f(x))),
            chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
             chk(no(c())) -> active(c()),
        mat(f(x), f(y())) -> f(mat(x, y())),
           mat(f(x), c()) -> no(c()),
              tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
      Qed
    SCC:
     Strict:
      {  f#(mark(x)) -> f#(x),
       f#(active(x)) -> f#(x),
       f#(active(x)) -> active#(f(x)),
           f#(no(x)) -> f#(x),
       active#(f(x)) -> f#(f(x))}
     Weak:
     {       f(mark(x)) -> mark(f(x)),
           f(active(x)) -> active(f(x)),
               f(no(x)) -> no(f(x)),
           active(f(x)) -> mark(f(f(x))),
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
           chk(no(c())) -> active(c()),
      mat(f(x), f(y())) -> f(mat(x, y())),
         mat(f(x), c()) -> no(c()),
            tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
     POLY:
      Argument Filtering:
       pi(tp) = [], pi(c) = [], pi(y) = [], pi(no) = [0], pi(X) = [], pi(mat) = [], pi(chk) = [], pi(active#) = [0], pi(active) = [0], pi(f#) = [0], pi(f) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [active#](x0) = x0 + 1,
       [f#](x0) = x0 + 1,
       [no](x0) = x0 + 1,
       [active](x0) = x0 + 1
      Strict:
       {  f#(mark(x)) -> f#(x),
        active#(f(x)) -> f#(f(x))}
      Weak:
       {       f(mark(x)) -> mark(f(x)),
             f(active(x)) -> active(f(x)),
                 f(no(x)) -> no(f(x)),
             active(f(x)) -> mark(f(f(x))),
            chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
             chk(no(c())) -> active(c()),
        mat(f(x), f(y())) -> f(mat(x, y())),
           mat(f(x), c()) -> no(c()),
              tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
      EDG:
       {(active#(f(x)) -> f#(f(x)), f#(mark(x)) -> f#(x))
        (f#(mark(x)) -> f#(x), f#(mark(x)) -> f#(x))}
       SCCS:
        Scc:
         {f#(mark(x)) -> f#(x)}
        SCC:
         Strict:
          {f#(mark(x)) -> f#(x)}
         Weak:
         {       f(mark(x)) -> mark(f(x)),
               f(active(x)) -> active(f(x)),
                   f(no(x)) -> no(f(x)),
               active(f(x)) -> mark(f(f(x))),
              chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
               chk(no(c())) -> active(c()),
          mat(f(x), f(y())) -> f(mat(x, y())),
             mat(f(x), c()) -> no(c()),
                tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed