MAYBE
Time: 0.010

Problem:
 Equations:
  
 TRS:
  timesAC(plusAC(x,y),z) -> plusAC(timesAC(x,z),timesAC(y,z))
  timesAC(z,plusAC(x,f(y))) -> timesAC(g(z,y),plusAC(x,a()))

Proof:
 Open