MAYBE
Time: 0.002263
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:
  DP:
   {        +#(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()))}
  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()))}
  UR:
   {         +(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())),
               a(z, w) -> z,
               a(z, w) -> w}
   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))}
    STATUS:
     arrows: 0.850000
     SCCS (5):
      Scc:
       {iffact#(x, true()) -> fact# -(x, s 0()),
                   fact# x -> iffact#(x, ge(x, s s 0()))}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      Scc:
       {*#(x, s y) -> *#(x, y)}
      Scc:
       {+#(x, s y) -> +#(x, y)}
      
      SCC (2):
       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()))}
       Open
      
      SCC (1):
       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()))}
       Open
      
      SCC (1):
       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()))}
       Open
      
      SCC (1):
       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()))}
       Open
      
      SCC (1):
       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()))}
       Open