Time: 5.045585
TRS:
 {                      f(x, y) -> if1(greater_int(x, y), x, y),
                        h(x, y) -> if2(greater_int(x, y), x, y),
              if1(true(), x, y) -> h(x, y),
             if1(false(), x, y) -> pos 0(),
              if2(true(), x, y) -> pos 0(),
             if2(false(), x, y) -> f(x, y),
  greater_int(pos 0(), pos 0()) -> false(),
  greater_int(pos 0(), pos s y) -> false(),
  greater_int(pos 0(), neg 0()) -> false(),
  greater_int(pos 0(), neg s y) -> true(),
  greater_int(pos s x, pos 0()) -> true(),
  greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
  greater_int(pos s x, neg 0()) -> true(),
  greater_int(pos s x, neg s y) -> true(),
  greater_int(neg 0(), pos 0()) -> false(),
  greater_int(neg 0(), pos s y) -> false(),
  greater_int(neg 0(), neg 0()) -> false(),
  greater_int(neg 0(), neg s y) -> true(),
  greater_int(neg s x, pos 0()) -> false(),
  greater_int(neg s x, pos s y) -> false(),
  greater_int(neg s x, neg 0()) -> false(),
  greater_int(neg s x, neg s y) -> greater_int(neg x, neg y)}
 SRS: We consider a TRS.
  Trs:
   {                      f(x, y) -> if1(greater_int(x, y), x, y),
                          h(x, y) -> if2(greater_int(x, y), x, y),
                if1(true(), x, y) -> h(x, y),
               if1(false(), x, y) -> pos 0(),
                if2(true(), x, y) -> pos 0(),
               if2(false(), x, y) -> f(x, y),
    greater_int(pos 0(), pos 0()) -> false(),
    greater_int(pos 0(), pos s y) -> false(),
    greater_int(pos 0(), neg 0()) -> false(),
    greater_int(pos 0(), neg s y) -> true(),
    greater_int(pos s x, pos 0()) -> true(),
    greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
    greater_int(pos s x, neg 0()) -> true(),
    greater_int(pos s x, neg s y) -> true(),
    greater_int(neg 0(), pos 0()) -> false(),
    greater_int(neg 0(), pos s y) -> false(),
    greater_int(neg 0(), neg 0()) -> false(),
    greater_int(neg 0(), neg s y) -> true(),
    greater_int(neg s x, pos 0()) -> false(),
    greater_int(neg s x, pos s y) -> false(),
    greater_int(neg s x, neg 0()) -> false(),
    greater_int(neg s x, neg s y) -> greater_int(neg x, neg y)}
  Fail