MAYBE
Time: 3.275

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:
  U101(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
  U11(tt(),A) -> A
  U111(tt()) -> false()
  U121(tt(),A) -> A
  U131(tt(),B,U') -> U132(equal(_isNotEqualTo_(B,true()),true()),U')
  U132(tt(),U') -> U'
  U141(tt(),U) -> U
  U151(tt(),A) -> _xor_AC(A,true())
  U21(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
  U31(tt()) -> false()
  U41(tt(),A) -> A
  U51(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
  U61(tt(),U',U) -> U62(equal(_isNotEqualTo_(U,U'),true()))
  U62(tt()) -> false()
  U71(tt()) -> true()
  U81(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
  U91(tt()) -> false()
  _and_AC(A,A) -> U11(isBool(A),A)
  _and_AC(A,_xor_AC(B,C)) -> U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
  _and_AC(false(),A) -> U31(isBool(A))
  _and_AC(true(),A) -> U41(isBool(A),A)
  _implies_(A,B) -> U51(and(isBool(A),isBool(B)),A,B)
  _isEqualTo_(U,U') -> U61(and(isS(U'),isS(U)),U',U)
  _isEqualTo_(U,U) -> U71(isS(U))
  _isNotEqualTo_(U,U') -> U81(and(isS(U'),isS(U)),U',U)
  _isNotEqualTo_(U,U) -> U91(isS(U))
  _or_AC(A,B) -> U101(and(isBool(A),isBool(B)),A,B)
  _xor_AC(A,A) -> U111(isBool(A))
  _xor_AC(false(),A) -> U121(isBool(A),A)
  and(tt(),X) -> X
  equal(X,X) -> tt()
  if_then_else_fi(B,U,U') -> U131(and(isBool(B),and(isS(U'),isS(U))),B,U')
  if_then_else_fi(true(),U,U') -> U141(and(isS(U'),isS(U)),U)
  isBool(false()) -> tt()
  isBool(true()) -> tt()
  isBool(_and_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
  isBool(_implies_(V1,V2)) -> and(isBool(V1),isBool(V2))
  isBool(_isEqualTo_(V1,V2)) -> and(isUniversal(V1),isUniversal(V2))
  isBool(_isNotEqualTo_(V1,V2)) -> and(isUniversal(V1),isUniversal(V2))
  isBool(_or_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
  isBool(_xor_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
  isBool(not_(V1)) -> isBool(V1)
  not_(A) -> U151(isBool(A),A)
  not_(false()) -> true()
  not_(true()) -> false()

Proof:
 DP Processor:
  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)
  DPs:
   U101#(tt(),A,B) -> _xor_{AC,#}(A,B)
   U101#(tt(),A,B) -> _and_{AC,#}(A,B)
   U101#(tt(),A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
   U131#(tt(),B,U') -> _isNotEqualTo_#(B,true())
   U131#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
   U131#(tt(),B,U') -> U132#(equal(_isNotEqualTo_(B,true()),true()),U')
   U151#(tt(),A) -> _xor_{AC,#}(A,true())
   U21#(tt(),A,B,C) -> _and_{AC,#}(A,C)
   U21#(tt(),A,B,C) -> _and_{AC,#}(A,B)
   U21#(tt(),A,B,C) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
   U51#(tt(),A,B) -> _and_{AC,#}(A,B)
   U51#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(A,B))
   U51#(tt(),A,B) -> not_#(_xor_AC(A,_and_AC(A,B)))
   U61#(tt(),U',U) -> _isNotEqualTo_#(U,U')
   U61#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
   U61#(tt(),U',U) -> U62#(equal(_isNotEqualTo_(U,U'),true()))
   U81#(tt(),U',U) -> _isEqualTo_#(U,U')
   U81#(tt(),U',U) -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true())
   _and_{AC,#}(A,A) -> isBool#(A)
   _and_{AC,#}(A,A) -> U11#(isBool(A),A)
   _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(C)
   _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(B)
   _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(B),isBool(C))
   _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(A)
   _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(A),and(isBool(B),isBool(C)))
   _and_{AC,#}(A,_xor_AC(B,C)) -> U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
   _and_{AC,#}(false(),A) -> isBool#(A)
   _and_{AC,#}(false(),A) -> U31#(isBool(A))
   _and_{AC,#}(true(),A) -> isBool#(A)
   _and_{AC,#}(true(),A) -> U41#(isBool(A),A)
   _implies_#(A,B) -> isBool#(B)
   _implies_#(A,B) -> isBool#(A)
   _implies_#(A,B) -> and#(isBool(A),isBool(B))
   _implies_#(A,B) -> U51#(and(isBool(A),isBool(B)),A,B)
   _isEqualTo_#(U,U') -> and#(isS(U'),isS(U))
   _isEqualTo_#(U,U') -> U61#(and(isS(U'),isS(U)),U',U)
   _isEqualTo_#(U,U) -> U71#(isS(U))
   _isNotEqualTo_#(U,U') -> and#(isS(U'),isS(U))
   _isNotEqualTo_#(U,U') -> U81#(and(isS(U'),isS(U)),U',U)
   _isNotEqualTo_#(U,U) -> U91#(isS(U))
   _or_{AC,#}(A,B) -> isBool#(B)
   _or_{AC,#}(A,B) -> isBool#(A)
   _or_{AC,#}(A,B) -> and#(isBool(A),isBool(B))
   _or_{AC,#}(A,B) -> U101#(and(isBool(A),isBool(B)),A,B)
   _xor_{AC,#}(A,A) -> isBool#(A)
   _xor_{AC,#}(A,A) -> U111#(isBool(A))
   _xor_{AC,#}(false(),A) -> isBool#(A)
   _xor_{AC,#}(false(),A) -> U121#(isBool(A),A)
   if_then_else_fi#(B,U,U') -> and#(isS(U'),isS(U))
   if_then_else_fi#(B,U,U') -> isBool#(B)
   if_then_else_fi#(B,U,U') -> and#(isBool(B),and(isS(U'),isS(U)))
   if_then_else_fi#(B,U,U') -> U131#(and(isBool(B),and(isS(U'),isS(U))),B,U')
   if_then_else_fi#(true(),U,U') -> and#(isS(U'),isS(U))
   if_then_else_fi#(true(),U,U') -> U141#(and(isS(U'),isS(U)),U)
   isBool#(_and_AC(V1,V2)) -> isBool#(V2)
   isBool#(_and_AC(V1,V2)) -> isBool#(V1)
   isBool#(_and_AC(V1,V2)) -> and#(isBool(V1),isBool(V2))
   isBool#(_implies_(V1,V2)) -> isBool#(V2)
   isBool#(_implies_(V1,V2)) -> isBool#(V1)
   isBool#(_implies_(V1,V2)) -> and#(isBool(V1),isBool(V2))
   isBool#(_isEqualTo_(V1,V2)) -> and#(isUniversal(V1),isUniversal(V2))
   isBool#(_isNotEqualTo_(V1,V2)) -> and#(isUniversal(V1),isUniversal(V2))
   isBool#(_or_AC(V1,V2)) -> isBool#(V2)
   isBool#(_or_AC(V1,V2)) -> isBool#(V1)
   isBool#(_or_AC(V1,V2)) -> and#(isBool(V1),isBool(V2))
   isBool#(_xor_AC(V1,V2)) -> isBool#(V2)
   isBool#(_xor_AC(V1,V2)) -> isBool#(V1)
   isBool#(_xor_AC(V1,V2)) -> and#(isBool(V1),isBool(V2))
   isBool#(not_(V1)) -> isBool#(V1)
   not_#(A) -> isBool#(A)
   not_#(A) -> U151#(isBool(A),A)
   _and_{AC,#}(x11,_and_AC(A,A)) -> isBool#(A)
   _and_{AC,#}(x11,_and_AC(A,A)) -> U11#(isBool(A),A)
   _and_{AC,#}(x11,_and_AC(A,A)) -> _and_{AC,#}(x11,U11(isBool(A),A))
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(C)
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(B)
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(B),isBool(C))
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(A)
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(A),and(isBool(B),isBool(C)))
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) ->
   _and_{AC,#}(x12,U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C))
   _and_{AC,#}(x13,_and_AC(false(),A)) -> isBool#(A)
   _and_{AC,#}(x13,_and_AC(false(),A)) -> U31#(isBool(A))
   _and_{AC,#}(x13,_and_AC(false(),A)) -> _and_{AC,#}(x13,U31(isBool(A)))
   _and_{AC,#}(x14,_and_AC(true(),A)) -> isBool#(A)
   _and_{AC,#}(x14,_and_AC(true(),A)) -> U41#(isBool(A),A)
   _and_{AC,#}(x14,_and_AC(true(),A)) -> _and_{AC,#}(x14,U41(isBool(A),A))
   _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(B)
   _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(A)
   _or_{AC,#}(x15,_or_AC(A,B)) -> and#(isBool(A),isBool(B))
   _or_{AC,#}(x15,_or_AC(A,B)) -> U101#(and(isBool(A),isBool(B)),A,B)
   _or_{AC,#}(x15,_or_AC(A,B)) -> _or_{AC,#}(x15,U101(and(isBool(A),isBool(B)),A,B))
   _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBool#(A)
   _xor_{AC,#}(x16,_xor_AC(A,A)) -> U111#(isBool(A))
   _xor_{AC,#}(x16,_xor_AC(A,A)) -> _xor_{AC,#}(x16,U111(isBool(A)))
   _xor_{AC,#}(x17,_xor_AC(false(),A)) -> isBool#(A)
   _xor_{AC,#}(x17,_xor_AC(false(),A)) -> U121#(isBool(A),A)
   _xor_{AC,#}(x17,_xor_AC(false(),A)) -> _xor_{AC,#}(x17,U121(isBool(A),A))
  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:
   U101(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
   U11(tt(),A) -> A
   U111(tt()) -> false()
   U121(tt(),A) -> A
   U131(tt(),B,U') -> U132(equal(_isNotEqualTo_(B,true()),true()),U')
   U132(tt(),U') -> U'
   U141(tt(),U) -> U
   U151(tt(),A) -> _xor_AC(A,true())
   U21(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
   U31(tt()) -> false()
   U41(tt(),A) -> A
   U51(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
   U61(tt(),U',U) -> U62(equal(_isNotEqualTo_(U,U'),true()))
   U62(tt()) -> false()
   U71(tt()) -> true()
   U81(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
   U91(tt()) -> false()
   _and_AC(A,A) -> U11(isBool(A),A)
   _and_AC(A,_xor_AC(B,C)) -> U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
   _and_AC(false(),A) -> U31(isBool(A))
   _and_AC(true(),A) -> U41(isBool(A),A)
   _implies_(A,B) -> U51(and(isBool(A),isBool(B)),A,B)
   _isEqualTo_(U,U') -> U61(and(isS(U'),isS(U)),U',U)
   _isEqualTo_(U,U) -> U71(isS(U))
   _isNotEqualTo_(U,U') -> U81(and(isS(U'),isS(U)),U',U)
   _isNotEqualTo_(U,U) -> U91(isS(U))
   _or_AC(A,B) -> U101(and(isBool(A),isBool(B)),A,B)
   _xor_AC(A,A) -> U111(isBool(A))
   _xor_AC(false(),A) -> U121(isBool(A),A)
   and(tt(),X) -> X
   equal(X,X) -> tt()
   if_then_else_fi(B,U,U') -> U131(and(isBool(B),and(isS(U'),isS(U))),B,U')
   if_then_else_fi(true(),U,U') -> U141(and(isS(U'),isS(U)),U)
   isBool(false()) -> tt()
   isBool(true()) -> tt()
   isBool(_and_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
   isBool(_implies_(V1,V2)) -> and(isBool(V1),isBool(V2))
   isBool(_isEqualTo_(V1,V2)) -> and(isUniversal(V1),isUniversal(V2))
   isBool(_isNotEqualTo_(V1,V2)) -> and(isUniversal(V1),isUniversal(V2))
   isBool(_or_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
   isBool(_xor_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
   isBool(not_(V1)) -> isBool(V1)
   not_(A) -> U151(isBool(A),A)
   not_(false()) -> true()
   not_(true()) -> false()
  S:
   _xor_{AC,#}(_xor_AC(x18,x19),x20) -> _xor_{AC,#}(x18,x19)
   _xor_{AC,#}(x18,_xor_AC(x19,x20)) -> _xor_{AC,#}(x19,x20)
   _and_{AC,#}(_and_AC(x18,x19),x20) -> _and_{AC,#}(x18,x19)
   _and_{AC,#}(x18,_and_AC(x19,x20)) -> _and_{AC,#}(x19,x20)
   _or_{AC,#}(_or_AC(x18,x19),x20) -> _or_{AC,#}(x18,x19)
   _or_{AC,#}(x18,_or_AC(x19,x20)) -> _or_{AC,#}(x19,x20)
  AC-EDG Processor:
   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)
   DPs:
    U101#(tt(),A,B) -> _xor_{AC,#}(A,B)
    U101#(tt(),A,B) -> _and_{AC,#}(A,B)
    U101#(tt(),A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
    U131#(tt(),B,U') -> _isNotEqualTo_#(B,true())
    U131#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
    U131#(tt(),B,U') -> U132#(equal(_isNotEqualTo_(B,true()),true()),U')
    U151#(tt(),A) -> _xor_{AC,#}(A,true())
    U21#(tt(),A,B,C) -> _and_{AC,#}(A,C)
    U21#(tt(),A,B,C) -> _and_{AC,#}(A,B)
    U21#(tt(),A,B,C) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
    U51#(tt(),A,B) -> _and_{AC,#}(A,B)
    U51#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(A,B))
    U51#(tt(),A,B) -> not_#(_xor_AC(A,_and_AC(A,B)))
    U61#(tt(),U',U) -> _isNotEqualTo_#(U,U')
    U61#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
    U61#(tt(),U',U) -> U62#(equal(_isNotEqualTo_(U,U'),true()))
    U81#(tt(),U',U) -> _isEqualTo_#(U,U')
    U81#(tt(),U',U) -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true())
    _and_{AC,#}(A,A) -> isBool#(A)
    _and_{AC,#}(A,A) -> U11#(isBool(A),A)
    _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(C)
    _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(B)
    _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(B),isBool(C))
    _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(A)
    _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(A),and(isBool(B),isBool(C)))
    _and_{AC,#}(A,_xor_AC(B,C)) -> U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
    _and_{AC,#}(false(),A) -> isBool#(A)
    _and_{AC,#}(false(),A) -> U31#(isBool(A))
    _and_{AC,#}(true(),A) -> isBool#(A)
    _and_{AC,#}(true(),A) -> U41#(isBool(A),A)
    _implies_#(A,B) -> isBool#(B)
    _implies_#(A,B) -> isBool#(A)
    _implies_#(A,B) -> and#(isBool(A),isBool(B))
    _implies_#(A,B) -> U51#(and(isBool(A),isBool(B)),A,B)
    _isEqualTo_#(U,U') -> and#(isS(U'),isS(U))
    _isEqualTo_#(U,U') -> U61#(and(isS(U'),isS(U)),U',U)
    _isEqualTo_#(U,U) -> U71#(isS(U))
    _isNotEqualTo_#(U,U') -> and#(isS(U'),isS(U))
    _isNotEqualTo_#(U,U') -> U81#(and(isS(U'),isS(U)),U',U)
    _isNotEqualTo_#(U,U) -> U91#(isS(U))
    _or_{AC,#}(A,B) -> isBool#(B)
    _or_{AC,#}(A,B) -> isBool#(A)
    _or_{AC,#}(A,B) -> and#(isBool(A),isBool(B))
    _or_{AC,#}(A,B) -> U101#(and(isBool(A),isBool(B)),A,B)
    _xor_{AC,#}(A,A) -> isBool#(A)
    _xor_{AC,#}(A,A) -> U111#(isBool(A))
    _xor_{AC,#}(false(),A) -> isBool#(A)
    _xor_{AC,#}(false(),A) -> U121#(isBool(A),A)
    if_then_else_fi#(B,U,U') -> and#(isS(U'),isS(U))
    if_then_else_fi#(B,U,U') -> isBool#(B)
    if_then_else_fi#(B,U,U') -> and#(isBool(B),and(isS(U'),isS(U)))
    if_then_else_fi#(B,U,U') -> U131#(and(isBool(B),and(isS(U'),isS(U))),B,U')
    if_then_else_fi#(true(),U,U') -> and#(isS(U'),isS(U))
    if_then_else_fi#(true(),U,U') -> U141#(and(isS(U'),isS(U)),U)
    isBool#(_and_AC(V1,V2)) -> isBool#(V2)
    isBool#(_and_AC(V1,V2)) -> isBool#(V1)
    isBool#(_and_AC(V1,V2)) -> and#(isBool(V1),isBool(V2))
    isBool#(_implies_(V1,V2)) -> isBool#(V2)
    isBool#(_implies_(V1,V2)) -> isBool#(V1)
    isBool#(_implies_(V1,V2)) -> and#(isBool(V1),isBool(V2))
    isBool#(_isEqualTo_(V1,V2)) -> and#(isUniversal(V1),isUniversal(V2))
    isBool#(_isNotEqualTo_(V1,V2)) -> and#(isUniversal(V1),isUniversal(V2))
    isBool#(_or_AC(V1,V2)) -> isBool#(V2)
    isBool#(_or_AC(V1,V2)) -> isBool#(V1)
    isBool#(_or_AC(V1,V2)) -> and#(isBool(V1),isBool(V2))
    isBool#(_xor_AC(V1,V2)) -> isBool#(V2)
    isBool#(_xor_AC(V1,V2)) -> isBool#(V1)
    isBool#(_xor_AC(V1,V2)) -> and#(isBool(V1),isBool(V2))
    isBool#(not_(V1)) -> isBool#(V1)
    not_#(A) -> isBool#(A)
    not_#(A) -> U151#(isBool(A),A)
    _and_{AC,#}(x11,_and_AC(A,A)) -> isBool#(A)
    _and_{AC,#}(x11,_and_AC(A,A)) -> U11#(isBool(A),A)
    _and_{AC,#}(x11,_and_AC(A,A)) -> _and_{AC,#}(x11,U11(isBool(A),A))
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(C)
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(B)
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(B),isBool(C))
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(A)
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(A),and(isBool(B),isBool(C)))
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) ->
    _and_{AC,#}(x12,U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C))
    _and_{AC,#}(x13,_and_AC(false(),A)) -> isBool#(A)
    _and_{AC,#}(x13,_and_AC(false(),A)) -> U31#(isBool(A))
    _and_{AC,#}(x13,_and_AC(false(),A)) -> _and_{AC,#}(x13,U31(isBool(A)))
    _and_{AC,#}(x14,_and_AC(true(),A)) -> isBool#(A)
    _and_{AC,#}(x14,_and_AC(true(),A)) -> U41#(isBool(A),A)
    _and_{AC,#}(x14,_and_AC(true(),A)) -> _and_{AC,#}(x14,U41(isBool(A),A))
    _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(B)
    _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(A)
    _or_{AC,#}(x15,_or_AC(A,B)) -> and#(isBool(A),isBool(B))
    _or_{AC,#}(x15,_or_AC(A,B)) -> U101#(and(isBool(A),isBool(B)),A,B)
    _or_{AC,#}(x15,_or_AC(A,B)) -> _or_{AC,#}(x15,U101(and(isBool(A),isBool(B)),A,B))
    _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBool#(A)
    _xor_{AC,#}(x16,_xor_AC(A,A)) -> U111#(isBool(A))
    _xor_{AC,#}(x16,_xor_AC(A,A)) -> _xor_{AC,#}(x16,U111(isBool(A)))
    _xor_{AC,#}(x17,_xor_AC(false(),A)) -> isBool#(A)
    _xor_{AC,#}(x17,_xor_AC(false(),A)) -> U121#(isBool(A),A)
    _xor_{AC,#}(x17,_xor_AC(false(),A)) -> _xor_{AC,#}(x17,U121(isBool(A),A))
   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:
    U101(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
    U11(tt(),A) -> A
    U111(tt()) -> false()
    U121(tt(),A) -> A
    U131(tt(),B,U') -> U132(equal(_isNotEqualTo_(B,true()),true()),U')
    U132(tt(),U') -> U'
    U141(tt(),U) -> U
    U151(tt(),A) -> _xor_AC(A,true())
    U21(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
    U31(tt()) -> false()
    U41(tt(),A) -> A
    U51(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
    U61(tt(),U',U) -> U62(equal(_isNotEqualTo_(U,U'),true()))
    U62(tt()) -> false()
    U71(tt()) -> true()
    U81(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
    U91(tt()) -> false()
    _and_AC(A,A) -> U11(isBool(A),A)
    _and_AC(A,_xor_AC(B,C)) -> U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)
    _and_AC(false(),A) -> U31(isBool(A))
    _and_AC(true(),A) -> U41(isBool(A),A)
    _implies_(A,B) -> U51(and(isBool(A),isBool(B)),A,B)
    _isEqualTo_(U,U') -> U61(and(isS(U'),isS(U)),U',U)
    _isEqualTo_(U,U) -> U71(isS(U))
    _isNotEqualTo_(U,U') -> U81(and(isS(U'),isS(U)),U',U)
    _isNotEqualTo_(U,U) -> U91(isS(U))
    _or_AC(A,B) -> U101(and(isBool(A),isBool(B)),A,B)
    _xor_AC(A,A) -> U111(isBool(A))
    _xor_AC(false(),A) -> U121(isBool(A),A)
    and(tt(),X) -> X
    equal(X,X) -> tt()
    if_then_else_fi(B,U,U') -> U131(and(isBool(B),and(isS(U'),isS(U))),B,U')
    if_then_else_fi(true(),U,U') -> U141(and(isS(U'),isS(U)),U)
    isBool(false()) -> tt()
    isBool(true()) -> tt()
    isBool(_and_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
    isBool(_implies_(V1,V2)) -> and(isBool(V1),isBool(V2))
    isBool(_isEqualTo_(V1,V2)) -> and(isUniversal(V1),isUniversal(V2))
    isBool(_isNotEqualTo_(V1,V2)) -> and(isUniversal(V1),isUniversal(V2))
    isBool(_or_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
    isBool(_xor_AC(V1,V2)) -> and(isBool(V1),isBool(V2))
    isBool(not_(V1)) -> isBool(V1)
    not_(A) -> U151(isBool(A),A)
    not_(false()) -> true()
    not_(true()) -> false()
   S:
    _xor_{AC,#}(_xor_AC(x18,x19),x20) -> _xor_{AC,#}(x18,x19)
    _xor_{AC,#}(x18,_xor_AC(x19,x20)) -> _xor_{AC,#}(x19,x20)
    _and_{AC,#}(_and_AC(x18,x19),x20) -> _and_{AC,#}(x18,x19)
    _and_{AC,#}(x18,_and_AC(x19,x20)) -> _and_{AC,#}(x19,x20)
    _or_{AC,#}(_or_AC(x18,x19),x20) -> _or_{AC,#}(x18,x19)
    _or_{AC,#}(x18,_or_AC(x19,x20)) -> _or_{AC,#}(x19,x20)
   Open