MAYBE
TRS:
 {         +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y)),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
          ge(x, 0()) -> true(),
       ge(0(), s(y)) -> false(),
      ge(s(x), s(y)) -> ge(x, y),
           -(x, 0()) -> x,
       -(s(x), s(y)) -> -(x, y),
   iffact(x, true()) -> *(x, fact(-(x, s(0())))),
  iffact(x, false()) -> s(0()),
             fact(x) -> iffact(x, ge(x, s(s(0()))))}
 DP:
  Strict:
   {       +#(x, s(y)) -> +#(x, y),
           *#(x, s(y)) -> +#(*(x, y), x),
           *#(x, s(y)) -> *#(x, y),
       ge#(s(x), s(y)) -> ge#(x, y),
        -#(s(x), s(y)) -> -#(x, y),
    iffact#(x, true()) -> *#(x, fact(-(x, s(0())))),
    iffact#(x, true()) -> -#(x, s(0())),
    iffact#(x, true()) -> fact#(-(x, s(0()))),
              fact#(x) -> ge#(x, s(s(0()))),
              fact#(x) -> iffact#(x, ge(x, s(s(0()))))}
  Weak:
  {         +(x, 0()) -> x,
           +(x, s(y)) -> s(+(x, y)),
            *(x, 0()) -> 0(),
           *(x, s(y)) -> +(*(x, y), x),
           ge(x, 0()) -> true(),
        ge(0(), s(y)) -> false(),
       ge(s(x), s(y)) -> ge(x, y),
            -(x, 0()) -> x,
        -(s(x), s(y)) -> -(x, y),
    iffact(x, true()) -> *(x, fact(-(x, s(0())))),
   iffact(x, false()) -> s(0()),
              fact(x) -> iffact(x, ge(x, s(s(0()))))}
  EDG:
   {(fact#(x) -> iffact#(x, ge(x, s(s(0())))), iffact#(x, true()) -> fact#(-(x, s(0()))))
    (fact#(x) -> iffact#(x, ge(x, s(s(0())))), iffact#(x, true()) -> -#(x, s(0())))
    (fact#(x) -> iffact#(x, ge(x, s(s(0())))), iffact#(x, true()) -> *#(x, fact(-(x, s(0())))))
    (fact#(x) -> ge#(x, s(s(0()))), ge#(s(x), s(y)) -> ge#(x, y))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> *#(x, y))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> +#(*(x, y), x))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (iffact#(x, true()) -> fact#(-(x, s(0()))), fact#(x) -> iffact#(x, ge(x, s(s(0())))))
    (iffact#(x, true()) -> fact#(-(x, s(0()))), fact#(x) -> ge#(x, s(s(0()))))
    (*#(x, s(y)) -> +#(*(x, y), x), +#(x, s(y)) -> +#(x, y))
    (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (iffact#(x, true()) -> -#(x, s(0())), -#(s(x), s(y)) -> -#(x, y))
    (iffact#(x, true()) -> *#(x, fact(-(x, s(0())))), *#(x, s(y)) -> +#(*(x, y), x))
    (iffact#(x, true()) -> *#(x, fact(-(x, s(0())))), *#(x, s(y)) -> *#(x, y))}
   SCCS:
    Scc:
     {iffact#(x, true()) -> fact#(-(x, s(0()))),
                fact#(x) -> iffact#(x, ge(x, s(s(0()))))}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    Scc:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    Scc:
     {*#(x, s(y)) -> *#(x, y)}
    Scc:
     {+#(x, s(y)) -> +#(x, y)}
    SCC:
     Strict:
      {iffact#(x, true()) -> fact#(-(x, s(0()))),
                 fact#(x) -> iffact#(x, ge(x, s(s(0()))))}
     Weak:
     {         +(x, 0()) -> x,
              +(x, s(y)) -> s(+(x, y)),
               *(x, 0()) -> 0(),
              *(x, s(y)) -> +(*(x, y), x),
              ge(x, 0()) -> true(),
           ge(0(), s(y)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
               -(x, 0()) -> x,
           -(s(x), s(y)) -> -(x, y),
       iffact(x, true()) -> *(x, fact(-(x, s(0())))),
      iffact(x, false()) -> s(0()),
                 fact(x) -> iffact(x, ge(x, s(s(0()))))}
     Fail
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {         +(x, 0()) -> x,
              +(x, s(y)) -> s(+(x, y)),
               *(x, 0()) -> 0(),
              *(x, s(y)) -> +(*(x, y), x),
              ge(x, 0()) -> true(),
           ge(0(), s(y)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
               -(x, 0()) -> x,
           -(s(x), s(y)) -> -(x, y),
       iffact(x, true()) -> *(x, fact(-(x, s(0())))),
      iffact(x, false()) -> s(0()),
                 fact(x) -> iffact(x, ge(x, s(s(0()))))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {ge#(s(x), s(y)) -> ge#(x, y)}
     Weak:
     {         +(x, 0()) -> x,
              +(x, s(y)) -> s(+(x, y)),
               *(x, 0()) -> 0(),
              *(x, s(y)) -> +(*(x, y), x),
              ge(x, 0()) -> true(),
           ge(0(), s(y)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
               -(x, 0()) -> x,
           -(s(x), s(y)) -> -(x, y),
       iffact(x, true()) -> *(x, fact(-(x, s(0())))),
      iffact(x, false()) -> s(0()),
                 fact(x) -> iffact(x, ge(x, s(s(0()))))}
     SPSC:
      Simple Projection:
       pi(ge#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(x, s(y)) -> *#(x, y)}
     Weak:
     {         +(x, 0()) -> x,
              +(x, s(y)) -> s(+(x, y)),
               *(x, 0()) -> 0(),
              *(x, s(y)) -> +(*(x, y), x),
              ge(x, 0()) -> true(),
           ge(0(), s(y)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
               -(x, 0()) -> x,
           -(s(x), s(y)) -> -(x, y),
       iffact(x, true()) -> *(x, fact(-(x, s(0())))),
      iffact(x, false()) -> s(0()),
                 fact(x) -> iffact(x, ge(x, s(s(0()))))}
     SPSC:
      Simple Projection:
       pi(*#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {+#(x, s(y)) -> +#(x, y)}
     Weak:
     {         +(x, 0()) -> x,
              +(x, s(y)) -> s(+(x, y)),
               *(x, 0()) -> 0(),
              *(x, s(y)) -> +(*(x, y), x),
              ge(x, 0()) -> true(),
           ge(0(), s(y)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
               -(x, 0()) -> x,
           -(s(x), s(y)) -> -(x, y),
       iffact(x, true()) -> *(x, fact(-(x, s(0())))),
      iffact(x, false()) -> s(0()),
                 fact(x) -> iffact(x, ge(x, s(s(0()))))}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed