TRS:
 { cond(true(), x, y) -> cond(and(gr(x, 0()), gr(y, 0())), p(x), p(y)),
  and(true(), true()) -> true(),
      and(x, false()) -> false(),
      and(false(), x) -> false(),
         gr(0(), 0()) -> false(),
           gr(0(), x) -> false(),
        gr(s(x), 0()) -> true(),
       gr(s(x), s(y)) -> gr(x, y),
               p(0()) -> 0(),
              p(s(x)) -> x}
 Fail