MAYBE
Time: 0.154557
TRS:
 {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
               mark zero X -> active zero mark X,
                  mark s X -> active s mark X,
                  mark 0() -> active 0(),
         mark prod(X1, X2) -> active prod(mark X1, mark X2),
               mark fact X -> active fact mark X,
                  mark p X -> active p mark X,
          mark add(X1, X2) -> active add(mark X1, mark X2),
               mark true() -> active true(),
              mark false() -> active false(),
       if(X1, X2, mark X3) -> if(X1, X2, X3),
     if(X1, X2, active X3) -> if(X1, X2, X3),
       if(X1, mark X2, X3) -> if(X1, X2, X3),
     if(X1, active X2, X3) -> if(X1, X2, X3),
       if(mark X1, X2, X3) -> if(X1, X2, X3),
     if(active X1, X2, X3) -> if(X1, X2, X3),
               zero mark X -> zero X,
             zero active X -> zero X,
                  s mark X -> s X,
                s active X -> s X,
         prod(X1, mark X2) -> prod(X1, X2),
       prod(X1, active X2) -> prod(X1, X2),
         prod(mark X1, X2) -> prod(X1, X2),
       prod(active X1, X2) -> prod(X1, X2),
               fact mark X -> fact X,
             fact active X -> fact X,
                  p mark X -> p X,
                p active X -> p X,
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
           active zero s X -> mark false(),
           active zero 0() -> mark true(),
       active prod(s X, Y) -> mark add(Y, prod(X, Y)),
       active prod(0(), X) -> mark 0(),
             active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
              active p s X -> mark X,
        active add(s X, Y) -> mark s add(X, Y),
        active add(0(), X) -> mark X,
          add(X1, mark X2) -> add(X1, X2),
        add(X1, active X2) -> add(X1, X2),
          add(mark X1, X2) -> add(X1, X2),
        add(active X1, X2) -> add(X1, X2)}
 DP:
  DP:
   {     mark# if(X1, X2, X3) -> mark# X1,
         mark# if(X1, X2, X3) -> if#(mark X1, X2, X3),
         mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3),
                 mark# zero X -> mark# X,
                 mark# zero X -> zero# mark X,
                 mark# zero X -> active# zero mark X,
                    mark# s X -> mark# X,
                    mark# s X -> s# mark X,
                    mark# s X -> active# s mark X,
                    mark# 0() -> active# 0(),
           mark# prod(X1, X2) -> mark# X1,
           mark# prod(X1, X2) -> mark# X2,
           mark# prod(X1, X2) -> prod#(mark X1, mark X2),
           mark# prod(X1, X2) -> active# prod(mark X1, mark X2),
                 mark# fact X -> mark# X,
                 mark# fact X -> fact# mark X,
                 mark# fact X -> active# fact mark X,
                    mark# p X -> mark# X,
                    mark# p X -> p# mark X,
                    mark# p X -> active# p mark X,
            mark# add(X1, X2) -> mark# X1,
            mark# add(X1, X2) -> mark# X2,
            mark# add(X1, X2) -> active# add(mark X1, mark X2),
            mark# add(X1, X2) -> add#(mark X1, mark X2),
                 mark# true() -> active# true(),
                mark# false() -> active# false(),
         if#(X1, X2, mark X3) -> if#(X1, X2, X3),
       if#(X1, X2, active X3) -> if#(X1, X2, X3),
         if#(X1, mark X2, X3) -> if#(X1, X2, X3),
       if#(X1, active X2, X3) -> if#(X1, X2, X3),
         if#(mark X1, X2, X3) -> if#(X1, X2, X3),
       if#(active X1, X2, X3) -> if#(X1, X2, X3),
                 zero# mark X -> zero# X,
               zero# active X -> zero# X,
                    s# mark X -> s# X,
                  s# active X -> s# X,
           prod#(X1, mark X2) -> prod#(X1, X2),
         prod#(X1, active X2) -> prod#(X1, X2),
           prod#(mark X1, X2) -> prod#(X1, X2),
         prod#(active X1, X2) -> prod#(X1, X2),
                 fact# mark X -> fact# X,
               fact# active X -> fact# X,
                    p# mark X -> p# X,
                  p# active X -> p# X,
     active# if(true(), X, Y) -> mark# X,
    active# if(false(), X, Y) -> mark# Y,
             active# zero s X -> mark# false(),
             active# zero 0() -> mark# true(),
         active# prod(s X, Y) -> mark# add(Y, prod(X, Y)),
         active# prod(s X, Y) -> prod#(X, Y),
         active# prod(s X, Y) -> add#(Y, prod(X, Y)),
         active# prod(0(), X) -> mark# 0(),
               active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)),
               active# fact X -> if#(zero X, s 0(), prod(X, fact p X)),
               active# fact X -> zero# X,
               active# fact X -> s# 0(),
               active# fact X -> prod#(X, fact p X),
               active# fact X -> fact# p X,
               active# fact X -> p# X,
                active# p s X -> mark# X,
          active# add(s X, Y) -> mark# s add(X, Y),
          active# add(s X, Y) -> s# add(X, Y),
          active# add(s X, Y) -> add#(X, Y),
          active# add(0(), X) -> mark# X,
            add#(X1, mark X2) -> add#(X1, X2),
          add#(X1, active X2) -> add#(X1, X2),
            add#(mark X1, X2) -> add#(X1, X2),
          add#(active X1, X2) -> add#(X1, X2)}
  TRS:
  {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                mark zero X -> active zero mark X,
                   mark s X -> active s mark X,
                   mark 0() -> active 0(),
          mark prod(X1, X2) -> active prod(mark X1, mark X2),
                mark fact X -> active fact mark X,
                   mark p X -> active p mark X,
           mark add(X1, X2) -> active add(mark X1, mark X2),
                mark true() -> active true(),
               mark false() -> active false(),
        if(X1, X2, mark X3) -> if(X1, X2, X3),
      if(X1, X2, active X3) -> if(X1, X2, X3),
        if(X1, mark X2, X3) -> if(X1, X2, X3),
      if(X1, active X2, X3) -> if(X1, X2, X3),
        if(mark X1, X2, X3) -> if(X1, X2, X3),
      if(active X1, X2, X3) -> if(X1, X2, X3),
                zero mark X -> zero X,
              zero active X -> zero X,
                   s mark X -> s X,
                 s active X -> s X,
          prod(X1, mark X2) -> prod(X1, X2),
        prod(X1, active X2) -> prod(X1, X2),
          prod(mark X1, X2) -> prod(X1, X2),
        prod(active X1, X2) -> prod(X1, X2),
                fact mark X -> fact X,
              fact active X -> fact X,
                   p mark X -> p X,
                 p active X -> p X,
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
            active zero s X -> mark false(),
            active zero 0() -> mark true(),
        active prod(s X, Y) -> mark add(Y, prod(X, Y)),
        active prod(0(), X) -> mark 0(),
              active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
               active p s X -> mark X,
         active add(s X, Y) -> mark s add(X, Y),
         active add(0(), X) -> mark X,
           add(X1, mark X2) -> add(X1, X2),
         add(X1, active X2) -> add(X1, X2),
           add(mark X1, X2) -> add(X1, X2),
         add(active X1, X2) -> add(X1, X2)}
  UR:
   {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                 mark zero X -> active zero mark X,
                    mark s X -> active s mark X,
                    mark 0() -> active 0(),
           mark prod(X1, X2) -> active prod(mark X1, mark X2),
                 mark fact X -> active fact mark X,
                    mark p X -> active p mark X,
            mark add(X1, X2) -> active add(mark X1, mark X2),
                 mark true() -> active true(),
                mark false() -> active false(),
         if(X1, X2, mark X3) -> if(X1, X2, X3),
       if(X1, X2, active X3) -> if(X1, X2, X3),
         if(X1, mark X2, X3) -> if(X1, X2, X3),
       if(X1, active X2, X3) -> if(X1, X2, X3),
         if(mark X1, X2, X3) -> if(X1, X2, X3),
       if(active X1, X2, X3) -> if(X1, X2, X3),
                 zero mark X -> zero X,
               zero active X -> zero X,
                    s mark X -> s X,
                  s active X -> s X,
           prod(X1, mark X2) -> prod(X1, X2),
         prod(X1, active X2) -> prod(X1, X2),
           prod(mark X1, X2) -> prod(X1, X2),
         prod(active X1, X2) -> prod(X1, X2),
                 fact mark X -> fact X,
               fact active X -> fact X,
                    p mark X -> p X,
                  p active X -> p X,
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
             active zero s X -> mark false(),
             active zero 0() -> mark true(),
         active prod(s X, Y) -> mark add(Y, prod(X, Y)),
         active prod(0(), X) -> mark 0(),
               active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                active p s X -> mark X,
          active add(s X, Y) -> mark s add(X, Y),
          active add(0(), X) -> mark X,
            add(X1, mark X2) -> add(X1, X2),
          add(X1, active X2) -> add(X1, X2),
            add(mark X1, X2) -> add(X1, X2),
          add(active X1, X2) -> add(X1, X2),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {
     (mark# s X -> s# mark X, s# active X -> s# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (mark# p X -> p# mark X, p# active X -> p# X)
     (mark# p X -> p# mark X, p# mark X -> p# X)
     (mark# zero X -> mark# X, mark# false() -> active# false())
     (mark# zero X -> mark# X, mark# true() -> active# true())
     (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# zero X -> mark# X, mark# p X -> active# p mark X)
     (mark# zero X -> mark# X, mark# p X -> p# mark X)
     (mark# zero X -> mark# X, mark# p X -> mark# X)
     (mark# zero X -> mark# X, mark# fact X -> active# fact mark X)
     (mark# zero X -> mark# X, mark# fact X -> fact# mark X)
     (mark# zero X -> mark# X, mark# fact X -> mark# X)
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# zero X -> mark# X, mark# 0() -> active# 0())
     (mark# zero X -> mark# X, mark# s X -> active# s mark X)
     (mark# zero X -> mark# X, mark# s X -> s# mark X)
     (mark# zero X -> mark# X, mark# s X -> mark# X)
     (mark# zero X -> mark# X, mark# zero X -> active# zero mark X)
     (mark# zero X -> mark# X, mark# zero X -> zero# mark X)
     (mark# zero X -> mark# X, mark# zero X -> mark# X)
     (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# fact X -> mark# X, mark# false() -> active# false())
     (mark# fact X -> mark# X, mark# true() -> active# true())
     (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# fact X -> mark# X, mark# p X -> active# p mark X)
     (mark# fact X -> mark# X, mark# p X -> p# mark X)
     (mark# fact X -> mark# X, mark# p X -> mark# X)
     (mark# fact X -> mark# X, mark# fact X -> active# fact mark X)
     (mark# fact X -> mark# X, mark# fact X -> fact# mark X)
     (mark# fact X -> mark# X, mark# fact X -> mark# X)
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# fact X -> mark# X, mark# 0() -> active# 0())
     (mark# fact X -> mark# X, mark# s X -> active# s mark X)
     (mark# fact X -> mark# X, mark# s X -> s# mark X)
     (mark# fact X -> mark# X, mark# s X -> mark# X)
     (mark# fact X -> mark# X, mark# zero X -> active# zero mark X)
     (mark# fact X -> mark# X, mark# zero X -> zero# mark X)
     (mark# fact X -> mark# X, mark# zero X -> mark# X)
     (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (zero# mark X -> zero# X, zero# active X -> zero# X)
     (zero# mark X -> zero# X, zero# mark X -> zero# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (fact# mark X -> fact# X, fact# active X -> fact# X)
     (fact# mark X -> fact# X, fact# mark X -> fact# X)
     (p# mark X -> p# X, p# active X -> p# X)
     (p# mark X -> p# X, p# mark X -> p# X)
     (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false())
     (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true())
     (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
     (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
     (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p mark X)
     (active# if(true(), X, Y) -> mark# X, mark# p X -> p# mark X)
     (active# if(true(), X, Y) -> mark# X, mark# p X -> mark# X)
     (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X)
     (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X)
     (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X)
     (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0())
     (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X)
     (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X)
     (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X)
     (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X)
     (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X)
     (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (active# fact X -> p# X, p# active X -> p# X)
     (active# fact X -> p# X, p# mark X -> p# X)
     (active# add(0(), X) -> mark# X, mark# false() -> active# false())
     (active# add(0(), X) -> mark# X, mark# true() -> active# true())
     (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
     (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
     (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X)
     (active# add(0(), X) -> mark# X, mark# p X -> p# mark X)
     (active# add(0(), X) -> mark# X, mark# p X -> mark# X)
     (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X)
     (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X)
     (active# add(0(), X) -> mark# X, mark# fact X -> mark# X)
     (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
     (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X)
     (active# add(0(), X) -> mark# X, mark# s X -> s# mark X)
     (active# add(0(), X) -> mark# X, mark# s X -> mark# X)
     (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X)
     (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X)
     (active# add(0(), X) -> mark# X, mark# zero X -> mark# X)
     (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# zero X -> active# zero mark X, active# add(0(), X) -> mark# X)
     (mark# zero X -> active# zero mark X, active# add(s X, Y) -> add#(X, Y))
     (mark# zero X -> active# zero mark X, active# add(s X, Y) -> s# add(X, Y))
     (mark# zero X -> active# zero mark X, active# add(s X, Y) -> mark# s add(X, Y))
     (mark# zero X -> active# zero mark X, active# p s X -> mark# X)
     (mark# zero X -> active# zero mark X, active# fact X -> p# X)
     (mark# zero X -> active# zero mark X, active# fact X -> fact# p X)
     (mark# zero X -> active# zero mark X, active# fact X -> prod#(X, fact p X))
     (mark# zero X -> active# zero mark X, active# fact X -> s# 0())
     (mark# zero X -> active# zero mark X, active# fact X -> zero# X)
     (mark# zero X -> active# zero mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# zero X -> active# zero mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# zero X -> active# zero mark X, active# prod(0(), X) -> mark# 0())
     (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> prod#(X, Y))
     (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true())
     (mark# zero X -> active# zero mark X, active# zero s X -> mark# false())
     (mark# zero X -> active# zero mark X, active# if(false(), X, Y) -> mark# Y)
     (mark# zero X -> active# zero mark X, active# if(true(), X, Y) -> mark# X)
     (mark# fact X -> active# fact mark X, active# add(0(), X) -> mark# X)
     (mark# fact X -> active# fact mark X, active# add(s X, Y) -> add#(X, Y))
     (mark# fact X -> active# fact mark X, active# add(s X, Y) -> s# add(X, Y))
     (mark# fact X -> active# fact mark X, active# add(s X, Y) -> mark# s add(X, Y))
     (mark# fact X -> active# fact mark X, active# p s X -> mark# X)
     (mark# fact X -> active# fact mark X, active# fact X -> p# X)
     (mark# fact X -> active# fact mark X, active# fact X -> fact# p X)
     (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X))
     (mark# fact X -> active# fact mark X, active# fact X -> s# 0())
     (mark# fact X -> active# fact mark X, active# fact X -> zero# X)
     (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# fact X -> active# fact mark X, active# prod(0(), X) -> mark# 0())
     (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> prod#(X, Y))
     (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# fact X -> active# fact mark X, active# zero 0() -> mark# true())
     (mark# fact X -> active# fact mark X, active# zero s X -> mark# false())
     (mark# fact X -> active# fact mark X, active# if(false(), X, Y) -> mark# Y)
     (mark# fact X -> active# fact mark X, active# if(true(), X, Y) -> mark# X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# false() -> active# false())
     (active# add(s X, Y) -> mark# s add(X, Y), mark# true() -> active# true())
     (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X2)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> active# p mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> p# mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> mark# X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> active# fact mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> fact# mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> mark# X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X2)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X1)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# 0() -> active# 0())
     (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> active# zero mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> zero# mark X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> mark# X)
     (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> mark# X1)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# p s X -> mark# X)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> p# X)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> fact# p X)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> prod#(X, fact p X))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> s# 0())
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> zero# X)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(0(), X) -> mark# 0())
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero 0() -> mark# true())
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero s X -> mark# false())
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y)
     (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(true(), X, Y) -> mark# X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# false() -> active# false())
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# true() -> active# true())
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X2)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X1)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> active# p mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> p# mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> mark# X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> active# fact mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> fact# mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> mark# X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X2)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X1)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# 0() -> active# 0())
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> active# s mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> s# mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> mark# X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> active# zero mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> zero# mark X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> mark# X)
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1)
     (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2))
     (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2))
     (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2))
     (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false())
     (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true())
     (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> 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 -> active# fact mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> 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) -> active# prod(mark X1, mark X2))
     (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> 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# 0() -> active# 0())
     (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
     (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false())
     (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true())
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
     (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X)
     (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
     (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
     (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
     (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
     (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
     (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
     (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
     (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
     (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
     (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
     (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
     (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
     (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
     (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
     (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (mark# 0() -> active# 0(), active# add(0(), X) -> mark# X)
     (mark# 0() -> active# 0(), active# add(s X, Y) -> add#(X, Y))
     (mark# 0() -> active# 0(), active# add(s X, Y) -> s# add(X, Y))
     (mark# 0() -> active# 0(), active# add(s X, Y) -> mark# s add(X, Y))
     (mark# 0() -> active# 0(), active# p s X -> mark# X)
     (mark# 0() -> active# 0(), active# fact X -> p# X)
     (mark# 0() -> active# 0(), active# fact X -> fact# p X)
     (mark# 0() -> active# 0(), active# fact X -> prod#(X, fact p X))
     (mark# 0() -> active# 0(), active# fact X -> s# 0())
     (mark# 0() -> active# 0(), active# fact X -> zero# X)
     (mark# 0() -> active# 0(), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# 0() -> active# 0(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# 0() -> active# 0(), active# prod(0(), X) -> mark# 0())
     (mark# 0() -> active# 0(), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# 0() -> active# 0(), active# prod(s X, Y) -> prod#(X, Y))
     (mark# 0() -> active# 0(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# 0() -> active# 0(), active# zero 0() -> mark# true())
     (mark# 0() -> active# 0(), active# zero s X -> mark# false())
     (mark# 0() -> active# 0(), active# if(false(), X, Y) -> mark# Y)
     (mark# 0() -> active# 0(), active# if(true(), X, Y) -> mark# X)
     (mark# false() -> active# false(), active# add(0(), X) -> mark# X)
     (mark# false() -> active# false(), active# add(s X, Y) -> add#(X, Y))
     (mark# false() -> active# false(), active# add(s X, Y) -> s# add(X, Y))
     (mark# false() -> active# false(), active# add(s X, Y) -> mark# s add(X, Y))
     (mark# false() -> active# false(), active# p s X -> mark# X)
     (mark# false() -> active# false(), active# fact X -> p# X)
     (mark# false() -> active# false(), active# fact X -> fact# p X)
     (mark# false() -> active# false(), active# fact X -> prod#(X, fact p X))
     (mark# false() -> active# false(), active# fact X -> s# 0())
     (mark# false() -> active# false(), active# fact X -> zero# X)
     (mark# false() -> active# false(), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# false() -> active# false(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# false() -> active# false(), active# prod(0(), X) -> mark# 0())
     (mark# false() -> active# false(), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# false() -> active# false(), active# prod(s X, Y) -> prod#(X, Y))
     (mark# false() -> active# false(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# false() -> active# false(), active# zero 0() -> mark# true())
     (mark# false() -> active# false(), active# zero s X -> mark# false())
     (mark# false() -> active# false(), active# if(false(), X, Y) -> mark# Y)
     (mark# false() -> active# false(), active# if(true(), X, Y) -> mark# X)
     (active# zero 0() -> mark# true(), mark# false() -> active# false())
     (active# zero 0() -> mark# true(), mark# true() -> active# true())
     (active# zero 0() -> mark# true(), mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# zero 0() -> mark# true(), mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# zero 0() -> mark# true(), mark# add(X1, X2) -> mark# X2)
     (active# zero 0() -> mark# true(), mark# add(X1, X2) -> mark# X1)
     (active# zero 0() -> mark# true(), mark# p X -> active# p mark X)
     (active# zero 0() -> mark# true(), mark# p X -> p# mark X)
     (active# zero 0() -> mark# true(), mark# p X -> mark# X)
     (active# zero 0() -> mark# true(), mark# fact X -> active# fact mark X)
     (active# zero 0() -> mark# true(), mark# fact X -> fact# mark X)
     (active# zero 0() -> mark# true(), mark# fact X -> mark# X)
     (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> mark# X2)
     (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> mark# X1)
     (active# zero 0() -> mark# true(), mark# 0() -> active# 0())
     (active# zero 0() -> mark# true(), mark# s X -> active# s mark X)
     (active# zero 0() -> mark# true(), mark# s X -> s# mark X)
     (active# zero 0() -> mark# true(), mark# s X -> mark# X)
     (active# zero 0() -> mark# true(), mark# zero X -> active# zero mark X)
     (active# zero 0() -> mark# true(), mark# zero X -> zero# mark X)
     (active# zero 0() -> mark# true(), mark# zero X -> mark# X)
     (active# zero 0() -> mark# true(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# zero 0() -> mark# true(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# zero 0() -> mark# true(), mark# if(X1, X2, X3) -> mark# X1)
     (active# fact X -> s# 0(), s# active X -> s# X)
     (active# fact X -> s# 0(), s# mark X -> s# X)
     (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false())
     (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true())
     (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
     (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X)
     (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X)
     (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
     (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X)
     (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X)
     (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> 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# 0() -> active# 0())
     (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
     (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
     (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X)
     (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
     (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X)
     (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# false() -> active# false())
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# true() -> active# true())
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> active# p mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> p# mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> mark# X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> active# fact mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> fact# mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> mark# X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X2)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X1)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# 0() -> active# 0())
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> active# s mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> s# mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> mark# X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> active# zero mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> zero# mark X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> mark# X)
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> mark# X1)
     (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
     (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2))
     (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2))
     (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2))
     (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2))
     (active# fact X -> prod#(X, fact p X), prod#(X1, mark X2) -> prod#(X1, X2))
     (active# fact X -> prod#(X, fact p X), prod#(X1, active X2) -> prod#(X1, X2))
     (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2))
     (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
     (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X)
     (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (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) -> prod#(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X)
     (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X)
     (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true())
     (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false())
     (active# prod(0(), X) -> mark# 0(), mark# if(X1, X2, X3) -> mark# X1)
     (active# prod(0(), X) -> mark# 0(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# prod(0(), X) -> mark# 0(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# prod(0(), X) -> mark# 0(), mark# zero X -> mark# X)
     (active# prod(0(), X) -> mark# 0(), mark# zero X -> zero# mark X)
     (active# prod(0(), X) -> mark# 0(), mark# zero X -> active# zero mark X)
     (active# prod(0(), X) -> mark# 0(), mark# s X -> mark# X)
     (active# prod(0(), X) -> mark# 0(), mark# s X -> s# mark X)
     (active# prod(0(), X) -> mark# 0(), mark# s X -> active# s mark X)
     (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0())
     (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> mark# X1)
     (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> mark# X2)
     (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# prod(0(), X) -> mark# 0(), mark# fact X -> mark# X)
     (active# prod(0(), X) -> mark# 0(), mark# fact X -> fact# mark X)
     (active# prod(0(), X) -> mark# 0(), mark# fact X -> active# fact mark X)
     (active# prod(0(), X) -> mark# 0(), mark# p X -> mark# X)
     (active# prod(0(), X) -> mark# 0(), mark# p X -> p# mark X)
     (active# prod(0(), X) -> mark# 0(), mark# p X -> active# p mark X)
     (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> mark# X1)
     (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> mark# X2)
     (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# prod(0(), X) -> mark# 0(), mark# true() -> active# true())
     (active# prod(0(), X) -> mark# 0(), mark# false() -> active# false())
     (active# zero s X -> mark# false(), mark# if(X1, X2, X3) -> mark# X1)
     (active# zero s X -> mark# false(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# zero s X -> mark# false(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# zero s X -> mark# false(), mark# zero X -> mark# X)
     (active# zero s X -> mark# false(), mark# zero X -> zero# mark X)
     (active# zero s X -> mark# false(), mark# zero X -> active# zero mark X)
     (active# zero s X -> mark# false(), mark# s X -> mark# X)
     (active# zero s X -> mark# false(), mark# s X -> s# mark X)
     (active# zero s X -> mark# false(), mark# s X -> active# s mark X)
     (active# zero s X -> mark# false(), mark# 0() -> active# 0())
     (active# zero s X -> mark# false(), mark# prod(X1, X2) -> mark# X1)
     (active# zero s X -> mark# false(), mark# prod(X1, X2) -> mark# X2)
     (active# zero s X -> mark# false(), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# zero s X -> mark# false(), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# zero s X -> mark# false(), mark# fact X -> mark# X)
     (active# zero s X -> mark# false(), mark# fact X -> fact# mark X)
     (active# zero s X -> mark# false(), mark# fact X -> active# fact mark X)
     (active# zero s X -> mark# false(), mark# p X -> mark# X)
     (active# zero s X -> mark# false(), mark# p X -> p# mark X)
     (active# zero s X -> mark# false(), mark# p X -> active# p mark X)
     (active# zero s X -> mark# false(), mark# add(X1, X2) -> mark# X1)
     (active# zero s X -> mark# false(), mark# add(X1, X2) -> mark# X2)
     (active# zero s X -> mark# false(), mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# zero s X -> mark# false(), mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# zero s X -> mark# false(), mark# true() -> active# true())
     (active# zero s X -> mark# false(), mark# false() -> active# false())
     (mark# true() -> active# true(), active# if(true(), X, Y) -> mark# X)
     (mark# true() -> active# true(), active# if(false(), X, Y) -> mark# Y)
     (mark# true() -> active# true(), active# zero s X -> mark# false())
     (mark# true() -> active# true(), active# zero 0() -> mark# true())
     (mark# true() -> active# true(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# true() -> active# true(), active# prod(s X, Y) -> prod#(X, Y))
     (mark# true() -> active# true(), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# true() -> active# true(), active# prod(0(), X) -> mark# 0())
     (mark# true() -> active# true(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# true() -> active# true(), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# true() -> active# true(), active# fact X -> zero# X)
     (mark# true() -> active# true(), active# fact X -> s# 0())
     (mark# true() -> active# true(), active# fact X -> prod#(X, fact p X))
     (mark# true() -> active# true(), active# fact X -> fact# p X)
     (mark# true() -> active# true(), active# fact X -> p# X)
     (mark# true() -> active# true(), active# p s X -> mark# X)
     (mark# true() -> active# true(), active# add(s X, Y) -> mark# s add(X, Y))
     (mark# true() -> active# true(), active# add(s X, Y) -> s# add(X, Y))
     (mark# true() -> active# true(), active# add(s X, Y) -> add#(X, Y))
     (mark# true() -> active# true(), active# add(0(), X) -> mark# X)
     (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
     (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
     (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
     (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
     (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
     (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
     (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
     (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X)
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y)
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero s X -> mark# false())
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero 0() -> mark# true())
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> prod#(X, Y))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(0(), X) -> mark# 0())
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> zero# X)
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> s# 0())
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> prod#(X, fact p X))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> fact# p X)
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> p# X)
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# p s X -> mark# X)
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> mark# s add(X, Y))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> s# add(X, Y))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> add#(X, Y))
     (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(0(), X) -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
     (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (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) -> prod#(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
     (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X)
     (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true())
     (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false())
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
     (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2))
     (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2))
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# if(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
     (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
     (active# if(false(), X, Y) -> mark# Y, mark# s X -> s# mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0())
     (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
     (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
     (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
     (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# p X -> mark# X)
     (active# if(false(), X, Y) -> mark# Y, mark# p X -> p# mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# p X -> active# p mark X)
     (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
     (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
     (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true())
     (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false())
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(true(), X, Y) -> mark# X)
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y)
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero s X -> mark# false())
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero 0() -> mark# true())
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0())
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> zero# X)
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> s# 0())
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> prod#(X, fact p X))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> fact# p X)
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> p# X)
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# p s X -> mark# X)
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
     (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(0(), X) -> mark# X)
     (mark# p X -> active# p mark X, active# if(true(), X, Y) -> mark# X)
     (mark# p X -> active# p mark X, active# if(false(), X, Y) -> mark# Y)
     (mark# p X -> active# p mark X, active# zero s X -> mark# false())
     (mark# p X -> active# p mark X, active# zero 0() -> mark# true())
     (mark# p X -> active# p mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# p X -> active# p mark X, active# prod(s X, Y) -> prod#(X, Y))
     (mark# p X -> active# p mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# p X -> active# p mark X, active# prod(0(), X) -> mark# 0())
     (mark# p X -> active# p mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# p X -> active# p mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# p X -> active# p mark X, active# fact X -> zero# X)
     (mark# p X -> active# p mark X, active# fact X -> s# 0())
     (mark# p X -> active# p mark X, active# fact X -> prod#(X, fact p X))
     (mark# p X -> active# p mark X, active# fact X -> fact# p X)
     (mark# p X -> active# p mark X, active# fact X -> p# X)
     (mark# p X -> active# p mark X, active# p s X -> mark# X)
     (mark# p X -> active# p mark X, active# add(s X, Y) -> mark# s add(X, Y))
     (mark# p X -> active# p mark X, active# add(s X, Y) -> s# add(X, Y))
     (mark# p X -> active# p mark X, active# add(s X, Y) -> add#(X, Y))
     (mark# p X -> active# p mark X, active# add(0(), X) -> mark# X)
     (mark# s X -> active# s mark X, active# if(true(), X, Y) -> mark# X)
     (mark# s X -> active# s mark X, active# if(false(), X, Y) -> mark# Y)
     (mark# s X -> active# s mark X, active# zero s X -> mark# false())
     (mark# s X -> active# s mark X, active# zero 0() -> mark# true())
     (mark# s X -> active# s mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
     (mark# s X -> active# s mark X, active# prod(s X, Y) -> prod#(X, Y))
     (mark# s X -> active# s mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (mark# s X -> active# s mark X, active# prod(0(), X) -> mark# 0())
     (mark# s X -> active# s mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
     (mark# s X -> active# s mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (mark# s X -> active# s mark X, active# fact X -> zero# X)
     (mark# s X -> active# s mark X, active# fact X -> s# 0())
     (mark# s X -> active# s mark X, active# fact X -> prod#(X, fact p X))
     (mark# s X -> active# s mark X, active# fact X -> fact# p X)
     (mark# s X -> active# s mark X, active# fact X -> p# X)
     (mark# s X -> active# s mark X, active# p s X -> mark# X)
     (mark# s X -> active# s mark X, active# add(s X, Y) -> mark# s add(X, Y))
     (mark# s X -> active# s mark X, active# add(s X, Y) -> s# add(X, Y))
     (mark# s X -> active# s mark X, active# add(s X, Y) -> add#(X, Y))
     (mark# s X -> active# s mark X, active# add(0(), X) -> mark# X)
     (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, mark X2) -> add#(X1, X2))
     (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, active X2) -> add#(X1, X2))
     (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2))
     (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2))
     (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (active# p s X -> mark# X, mark# zero X -> mark# X)
     (active# p s X -> mark# X, mark# zero X -> zero# mark X)
     (active# p s X -> mark# X, mark# zero X -> active# zero mark X)
     (active# p s X -> mark# X, mark# s X -> mark# X)
     (active# p s X -> mark# X, mark# s X -> s# mark X)
     (active# p s X -> mark# X, mark# s X -> active# s mark X)
     (active# p s X -> mark# X, mark# 0() -> active# 0())
     (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (active# p s X -> mark# X, mark# fact X -> mark# X)
     (active# p s X -> mark# X, mark# fact X -> fact# mark X)
     (active# p s X -> mark# X, mark# fact X -> active# fact mark X)
     (active# p s X -> mark# X, mark# p X -> mark# X)
     (active# p s X -> mark# X, mark# p X -> p# mark X)
     (active# p s X -> mark# X, mark# p X -> active# p mark X)
     (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (active# p s X -> mark# X, mark# true() -> active# true())
     (active# p s X -> mark# X, mark# false() -> active# false())
     (active# fact X -> zero# X, zero# mark X -> zero# X)
     (active# fact X -> zero# X, zero# active X -> zero# X)
     (p# active X -> p# X, p# mark X -> p# X)
     (p# active X -> p# X, p# active X -> p# X)
     (fact# active X -> fact# X, fact# mark X -> fact# X)
     (fact# active X -> fact# X, fact# active X -> fact# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (s# active X -> s# X, s# active X -> s# X)
     (zero# active X -> zero# X, zero# mark X -> zero# X)
     (zero# active X -> zero# X, zero# active X -> zero# X)
     (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# p X -> mark# X, mark# zero X -> mark# X)
     (mark# p X -> mark# X, mark# zero X -> zero# mark X)
     (mark# p X -> mark# X, mark# zero X -> active# zero mark X)
     (mark# p X -> mark# X, mark# s X -> mark# X)
     (mark# p X -> mark# X, mark# s X -> s# mark X)
     (mark# p X -> mark# X, mark# s X -> active# s mark X)
     (mark# p X -> mark# X, mark# 0() -> active# 0())
     (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (mark# p X -> mark# X, mark# fact X -> mark# X)
     (mark# p X -> mark# X, mark# fact X -> fact# mark X)
     (mark# p X -> mark# X, mark# fact X -> active# fact mark X)
     (mark# p X -> mark# X, mark# p X -> mark# X)
     (mark# p X -> mark# X, mark# p X -> p# mark X)
     (mark# p X -> mark# X, mark# p X -> active# p mark X)
     (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# p X -> mark# X, mark# true() -> active# true())
     (mark# p X -> mark# X, mark# false() -> active# false())
     (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# zero X -> mark# X)
     (mark# s X -> mark# X, mark# zero X -> zero# mark X)
     (mark# s X -> mark# X, mark# zero X -> active# zero mark X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
     (mark# s X -> mark# X, mark# fact X -> mark# X)
     (mark# s X -> mark# X, mark# fact X -> fact# mark X)
     (mark# s X -> mark# X, mark# fact X -> active# fact mark X)
     (mark# s X -> mark# X, mark# p X -> mark# X)
     (mark# s X -> mark# X, mark# p X -> p# mark X)
     (mark# s X -> mark# X, mark# p X -> active# p mark X)
     (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
     (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# true() -> active# true())
     (mark# s X -> mark# X, mark# false() -> active# false())
     (active# fact X -> fact# p X, fact# mark X -> fact# X)
     (active# fact X -> fact# p X, fact# active X -> fact# X)
     (mark# fact X -> fact# mark X, fact# mark X -> fact# X)
     (mark# fact X -> fact# mark X, fact# active X -> fact# X)
     (mark# zero X -> zero# mark X, zero# mark X -> zero# X)
     (mark# zero X -> zero# mark X, zero# active X -> zero# X)
    }
    EDG:
     {
      (mark# s X -> s# mark X, s# active X -> s# X)
      (mark# s X -> s# mark X, s# mark X -> s# X)
      (mark# p X -> p# mark X, p# active X -> p# X)
      (mark# p X -> p# mark X, p# mark X -> p# X)
      (mark# zero X -> mark# X, mark# false() -> active# false())
      (mark# zero X -> mark# X, mark# true() -> active# true())
      (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# zero X -> mark# X, mark# p X -> active# p mark X)
      (mark# zero X -> mark# X, mark# p X -> p# mark X)
      (mark# zero X -> mark# X, mark# p X -> mark# X)
      (mark# zero X -> mark# X, mark# fact X -> active# fact mark X)
      (mark# zero X -> mark# X, mark# fact X -> fact# mark X)
      (mark# zero X -> mark# X, mark# fact X -> mark# X)
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# zero X -> mark# X, mark# 0() -> active# 0())
      (mark# zero X -> mark# X, mark# s X -> active# s mark X)
      (mark# zero X -> mark# X, mark# s X -> s# mark X)
      (mark# zero X -> mark# X, mark# s X -> mark# X)
      (mark# zero X -> mark# X, mark# zero X -> active# zero mark X)
      (mark# zero X -> mark# X, mark# zero X -> zero# mark X)
      (mark# zero X -> mark# X, mark# zero X -> mark# X)
      (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# fact X -> mark# X, mark# false() -> active# false())
      (mark# fact X -> mark# X, mark# true() -> active# true())
      (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# fact X -> mark# X, mark# p X -> active# p mark X)
      (mark# fact X -> mark# X, mark# p X -> p# mark X)
      (mark# fact X -> mark# X, mark# p X -> mark# X)
      (mark# fact X -> mark# X, mark# fact X -> active# fact mark X)
      (mark# fact X -> mark# X, mark# fact X -> fact# mark X)
      (mark# fact X -> mark# X, mark# fact X -> mark# X)
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# fact X -> mark# X, mark# 0() -> active# 0())
      (mark# fact X -> mark# X, mark# s X -> active# s mark X)
      (mark# fact X -> mark# X, mark# s X -> s# mark X)
      (mark# fact X -> mark# X, mark# s X -> mark# X)
      (mark# fact X -> mark# X, mark# zero X -> active# zero mark X)
      (mark# fact X -> mark# X, mark# zero X -> zero# mark X)
      (mark# fact X -> mark# X, mark# zero X -> mark# X)
      (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (zero# mark X -> zero# X, zero# active X -> zero# X)
      (zero# mark X -> zero# X, zero# mark X -> zero# X)
      (s# mark X -> s# X, s# active X -> s# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (fact# mark X -> fact# X, fact# active X -> fact# X)
      (fact# mark X -> fact# X, fact# mark X -> fact# X)
      (p# mark X -> p# X, p# active X -> p# X)
      (p# mark X -> p# X, p# mark X -> p# X)
      (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false())
      (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true())
      (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
      (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
      (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p mark X)
      (active# if(true(), X, Y) -> mark# X, mark# p X -> p# mark X)
      (active# if(true(), X, Y) -> mark# X, mark# p X -> mark# X)
      (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X)
      (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X)
      (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X)
      (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0())
      (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X)
      (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X)
      (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X)
      (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X)
      (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X)
      (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
      (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (active# fact X -> p# X, p# active X -> p# X)
      (active# fact X -> p# X, p# mark X -> p# X)
      (active# add(0(), X) -> mark# X, mark# false() -> active# false())
      (active# add(0(), X) -> mark# X, mark# true() -> active# true())
      (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
      (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
      (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X)
      (active# add(0(), X) -> mark# X, mark# p X -> p# mark X)
      (active# add(0(), X) -> mark# X, mark# p X -> mark# X)
      (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X)
      (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X)
      (active# add(0(), X) -> mark# X, mark# fact X -> mark# X)
      (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
      (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X)
      (active# add(0(), X) -> mark# X, mark# s X -> s# mark X)
      (active# add(0(), X) -> mark# X, mark# s X -> mark# X)
      (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X)
      (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X)
      (active# add(0(), X) -> mark# X, mark# zero X -> mark# X)
      (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# zero X -> active# zero mark X, active# add(0(), X) -> mark# X)
      (mark# zero X -> active# zero mark X, active# add(s X, Y) -> add#(X, Y))
      (mark# zero X -> active# zero mark X, active# add(s X, Y) -> s# add(X, Y))
      (mark# zero X -> active# zero mark X, active# add(s X, Y) -> mark# s add(X, Y))
      (mark# zero X -> active# zero mark X, active# p s X -> mark# X)
      (mark# zero X -> active# zero mark X, active# fact X -> p# X)
      (mark# zero X -> active# zero mark X, active# fact X -> fact# p X)
      (mark# zero X -> active# zero mark X, active# fact X -> prod#(X, fact p X))
      (mark# zero X -> active# zero mark X, active# fact X -> s# 0())
      (mark# zero X -> active# zero mark X, active# fact X -> zero# X)
      (mark# zero X -> active# zero mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# zero X -> active# zero mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# zero X -> active# zero mark X, active# prod(0(), X) -> mark# 0())
      (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> prod#(X, Y))
      (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true())
      (mark# zero X -> active# zero mark X, active# zero s X -> mark# false())
      (mark# zero X -> active# zero mark X, active# if(false(), X, Y) -> mark# Y)
      (mark# zero X -> active# zero mark X, active# if(true(), X, Y) -> mark# X)
      (mark# fact X -> active# fact mark X, active# add(0(), X) -> mark# X)
      (mark# fact X -> active# fact mark X, active# add(s X, Y) -> add#(X, Y))
      (mark# fact X -> active# fact mark X, active# add(s X, Y) -> s# add(X, Y))
      (mark# fact X -> active# fact mark X, active# add(s X, Y) -> mark# s add(X, Y))
      (mark# fact X -> active# fact mark X, active# p s X -> mark# X)
      (mark# fact X -> active# fact mark X, active# fact X -> p# X)
      (mark# fact X -> active# fact mark X, active# fact X -> fact# p X)
      (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X))
      (mark# fact X -> active# fact mark X, active# fact X -> s# 0())
      (mark# fact X -> active# fact mark X, active# fact X -> zero# X)
      (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# fact X -> active# fact mark X, active# prod(0(), X) -> mark# 0())
      (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> prod#(X, Y))
      (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# fact X -> active# fact mark X, active# zero 0() -> mark# true())
      (mark# fact X -> active# fact mark X, active# zero s X -> mark# false())
      (mark# fact X -> active# fact mark X, active# if(false(), X, Y) -> mark# Y)
      (mark# fact X -> active# fact mark X, active# if(true(), X, Y) -> mark# X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# false() -> active# false())
      (active# add(s X, Y) -> mark# s add(X, Y), mark# true() -> active# true())
      (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X2)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> active# p mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> p# mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> mark# X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> active# fact mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> fact# mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> mark# X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X2)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X1)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# 0() -> active# 0())
      (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> active# zero mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> zero# mark X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> mark# X)
      (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> mark# X1)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# p s X -> mark# X)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> p# X)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> fact# p X)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> prod#(X, fact p X))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> s# 0())
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> zero# X)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(0(), X) -> mark# 0())
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero 0() -> mark# true())
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero s X -> mark# false())
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y)
      (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(true(), X, Y) -> mark# X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# false() -> active# false())
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# true() -> active# true())
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X2)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X1)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> active# p mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> p# mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> mark# X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> active# fact mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> fact# mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> mark# X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X2)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X1)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# 0() -> active# 0())
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> active# s mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> s# mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> mark# X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> active# zero mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> zero# mark X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> mark# X)
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1)
      (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2))
      (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2))
      (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2))
      (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
      (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false())
      (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true())
      (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> 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 -> active# fact mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> 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) -> active# prod(mark X1, mark X2))
      (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> 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# 0() -> active# 0())
      (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
      (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
      (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false())
      (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true())
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
      (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X)
      (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
      (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
      (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
      (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
      (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
      (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
      (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
      (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
      (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
      (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
      (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
      (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
      (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
      (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
      (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
      (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
      (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
      (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
      (active# zero 0() -> mark# true(), mark# true() -> active# true())
      (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false())
      (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true())
      (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
      (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X)
      (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X)
      (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
      (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X)
      (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X)
      (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> 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# 0() -> active# 0())
      (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
      (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
      (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X)
      (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
      (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X)
      (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# false() -> active# false())
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# true() -> active# true())
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> active# p mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> p# mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> mark# X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> active# fact mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> fact# mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> mark# X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X2)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X1)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# 0() -> active# 0())
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> active# s mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> s# mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> mark# X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> active# zero mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> zero# mark X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> mark# X)
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> mark# X1)
      (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
      (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2))
      (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2))
      (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2))
      (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2))
      (active# fact X -> prod#(X, fact p X), prod#(X1, mark X2) -> prod#(X1, X2))
      (active# fact X -> prod#(X, fact p X), prod#(X1, active X2) -> prod#(X1, X2))
      (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2))
      (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2))
      (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
      (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X)
      (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (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) -> prod#(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X)
      (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X)
      (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true())
      (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false())
      (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0())
      (active# zero s X -> mark# false(), mark# false() -> active# false())
      (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
      (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
      (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
      (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
      (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
      (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
      (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
      (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
      (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
      (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
      (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
      (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X)
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y)
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero s X -> mark# false())
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero 0() -> mark# true())
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> prod#(X, Y))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(0(), X) -> mark# 0())
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> zero# X)
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> s# 0())
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> prod#(X, fact p X))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> fact# p X)
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> p# X)
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# p s X -> mark# X)
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> mark# s add(X, Y))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> s# add(X, Y))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> add#(X, Y))
      (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(0(), X) -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
      (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (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) -> prod#(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
      (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X)
      (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true())
      (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false())
      (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
      (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2))
      (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2))
      (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
      (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# if(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
      (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
      (active# if(false(), X, Y) -> mark# Y, mark# s X -> s# mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0())
      (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
      (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
      (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
      (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# p X -> mark# X)
      (active# if(false(), X, Y) -> mark# Y, mark# p X -> p# mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# p X -> active# p mark X)
      (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
      (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
      (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true())
      (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false())
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(true(), X, Y) -> mark# X)
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y)
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero s X -> mark# false())
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero 0() -> mark# true())
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0())
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> zero# X)
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> s# 0())
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> prod#(X, fact p X))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> fact# p X)
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> p# X)
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# p s X -> mark# X)
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
      (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(0(), X) -> mark# X)
      (mark# p X -> active# p mark X, active# if(true(), X, Y) -> mark# X)
      (mark# p X -> active# p mark X, active# if(false(), X, Y) -> mark# Y)
      (mark# p X -> active# p mark X, active# zero s X -> mark# false())
      (mark# p X -> active# p mark X, active# zero 0() -> mark# true())
      (mark# p X -> active# p mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# p X -> active# p mark X, active# prod(s X, Y) -> prod#(X, Y))
      (mark# p X -> active# p mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# p X -> active# p mark X, active# prod(0(), X) -> mark# 0())
      (mark# p X -> active# p mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# p X -> active# p mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# p X -> active# p mark X, active# fact X -> zero# X)
      (mark# p X -> active# p mark X, active# fact X -> s# 0())
      (mark# p X -> active# p mark X, active# fact X -> prod#(X, fact p X))
      (mark# p X -> active# p mark X, active# fact X -> fact# p X)
      (mark# p X -> active# p mark X, active# fact X -> p# X)
      (mark# p X -> active# p mark X, active# p s X -> mark# X)
      (mark# p X -> active# p mark X, active# add(s X, Y) -> mark# s add(X, Y))
      (mark# p X -> active# p mark X, active# add(s X, Y) -> s# add(X, Y))
      (mark# p X -> active# p mark X, active# add(s X, Y) -> add#(X, Y))
      (mark# p X -> active# p mark X, active# add(0(), X) -> mark# X)
      (mark# s X -> active# s mark X, active# if(true(), X, Y) -> mark# X)
      (mark# s X -> active# s mark X, active# if(false(), X, Y) -> mark# Y)
      (mark# s X -> active# s mark X, active# zero s X -> mark# false())
      (mark# s X -> active# s mark X, active# zero 0() -> mark# true())
      (mark# s X -> active# s mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
      (mark# s X -> active# s mark X, active# prod(s X, Y) -> prod#(X, Y))
      (mark# s X -> active# s mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (mark# s X -> active# s mark X, active# prod(0(), X) -> mark# 0())
      (mark# s X -> active# s mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
      (mark# s X -> active# s mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (mark# s X -> active# s mark X, active# fact X -> zero# X)
      (mark# s X -> active# s mark X, active# fact X -> s# 0())
      (mark# s X -> active# s mark X, active# fact X -> prod#(X, fact p X))
      (mark# s X -> active# s mark X, active# fact X -> fact# p X)
      (mark# s X -> active# s mark X, active# fact X -> p# X)
      (mark# s X -> active# s mark X, active# p s X -> mark# X)
      (mark# s X -> active# s mark X, active# add(s X, Y) -> mark# s add(X, Y))
      (mark# s X -> active# s mark X, active# add(s X, Y) -> s# add(X, Y))
      (mark# s X -> active# s mark X, active# add(s X, Y) -> add#(X, Y))
      (mark# s X -> active# s mark X, active# add(0(), X) -> mark# X)
      (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, mark X2) -> add#(X1, X2))
      (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, active X2) -> add#(X1, X2))
      (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2))
      (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2))
      (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (active# p s X -> mark# X, mark# zero X -> mark# X)
      (active# p s X -> mark# X, mark# zero X -> zero# mark X)
      (active# p s X -> mark# X, mark# zero X -> active# zero mark X)
      (active# p s X -> mark# X, mark# s X -> mark# X)
      (active# p s X -> mark# X, mark# s X -> s# mark X)
      (active# p s X -> mark# X, mark# s X -> active# s mark X)
      (active# p s X -> mark# X, mark# 0() -> active# 0())
      (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (active# p s X -> mark# X, mark# fact X -> mark# X)
      (active# p s X -> mark# X, mark# fact X -> fact# mark X)
      (active# p s X -> mark# X, mark# fact X -> active# fact mark X)
      (active# p s X -> mark# X, mark# p X -> mark# X)
      (active# p s X -> mark# X, mark# p X -> p# mark X)
      (active# p s X -> mark# X, mark# p X -> active# p mark X)
      (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (active# p s X -> mark# X, mark# true() -> active# true())
      (active# p s X -> mark# X, mark# false() -> active# false())
      (active# fact X -> zero# X, zero# mark X -> zero# X)
      (active# fact X -> zero# X, zero# active X -> zero# X)
      (p# active X -> p# X, p# mark X -> p# X)
      (p# active X -> p# X, p# active X -> p# X)
      (fact# active X -> fact# X, fact# mark X -> fact# X)
      (fact# active X -> fact# X, fact# active X -> fact# X)
      (s# active X -> s# X, s# mark X -> s# X)
      (s# active X -> s# X, s# active X -> s# X)
      (zero# active X -> zero# X, zero# mark X -> zero# X)
      (zero# active X -> zero# X, zero# active X -> zero# X)
      (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# p X -> mark# X, mark# zero X -> mark# X)
      (mark# p X -> mark# X, mark# zero X -> zero# mark X)
      (mark# p X -> mark# X, mark# zero X -> active# zero mark X)
      (mark# p X -> mark# X, mark# s X -> mark# X)
      (mark# p X -> mark# X, mark# s X -> s# mark X)
      (mark# p X -> mark# X, mark# s X -> active# s mark X)
      (mark# p X -> mark# X, mark# 0() -> active# 0())
      (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (mark# p X -> mark# X, mark# fact X -> mark# X)
      (mark# p X -> mark# X, mark# fact X -> fact# mark X)
      (mark# p X -> mark# X, mark# fact X -> active# fact mark X)
      (mark# p X -> mark# X, mark# p X -> mark# X)
      (mark# p X -> mark# X, mark# p X -> p# mark X)
      (mark# p X -> mark# X, mark# p X -> active# p mark X)
      (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# p X -> mark# X, mark# true() -> active# true())
      (mark# p X -> mark# X, mark# false() -> active# false())
      (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
      (mark# s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
      (mark# s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
      (mark# s X -> mark# X, mark# zero X -> mark# X)
      (mark# s X -> mark# X, mark# zero X -> zero# mark X)
      (mark# s X -> mark# X, mark# zero X -> active# zero mark X)
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# s X -> s# mark X)
      (mark# s X -> mark# X, mark# s X -> active# s mark X)
      (mark# s X -> mark# X, mark# 0() -> active# 0())
      (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
      (mark# s X -> mark# X, mark# fact X -> mark# X)
      (mark# s X -> mark# X, mark# fact X -> fact# mark X)
      (mark# s X -> mark# X, mark# fact X -> active# fact mark X)
      (mark# s X -> mark# X, mark# p X -> mark# X)
      (mark# s X -> mark# X, mark# p X -> p# mark X)
      (mark# s X -> mark# X, mark# p X -> active# p mark X)
      (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
      (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# true() -> active# true())
      (mark# s X -> mark# X, mark# false() -> active# false())
      (active# fact X -> fact# p X, fact# mark X -> fact# X)
      (active# fact X -> fact# p X, fact# active X -> fact# X)
      (mark# fact X -> fact# mark X, fact# mark X -> fact# X)
      (mark# fact X -> fact# mark X, fact# active X -> fact# X)
      (mark# zero X -> zero# mark X, zero# mark X -> zero# X)
      (mark# zero X -> zero# mark X, zero# active X -> zero# X)
     }
     EDG:
      {
       (mark# s X -> s# mark X, s# active X -> s# X)
       (mark# s X -> s# mark X, s# mark X -> s# X)
       (mark# p X -> p# mark X, p# active X -> p# X)
       (mark# p X -> p# mark X, p# mark X -> p# X)
       (mark# zero X -> mark# X, mark# false() -> active# false())
       (mark# zero X -> mark# X, mark# true() -> active# true())
       (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# zero X -> mark# X, mark# p X -> active# p mark X)
       (mark# zero X -> mark# X, mark# p X -> p# mark X)
       (mark# zero X -> mark# X, mark# p X -> mark# X)
       (mark# zero X -> mark# X, mark# fact X -> active# fact mark X)
       (mark# zero X -> mark# X, mark# fact X -> fact# mark X)
       (mark# zero X -> mark# X, mark# fact X -> mark# X)
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# zero X -> mark# X, mark# 0() -> active# 0())
       (mark# zero X -> mark# X, mark# s X -> active# s mark X)
       (mark# zero X -> mark# X, mark# s X -> s# mark X)
       (mark# zero X -> mark# X, mark# s X -> mark# X)
       (mark# zero X -> mark# X, mark# zero X -> active# zero mark X)
       (mark# zero X -> mark# X, mark# zero X -> zero# mark X)
       (mark# zero X -> mark# X, mark# zero X -> mark# X)
       (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# fact X -> mark# X, mark# false() -> active# false())
       (mark# fact X -> mark# X, mark# true() -> active# true())
       (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# fact X -> mark# X, mark# p X -> active# p mark X)
       (mark# fact X -> mark# X, mark# p X -> p# mark X)
       (mark# fact X -> mark# X, mark# p X -> mark# X)
       (mark# fact X -> mark# X, mark# fact X -> active# fact mark X)
       (mark# fact X -> mark# X, mark# fact X -> fact# mark X)
       (mark# fact X -> mark# X, mark# fact X -> mark# X)
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# fact X -> mark# X, mark# 0() -> active# 0())
       (mark# fact X -> mark# X, mark# s X -> active# s mark X)
       (mark# fact X -> mark# X, mark# s X -> s# mark X)
       (mark# fact X -> mark# X, mark# s X -> mark# X)
       (mark# fact X -> mark# X, mark# zero X -> active# zero mark X)
       (mark# fact X -> mark# X, mark# zero X -> zero# mark X)
       (mark# fact X -> mark# X, mark# zero X -> mark# X)
       (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (zero# mark X -> zero# X, zero# active X -> zero# X)
       (zero# mark X -> zero# X, zero# mark X -> zero# X)
       (s# mark X -> s# X, s# active X -> s# X)
       (s# mark X -> s# X, s# mark X -> s# X)
       (fact# mark X -> fact# X, fact# active X -> fact# X)
       (fact# mark X -> fact# X, fact# mark X -> fact# X)
       (p# mark X -> p# X, p# active X -> p# X)
       (p# mark X -> p# X, p# mark X -> p# X)
       (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false())
       (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true())
       (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
       (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
       (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p mark X)
       (active# if(true(), X, Y) -> mark# X, mark# p X -> p# mark X)
       (active# if(true(), X, Y) -> mark# X, mark# p X -> mark# X)
       (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X)
       (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X)
       (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X)
       (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0())
       (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X)
       (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X)
       (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X)
       (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X)
       (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X)
       (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
       (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (active# fact X -> p# X, p# active X -> p# X)
       (active# fact X -> p# X, p# mark X -> p# X)
       (active# add(0(), X) -> mark# X, mark# false() -> active# false())
       (active# add(0(), X) -> mark# X, mark# true() -> active# true())
       (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
       (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
       (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X)
       (active# add(0(), X) -> mark# X, mark# p X -> p# mark X)
       (active# add(0(), X) -> mark# X, mark# p X -> mark# X)
       (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X)
       (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X)
       (active# add(0(), X) -> mark# X, mark# fact X -> mark# X)
       (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
       (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X)
       (active# add(0(), X) -> mark# X, mark# s X -> s# mark X)
       (active# add(0(), X) -> mark# X, mark# s X -> mark# X)
       (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X)
       (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X)
       (active# add(0(), X) -> mark# X, mark# zero X -> mark# X)
       (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true())
       (mark# zero X -> active# zero mark X, active# zero s X -> mark# false())
       (mark# fact X -> active# fact mark X, active# fact X -> p# X)
       (mark# fact X -> active# fact mark X, active# fact X -> fact# p X)
       (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X))
       (mark# fact X -> active# fact mark X, active# fact X -> s# 0())
       (mark# fact X -> active# fact mark X, active# fact X -> zero# X)
       (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
       (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
       (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X)
       (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X)
       (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X)
       (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X)
       (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
       (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
       (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
       (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1)
       (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2))
       (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2))
       (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2))
       (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
       (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false())
       (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true())
       (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> 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 -> active# fact mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> 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) -> active# prod(mark X1, mark X2))
       (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> 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# 0() -> active# 0())
       (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
       (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
       (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false())
       (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true())
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
       (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
       (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X)
       (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
       (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
       (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
       (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
       (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
       (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
       (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
       (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
       (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
       (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
       (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
       (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
       (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
       (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
       (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
       (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
       (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
       (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
       (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
       (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
       (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
       (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
       (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
       (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
       (active# zero 0() -> mark# true(), mark# true() -> active# true())
       (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false())
       (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true())
       (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
       (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X)
       (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X)
       (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
       (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X)
       (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X)
       (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> 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# 0() -> active# 0())
       (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
       (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
       (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
       (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
       (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
       (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X)
       (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
       (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2))
       (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2)
       (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1)
       (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
       (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
       (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2))
       (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
       (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2))
       (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2))
       (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2))
       (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2))
       (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2))
       (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2))
       (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
       (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X)
       (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X)
       (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0())
       (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) -> prod#(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X)
       (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X)
       (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true())
       (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false())
       (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0())
       (active# zero s X -> mark# false(), mark# false() -> active# false())
       (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
       (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
       (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
       (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
       (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
       (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
       (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
       (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
       (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
       (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
       (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
       (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
       (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
       (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
       (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
       (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
       (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X)
       (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y)
       (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
       (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (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) -> prod#(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
       (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X)
       (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true())
       (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false())
       (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
       (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
       (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2))
       (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2))
       (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2))
       (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2))
       (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
       (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (active# if(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
       (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
       (active# if(false(), X, Y) -> mark# Y, mark# s X -> s# mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0())
       (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
       (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
       (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
       (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# p X -> mark# X)
       (active# if(false(), X, Y) -> mark# Y, mark# p X -> p# mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# p X -> active# p mark X)
       (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
       (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
       (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true())
       (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false())
       (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
       (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y))
       (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
       (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0())
       (mark# p X -> active# p mark X, active# p s X -> mark# X)
       (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2))
       (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2))
       (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (active# p s X -> mark# X, mark# zero X -> mark# X)
       (active# p s X -> mark# X, mark# zero X -> zero# mark X)
       (active# p s X -> mark# X, mark# zero X -> active# zero mark X)
       (active# p s X -> mark# X, mark# s X -> mark# X)
       (active# p s X -> mark# X, mark# s X -> s# mark X)
       (active# p s X -> mark# X, mark# s X -> active# s mark X)
       (active# p s X -> mark# X, mark# 0() -> active# 0())
       (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (active# p s X -> mark# X, mark# fact X -> mark# X)
       (active# p s X -> mark# X, mark# fact X -> fact# mark X)
       (active# p s X -> mark# X, mark# fact X -> active# fact mark X)
       (active# p s X -> mark# X, mark# p X -> mark# X)
       (active# p s X -> mark# X, mark# p X -> p# mark X)
       (active# p s X -> mark# X, mark# p X -> active# p mark X)
       (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (active# p s X -> mark# X, mark# true() -> active# true())
       (active# p s X -> mark# X, mark# false() -> active# false())
       (active# fact X -> zero# X, zero# mark X -> zero# X)
       (active# fact X -> zero# X, zero# active X -> zero# X)
       (p# active X -> p# X, p# mark X -> p# X)
       (p# active X -> p# X, p# active X -> p# X)
       (fact# active X -> fact# X, fact# mark X -> fact# X)
       (fact# active X -> fact# X, fact# active X -> fact# X)
       (s# active X -> s# X, s# mark X -> s# X)
       (s# active X -> s# X, s# active X -> s# X)
       (zero# active X -> zero# X, zero# mark X -> zero# X)
       (zero# active X -> zero# X, zero# active X -> zero# X)
       (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# p X -> mark# X, mark# zero X -> mark# X)
       (mark# p X -> mark# X, mark# zero X -> zero# mark X)
       (mark# p X -> mark# X, mark# zero X -> active# zero mark X)
       (mark# p X -> mark# X, mark# s X -> mark# X)
       (mark# p X -> mark# X, mark# s X -> s# mark X)
       (mark# p X -> mark# X, mark# s X -> active# s mark X)
       (mark# p X -> mark# X, mark# 0() -> active# 0())
       (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (mark# p X -> mark# X, mark# fact X -> mark# X)
       (mark# p X -> mark# X, mark# fact X -> fact# mark X)
       (mark# p X -> mark# X, mark# fact X -> active# fact mark X)
       (mark# p X -> mark# X, mark# p X -> mark# X)
       (mark# p X -> mark# X, mark# p X -> p# mark X)
       (mark# p X -> mark# X, mark# p X -> active# p mark X)
       (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# p X -> mark# X, mark# true() -> active# true())
       (mark# p X -> mark# X, mark# false() -> active# false())
       (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
       (mark# s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
       (mark# s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
       (mark# s X -> mark# X, mark# zero X -> mark# X)
       (mark# s X -> mark# X, mark# zero X -> zero# mark X)
       (mark# s X -> mark# X, mark# zero X -> active# zero mark X)
       (mark# s X -> mark# X, mark# s X -> mark# X)
       (mark# s X -> mark# X, mark# s X -> s# mark X)
       (mark# s X -> mark# X, mark# s X -> active# s mark X)
       (mark# s X -> mark# X, mark# 0() -> active# 0())
       (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
       (mark# s X -> mark# X, mark# fact X -> mark# X)
       (mark# s X -> mark# X, mark# fact X -> fact# mark X)
       (mark# s X -> mark# X, mark# fact X -> active# fact mark X)
       (mark# s X -> mark# X, mark# p X -> mark# X)
       (mark# s X -> mark# X, mark# p X -> p# mark X)
       (mark# s X -> mark# X, mark# p X -> active# p mark X)
       (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
       (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# true() -> active# true())
       (mark# s X -> mark# X, mark# false() -> active# false())
       (mark# fact X -> fact# mark X, fact# mark X -> fact# X)
       (mark# fact X -> fact# mark X, fact# active X -> fact# X)
       (mark# zero X -> zero# mark X, zero# mark X -> zero# X)
       (mark# zero X -> zero# mark X, zero# active X -> zero# X)
      }
      EDG:
       {
        (mark# s X -> s# mark X, s# active X -> s# X)
        (mark# s X -> s# mark X, s# mark X -> s# X)
        (mark# p X -> p# mark X, p# active X -> p# X)
        (mark# p X -> p# mark X, p# mark X -> p# X)
        (mark# zero X -> mark# X, mark# false() -> active# false())
        (mark# zero X -> mark# X, mark# true() -> active# true())
        (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# zero X -> mark# X, mark# p X -> active# p mark X)
        (mark# zero X -> mark# X, mark# p X -> p# mark X)
        (mark# zero X -> mark# X, mark# p X -> mark# X)
        (mark# zero X -> mark# X, mark# fact X -> active# fact mark X)
        (mark# zero X -> mark# X, mark# fact X -> fact# mark X)
        (mark# zero X -> mark# X, mark# fact X -> mark# X)
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# zero X -> mark# X, mark# 0() -> active# 0())
        (mark# zero X -> mark# X, mark# s X -> active# s mark X)
        (mark# zero X -> mark# X, mark# s X -> s# mark X)
        (mark# zero X -> mark# X, mark# s X -> mark# X)
        (mark# zero X -> mark# X, mark# zero X -> active# zero mark X)
        (mark# zero X -> mark# X, mark# zero X -> zero# mark X)
        (mark# zero X -> mark# X, mark# zero X -> mark# X)
        (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# fact X -> mark# X, mark# false() -> active# false())
        (mark# fact X -> mark# X, mark# true() -> active# true())
        (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# fact X -> mark# X, mark# p X -> active# p mark X)
        (mark# fact X -> mark# X, mark# p X -> p# mark X)
        (mark# fact X -> mark# X, mark# p X -> mark# X)
        (mark# fact X -> mark# X, mark# fact X -> active# fact mark X)
        (mark# fact X -> mark# X, mark# fact X -> fact# mark X)
        (mark# fact X -> mark# X, mark# fact X -> mark# X)
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# fact X -> mark# X, mark# 0() -> active# 0())
        (mark# fact X -> mark# X, mark# s X -> active# s mark X)
        (mark# fact X -> mark# X, mark# s X -> s# mark X)
        (mark# fact X -> mark# X, mark# s X -> mark# X)
        (mark# fact X -> mark# X, mark# zero X -> active# zero mark X)
        (mark# fact X -> mark# X, mark# zero X -> zero# mark X)
        (mark# fact X -> mark# X, mark# zero X -> mark# X)
        (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (zero# mark X -> zero# X, zero# active X -> zero# X)
        (zero# mark X -> zero# X, zero# mark X -> zero# X)
        (s# mark X -> s# X, s# active X -> s# X)
        (s# mark X -> s# X, s# mark X -> s# X)
        (fact# mark X -> fact# X, fact# active X -> fact# X)
        (fact# mark X -> fact# X, fact# mark X -> fact# X)
        (p# mark X -> p# X, p# active X -> p# X)
        (p# mark X -> p# X, p# mark X -> p# X)
        (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false())
        (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true())
        (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2)
        (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1)
        (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p mark X)
        (active# if(true(), X, Y) -> mark# X, mark# p X -> p# mark X)
        (active# if(true(), X, Y) -> mark# X, mark# p X -> mark# X)
        (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X)
        (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X)
        (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X)
        (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0())
        (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X)
        (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X)
        (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X)
        (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X)
        (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X)
        (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X)
        (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (active# fact X -> p# X, p# active X -> p# X)
        (active# fact X -> p# X, p# mark X -> p# X)
        (active# add(0(), X) -> mark# X, mark# false() -> active# false())
        (active# add(0(), X) -> mark# X, mark# true() -> active# true())
        (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
        (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
        (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X)
        (active# add(0(), X) -> mark# X, mark# p X -> p# mark X)
        (active# add(0(), X) -> mark# X, mark# p X -> mark# X)
        (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X)
        (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X)
        (active# add(0(), X) -> mark# X, mark# fact X -> mark# X)
        (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
        (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X)
        (active# add(0(), X) -> mark# X, mark# s X -> s# mark X)
        (active# add(0(), X) -> mark# X, mark# s X -> mark# X)
        (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X)
        (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X)
        (active# add(0(), X) -> mark# X, mark# zero X -> mark# X)
        (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true())
        (mark# zero X -> active# zero mark X, active# zero s X -> mark# false())
        (mark# fact X -> active# fact mark X, active# fact X -> p# X)
        (mark# fact X -> active# fact mark X, active# fact X -> fact# p X)
        (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X))
        (mark# fact X -> active# fact mark X, active# fact X -> s# 0())
        (mark# fact X -> active# fact mark X, active# fact X -> zero# X)
        (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
        (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)))
        (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X)
        (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X)
        (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X)
        (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X)
        (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
        (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
        (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
        (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1)
        (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2))
        (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2))
        (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2))
        (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
        (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false())
        (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true())
        (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> 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 -> active# fact mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> 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) -> active# prod(mark X1, mark X2))
        (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> 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# 0() -> active# 0())
        (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X)
        (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
        (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false())
        (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true())
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
        (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
        (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X)
        (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
        (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2)
        (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1)
        (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
        (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
        (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
        (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X)
        (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
        (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
        (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
        (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
        (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
        (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
        (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
        (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
        (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
        (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
        (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
        (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
        (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
        (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
        (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
        (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
        (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
        (active# zero 0() -> mark# true(), mark# true() -> active# true())
        (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false())
        (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true())
        (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# 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# p X -> active# p mark X)
        (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X)
        (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X)
        (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
        (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X)
        (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X)
        (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> 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# 0() -> active# 0())
        (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
        (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
        (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
        (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
        (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
        (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X)
        (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
        (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2))
        (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2)
        (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1)
        (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
        (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
        (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2))
        (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
        (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2))
        (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2))
        (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2))
        (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2))
        (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2))
        (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2))
        (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
        (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X)
        (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X)
        (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0())
        (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) -> prod#(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X)
        (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X)
        (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true())
        (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false())
        (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0())
        (active# zero s X -> mark# false(), mark# false() -> active# false())
        (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
        (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
        (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
        (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
        (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
        (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
        (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
        (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
        (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
        (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
        (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
        (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
        (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
        (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2))
        (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
        (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2))
        (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X)
        (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y)
        (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
        (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (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) -> prod#(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# 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 -> fact# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X)
        (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X)
        (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p 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) -> active# add(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true())
        (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false())
        (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
        (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3))
        (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2))
        (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2))
        (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2))
        (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2))
        (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
        (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (active# if(false(), X, Y) -> mark# Y, mark# zero X -> mark# X)
        (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
        (active# if(false(), X, Y) -> mark# Y, mark# s X -> s# mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0())
        (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1)
        (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2)
        (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X)
        (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# p X -> mark# X)
        (active# if(false(), X, Y) -> mark# Y, mark# p X -> p# mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# p X -> active# p mark X)
        (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1)
        (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2)
        (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true())
        (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false())
        (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)))
        (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y))
        (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y)))
        (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0())
        (mark# p X -> active# p mark X, active# p s X -> mark# X)
        (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2))
        (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2))
        (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (active# p s X -> mark# X, mark# zero X -> mark# X)
        (active# p s X -> mark# X, mark# zero X -> zero# mark X)
        (active# p s X -> mark# X, mark# zero X -> active# zero mark X)
        (active# p s X -> mark# X, mark# s X -> mark# X)
        (active# p s X -> mark# X, mark# s X -> s# mark X)
        (active# p s X -> mark# X, mark# s X -> active# s mark X)
        (active# p s X -> mark# X, mark# 0() -> active# 0())
        (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (active# p s X -> mark# X, mark# fact X -> mark# X)
        (active# p s X -> mark# X, mark# fact X -> fact# mark X)
        (active# p s X -> mark# X, mark# fact X -> active# fact mark X)
        (active# p s X -> mark# X, mark# p X -> mark# X)
        (active# p s X -> mark# X, mark# p X -> p# mark X)
        (active# p s X -> mark# X, mark# p X -> active# p mark X)
        (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (active# p s X -> mark# X, mark# true() -> active# true())
        (active# p s X -> mark# X, mark# false() -> active# false())
        (active# fact X -> zero# X, zero# mark X -> zero# X)
        (active# fact X -> zero# X, zero# active X -> zero# X)
        (p# active X -> p# X, p# mark X -> p# X)
        (p# active X -> p# X, p# active X -> p# X)
        (fact# active X -> fact# X, fact# mark X -> fact# X)
        (fact# active X -> fact# X, fact# active X -> fact# X)
        (s# active X -> s# X, s# mark X -> s# X)
        (s# active X -> s# X, s# active X -> s# X)
        (zero# active X -> zero# X, zero# mark X -> zero# X)
        (zero# active X -> zero# X, zero# active X -> zero# X)
        (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# p X -> mark# X, mark# zero X -> mark# X)
        (mark# p X -> mark# X, mark# zero X -> zero# mark X)
        (mark# p X -> mark# X, mark# zero X -> active# zero mark X)
        (mark# p X -> mark# X, mark# s X -> mark# X)
        (mark# p X -> mark# X, mark# s X -> s# mark X)
        (mark# p X -> mark# X, mark# s X -> active# s mark X)
        (mark# p X -> mark# X, mark# 0() -> active# 0())
        (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (mark# p X -> mark# X, mark# fact X -> mark# X)
        (mark# p X -> mark# X, mark# fact X -> fact# mark X)
        (mark# p X -> mark# X, mark# fact X -> active# fact mark X)
        (mark# p X -> mark# X, mark# p X -> mark# X)
        (mark# p X -> mark# X, mark# p X -> p# mark X)
        (mark# p X -> mark# X, mark# p X -> active# p mark X)
        (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# p X -> mark# X, mark# true() -> active# true())
        (mark# p X -> mark# X, mark# false() -> active# false())
        (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
        (mark# s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3))
        (mark# s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3))
        (mark# s X -> mark# X, mark# zero X -> mark# X)
        (mark# s X -> mark# X, mark# zero X -> zero# mark X)
        (mark# s X -> mark# X, mark# zero X -> active# zero mark X)
        (mark# s X -> mark# X, mark# s X -> mark# X)
        (mark# s X -> mark# X, mark# s X -> s# mark X)
        (mark# s X -> mark# X, mark# s X -> active# s mark X)
        (mark# s X -> mark# X, mark# 0() -> active# 0())
        (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2))
        (mark# s X -> mark# X, mark# fact X -> mark# X)
        (mark# s X -> mark# X, mark# fact X -> fact# mark X)
        (mark# s X -> mark# X, mark# fact X -> active# fact mark X)
        (mark# s X -> mark# X, mark# p X -> mark# X)
        (mark# s X -> mark# X, mark# p X -> p# mark X)
        (mark# s X -> mark# X, mark# p X -> active# p mark X)
        (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
        (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# true() -> active# true())
        (mark# s X -> mark# X, mark# false() -> active# false())
        (mark# fact X -> fact# mark X, fact# mark X -> fact# X)
        (mark# fact X -> fact# mark X, fact# active X -> fact# X)
        (mark# zero X -> zero# mark X, zero# mark X -> zero# X)
        (mark# zero X -> zero# mark X, zero# active X -> zero# X)
       }
       STATUS:
        arrows: 0.893382
        SCCS (8):
         Scc:
          {     mark# if(X1, X2, X3) -> mark# X1,
                mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3),
                        mark# zero X -> mark# X,
                           mark# s X -> mark# X,
                  mark# prod(X1, X2) -> mark# X1,
                  mark# prod(X1, X2) -> mark# X2,
                  mark# prod(X1, X2) -> active# prod(mark X1, mark X2),
                        mark# fact X -> mark# X,
                        mark# fact X -> active# fact mark X,
                           mark# p X -> mark# X,
                           mark# p X -> active# p mark X,
                   mark# add(X1, X2) -> mark# X1,
                   mark# add(X1, X2) -> mark# X2,
                   mark# add(X1, X2) -> active# add(mark X1, mark X2),
            active# if(true(), X, Y) -> mark# X,
           active# if(false(), X, Y) -> mark# Y,
                active# prod(s X, Y) -> mark# add(Y, prod(X, Y)),
                      active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)),
                       active# p s X -> mark# X,
                 active# add(s X, Y) -> mark# s add(X, Y),
                 active# add(0(), X) -> mark# X}
         Scc:
          {  add#(X1, mark X2) -> add#(X1, X2),
           add#(X1, active X2) -> add#(X1, X2),
             add#(mark X1, X2) -> add#(X1, X2),
           add#(active X1, X2) -> add#(X1, X2)}
         Scc:
          {  prod#(X1, mark X2) -> prod#(X1, X2),
           prod#(X1, active X2) -> prod#(X1, X2),
             prod#(mark X1, X2) -> prod#(X1, X2),
           prod#(active X1, X2) -> prod#(X1, X2)}
         Scc:
          {  if#(X1, X2, mark X3) -> if#(X1, X2, X3),
           if#(X1, X2, active X3) -> if#(X1, X2, X3),
             if#(X1, mark X2, X3) -> if#(X1, X2, X3),
           if#(X1, active X2, X3) -> if#(X1, X2, X3),
             if#(mark X1, X2, X3) -> if#(X1, X2, X3),
           if#(active X1, X2, X3) -> if#(X1, X2, X3)}
         Scc:
          {  p# mark X -> p# X,
           p# active X -> p# X}
         Scc:
          {  fact# mark X -> fact# X,
           fact# active X -> fact# X}
         Scc:
          {  s# mark X -> s# X,
           s# active X -> s# X}
         Scc:
          {  zero# mark X -> zero# X,
           zero# active X -> zero# X}
         
         SCC (21):
          Strict:
           {     mark# if(X1, X2, X3) -> mark# X1,
                 mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3),
                         mark# zero X -> mark# X,
                            mark# s X -> mark# X,
                   mark# prod(X1, X2) -> mark# X1,
                   mark# prod(X1, X2) -> mark# X2,
                   mark# prod(X1, X2) -> active# prod(mark X1, mark X2),
                         mark# fact X -> mark# X,
                         mark# fact X -> active# fact mark X,
                            mark# p X -> mark# X,
                            mark# p X -> active# p mark X,
                    mark# add(X1, X2) -> mark# X1,
                    mark# add(X1, X2) -> mark# X2,
                    mark# add(X1, X2) -> active# add(mark X1, mark X2),
             active# if(true(), X, Y) -> mark# X,
            active# if(false(), X, Y) -> mark# Y,
                 active# prod(s X, Y) -> mark# add(Y, prod(X, Y)),
                       active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)),
                        active# p s X -> mark# X,
                  active# add(s X, Y) -> mark# s add(X, Y),
                  active# add(0(), X) -> mark# X}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         
         
         
         
         SCC (4):
          Strict:
           {  add#(X1, mark X2) -> add#(X1, X2),
            add#(X1, active X2) -> add#(X1, X2),
              add#(mark X1, X2) -> add#(X1, X2),
            add#(active X1, X2) -> add#(X1, X2)}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         
         
         
         
         
         
         SCC (4):
          Strict:
           {  prod#(X1, mark X2) -> prod#(X1, X2),
            prod#(X1, active X2) -> prod#(X1, X2),
              prod#(mark X1, X2) -> prod#(X1, X2),
            prod#(active X1, X2) -> prod#(X1, X2)}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         
         
         
         
         
         
         
         SCC (6):
          Strict:
           {  if#(X1, X2, mark X3) -> if#(X1, X2, X3),
            if#(X1, X2, active X3) -> if#(X1, X2, X3),
              if#(X1, mark X2, X3) -> if#(X1, X2, X3),
            if#(X1, active X2, X3) -> if#(X1, X2, X3),
              if#(mark X1, X2, X3) -> if#(X1, X2, X3),
            if#(active X1, X2, X3) -> if#(X1, X2, X3)}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         
         SCC (2):
          Strict:
           {  p# mark X -> p# X,
            p# active X -> p# X}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         SCC (2):
          Strict:
           {  fact# mark X -> fact# X,
            fact# active X -> fact# X}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         SCC (2):
          Strict:
           {  s# mark X -> s# X,
            s# active X -> s# X}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open
         
         SCC (2):
          Strict:
           {  zero# mark X -> zero# X,
            zero# active X -> zero# X}
          Weak:
          {     mark if(X1, X2, X3) -> active if(mark X1, X2, X3),
                        mark zero X -> active zero mark X,
                           mark s X -> active s mark X,
                           mark 0() -> active 0(),
                  mark prod(X1, X2) -> active prod(mark X1, mark X2),
                        mark fact X -> active fact mark X,
                           mark p X -> active p mark X,
                   mark add(X1, X2) -> active add(mark X1, mark X2),
                        mark true() -> active true(),
                       mark false() -> active false(),
                if(X1, X2, mark X3) -> if(X1, X2, X3),
              if(X1, X2, active X3) -> if(X1, X2, X3),
                if(X1, mark X2, X3) -> if(X1, X2, X3),
              if(X1, active X2, X3) -> if(X1, X2, X3),
                if(mark X1, X2, X3) -> if(X1, X2, X3),
              if(active X1, X2, X3) -> if(X1, X2, X3),
                        zero mark X -> zero X,
                      zero active X -> zero X,
                           s mark X -> s X,
                         s active X -> s X,
                  prod(X1, mark X2) -> prod(X1, X2),
                prod(X1, active X2) -> prod(X1, X2),
                  prod(mark X1, X2) -> prod(X1, X2),
                prod(active X1, X2) -> prod(X1, X2),
                        fact mark X -> fact X,
                      fact active X -> fact X,
                           p mark X -> p X,
                         p active X -> p X,
            active if(true(), X, Y) -> mark X,
           active if(false(), X, Y) -> mark Y,
                    active zero s X -> mark false(),
                    active zero 0() -> mark true(),
                active prod(s X, Y) -> mark add(Y, prod(X, Y)),
                active prod(0(), X) -> mark 0(),
                      active fact X -> mark if(zero X, s 0(), prod(X, fact p X)),
                       active p s X -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                   add(X1, mark X2) -> add(X1, X2),
                 add(X1, active X2) -> add(X1, X2),
                   add(mark X1, X2) -> add(X1, X2),
                 add(active X1, X2) -> add(X1, X2)}
          Open