MAYBE
Time: 1.126

Problem:
 Equations:
  _and_AC(_and_AC(x6,x7),x8) -> _and_AC(x6,_and_AC(x7,x8))
  _and_AC(x6,x7) -> _and_AC(x7,x6)
  _xor_AC(_xor_AC(x6,x7),x8) -> _xor_AC(x6,_xor_AC(x7,x8))
  _xor_AC(x6,x7) -> _xor_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)
  _and_AC(x6,_and_AC(x7,x8)) -> _and_AC(_and_AC(x6,x7),x8)
  _and_AC(x7,x6) -> _and_AC(x6,x7)
  _xor_AC(x6,_xor_AC(x7,x8)) -> _xor_AC(_xor_AC(x6,x7),x8)
  _xor_AC(x7,x6) -> _xor_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(),U',U) -> U12(equal(_isNotEqualTo_(U,U'),true()))
  U12(tt()) -> false()
  U21(tt(),B,U') -> U22(equal(_isNotEqualTo_(B,true()),true()),U')
  U22(tt(),U') -> U'
  _and_AC(A,A) -> A
  _and_AC(A,_xor_AC(B,C)) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
  _and_AC(false(),A) -> false()
  _and_AC(true(),A) -> A
  _implies_(A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
  _isEqualTo_(U,U') -> U11(tt(),U',U)
  _isEqualTo_(U,U) -> true()
  _isNotEqualTo_(U,U') -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
  _isNotEqualTo_(U,U) -> false()
  _or_AC(A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
  _xor_AC(A,A) -> false()
  _xor_AC(false(),A) -> A
  and(tt(),X) -> X
  equal(X,X) -> tt()
  if_then_else_fi(B,U,U') -> U21(tt(),B,U')
  if_then_else_fi(true(),U,U') -> U
  not_(A) -> _xor_AC(A,true())
  not_(false()) -> true()
  not_(true()) -> false()

Proof:
 DP Processor:
  Equations#:
   _and_{AC,#}(_and_AC(x6,x7),x8) -> _and_{AC,#}(x6,_and_AC(x7,x8))
   _and_{AC,#}(x6,x7) -> _and_{AC,#}(x7,x6)
   _xor_{AC,#}(_xor_AC(x6,x7),x8) -> _xor_{AC,#}(x6,_xor_AC(x7,x8))
   _xor_{AC,#}(x6,x7) -> _xor_{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)
   _and_{AC,#}(x6,_and_AC(x7,x8)) -> _and_{AC,#}(_and_AC(x6,x7),x8)
   _and_{AC,#}(x7,x6) -> _and_{AC,#}(x6,x7)
   _xor_{AC,#}(x6,_xor_AC(x7,x8)) -> _xor_{AC,#}(_xor_AC(x6,x7),x8)
   _xor_{AC,#}(x7,x6) -> _xor_{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(),U',U) -> _isNotEqualTo_#(U,U')
   U11#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
   U11#(tt(),U',U) -> U12#(equal(_isNotEqualTo_(U,U'),true()))
   U21#(tt(),B,U') -> _isNotEqualTo_#(B,true())
   U21#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
   U21#(tt(),B,U') -> U22#(equal(_isNotEqualTo_(B,true()),true()),U')
   _and_{AC,#}(A,_xor_AC(B,C)) -> _and_{AC,#}(A,C)
   _and_{AC,#}(A,_xor_AC(B,C)) -> _and_{AC,#}(A,B)
   _and_{AC,#}(A,_xor_AC(B,C)) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
   _implies_#(A,B) -> _and_{AC,#}(A,B)
   _implies_#(A,B) -> _xor_{AC,#}(A,_and_AC(A,B))
   _implies_#(A,B) -> not_#(_xor_AC(A,_and_AC(A,B)))
   _isEqualTo_#(U,U') -> U11#(tt(),U',U)
   _isNotEqualTo_#(U,U') -> _isEqualTo_#(U,U')
   _isNotEqualTo_#(U,U') -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true())
   _or_{AC,#}(A,B) -> _xor_{AC,#}(A,B)
   _or_{AC,#}(A,B) -> _and_{AC,#}(A,B)
   _or_{AC,#}(A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
   if_then_else_fi#(B,U,U') -> U21#(tt(),B,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))) -> _and_{AC,#}(A,C)
   _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(A,B)
   _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
   _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x10,_xor_AC(_and_AC(A,B),_and_AC(A,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)) -> _xor_{AC,#}(A,B)
   _or_{AC,#}(x13,_or_AC(A,B)) -> _and_{AC,#}(A,B)
   _or_{AC,#}(x13,_or_AC(A,B)) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
   _or_{AC,#}(x13,_or_AC(A,B)) -> _or_{AC,#}(x13,_xor_AC(_and_AC(A,B),_xor_AC(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:
   _and_AC(_and_AC(x6,x7),x8) -> _and_AC(x6,_and_AC(x7,x8))
   _and_AC(x6,x7) -> _and_AC(x7,x6)
   _xor_AC(_xor_AC(x6,x7),x8) -> _xor_AC(x6,_xor_AC(x7,x8))
   _xor_AC(x6,x7) -> _xor_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)
   _and_AC(x6,_and_AC(x7,x8)) -> _and_AC(_and_AC(x6,x7),x8)
   _and_AC(x7,x6) -> _and_AC(x6,x7)
   _xor_AC(x6,_xor_AC(x7,x8)) -> _xor_AC(_xor_AC(x6,x7),x8)
   _xor_AC(x7,x6) -> _xor_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(),U',U) -> U12(equal(_isNotEqualTo_(U,U'),true()))
   U12(tt()) -> false()
   U21(tt(),B,U') -> U22(equal(_isNotEqualTo_(B,true()),true()),U')
   U22(tt(),U') -> U'
   _and_AC(A,A) -> A
   _and_AC(A,_xor_AC(B,C)) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
   _and_AC(false(),A) -> false()
   _and_AC(true(),A) -> A
   _implies_(A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
   _isEqualTo_(U,U') -> U11(tt(),U',U)
   _isEqualTo_(U,U) -> true()
   _isNotEqualTo_(U,U') -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
   _isNotEqualTo_(U,U) -> false()
   _or_AC(A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
   _xor_AC(A,A) -> false()
   _xor_AC(false(),A) -> A
   and(tt(),X) -> X
   equal(X,X) -> tt()
   if_then_else_fi(B,U,U') -> U21(tt(),B,U')
   if_then_else_fi(true(),U,U') -> U
   not_(A) -> _xor_AC(A,true())
   not_(false()) -> true()
   not_(true()) -> false()
  S:
   _and_{AC,#}(_and_AC(x16,x17),x18) -> _and_{AC,#}(x16,x17)
   _and_{AC,#}(x16,_and_AC(x17,x18)) -> _and_{AC,#}(x17,x18)
   _xor_{AC,#}(_xor_AC(x16,x17),x18) -> _xor_{AC,#}(x16,x17)
   _xor_{AC,#}(x16,_xor_AC(x17,x18)) -> _xor_{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#:
    _and_{AC,#}(_and_AC(x6,x7),x8) -> _and_{AC,#}(x6,_and_AC(x7,x8))
    _and_{AC,#}(x6,x7) -> _and_{AC,#}(x7,x6)
    _xor_{AC,#}(_xor_AC(x6,x7),x8) -> _xor_{AC,#}(x6,_xor_AC(x7,x8))
    _xor_{AC,#}(x6,x7) -> _xor_{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)
    _and_{AC,#}(x6,_and_AC(x7,x8)) -> _and_{AC,#}(_and_AC(x6,x7),x8)
    _and_{AC,#}(x7,x6) -> _and_{AC,#}(x6,x7)
    _xor_{AC,#}(x6,_xor_AC(x7,x8)) -> _xor_{AC,#}(_xor_AC(x6,x7),x8)
    _xor_{AC,#}(x7,x6) -> _xor_{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(),U',U) -> _isNotEqualTo_#(U,U')
    U11#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
    U11#(tt(),U',U) -> U12#(equal(_isNotEqualTo_(U,U'),true()))
    U21#(tt(),B,U') -> _isNotEqualTo_#(B,true())
    U21#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
    U21#(tt(),B,U') -> U22#(equal(_isNotEqualTo_(B,true()),true()),U')
    _and_{AC,#}(A,_xor_AC(B,C)) -> _and_{AC,#}(A,C)
    _and_{AC,#}(A,_xor_AC(B,C)) -> _and_{AC,#}(A,B)
    _and_{AC,#}(A,_xor_AC(B,C)) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
    _implies_#(A,B) -> _and_{AC,#}(A,B)
    _implies_#(A,B) -> _xor_{AC,#}(A,_and_AC(A,B))
    _implies_#(A,B) -> not_#(_xor_AC(A,_and_AC(A,B)))
    _isEqualTo_#(U,U') -> U11#(tt(),U',U)
    _isNotEqualTo_#(U,U') -> _isEqualTo_#(U,U')
    _isNotEqualTo_#(U,U') -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true())
    _or_{AC,#}(A,B) -> _xor_{AC,#}(A,B)
    _or_{AC,#}(A,B) -> _and_{AC,#}(A,B)
    _or_{AC,#}(A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
    if_then_else_fi#(B,U,U') -> U21#(tt(),B,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))) -> _and_{AC,#}(A,C)
    _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(A,B)
    _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
    _and_{AC,#}(x10,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x10,_xor_AC(_and_AC(A,B),_and_AC(A,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)) -> _xor_{AC,#}(A,B)
    _or_{AC,#}(x13,_or_AC(A,B)) -> _and_{AC,#}(A,B)
    _or_{AC,#}(x13,_or_AC(A,B)) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
    _or_{AC,#}(x13,_or_AC(A,B)) -> _or_{AC,#}(x13,_xor_AC(_and_AC(A,B),_xor_AC(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:
    _and_AC(_and_AC(x6,x7),x8) -> _and_AC(x6,_and_AC(x7,x8))
    _and_AC(x6,x7) -> _and_AC(x7,x6)
    _xor_AC(_xor_AC(x6,x7),x8) -> _xor_AC(x6,_xor_AC(x7,x8))
    _xor_AC(x6,x7) -> _xor_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)
    _and_AC(x6,_and_AC(x7,x8)) -> _and_AC(_and_AC(x6,x7),x8)
    _and_AC(x7,x6) -> _and_AC(x6,x7)
    _xor_AC(x6,_xor_AC(x7,x8)) -> _xor_AC(_xor_AC(x6,x7),x8)
    _xor_AC(x7,x6) -> _xor_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(),U',U) -> U12(equal(_isNotEqualTo_(U,U'),true()))
    U12(tt()) -> false()
    U21(tt(),B,U') -> U22(equal(_isNotEqualTo_(B,true()),true()),U')
    U22(tt(),U') -> U'
    _and_AC(A,A) -> A
    _and_AC(A,_xor_AC(B,C)) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
    _and_AC(false(),A) -> false()
    _and_AC(true(),A) -> A
    _implies_(A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
    _isEqualTo_(U,U') -> U11(tt(),U',U)
    _isEqualTo_(U,U) -> true()
    _isNotEqualTo_(U,U') -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
    _isNotEqualTo_(U,U) -> false()
    _or_AC(A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
    _xor_AC(A,A) -> false()
    _xor_AC(false(),A) -> A
    and(tt(),X) -> X
    equal(X,X) -> tt()
    if_then_else_fi(B,U,U') -> U21(tt(),B,U')
    if_then_else_fi(true(),U,U') -> U
    not_(A) -> _xor_AC(A,true())
    not_(false()) -> true()
    not_(true()) -> false()
   S:
    _and_{AC,#}(_and_AC(x16,x17),x18) -> _and_{AC,#}(x16,x17)
    _and_{AC,#}(x16,_and_AC(x17,x18)) -> _and_{AC,#}(x17,x18)
    _xor_{AC,#}(_xor_AC(x16,x17),x18) -> _xor_{AC,#}(x16,x17)
    _xor_{AC,#}(x16,_xor_AC(x17,x18)) -> _xor_{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