MAYBE
Time: 0.036

Problem:
 Equations:
  timesAC(timesAC(x1,x2),x3) -> timesAC(x1,timesAC(x2,x3))
  timesAC(x1,x2) -> timesAC(x2,x1)
  timesAC(x1,timesAC(x2,x3)) -> timesAC(timesAC(x1,x2),x3)
  timesAC(x2,x1) -> timesAC(x1,x2)
 TRS:
  p(s(x)) -> x
  fac(0()) -> s(0())
  fac(s(x)) -> timesAC(s(x),fac(p(s(x))))

Proof:
 DP Processor:
  Equations#:
   times{AC,#}(timesAC(x1,x2),x3) -> times{AC,#}(x1,timesAC(x2,x3))
   times{AC,#}(x1,x2) -> times{AC,#}(x2,x1)
   times{AC,#}(x1,timesAC(x2,x3)) -> times{AC,#}(timesAC(x1,x2),x3)
   times{AC,#}(x2,x1) -> times{AC,#}(x1,x2)
  DPs:
   fac#(s(x)) -> p#(s(x))
   fac#(s(x)) -> fac#(p(s(x)))
  Equations:
   timesAC(timesAC(x1,x2),x3) -> timesAC(x1,timesAC(x2,x3))
   timesAC(x1,x2) -> timesAC(x2,x1)
   timesAC(x1,timesAC(x2,x3)) -> timesAC(timesAC(x1,x2),x3)
   timesAC(x2,x1) -> timesAC(x1,x2)
  TRS:
   p(s(x)) -> x
   fac(0()) -> s(0())
   fac(s(x)) -> timesAC(s(x),fac(p(s(x))))
  S:
   times{AC,#}(timesAC(x4,x5),x6) -> times{AC,#}(x4,x5)
   times{AC,#}(x4,timesAC(x5,x6)) -> times{AC,#}(x5,x6)
  AC-EDG Processor:
   Equations#:
    times{AC,#}(timesAC(x1,x2),x3) -> times{AC,#}(x1,timesAC(x2,x3))
    times{AC,#}(x1,x2) -> times{AC,#}(x2,x1)
    times{AC,#}(x1,timesAC(x2,x3)) -> times{AC,#}(timesAC(x1,x2),x3)
    times{AC,#}(x2,x1) -> times{AC,#}(x1,x2)
   DPs:
    fac#(s(x)) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x)))
   Equations:
    timesAC(timesAC(x1,x2),x3) -> timesAC(x1,timesAC(x2,x3))
    timesAC(x1,x2) -> timesAC(x2,x1)
    timesAC(x1,timesAC(x2,x3)) -> timesAC(timesAC(x1,x2),x3)
    timesAC(x2,x1) -> timesAC(x1,x2)
   TRS:
    p(s(x)) -> x
    fac(0()) -> s(0())
    fac(s(x)) -> timesAC(s(x),fac(p(s(x))))
   S:
    times{AC,#}(timesAC(x4,x5),x6) -> times{AC,#}(x4,x5)
    times{AC,#}(x4,timesAC(x5,x6)) -> times{AC,#}(x5,x6)
   Open