MAYBE

Problem:
 fac(s(x)) -> *(fac(p(s(x))),s(x))
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))

Proof:
 DP Processor:
  DPs:
   fac#(s(x)) -> p#(s(x))
   fac#(s(x)) -> fac#(p(s(x)))
   p#(s(s(x))) -> p#(s(x))
  TRS:
   fac(s(x)) -> *(fac(p(s(x))),s(x))
   p(s(0())) -> 0()
   p(s(s(x))) -> s(p(s(x)))
  CDG Processor:
   DPs:
    fac#(s(x)) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x)))
    p#(s(s(x))) -> p#(s(x))
   TRS:
    fac(s(x)) -> *(fac(p(s(x))),s(x))
    p(s(0())) -> 0()
    p(s(s(x))) -> s(p(s(x)))
   graph:
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    fac#(s(x)) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x))) -> fac#(s(x)) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x))) -> fac#(s(x)) -> fac#(p(s(x)))
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     fac#(s(x)) -> fac#(p(s(x)))
    TRS:
     fac(s(x)) -> *(fac(p(s(x))),s(x))
     p(s(0())) -> 0()
     p(s(s(x))) -> s(p(s(x)))
    Open
    
    DPs:
     p#(s(s(x))) -> p#(s(x))
    TRS:
     fac(s(x)) -> *(fac(p(s(x))),s(x))
     p(s(0())) -> 0()
     p(s(s(x))) -> s(p(s(x)))
    Open