MAYBE
Time: 0.733

Problem:
 Equations:
  fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
  fAC(x3,x4) -> fAC(x4,x3)
  fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
  fAC(x4,x3) -> fAC(x3,x4)
 TRS:
  fAC(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
  fAC(one(),x) -> x
  phi(one(),x) -> x
  fAC(i(x),x) -> one()
  i(one()) -> one()
  i(i(x)) -> x
  phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
  fAC(i(fAC(x,y1)),y1) -> i(x)
  i(fAC(i(y1),x)) -> fAC(i(x),y1)
  fAC(i(x),i(y1)) -> i(fAC(x,y1))

Proof:
 DP Processor:
  Equations#:
   f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
   f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
   f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
   f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
  DPs:
   f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(x,y1)
   f{AC,#}(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
   f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(i(fAC(x,y1)),y2)
   phi#(x,phi(y1,y2)) -> f{AC,#}(x,y1)
   phi#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
   f{AC,#}(i(fAC(x,y1)),y1) -> i#(x)
   i#(fAC(i(y1),x)) -> i#(x)
   i#(fAC(i(y1),x)) -> f{AC,#}(i(x),y1)
   f{AC,#}(i(x),i(y1)) -> f{AC,#}(x,y1)
   f{AC,#}(i(x),i(y1)) -> i#(fAC(x,y1))
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x,y1)
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(i(fAC(x,y1)),y2)
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x6,fAC(i(fAC(x,y1)),y2))
   f{AC,#}(x7,fAC(one(),x)) -> f{AC,#}(x7,x)
   f{AC,#}(x8,fAC(i(x),x)) -> f{AC,#}(x8,one())
   f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
   f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> f{AC,#}(x9,i(x))
   f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x,y1)
   f{AC,#}(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
   f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x10,i(fAC(x,y1)))
  Equations:
   fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
   fAC(x3,x4) -> fAC(x4,x3)
   fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
   fAC(x4,x3) -> fAC(x3,x4)
  TRS:
   fAC(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
   fAC(one(),x) -> x
   phi(one(),x) -> x
   fAC(i(x),x) -> one()
   i(one()) -> one()
   i(i(x)) -> x
   phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
   fAC(i(fAC(x,y1)),y1) -> i(x)
   i(fAC(i(y1),x)) -> fAC(i(x),y1)
   fAC(i(x),i(y1)) -> i(fAC(x,y1))
  S:
   f{AC,#}(fAC(x11,x12),x13) -> f{AC,#}(x11,x12)
   f{AC,#}(x11,fAC(x12,x13)) -> f{AC,#}(x12,x13)
  AC-EDG Processor:
   Equations#:
    f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
    f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
    f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
    f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
   DPs:
    f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(x,y1)
    f{AC,#}(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
    f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(i(fAC(x,y1)),y2)
    phi#(x,phi(y1,y2)) -> f{AC,#}(x,y1)
    phi#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
    f{AC,#}(i(fAC(x,y1)),y1) -> i#(x)
    i#(fAC(i(y1),x)) -> i#(x)
    i#(fAC(i(y1),x)) -> f{AC,#}(i(x),y1)
    f{AC,#}(i(x),i(y1)) -> f{AC,#}(x,y1)
    f{AC,#}(i(x),i(y1)) -> i#(fAC(x,y1))
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x,y1)
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(i(fAC(x,y1)),y2)
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x6,fAC(i(fAC(x,y1)),y2))
    f{AC,#}(x7,fAC(one(),x)) -> f{AC,#}(x7,x)
    f{AC,#}(x8,fAC(i(x),x)) -> f{AC,#}(x8,one())
    f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
    f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> f{AC,#}(x9,i(x))
    f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x,y1)
    f{AC,#}(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
    f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x10,i(fAC(x,y1)))
   Equations:
    fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
    fAC(x3,x4) -> fAC(x4,x3)
    fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
    fAC(x4,x3) -> fAC(x3,x4)
   TRS:
    fAC(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
    fAC(one(),x) -> x
    phi(one(),x) -> x
    fAC(i(x),x) -> one()
    i(one()) -> one()
    i(i(x)) -> x
    phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
    fAC(i(fAC(x,y1)),y1) -> i(x)
    i(fAC(i(y1),x)) -> fAC(i(x),y1)
    fAC(i(x),i(y1)) -> i(fAC(x,y1))
   S:
    f{AC,#}(fAC(x11,x12),x13) -> f{AC,#}(x11,x12)
    f{AC,#}(x11,fAC(x12,x13)) -> f{AC,#}(x12,x13)
   Open