MAYBE
Time: 0.003948
TRS:
 {        plus(0(), x) -> x,
          plus(s x, y) -> s plus(x, y),
         times(0(), y) -> 0(),
         times(s x, y) -> plus(y, times(x, y)),
                 p 0() -> 0(),
                 p s x -> x,
         minus(x, 0()) -> x,
         minus(x, s y) -> p minus(x, y),
         minus(0(), x) -> 0(),
            isZero 0() -> true(),
            isZero s x -> false(),
   if(true(), x, y, z) -> y,
  if(false(), x, y, z) -> facIter(x, z),
         facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x)),
           factorial x -> facIter(x, s 0())}
 DP:
  DP:
   {        plus#(s x, y) -> plus#(x, y),
           times#(s x, y) -> plus#(y, times(x, y)),
           times#(s x, y) -> times#(x, y),
           minus#(x, s y) -> p# minus(x, y),
           minus#(x, s y) -> minus#(x, y),
    if#(false(), x, y, z) -> facIter#(x, z),
           facIter#(x, y) -> times#(y, x),
           facIter#(x, y) -> minus#(x, s 0()),
           facIter#(x, y) -> isZero# x,
           facIter#(x, y) -> if#(isZero x, minus(x, s 0()), y, times(y, x)),
             factorial# x -> facIter#(x, s 0())}
  TRS:
  {        plus(0(), x) -> x,
           plus(s x, y) -> s plus(x, y),
          times(0(), y) -> 0(),
          times(s x, y) -> plus(y, times(x, y)),
                  p 0() -> 0(),
                  p s x -> x,
          minus(x, 0()) -> x,
          minus(x, s y) -> p minus(x, y),
          minus(0(), x) -> 0(),
             isZero 0() -> true(),
             isZero s x -> false(),
    if(true(), x, y, z) -> y,
   if(false(), x, y, z) -> facIter(x, z),
          facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x)),
            factorial x -> facIter(x, s 0())}
  UR:
   { plus(0(), x) -> x,
     plus(s x, y) -> s plus(x, y),
    times(0(), y) -> 0(),
    times(s x, y) -> plus(y, times(x, y)),
            p 0() -> 0(),
            p s x -> x,
    minus(x, 0()) -> x,
    minus(x, s y) -> p minus(x, y),
    minus(0(), x) -> 0(),
       isZero 0() -> true(),
       isZero s x -> false(),
          a(w, v) -> w,
          a(w, v) -> v}
   EDG:
    {(plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> p# minus(x, y))
     (factorial# x -> facIter#(x, s 0()), facIter#(x, y) -> if#(isZero x, minus(x, s 0()), y, times(y, x)))
     (factorial# x -> facIter#(x, s 0()), facIter#(x, y) -> isZero# x)
     (factorial# x -> facIter#(x, s 0()), facIter#(x, y) -> minus#(x, s 0()))
     (factorial# x -> facIter#(x, s 0()), facIter#(x, y) -> times#(y, x))
     (facIter#(x, y) -> times#(y, x), times#(s x, y) -> times#(x, y))
     (facIter#(x, y) -> times#(y, x), times#(s x, y) -> plus#(y, times(x, y)))
     (if#(false(), x, y, z) -> facIter#(x, z), facIter#(x, y) -> times#(y, x))
     (if#(false(), x, y, z) -> facIter#(x, z), facIter#(x, y) -> minus#(x, s 0()))
     (if#(false(), x, y, z) -> facIter#(x, z), facIter#(x, y) -> isZero# x)
     (if#(false(), x, y, z) -> facIter#(x, z), facIter#(x, y) -> if#(isZero x, minus(x, s 0()), y, times(y, x)))
     (facIter#(x, y) -> if#(isZero x, minus(x, s 0()), y, times(y, x)), if#(false(), x, y, z) -> facIter#(x, z))
     (facIter#(x, y) -> minus#(x, s 0()), minus#(x, s y) -> p# minus(x, y))
     (facIter#(x, y) -> minus#(x, s 0()), minus#(x, s y) -> minus#(x, y))
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))}
    STATUS:
     arrows: 0.842975
     SCCS (4):
      Scc:
       {if#(false(), x, y, z) -> facIter#(x, z),
               facIter#(x, y) -> if#(isZero x, minus(x, s 0()), y, times(y, x))}
      Scc:
       {minus#(x, s y) -> minus#(x, y)}
      Scc:
       {times#(s x, y) -> times#(x, y)}
      Scc:
       {plus#(s x, y) -> plus#(x, y)}
      
      
      SCC (2):
       Strict:
        {if#(false(), x, y, z) -> facIter#(x, z),
                facIter#(x, y) -> if#(isZero x, minus(x, s 0()), y, times(y, x))}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(x, y),
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(x, y)),
                       p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
               minus(0(), x) -> 0(),
                  isZero 0() -> true(),
                  isZero s x -> false(),
         if(true(), x, y, z) -> y,
        if(false(), x, y, z) -> facIter(x, z),
               facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x)),
                 factorial x -> facIter(x, s 0())}
       Open
      
      
      SCC (1):
       Strict:
        {minus#(x, s y) -> minus#(x, y)}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(x, y),
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(x, y)),
                       p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
               minus(0(), x) -> 0(),
                  isZero 0() -> true(),
                  isZero s x -> false(),
         if(true(), x, y, z) -> y,
        if(false(), x, y, z) -> facIter(x, z),
               facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x)),
                 factorial x -> facIter(x, s 0())}
       Open
      
      SCC (1):
       Strict:
        {times#(s x, y) -> times#(x, y)}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(x, y),
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(x, y)),
                       p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
               minus(0(), x) -> 0(),
                  isZero 0() -> true(),
                  isZero s x -> false(),
         if(true(), x, y, z) -> y,
        if(false(), x, y, z) -> facIter(x, z),
               facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x)),
                 factorial x -> facIter(x, s 0())}
       Open
      
      SCC (1):
       Strict:
        {plus#(s x, y) -> plus#(x, y)}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(x, y),
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(x, y)),
                       p 0() -> 0(),
                       p s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> p minus(x, y),
               minus(0(), x) -> 0(),
                  isZero 0() -> true(),
                  isZero s x -> false(),
         if(true(), x, y, z) -> y,
        if(false(), x, y, z) -> facIter(x, z),
               facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x)),
                 factorial x -> facIter(x, s 0())}
       Open