MAYBE
Time: 0.168352
TRS:
 {          1() -> s 0(),
        fac 0() -> 1(),
        fac 0() -> s 0(),
        fac s x -> *(s x, fac x),
      *(x, 0()) -> 0(),
      *(x, s y) -> +(*(x, y), x),
  floop(0(), y) -> y,
  floop(s x, y) -> floop(x, *(s x, y)),
      +(x, 0()) -> x,
      +(x, s y) -> s +(x, y)}
 DP:
  DP:
   {      fac# 0() -> 1#(),
          fac# s x -> fac# x,
          fac# s x -> *#(s x, fac x),
        *#(x, s y) -> *#(x, y),
        *#(x, s y) -> +#(*(x, y), x),
    floop#(s x, y) -> *#(s x, y),
    floop#(s x, y) -> floop#(x, *(s x, y)),
        +#(x, s y) -> +#(x, y)}
  TRS:
  {          1() -> s 0(),
         fac 0() -> 1(),
         fac 0() -> s 0(),
         fac s x -> *(s x, fac x),
       *(x, 0()) -> 0(),
       *(x, s y) -> +(*(x, y), x),
   floop(0(), y) -> y,
   floop(s x, y) -> floop(x, *(s x, y)),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y)}
  UR:
   {      1() -> s 0(),
      fac 0() -> 1(),
      fac 0() -> s 0(),
      fac s x -> *(s x, fac x),
    *(x, 0()) -> 0(),
    *(x, s y) -> +(*(x, y), x),
    +(x, 0()) -> x,
    +(x, s y) -> s +(x, y),
      a(z, w) -> z,
      a(z, w) -> w}
   EDG:
    {(floop#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(*(x, y), x))
     (floop#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y))
     (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x))
     (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y))
     (fac# s x -> *#(s x, fac x), *#(x, s y) -> +#(*(x, y), x))
     (fac# s x -> *#(s x, fac x), *#(x, s y) -> *#(x, y))
     (*#(x, s y) -> +#(*(x, y), x), +#(x, s y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> *#(s x, y))
     (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> floop#(x, *(s x, y)))
     (fac# s x -> fac# x, fac# 0() -> 1#())
     (fac# s x -> fac# x, fac# s x -> fac# x)
     (fac# s x -> fac# x, fac# s x -> *#(s x, fac x))}
    STATUS:
     arrows: 0.796875
     SCCS (4):
      Scc:
       {floop#(s x, y) -> floop#(x, *(s x, y))}
      Scc:
       {fac# s x -> fac# x}
      Scc:
       {*#(x, s y) -> *#(x, y)}
      Scc:
       {+#(x, s y) -> +#(x, y)}
      
      SCC (1):
       Strict:
        {floop#(s x, y) -> floop#(x, *(s x, y))}
       Weak:
       {          1() -> s 0(),
              fac 0() -> 1(),
              fac 0() -> s 0(),
              fac s x -> *(s x, fac x),
            *(x, 0()) -> 0(),
            *(x, s y) -> +(*(x, y), x),
        floop(0(), y) -> y,
        floop(s x, y) -> floop(x, *(s x, y)),
            +(x, 0()) -> x,
            +(x, s y) -> s +(x, y)}
       Open
      
      SCC (1):
       Strict:
        {fac# s x -> fac# x}
       Weak:
       {          1() -> s 0(),
              fac 0() -> 1(),
              fac 0() -> s 0(),
              fac s x -> *(s x, fac x),
            *(x, 0()) -> 0(),
            *(x, s y) -> +(*(x, y), x),
        floop(0(), y) -> y,
        floop(s x, y) -> floop(x, *(s x, y)),
            +(x, 0()) -> x,
            +(x, s y) -> s +(x, y)}
       Open
      
      SCC (1):
       Strict:
        {*#(x, s y) -> *#(x, y)}
       Weak:
       {          1() -> s 0(),
              fac 0() -> 1(),
              fac 0() -> s 0(),
              fac s x -> *(s x, fac x),
            *(x, 0()) -> 0(),
            *(x, s y) -> +(*(x, y), x),
        floop(0(), y) -> y,
        floop(s x, y) -> floop(x, *(s x, y)),
            +(x, 0()) -> x,
            +(x, s y) -> s +(x, y)}
       Open
      
      SCC (1):
       Strict:
        {+#(x, s y) -> +#(x, y)}
       Weak:
       {          1() -> s 0(),
              fac 0() -> 1(),
              fac 0() -> s 0(),
              fac s x -> *(s x, fac x),
            *(x, 0()) -> 0(),
            *(x, s y) -> +(*(x, y), x),
        floop(0(), y) -> y,
        floop(s x, y) -> floop(x, *(s x, y)),
            +(x, 0()) -> x,
            +(x, s y) -> s +(x, y)}
       Open