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