MAYBE
Time: 0.110975
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())}
  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())}
      Fail
     
     
     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())}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2, x3) = x0 + 1,
        
        [plus](x0, x1) = x0 + 1,
        
        [times](x0, x1) = x0 + 1,
        
        [minus](x0, x1) = x0 + 1,
        
        [facIter](x0, x1) = 0,
        
        [s](x0) = x0 + 1,
        
        [p](x0) = x0 + 1,
        
        [isZero](x0) = x0 + 1,
        
        [factorial](x0) = 0,
        
        [0] = 1,
        
        [true] = 1,
        
        [false] = 1,
        
        [minus#](x0, x1) = x0
       Strict:
        minus#(x, s y) -> minus#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        factorial x -> facIter(x, s 0())
        0 + 0x >= 0 + 0x
        facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x))
        0 + 0x + 0y >= 2 + 1x + 0y
        if(false(), x, y, z) -> facIter(x, z)
        2 + 0x + 0y + 0z >= 0 + 0x + 0z
        if(true(), x, y, z) -> y
        2 + 0x + 0y + 0z >= 1y
        isZero s x -> false()
        2 + 1x >= 1
        isZero 0() -> true()
        2 >= 1
        minus(0(), x) -> 0()
        1 + 1x >= 1
        minus(x, s y) -> p minus(x, y)
        2 + 0x + 1y >= 2 + 0x + 1y
        minus(x, 0()) -> x
        2 + 0x >= 1x
        p s x -> x
        2 + 1x >= 1x
        p 0() -> 0()
        2 >= 1
        times(s x, y) -> plus(y, times(x, y))
        2 + 1x + 0y >= 1 + 0x + 1y
        times(0(), y) -> 0()
        2 + 0y >= 1
        plus(s x, y) -> s plus(x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
        plus(0(), x) -> x
        2 + 0x >= 1x
      Qed
    
    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())}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2, x3) = x0 + 1,
       
       [plus](x0, x1) = x0 + 1,
       
       [times](x0, x1) = x0 + 1,
       
       [minus](x0, x1) = x0 + 1,
       
       [facIter](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [p](x0) = x0 + 1,
       
       [isZero](x0) = x0 + 1,
       
       [factorial](x0) = 0,
       
       [0] = 1,
       
       [true] = 1,
       
       [false] = 1,
       
       [times#](x0, x1) = x0
      Strict:
       times#(s x, y) -> times#(x, y)
       1 + 1x + 0y >= 0 + 1x + 0y
      Weak:
       factorial x -> facIter(x, s 0())
       0 + 0x >= 0 + 0x
       facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x))
       0 + 0x + 0y >= 2 + 1x + 0y
       if(false(), x, y, z) -> facIter(x, z)
       2 + 0x + 0y + 0z >= 0 + 0x + 0z
       if(true(), x, y, z) -> y
       2 + 0x + 0y + 0z >= 1y
       isZero s x -> false()
       2 + 1x >= 1
       isZero 0() -> true()
       2 >= 1
       minus(0(), x) -> 0()
       1 + 1x >= 1
       minus(x, s y) -> p minus(x, y)
       2 + 0x + 1y >= 2 + 0x + 1y
       minus(x, 0()) -> x
       2 + 0x >= 1x
       p s x -> x
       2 + 1x >= 1x
       p 0() -> 0()
       2 >= 1
       times(s x, y) -> plus(y, times(x, y))
       2 + 1x + 0y >= 1 + 0x + 1y
       times(0(), y) -> 0()
       2 + 0y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 0y >= 2 + 1x + 0y
       plus(0(), x) -> x
       2 + 0x >= 1x
     Qed
    
    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())}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2, x3) = x0 + 1,
       
       [plus](x0, x1) = x0 + 1,
       
       [times](x0, x1) = x0 + 1,
       
       [minus](x0, x1) = x0 + 1,
       
       [facIter](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [p](x0) = x0 + 1,
       
       [isZero](x0) = x0 + 1,
       
       [factorial](x0) = 0,
       
       [0] = 1,
       
       [true] = 1,
       
       [false] = 1,
       
       [plus#](x0, x1) = x0
      Strict:
       plus#(s x, y) -> plus#(x, y)
       1 + 1x + 0y >= 0 + 1x + 0y
      Weak:
       factorial x -> facIter(x, s 0())
       0 + 0x >= 0 + 0x
       facIter(x, y) -> if(isZero x, minus(x, s 0()), y, times(y, x))
       0 + 0x + 0y >= 2 + 1x + 0y
       if(false(), x, y, z) -> facIter(x, z)
       2 + 0x + 0y + 0z >= 0 + 0x + 0z
       if(true(), x, y, z) -> y
       2 + 0x + 0y + 0z >= 1y
       isZero s x -> false()
       2 + 1x >= 1
       isZero 0() -> true()
       2 >= 1
       minus(0(), x) -> 0()
       1 + 1x >= 1
       minus(x, s y) -> p minus(x, y)
       2 + 0x + 1y >= 2 + 0x + 1y
       minus(x, 0()) -> x
       2 + 0x >= 1x
       p s x -> x
       2 + 1x >= 1x
       p 0() -> 0()
       2 >= 1
       times(s x, y) -> plus(y, times(x, y))
       2 + 1x + 0y >= 1 + 0x + 1y
       times(0(), y) -> 0()
       2 + 0y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 0y >= 2 + 1x + 0y
       plus(0(), x) -> x
       2 + 0x >= 1x
     Qed