MAYBE
Time: 0.038

Problem:
 Equations:
  _xor_AC(_xor_AC(x10,x11),x12) -> _xor_AC(x10,_xor_AC(x11,x12))
  _xor_AC(x10,x11) -> _xor_AC(x11,x10)
  _and_AC(_and_AC(x10,x11),x12) -> _and_AC(x10,_and_AC(x11,x12))
  _and_AC(x10,x11) -> _and_AC(x11,x10)
  _or_AC(_or_AC(x10,x11),x12) -> _or_AC(x10,_or_AC(x11,x12))
  _or_AC(x10,x11) -> _or_AC(x11,x10)
  _xor_AC(x10,_xor_AC(x11,x12)) -> _xor_AC(_xor_AC(x10,x11),x12)
  _xor_AC(x11,x10) -> _xor_AC(x10,x11)
  _and_AC(x10,_and_AC(x11,x12)) -> _and_AC(_and_AC(x10,x11),x12)
  _and_AC(x11,x10) -> _and_AC(x10,x11)
  _or_AC(x10,_or_AC(x11,x12)) -> _or_AC(_or_AC(x10,x11),x12)
  _or_AC(x11,x10) -> _or_AC(x10,x11)
 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(),V1,V2) -> U152(isBool(V1),V2)
  U152(tt(),V2) -> U153(isBool(V2))
  U153(tt()) -> tt()
  U161(tt(),V1,V2) -> U162(isBool(V1),V2)
  U162(tt(),V2) -> U163(isBool(V2))
  U163(tt()) -> tt()
  U171(tt(),V1,V2) -> U172(isBool(V1),V2)
  U172(tt(),V2) -> U173(isBool(V2))
  U173(tt()) -> tt()
  U181(tt(),V1,V2) -> U182(isBool(V1),V2)
  U182(tt(),V2) -> U183(isBool(V2))
  U183(tt()) -> tt()
  U191(tt(),V1) -> U192(isBool(V1))
  U192(tt()) -> tt()
  U201(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(and(isBool(A),isBoolKind(A)),A)
  _and_AC(A,_xor_AC(B,C)) ->
  U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)),
                                           and(isBool(C),isBoolKind(C)))),
      A,B,C)
  _and_AC(false(),A) -> U31(and(isBool(A),isBoolKind(A)))
  _and_AC(true(),A) -> U41(and(isBool(A),isBoolKind(A)),A)
  _implies_(A,B) -> U51(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B)
  _isEqualTo_(U,U') -> U61(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U)
  _isEqualTo_(U,U) -> U71(and(isS(U),isSKind(U)))
  _isNotEqualTo_(U,U') -> U81(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U)
  _isNotEqualTo_(U,U) -> U91(and(isS(U),isSKind(U)))
  _or_AC(A,B) -> U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B)
  _xor_AC(A,A) -> U111(and(isBool(A),isBoolKind(A)))
  _xor_AC(false(),A) -> U121(and(isBool(A),isBoolKind(A)),A)
  and(tt(),X) -> X
  equal(X,X) -> tt()
  if_then_else_fi(B,U,U') ->
  U131(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))),B,U')
  if_then_else_fi(true(),U,U') -> U141(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U)
  isBool(false()) -> tt()
  isBool(true()) -> tt()
  isBool(_and_AC(V1,V2)) -> U151(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)
  isBool(_implies_(V1,V2)) -> U161(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)
  isBool(_isEqualTo_(V1,V2)) -> tt()
  isBool(_isNotEqualTo_(V1,V2)) -> tt()
  isBool(_or_AC(V1,V2)) -> U171(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)
  isBool(_xor_AC(V1,V2)) -> U181(and(isBoolKind(V1),isBoolKind(V2)),V1,V2)
  isBool(not_(V1)) -> U191(isBoolKind(V1),V1)
  isBoolKind(false()) -> tt()
  isBoolKind(true()) -> tt()
  isBoolKind(_and_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))
  isBoolKind(_implies_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))
  isBoolKind(_isEqualTo_(V1,V2)) -> tt()
  isBoolKind(_isNotEqualTo_(V1,V2)) -> tt()
  isBoolKind(_or_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))
  isBoolKind(_xor_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2))
  isBoolKind(not_(V1)) -> isBoolKind(V1)
  not_(A) -> U201(and(isBool(A),isBoolKind(A)),A)
  not_(false()) -> true()
  not_(true()) -> false()

Proof:
 Open