Time: 5.211807
TRS:
 {                            f x -> cond1(greater_int(x, pos s 0()), x),
                cond1(false(), x) -> x,
                 cond1(true(), x) -> cond2(equal_int(mod_int(x, pos s s 0()), pos 0()), x),
           plus_int(pos x, pos y) -> pos plus_nat(x, y),
           plus_int(pos x, neg y) -> minus_nat(x, y),
           plus_int(neg x, pos y) -> minus_nat(y, x),
           plus_int(neg x, neg y) -> neg plus_nat(x, y),
           mult_int(pos x, pos y) -> pos mult_nat(x, y),
           mult_int(pos x, neg y) -> neg mult_nat(x, y),
           mult_int(neg x, pos y) -> neg mult_nat(x, y),
           mult_int(neg x, neg y) -> pos mult_nat(x, y),
                cond2(false(), x) -> f plus_int(pos s 0(), mult_int(pos s s s 0(), x)),
                 cond2(true(), x) -> f div_int(x, pos s s 0()),
    greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
    greater_int(pos s x, pos 0()) -> true(),
    greater_int(pos s x, neg s y) -> true(),
    greater_int(pos s x, neg 0()) -> true(),
    greater_int(pos 0(), pos s y) -> false(),
    greater_int(pos 0(), pos 0()) -> false(),
    greater_int(pos 0(), neg s y) -> true(),
    greater_int(pos 0(), neg 0()) -> false(),
    greater_int(neg s x, pos s y) -> false(),
    greater_int(neg s x, pos 0()) -> false(),
    greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
    greater_int(neg s x, neg 0()) -> false(),
    greater_int(neg 0(), pos s y) -> false(),
    greater_int(neg 0(), pos 0()) -> false(),
    greater_int(neg 0(), neg s y) -> true(),
    greater_int(neg 0(), neg 0()) -> false(),
      equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
      equal_int(pos s x, pos 0()) -> false(),
      equal_int(pos s x, neg s y) -> false(),
      equal_int(pos s x, neg 0()) -> false(),
      equal_int(pos 0(), pos s y) -> false(),
      equal_int(pos 0(), pos 0()) -> true(),
      equal_int(pos 0(), neg s y) -> false(),
      equal_int(pos 0(), neg 0()) -> true(),
      equal_int(neg s x, pos s y) -> false(),
      equal_int(neg s x, pos 0()) -> false(),
      equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
      equal_int(neg s x, neg 0()) -> false(),
      equal_int(neg 0(), pos s y) -> false(),
      equal_int(neg 0(), pos 0()) -> true(),
      equal_int(neg 0(), neg s y) -> false(),
      equal_int(neg 0(), neg 0()) -> true(),
            mod_int(pos x, pos y) -> pos mod_nat(x, y),
            mod_int(pos x, neg y) -> pos mod_nat(x, y),
            mod_int(neg x, pos y) -> neg mod_nat(x, y),
            mod_int(neg x, neg y) -> neg mod_nat(x, y),
          div_int(pos x, pos s y) -> pos div_nat(x, s y),
          div_int(pos x, neg s y) -> neg div_nat(x, s y),
          div_int(neg x, pos s y) -> neg div_nat(x, s y),
          div_int(neg x, neg s y) -> pos div_nat(x, s y),
              minus_nat(s x, s y) -> minus_nat(x, y),
              minus_nat(s x, 0()) -> pos s x,
              minus_nat(0(), s y) -> neg s y,
              minus_nat(0(), 0()) -> pos 0(),
                 plus_nat(s x, y) -> s plus_nat(x, y),
                 plus_nat(0(), x) -> x,
               mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
               mult_nat(s x, 0()) -> 0(),
                 mult_nat(0(), y) -> 0(),
                mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                mod_nat(0(), s x) -> 0(),
                if(false(), x, y) -> y,
                 if(true(), x, y) -> x,
    greatereq_int(pos x, pos 0()) -> true(),
      greatereq_int(pos x, neg y) -> true(),
  greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
  greatereq_int(pos 0(), pos s y) -> false(),
    greatereq_int(neg x, pos s y) -> false(),
  greatereq_int(neg s x, pos 0()) -> false(),
  greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
  greatereq_int(neg s x, neg 0()) -> false(),
  greatereq_int(neg 0(), pos 0()) -> true(),
    greatereq_int(neg 0(), neg y) -> true(),
              minus_nat_s(x, 0()) -> x,
            minus_nat_s(s x, s y) -> minus_nat_s(x, y),
            minus_nat_s(0(), s y) -> 0(),
                div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                div_nat(0(), s y) -> 0()}
 SRS: We consider a TRS.
  Trs:
   {                            f x -> cond1(greater_int(x, pos s 0()), x),
                  cond1(false(), x) -> x,
                   cond1(true(), x) -> cond2(equal_int(mod_int(x, pos s s 0()), pos 0()), x),
             plus_int(pos x, pos y) -> pos plus_nat(x, y),
             plus_int(pos x, neg y) -> minus_nat(x, y),
             plus_int(neg x, pos y) -> minus_nat(y, x),
             plus_int(neg x, neg y) -> neg plus_nat(x, y),
             mult_int(pos x, pos y) -> pos mult_nat(x, y),
             mult_int(pos x, neg y) -> neg mult_nat(x, y),
             mult_int(neg x, pos y) -> neg mult_nat(x, y),
             mult_int(neg x, neg y) -> pos mult_nat(x, y),
                  cond2(false(), x) -> f plus_int(pos s 0(), mult_int(pos s s s 0(), x)),
                   cond2(true(), x) -> f div_int(x, pos s s 0()),
      greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
      greater_int(pos s x, pos 0()) -> true(),
      greater_int(pos s x, neg s y) -> true(),
      greater_int(pos s x, neg 0()) -> true(),
      greater_int(pos 0(), pos s y) -> false(),
      greater_int(pos 0(), pos 0()) -> false(),
      greater_int(pos 0(), neg s y) -> true(),
      greater_int(pos 0(), neg 0()) -> false(),
      greater_int(neg s x, pos s y) -> false(),
      greater_int(neg s x, pos 0()) -> false(),
      greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
      greater_int(neg s x, neg 0()) -> false(),
      greater_int(neg 0(), pos s y) -> false(),
      greater_int(neg 0(), pos 0()) -> false(),
      greater_int(neg 0(), neg s y) -> true(),
      greater_int(neg 0(), neg 0()) -> false(),
        equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
        equal_int(pos s x, pos 0()) -> false(),
        equal_int(pos s x, neg s y) -> false(),
        equal_int(pos s x, neg 0()) -> false(),
        equal_int(pos 0(), pos s y) -> false(),
        equal_int(pos 0(), pos 0()) -> true(),
        equal_int(pos 0(), neg s y) -> false(),
        equal_int(pos 0(), neg 0()) -> true(),
        equal_int(neg s x, pos s y) -> false(),
        equal_int(neg s x, pos 0()) -> false(),
        equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
        equal_int(neg s x, neg 0()) -> false(),
        equal_int(neg 0(), pos s y) -> false(),
        equal_int(neg 0(), pos 0()) -> true(),
        equal_int(neg 0(), neg s y) -> false(),
        equal_int(neg 0(), neg 0()) -> true(),
              mod_int(pos x, pos y) -> pos mod_nat(x, y),
              mod_int(pos x, neg y) -> pos mod_nat(x, y),
              mod_int(neg x, pos y) -> neg mod_nat(x, y),
              mod_int(neg x, neg y) -> neg mod_nat(x, y),
            div_int(pos x, pos s y) -> pos div_nat(x, s y),
            div_int(pos x, neg s y) -> neg div_nat(x, s y),
            div_int(neg x, pos s y) -> neg div_nat(x, s y),
            div_int(neg x, neg s y) -> pos div_nat(x, s y),
                minus_nat(s x, s y) -> minus_nat(x, y),
                minus_nat(s x, 0()) -> pos s x,
                minus_nat(0(), s y) -> neg s y,
                minus_nat(0(), 0()) -> pos 0(),
                   plus_nat(s x, y) -> s plus_nat(x, y),
                   plus_nat(0(), x) -> x,
                 mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                 mult_nat(s x, 0()) -> 0(),
                   mult_nat(0(), y) -> 0(),
                  mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                  mod_nat(0(), s x) -> 0(),
                  if(false(), x, y) -> y,
                   if(true(), x, y) -> x,
      greatereq_int(pos x, pos 0()) -> true(),
        greatereq_int(pos x, neg y) -> true(),
    greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
    greatereq_int(pos 0(), pos s y) -> false(),
      greatereq_int(neg x, pos s y) -> false(),
    greatereq_int(neg s x, pos 0()) -> false(),
    greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
    greatereq_int(neg s x, neg 0()) -> false(),
    greatereq_int(neg 0(), pos 0()) -> true(),
      greatereq_int(neg 0(), neg y) -> true(),
                minus_nat_s(x, 0()) -> x,
              minus_nat_s(s x, s y) -> minus_nat_s(x, y),
              minus_nat_s(0(), s y) -> 0(),
                  div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                  div_nat(0(), s y) -> 0()}
  Fail