MAYBE
Time: 0.898

Problem:
 Equations:
  transAC(transAC(x5,x6),x15) -> transAC(x5,transAC(x6,x15))
  transAC(x5,x6) -> transAC(x6,x5)
  transAC(x5,transAC(x6,x15)) -> transAC(transAC(x5,x6),x15)
  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:
 DP Processor:
  Equations#:
   trans{AC,#}(transAC(x5,x6),x15) -> trans{AC,#}(x5,transAC(x6,x15))
   trans{AC,#}(x5,x6) -> trans{AC,#}(x6,x5)
   trans{AC,#}(x5,transAC(x6,x15)) -> trans{AC,#}(transAC(x5,x6),x15)
   trans{AC,#}(x6,x5) -> trans{AC,#}(x5,x6)
  DPs:
   trans{AC,#}(orfalse1(),x1) -> congror2#(x1)
   trans{AC,#}(orfalse1(),x1) -> trans{AC,#}(congror2(x1),orfalse1())
   trans{AC,#}(orfalse2(),x1) -> congror1#(x1)
   trans{AC,#}(orfalse2(),x1) -> trans{AC,#}(congror1(x1),orfalse2())
   trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
   trans{AC,#}(x2,x4)
   trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
   congror2#(transAC(x2,x4))
   trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
   trans{AC,#}(x1,x3)
   trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
   congror1#(transAC(x1,x3))
   trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
   trans{AC,#}(congror1(transAC(x1,x3)),congror2(transAC(x2,x4)))
   trans{AC,#}(x7,transAC(x1,refl())) -> trans{AC,#}(x7,x1)
   trans{AC,#}(x8,transAC(congror1(x1),ortrue2())) -> trans{AC,#}(x8,ortrue2())
   trans{AC,#}(x9,transAC(congror2(x1),ortrue1())) -> trans{AC,#}(x9,ortrue1())
   trans{AC,#}(x10,transAC(orfalse1(),x1)) -> congror2#(x1)
   trans{AC,#}(x10,transAC(orfalse1(),x1)) -> trans{AC,#}(congror2(x1),orfalse1())
   trans{AC,#}(x10,transAC(orfalse1(),x1)) -> trans{AC,#}(x10,transAC(congror2(x1),orfalse1()))
   trans{AC,#}(x11,transAC(orfalse2(),x1)) -> congror1#(x1)
   trans{AC,#}(x11,transAC(orfalse2(),x1)) -> trans{AC,#}(congror1(x1),orfalse2())
   trans{AC,#}(x11,transAC(orfalse2(),x1)) -> trans{AC,#}(x11,transAC(congror1(x1),orfalse2()))
   trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
   -> trans{AC,#}(x2,x4)
   trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
   -> congror2#(transAC(x2,x4))
   trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
   -> trans{AC,#}(x1,x3)
   trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
   -> congror1#(transAC(x1,x3))
   trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
   -> trans{AC,#}(congror1(transAC(x1,x3)),congror2(transAC(x2,x4)))
   trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
   -> trans{AC,#}(x12,transAC(congror1(transAC(x1,x3)),congror2(transAC(x2,x4))))
   trans{AC,#}(x13,transAC(ortrue1(),x1)) -> trans{AC,#}(x13,ortrue1())
   trans{AC,#}(x14,transAC(ortrue2(),x1)) -> trans{AC,#}(x14,ortrue2())
  Equations:
   transAC(transAC(x5,x6),x15) -> transAC(x5,transAC(x6,x15))
   transAC(x5,x6) -> transAC(x6,x5)
   transAC(x5,transAC(x6,x15)) -> transAC(transAC(x5,x6),x15)
   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()
  S:
   trans{AC,#}(transAC(x16,x17),x19) -> trans{AC,#}(x16,x17)
   trans{AC,#}(x16,transAC(x17,x19)) -> trans{AC,#}(x17,x19)
  AC-EDG Processor:
   Equations#:
    trans{AC,#}(transAC(x5,x6),x15) -> trans{AC,#}(x5,transAC(x6,x15))
    trans{AC,#}(x5,x6) -> trans{AC,#}(x6,x5)
    trans{AC,#}(x5,transAC(x6,x15)) -> trans{AC,#}(transAC(x5,x6),x15)
    trans{AC,#}(x6,x5) -> trans{AC,#}(x5,x6)
   DPs:
    trans{AC,#}(orfalse1(),x1) -> congror2#(x1)
    trans{AC,#}(orfalse1(),x1) -> trans{AC,#}(congror2(x1),orfalse1())
    trans{AC,#}(orfalse2(),x1) -> congror1#(x1)
    trans{AC,#}(orfalse2(),x1) -> trans{AC,#}(congror1(x1),orfalse2())
    trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
    trans{AC,#}(x2,x4)
    trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
    congror2#(transAC(x2,x4))
    trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
    trans{AC,#}(x1,x3)
    trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
    congror1#(transAC(x1,x3))
    trans{AC,#}(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))) ->
    trans{AC,#}(congror1(transAC(x1,x3)),congror2(transAC(x2,x4)))
    trans{AC,#}(x7,transAC(x1,refl())) -> trans{AC,#}(x7,x1)
    trans{AC,#}(x8,transAC(congror1(x1),ortrue2())) -> trans{AC,#}(x8,ortrue2())
    trans{AC,#}(x9,transAC(congror2(x1),ortrue1())) -> trans{AC,#}(x9,ortrue1())
    trans{AC,#}(x10,transAC(orfalse1(),x1)) -> congror2#(x1)
    trans{AC,#}(x10,transAC(orfalse1(),x1)) -> trans{AC,#}(congror2(x1),orfalse1())
    trans{AC,#}(x10,transAC(orfalse1(),x1)) -> trans{AC,#}(x10,transAC(congror2(x1),orfalse1()))
    trans{AC,#}(x11,transAC(orfalse2(),x1)) -> congror1#(x1)
    trans{AC,#}(x11,transAC(orfalse2(),x1)) -> trans{AC,#}(congror1(x1),orfalse2())
    trans{AC,#}(x11,transAC(orfalse2(),x1)) -> trans{AC,#}(x11,transAC(congror1(x1),orfalse2()))
    trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
    -> trans{AC,#}(x2,x4)
    trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
    -> congror2#(transAC(x2,x4))
    trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
    -> trans{AC,#}(x1,x3)
    trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
    -> congror1#(transAC(x1,x3))
    trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
    -> trans{AC,#}(congror1(transAC(x1,x3)),congror2(transAC(x2,x4)))
    trans{AC,#}(x12,transAC(transAC(congror1(x1),congror2(x2)),transAC(congror1(x3),congror2(x4))))
    -> trans{AC,#}(x12,transAC(congror1(transAC(x1,x3)),congror2(transAC(x2,x4))))
    trans{AC,#}(x13,transAC(ortrue1(),x1)) -> trans{AC,#}(x13,ortrue1())
    trans{AC,#}(x14,transAC(ortrue2(),x1)) -> trans{AC,#}(x14,ortrue2())
   Equations:
    transAC(transAC(x5,x6),x15) -> transAC(x5,transAC(x6,x15))
    transAC(x5,x6) -> transAC(x6,x5)
    transAC(x5,transAC(x6,x15)) -> transAC(transAC(x5,x6),x15)
    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()
   S:
    trans{AC,#}(transAC(x16,x17),x19) -> trans{AC,#}(x16,x17)
    trans{AC,#}(x16,transAC(x17,x19)) -> trans{AC,#}(x17,x19)
   Open