MAYBE

Problem:
 fac(0()) -> 1()
 fac(s(x)) -> *(s(x),fac(x))
 floop(0(),y) -> y
 floop(s(x),y) -> floop(x,*(s(x),y))
 *(x,0()) -> 0()
 *(x,s(y)) -> +(*(x,y),x)
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 1() -> s(0())
 fac(0()) -> s(0())

Proof:
 DP Processor:
  DPs:
   fac#(0()) -> 1#()
   fac#(s(x)) -> fac#(x)
   fac#(s(x)) -> *#(s(x),fac(x))
   floop#(s(x),y) -> *#(s(x),y)
   floop#(s(x),y) -> floop#(x,*(s(x),y))
   *#(x,s(y)) -> *#(x,y)
   *#(x,s(y)) -> +#(*(x,y),x)
   +#(x,s(y)) -> +#(x,y)
  TRS:
   fac(0()) -> 1()
   fac(s(x)) -> *(s(x),fac(x))
   floop(0(),y) -> y
   floop(s(x),y) -> floop(x,*(s(x),y))
   *(x,0()) -> 0()
   *(x,s(y)) -> +(*(x,y),x)
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   1() -> s(0())
   fac(0()) -> s(0())
  Usable Rule Processor:
   DPs:
    fac#(0()) -> 1#()
    fac#(s(x)) -> fac#(x)
    fac#(s(x)) -> *#(s(x),fac(x))
    floop#(s(x),y) -> *#(s(x),y)
    floop#(s(x),y) -> floop#(x,*(s(x),y))
    *#(x,s(y)) -> *#(x,y)
    *#(x,s(y)) -> +#(*(x,y),x)
    +#(x,s(y)) -> +#(x,y)
   TRS:
    f12(x,y) -> x
    f12(x,y) -> y
    fac(0()) -> 1()
    fac(s(x)) -> *(s(x),fac(x))
    fac(0()) -> s(0())
    1() -> s(0())
    *(x,0()) -> 0()
    *(x,s(y)) -> +(*(x,y),x)
    +(x,0()) -> x
    +(x,s(y)) -> s(+(x,y))
   EDG Processor:
    DPs:
     fac#(0()) -> 1#()
     fac#(s(x)) -> fac#(x)
     fac#(s(x)) -> *#(s(x),fac(x))
     floop#(s(x),y) -> *#(s(x),y)
     floop#(s(x),y) -> floop#(x,*(s(x),y))
     *#(x,s(y)) -> *#(x,y)
     *#(x,s(y)) -> +#(*(x,y),x)
     +#(x,s(y)) -> +#(x,y)
    TRS:
     f12(x,y) -> x
     f12(x,y) -> y
     fac(0()) -> 1()
     fac(s(x)) -> *(s(x),fac(x))
     fac(0()) -> s(0())
     1() -> s(0())
     *(x,0()) -> 0()
     *(x,s(y)) -> +(*(x,y),x)
     +(x,0()) -> x
     +(x,s(y)) -> s(+(x,y))
    graph:
     +#(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))
     floop#(s(x),y) -> *#(s(x),y) -> *#(x,s(y)) -> *#(x,y)
     floop#(s(x),y) -> *#(s(x),y) -> *#(x,s(y)) -> +#(*(x,y),x)
     *#(x,s(y)) -> +#(*(x,y),x) -> +#(x,s(y)) -> +#(x,y)
     *#(x,s(y)) -> *#(x,y) -> *#(x,s(y)) -> *#(x,y)
     *#(x,s(y)) -> *#(x,y) -> *#(x,s(y)) -> +#(*(x,y),x)
     fac#(s(x)) -> *#(s(x),fac(x)) -> *#(x,s(y)) -> *#(x,y)
     fac#(s(x)) -> *#(s(x),fac(x)) -> *#(x,s(y)) -> +#(*(x,y),x)
     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))
    Restore Modifier:
     DPs:
      fac#(0()) -> 1#()
      fac#(s(x)) -> fac#(x)
      fac#(s(x)) -> *#(s(x),fac(x))
      floop#(s(x),y) -> *#(s(x),y)
      floop#(s(x),y) -> floop#(x,*(s(x),y))
      *#(x,s(y)) -> *#(x,y)
      *#(x,s(y)) -> +#(*(x,y),x)
      +#(x,s(y)) -> +#(x,y)
     TRS:
      fac(0()) -> 1()
      fac(s(x)) -> *(s(x),fac(x))
      floop(0(),y) -> y
      floop(s(x),y) -> floop(x,*(s(x),y))
      *(x,0()) -> 0()
      *(x,s(y)) -> +(*(x,y),x)
      +(x,0()) -> x
      +(x,s(y)) -> s(+(x,y))
      1() -> s(0())
      fac(0()) -> s(0())
     SCC Processor:
      #sccs: 4
      #rules: 4
      #arcs: 13/64
      DPs:
       fac#(s(x)) -> fac#(x)
      TRS:
       fac(0()) -> 1()
       fac(s(x)) -> *(s(x),fac(x))
       floop(0(),y) -> y
       floop(s(x),y) -> floop(x,*(s(x),y))
       *(x,0()) -> 0()
       *(x,s(y)) -> +(*(x,y),x)
       +(x,0()) -> x
       +(x,s(y)) -> s(+(x,y))
       1() -> s(0())
       fac(0()) -> s(0())
      Open
      
      DPs:
       floop#(s(x),y) -> floop#(x,*(s(x),y))
      TRS:
       fac(0()) -> 1()
       fac(s(x)) -> *(s(x),fac(x))
       floop(0(),y) -> y
       floop(s(x),y) -> floop(x,*(s(x),y))
       *(x,0()) -> 0()
       *(x,s(y)) -> +(*(x,y),x)
       +(x,0()) -> x
       +(x,s(y)) -> s(+(x,y))
       1() -> s(0())
       fac(0()) -> s(0())
      Open
      
      DPs:
       *#(x,s(y)) -> *#(x,y)
      TRS:
       fac(0()) -> 1()
       fac(s(x)) -> *(s(x),fac(x))
       floop(0(),y) -> y
       floop(s(x),y) -> floop(x,*(s(x),y))
       *(x,0()) -> 0()
       *(x,s(y)) -> +(*(x,y),x)
       +(x,0()) -> x
       +(x,s(y)) -> s(+(x,y))
       1() -> s(0())
       fac(0()) -> s(0())
      Open
      
      DPs:
       +#(x,s(y)) -> +#(x,y)
      TRS:
       fac(0()) -> 1()
       fac(s(x)) -> *(s(x),fac(x))
       floop(0(),y) -> y
       floop(s(x),y) -> floop(x,*(s(x),y))
       *(x,0()) -> 0()
       *(x,s(y)) -> +(*(x,y),x)
       +(x,0()) -> x
       +(x,s(y)) -> s(+(x,y))
       1() -> s(0())
       fac(0()) -> s(0())
      Open