MAYBE
MAYBE
TRS:
 {
   cond2(true(), x, y) -> cond1(y, y),
  cond2(false(), x, y) -> cond1(p(x), y),
        gr(s(x), s(y)) -> gr(x, y),
         gr(s(x), 0()) -> true(),
            gr(0(), x) -> false(),
        cond1(s(x), y) -> cond2(gr(s(x), y), s(x), y),
               p(s(x)) -> x,
                p(0()) -> 0(),
       neq(s(x), s(y)) -> neq(x, y),
        neq(s(x), 0()) -> true(),
        neq(0(), s(x)) -> true(),
         neq(0(), 0()) -> false()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
     cond2(true(), x, y) -> cond1(y, y),
    cond2(false(), x, y) -> cond1(p(x), y),
          gr(s(x), s(y)) -> gr(x, y),
           gr(s(x), 0()) -> true(),
              gr(0(), x) -> false(),
          cond1(s(x), y) -> cond2(gr(s(x), y), s(x), y),
                 p(s(x)) -> x,
                  p(0()) -> 0(),
         neq(s(x), s(y)) -> neq(x, y),
          neq(s(x), 0()) -> true(),
          neq(0(), s(x)) -> true(),
           neq(0(), 0()) -> false()
   }
  Fail