YES

We show the termination of the TRS R:

  not(x) -> if(x,false(),true())
  and(x,y) -> if(x,y,false())
  or(x,y) -> if(x,true(),y)
  implies(x,y) -> if(x,y,true())
  =(x,x) -> true()
  =(x,y) -> if(x,y,not(y))
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  if(x,x,if(x,false(),true())) -> true()
  =(x,y) -> if(x,y,if(y,false(),true()))

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: not#(x) -> if#(x,false(),true())
p2: and#(x,y) -> if#(x,y,false())
p3: or#(x,y) -> if#(x,true(),y)
p4: implies#(x,y) -> if#(x,y,true())
p5: =#(x,y) -> if#(x,y,not(y))
p6: =#(x,y) -> not#(y)
p7: =#(x,y) -> if#(x,y,if(y,false(),true()))
p8: =#(x,y) -> if#(y,false(),true())

and R consists of:

r1: not(x) -> if(x,false(),true())
r2: and(x,y) -> if(x,y,false())
r3: or(x,y) -> if(x,true(),y)
r4: implies(x,y) -> if(x,y,true())
r5: =(x,x) -> true()
r6: =(x,y) -> if(x,y,not(y))
r7: if(true(),x,y) -> x
r8: if(false(),x,y) -> y
r9: if(x,x,if(x,false(),true())) -> true()
r10: =(x,y) -> if(x,y,if(y,false(),true()))

The estimated dependency graph contains the following SCCs:

  (no SCCs)