MAYBE
MAYBE
TRS:
 {
  f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, y, s(z)),
  f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, s(y), z),
      and(x, true()) -> x,
     and(x, false()) -> false(),
      gt(s(u), s(v)) -> gt(u, v),
       gt(s(u), 0()) -> true(),
          gt(0(), v) -> false()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
    f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, y, s(z)),
    f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, s(y), z),
        and(x, true()) -> x,
       and(x, false()) -> false(),
        gt(s(u), s(v)) -> gt(u, v),
         gt(s(u), 0()) -> true(),
            gt(0(), v) -> false()
   }
  Fail