MAYBE
Time: 1.968

Problem:
 Equations:
  _xor_AC(_xor_AC(x8,x9),x10) -> _xor_AC(x8,_xor_AC(x9,x10))
  _xor_AC(x8,x9) -> _xor_AC(x9,x8)
  _and_AC(_and_AC(x8,x9),x10) -> _and_AC(x8,_and_AC(x9,x10))
  _and_AC(x8,x9) -> _and_AC(x9,x8)
  _or_AC(_or_AC(x8,x9),x10) -> _or_AC(x8,_or_AC(x9,x10))
  _or_AC(x8,x9) -> _or_AC(x9,x8)
  _xor_AC(x8,_xor_AC(x9,x10)) -> _xor_AC(_xor_AC(x8,x9),x10)
  _xor_AC(x9,x8) -> _xor_AC(x8,x9)
  _and_AC(x8,_and_AC(x9,x10)) -> _and_AC(_and_AC(x8,x9),x10)
  _and_AC(x9,x8) -> _and_AC(x8,x9)
  _or_AC(x8,_or_AC(x9,x10)) -> _or_AC(_or_AC(x8,x9),x10)
  _or_AC(x9,x8) -> _or_AC(x8,x9)
 TRS:
  U11(tt(),A,B,C) -> U12(tt(),A,B,C)
  U12(tt(),A,B,C) -> U13(tt(),A,B,C)
  U13(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
  U21(tt(),A,B) -> U22(tt(),A,B)
  U22(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
  U31(tt(),U',U) -> U32(tt(),U',U)
  U32(tt(),U',U) -> U33(equal(_isNotEqualTo_(U,U'),true()))
  U33(tt()) -> false()
  U41(tt(),U',U) -> U42(tt(),U',U)
  U42(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
  U51(tt(),A,B) -> U52(tt(),A,B)
  U52(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
  U61(tt(),B,U') -> U62(tt(),B,U')
  U62(tt(),B,U') -> U63(tt(),B,U')
  U63(tt(),B,U') -> U64(equal(_isNotEqualTo_(B,true()),true()),U')
  U64(tt(),U') -> U'
  U71(tt(),U) -> U72(tt(),U)
  U72(tt(),U) -> U
  _and_AC(A,A) -> A
  _and_AC(A,_xor_AC(B,C)) -> U11(tt(),A,B,C)
  _and_AC(false(),A) -> false()
  _and_AC(true(),A) -> A
  _implies_(A,B) -> U21(tt(),A,B)
  _isEqualTo_(U,U') -> U31(tt(),U',U)
  _isEqualTo_(U,U) -> true()
  _isNotEqualTo_(U,U') -> U41(tt(),U',U)
  _isNotEqualTo_(U,U) -> false()
  _or_AC(A,B) -> U51(tt(),A,B)
  _xor_AC(A,A) -> false()
  _xor_AC(false(),A) -> A
  equal(X,X) -> tt()
  if_then_else_fi(B,U,U') -> U61(tt(),B,U')
  if_then_else_fi(true(),U,U') -> U71(tt(),U)
  not_(A) -> _xor_AC(A,true())
  not_(false()) -> true()
  not_(true()) -> false()

Proof:
 Open