YES
Time: 0.068172
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)}
  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))}
   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))}
    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))}
     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)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [*](x0, x1) = 0,
           
           [floop](x0, x1) = 0,
           
           [+](x0, x1) = 0,
           
           [fac](x0) = x0 + 1,
           
           [s](x0) = x0 + 1,
           
           [1] = 0,
           
           [0] = 1,
           
           [floop#](x0, x1) = x0
          Strict:
           floop#(s x, y) -> floop#(x, *(s x, y))
           1 + 1x + 0y >= 0 + 1x + 0y
          Weak:
           +(x, s y) -> s +(x, y)
           0 + 0x + 0y >= 1 + 0x + 0y
           +(x, 0()) -> x
           0 + 0x >= 1x
           floop(s x, y) -> floop(x, *(s x, y))
           0 + 0x + 0y >= 0 + 0x + 0y
           floop(0(), y) -> y
           0 + 0y >= 1y
           *(x, s y) -> +(*(x, y), x)
           0 + 0x + 0y >= 0 + 0x + 0y
           *(x, 0()) -> 0()
           0 + 0x >= 1
           fac s x -> *(s x, fac x)
           2 + 1x >= 0 + 0x
           fac 0() -> s 0()
           2 >= 2
           fac 0() -> 1()
           2 >= 0
           1() -> s 0()
           0 >= 2
         Qed
       
       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)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [*](x0, x1) = 0,
          
          [floop](x0, x1) = 0,
          
          [+](x0, x1) = 0,
          
          [fac](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [1] = 0,
          
          [0] = 1,
          
          [fac#](x0) = x0
         Strict:
          fac# s x -> fac# x
          1 + 1x >= 0 + 1x
         Weak:
          +(x, s y) -> s +(x, y)
          0 + 0x + 0y >= 1 + 0x + 0y
          +(x, 0()) -> x
          0 + 0x >= 1x
          floop(s x, y) -> floop(x, *(s x, y))
          0 + 0x + 0y >= 0 + 0x + 0y
          floop(0(), y) -> y
          0 + 0y >= 1y
          *(x, s y) -> +(*(x, y), x)
          0 + 0x + 0y >= 0 + 0x + 0y
          *(x, 0()) -> 0()
          0 + 0x >= 1
          fac s x -> *(s x, fac x)
          2 + 1x >= 0 + 0x
          fac 0() -> s 0()
          2 >= 2
          fac 0() -> 1()
          2 >= 0
          1() -> s 0()
          0 >= 2
        Qed
       
       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)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [*](x0, x1) = 0,
          
          [floop](x0, x1) = 0,
          
          [+](x0, x1) = 0,
          
          [fac](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [1] = 0,
          
          [0] = 1,
          
          [*#](x0, x1) = x0
         Strict:
          *#(x, s y) -> *#(x, y)
          1 + 0x + 1y >= 0 + 0x + 1y
         Weak:
          +(x, s y) -> s +(x, y)
          0 + 0x + 0y >= 1 + 0x + 0y
          +(x, 0()) -> x
          0 + 0x >= 1x
          floop(s x, y) -> floop(x, *(s x, y))
          0 + 0x + 0y >= 0 + 0x + 0y
          floop(0(), y) -> y
          0 + 0y >= 1y
          *(x, s y) -> +(*(x, y), x)
          0 + 0x + 0y >= 0 + 0x + 0y
          *(x, 0()) -> 0()
          0 + 0x >= 1
          fac s x -> *(s x, fac x)
          2 + 1x >= 0 + 0x
          fac 0() -> s 0()
          2 >= 2
          fac 0() -> 1()
          2 >= 0
          1() -> s 0()
          0 >= 2
        Qed
      
      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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [*](x0, x1) = 0,
         
         [floop](x0, x1) = 0,
         
         [+](x0, x1) = 0,
         
         [fac](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [1] = 0,
         
         [0] = 1,
         
         [+#](x0, x1) = x0
        Strict:
         +#(x, s y) -> +#(x, y)
         1 + 0x + 1y >= 0 + 0x + 1y
        Weak:
         +(x, s y) -> s +(x, y)
         0 + 0x + 0y >= 1 + 0x + 0y
         +(x, 0()) -> x
         0 + 0x >= 1x
         floop(s x, y) -> floop(x, *(s x, y))
         0 + 0x + 0y >= 0 + 0x + 0y
         floop(0(), y) -> y
         0 + 0y >= 1y
         *(x, s y) -> +(*(x, y), x)
         0 + 0x + 0y >= 0 + 0x + 0y
         *(x, 0()) -> 0()
         0 + 0x >= 1
         fac s x -> *(s x, fac x)
         2 + 1x >= 0 + 0x
         fac 0() -> s 0()
         2 >= 2
         fac 0() -> 1()
         2 >= 0
         1() -> s 0()
         0 >= 2
       Qed