YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

  (no rules)

and R consists of:

r1: not(x) -> xor(x,true())
r2: implies(x,y) -> xor(and(x,y),xor(x,true()))
r3: or(x,y) -> xor(and(x,y),xor(x,y))
r4: =(x,y) -> xor(x,xor(y,true()))

The estimated dependency graph contains the following SCCs:

  (no SCCs)