YES
Time: 0.004503
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)}
 BOUND:
  Bound: roof(-raise)-bounded by 3
  Automaton:
   {      =_0(1, 1) -> 1*
    implies_0(1, 1) -> 1*
         or_0(1, 1) -> 1*
        and_0(1, 1) -> 1*
           not_1(1) -> 1*
           true_3() -> 1*
          false_2() -> 1*
      if_2(1, 1, 1) -> 1*}
  Strict:
   {}
  Qed