MAYBE
Time: 1.170563
TRS:
 {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
   if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
               zero mark X -> mark zero X,
                 zero ok X -> ok zero X,
                  s mark X -> mark s X,
                    s ok X -> ok s X,
         prod(X1, mark X2) -> mark prod(X1, X2),
         prod(mark X1, X2) -> mark prod(X1, X2),
        prod(ok X1, ok X2) -> ok prod(X1, X2),
               fact mark X -> mark fact X,
                 fact ok X -> ok fact X,
                  p mark X -> mark p X,
                    p ok X -> ok p X,
     active if(X1, X2, X3) -> if(active X1, X2, X3),
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
             active zero X -> zero active X,
           active zero s X -> mark false(),
           active zero 0() -> mark true(),
                active s X -> s active X,
       active prod(X1, X2) -> prod(X1, active X2),
       active prod(X1, X2) -> prod(active X1, X2),
       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 fact X -> fact active X,
                active p X -> p active X,
              active p s X -> mark X,
        active add(X1, X2) -> add(X1, active X2),
        active add(X1, X2) -> add(active X1, X2),
        active add(s X, Y) -> mark s add(X, Y),
        active add(0(), X) -> mark X,
          add(X1, mark X2) -> mark add(X1, X2),
          add(mark X1, X2) -> mark add(X1, X2),
         add(ok X1, ok X2) -> ok add(X1, X2),
     proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
             proper zero X -> zero proper X,
                proper s X -> s proper X,
                proper 0() -> ok 0(),
       proper prod(X1, X2) -> prod(proper X1, proper X2),
             proper fact X -> fact proper X,
                proper p X -> p proper X,
        proper add(X1, X2) -> add(proper X1, proper X2),
             proper true() -> ok true(),
            proper false() -> ok false(),
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
    if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3),
                zero# mark X -> zero# X,
                  zero# ok X -> zero# X,
                   s# mark X -> s# X,
                     s# ok X -> s# X,
          prod#(X1, mark X2) -> prod#(X1, X2),
          prod#(mark X1, X2) -> prod#(X1, X2),
         prod#(ok X1, ok X2) -> prod#(X1, X2),
                fact# mark X -> fact# X,
                  fact# ok X -> fact# X,
                   p# mark X -> p# X,
                     p# ok X -> p# X,
      active# if(X1, X2, X3) -> if#(active X1, X2, X3),
      active# if(X1, X2, X3) -> active# X1,
              active# zero X -> zero# active X,
              active# zero X -> active# X,
                 active# s X -> s# active X,
                 active# s X -> active# X,
        active# prod(X1, X2) -> prod#(X1, active X2),
        active# prod(X1, X2) -> prod#(active X1, X2),
        active# prod(X1, X2) -> active# X1,
        active# prod(X1, X2) -> active# X2,
        active# prod(s X, Y) -> prod#(X, Y),
        active# prod(s X, Y) -> add#(Y, prod(X, Y)),
              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 -> fact# active X,
              active# fact X -> p# X,
              active# fact X -> active# X,
                 active# p X -> p# active X,
                 active# p X -> active# X,
         active# add(X1, X2) -> active# X1,
         active# add(X1, X2) -> active# X2,
         active# add(X1, X2) -> add#(X1, active X2),
         active# add(X1, X2) -> add#(active X1, X2),
         active# add(s X, Y) -> s# add(X, Y),
         active# add(s X, Y) -> add#(X, Y),
           add#(X1, mark X2) -> add#(X1, X2),
           add#(mark X1, X2) -> add#(X1, X2),
          add#(ok X1, ok X2) -> add#(X1, X2),
      proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3),
      proper# if(X1, X2, X3) -> proper# X1,
      proper# if(X1, X2, X3) -> proper# X2,
      proper# if(X1, X2, X3) -> proper# X3,
              proper# zero X -> zero# proper X,
              proper# zero X -> proper# X,
                 proper# s X -> s# proper X,
                 proper# s X -> proper# X,
        proper# prod(X1, X2) -> prod#(proper X1, proper X2),
        proper# prod(X1, X2) -> proper# X1,
        proper# prod(X1, X2) -> proper# X2,
              proper# fact X -> fact# proper X,
              proper# fact X -> proper# X,
                 proper# p X -> p# proper X,
                 proper# p X -> proper# X,
         proper# add(X1, X2) -> add#(proper X1, proper X2),
         proper# add(X1, X2) -> proper# X1,
         proper# add(X1, X2) -> proper# X2,
                 top# mark X -> proper# X,
                 top# mark X -> top# proper X,
                   top# ok X -> active# X,
                   top# ok X -> top# active X}
  TRS:
  {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
    if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                zero mark X -> mark zero X,
                  zero ok X -> ok zero X,
                   s mark X -> mark s X,
                     s ok X -> ok s X,
          prod(X1, mark X2) -> mark prod(X1, X2),
          prod(mark X1, X2) -> mark prod(X1, X2),
         prod(ok X1, ok X2) -> ok prod(X1, X2),
                fact mark X -> mark fact X,
                  fact ok X -> ok fact X,
                   p mark X -> mark p X,
                     p ok X -> ok p X,
      active if(X1, X2, X3) -> if(active X1, X2, X3),
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
              active zero X -> zero active X,
            active zero s X -> mark false(),
            active zero 0() -> mark true(),
                 active s X -> s active X,
        active prod(X1, X2) -> prod(X1, active X2),
        active prod(X1, X2) -> prod(active X1, X2),
        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 fact X -> fact active X,
                 active p X -> p active X,
               active p s X -> mark X,
         active add(X1, X2) -> add(X1, active X2),
         active add(X1, X2) -> add(active X1, X2),
         active add(s X, Y) -> mark s add(X, Y),
         active add(0(), X) -> mark X,
           add(X1, mark X2) -> mark add(X1, X2),
           add(mark X1, X2) -> mark add(X1, X2),
          add(ok X1, ok X2) -> ok add(X1, X2),
      proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
              proper zero X -> zero proper X,
                 proper s X -> s proper X,
                 proper 0() -> ok 0(),
        proper prod(X1, X2) -> prod(proper X1, proper X2),
              proper fact X -> fact proper X,
                 proper p X -> p proper X,
         proper add(X1, X2) -> add(proper X1, proper X2),
              proper true() -> ok true(),
             proper false() -> ok false(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  UR:
   {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
     if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                 zero mark X -> mark zero X,
                   zero ok X -> ok zero X,
                    s mark X -> mark s X,
                      s ok X -> ok s X,
           prod(X1, mark X2) -> mark prod(X1, X2),
           prod(mark X1, X2) -> mark prod(X1, X2),
          prod(ok X1, ok X2) -> ok prod(X1, X2),
                 fact mark X -> mark fact X,
                   fact ok X -> ok fact X,
                    p mark X -> mark p X,
                      p ok X -> ok p X,
       active if(X1, X2, X3) -> if(active X1, X2, X3),
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
               active zero X -> zero active X,
             active zero s X -> mark false(),
             active zero 0() -> mark true(),
                  active s X -> s active X,
         active prod(X1, X2) -> prod(X1, active X2),
         active prod(X1, X2) -> prod(active X1, X2),
         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 fact X -> fact active X,
                  active p X -> p active X,
                active p s X -> mark X,
          active add(X1, X2) -> add(X1, active X2),
          active add(X1, X2) -> add(active X1, X2),
          active add(s X, Y) -> mark s add(X, Y),
          active add(0(), X) -> mark X,
            add(X1, mark X2) -> mark add(X1, X2),
            add(mark X1, X2) -> mark add(X1, X2),
           add(ok X1, ok X2) -> ok add(X1, X2),
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
               proper zero X -> zero proper X,
                  proper s X -> s proper X,
                  proper 0() -> ok 0(),
         proper prod(X1, X2) -> prod(proper X1, proper X2),
               proper fact X -> fact proper X,
                  proper p X -> p proper X,
          proper add(X1, X2) -> add(proper X1, proper X2),
               proper true() -> ok true(),
              proper false() -> ok false()}
   EDG:
    {
     (active# prod(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     (active# prod(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
     (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
     (active# prod(X1, X2) -> active# X1, active# p X -> active# X)
     (active# prod(X1, X2) -> active# X1, active# p X -> p# active X)
     (active# prod(X1, X2) -> active# X1, active# fact X -> active# X)
     (active# prod(X1, X2) -> active# X1, active# fact X -> p# X)
     (active# prod(X1, X2) -> active# X1, active# fact X -> fact# active X)
     (active# prod(X1, X2) -> active# X1, active# fact X -> fact# p X)
     (active# prod(X1, X2) -> active# X1, active# fact X -> prod#(X, fact p X))
     (active# prod(X1, X2) -> active# X1, active# fact X -> s# 0())
     (active# prod(X1, X2) -> active# X1, active# fact X -> zero# X)
     (active# prod(X1, X2) -> active# X1, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# prod(X1, X2) -> active# X1, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# prod(X1, X2) -> active# X1, active# prod(s X, Y) -> prod#(X, Y))
     (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X2)
     (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X1)
     (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# prod(X1, X2) -> active# X1, active# s X -> active# X)
     (active# prod(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# prod(X1, X2) -> active# X1, active# zero X -> active# X)
     (active# prod(X1, X2) -> active# X1, active# zero X -> zero# active X)
     (active# prod(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
     (active# prod(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (proper# if(X1, X2, X3) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X1, proper# p X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# p X -> p# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# fact X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# fact X -> fact# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# prod(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# prod(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# zero X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# zero X -> zero# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X1, proper# p X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# p X -> p# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# fact X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# fact X -> fact# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# zero X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# zero X -> zero# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (active# prod(s X, Y) -> prod#(X, Y), prod#(ok X1, ok 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#(X1, mark X2) -> prod#(X1, X2))
     (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(ok X1, ok 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#(X1, mark X2) -> add#(X1, X2))
     (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(ok X1, ok X2, ok 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 -> prod#(X, fact p X), prod#(ok X1, ok 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#(X1, mark X2) -> prod#(X1, X2))
     (active# add(X1, X2) -> add#(active X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(active X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(active X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (zero# ok X -> zero# X, zero# ok X -> zero# X)
     (zero# ok X -> zero# X, zero# mark X -> zero# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (fact# ok X -> fact# X, fact# ok X -> fact# X)
     (fact# ok X -> fact# X, fact# mark X -> fact# X)
     (p# ok X -> p# X, p# ok X -> p# X)
     (p# ok X -> p# X, p# mark X -> p# X)
     (active# s X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# s X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# s X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# s X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# s X -> active# X, active# add(X1, X2) -> active# X2)
     (active# s X -> active# X, active# add(X1, X2) -> active# X1)
     (active# s X -> active# X, active# p X -> active# X)
     (active# s X -> active# X, active# p X -> p# active X)
     (active# s X -> active# X, active# fact X -> active# X)
     (active# s X -> active# X, active# fact X -> p# X)
     (active# s X -> active# X, active# fact X -> fact# active X)
     (active# s X -> active# X, active# fact X -> fact# p X)
     (active# s X -> active# X, active# fact X -> prod#(X, fact p X))
     (active# s X -> active# X, active# fact X -> s# 0())
     (active# s X -> active# X, active# fact X -> zero# X)
     (active# s X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# s X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# s X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
     (active# s X -> active# X, active# prod(X1, X2) -> active# X2)
     (active# s X -> active# X, active# prod(X1, X2) -> active# X1)
     (active# s X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# s X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# zero X -> active# X)
     (active# s X -> active# X, active# zero X -> zero# active X)
     (active# s X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# fact X -> p# X, p# ok X -> p# X)
     (active# fact X -> p# X, p# mark X -> p# X)
     (active# p X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# p X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# p X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# p X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# p X -> active# X, active# add(X1, X2) -> active# X2)
     (active# p X -> active# X, active# add(X1, X2) -> active# X1)
     (active# p X -> active# X, active# p X -> active# X)
     (active# p X -> active# X, active# p X -> p# active X)
     (active# p X -> active# X, active# fact X -> active# X)
     (active# p X -> active# X, active# fact X -> p# X)
     (active# p X -> active# X, active# fact X -> fact# active X)
     (active# p X -> active# X, active# fact X -> fact# p X)
     (active# p X -> active# X, active# fact X -> prod#(X, fact p X))
     (active# p X -> active# X, active# fact X -> s# 0())
     (active# p X -> active# X, active# fact X -> zero# X)
     (active# p X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# p X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# p X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
     (active# p X -> active# X, active# prod(X1, X2) -> active# X2)
     (active# p X -> active# X, active# prod(X1, X2) -> active# X1)
     (active# p X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# p X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# p X -> active# X, active# s X -> active# X)
     (active# p X -> active# X, active# s X -> s# active X)
     (active# p X -> active# X, active# zero X -> active# X)
     (active# p X -> active# X, active# zero X -> zero# active X)
     (active# p X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# p X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# p X -> proper# X)
     (proper# s X -> proper# X, proper# p X -> p# proper X)
     (proper# s X -> proper# X, proper# fact X -> proper# X)
     (proper# s X -> proper# X, proper# fact X -> fact# proper X)
     (proper# s X -> proper# X, proper# prod(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# prod(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# zero X -> proper# X)
     (proper# s X -> proper# X, proper# zero X -> zero# proper X)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# p X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# p X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# p X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# p X -> proper# X, proper# p X -> proper# X)
     (proper# p X -> proper# X, proper# p X -> p# proper X)
     (proper# p X -> proper# X, proper# fact X -> proper# X)
     (proper# p X -> proper# X, proper# fact X -> fact# proper X)
     (proper# p X -> proper# X, proper# prod(X1, X2) -> proper# X2)
     (proper# p X -> proper# X, proper# prod(X1, X2) -> proper# X1)
     (proper# p X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# p X -> proper# X, proper# s X -> proper# X)
     (proper# p X -> proper# X, proper# s X -> s# proper X)
     (proper# p X -> proper# X, proper# zero X -> proper# X)
     (proper# p X -> proper# X, proper# zero X -> zero# proper X)
     (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# p X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (top# ok X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (top# ok X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (top# ok X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (top# ok X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (top# ok X -> active# X, active# add(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# add(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# p X -> active# X)
     (top# ok X -> active# X, active# p X -> p# active X)
     (top# ok X -> active# X, active# fact X -> active# X)
     (top# ok X -> active# X, active# fact X -> p# X)
     (top# ok X -> active# X, active# fact X -> fact# active X)
     (top# ok X -> active# X, active# fact X -> fact# p X)
     (top# ok X -> active# X, active# fact X -> prod#(X, fact p X))
     (top# ok X -> active# X, active# fact X -> s# 0())
     (top# ok X -> active# X, active# fact X -> zero# X)
     (top# ok X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (top# ok X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (top# ok X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
     (top# ok X -> active# X, active# prod(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# prod(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
     (top# ok X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# zero X -> active# X)
     (top# ok X -> active# X, active# zero X -> zero# active X)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
     (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
     (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
     (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
     (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X2, active# p X -> active# X)
     (active# add(X1, X2) -> active# X2, active# p X -> p# active X)
     (active# add(X1, X2) -> active# X2, active# fact X -> active# X)
     (active# add(X1, X2) -> active# X2, active# fact X -> p# X)
     (active# add(X1, X2) -> active# X2, active# fact X -> fact# active X)
     (active# add(X1, X2) -> active# X2, active# fact X -> fact# p X)
     (active# add(X1, X2) -> active# X2, active# fact X -> prod#(X, fact p X))
     (active# add(X1, X2) -> active# X2, active# fact X -> s# 0())
     (active# add(X1, X2) -> active# X2, active# fact X -> zero# X)
     (active# add(X1, X2) -> active# X2, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# add(X1, X2) -> active# X2, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# add(X1, X2) -> active# X2, active# prod(s X, Y) -> prod#(X, Y))
     (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# add(X1, X2) -> active# X2, active# s X -> active# X)
     (active# add(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# add(X1, X2) -> active# X2, active# zero X -> active# X)
     (active# add(X1, X2) -> active# X2, active# zero X -> zero# active X)
     (active# add(X1, X2) -> active# X2, active# if(X1, X2, X3) -> active# X1)
     (active# add(X1, X2) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (proper# prod(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# prod(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# prod(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# prod(X1, X2) -> proper# X2, proper# p X -> proper# X)
     (proper# prod(X1, X2) -> proper# X2, proper# p X -> p# proper X)
     (proper# prod(X1, X2) -> proper# X2, proper# fact X -> proper# X)
     (proper# prod(X1, X2) -> proper# X2, proper# fact X -> fact# proper X)
     (proper# prod(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X2)
     (proper# prod(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X1)
     (proper# prod(X1, X2) -> proper# X2, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# prod(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# prod(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# prod(X1, X2) -> proper# X2, proper# zero X -> proper# X)
     (proper# prod(X1, X2) -> proper# X2, proper# zero X -> zero# proper X)
     (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (prod#(X1, mark X2) -> prod#(X1, X2), prod#(ok X1, ok 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, mark X2) -> prod#(X1, X2))
     (prod#(ok X1, ok X2) -> prod#(X1, X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
     (prod#(ok X1, ok X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (prod#(ok X1, ok X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (add#(mark X1, X2) -> add#(X1, X2), add#(ok X1, ok 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, mark X2) -> add#(X1, X2))
     (active# prod(X1, X2) -> prod#(X1, active X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
     (active# prod(X1, X2) -> prod#(X1, active X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (active# prod(X1, X2) -> prod#(X1, active X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (proper# prod(X1, X2) -> prod#(proper X1, proper X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
     (proper# prod(X1, X2) -> prod#(proper X1, proper X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (proper# prod(X1, X2) -> prod#(proper X1, proper X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
     (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# zero X -> zero# active X, zero# ok X -> zero# X)
     (active# zero X -> zero# active X, zero# mark X -> zero# X)
     (active# fact X -> fact# p X, fact# ok X -> fact# X)
     (active# fact X -> fact# p X, fact# mark X -> fact# X)
     (active# p X -> p# active X, p# ok X -> p# X)
     (active# p X -> p# active X, p# mark X -> p# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# p X -> p# proper X, p# ok X -> p# X)
     (proper# p X -> p# proper X, p# mark X -> p# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (proper# fact X -> fact# proper X, fact# mark X -> fact# X)
     (proper# fact X -> fact# proper X, fact# ok X -> fact# X)
     (proper# zero X -> zero# proper X, zero# mark X -> zero# X)
     (proper# zero X -> zero# proper X, zero# ok X -> zero# X)
     (active# fact X -> fact# active X, fact# mark X -> fact# X)
     (active# fact X -> fact# active X, fact# ok X -> fact# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# s X -> s# active X, s# ok X -> s# X)
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok 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#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(X1, mark X2) -> add#(X1, X2))
     (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(mark X1, X2) -> add#(X1, X2))
     (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(X1, active X2), add#(mark X1, X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (add#(ok X1, ok X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (add#(ok X1, ok X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (add#(ok X1, ok X2) -> add#(X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (add#(X1, mark 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#(X1, mark X2) -> add#(X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark 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#(ok X1, ok X2) -> prod#(X1, X2))
     (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# add(X1, X2) -> proper# X2, proper# zero X -> zero# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# zero X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# fact X -> fact# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# fact X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# p X -> p# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# p X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X2, proper# zero X -> zero# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# zero X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X2, proper# prod(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# prod(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# fact X -> fact# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# fact X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# p X -> p# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# p X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (active# prod(X1, X2) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# prod(X1, X2) -> active# X2, active# if(X1, X2, X3) -> active# X1)
     (active# prod(X1, X2) -> active# X2, active# zero X -> zero# active X)
     (active# prod(X1, X2) -> active# X2, active# zero X -> active# X)
     (active# prod(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# prod(X1, X2) -> active# X2, active# s X -> active# X)
     (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X1)
     (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X2)
     (active# prod(X1, X2) -> active# X2, active# prod(s X, Y) -> prod#(X, Y))
     (active# prod(X1, X2) -> active# X2, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# prod(X1, X2) -> active# X2, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# prod(X1, X2) -> active# X2, active# fact X -> zero# X)
     (active# prod(X1, X2) -> active# X2, active# fact X -> s# 0())
     (active# prod(X1, X2) -> active# X2, active# fact X -> prod#(X, fact p X))
     (active# prod(X1, X2) -> active# X2, active# fact X -> fact# p X)
     (active# prod(X1, X2) -> active# X2, active# fact X -> fact# active X)
     (active# prod(X1, X2) -> active# X2, active# fact X -> p# X)
     (active# prod(X1, X2) -> active# X2, active# fact X -> active# X)
     (active# prod(X1, X2) -> active# X2, active# p X -> p# active X)
     (active# prod(X1, X2) -> active# X2, active# p X -> active# X)
     (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
     (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
     (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
     (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
     (active# prod(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
     (active# prod(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# zero X -> zero# proper X)
     (top# mark X -> proper# X, proper# zero X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# prod(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# prod(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# fact X -> fact# proper X)
     (top# mark X -> proper# X, proper# fact X -> proper# X)
     (top# mark X -> proper# X, proper# p X -> p# proper X)
     (top# mark X -> proper# X, proper# p X -> proper# X)
     (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (proper# fact X -> proper# X, proper# zero X -> zero# proper X)
     (proper# fact X -> proper# X, proper# zero X -> proper# X)
     (proper# fact X -> proper# X, proper# s X -> s# proper X)
     (proper# fact X -> proper# X, proper# s X -> proper# X)
     (proper# fact X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# fact X -> proper# X, proper# prod(X1, X2) -> proper# X1)
     (proper# fact X -> proper# X, proper# prod(X1, X2) -> proper# X2)
     (proper# fact X -> proper# X, proper# fact X -> fact# proper X)
     (proper# fact X -> proper# X, proper# fact X -> proper# X)
     (proper# fact X -> proper# X, proper# p X -> p# proper X)
     (proper# fact X -> proper# X, proper# p X -> proper# X)
     (proper# fact X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# fact X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# fact X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (proper# zero X -> proper# X, proper# zero X -> zero# proper X)
     (proper# zero X -> proper# X, proper# zero X -> proper# X)
     (proper# zero X -> proper# X, proper# s X -> s# proper X)
     (proper# zero X -> proper# X, proper# s X -> proper# X)
     (proper# zero X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# zero X -> proper# X, proper# prod(X1, X2) -> proper# X1)
     (proper# zero X -> proper# X, proper# prod(X1, X2) -> proper# X2)
     (proper# zero X -> proper# X, proper# fact X -> fact# proper X)
     (proper# zero X -> proper# X, proper# fact X -> proper# X)
     (proper# zero X -> proper# X, proper# p X -> p# proper X)
     (proper# zero X -> proper# X, proper# p X -> proper# X)
     (proper# zero X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# zero X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# zero X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (active# fact X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# fact X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# fact X -> active# X, active# zero X -> zero# active X)
     (active# fact X -> active# X, active# zero X -> active# X)
     (active# fact X -> active# X, active# s X -> s# active X)
     (active# fact X -> active# X, active# s X -> active# X)
     (active# fact X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# fact X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# fact X -> active# X, active# prod(X1, X2) -> active# X1)
     (active# fact X -> active# X, active# prod(X1, X2) -> active# X2)
     (active# fact X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
     (active# fact X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# fact X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# fact X -> active# X, active# fact X -> zero# X)
     (active# fact X -> active# X, active# fact X -> s# 0())
     (active# fact X -> active# X, active# fact X -> prod#(X, fact p X))
     (active# fact X -> active# X, active# fact X -> fact# p X)
     (active# fact X -> active# X, active# fact X -> fact# active X)
     (active# fact X -> active# X, active# fact X -> p# X)
     (active# fact X -> active# X, active# fact X -> active# X)
     (active# fact X -> active# X, active# p X -> p# active X)
     (active# fact X -> active# X, active# p X -> active# X)
     (active# fact X -> active# X, active# add(X1, X2) -> active# X1)
     (active# fact X -> active# X, active# add(X1, X2) -> active# X2)
     (active# fact X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# fact X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# fact X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# fact X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# fact X -> zero# X, zero# mark X -> zero# X)
     (active# fact X -> zero# X, zero# ok X -> zero# X)
     (active# zero X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# zero X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# zero X -> active# X, active# zero X -> zero# active X)
     (active# zero X -> active# X, active# zero X -> active# X)
     (active# zero X -> active# X, active# s X -> s# active X)
     (active# zero X -> active# X, active# s X -> active# X)
     (active# zero X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# zero X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# zero X -> active# X, active# prod(X1, X2) -> active# X1)
     (active# zero X -> active# X, active# prod(X1, X2) -> active# X2)
     (active# zero X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
     (active# zero X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# zero X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# zero X -> active# X, active# fact X -> zero# X)
     (active# zero X -> active# X, active# fact X -> s# 0())
     (active# zero X -> active# X, active# fact X -> prod#(X, fact p X))
     (active# zero X -> active# X, active# fact X -> fact# p X)
     (active# zero X -> active# X, active# fact X -> fact# active X)
     (active# zero X -> active# X, active# fact X -> p# X)
     (active# zero X -> active# X, active# fact X -> active# X)
     (active# zero X -> active# X, active# p X -> p# active X)
     (active# zero X -> active# X, active# p X -> active# X)
     (active# zero X -> active# X, active# add(X1, X2) -> active# X1)
     (active# zero X -> active# X, active# add(X1, X2) -> active# X2)
     (active# zero X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# zero X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# zero X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# zero X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (p# mark X -> p# X, p# mark X -> p# X)
     (p# mark X -> p# X, p# ok X -> p# X)
     (fact# mark X -> fact# X, fact# mark X -> fact# X)
     (fact# mark X -> fact# X, fact# ok X -> fact# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (zero# mark X -> zero# X, zero# mark X -> zero# X)
     (zero# mark X -> zero# X, zero# ok X -> zero# X)
     (active# prod(X1, X2) -> prod#(active X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
     (active# prod(X1, X2) -> prod#(active X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
     (active# prod(X1, X2) -> prod#(active X1, X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X3, proper# zero X -> zero# proper X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# zero X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X3, proper# prod(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# prod(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# fact X -> fact# proper X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# fact X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# p X -> p# proper X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# p X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X3, proper# add(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# add(X1, X2) -> proper# X2)
     (active# add(s X, Y) -> add#(X, Y), add#(X1, mark 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#(ok X1, ok X2) -> add#(X1, X2))
     (active# fact X -> s# 0(), s# mark X -> s# X)
     (active# fact X -> s# 0(), s# ok X -> s# X)
     (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# prod(X1, X2) -> proper# X1, proper# zero X -> zero# proper X)
     (proper# prod(X1, X2) -> proper# X1, proper# zero X -> proper# X)
     (proper# prod(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# prod(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# prod(X1, X2) -> proper# X1, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
     (proper# prod(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X1)
     (proper# prod(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X2)
     (proper# prod(X1, X2) -> proper# X1, proper# fact X -> fact# proper X)
     (proper# prod(X1, X2) -> proper# X1, proper# fact X -> proper# X)
     (proper# prod(X1, X2) -> proper# X1, proper# p X -> p# proper X)
     (proper# prod(X1, X2) -> proper# X1, proper# p X -> proper# X)
     (proper# prod(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# prod(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# prod(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (active# add(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# add(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
     (active# add(X1, X2) -> active# X1, active# zero X -> zero# active X)
     (active# add(X1, X2) -> active# X1, active# zero X -> active# X)
     (active# add(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# add(X1, X2) -> active# X1, active# s X -> active# X)
     (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X1, active# prod(s X, Y) -> prod#(X, Y))
     (active# add(X1, X2) -> active# X1, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# add(X1, X2) -> active# X1, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# add(X1, X2) -> active# X1, active# fact X -> zero# X)
     (active# add(X1, X2) -> active# X1, active# fact X -> s# 0())
     (active# add(X1, X2) -> active# X1, active# fact X -> prod#(X, fact p X))
     (active# add(X1, X2) -> active# X1, active# fact X -> fact# p X)
     (active# add(X1, X2) -> active# X1, active# fact X -> fact# active X)
     (active# add(X1, X2) -> active# X1, active# fact X -> p# X)
     (active# add(X1, X2) -> active# X1, active# fact X -> active# X)
     (active# add(X1, X2) -> active# X1, active# p X -> p# active X)
     (active# add(X1, X2) -> active# X1, active# p X -> active# X)
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X1)
     (active# if(X1, X2, X3) -> active# X1, active# zero X -> zero# active X)
     (active# if(X1, X2, X3) -> active# X1, active# zero X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# if(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> prod#(X1, active X2))
     (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> prod#(active X1, X2))
     (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> active# X1)
     (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> active# X2)
     (active# if(X1, X2, X3) -> active# X1, active# prod(s X, Y) -> prod#(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> zero# X)
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> s# 0())
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> prod#(X, fact p X))
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> fact# p X)
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> fact# active X)
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> p# X)
     (active# if(X1, X2, X3) -> active# X1, active# fact X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# p X -> p# active X)
     (active# if(X1, X2, X3) -> active# X1, active# p X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> active# X1)
     (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> active# X2)
     (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# if(X1, X2, X3) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# add(s X, Y) -> add#(X, Y))
    }
    EDG:
     {
      (active# prod(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
      (active# prod(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
      (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
      (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
      (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
      (active# prod(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
      (active# prod(X1, X2) -> active# X1, active# p X -> active# X)
      (active# prod(X1, X2) -> active# X1, active# p X -> p# active X)
      (active# prod(X1, X2) -> active# X1, active# fact X -> active# X)
      (active# prod(X1, X2) -> active# X1, active# fact X -> p# X)
      (active# prod(X1, X2) -> active# X1, active# fact X -> fact# active X)
      (active# prod(X1, X2) -> active# X1, active# fact X -> fact# p X)
      (active# prod(X1, X2) -> active# X1, active# fact X -> prod#(X, fact p X))
      (active# prod(X1, X2) -> active# X1, active# fact X -> s# 0())
      (active# prod(X1, X2) -> active# X1, active# fact X -> zero# X)
      (active# prod(X1, X2) -> active# X1, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# prod(X1, X2) -> active# X1, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# prod(X1, X2) -> active# X1, active# prod(s X, Y) -> prod#(X, Y))
      (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X2)
      (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X1)
      (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# prod(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# prod(X1, X2) -> active# X1, active# s X -> active# X)
      (active# prod(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# prod(X1, X2) -> active# X1, active# zero X -> active# X)
      (active# prod(X1, X2) -> active# X1, active# zero X -> zero# active X)
      (active# prod(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
      (active# prod(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (proper# if(X1, X2, X3) -> proper# X1, proper# add(X1, X2) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X1, proper# add(X1, X2) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# if(X1, X2, X3) -> proper# X1, proper# p X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# p X -> p# proper X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# fact X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# fact X -> fact# proper X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# prod(X1, X2) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X1, proper# prod(X1, X2) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X1, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# zero X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# zero X -> zero# proper X)
      (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
      (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
      (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# add(X1, X2) -> proper# X1, proper# p X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# p X -> p# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# fact X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# fact X -> fact# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X2)
      (proper# add(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X1, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# zero X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# zero X -> zero# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
      (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
      (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
      (proper# add(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(ok X1, ok X2) -> add#(X1, X2))
      (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, mark X2) -> add#(X1, X2))
      (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 -> prod#(X, fact p X), prod#(X1, mark X2) -> prod#(X1, X2))
      (active# add(X1, X2) -> add#(active X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
      (active# add(X1, X2) -> add#(active X1, X2), add#(mark X1, X2) -> add#(X1, X2))
      (zero# ok X -> zero# X, zero# ok X -> zero# X)
      (zero# ok X -> zero# X, zero# mark X -> zero# X)
      (s# ok X -> s# X, s# ok X -> s# X)
      (s# ok X -> s# X, s# mark X -> s# X)
      (fact# ok X -> fact# X, fact# ok X -> fact# X)
      (fact# ok X -> fact# X, fact# mark X -> fact# X)
      (p# ok X -> p# X, p# ok X -> p# X)
      (p# ok X -> p# X, p# mark X -> p# X)
      (active# s X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# s X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# s X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# s X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# s X -> active# X, active# add(X1, X2) -> active# X2)
      (active# s X -> active# X, active# add(X1, X2) -> active# X1)
      (active# s X -> active# X, active# p X -> active# X)
      (active# s X -> active# X, active# p X -> p# active X)
      (active# s X -> active# X, active# fact X -> active# X)
      (active# s X -> active# X, active# fact X -> p# X)
      (active# s X -> active# X, active# fact X -> fact# active X)
      (active# s X -> active# X, active# fact X -> fact# p X)
      (active# s X -> active# X, active# fact X -> prod#(X, fact p X))
      (active# s X -> active# X, active# fact X -> s# 0())
      (active# s X -> active# X, active# fact X -> zero# X)
      (active# s X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# s X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# s X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
      (active# s X -> active# X, active# prod(X1, X2) -> active# X2)
      (active# s X -> active# X, active# prod(X1, X2) -> active# X1)
      (active# s X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# s X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# s X -> active# X, active# s X -> active# X)
      (active# s X -> active# X, active# s X -> s# active X)
      (active# s X -> active# X, active# zero X -> active# X)
      (active# s X -> active# X, active# zero X -> zero# active X)
      (active# s X -> active# X, active# if(X1, X2, X3) -> active# X1)
      (active# s X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# p X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# p X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# p X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# p X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# p X -> active# X, active# add(X1, X2) -> active# X2)
      (active# p X -> active# X, active# add(X1, X2) -> active# X1)
      (active# p X -> active# X, active# p X -> active# X)
      (active# p X -> active# X, active# p X -> p# active X)
      (active# p X -> active# X, active# fact X -> active# X)
      (active# p X -> active# X, active# fact X -> p# X)
      (active# p X -> active# X, active# fact X -> fact# active X)
      (active# p X -> active# X, active# fact X -> fact# p X)
      (active# p X -> active# X, active# fact X -> prod#(X, fact p X))
      (active# p X -> active# X, active# fact X -> s# 0())
      (active# p X -> active# X, active# fact X -> zero# X)
      (active# p X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# p X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# p X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
      (active# p X -> active# X, active# prod(X1, X2) -> active# X2)
      (active# p X -> active# X, active# prod(X1, X2) -> active# X1)
      (active# p X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# p X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# p X -> active# X, active# s X -> active# X)
      (active# p X -> active# X, active# s X -> s# active X)
      (active# p X -> active# X, active# zero X -> active# X)
      (active# p X -> active# X, active# zero X -> zero# active X)
      (active# p X -> active# X, active# if(X1, X2, X3) -> active# X1)
      (active# p X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# p X -> proper# X)
      (proper# s X -> proper# X, proper# p X -> p# proper X)
      (proper# s X -> proper# X, proper# fact X -> proper# X)
      (proper# s X -> proper# X, proper# fact X -> fact# proper X)
      (proper# s X -> proper# X, proper# prod(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# prod(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# s X -> proper# X)
      (proper# s X -> proper# X, proper# s X -> s# proper X)
      (proper# s X -> proper# X, proper# zero X -> proper# X)
      (proper# s X -> proper# X, proper# zero X -> zero# proper X)
      (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
      (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
      (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
      (proper# s X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# p X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# p X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# p X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# p X -> proper# X, proper# p X -> proper# X)
      (proper# p X -> proper# X, proper# p X -> p# proper X)
      (proper# p X -> proper# X, proper# fact X -> proper# X)
      (proper# p X -> proper# X, proper# fact X -> fact# proper X)
      (proper# p X -> proper# X, proper# prod(X1, X2) -> proper# X2)
      (proper# p X -> proper# X, proper# prod(X1, X2) -> proper# X1)
      (proper# p X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# p X -> proper# X, proper# s X -> proper# X)
      (proper# p X -> proper# X, proper# s X -> s# proper X)
      (proper# p X -> proper# X, proper# zero X -> proper# X)
      (proper# p X -> proper# X, proper# zero X -> zero# proper X)
      (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
      (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
      (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
      (proper# p X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (top# ok X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (top# ok X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (top# ok X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (top# ok X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (top# ok X -> active# X, active# add(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# add(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# p X -> active# X)
      (top# ok X -> active# X, active# p X -> p# active X)
      (top# ok X -> active# X, active# fact X -> active# X)
      (top# ok X -> active# X, active# fact X -> p# X)
      (top# ok X -> active# X, active# fact X -> fact# active X)
      (top# ok X -> active# X, active# fact X -> fact# p X)
      (top# ok X -> active# X, active# fact X -> prod#(X, fact p X))
      (top# ok X -> active# X, active# fact X -> s# 0())
      (top# ok X -> active# X, active# fact X -> zero# X)
      (top# ok X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (top# ok X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (top# ok X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
      (top# ok X -> active# X, active# prod(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# prod(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
      (top# ok X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
      (top# ok X -> active# X, active# s X -> active# X)
      (top# ok X -> active# X, active# s X -> s# active X)
      (top# ok X -> active# X, active# zero X -> active# X)
      (top# ok X -> active# X, active# zero X -> zero# active X)
      (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1)
      (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
      (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
      (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
      (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
      (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X2, active# p X -> active# X)
      (active# add(X1, X2) -> active# X2, active# p X -> p# active X)
      (active# add(X1, X2) -> active# X2, active# fact X -> active# X)
      (active# add(X1, X2) -> active# X2, active# fact X -> p# X)
      (active# add(X1, X2) -> active# X2, active# fact X -> fact# active X)
      (active# add(X1, X2) -> active# X2, active# fact X -> fact# p X)
      (active# add(X1, X2) -> active# X2, active# fact X -> prod#(X, fact p X))
      (active# add(X1, X2) -> active# X2, active# fact X -> s# 0())
      (active# add(X1, X2) -> active# X2, active# fact X -> zero# X)
      (active# add(X1, X2) -> active# X2, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# add(X1, X2) -> active# X2, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# add(X1, X2) -> active# X2, active# prod(s X, Y) -> prod#(X, Y))
      (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# add(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# add(X1, X2) -> active# X2, active# s X -> active# X)
      (active# add(X1, X2) -> active# X2, active# s X -> s# active X)
      (active# add(X1, X2) -> active# X2, active# zero X -> active# X)
      (active# add(X1, X2) -> active# X2, active# zero X -> zero# active X)
      (active# add(X1, X2) -> active# X2, active# if(X1, X2, X3) -> active# X1)
      (active# add(X1, X2) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (proper# prod(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
      (proper# prod(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
      (proper# prod(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# prod(X1, X2) -> proper# X2, proper# p X -> proper# X)
      (proper# prod(X1, X2) -> proper# X2, proper# p X -> p# proper X)
      (proper# prod(X1, X2) -> proper# X2, proper# fact X -> proper# X)
      (proper# prod(X1, X2) -> proper# X2, proper# fact X -> fact# proper X)
      (proper# prod(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X2)
      (proper# prod(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X1)
      (proper# prod(X1, X2) -> proper# X2, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# prod(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# prod(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# prod(X1, X2) -> proper# X2, proper# zero X -> proper# X)
      (proper# prod(X1, X2) -> proper# X2, proper# zero X -> zero# proper X)
      (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
      (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
      (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
      (proper# prod(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (prod#(X1, mark X2) -> prod#(X1, X2), prod#(ok X1, ok 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, mark X2) -> prod#(X1, X2))
      (prod#(ok X1, ok X2) -> prod#(X1, X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
      (prod#(ok X1, ok X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (prod#(ok X1, ok X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (add#(mark X1, X2) -> add#(X1, X2), add#(ok X1, ok 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, mark X2) -> add#(X1, X2))
      (active# prod(X1, X2) -> prod#(X1, active X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
      (active# prod(X1, X2) -> prod#(X1, active X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (proper# prod(X1, X2) -> prod#(proper X1, proper X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
      (proper# prod(X1, X2) -> prod#(proper X1, proper X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (proper# prod(X1, X2) -> prod#(proper X1, proper X2), prod#(X1, mark X2) -> prod#(X1, X2))
      (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
      (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
      (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
      (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (active# zero X -> zero# active X, zero# ok X -> zero# X)
      (active# zero X -> zero# active X, zero# mark X -> zero# X)
      (active# fact X -> fact# p X, fact# ok X -> fact# X)
      (active# fact X -> fact# p X, fact# mark X -> fact# X)
      (active# p X -> p# active X, p# ok X -> p# X)
      (active# p X -> p# active X, p# mark X -> p# X)
      (proper# s X -> s# proper X, s# ok X -> s# X)
      (proper# s X -> s# proper X, s# mark X -> s# X)
      (proper# p X -> p# proper X, p# ok X -> p# X)
      (proper# p X -> p# proper X, p# mark X -> p# X)
      (top# ok X -> top# active X, top# ok X -> top# active X)
      (top# ok X -> top# active X, top# ok X -> active# X)
      (top# ok X -> top# active X, top# mark X -> top# proper X)
      (top# ok X -> top# active X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> top# proper X)
      (top# mark X -> top# proper X, top# ok X -> active# X)
      (top# mark X -> top# proper X, top# ok X -> top# active X)
      (proper# fact X -> fact# proper X, fact# mark X -> fact# X)
      (proper# fact X -> fact# proper X, fact# ok X -> fact# X)
      (proper# zero X -> zero# proper X, zero# mark X -> zero# X)
      (proper# zero X -> zero# proper X, zero# ok X -> zero# X)
      (active# fact X -> fact# active X, fact# mark X -> fact# X)
      (active# fact X -> fact# active X, fact# ok X -> fact# X)
      (active# s X -> s# active X, s# mark X -> s# X)
      (active# s X -> s# active X, s# ok X -> s# X)
      (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok 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#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
      (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(X1, mark X2) -> add#(X1, X2))
      (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(mark X1, X2) -> add#(X1, X2))
      (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(ok X1, ok X2) -> add#(X1, X2))
      (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
      (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
      (add#(ok X1, ok X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
      (add#(ok X1, ok X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
      (add#(ok X1, ok X2) -> add#(X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
      (add#(X1, mark 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#(X1, mark X2) -> add#(X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
      (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark 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#(ok X1, ok X2) -> prod#(X1, X2))
      (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
      (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
      (proper# add(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
      (proper# add(X1, X2) -> proper# X2, proper# zero X -> zero# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# zero X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# add(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X2, proper# prod(X1, X2) -> proper# X2)
      (proper# add(X1, X2) -> proper# X2, proper# fact X -> fact# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# fact X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# p X -> p# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# p X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
      (proper# if(X1, X2, X3) -> proper# X2, proper# zero X -> zero# proper X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# zero X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# if(X1, X2, X3) -> proper# X2, proper# prod(X1, X2) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X2, proper# prod(X1, X2) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X2, proper# fact X -> fact# proper X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# fact X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# p X -> p# proper X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# p X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# if(X1, X2, X3) -> proper# X2, proper# add(X1, X2) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X2, proper# add(X1, X2) -> proper# X2)
      (active# prod(X1, X2) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# prod(X1, X2) -> active# X2, active# if(X1, X2, X3) -> active# X1)
      (active# prod(X1, X2) -> active# X2, active# zero X -> zero# active X)
      (active# prod(X1, X2) -> active# X2, active# zero X -> active# X)
      (active# prod(X1, X2) -> active# X2, active# s X -> s# active X)
      (active# prod(X1, X2) -> active# X2, active# s X -> active# X)
      (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X1)
      (active# prod(X1, X2) -> active# X2, active# prod(X1, X2) -> active# X2)
      (active# prod(X1, X2) -> active# X2, active# prod(s X, Y) -> prod#(X, Y))
      (active# prod(X1, X2) -> active# X2, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# prod(X1, X2) -> active# X2, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# prod(X1, X2) -> active# X2, active# fact X -> zero# X)
      (active# prod(X1, X2) -> active# X2, active# fact X -> s# 0())
      (active# prod(X1, X2) -> active# X2, active# fact X -> prod#(X, fact p X))
      (active# prod(X1, X2) -> active# X2, active# fact X -> fact# p X)
      (active# prod(X1, X2) -> active# X2, active# fact X -> fact# active X)
      (active# prod(X1, X2) -> active# X2, active# fact X -> p# X)
      (active# prod(X1, X2) -> active# X2, active# fact X -> active# X)
      (active# prod(X1, X2) -> active# X2, active# p X -> p# active X)
      (active# prod(X1, X2) -> active# X2, active# p X -> active# X)
      (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
      (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
      (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
      (active# prod(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
      (active# prod(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
      (active# prod(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
      (top# mark X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
      (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
      (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
      (top# mark X -> proper# X, proper# zero X -> zero# proper X)
      (top# mark X -> proper# X, proper# zero X -> proper# X)
      (top# mark X -> proper# X, proper# s X -> s# proper X)
      (top# mark X -> proper# X, proper# s X -> proper# X)
      (top# mark X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# prod(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# prod(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# fact X -> fact# proper X)
      (top# mark X -> proper# X, proper# fact X -> proper# X)
      (top# mark X -> proper# X, proper# p X -> p# proper X)
      (top# mark X -> proper# X, proper# p X -> proper# X)
      (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
      (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
      (proper# fact X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
      (proper# fact X -> proper# X, proper# zero X -> zero# proper X)
      (proper# fact X -> proper# X, proper# zero X -> proper# X)
      (proper# fact X -> proper# X, proper# s X -> s# proper X)
      (proper# fact X -> proper# X, proper# s X -> proper# X)
      (proper# fact X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# fact X -> proper# X, proper# prod(X1, X2) -> proper# X1)
      (proper# fact X -> proper# X, proper# prod(X1, X2) -> proper# X2)
      (proper# fact X -> proper# X, proper# fact X -> fact# proper X)
      (proper# fact X -> proper# X, proper# fact X -> proper# X)
      (proper# fact X -> proper# X, proper# p X -> p# proper X)
      (proper# fact X -> proper# X, proper# p X -> proper# X)
      (proper# fact X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# fact X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# fact X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
      (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
      (proper# zero X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
      (proper# zero X -> proper# X, proper# zero X -> zero# proper X)
      (proper# zero X -> proper# X, proper# zero X -> proper# X)
      (proper# zero X -> proper# X, proper# s X -> s# proper X)
      (proper# zero X -> proper# X, proper# s X -> proper# X)
      (proper# zero X -> proper# X, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# zero X -> proper# X, proper# prod(X1, X2) -> proper# X1)
      (proper# zero X -> proper# X, proper# prod(X1, X2) -> proper# X2)
      (proper# zero X -> proper# X, proper# fact X -> fact# proper X)
      (proper# zero X -> proper# X, proper# fact X -> proper# X)
      (proper# zero X -> proper# X, proper# p X -> p# proper X)
      (proper# zero X -> proper# X, proper# p X -> proper# X)
      (proper# zero X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# zero X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# zero X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (active# fact X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# fact X -> active# X, active# if(X1, X2, X3) -> active# X1)
      (active# fact X -> active# X, active# zero X -> zero# active X)
      (active# fact X -> active# X, active# zero X -> active# X)
      (active# fact X -> active# X, active# s X -> s# active X)
      (active# fact X -> active# X, active# s X -> active# X)
      (active# fact X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# fact X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# fact X -> active# X, active# prod(X1, X2) -> active# X1)
      (active# fact X -> active# X, active# prod(X1, X2) -> active# X2)
      (active# fact X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
      (active# fact X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# fact X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# fact X -> active# X, active# fact X -> zero# X)
      (active# fact X -> active# X, active# fact X -> s# 0())
      (active# fact X -> active# X, active# fact X -> prod#(X, fact p X))
      (active# fact X -> active# X, active# fact X -> fact# p X)
      (active# fact X -> active# X, active# fact X -> fact# active X)
      (active# fact X -> active# X, active# fact X -> p# X)
      (active# fact X -> active# X, active# fact X -> active# X)
      (active# fact X -> active# X, active# p X -> p# active X)
      (active# fact X -> active# X, active# p X -> active# X)
      (active# fact X -> active# X, active# add(X1, X2) -> active# X1)
      (active# fact X -> active# X, active# add(X1, X2) -> active# X2)
      (active# fact X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# fact X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# fact X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# fact X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# zero X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# zero X -> active# X, active# if(X1, X2, X3) -> active# X1)
      (active# zero X -> active# X, active# zero X -> zero# active X)
      (active# zero X -> active# X, active# zero X -> active# X)
      (active# zero X -> active# X, active# s X -> s# active X)
      (active# zero X -> active# X, active# s X -> active# X)
      (active# zero X -> active# X, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# zero X -> active# X, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# zero X -> active# X, active# prod(X1, X2) -> active# X1)
      (active# zero X -> active# X, active# prod(X1, X2) -> active# X2)
      (active# zero X -> active# X, active# prod(s X, Y) -> prod#(X, Y))
      (active# zero X -> active# X, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# zero X -> active# X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# zero X -> active# X, active# fact X -> zero# X)
      (active# zero X -> active# X, active# fact X -> s# 0())
      (active# zero X -> active# X, active# fact X -> prod#(X, fact p X))
      (active# zero X -> active# X, active# fact X -> fact# p X)
      (active# zero X -> active# X, active# fact X -> fact# active X)
      (active# zero X -> active# X, active# fact X -> p# X)
      (active# zero X -> active# X, active# fact X -> active# X)
      (active# zero X -> active# X, active# p X -> p# active X)
      (active# zero X -> active# X, active# p X -> active# X)
      (active# zero X -> active# X, active# add(X1, X2) -> active# X1)
      (active# zero X -> active# X, active# add(X1, X2) -> active# X2)
      (active# zero X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# zero X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# zero X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# zero X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (p# mark X -> p# X, p# mark X -> p# X)
      (p# mark X -> p# X, p# ok X -> p# X)
      (fact# mark X -> fact# X, fact# mark X -> fact# X)
      (fact# mark X -> fact# X, fact# ok X -> fact# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# ok X -> s# X)
      (zero# mark X -> zero# X, zero# mark X -> zero# X)
      (zero# mark X -> zero# X, zero# ok X -> zero# X)
      (active# prod(X1, X2) -> prod#(active X1, X2), prod#(mark X1, X2) -> prod#(X1, X2))
      (active# prod(X1, X2) -> prod#(active X1, X2), prod#(ok X1, ok X2) -> prod#(X1, X2))
      (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
      (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
      (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3)
      (proper# if(X1, X2, X3) -> proper# X3, proper# zero X -> zero# proper X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# zero X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# if(X1, X2, X3) -> proper# X3, proper# prod(X1, X2) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X3, proper# prod(X1, X2) -> proper# X2)
      (proper# if(X1, X2, X3) -> proper# X3, proper# fact X -> fact# proper X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# fact X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# p X -> p# proper X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# p X -> proper# X)
      (proper# if(X1, X2, X3) -> proper# X3, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# if(X1, X2, X3) -> proper# X3, proper# add(X1, X2) -> proper# X1)
      (proper# if(X1, X2, X3) -> proper# X3, proper# add(X1, X2) -> proper# X2)
      (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
      (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
      (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
      (proper# prod(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
      (proper# prod(X1, X2) -> proper# X1, proper# zero X -> zero# proper X)
      (proper# prod(X1, X2) -> proper# X1, proper# zero X -> proper# X)
      (proper# prod(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# prod(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# prod(X1, X2) -> proper# X1, proper# prod(X1, X2) -> prod#(proper X1, proper X2))
      (proper# prod(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X1)
      (proper# prod(X1, X2) -> proper# X1, proper# prod(X1, X2) -> proper# X2)
      (proper# prod(X1, X2) -> proper# X1, proper# fact X -> fact# proper X)
      (proper# prod(X1, X2) -> proper# X1, proper# fact X -> proper# X)
      (proper# prod(X1, X2) -> proper# X1, proper# p X -> p# proper X)
      (proper# prod(X1, X2) -> proper# X1, proper# p X -> proper# X)
      (proper# prod(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# prod(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
      (proper# prod(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
      (active# add(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# add(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
      (active# add(X1, X2) -> active# X1, active# zero X -> zero# active X)
      (active# add(X1, X2) -> active# X1, active# zero X -> active# X)
      (active# add(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# add(X1, X2) -> active# X1, active# s X -> active# X)
      (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X1, active# prod(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X1, active# prod(s X, Y) -> prod#(X, Y))
      (active# add(X1, X2) -> active# X1, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# add(X1, X2) -> active# X1, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# add(X1, X2) -> active# X1, active# fact X -> zero# X)
      (active# add(X1, X2) -> active# X1, active# fact X -> s# 0())
      (active# add(X1, X2) -> active# X1, active# fact X -> prod#(X, fact p X))
      (active# add(X1, X2) -> active# X1, active# fact X -> fact# p X)
      (active# add(X1, X2) -> active# X1, active# fact X -> fact# active X)
      (active# add(X1, X2) -> active# X1, active# fact X -> p# X)
      (active# add(X1, X2) -> active# X1, active# fact X -> active# X)
      (active# add(X1, X2) -> active# X1, active# p X -> p# active X)
      (active# add(X1, X2) -> active# X1, active# p X -> active# X)
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
      (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
      (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
      (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
      (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X1)
      (active# if(X1, X2, X3) -> active# X1, active# zero X -> zero# active X)
      (active# if(X1, X2, X3) -> active# X1, active# zero X -> active# X)
      (active# if(X1, X2, X3) -> active# X1, active# s X -> s# active X)
      (active# if(X1, X2, X3) -> active# X1, active# s X -> active# X)
      (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> prod#(X1, active X2))
      (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> prod#(active X1, X2))
      (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> active# X1)
      (active# if(X1, X2, X3) -> active# X1, active# prod(X1, X2) -> active# X2)
      (active# if(X1, X2, X3) -> active# X1, active# prod(s X, Y) -> prod#(X, Y))
      (active# if(X1, X2, X3) -> active# X1, active# prod(s X, Y) -> add#(Y, prod(X, Y)))
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> if#(zero X, s 0(), prod(X, fact p X)))
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> zero# X)
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> s# 0())
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> prod#(X, fact p X))
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> fact# p X)
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> fact# active X)
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> p# X)
      (active# if(X1, X2, X3) -> active# X1, active# fact X -> active# X)
      (active# if(X1, X2, X3) -> active# X1, active# p X -> p# active X)
      (active# if(X1, X2, X3) -> active# X1, active# p X -> active# X)
      (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> active# X1)
      (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> active# X2)
      (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
      (active# if(X1, X2, X3) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
      (active# if(X1, X2, X3) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
      (active# if(X1, X2, X3) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     }
     STATUS:
      arrows: 0.865932
      SCCS (10):
       Scc:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Scc:
        {proper# if(X1, X2, X3) -> proper# X1,
         proper# if(X1, X2, X3) -> proper# X2,
         proper# if(X1, X2, X3) -> proper# X3,
                 proper# zero X -> proper# X,
                    proper# s X -> proper# X,
           proper# prod(X1, X2) -> proper# X1,
           proper# prod(X1, X2) -> proper# X2,
                 proper# fact X -> proper# X,
                    proper# p X -> proper# X,
            proper# add(X1, X2) -> proper# X1,
            proper# add(X1, X2) -> proper# X2}
       Scc:
        {active# if(X1, X2, X3) -> active# X1,
                 active# zero X -> active# X,
                    active# s X -> active# X,
           active# prod(X1, X2) -> active# X1,
           active# prod(X1, X2) -> active# X2,
                 active# fact X -> active# X,
                    active# p X -> active# X,
            active# add(X1, X2) -> active# X1,
            active# add(X1, X2) -> active# X2}
       Scc:
        {p# mark X -> p# X,
           p# ok X -> p# X}
       Scc:
        {fact# mark X -> fact# X,
           fact# ok X -> fact# X}
       Scc:
        { add#(X1, mark X2) -> add#(X1, X2),
          add#(mark X1, X2) -> add#(X1, X2),
         add#(ok X1, ok X2) -> add#(X1, X2)}
       Scc:
        { prod#(X1, mark X2) -> prod#(X1, X2),
          prod#(mark X1, X2) -> prod#(X1, X2),
         prod#(ok X1, ok X2) -> prod#(X1, X2)}
       Scc:
        {s# mark X -> s# X,
           s# ok X -> s# X}
       Scc:
        {zero# mark X -> zero# X,
           zero# ok X -> zero# X}
       Scc:
        {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
         if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
       
       SCC (2):
        Strict:
         {top# mark X -> top# proper X,
            top# ok X -> top# active X}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       
       SCC (11):
        Strict:
         {proper# if(X1, X2, X3) -> proper# X1,
          proper# if(X1, X2, X3) -> proper# X2,
          proper# if(X1, X2, X3) -> proper# X3,
                  proper# zero X -> proper# X,
                     proper# s X -> proper# X,
            proper# prod(X1, X2) -> proper# X1,
            proper# prod(X1, X2) -> proper# X2,
                  proper# fact X -> proper# X,
                     proper# p X -> proper# X,
             proper# add(X1, X2) -> proper# X1,
             proper# add(X1, X2) -> proper# X2}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       
       
       
       
       
       
       SCC (9):
        Strict:
         {active# if(X1, X2, X3) -> active# X1,
                  active# zero X -> active# X,
                     active# s X -> active# X,
            active# prod(X1, X2) -> active# X1,
            active# prod(X1, X2) -> active# X2,
                  active# fact X -> active# X,
                     active# p X -> active# X,
             active# add(X1, X2) -> active# X1,
             active# add(X1, X2) -> active# X2}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       
       
       
       
       SCC (2):
        Strict:
         {p# mark X -> p# X,
            p# ok X -> p# X}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       
       
       SCC (2):
        Strict:
         {fact# mark X -> fact# X,
            fact# ok X -> fact# X}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       
       
       
       
       SCC (3):
        Strict:
         { add#(X1, mark X2) -> add#(X1, X2),
           add#(mark X1, X2) -> add#(X1, X2),
          add#(ok X1, ok X2) -> add#(X1, X2)}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       
       
       SCC (3):
        Strict:
         { prod#(X1, mark X2) -> prod#(X1, X2),
           prod#(mark X1, X2) -> prod#(X1, X2),
          prod#(ok X1, ok X2) -> prod#(X1, X2)}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {s# mark X -> s# X,
            s# ok X -> s# X}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {zero# mark X -> zero# X,
            zero# ok X -> zero# X}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
          if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
        Weak:
        {     if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      zero mark X -> mark zero X,
                        zero ok X -> ok zero X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                prod(X1, mark X2) -> mark prod(X1, X2),
                prod(mark X1, X2) -> mark prod(X1, X2),
               prod(ok X1, ok X2) -> ok prod(X1, X2),
                      fact mark X -> mark fact X,
                        fact ok X -> ok fact X,
                         p mark X -> mark p X,
                           p ok X -> ok p X,
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                    active zero X -> zero active X,
                  active zero s X -> mark false(),
                  active zero 0() -> mark true(),
                       active s X -> s active X,
              active prod(X1, X2) -> prod(X1, active X2),
              active prod(X1, X2) -> prod(active X1, X2),
              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 fact X -> fact active X,
                       active p X -> p active X,
                     active p s X -> mark X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                 add(X1, mark X2) -> mark add(X1, X2),
                 add(mark X1, X2) -> mark add(X1, X2),
                add(ok X1, ok X2) -> ok add(X1, X2),
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper zero X -> zero proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
              proper prod(X1, X2) -> prod(proper X1, proper X2),
                    proper fact X -> fact proper X,
                       proper p X -> p proper X,
               proper add(X1, X2) -> add(proper X1, proper X2),
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        Open