MAYBE
Time: 3.403

Problem:
 Equations:
  _xor_AC(_xor_AC(x6,x7),x8) -> _xor_AC(x6,_xor_AC(x7,x8))
  _xor_AC(x6,x7) -> _xor_AC(x7,x6)
  _and_AC(_and_AC(x6,x7),x8) -> _and_AC(x6,_and_AC(x7,x8))
  _and_AC(x6,x7) -> _and_AC(x7,x6)
  _or_AC(_or_AC(x6,x7),x8) -> _or_AC(x6,_or_AC(x7,x8))
  _or_AC(x6,x7) -> _or_AC(x7,x6)
  _xor_AC(x6,_xor_AC(x7,x8)) -> _xor_AC(_xor_AC(x6,x7),x8)
  _xor_AC(x7,x6) -> _xor_AC(x6,x7)
  _and_AC(x6,_and_AC(x7,x8)) -> _and_AC(_and_AC(x6,x7),x8)
  _and_AC(x7,x6) -> _and_AC(x6,x7)
  _or_AC(x6,_or_AC(x7,x8)) -> _or_AC(_or_AC(x6,x7),x8)
  _or_AC(x7,x6) -> _or_AC(x6,x7)
 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:
 DP Processor:
  Equations#:
   _xor_{AC,#}(_xor_AC(x6,x7),x8) -> _xor_{AC,#}(x6,_xor_AC(x7,x8))
   _xor_{AC,#}(x6,x7) -> _xor_{AC,#}(x7,x6)
   _and_{AC,#}(_and_AC(x6,x7),x8) -> _and_{AC,#}(x6,_and_AC(x7,x8))
   _and_{AC,#}(x6,x7) -> _and_{AC,#}(x7,x6)
   _or_{AC,#}(_or_AC(x6,x7),x8) -> _or_{AC,#}(x6,_or_AC(x7,x8))
   _or_{AC,#}(x6,x7) -> _or_{AC,#}(x7,x6)
   _xor_{AC,#}(x6,_xor_AC(x7,x8)) -> _xor_{AC,#}(_xor_AC(x6,x7),x8)
   _xor_{AC,#}(x7,x6) -> _xor_{AC,#}(x6,x7)
   _and_{AC,#}(x6,_and_AC(x7,x8)) -> _and_{AC,#}(_and_AC(x6,x7),x8)
   _and_{AC,#}(x7,x6) -> _and_{AC,#}(x6,x7)
   _or_{AC,#}(x6,_or_AC(x7,x8)) -> _or_{AC,#}(_or_AC(x6,x7),x8)
   _or_{AC,#}(x7,x6) -> _or_{AC,#}(x6,x7)
  DPs:
   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) -> _and_{AC,#}(A,C)
   U13#(tt(),A,B,C) -> _and_{AC,#}(A,B)
   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) -> _and_{AC,#}(A,B)
   U22#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(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) -> _isNotEqualTo_#(U,U')
   U32#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
   U32#(tt(),U',U) -> U33#(equal(_isNotEqualTo_(U,U'),true()))
   U41#(tt(),U',U) -> U42#(tt(),U',U)
   U42#(tt(),U',U) -> _isEqualTo_#(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,#}(A,B)
   U52#(tt(),A,B) -> _and_{AC,#}(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') -> _isNotEqualTo_#(B,true())
   U63#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
   U63#(tt(),B,U') -> U64#(equal(_isNotEqualTo_(B,true()),true()),U')
   U71#(tt(),U) -> U72#(tt(),U)
   _and_{AC,#}(A,_xor_AC(B,C)) -> U11#(tt(),A,B,C)
   _implies_#(A,B) -> U21#(tt(),A,B)
   _isEqualTo_#(U,U') -> U31#(tt(),U',U)
   _isNotEqualTo_#(U,U') -> U41#(tt(),U',U)
   _or_{AC,#}(A,B) -> U51#(tt(),A,B)
   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())
   _and_{AC,#}(x9,_and_AC(A,A)) -> _and_{AC,#}(x9,A)
   _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> U11#(tt(),A,B,C)
   _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x10,U11(tt(),A,B,C))
   _and_{AC,#}(x11,_and_AC(false(),A)) -> _and_{AC,#}(x11,false())
   _and_{AC,#}(x12,_and_AC(true(),A)) -> _and_{AC,#}(x12,A)
   _or_{AC,#}(x13,_or_AC(A,B)) -> U51#(tt(),A,B)
   _or_{AC,#}(x13,_or_AC(A,B)) -> _or_{AC,#}(x13,U51(tt(),A,B))
   _xor_{AC,#}(x14,_xor_AC(A,A)) -> _xor_{AC,#}(x14,false())
   _xor_{AC,#}(x15,_xor_AC(false(),A)) -> _xor_{AC,#}(x15,A)
  Equations:
   _xor_AC(_xor_AC(x6,x7),x8) -> _xor_AC(x6,_xor_AC(x7,x8))
   _xor_AC(x6,x7) -> _xor_AC(x7,x6)
   _and_AC(_and_AC(x6,x7),x8) -> _and_AC(x6,_and_AC(x7,x8))
   _and_AC(x6,x7) -> _and_AC(x7,x6)
   _or_AC(_or_AC(x6,x7),x8) -> _or_AC(x6,_or_AC(x7,x8))
   _or_AC(x6,x7) -> _or_AC(x7,x6)
   _xor_AC(x6,_xor_AC(x7,x8)) -> _xor_AC(_xor_AC(x6,x7),x8)
   _xor_AC(x7,x6) -> _xor_AC(x6,x7)
   _and_AC(x6,_and_AC(x7,x8)) -> _and_AC(_and_AC(x6,x7),x8)
   _and_AC(x7,x6) -> _and_AC(x6,x7)
   _or_AC(x6,_or_AC(x7,x8)) -> _or_AC(_or_AC(x6,x7),x8)
   _or_AC(x7,x6) -> _or_AC(x6,x7)
  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()
  S:
   _xor_{AC,#}(_xor_AC(x16,x17),x18) -> _xor_{AC,#}(x16,x17)
   _xor_{AC,#}(x16,_xor_AC(x17,x18)) -> _xor_{AC,#}(x17,x18)
   _and_{AC,#}(_and_AC(x16,x17),x18) -> _and_{AC,#}(x16,x17)
   _and_{AC,#}(x16,_and_AC(x17,x18)) -> _and_{AC,#}(x17,x18)
   _or_{AC,#}(_or_AC(x16,x17),x18) -> _or_{AC,#}(x16,x17)
   _or_{AC,#}(x16,_or_AC(x17,x18)) -> _or_{AC,#}(x17,x18)
  AC-EDG Processor:
   Equations#:
    _xor_{AC,#}(_xor_AC(x6,x7),x8) -> _xor_{AC,#}(x6,_xor_AC(x7,x8))
    _xor_{AC,#}(x6,x7) -> _xor_{AC,#}(x7,x6)
    _and_{AC,#}(_and_AC(x6,x7),x8) -> _and_{AC,#}(x6,_and_AC(x7,x8))
    _and_{AC,#}(x6,x7) -> _and_{AC,#}(x7,x6)
    _or_{AC,#}(_or_AC(x6,x7),x8) -> _or_{AC,#}(x6,_or_AC(x7,x8))
    _or_{AC,#}(x6,x7) -> _or_{AC,#}(x7,x6)
    _xor_{AC,#}(x6,_xor_AC(x7,x8)) -> _xor_{AC,#}(_xor_AC(x6,x7),x8)
    _xor_{AC,#}(x7,x6) -> _xor_{AC,#}(x6,x7)
    _and_{AC,#}(x6,_and_AC(x7,x8)) -> _and_{AC,#}(_and_AC(x6,x7),x8)
    _and_{AC,#}(x7,x6) -> _and_{AC,#}(x6,x7)
    _or_{AC,#}(x6,_or_AC(x7,x8)) -> _or_{AC,#}(_or_AC(x6,x7),x8)
    _or_{AC,#}(x7,x6) -> _or_{AC,#}(x6,x7)
   DPs:
    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) -> _and_{AC,#}(A,C)
    U13#(tt(),A,B,C) -> _and_{AC,#}(A,B)
    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) -> _and_{AC,#}(A,B)
    U22#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(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) -> _isNotEqualTo_#(U,U')
    U32#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
    U32#(tt(),U',U) -> U33#(equal(_isNotEqualTo_(U,U'),true()))
    U41#(tt(),U',U) -> U42#(tt(),U',U)
    U42#(tt(),U',U) -> _isEqualTo_#(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,#}(A,B)
    U52#(tt(),A,B) -> _and_{AC,#}(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') -> _isNotEqualTo_#(B,true())
    U63#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
    U63#(tt(),B,U') -> U64#(equal(_isNotEqualTo_(B,true()),true()),U')
    U71#(tt(),U) -> U72#(tt(),U)
    _and_{AC,#}(A,_xor_AC(B,C)) -> U11#(tt(),A,B,C)
    _implies_#(A,B) -> U21#(tt(),A,B)
    _isEqualTo_#(U,U') -> U31#(tt(),U',U)
    _isNotEqualTo_#(U,U') -> U41#(tt(),U',U)
    _or_{AC,#}(A,B) -> U51#(tt(),A,B)
    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())
    _and_{AC,#}(x9,_and_AC(A,A)) -> _and_{AC,#}(x9,A)
    _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> U11#(tt(),A,B,C)
    _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x10,U11(tt(),A,B,C))
    _and_{AC,#}(x11,_and_AC(false(),A)) -> _and_{AC,#}(x11,false())
    _and_{AC,#}(x12,_and_AC(true(),A)) -> _and_{AC,#}(x12,A)
    _or_{AC,#}(x13,_or_AC(A,B)) -> U51#(tt(),A,B)
    _or_{AC,#}(x13,_or_AC(A,B)) -> _or_{AC,#}(x13,U51(tt(),A,B))
    _xor_{AC,#}(x14,_xor_AC(A,A)) -> _xor_{AC,#}(x14,false())
    _xor_{AC,#}(x15,_xor_AC(false(),A)) -> _xor_{AC,#}(x15,A)
   Equations:
    _xor_AC(_xor_AC(x6,x7),x8) -> _xor_AC(x6,_xor_AC(x7,x8))
    _xor_AC(x6,x7) -> _xor_AC(x7,x6)
    _and_AC(_and_AC(x6,x7),x8) -> _and_AC(x6,_and_AC(x7,x8))
    _and_AC(x6,x7) -> _and_AC(x7,x6)
    _or_AC(_or_AC(x6,x7),x8) -> _or_AC(x6,_or_AC(x7,x8))
    _or_AC(x6,x7) -> _or_AC(x7,x6)
    _xor_AC(x6,_xor_AC(x7,x8)) -> _xor_AC(_xor_AC(x6,x7),x8)
    _xor_AC(x7,x6) -> _xor_AC(x6,x7)
    _and_AC(x6,_and_AC(x7,x8)) -> _and_AC(_and_AC(x6,x7),x8)
    _and_AC(x7,x6) -> _and_AC(x6,x7)
    _or_AC(x6,_or_AC(x7,x8)) -> _or_AC(_or_AC(x6,x7),x8)
    _or_AC(x7,x6) -> _or_AC(x6,x7)
   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()
   S:
    _xor_{AC,#}(_xor_AC(x16,x17),x18) -> _xor_{AC,#}(x16,x17)
    _xor_{AC,#}(x16,_xor_AC(x17,x18)) -> _xor_{AC,#}(x17,x18)
    _and_{AC,#}(_and_AC(x16,x17),x18) -> _and_{AC,#}(x16,x17)
    _and_{AC,#}(x16,_and_AC(x17,x18)) -> _and_{AC,#}(x17,x18)
    _or_{AC,#}(_or_AC(x16,x17),x18) -> _or_{AC,#}(x16,x17)
    _or_{AC,#}(x16,_or_AC(x17,x18)) -> _or_{AC,#}(x17,x18)
   Open