MAYBE
Time: 0.433

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