MAYBE
TRS:
 {             a__p(X) -> p(X),
             a__p(0()) -> 0(),
            a__p(s(X)) -> mark(X),
             mark(0()) -> 0(),
            mark(s(X)) -> s(mark(X)),
          mark(true()) -> true(),
         mark(false()) -> false(),
    mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)),
            mark(p(X)) -> a__p(mark(X)),
     mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)),
  mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
        a__leq(X1, X2) -> leq(X1, X2),
        a__leq(0(), Y) -> true(),
     a__leq(s(X), 0()) -> false(),
    a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)),
     a__if(X1, X2, X3) -> if(X1, X2, X3),
   a__if(true(), X, Y) -> mark(X),
  a__if(false(), X, Y) -> mark(Y),
         a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))),
       a__diff(X1, X2) -> diff(X1, X2)}
 DP:
  Strict:
   {          a__p#(s(X)) -> mark#(X),
              mark#(s(X)) -> mark#(X),
      mark#(diff(X1, X2)) -> mark#(X1),
      mark#(diff(X1, X2)) -> mark#(X2),
      mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)),
              mark#(p(X)) -> a__p#(mark(X)),
              mark#(p(X)) -> mark#(X),
       mark#(leq(X1, X2)) -> mark#(X1),
       mark#(leq(X1, X2)) -> mark#(X2),
       mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)),
    mark#(if(X1, X2, X3)) -> mark#(X1),
    mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
      a__leq#(s(X), s(Y)) -> mark#(X),
      a__leq#(s(X), s(Y)) -> mark#(Y),
      a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)),
     a__if#(true(), X, Y) -> mark#(X),
    a__if#(false(), X, Y) -> mark#(Y),
           a__diff#(X, Y) -> mark#(X),
           a__diff#(X, Y) -> mark#(Y),
           a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)),
           a__diff#(X, Y) -> a__if#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y)))}
  Weak:
  {             a__p(X) -> p(X),
              a__p(0()) -> 0(),
             a__p(s(X)) -> mark(X),
              mark(0()) -> 0(),
             mark(s(X)) -> s(mark(X)),
           mark(true()) -> true(),
          mark(false()) -> false(),
     mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)),
             mark(p(X)) -> a__p(mark(X)),
      mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)),
   mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
         a__leq(X1, X2) -> leq(X1, X2),
         a__leq(0(), Y) -> true(),
      a__leq(s(X), 0()) -> false(),
     a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)),
      a__if(X1, X2, X3) -> if(X1, X2, X3),
    a__if(true(), X, Y) -> mark(X),
   a__if(false(), X, Y) -> mark(Y),
          a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))),
        a__diff(X1, X2) -> diff(X1, X2)}
  EDG:
   {
    (mark#(p(X)) -> a__p#(mark(X)), a__p#(s(X)) -> mark#(X))
    (mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)), a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)))
    (mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)), a__leq#(s(X), s(Y)) -> mark#(Y))
    (mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)), a__leq#(s(X), s(Y)) -> mark#(X))
    (a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)), a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)))
    (a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)), a__leq#(s(X), s(Y)) -> mark#(Y))
    (a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)), a__leq#(s(X), s(Y)) -> mark#(X))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(leq(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(leq(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X2))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X1))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(p(X)) -> mark#(X))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(p(X)) -> a__p#(mark(X)))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X2))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X1))
    (a__leq#(s(X), s(Y)) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__diff#(X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__diff#(X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__diff#(X, Y) -> mark#(Y), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__diff#(X, Y) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X2))
    (a__diff#(X, Y) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X1))
    (a__diff#(X, Y) -> mark#(Y), mark#(p(X)) -> mark#(X))
    (a__diff#(X, Y) -> mark#(Y), mark#(p(X)) -> a__p#(mark(X)))
    (a__diff#(X, Y) -> mark#(Y), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__diff#(X, Y) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X2))
    (a__diff#(X, Y) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X1))
    (a__diff#(X, Y) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1))
    (a__leq#(s(X), s(Y)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__diff#(X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__diff#(X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__diff#(X, Y) -> mark#(X), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__diff#(X, Y) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2))
    (a__diff#(X, Y) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1))
    (a__diff#(X, Y) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__diff#(X, Y) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__diff#(X, Y) -> mark#(X), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__diff#(X, Y) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2))
    (a__diff#(X, Y) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1))
    (a__diff#(X, Y) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3), a__if#(true(), X, Y) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3), a__if#(false(), X, Y) -> mark#(Y))
    (a__if#(true(), X, Y) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__p#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2))
    (a__p#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2))
    (a__p#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__p#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(p(X)) -> a__p#(mark(X)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(p(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X1))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X2))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X1))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X2))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)), a__leq#(s(X), s(Y)) -> mark#(X))
    (a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)), a__leq#(s(X), s(Y)) -> mark#(Y))
    (a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)), a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)))
    (mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)), a__diff#(X, Y) -> mark#(X))
    (mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)), a__diff#(X, Y) -> mark#(Y))
    (mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)), a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)))
    (mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)), a__diff#(X, Y) -> a__if#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))))
    (a__diff#(X, Y) -> a__if#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__if#(true(), X, Y) -> mark#(X))
    (a__diff#(X, Y) -> a__if#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__if#(false(), X, Y) -> mark#(Y))
   }
   SCCS:
    Scc:
     {          a__p#(s(X)) -> mark#(X),
                mark#(s(X)) -> mark#(X),
        mark#(diff(X1, X2)) -> mark#(X1),
        mark#(diff(X1, X2)) -> mark#(X2),
        mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)),
                mark#(p(X)) -> a__p#(mark(X)),
                mark#(p(X)) -> mark#(X),
         mark#(leq(X1, X2)) -> mark#(X1),
         mark#(leq(X1, X2)) -> mark#(X2),
         mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)),
      mark#(if(X1, X2, X3)) -> mark#(X1),
      mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
        a__leq#(s(X), s(Y)) -> mark#(X),
        a__leq#(s(X), s(Y)) -> mark#(Y),
        a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)),
       a__if#(true(), X, Y) -> mark#(X),
      a__if#(false(), X, Y) -> mark#(Y),
             a__diff#(X, Y) -> mark#(X),
             a__diff#(X, Y) -> mark#(Y),
             a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)),
             a__diff#(X, Y) -> a__if#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y)))}
    SCC:
     Strict:
      {          a__p#(s(X)) -> mark#(X),
                 mark#(s(X)) -> mark#(X),
         mark#(diff(X1, X2)) -> mark#(X1),
         mark#(diff(X1, X2)) -> mark#(X2),
         mark#(diff(X1, X2)) -> a__diff#(mark(X1), mark(X2)),
                 mark#(p(X)) -> a__p#(mark(X)),
                 mark#(p(X)) -> mark#(X),
          mark#(leq(X1, X2)) -> mark#(X1),
          mark#(leq(X1, X2)) -> mark#(X2),
          mark#(leq(X1, X2)) -> a__leq#(mark(X1), mark(X2)),
       mark#(if(X1, X2, X3)) -> mark#(X1),
       mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
         a__leq#(s(X), s(Y)) -> mark#(X),
         a__leq#(s(X), s(Y)) -> mark#(Y),
         a__leq#(s(X), s(Y)) -> a__leq#(mark(X), mark(Y)),
        a__if#(true(), X, Y) -> mark#(X),
       a__if#(false(), X, Y) -> mark#(Y),
              a__diff#(X, Y) -> mark#(X),
              a__diff#(X, Y) -> mark#(Y),
              a__diff#(X, Y) -> a__leq#(mark(X), mark(Y)),
              a__diff#(X, Y) -> a__if#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y)))}
     Weak:
     {             a__p(X) -> p(X),
                 a__p(0()) -> 0(),
                a__p(s(X)) -> mark(X),
                 mark(0()) -> 0(),
                mark(s(X)) -> s(mark(X)),
              mark(true()) -> true(),
             mark(false()) -> false(),
        mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)),
                mark(p(X)) -> a__p(mark(X)),
         mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)),
      mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
            a__leq(X1, X2) -> leq(X1, X2),
            a__leq(0(), Y) -> true(),
         a__leq(s(X), 0()) -> false(),
        a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)),
         a__if(X1, X2, X3) -> if(X1, X2, X3),
       a__if(true(), X, Y) -> mark(X),
      a__if(false(), X, Y) -> mark(Y),
             a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))),
           a__diff(X1, X2) -> diff(X1, X2)}
     Fail