MAYBE
Time: 5.146

Problem:
 Equations:
  
 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:
 Open