MAYBE
Time: 0.045916
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:
  DP:
   { 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}
  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}
  UR:
   {   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,
                 a(x, y) -> x,
                 a(x, y) -> y}
   EDG:
    {
     (mark# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# zero X -> mark# X)
     (mark# s X -> mark# X, mark# zero X -> a__zero# mark X)
     (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# p X -> a__p# mark X)
     (mark# s X -> mark# X, mark# p X -> mark# X)
     (mark# s X -> mark# X, mark# fact X -> a__fact# mark X)
     (mark# s X -> mark# X, mark# fact X -> mark# X)
     (mark# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# p X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# p X -> mark# X, mark# zero X -> mark# X)
     (mark# p X -> mark# X, mark# zero X -> a__zero# mark X)
     (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))
     (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# fact X -> a__fact# mark X)
     (mark# p X -> mark# X, mark# fact X -> mark# X)
     (mark# p X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# p X -> mark# X, mark# s X -> mark# X)
     (a__fact# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (a__fact# X -> mark# X, mark# zero X -> mark# X)
     (a__fact# X -> mark# X, mark# zero X -> a__zero# mark X)
     (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (a__fact# X -> mark# X, mark# p X -> a__p# mark X)
     (a__fact# X -> mark# X, mark# p X -> mark# X)
     (a__fact# X -> mark# X, mark# fact X -> a__fact# mark X)
     (a__fact# X -> mark# X, mark# fact X -> mark# X)
     (a__fact# X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (a__fact# X -> mark# X, mark# s X -> mark# X)
     (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
     (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
     (a__add#(0(), X) -> mark# X, mark# zero X -> mark# X)
     (a__add#(0(), X) -> mark# X, mark# zero X -> a__zero# mark X)
     (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (a__add#(0(), X) -> mark# X, mark# p X -> a__p# mark X)
     (a__add#(0(), X) -> mark# X, mark# p X -> mark# X)
     (a__add#(0(), X) -> mark# X, mark# fact X -> a__fact# mark X)
     (a__add#(0(), X) -> mark# X, mark# fact X -> mark# X)
     (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (a__add#(0(), X) -> mark# X, mark# s X -> mark# X)
     (a__p# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (a__p# s X -> mark# X, mark# zero X -> mark# X)
     (a__p# s X -> mark# X, mark# zero X -> a__zero# mark X)
     (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__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# fact X -> a__fact# mark X)
     (a__p# s X -> mark# X, mark# fact X -> mark# X)
     (a__p# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (a__p# s X -> mark# X, mark# s X -> 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# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)
     (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__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# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2)
     (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1)
     (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> a__zero# mark X)
     (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# 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# fact X -> a__fact# mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X)
     (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# prod(X1, X2) -> mark# X2)
     (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
     (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
     (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
     (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
     (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
     (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
     (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))
     (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# fact X -> a__fact# mark X)
     (a__if#(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
     (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# prod(X1, X2) -> mark# X2)
     (a__if#(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
     (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
     (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
     (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
     (a__prod#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
     (a__prod#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
     (a__prod#(s X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
     (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# p X -> a__p# mark X)
     (a__prod#(s X, Y) -> mark# Y, mark# p 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# fact X -> mark# X)
     (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# prod(X1, X2) -> mark# X2)
     (a__prod#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
     (a__prod#(s X, Y) -> mark# Y, 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)
     (a__add#(s X, Y) -> mark# Y, mark# s X -> mark# X)
     (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
     (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
     (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# fact 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# p X -> mark# X)
     (a__add#(s X, Y) -> mark# Y, mark# p X -> a__p# mark X)
     (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# if(X1, X2, X3) -> mark# X1)
     (a__add#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
     (a__add#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
     (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
     (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
     (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
     (mark# add(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
     (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
     (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
     (mark# prod(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
     (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
     (mark# prod(X1, X2) -> mark# X1, 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__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(s X, Y) -> mark# X)
     (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) -> a__add#(mark X, mark Y))
     (a__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(0(), X) -> mark# X)
     (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__prod#(s X, Y) -> mark# X, mark# s X -> mark# X)
     (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> 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# X, mark# fact 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# p X -> mark# X)
     (a__prod#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
     (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# if(X1, X2, X3) -> mark# X1)
     (a__prod#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
     (a__prod#(s X, Y) -> mark# X, mark# zero X -> mark# X)
     (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
     (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
     (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__add#(s X, Y) -> mark# X, mark# s X -> mark# X)
     (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (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# fact 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# p X -> mark# X)
     (a__add#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
     (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# if(X1, X2, X3) -> mark# X1)
     (a__add#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
     (a__add#(s X, Y) -> mark# X, mark# zero X -> mark# X)
     (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
     (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
     (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# zero X -> mark# X, mark# s X -> mark# X)
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (mark# zero X -> mark# X, mark# fact X -> mark# X)
     (mark# zero X -> mark# X, mark# fact X -> a__fact# mark X)
     (mark# zero X -> mark# X, mark# p X -> mark# X)
     (mark# zero X -> mark# X, mark# p X -> a__p# mark X)
     (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# zero X -> mark# X, mark# zero X -> a__zero# mark X)
     (mark# zero X -> mark# X, mark# zero X -> mark# X)
     (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# zero X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (mark# fact X -> mark# X, mark# s X -> mark# X)
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
     (mark# fact X -> mark# X, mark# fact X -> mark# X)
     (mark# fact X -> mark# X, mark# fact X -> a__fact# mark X)
     (mark# fact X -> mark# X, mark# p X -> mark# X)
     (mark# fact X -> mark# X, mark# p X -> a__p# mark X)
     (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
     (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# fact X -> mark# X, mark# zero X -> a__zero# mark X)
     (mark# fact X -> mark# X, mark# zero X -> mark# X)
     (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# fact X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X)
     (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (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# fact 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# p X -> mark# X)
     (a__if#(true(), X, Y) -> mark# X, mark# p X -> a__p# mark X)
     (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# if(X1, X2, X3) -> mark# X1)
     (a__if#(true(), X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
     (a__if#(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
     (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
     (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
     (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
    }
    EDG:
     {
      (mark# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# zero X -> mark# X)
      (mark# s X -> mark# X, mark# zero X -> a__zero# mark X)
      (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (mark# s X -> mark# X, mark# p X -> a__p# mark X)
      (mark# s X -> mark# X, mark# p X -> mark# X)
      (mark# s X -> mark# X, mark# fact X -> a__fact# mark X)
      (mark# s X -> mark# X, mark# fact X -> mark# X)
      (mark# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# p X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# p X -> mark# X, mark# zero X -> mark# X)
      (mark# p X -> mark# X, mark# zero X -> a__zero# mark X)
      (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))
      (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# fact X -> a__fact# mark X)
      (mark# p X -> mark# X, mark# fact X -> mark# X)
      (mark# p X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# p X -> mark# X, mark# s X -> mark# X)
      (a__fact# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (a__fact# X -> mark# X, mark# zero X -> mark# X)
      (a__fact# X -> mark# X, mark# zero X -> a__zero# mark X)
      (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (a__fact# X -> mark# X, mark# p X -> a__p# mark X)
      (a__fact# X -> mark# X, mark# p X -> mark# X)
      (a__fact# X -> mark# X, mark# fact X -> a__fact# mark X)
      (a__fact# X -> mark# X, mark# fact X -> mark# X)
      (a__fact# X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (a__fact# X -> mark# X, mark# s X -> mark# X)
      (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
      (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
      (a__add#(0(), X) -> mark# X, mark# zero X -> mark# X)
      (a__add#(0(), X) -> mark# X, mark# zero X -> a__zero# mark X)
      (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (a__add#(0(), X) -> mark# X, mark# p X -> a__p# mark X)
      (a__add#(0(), X) -> mark# X, mark# p X -> mark# X)
      (a__add#(0(), X) -> mark# X, mark# fact X -> a__fact# mark X)
      (a__add#(0(), X) -> mark# X, mark# fact X -> mark# X)
      (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (a__add#(0(), X) -> mark# X, mark# s X -> mark# X)
      (a__p# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (a__p# s X -> mark# X, mark# zero X -> mark# X)
      (a__p# s X -> mark# X, mark# zero X -> a__zero# mark X)
      (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__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# fact X -> a__fact# mark X)
      (a__p# s X -> mark# X, mark# fact X -> mark# X)
      (a__p# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (a__p# s X -> mark# X, mark# s X -> 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# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)
      (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__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# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2)
      (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1)
      (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> a__zero# mark X)
      (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# 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# fact X -> a__fact# mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X)
      (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# prod(X1, X2) -> mark# X2)
      (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
      (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
      (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
      (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
      (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
      (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
      (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))
      (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# fact X -> a__fact# mark X)
      (a__if#(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
      (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# prod(X1, X2) -> mark# X2)
      (a__if#(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
      (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
      (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
      (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
      (a__prod#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
      (a__prod#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
      (a__prod#(s X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
      (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# p X -> a__p# mark X)
      (a__prod#(s X, Y) -> mark# Y, mark# p 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# fact X -> mark# X)
      (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# prod(X1, X2) -> mark# X2)
      (a__prod#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
      (a__prod#(s X, Y) -> mark# Y, 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)
      (a__add#(s X, Y) -> mark# Y, mark# s X -> mark# X)
      (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
      (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
      (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# fact 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# p X -> mark# X)
      (a__add#(s X, Y) -> mark# Y, mark# p X -> a__p# mark X)
      (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# if(X1, X2, X3) -> mark# X1)
      (a__add#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
      (a__add#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
      (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
      (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
      (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
      (mark# add(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
      (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
      (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
      (mark# prod(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
      (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
      (mark# prod(X1, X2) -> mark# X1, 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__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(s X, Y) -> mark# X)
      (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) -> a__add#(mark X, mark Y))
      (a__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(0(), X) -> mark# X)
      (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__prod#(s X, Y) -> mark# X, mark# s X -> mark# X)
      (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> 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# X, mark# fact 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# p X -> mark# X)
      (a__prod#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
      (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# if(X1, X2, X3) -> mark# X1)
      (a__prod#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
      (a__prod#(s X, Y) -> mark# X, mark# zero X -> mark# X)
      (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
      (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
      (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__add#(s X, Y) -> mark# X, mark# s X -> mark# X)
      (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (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# fact 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# p X -> mark# X)
      (a__add#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
      (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# if(X1, X2, X3) -> mark# X1)
      (a__add#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
      (a__add#(s X, Y) -> mark# X, mark# zero X -> mark# X)
      (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
      (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
      (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# zero X -> mark# X, mark# s X -> mark# X)
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (mark# zero X -> mark# X, mark# fact X -> mark# X)
      (mark# zero X -> mark# X, mark# fact X -> a__fact# mark X)
      (mark# zero X -> mark# X, mark# p X -> mark# X)
      (mark# zero X -> mark# X, mark# p X -> a__p# mark X)
      (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# zero X -> mark# X, mark# zero X -> a__zero# mark X)
      (mark# zero X -> mark# X, mark# zero X -> mark# X)
      (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# zero X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (mark# fact X -> mark# X, mark# s X -> mark# X)
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
      (mark# fact X -> mark# X, mark# fact X -> mark# X)
      (mark# fact X -> mark# X, mark# fact X -> a__fact# mark X)
      (mark# fact X -> mark# X, mark# p X -> mark# X)
      (mark# fact X -> mark# X, mark# p X -> a__p# mark X)
      (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
      (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# fact X -> mark# X, mark# zero X -> a__zero# mark X)
      (mark# fact X -> mark# X, mark# zero X -> mark# X)
      (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# fact X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X)
      (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (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# fact 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# p X -> mark# X)
      (a__if#(true(), X, Y) -> mark# X, mark# p X -> a__p# mark X)
      (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# if(X1, X2, X3) -> mark# X1)
      (a__if#(true(), X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
      (a__if#(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
      (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
      (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
      (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
     }
     EDG:
      {
       (mark# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# zero X -> mark# X)
       (mark# s X -> mark# X, mark# zero X -> a__zero# mark X)
       (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (mark# s X -> mark# X, mark# p X -> a__p# mark X)
       (mark# s X -> mark# X, mark# p X -> mark# X)
       (mark# s X -> mark# X, mark# fact X -> a__fact# mark X)
       (mark# s X -> mark# X, mark# fact X -> mark# X)
       (mark# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# s X -> mark# X)
       (mark# p X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# p X -> mark# X, mark# zero X -> mark# X)
       (mark# p X -> mark# X, mark# zero X -> a__zero# mark X)
       (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))
       (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# fact X -> a__fact# mark X)
       (mark# p X -> mark# X, mark# fact X -> mark# X)
       (mark# p X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# p X -> mark# X, mark# s X -> mark# X)
       (a__fact# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (a__fact# X -> mark# X, mark# zero X -> mark# X)
       (a__fact# X -> mark# X, mark# zero X -> a__zero# mark X)
       (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (a__fact# X -> mark# X, mark# p X -> a__p# mark X)
       (a__fact# X -> mark# X, mark# p X -> mark# X)
       (a__fact# X -> mark# X, mark# fact X -> a__fact# mark X)
       (a__fact# X -> mark# X, mark# fact X -> mark# X)
       (a__fact# X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (a__fact# X -> mark# X, mark# s X -> mark# X)
       (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
       (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
       (a__add#(0(), X) -> mark# X, mark# zero X -> mark# X)
       (a__add#(0(), X) -> mark# X, mark# zero X -> a__zero# mark X)
       (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (a__add#(0(), X) -> mark# X, mark# p X -> a__p# mark X)
       (a__add#(0(), X) -> mark# X, mark# p X -> mark# X)
       (a__add#(0(), X) -> mark# X, mark# fact X -> a__fact# mark X)
       (a__add#(0(), X) -> mark# X, mark# fact X -> mark# X)
       (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (a__add#(0(), X) -> mark# X, mark# s X -> mark# X)
       (a__p# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (a__p# s X -> mark# X, mark# zero X -> mark# X)
       (a__p# s X -> mark# X, mark# zero X -> a__zero# mark X)
       (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__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# fact X -> a__fact# mark X)
       (a__p# s X -> mark# X, mark# fact X -> mark# X)
       (a__p# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (a__p# s X -> mark# X, mark# s X -> 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# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)
       (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__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# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2)
       (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1)
       (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> a__zero# mark X)
       (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# 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# fact X -> a__fact# mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X)
       (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# prod(X1, X2) -> mark# X2)
       (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
       (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
       (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
       (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
       (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
       (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
       (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))
       (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# fact X -> a__fact# mark X)
       (a__if#(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
       (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# prod(X1, X2) -> mark# X2)
       (a__if#(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
       (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
       (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
       (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
       (a__prod#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
       (a__prod#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
       (a__prod#(s X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
       (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# p X -> a__p# mark X)
       (a__prod#(s X, Y) -> mark# Y, mark# p 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# fact X -> mark# X)
       (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# prod(X1, X2) -> mark# X2)
       (a__prod#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
       (a__prod#(s X, Y) -> mark# Y, 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)
       (a__add#(s X, Y) -> mark# Y, mark# s X -> mark# X)
       (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
       (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
       (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# fact 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# p X -> mark# X)
       (a__add#(s X, Y) -> mark# Y, mark# p X -> a__p# mark X)
       (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# if(X1, X2, X3) -> mark# X1)
       (a__add#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
       (a__add#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
       (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
       (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
       (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
       (mark# add(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
       (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
       (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
       (mark# prod(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
       (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
       (mark# prod(X1, X2) -> mark# X1, 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__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(s X, Y) -> mark# X)
       (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) -> a__add#(mark X, mark Y))
       (a__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(0(), X) -> mark# X)
       (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__prod#(s X, Y) -> mark# X, mark# s X -> mark# X)
       (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> 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# X, mark# fact 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# p X -> mark# X)
       (a__prod#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
       (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# if(X1, X2, X3) -> mark# X1)
       (a__prod#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
       (a__prod#(s X, Y) -> mark# X, mark# zero X -> mark# X)
       (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
       (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
       (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__add#(s X, Y) -> mark# X, mark# s X -> mark# X)
       (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (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# fact 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# p X -> mark# X)
       (a__add#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
       (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# if(X1, X2, X3) -> mark# X1)
       (a__add#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
       (a__add#(s X, Y) -> mark# X, mark# zero X -> mark# X)
       (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
       (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
       (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# zero X -> mark# X, mark# s X -> mark# X)
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (mark# zero X -> mark# X, mark# fact X -> mark# X)
       (mark# zero X -> mark# X, mark# fact X -> a__fact# mark X)
       (mark# zero X -> mark# X, mark# p X -> mark# X)
       (mark# zero X -> mark# X, mark# p X -> a__p# mark X)
       (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# zero X -> mark# X, mark# zero X -> a__zero# mark X)
       (mark# zero X -> mark# X, mark# zero X -> mark# X)
       (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# zero X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (mark# fact X -> mark# X, mark# s X -> mark# X)
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
       (mark# fact X -> mark# X, mark# fact X -> mark# X)
       (mark# fact X -> mark# X, mark# fact X -> a__fact# mark X)
       (mark# fact X -> mark# X, mark# p X -> mark# X)
       (mark# fact X -> mark# X, mark# p X -> a__p# mark X)
       (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
       (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# fact X -> mark# X, mark# zero X -> a__zero# mark X)
       (mark# fact X -> mark# X, mark# zero X -> mark# X)
       (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# fact X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X)
       (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (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# fact 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# p X -> mark# X)
       (a__if#(true(), X, Y) -> mark# X, mark# p X -> a__p# mark X)
       (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# if(X1, X2, X3) -> mark# X1)
       (a__if#(true(), X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
       (a__if#(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
       (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
       (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
       (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
      }
      EDG:
       {
        (mark# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# zero X -> mark# X)
        (mark# s X -> mark# X, mark# zero X -> a__zero# mark X)
        (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (mark# s X -> mark# X, mark# p X -> a__p# mark X)
        (mark# s X -> mark# X, mark# p X -> mark# X)
        (mark# s X -> mark# X, mark# fact X -> a__fact# mark X)
        (mark# s X -> mark# X, mark# fact X -> mark# X)
        (mark# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# s X -> mark# X)
        (mark# p X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# p X -> mark# X, mark# zero X -> mark# X)
        (mark# p X -> mark# X, mark# zero X -> a__zero# mark X)
        (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))
        (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# fact X -> a__fact# mark X)
        (mark# p X -> mark# X, mark# fact X -> mark# X)
        (mark# p X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# p X -> mark# X, mark# s X -> mark# X)
        (a__fact# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (a__fact# X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (a__fact# X -> mark# X, mark# zero X -> mark# X)
        (a__fact# X -> mark# X, mark# zero X -> a__zero# mark X)
        (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (a__fact# X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (a__fact# X -> mark# X, mark# p X -> a__p# mark X)
        (a__fact# X -> mark# X, mark# p X -> mark# X)
        (a__fact# X -> mark# X, mark# fact X -> a__fact# mark X)
        (a__fact# X -> mark# X, mark# fact X -> mark# X)
        (a__fact# X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (a__fact# X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (a__fact# X -> mark# X, mark# s X -> mark# X)
        (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
        (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
        (a__add#(0(), X) -> mark# X, mark# zero X -> mark# X)
        (a__add#(0(), X) -> mark# X, mark# zero X -> a__zero# mark X)
        (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (a__add#(0(), X) -> mark# X, mark# p X -> a__p# mark X)
        (a__add#(0(), X) -> mark# X, mark# p X -> mark# X)
        (a__add#(0(), X) -> mark# X, mark# fact X -> a__fact# mark X)
        (a__add#(0(), X) -> mark# X, mark# fact X -> mark# X)
        (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (a__add#(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (a__add#(0(), X) -> mark# X, mark# s X -> mark# X)
        (a__p# s X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (a__p# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (a__p# s X -> mark# X, mark# zero X -> mark# X)
        (a__p# s X -> mark# X, mark# zero X -> a__zero# mark X)
        (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__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# fact X -> a__fact# mark X)
        (a__p# s X -> mark# X, mark# fact X -> mark# X)
        (a__p# s X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (a__p# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (a__p# s X -> mark# X, mark# s X -> 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# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)
        (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__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# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2)
        (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1)
        (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> a__zero# mark X)
        (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# 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# fact X -> a__fact# mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X)
        (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# prod(X1, X2) -> mark# X2)
        (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
        (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
        (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
        (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
        (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
        (a__if#(false(), X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
        (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))
        (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# fact X -> a__fact# mark X)
        (a__if#(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
        (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# prod(X1, X2) -> mark# X2)
        (a__if#(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
        (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
        (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
        (a__prod#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
        (a__prod#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
        (a__prod#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
        (a__prod#(s X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
        (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# p X -> a__p# mark X)
        (a__prod#(s X, Y) -> mark# Y, mark# p 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# fact X -> mark# X)
        (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# prod(X1, X2) -> mark# X2)
        (a__prod#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
        (a__prod#(s X, Y) -> mark# Y, 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)
        (a__add#(s X, Y) -> mark# Y, mark# s X -> mark# X)
        (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
        (a__add#(s X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
        (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# fact 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# p X -> mark# X)
        (a__add#(s X, Y) -> mark# Y, mark# p X -> a__p# mark X)
        (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# if(X1, X2, X3) -> mark# X1)
        (a__add#(s X, Y) -> mark# Y, mark# zero X -> a__zero# mark X)
        (a__add#(s X, Y) -> mark# Y, mark# zero X -> mark# X)
        (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
        (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
        (a__add#(s X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
        (mark# add(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
        (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
        (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# fact X -> a__fact# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
        (mark# prod(X1, X2) -> mark# X1, mark# zero X -> a__zero# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
        (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
        (mark# prod(X1, X2) -> mark# X1, 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__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(s X, Y) -> mark# X)
        (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) -> a__add#(mark X, mark Y))
        (a__prod#(s X, Y) -> a__add#(mark Y, a__prod(mark X, mark Y)), a__add#(0(), X) -> mark# X)
        (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__prod#(s X, Y) -> mark# X, mark# s X -> mark# X)
        (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (a__prod#(s X, Y) -> mark# X, mark# prod(X1, X2) -> 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# X, mark# fact 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# p X -> mark# X)
        (a__prod#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
        (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# if(X1, X2, X3) -> mark# X1)
        (a__prod#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
        (a__prod#(s X, Y) -> mark# X, mark# zero X -> mark# X)
        (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
        (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
        (a__prod#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__add#(s X, Y) -> mark# X, mark# s X -> mark# X)
        (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (a__add#(s X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (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# fact 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# p X -> mark# X)
        (a__add#(s X, Y) -> mark# X, mark# p X -> a__p# mark X)
        (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# if(X1, X2, X3) -> mark# X1)
        (a__add#(s X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
        (a__add#(s X, Y) -> mark# X, mark# zero X -> mark# X)
        (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
        (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
        (a__add#(s X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# zero X -> mark# X, mark# s X -> mark# X)
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (mark# zero X -> mark# X, mark# fact X -> mark# X)
        (mark# zero X -> mark# X, mark# fact X -> a__fact# mark X)
        (mark# zero X -> mark# X, mark# p X -> mark# X)
        (mark# zero X -> mark# X, mark# p X -> a__p# mark X)
        (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# zero X -> mark# X, mark# zero X -> a__zero# mark X)
        (mark# zero X -> mark# X, mark# zero X -> mark# X)
        (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# zero X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (mark# fact X -> mark# X, mark# s X -> mark# X)
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> a__prod#(mark X1, mark X2))
        (mark# fact X -> mark# X, mark# fact X -> mark# X)
        (mark# fact X -> mark# X, mark# fact X -> a__fact# mark X)
        (mark# fact X -> mark# X, mark# p X -> mark# X)
        (mark# fact X -> mark# X, mark# p X -> a__p# mark X)
        (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
        (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# fact X -> mark# X, mark# zero X -> a__zero# mark X)
        (mark# fact X -> mark# X, mark# zero X -> mark# X)
        (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# fact X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
        (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X)
        (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (a__if#(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (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# fact 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# p X -> mark# X)
        (a__if#(true(), X, Y) -> mark# X, mark# p X -> a__p# mark X)
        (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# if(X1, X2, X3) -> mark# X1)
        (a__if#(true(), X, Y) -> mark# X, mark# zero X -> a__zero# mark X)
        (a__if#(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
        (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
        (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
        (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2))
       }
       STATUS:
        arrows: 0.645660
        SCCS (1):
         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 (27):
          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}
          Open