MAYBE
Time: 1.217223
TRS:
 {        if(true(), X, Y) -> activate X,
         if(false(), X, Y) -> activate Y,
                  zero 0() -> true(),
                  zero s X -> false(),
                    fact X -> if(zero X, n__s 0(), n__prod(X, fact p X)),
                     p s X -> X,
               add(0(), X) -> X,
               add(s X, Y) -> s add(X, Y),
                       s X -> n__s X,
              prod(X1, X2) -> n__prod(X1, X2),
              prod(0(), X) -> 0(),
              prod(s X, Y) -> add(Y, prod(X, Y)),
                activate X -> X,
           activate n__s X -> s X,
  activate n__prod(X1, X2) -> prod(X1, X2)}
 DP:
  DP:
   {        if#(true(), X, Y) -> activate# X,
           if#(false(), X, Y) -> activate# Y,
                      fact# X -> if#(zero X, n__s 0(), n__prod(X, fact p X)),
                      fact# X -> zero# X,
                      fact# X -> fact# p X,
                      fact# X -> p# X,
                 add#(s X, Y) -> add#(X, Y),
                 add#(s X, Y) -> s# add(X, Y),
                prod#(s X, Y) -> add#(Y, prod(X, Y)),
                prod#(s X, Y) -> prod#(X, Y),
             activate# n__s X -> s# X,
    activate# n__prod(X1, X2) -> prod#(X1, X2)}
  TRS:
  {        if(true(), X, Y) -> activate X,
          if(false(), X, Y) -> activate Y,
                   zero 0() -> true(),
                   zero s X -> false(),
                     fact X -> if(zero X, n__s 0(), n__prod(X, fact p X)),
                      p s X -> X,
                add(0(), X) -> X,
                add(s X, Y) -> s add(X, Y),
                        s X -> n__s X,
               prod(X1, X2) -> n__prod(X1, X2),
               prod(0(), X) -> 0(),
               prod(s X, Y) -> add(Y, prod(X, Y)),
                 activate X -> X,
            activate n__s X -> s X,
   activate n__prod(X1, X2) -> prod(X1, X2)}
  UR:
   {        if(true(), X, Y) -> activate X,
           if(false(), X, Y) -> activate Y,
                    zero 0() -> true(),
                    zero s X -> false(),
                      fact X -> if(zero X, n__s 0(), n__prod(X, fact p X)),
                       p s X -> X,
                 add(0(), X) -> X,
                 add(s X, Y) -> s add(X, Y),
                         s X -> n__s X,
                prod(X1, X2) -> n__prod(X1, X2),
                prod(0(), X) -> 0(),
                prod(s X, Y) -> add(Y, prod(X, Y)),
                  activate X -> X,
             activate n__s X -> s X,
    activate n__prod(X1, X2) -> prod(X1, X2),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(if#(false(), X, Y) -> activate# Y, activate# n__prod(X1, X2) -> prod#(X1, X2))
     (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# X)
     (prod#(s X, Y) -> add#(Y, prod(X, Y)), add#(s X, Y) -> s# add(X, Y))
     (prod#(s X, Y) -> add#(Y, prod(X, Y)), add#(s X, Y) -> add#(X, Y))
     (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> s# add(X, Y))
     (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y))
     (if#(true(), X, Y) -> activate# X, activate# n__prod(X1, X2) -> prod#(X1, X2))
     (if#(true(), X, Y) -> activate# X, activate# n__s X -> s# X)
     (fact# X -> fact# p X, fact# X -> p# X)
     (fact# X -> fact# p X, fact# X -> fact# p X)
     (fact# X -> fact# p X, fact# X -> zero# X)
     (fact# X -> fact# p X, fact# X -> if#(zero X, n__s 0(), n__prod(X, fact p X)))
     (prod#(s X, Y) -> prod#(X, Y), prod#(s X, Y) -> add#(Y, prod(X, Y)))
     (prod#(s X, Y) -> prod#(X, Y), prod#(s X, Y) -> prod#(X, Y))
     (fact# X -> if#(zero X, n__s 0(), n__prod(X, fact p X)), if#(true(), X, Y) -> activate# X)
     (fact# X -> if#(zero X, n__s 0(), n__prod(X, fact p X)), if#(false(), X, Y) -> activate# Y)
     (activate# n__prod(X1, X2) -> prod#(X1, X2), prod#(s X, Y) -> add#(Y, prod(X, Y)))
     (activate# n__prod(X1, X2) -> prod#(X1, X2), prod#(s X, Y) -> prod#(X, Y))}
    STATUS:
     arrows: 0.875000
     SCCS (3):
      Scc:
       {fact# X -> fact# p X}
      Scc:
       {prod#(s X, Y) -> prod#(X, Y)}
      Scc:
       {add#(s X, Y) -> add#(X, Y)}
      
      SCC (1):
       Strict:
        {fact# X -> fact# p X}
       Weak:
       {        if(true(), X, Y) -> activate X,
               if(false(), X, Y) -> activate Y,
                        zero 0() -> true(),
                        zero s X -> false(),
                          fact X -> if(zero X, n__s 0(), n__prod(X, fact p X)),
                           p s X -> X,
                     add(0(), X) -> X,
                     add(s X, Y) -> s add(X, Y),
                             s X -> n__s X,
                    prod(X1, X2) -> n__prod(X1, X2),
                    prod(0(), X) -> 0(),
                    prod(s X, Y) -> add(Y, prod(X, Y)),
                      activate X -> X,
                 activate n__s X -> s X,
        activate n__prod(X1, X2) -> prod(X1, X2)}
       Open
      
      
      
      
      
      
      SCC (1):
       Strict:
        {prod#(s X, Y) -> prod#(X, Y)}
       Weak:
       {        if(true(), X, Y) -> activate X,
               if(false(), X, Y) -> activate Y,
                        zero 0() -> true(),
                        zero s X -> false(),
                          fact X -> if(zero X, n__s 0(), n__prod(X, fact p X)),
                           p s X -> X,
                     add(0(), X) -> X,
                     add(s X, Y) -> s add(X, Y),
                             s X -> n__s X,
                    prod(X1, X2) -> n__prod(X1, X2),
                    prod(0(), X) -> 0(),
                    prod(s X, Y) -> add(Y, prod(X, Y)),
                      activate X -> X,
                 activate n__s X -> s X,
        activate n__prod(X1, X2) -> prod(X1, X2)}
       Open
      
      SCC (1):
       Strict:
        {add#(s X, Y) -> add#(X, Y)}
       Weak:
       {        if(true(), X, Y) -> activate X,
               if(false(), X, Y) -> activate Y,
                        zero 0() -> true(),
                        zero s X -> false(),
                          fact X -> if(zero X, n__s 0(), n__prod(X, fact p X)),
                           p s X -> X,
                     add(0(), X) -> X,
                     add(s X, Y) -> s add(X, Y),
                             s X -> n__s X,
                    prod(X1, X2) -> n__prod(X1, X2),
                    prod(0(), X) -> 0(),
                    prod(s X, Y) -> add(Y, prod(X, Y)),
                      activate X -> X,
                 activate n__s X -> s X,
        activate n__prod(X1, X2) -> prod(X1, X2)}
       Open