YES
Time: 0.539

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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
               [1 4]     [3]
   [fac](x0) = [1 8]x0 + [2],
   
         [1]
   [0] = [0],
   
             [4 0]     [2]
   [p](x0) = [1 0]x0 + [0],
   
             [1 1]     [0]
   [s](x0) = [2 3]x0 + [1],
   
                                 [0]
   [timesAC](x0, x1) = x0 + x1 + [3]
  orientation:
             [4 4]    [2]         
   p(s(x)) = [1 1]x + [0] >= x = x
   
              [4]    [1]         
   fac(0()) = [3] >= [3] = s(0())
   
               [9  13]    [7 ]    [9  9 ]    [5]                             
   fac(s(x)) = [17 25]x + [10] >= [14 15]x + [8] = timesAC(s(x),fac(p(s(x))))
  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:
    
  Qed