MAYBE
Time: 44.824

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) -> U102(isBoolKind(A),A,B)
  U102(tt(),A,B) -> U103(isBool(B),A,B)
  U103(tt(),A,B) -> U104(isBoolKind(B),A,B)
  U104(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
  U11(tt(),A) -> U12(isBoolKind(A),A)
  U111(tt(),A) -> U112(isBoolKind(A))
  U112(tt()) -> false()
  U12(tt(),A) -> A
  U121(tt(),A) -> U122(isBoolKind(A),A)
  U122(tt(),A) -> A
  U131(tt(),B,U',U) -> U132(isBoolKind(B),B,U',U)
  U132(tt(),B,U',U) -> U133(isS(U'),B,U',U)
  U133(tt(),B,U',U) -> U134(isSKind(U'),B,U',U)
  U134(tt(),B,U',U) -> U135(isS(U),B,U',U)
  U135(tt(),B,U',U) -> U136(isSKind(U),B,U')
  U136(tt(),B,U') -> U137(equal(_isNotEqualTo_(B,true()),true()),U')
  U137(tt(),U') -> U'
  U141(tt(),U',U) -> U142(isSKind(U'),U)
  U142(tt(),U) -> U143(isS(U),U)
  U143(tt(),U) -> U144(isSKind(U),U)
  U144(tt(),U) -> U
  U151(tt(),V1,V2) -> U152(isBoolKind(V1),V1,V2)
  U152(tt(),V1,V2) -> U153(isBoolKind(V2),V1,V2)
  U153(tt(),V1,V2) -> U154(isBoolKind(V2),V1,V2)
  U154(tt(),V1,V2) -> U155(isBool(V1),V2)
  U155(tt(),V2) -> U156(isBool(V2))
  U156(tt()) -> tt()
  U161(tt(),V1,V2) -> U162(isBoolKind(V1),V1,V2)
  U162(tt(),V1,V2) -> U163(isBoolKind(V2),V1,V2)
  U163(tt(),V1,V2) -> U164(isBoolKind(V2),V1,V2)
  U164(tt(),V1,V2) -> U165(isBool(V1),V2)
  U165(tt(),V2) -> U166(isBool(V2))
  U166(tt()) -> tt()
  U171(tt(),V1,V2) -> U172(isBoolKind(V1),V1,V2)
  U172(tt(),V1,V2) -> U173(isBoolKind(V2),V1,V2)
  U173(tt(),V1,V2) -> U174(isBoolKind(V2),V1,V2)
  U174(tt(),V1,V2) -> U175(isBool(V1),V2)
  U175(tt(),V2) -> U176(isBool(V2))
  U176(tt()) -> tt()
  U181(tt(),V1,V2) -> U182(isBoolKind(V1),V1,V2)
  U182(tt(),V1,V2) -> U183(isBoolKind(V2),V1,V2)
  U183(tt(),V1,V2) -> U184(isBoolKind(V2),V1,V2)
  U184(tt(),V1,V2) -> U185(isBool(V1),V2)
  U185(tt(),V2) -> U186(isBool(V2))
  U186(tt()) -> tt()
  U191(tt(),V1) -> U192(isBoolKind(V1),V1)
  U192(tt(),V1) -> U193(isBool(V1))
  U193(tt()) -> tt()
  U201(tt(),V2) -> U202(isBoolKind(V2))
  U202(tt()) -> tt()
  U21(tt(),A,B,C) -> U22(isBoolKind(A),A,B,C)
  U211(tt(),V2) -> U212(isBoolKind(V2))
  U212(tt()) -> tt()
  U22(tt(),A,B,C) -> U23(isBool(B),A,B,C)
  U221(tt(),V2) -> U222(isBoolKind(V2))
  U222(tt()) -> tt()
  U23(tt(),A,B,C) -> U24(isBoolKind(B),A,B,C)
  U231(tt(),V2) -> U232(isBoolKind(V2))
  U232(tt()) -> tt()
  U24(tt(),A,B,C) -> U25(isBool(C),A,B,C)
  U241(tt()) -> tt()
  U25(tt(),A,B,C) -> U26(isBoolKind(C),A,B,C)
  U251(tt(),A) -> U252(isBoolKind(A),A)
  U252(tt(),A) -> _xor_AC(A,true())
  U26(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
  U31(tt(),A) -> U32(isBoolKind(A))
  U32(tt()) -> false()
  U41(tt(),A) -> U42(isBoolKind(A),A)
  U42(tt(),A) -> A
  U51(tt(),A,B) -> U52(isBoolKind(A),A,B)
  U52(tt(),A,B) -> U53(isBool(B),A,B)
  U53(tt(),A,B) -> U54(isBoolKind(B),A,B)
  U54(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
  U61(tt(),U',U) -> U62(isSKind(U'),U',U)
  U62(tt(),U',U) -> U63(isS(U),U',U)
  U63(tt(),U',U) -> U64(isSKind(U),U',U)
  U64(tt(),U',U) -> U65(equal(_isNotEqualTo_(U,U'),true()))
  U65(tt()) -> false()
  U71(tt(),U) -> U72(isSKind(U))
  U72(tt()) -> true()
  U81(tt(),U',U) -> U82(isSKind(U'),U',U)
  U82(tt(),U',U) -> U83(isS(U),U',U)
  U83(tt(),U',U) -> U84(isSKind(U),U',U)
  U84(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
  U91(tt(),U) -> U92(isSKind(U))
  U92(tt()) -> false()
  _and_AC(A,A) -> U11(isBool(A),A)
  _and_AC(A,_xor_AC(B,C)) -> U21(isBool(A),A,B,C)
  _and_AC(false(),A) -> U31(isBool(A),A)
  _and_AC(true(),A) -> U41(isBool(A),A)
  _implies_(A,B) -> U51(isBool(A),A,B)
  _isEqualTo_(U,U') -> U61(isS(U'),U',U)
  _isEqualTo_(U,U) -> U71(isS(U),U)
  _isNotEqualTo_(U,U') -> U81(isS(U'),U',U)
  _isNotEqualTo_(U,U) -> U91(isS(U),U)
  _or_AC(A,B) -> U101(isBool(A),A,B)
  _xor_AC(A,A) -> U111(isBool(A),A)
  _xor_AC(false(),A) -> U121(isBool(A),A)
  equal(X,X) -> tt()
  if_then_else_fi(B,U,U') -> U131(isBool(B),B,U',U)
  if_then_else_fi(true(),U,U') -> U141(isS(U'),U',U)
  isBool(false()) -> tt()
  isBool(true()) -> tt()
  isBool(_and_AC(V1,V2)) -> U151(isBoolKind(V1),V1,V2)
  isBool(_implies_(V1,V2)) -> U161(isBoolKind(V1),V1,V2)
  isBool(_isEqualTo_(V1,V2)) -> tt()
  isBool(_isNotEqualTo_(V1,V2)) -> tt()
  isBool(_or_AC(V1,V2)) -> U171(isBoolKind(V1),V1,V2)
  isBool(_xor_AC(V1,V2)) -> U181(isBoolKind(V1),V1,V2)
  isBool(not_(V1)) -> U191(isBoolKind(V1),V1)
  isBoolKind(false()) -> tt()
  isBoolKind(true()) -> tt()
  isBoolKind(_and_AC(V1,V2)) -> U201(isBoolKind(V1),V2)
  isBoolKind(_implies_(V1,V2)) -> U211(isBoolKind(V1),V2)
  isBoolKind(_isEqualTo_(V1,V2)) -> tt()
  isBoolKind(_isNotEqualTo_(V1,V2)) -> tt()
  isBoolKind(_or_AC(V1,V2)) -> U221(isBoolKind(V1),V2)
  isBoolKind(_xor_AC(V1,V2)) -> U231(isBoolKind(V1),V2)
  isBoolKind(not_(V1)) -> U241(isBoolKind(V1))
  not_(A) -> U251(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) -> isBoolKind#(A)
   U101#(tt(),A,B) -> U102#(isBoolKind(A),A,B)
   U102#(tt(),A,B) -> isBool#(B)
   U102#(tt(),A,B) -> U103#(isBool(B),A,B)
   U103#(tt(),A,B) -> isBoolKind#(B)
   U103#(tt(),A,B) -> U104#(isBoolKind(B),A,B)
   U104#(tt(),A,B) -> _xor_{AC,#}(A,B)
   U104#(tt(),A,B) -> _and_{AC,#}(A,B)
   U104#(tt(),A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
   U11#(tt(),A) -> isBoolKind#(A)
   U11#(tt(),A) -> U12#(isBoolKind(A),A)
   U111#(tt(),A) -> isBoolKind#(A)
   U111#(tt(),A) -> U112#(isBoolKind(A))
   U121#(tt(),A) -> isBoolKind#(A)
   U121#(tt(),A) -> U122#(isBoolKind(A),A)
   U131#(tt(),B,U',U) -> isBoolKind#(B)
   U131#(tt(),B,U',U) -> U132#(isBoolKind(B),B,U',U)
   U132#(tt(),B,U',U) -> U133#(isS(U'),B,U',U)
   U133#(tt(),B,U',U) -> U134#(isSKind(U'),B,U',U)
   U134#(tt(),B,U',U) -> U135#(isS(U),B,U',U)
   U135#(tt(),B,U',U) -> U136#(isSKind(U),B,U')
   U136#(tt(),B,U') -> _isNotEqualTo_#(B,true())
   U136#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
   U136#(tt(),B,U') -> U137#(equal(_isNotEqualTo_(B,true()),true()),U')
   U141#(tt(),U',U) -> U142#(isSKind(U'),U)
   U142#(tt(),U) -> U143#(isS(U),U)
   U143#(tt(),U) -> U144#(isSKind(U),U)
   U151#(tt(),V1,V2) -> isBoolKind#(V1)
   U151#(tt(),V1,V2) -> U152#(isBoolKind(V1),V1,V2)
   U152#(tt(),V1,V2) -> isBoolKind#(V2)
   U152#(tt(),V1,V2) -> U153#(isBoolKind(V2),V1,V2)
   U153#(tt(),V1,V2) -> isBoolKind#(V2)
   U153#(tt(),V1,V2) -> U154#(isBoolKind(V2),V1,V2)
   U154#(tt(),V1,V2) -> isBool#(V1)
   U154#(tt(),V1,V2) -> U155#(isBool(V1),V2)
   U155#(tt(),V2) -> isBool#(V2)
   U155#(tt(),V2) -> U156#(isBool(V2))
   U161#(tt(),V1,V2) -> isBoolKind#(V1)
   U161#(tt(),V1,V2) -> U162#(isBoolKind(V1),V1,V2)
   U162#(tt(),V1,V2) -> isBoolKind#(V2)
   U162#(tt(),V1,V2) -> U163#(isBoolKind(V2),V1,V2)
   U163#(tt(),V1,V2) -> isBoolKind#(V2)
   U163#(tt(),V1,V2) -> U164#(isBoolKind(V2),V1,V2)
   U164#(tt(),V1,V2) -> isBool#(V1)
   U164#(tt(),V1,V2) -> U165#(isBool(V1),V2)
   U165#(tt(),V2) -> isBool#(V2)
   U165#(tt(),V2) -> U166#(isBool(V2))
   U171#(tt(),V1,V2) -> isBoolKind#(V1)
   U171#(tt(),V1,V2) -> U172#(isBoolKind(V1),V1,V2)
   U172#(tt(),V1,V2) -> isBoolKind#(V2)
   U172#(tt(),V1,V2) -> U173#(isBoolKind(V2),V1,V2)
   U173#(tt(),V1,V2) -> isBoolKind#(V2)
   U173#(tt(),V1,V2) -> U174#(isBoolKind(V2),V1,V2)
   U174#(tt(),V1,V2) -> isBool#(V1)
   U174#(tt(),V1,V2) -> U175#(isBool(V1),V2)
   U175#(tt(),V2) -> isBool#(V2)
   U175#(tt(),V2) -> U176#(isBool(V2))
   U181#(tt(),V1,V2) -> isBoolKind#(V1)
   U181#(tt(),V1,V2) -> U182#(isBoolKind(V1),V1,V2)
   U182#(tt(),V1,V2) -> isBoolKind#(V2)
   U182#(tt(),V1,V2) -> U183#(isBoolKind(V2),V1,V2)
   U183#(tt(),V1,V2) -> isBoolKind#(V2)
   U183#(tt(),V1,V2) -> U184#(isBoolKind(V2),V1,V2)
   U184#(tt(),V1,V2) -> isBool#(V1)
   U184#(tt(),V1,V2) -> U185#(isBool(V1),V2)
   U185#(tt(),V2) -> isBool#(V2)
   U185#(tt(),V2) -> U186#(isBool(V2))
   U191#(tt(),V1) -> isBoolKind#(V1)
   U191#(tt(),V1) -> U192#(isBoolKind(V1),V1)
   U192#(tt(),V1) -> isBool#(V1)
   U192#(tt(),V1) -> U193#(isBool(V1))
   U201#(tt(),V2) -> isBoolKind#(V2)
   U201#(tt(),V2) -> U202#(isBoolKind(V2))
   U21#(tt(),A,B,C) -> isBoolKind#(A)
   U21#(tt(),A,B,C) -> U22#(isBoolKind(A),A,B,C)
   U211#(tt(),V2) -> isBoolKind#(V2)
   U211#(tt(),V2) -> U212#(isBoolKind(V2))
   U22#(tt(),A,B,C) -> isBool#(B)
   U22#(tt(),A,B,C) -> U23#(isBool(B),A,B,C)
   U221#(tt(),V2) -> isBoolKind#(V2)
   U221#(tt(),V2) -> U222#(isBoolKind(V2))
   U23#(tt(),A,B,C) -> isBoolKind#(B)
   U23#(tt(),A,B,C) -> U24#(isBoolKind(B),A,B,C)
   U231#(tt(),V2) -> isBoolKind#(V2)
   U231#(tt(),V2) -> U232#(isBoolKind(V2))
   U24#(tt(),A,B,C) -> isBool#(C)
   U24#(tt(),A,B,C) -> U25#(isBool(C),A,B,C)
   U25#(tt(),A,B,C) -> isBoolKind#(C)
   U25#(tt(),A,B,C) -> U26#(isBoolKind(C),A,B,C)
   U251#(tt(),A) -> isBoolKind#(A)
   U251#(tt(),A) -> U252#(isBoolKind(A),A)
   U252#(tt(),A) -> _xor_{AC,#}(A,true())
   U26#(tt(),A,B,C) -> _and_{AC,#}(A,C)
   U26#(tt(),A,B,C) -> _and_{AC,#}(A,B)
   U26#(tt(),A,B,C) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
   U31#(tt(),A) -> isBoolKind#(A)
   U31#(tt(),A) -> U32#(isBoolKind(A))
   U41#(tt(),A) -> isBoolKind#(A)
   U41#(tt(),A) -> U42#(isBoolKind(A),A)
   U51#(tt(),A,B) -> isBoolKind#(A)
   U51#(tt(),A,B) -> U52#(isBoolKind(A),A,B)
   U52#(tt(),A,B) -> isBool#(B)
   U52#(tt(),A,B) -> U53#(isBool(B),A,B)
   U53#(tt(),A,B) -> isBoolKind#(B)
   U53#(tt(),A,B) -> U54#(isBoolKind(B),A,B)
   U54#(tt(),A,B) -> _and_{AC,#}(A,B)
   U54#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(A,B))
   U54#(tt(),A,B) -> not_#(_xor_AC(A,_and_AC(A,B)))
   U61#(tt(),U',U) -> U62#(isSKind(U'),U',U)
   U62#(tt(),U',U) -> U63#(isS(U),U',U)
   U63#(tt(),U',U) -> U64#(isSKind(U),U',U)
   U64#(tt(),U',U) -> _isNotEqualTo_#(U,U')
   U64#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
   U64#(tt(),U',U) -> U65#(equal(_isNotEqualTo_(U,U'),true()))
   U71#(tt(),U) -> U72#(isSKind(U))
   U81#(tt(),U',U) -> U82#(isSKind(U'),U',U)
   U82#(tt(),U',U) -> U83#(isS(U),U',U)
   U83#(tt(),U',U) -> U84#(isSKind(U),U',U)
   U84#(tt(),U',U) -> _isEqualTo_#(U,U')
   U84#(tt(),U',U) -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true())
   U91#(tt(),U) -> U92#(isSKind(U))
   _and_{AC,#}(A,A) -> isBool#(A)
   _and_{AC,#}(A,A) -> U11#(isBool(A),A)
   _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(A)
   _and_{AC,#}(A,_xor_AC(B,C)) -> U21#(isBool(A),A,B,C)
   _and_{AC,#}(false(),A) -> isBool#(A)
   _and_{AC,#}(false(),A) -> U31#(isBool(A),A)
   _and_{AC,#}(true(),A) -> isBool#(A)
   _and_{AC,#}(true(),A) -> U41#(isBool(A),A)
   _implies_#(A,B) -> isBool#(A)
   _implies_#(A,B) -> U51#(isBool(A),A,B)
   _isEqualTo_#(U,U') -> U61#(isS(U'),U',U)
   _isEqualTo_#(U,U) -> U71#(isS(U),U)
   _isNotEqualTo_#(U,U') -> U81#(isS(U'),U',U)
   _isNotEqualTo_#(U,U) -> U91#(isS(U),U)
   _or_{AC,#}(A,B) -> isBool#(A)
   _or_{AC,#}(A,B) -> U101#(isBool(A),A,B)
   _xor_{AC,#}(A,A) -> isBool#(A)
   _xor_{AC,#}(A,A) -> U111#(isBool(A),A)
   _xor_{AC,#}(false(),A) -> isBool#(A)
   _xor_{AC,#}(false(),A) -> U121#(isBool(A),A)
   if_then_else_fi#(B,U,U') -> isBool#(B)
   if_then_else_fi#(B,U,U') -> U131#(isBool(B),B,U',U)
   if_then_else_fi#(true(),U,U') -> U141#(isS(U'),U',U)
   isBool#(_and_AC(V1,V2)) -> isBoolKind#(V1)
   isBool#(_and_AC(V1,V2)) -> U151#(isBoolKind(V1),V1,V2)
   isBool#(_implies_(V1,V2)) -> isBoolKind#(V1)
   isBool#(_implies_(V1,V2)) -> U161#(isBoolKind(V1),V1,V2)
   isBool#(_or_AC(V1,V2)) -> isBoolKind#(V1)
   isBool#(_or_AC(V1,V2)) -> U171#(isBoolKind(V1),V1,V2)
   isBool#(_xor_AC(V1,V2)) -> isBoolKind#(V1)
   isBool#(_xor_AC(V1,V2)) -> U181#(isBoolKind(V1),V1,V2)
   isBool#(not_(V1)) -> isBoolKind#(V1)
   isBool#(not_(V1)) -> U191#(isBoolKind(V1),V1)
   isBoolKind#(_and_AC(V1,V2)) -> isBoolKind#(V1)
   isBoolKind#(_and_AC(V1,V2)) -> U201#(isBoolKind(V1),V2)
   isBoolKind#(_implies_(V1,V2)) -> isBoolKind#(V1)
   isBoolKind#(_implies_(V1,V2)) -> U211#(isBoolKind(V1),V2)
   isBoolKind#(_or_AC(V1,V2)) -> isBoolKind#(V1)
   isBoolKind#(_or_AC(V1,V2)) -> U221#(isBoolKind(V1),V2)
   isBoolKind#(_xor_AC(V1,V2)) -> isBoolKind#(V1)
   isBoolKind#(_xor_AC(V1,V2)) -> U231#(isBoolKind(V1),V2)
   isBoolKind#(not_(V1)) -> isBoolKind#(V1)
   isBoolKind#(not_(V1)) -> U241#(isBoolKind(V1))
   not_#(A) -> isBool#(A)
   not_#(A) -> U251#(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#(A)
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> U21#(isBool(A),A,B,C)
   _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x12,U21(isBool(A),A,B,C))
   _and_{AC,#}(x13,_and_AC(false(),A)) -> isBool#(A)
   _and_{AC,#}(x13,_and_AC(false(),A)) -> U31#(isBool(A),A)
   _and_{AC,#}(x13,_and_AC(false(),A)) -> _and_{AC,#}(x13,U31(isBool(A),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#(A)
   _or_{AC,#}(x15,_or_AC(A,B)) -> U101#(isBool(A),A,B)
   _or_{AC,#}(x15,_or_AC(A,B)) -> _or_{AC,#}(x15,U101(isBool(A),A,B))
   _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBool#(A)
   _xor_{AC,#}(x16,_xor_AC(A,A)) -> U111#(isBool(A),A)
   _xor_{AC,#}(x16,_xor_AC(A,A)) -> _xor_{AC,#}(x16,U111(isBool(A),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) -> U102(isBoolKind(A),A,B)
   U102(tt(),A,B) -> U103(isBool(B),A,B)
   U103(tt(),A,B) -> U104(isBoolKind(B),A,B)
   U104(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
   U11(tt(),A) -> U12(isBoolKind(A),A)
   U111(tt(),A) -> U112(isBoolKind(A))
   U112(tt()) -> false()
   U12(tt(),A) -> A
   U121(tt(),A) -> U122(isBoolKind(A),A)
   U122(tt(),A) -> A
   U131(tt(),B,U',U) -> U132(isBoolKind(B),B,U',U)
   U132(tt(),B,U',U) -> U133(isS(U'),B,U',U)
   U133(tt(),B,U',U) -> U134(isSKind(U'),B,U',U)
   U134(tt(),B,U',U) -> U135(isS(U),B,U',U)
   U135(tt(),B,U',U) -> U136(isSKind(U),B,U')
   U136(tt(),B,U') -> U137(equal(_isNotEqualTo_(B,true()),true()),U')
   U137(tt(),U') -> U'
   U141(tt(),U',U) -> U142(isSKind(U'),U)
   U142(tt(),U) -> U143(isS(U),U)
   U143(tt(),U) -> U144(isSKind(U),U)
   U144(tt(),U) -> U
   U151(tt(),V1,V2) -> U152(isBoolKind(V1),V1,V2)
   U152(tt(),V1,V2) -> U153(isBoolKind(V2),V1,V2)
   U153(tt(),V1,V2) -> U154(isBoolKind(V2),V1,V2)
   U154(tt(),V1,V2) -> U155(isBool(V1),V2)
   U155(tt(),V2) -> U156(isBool(V2))
   U156(tt()) -> tt()
   U161(tt(),V1,V2) -> U162(isBoolKind(V1),V1,V2)
   U162(tt(),V1,V2) -> U163(isBoolKind(V2),V1,V2)
   U163(tt(),V1,V2) -> U164(isBoolKind(V2),V1,V2)
   U164(tt(),V1,V2) -> U165(isBool(V1),V2)
   U165(tt(),V2) -> U166(isBool(V2))
   U166(tt()) -> tt()
   U171(tt(),V1,V2) -> U172(isBoolKind(V1),V1,V2)
   U172(tt(),V1,V2) -> U173(isBoolKind(V2),V1,V2)
   U173(tt(),V1,V2) -> U174(isBoolKind(V2),V1,V2)
   U174(tt(),V1,V2) -> U175(isBool(V1),V2)
   U175(tt(),V2) -> U176(isBool(V2))
   U176(tt()) -> tt()
   U181(tt(),V1,V2) -> U182(isBoolKind(V1),V1,V2)
   U182(tt(),V1,V2) -> U183(isBoolKind(V2),V1,V2)
   U183(tt(),V1,V2) -> U184(isBoolKind(V2),V1,V2)
   U184(tt(),V1,V2) -> U185(isBool(V1),V2)
   U185(tt(),V2) -> U186(isBool(V2))
   U186(tt()) -> tt()
   U191(tt(),V1) -> U192(isBoolKind(V1),V1)
   U192(tt(),V1) -> U193(isBool(V1))
   U193(tt()) -> tt()
   U201(tt(),V2) -> U202(isBoolKind(V2))
   U202(tt()) -> tt()
   U21(tt(),A,B,C) -> U22(isBoolKind(A),A,B,C)
   U211(tt(),V2) -> U212(isBoolKind(V2))
   U212(tt()) -> tt()
   U22(tt(),A,B,C) -> U23(isBool(B),A,B,C)
   U221(tt(),V2) -> U222(isBoolKind(V2))
   U222(tt()) -> tt()
   U23(tt(),A,B,C) -> U24(isBoolKind(B),A,B,C)
   U231(tt(),V2) -> U232(isBoolKind(V2))
   U232(tt()) -> tt()
   U24(tt(),A,B,C) -> U25(isBool(C),A,B,C)
   U241(tt()) -> tt()
   U25(tt(),A,B,C) -> U26(isBoolKind(C),A,B,C)
   U251(tt(),A) -> U252(isBoolKind(A),A)
   U252(tt(),A) -> _xor_AC(A,true())
   U26(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
   U31(tt(),A) -> U32(isBoolKind(A))
   U32(tt()) -> false()
   U41(tt(),A) -> U42(isBoolKind(A),A)
   U42(tt(),A) -> A
   U51(tt(),A,B) -> U52(isBoolKind(A),A,B)
   U52(tt(),A,B) -> U53(isBool(B),A,B)
   U53(tt(),A,B) -> U54(isBoolKind(B),A,B)
   U54(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
   U61(tt(),U',U) -> U62(isSKind(U'),U',U)
   U62(tt(),U',U) -> U63(isS(U),U',U)
   U63(tt(),U',U) -> U64(isSKind(U),U',U)
   U64(tt(),U',U) -> U65(equal(_isNotEqualTo_(U,U'),true()))
   U65(tt()) -> false()
   U71(tt(),U) -> U72(isSKind(U))
   U72(tt()) -> true()
   U81(tt(),U',U) -> U82(isSKind(U'),U',U)
   U82(tt(),U',U) -> U83(isS(U),U',U)
   U83(tt(),U',U) -> U84(isSKind(U),U',U)
   U84(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
   U91(tt(),U) -> U92(isSKind(U))
   U92(tt()) -> false()
   _and_AC(A,A) -> U11(isBool(A),A)
   _and_AC(A,_xor_AC(B,C)) -> U21(isBool(A),A,B,C)
   _and_AC(false(),A) -> U31(isBool(A),A)
   _and_AC(true(),A) -> U41(isBool(A),A)
   _implies_(A,B) -> U51(isBool(A),A,B)
   _isEqualTo_(U,U') -> U61(isS(U'),U',U)
   _isEqualTo_(U,U) -> U71(isS(U),U)
   _isNotEqualTo_(U,U') -> U81(isS(U'),U',U)
   _isNotEqualTo_(U,U) -> U91(isS(U),U)
   _or_AC(A,B) -> U101(isBool(A),A,B)
   _xor_AC(A,A) -> U111(isBool(A),A)
   _xor_AC(false(),A) -> U121(isBool(A),A)
   equal(X,X) -> tt()
   if_then_else_fi(B,U,U') -> U131(isBool(B),B,U',U)
   if_then_else_fi(true(),U,U') -> U141(isS(U'),U',U)
   isBool(false()) -> tt()
   isBool(true()) -> tt()
   isBool(_and_AC(V1,V2)) -> U151(isBoolKind(V1),V1,V2)
   isBool(_implies_(V1,V2)) -> U161(isBoolKind(V1),V1,V2)
   isBool(_isEqualTo_(V1,V2)) -> tt()
   isBool(_isNotEqualTo_(V1,V2)) -> tt()
   isBool(_or_AC(V1,V2)) -> U171(isBoolKind(V1),V1,V2)
   isBool(_xor_AC(V1,V2)) -> U181(isBoolKind(V1),V1,V2)
   isBool(not_(V1)) -> U191(isBoolKind(V1),V1)
   isBoolKind(false()) -> tt()
   isBoolKind(true()) -> tt()
   isBoolKind(_and_AC(V1,V2)) -> U201(isBoolKind(V1),V2)
   isBoolKind(_implies_(V1,V2)) -> U211(isBoolKind(V1),V2)
   isBoolKind(_isEqualTo_(V1,V2)) -> tt()
   isBoolKind(_isNotEqualTo_(V1,V2)) -> tt()
   isBoolKind(_or_AC(V1,V2)) -> U221(isBoolKind(V1),V2)
   isBoolKind(_xor_AC(V1,V2)) -> U231(isBoolKind(V1),V2)
   isBoolKind(not_(V1)) -> U241(isBoolKind(V1))
   not_(A) -> U251(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) -> isBoolKind#(A)
    U101#(tt(),A,B) -> U102#(isBoolKind(A),A,B)
    U102#(tt(),A,B) -> isBool#(B)
    U102#(tt(),A,B) -> U103#(isBool(B),A,B)
    U103#(tt(),A,B) -> isBoolKind#(B)
    U103#(tt(),A,B) -> U104#(isBoolKind(B),A,B)
    U104#(tt(),A,B) -> _xor_{AC,#}(A,B)
    U104#(tt(),A,B) -> _and_{AC,#}(A,B)
    U104#(tt(),A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B))
    U11#(tt(),A) -> isBoolKind#(A)
    U11#(tt(),A) -> U12#(isBoolKind(A),A)
    U111#(tt(),A) -> isBoolKind#(A)
    U111#(tt(),A) -> U112#(isBoolKind(A))
    U121#(tt(),A) -> isBoolKind#(A)
    U121#(tt(),A) -> U122#(isBoolKind(A),A)
    U131#(tt(),B,U',U) -> isBoolKind#(B)
    U131#(tt(),B,U',U) -> U132#(isBoolKind(B),B,U',U)
    U132#(tt(),B,U',U) -> U133#(isS(U'),B,U',U)
    U133#(tt(),B,U',U) -> U134#(isSKind(U'),B,U',U)
    U134#(tt(),B,U',U) -> U135#(isS(U),B,U',U)
    U135#(tt(),B,U',U) -> U136#(isSKind(U),B,U')
    U136#(tt(),B,U') -> _isNotEqualTo_#(B,true())
    U136#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true())
    U136#(tt(),B,U') -> U137#(equal(_isNotEqualTo_(B,true()),true()),U')
    U141#(tt(),U',U) -> U142#(isSKind(U'),U)
    U142#(tt(),U) -> U143#(isS(U),U)
    U143#(tt(),U) -> U144#(isSKind(U),U)
    U151#(tt(),V1,V2) -> isBoolKind#(V1)
    U151#(tt(),V1,V2) -> U152#(isBoolKind(V1),V1,V2)
    U152#(tt(),V1,V2) -> isBoolKind#(V2)
    U152#(tt(),V1,V2) -> U153#(isBoolKind(V2),V1,V2)
    U153#(tt(),V1,V2) -> isBoolKind#(V2)
    U153#(tt(),V1,V2) -> U154#(isBoolKind(V2),V1,V2)
    U154#(tt(),V1,V2) -> isBool#(V1)
    U154#(tt(),V1,V2) -> U155#(isBool(V1),V2)
    U155#(tt(),V2) -> isBool#(V2)
    U155#(tt(),V2) -> U156#(isBool(V2))
    U161#(tt(),V1,V2) -> isBoolKind#(V1)
    U161#(tt(),V1,V2) -> U162#(isBoolKind(V1),V1,V2)
    U162#(tt(),V1,V2) -> isBoolKind#(V2)
    U162#(tt(),V1,V2) -> U163#(isBoolKind(V2),V1,V2)
    U163#(tt(),V1,V2) -> isBoolKind#(V2)
    U163#(tt(),V1,V2) -> U164#(isBoolKind(V2),V1,V2)
    U164#(tt(),V1,V2) -> isBool#(V1)
    U164#(tt(),V1,V2) -> U165#(isBool(V1),V2)
    U165#(tt(),V2) -> isBool#(V2)
    U165#(tt(),V2) -> U166#(isBool(V2))
    U171#(tt(),V1,V2) -> isBoolKind#(V1)
    U171#(tt(),V1,V2) -> U172#(isBoolKind(V1),V1,V2)
    U172#(tt(),V1,V2) -> isBoolKind#(V2)
    U172#(tt(),V1,V2) -> U173#(isBoolKind(V2),V1,V2)
    U173#(tt(),V1,V2) -> isBoolKind#(V2)
    U173#(tt(),V1,V2) -> U174#(isBoolKind(V2),V1,V2)
    U174#(tt(),V1,V2) -> isBool#(V1)
    U174#(tt(),V1,V2) -> U175#(isBool(V1),V2)
    U175#(tt(),V2) -> isBool#(V2)
    U175#(tt(),V2) -> U176#(isBool(V2))
    U181#(tt(),V1,V2) -> isBoolKind#(V1)
    U181#(tt(),V1,V2) -> U182#(isBoolKind(V1),V1,V2)
    U182#(tt(),V1,V2) -> isBoolKind#(V2)
    U182#(tt(),V1,V2) -> U183#(isBoolKind(V2),V1,V2)
    U183#(tt(),V1,V2) -> isBoolKind#(V2)
    U183#(tt(),V1,V2) -> U184#(isBoolKind(V2),V1,V2)
    U184#(tt(),V1,V2) -> isBool#(V1)
    U184#(tt(),V1,V2) -> U185#(isBool(V1),V2)
    U185#(tt(),V2) -> isBool#(V2)
    U185#(tt(),V2) -> U186#(isBool(V2))
    U191#(tt(),V1) -> isBoolKind#(V1)
    U191#(tt(),V1) -> U192#(isBoolKind(V1),V1)
    U192#(tt(),V1) -> isBool#(V1)
    U192#(tt(),V1) -> U193#(isBool(V1))
    U201#(tt(),V2) -> isBoolKind#(V2)
    U201#(tt(),V2) -> U202#(isBoolKind(V2))
    U21#(tt(),A,B,C) -> isBoolKind#(A)
    U21#(tt(),A,B,C) -> U22#(isBoolKind(A),A,B,C)
    U211#(tt(),V2) -> isBoolKind#(V2)
    U211#(tt(),V2) -> U212#(isBoolKind(V2))
    U22#(tt(),A,B,C) -> isBool#(B)
    U22#(tt(),A,B,C) -> U23#(isBool(B),A,B,C)
    U221#(tt(),V2) -> isBoolKind#(V2)
    U221#(tt(),V2) -> U222#(isBoolKind(V2))
    U23#(tt(),A,B,C) -> isBoolKind#(B)
    U23#(tt(),A,B,C) -> U24#(isBoolKind(B),A,B,C)
    U231#(tt(),V2) -> isBoolKind#(V2)
    U231#(tt(),V2) -> U232#(isBoolKind(V2))
    U24#(tt(),A,B,C) -> isBool#(C)
    U24#(tt(),A,B,C) -> U25#(isBool(C),A,B,C)
    U25#(tt(),A,B,C) -> isBoolKind#(C)
    U25#(tt(),A,B,C) -> U26#(isBoolKind(C),A,B,C)
    U251#(tt(),A) -> isBoolKind#(A)
    U251#(tt(),A) -> U252#(isBoolKind(A),A)
    U252#(tt(),A) -> _xor_{AC,#}(A,true())
    U26#(tt(),A,B,C) -> _and_{AC,#}(A,C)
    U26#(tt(),A,B,C) -> _and_{AC,#}(A,B)
    U26#(tt(),A,B,C) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C))
    U31#(tt(),A) -> isBoolKind#(A)
    U31#(tt(),A) -> U32#(isBoolKind(A))
    U41#(tt(),A) -> isBoolKind#(A)
    U41#(tt(),A) -> U42#(isBoolKind(A),A)
    U51#(tt(),A,B) -> isBoolKind#(A)
    U51#(tt(),A,B) -> U52#(isBoolKind(A),A,B)
    U52#(tt(),A,B) -> isBool#(B)
    U52#(tt(),A,B) -> U53#(isBool(B),A,B)
    U53#(tt(),A,B) -> isBoolKind#(B)
    U53#(tt(),A,B) -> U54#(isBoolKind(B),A,B)
    U54#(tt(),A,B) -> _and_{AC,#}(A,B)
    U54#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(A,B))
    U54#(tt(),A,B) -> not_#(_xor_AC(A,_and_AC(A,B)))
    U61#(tt(),U',U) -> U62#(isSKind(U'),U',U)
    U62#(tt(),U',U) -> U63#(isS(U),U',U)
    U63#(tt(),U',U) -> U64#(isSKind(U),U',U)
    U64#(tt(),U',U) -> _isNotEqualTo_#(U,U')
    U64#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true())
    U64#(tt(),U',U) -> U65#(equal(_isNotEqualTo_(U,U'),true()))
    U71#(tt(),U) -> U72#(isSKind(U))
    U81#(tt(),U',U) -> U82#(isSKind(U'),U',U)
    U82#(tt(),U',U) -> U83#(isS(U),U',U)
    U83#(tt(),U',U) -> U84#(isSKind(U),U',U)
    U84#(tt(),U',U) -> _isEqualTo_#(U,U')
    U84#(tt(),U',U) -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true())
    U91#(tt(),U) -> U92#(isSKind(U))
    _and_{AC,#}(A,A) -> isBool#(A)
    _and_{AC,#}(A,A) -> U11#(isBool(A),A)
    _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(A)
    _and_{AC,#}(A,_xor_AC(B,C)) -> U21#(isBool(A),A,B,C)
    _and_{AC,#}(false(),A) -> isBool#(A)
    _and_{AC,#}(false(),A) -> U31#(isBool(A),A)
    _and_{AC,#}(true(),A) -> isBool#(A)
    _and_{AC,#}(true(),A) -> U41#(isBool(A),A)
    _implies_#(A,B) -> isBool#(A)
    _implies_#(A,B) -> U51#(isBool(A),A,B)
    _isEqualTo_#(U,U') -> U61#(isS(U'),U',U)
    _isEqualTo_#(U,U) -> U71#(isS(U),U)
    _isNotEqualTo_#(U,U') -> U81#(isS(U'),U',U)
    _isNotEqualTo_#(U,U) -> U91#(isS(U),U)
    _or_{AC,#}(A,B) -> isBool#(A)
    _or_{AC,#}(A,B) -> U101#(isBool(A),A,B)
    _xor_{AC,#}(A,A) -> isBool#(A)
    _xor_{AC,#}(A,A) -> U111#(isBool(A),A)
    _xor_{AC,#}(false(),A) -> isBool#(A)
    _xor_{AC,#}(false(),A) -> U121#(isBool(A),A)
    if_then_else_fi#(B,U,U') -> isBool#(B)
    if_then_else_fi#(B,U,U') -> U131#(isBool(B),B,U',U)
    if_then_else_fi#(true(),U,U') -> U141#(isS(U'),U',U)
    isBool#(_and_AC(V1,V2)) -> isBoolKind#(V1)
    isBool#(_and_AC(V1,V2)) -> U151#(isBoolKind(V1),V1,V2)
    isBool#(_implies_(V1,V2)) -> isBoolKind#(V1)
    isBool#(_implies_(V1,V2)) -> U161#(isBoolKind(V1),V1,V2)
    isBool#(_or_AC(V1,V2)) -> isBoolKind#(V1)
    isBool#(_or_AC(V1,V2)) -> U171#(isBoolKind(V1),V1,V2)
    isBool#(_xor_AC(V1,V2)) -> isBoolKind#(V1)
    isBool#(_xor_AC(V1,V2)) -> U181#(isBoolKind(V1),V1,V2)
    isBool#(not_(V1)) -> isBoolKind#(V1)
    isBool#(not_(V1)) -> U191#(isBoolKind(V1),V1)
    isBoolKind#(_and_AC(V1,V2)) -> isBoolKind#(V1)
    isBoolKind#(_and_AC(V1,V2)) -> U201#(isBoolKind(V1),V2)
    isBoolKind#(_implies_(V1,V2)) -> isBoolKind#(V1)
    isBoolKind#(_implies_(V1,V2)) -> U211#(isBoolKind(V1),V2)
    isBoolKind#(_or_AC(V1,V2)) -> isBoolKind#(V1)
    isBoolKind#(_or_AC(V1,V2)) -> U221#(isBoolKind(V1),V2)
    isBoolKind#(_xor_AC(V1,V2)) -> isBoolKind#(V1)
    isBoolKind#(_xor_AC(V1,V2)) -> U231#(isBoolKind(V1),V2)
    isBoolKind#(not_(V1)) -> isBoolKind#(V1)
    isBoolKind#(not_(V1)) -> U241#(isBoolKind(V1))
    not_#(A) -> isBool#(A)
    not_#(A) -> U251#(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#(A)
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> U21#(isBool(A),A,B,C)
    _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x12,U21(isBool(A),A,B,C))
    _and_{AC,#}(x13,_and_AC(false(),A)) -> isBool#(A)
    _and_{AC,#}(x13,_and_AC(false(),A)) -> U31#(isBool(A),A)
    _and_{AC,#}(x13,_and_AC(false(),A)) -> _and_{AC,#}(x13,U31(isBool(A),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#(A)
    _or_{AC,#}(x15,_or_AC(A,B)) -> U101#(isBool(A),A,B)
    _or_{AC,#}(x15,_or_AC(A,B)) -> _or_{AC,#}(x15,U101(isBool(A),A,B))
    _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBool#(A)
    _xor_{AC,#}(x16,_xor_AC(A,A)) -> U111#(isBool(A),A)
    _xor_{AC,#}(x16,_xor_AC(A,A)) -> _xor_{AC,#}(x16,U111(isBool(A),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) -> U102(isBoolKind(A),A,B)
    U102(tt(),A,B) -> U103(isBool(B),A,B)
    U103(tt(),A,B) -> U104(isBoolKind(B),A,B)
    U104(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(A,B))
    U11(tt(),A) -> U12(isBoolKind(A),A)
    U111(tt(),A) -> U112(isBoolKind(A))
    U112(tt()) -> false()
    U12(tt(),A) -> A
    U121(tt(),A) -> U122(isBoolKind(A),A)
    U122(tt(),A) -> A
    U131(tt(),B,U',U) -> U132(isBoolKind(B),B,U',U)
    U132(tt(),B,U',U) -> U133(isS(U'),B,U',U)
    U133(tt(),B,U',U) -> U134(isSKind(U'),B,U',U)
    U134(tt(),B,U',U) -> U135(isS(U),B,U',U)
    U135(tt(),B,U',U) -> U136(isSKind(U),B,U')
    U136(tt(),B,U') -> U137(equal(_isNotEqualTo_(B,true()),true()),U')
    U137(tt(),U') -> U'
    U141(tt(),U',U) -> U142(isSKind(U'),U)
    U142(tt(),U) -> U143(isS(U),U)
    U143(tt(),U) -> U144(isSKind(U),U)
    U144(tt(),U) -> U
    U151(tt(),V1,V2) -> U152(isBoolKind(V1),V1,V2)
    U152(tt(),V1,V2) -> U153(isBoolKind(V2),V1,V2)
    U153(tt(),V1,V2) -> U154(isBoolKind(V2),V1,V2)
    U154(tt(),V1,V2) -> U155(isBool(V1),V2)
    U155(tt(),V2) -> U156(isBool(V2))
    U156(tt()) -> tt()
    U161(tt(),V1,V2) -> U162(isBoolKind(V1),V1,V2)
    U162(tt(),V1,V2) -> U163(isBoolKind(V2),V1,V2)
    U163(tt(),V1,V2) -> U164(isBoolKind(V2),V1,V2)
    U164(tt(),V1,V2) -> U165(isBool(V1),V2)
    U165(tt(),V2) -> U166(isBool(V2))
    U166(tt()) -> tt()
    U171(tt(),V1,V2) -> U172(isBoolKind(V1),V1,V2)
    U172(tt(),V1,V2) -> U173(isBoolKind(V2),V1,V2)
    U173(tt(),V1,V2) -> U174(isBoolKind(V2),V1,V2)
    U174(tt(),V1,V2) -> U175(isBool(V1),V2)
    U175(tt(),V2) -> U176(isBool(V2))
    U176(tt()) -> tt()
    U181(tt(),V1,V2) -> U182(isBoolKind(V1),V1,V2)
    U182(tt(),V1,V2) -> U183(isBoolKind(V2),V1,V2)
    U183(tt(),V1,V2) -> U184(isBoolKind(V2),V1,V2)
    U184(tt(),V1,V2) -> U185(isBool(V1),V2)
    U185(tt(),V2) -> U186(isBool(V2))
    U186(tt()) -> tt()
    U191(tt(),V1) -> U192(isBoolKind(V1),V1)
    U192(tt(),V1) -> U193(isBool(V1))
    U193(tt()) -> tt()
    U201(tt(),V2) -> U202(isBoolKind(V2))
    U202(tt()) -> tt()
    U21(tt(),A,B,C) -> U22(isBoolKind(A),A,B,C)
    U211(tt(),V2) -> U212(isBoolKind(V2))
    U212(tt()) -> tt()
    U22(tt(),A,B,C) -> U23(isBool(B),A,B,C)
    U221(tt(),V2) -> U222(isBoolKind(V2))
    U222(tt()) -> tt()
    U23(tt(),A,B,C) -> U24(isBoolKind(B),A,B,C)
    U231(tt(),V2) -> U232(isBoolKind(V2))
    U232(tt()) -> tt()
    U24(tt(),A,B,C) -> U25(isBool(C),A,B,C)
    U241(tt()) -> tt()
    U25(tt(),A,B,C) -> U26(isBoolKind(C),A,B,C)
    U251(tt(),A) -> U252(isBoolKind(A),A)
    U252(tt(),A) -> _xor_AC(A,true())
    U26(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C))
    U31(tt(),A) -> U32(isBoolKind(A))
    U32(tt()) -> false()
    U41(tt(),A) -> U42(isBoolKind(A),A)
    U42(tt(),A) -> A
    U51(tt(),A,B) -> U52(isBoolKind(A),A,B)
    U52(tt(),A,B) -> U53(isBool(B),A,B)
    U53(tt(),A,B) -> U54(isBoolKind(B),A,B)
    U54(tt(),A,B) -> not_(_xor_AC(A,_and_AC(A,B)))
    U61(tt(),U',U) -> U62(isSKind(U'),U',U)
    U62(tt(),U',U) -> U63(isS(U),U',U)
    U63(tt(),U',U) -> U64(isSKind(U),U',U)
    U64(tt(),U',U) -> U65(equal(_isNotEqualTo_(U,U'),true()))
    U65(tt()) -> false()
    U71(tt(),U) -> U72(isSKind(U))
    U72(tt()) -> true()
    U81(tt(),U',U) -> U82(isSKind(U'),U',U)
    U82(tt(),U',U) -> U83(isS(U),U',U)
    U83(tt(),U',U) -> U84(isSKind(U),U',U)
    U84(tt(),U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false(),true())
    U91(tt(),U) -> U92(isSKind(U))
    U92(tt()) -> false()
    _and_AC(A,A) -> U11(isBool(A),A)
    _and_AC(A,_xor_AC(B,C)) -> U21(isBool(A),A,B,C)
    _and_AC(false(),A) -> U31(isBool(A),A)
    _and_AC(true(),A) -> U41(isBool(A),A)
    _implies_(A,B) -> U51(isBool(A),A,B)
    _isEqualTo_(U,U') -> U61(isS(U'),U',U)
    _isEqualTo_(U,U) -> U71(isS(U),U)
    _isNotEqualTo_(U,U') -> U81(isS(U'),U',U)
    _isNotEqualTo_(U,U) -> U91(isS(U),U)
    _or_AC(A,B) -> U101(isBool(A),A,B)
    _xor_AC(A,A) -> U111(isBool(A),A)
    _xor_AC(false(),A) -> U121(isBool(A),A)
    equal(X,X) -> tt()
    if_then_else_fi(B,U,U') -> U131(isBool(B),B,U',U)
    if_then_else_fi(true(),U,U') -> U141(isS(U'),U',U)
    isBool(false()) -> tt()
    isBool(true()) -> tt()
    isBool(_and_AC(V1,V2)) -> U151(isBoolKind(V1),V1,V2)
    isBool(_implies_(V1,V2)) -> U161(isBoolKind(V1),V1,V2)
    isBool(_isEqualTo_(V1,V2)) -> tt()
    isBool(_isNotEqualTo_(V1,V2)) -> tt()
    isBool(_or_AC(V1,V2)) -> U171(isBoolKind(V1),V1,V2)
    isBool(_xor_AC(V1,V2)) -> U181(isBoolKind(V1),V1,V2)
    isBool(not_(V1)) -> U191(isBoolKind(V1),V1)
    isBoolKind(false()) -> tt()
    isBoolKind(true()) -> tt()
    isBoolKind(_and_AC(V1,V2)) -> U201(isBoolKind(V1),V2)
    isBoolKind(_implies_(V1,V2)) -> U211(isBoolKind(V1),V2)
    isBoolKind(_isEqualTo_(V1,V2)) -> tt()
    isBoolKind(_isNotEqualTo_(V1,V2)) -> tt()
    isBoolKind(_or_AC(V1,V2)) -> U221(isBoolKind(V1),V2)
    isBoolKind(_xor_AC(V1,V2)) -> U231(isBoolKind(V1),V2)
    isBoolKind(not_(V1)) -> U241(isBoolKind(V1))
    not_(A) -> U251(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