YES
TRS:
 {if(x, x, if(x, false(), true())) -> true(),
                 if(false(), x, y) -> y,
                  if(true(), x, y) -> x,
                            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, if(y, false(), true())),
                           =(x, y) -> if(x, y, not(y))}
 DP:
  Strict:
   {       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, y) -> if#(x, y, if(y, false(), true())),
          =#(x, y) -> if#(x, y, not(y)),
          =#(x, y) -> if#(y, false(), true()),
          =#(x, y) -> not#(y)}
  Weak:
  {if(x, x, if(x, false(), true())) -> true(),
                  if(false(), x, y) -> y,
                   if(true(), x, y) -> x,
                             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, if(y, false(), true())),
                            =(x, y) -> if(x, y, not(y))}
  EDG:
   {(=#(x, y) -> not#(y), not#(x) -> if#(x, false(), true()))}
   SCCS:
    
    Qed