MAYBE
TRS:
 {   a__if(X1, X2, X3) -> if(X1, X2, X3),
   a__if(true(), X, Y) -> mark(X),
  a__if(false(), X, Y) -> mark(Y),
            a__zero(X) -> zero(X),
         a__zero(s(X)) -> false(),
          a__zero(0()) -> true(),
            mark(s(X)) -> s(mark(X)),
             mark(0()) -> 0(),
    mark(prod(X1, X2)) -> a__prod(mark(X1), mark(X2)),
         mark(fact(X)) -> a__fact(mark(X)),
            mark(p(X)) -> a__p(mark(X)),
          mark(true()) -> true(),
         mark(false()) -> false(),
  mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
         mark(zero(X)) -> a__zero(mark(X)),
     mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
            a__fact(X) -> a__if(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))),
            a__fact(X) -> fact(X),
        a__add(X1, X2) -> add(X1, X2),
       a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))),
        a__add(0(), X) -> mark(X),
       a__prod(X1, X2) -> prod(X1, X2),
      a__prod(s(X), Y) -> a__add(mark(Y), a__prod(mark(X), mark(Y))),
       a__prod(0(), X) -> 0(),
               a__p(X) -> p(X),
            a__p(s(X)) -> mark(X)}
 DP:
  Strict:
   { a__if#(true(), X, Y) -> mark#(X),
    a__if#(false(), X, Y) -> mark#(Y),
              mark#(s(X)) -> mark#(X),
      mark#(prod(X1, X2)) -> mark#(X1),
      mark#(prod(X1, X2)) -> mark#(X2),
      mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)),
           mark#(fact(X)) -> mark#(X),
           mark#(fact(X)) -> a__fact#(mark(X)),
              mark#(p(X)) -> mark#(X),
              mark#(p(X)) -> a__p#(mark(X)),
    mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
    mark#(if(X1, X2, X3)) -> mark#(X1),
           mark#(zero(X)) -> a__zero#(mark(X)),
           mark#(zero(X)) -> mark#(X),
       mark#(add(X1, X2)) -> mark#(X1),
       mark#(add(X1, X2)) -> mark#(X2),
       mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
              a__fact#(X) -> a__if#(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))),
              a__fact#(X) -> a__zero#(mark(X)),
              a__fact#(X) -> mark#(X),
         a__add#(s(X), Y) -> mark#(X),
         a__add#(s(X), Y) -> mark#(Y),
         a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)),
          a__add#(0(), X) -> mark#(X),
        a__prod#(s(X), Y) -> mark#(X),
        a__prod#(s(X), Y) -> mark#(Y),
        a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))),
        a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)),
              a__p#(s(X)) -> mark#(X)}
  Weak:
  {   a__if(X1, X2, X3) -> if(X1, X2, X3),
    a__if(true(), X, Y) -> mark(X),
   a__if(false(), X, Y) -> mark(Y),
             a__zero(X) -> zero(X),
          a__zero(s(X)) -> false(),
           a__zero(0()) -> true(),
             mark(s(X)) -> s(mark(X)),
              mark(0()) -> 0(),
     mark(prod(X1, X2)) -> a__prod(mark(X1), mark(X2)),
          mark(fact(X)) -> a__fact(mark(X)),
             mark(p(X)) -> a__p(mark(X)),
           mark(true()) -> true(),
          mark(false()) -> false(),
   mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
          mark(zero(X)) -> a__zero(mark(X)),
      mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
             a__fact(X) -> a__if(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))),
             a__fact(X) -> fact(X),
         a__add(X1, X2) -> add(X1, X2),
        a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))),
         a__add(0(), X) -> mark(X),
        a__prod(X1, X2) -> prod(X1, X2),
       a__prod(s(X), Y) -> a__add(mark(Y), a__prod(mark(X), mark(Y))),
        a__prod(0(), X) -> 0(),
                a__p(X) -> p(X),
             a__p(s(X)) -> mark(X)}
  EDG:
   {
    (a__add#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(Y), mark#(zero(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__add#(s(X), Y) -> mark#(Y), mark#(p(X)) -> a__p#(mark(X)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(p(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(fact(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(Y), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(Y), mark#(prod(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(Y), mark#(prod(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (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))
    (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#(fact(X)) -> a__fact#(mark(X)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(fact(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(fact(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(fact(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(fact(X)) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (mark#(fact(X)) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(fact(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(fact(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(fact(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(fact(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(fact(X)) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(fact(X)) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (mark#(fact(X)) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(fact(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(fact(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(fact(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(zero(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(zero(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(zero(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(zero(X)) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (mark#(zero(X)) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(zero(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(zero(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(zero(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(zero(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(zero(X)) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(zero(X)) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (mark#(zero(X)) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(zero(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(zero(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(zero(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__add#(s(X), Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__add#(s(X), Y) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__add#(s(X), Y) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__add#(s(X), Y) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (a__add#(s(X), Y) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (a__add#(s(X), Y) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (a__add#(s(X), Y) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__prod#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__prod#(s(X), Y) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__prod#(s(X), Y) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__prod#(s(X), Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__prod#(s(X), Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__prod#(s(X), Y) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__prod#(s(X), Y) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__prod#(s(X), Y) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__prod#(s(X), Y) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (a__prod#(s(X), Y) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (a__prod#(s(X), Y) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))), a__add#(0(), X) -> mark#(X))
    (a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))), a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)))
    (a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))), a__add#(s(X), Y) -> mark#(Y))
    (a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))), a__add#(s(X), Y) -> mark#(X))
    (mark#(p(X)) -> a__p#(mark(X)), a__p#(s(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(s(X), Y) -> mark#(Y))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(s(X), Y) -> mark#(X))
    (a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)), a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)))
    (a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)), a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))))
    (a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)), a__prod#(s(X), Y) -> mark#(Y))
    (a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)), a__prod#(s(X), Y) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(zero(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fact(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(zero(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(fact(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(prod(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(zero(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fact(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (a__fact#(X) -> a__if#(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))), a__if#(true(), X, Y) -> mark#(X))
    (a__fact#(X) -> a__if#(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))), a__if#(false(), X, Y) -> mark#(Y))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(fact(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(zero(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (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))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(fact(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(zero(X)) -> mark#(X))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(prod(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(s(X), Y) -> mark#(X))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(s(X), Y) -> mark#(Y))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)))
    (a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)), a__add#(0(), X) -> mark#(X))
    (mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)), a__prod#(s(X), Y) -> mark#(X))
    (mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)), a__prod#(s(X), Y) -> mark#(Y))
    (mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)), a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))))
    (mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)), a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)))
    (mark#(fact(X)) -> a__fact#(mark(X)), a__fact#(X) -> a__if#(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))))
    (mark#(fact(X)) -> a__fact#(mark(X)), a__fact#(X) -> a__zero#(mark(X)))
    (mark#(fact(X)) -> a__fact#(mark(X)), a__fact#(X) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (a__p#(s(X)) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__p#(s(X)) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__p#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__p#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__p#(s(X)) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__p#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__add#(0(), X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__fact#(X) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__fact#(X) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (a__fact#(X) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (a__fact#(X) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__fact#(X) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (a__fact#(X) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__fact#(X) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__fact#(X) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__fact#(X) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__fact#(X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__fact#(X) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__fact#(X) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (a__fact#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__fact#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__fact#(X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(p(X)) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(p(X)) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(zero(X)) -> a__zero#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(p(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(prod(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(fact(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(fact(X)) -> a__fact#(mark(X)))
    (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#(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#(zero(X)) -> a__zero#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(zero(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(prod(X1, X2)) -> mark#(X1))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(prod(X1, X2)) -> mark#(X2))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(fact(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(p(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(p(X)) -> a__p#(mark(X)))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(zero(X)) -> mark#(X))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__prod#(s(X), Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(prod(X1, X2)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(prod(X1, X2)) -> mark#(X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(fact(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(fact(X)) -> a__fact#(mark(X)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(p(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(p(X)) -> a__p#(mark(X)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(zero(X)) -> a__zero#(mark(X)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(zero(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
   }
   SCCS:
    Scc:
     { a__if#(true(), X, Y) -> mark#(X),
      a__if#(false(), X, Y) -> mark#(Y),
                mark#(s(X)) -> mark#(X),
        mark#(prod(X1, X2)) -> mark#(X1),
        mark#(prod(X1, X2)) -> mark#(X2),
        mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)),
             mark#(fact(X)) -> mark#(X),
             mark#(fact(X)) -> a__fact#(mark(X)),
                mark#(p(X)) -> mark#(X),
                mark#(p(X)) -> a__p#(mark(X)),
      mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
      mark#(if(X1, X2, X3)) -> mark#(X1),
             mark#(zero(X)) -> mark#(X),
         mark#(add(X1, X2)) -> mark#(X1),
         mark#(add(X1, X2)) -> mark#(X2),
         mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                a__fact#(X) -> a__if#(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))),
                a__fact#(X) -> mark#(X),
           a__add#(s(X), Y) -> mark#(X),
           a__add#(s(X), Y) -> mark#(Y),
           a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)),
            a__add#(0(), X) -> mark#(X),
          a__prod#(s(X), Y) -> mark#(X),
          a__prod#(s(X), Y) -> mark#(Y),
          a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))),
          a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)),
                a__p#(s(X)) -> mark#(X)}
    SCC:
     Strict:
      { a__if#(true(), X, Y) -> mark#(X),
       a__if#(false(), X, Y) -> mark#(Y),
                 mark#(s(X)) -> mark#(X),
         mark#(prod(X1, X2)) -> mark#(X1),
         mark#(prod(X1, X2)) -> mark#(X2),
         mark#(prod(X1, X2)) -> a__prod#(mark(X1), mark(X2)),
              mark#(fact(X)) -> mark#(X),
              mark#(fact(X)) -> a__fact#(mark(X)),
                 mark#(p(X)) -> mark#(X),
                 mark#(p(X)) -> a__p#(mark(X)),
       mark#(if(X1, X2, X3)) -> a__if#(mark(X1), X2, X3),
       mark#(if(X1, X2, X3)) -> mark#(X1),
              mark#(zero(X)) -> mark#(X),
          mark#(add(X1, X2)) -> mark#(X1),
          mark#(add(X1, X2)) -> mark#(X2),
          mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                 a__fact#(X) -> a__if#(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))),
                 a__fact#(X) -> mark#(X),
            a__add#(s(X), Y) -> mark#(X),
            a__add#(s(X), Y) -> mark#(Y),
            a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)),
             a__add#(0(), X) -> mark#(X),
           a__prod#(s(X), Y) -> mark#(X),
           a__prod#(s(X), Y) -> mark#(Y),
           a__prod#(s(X), Y) -> a__add#(mark(Y), a__prod(mark(X), mark(Y))),
           a__prod#(s(X), Y) -> a__prod#(mark(X), mark(Y)),
                 a__p#(s(X)) -> mark#(X)}
     Weak:
     {   a__if(X1, X2, X3) -> if(X1, X2, X3),
       a__if(true(), X, Y) -> mark(X),
      a__if(false(), X, Y) -> mark(Y),
                a__zero(X) -> zero(X),
             a__zero(s(X)) -> false(),
              a__zero(0()) -> true(),
                mark(s(X)) -> s(mark(X)),
                 mark(0()) -> 0(),
        mark(prod(X1, X2)) -> a__prod(mark(X1), mark(X2)),
             mark(fact(X)) -> a__fact(mark(X)),
                mark(p(X)) -> a__p(mark(X)),
              mark(true()) -> true(),
             mark(false()) -> false(),
      mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3),
             mark(zero(X)) -> a__zero(mark(X)),
         mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                a__fact(X) -> a__if(a__zero(mark(X)), s(0()), prod(X, fact(p(X)))),
                a__fact(X) -> fact(X),
            a__add(X1, X2) -> add(X1, X2),
           a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))),
            a__add(0(), X) -> mark(X),
           a__prod(X1, X2) -> prod(X1, X2),
          a__prod(s(X), Y) -> a__add(mark(Y), a__prod(mark(X), mark(Y))),
           a__prod(0(), X) -> 0(),
                   a__p(X) -> p(X),
                a__p(s(X)) -> mark(X)}
     Fail