YES
Time: 0.001666
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)}
  UR:
   {if(false(), x, y) -> y,
     if(true(), x, y) -> x,
                not x -> if(x, false(), true()),
              a(z, w) -> z,
              a(z, w) -> w}
   EDG:
    {(=#(x, y) -> not# y, not# x -> if#(x, false(), true()))}
    EDG:
     {(=#(x, y) -> not# y, not# x -> if#(x, false(), true()))}
     EDG:
      {(=#(x, y) -> not# y, not# x -> if#(x, false(), true()))}
      EDG:
       {(=#(x, y) -> not# y, not# x -> if#(x, false(), true()))}
       STATUS:
        arrows: 0.984375
        SCCS (0):