MAYBE
Time: 0.038

Problem:
 Equations:
  transAC(transAC(x5,x6),x7) -> transAC(x5,transAC(x6,x7))
  transAC(x5,x6) -> transAC(x6,x5)
  transAC(x5,transAC(x6,x7)) -> transAC(transAC(x5,x6),x7)
  transAC(x6,x5) -> transAC(x5,x6)
 TRS:
  transAC(x1,refl()) -> x1
  congror1(refl()) -> refl()
  congror2(refl()) -> refl()
  transAC(congror1(x1),ortrue2()) -> ortrue2()
  transAC(congror2(x1),ortrue1()) -> ortrue1()
  transAC(orfalse1(),x1) -> transAC(congror2(x1),orfalse1())
  transAC(orfalse2(),x1) -> transAC(congror1(x1),orfalse2())
  transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
  transAC(congror1(transAC(x1,x3)),congror2(transAC(x2,x4)))
  transAC(ortrue1(),x1) -> ortrue1()
  transAC(ortrue2(),x1) -> ortrue2()

Proof:
 Open