Time: 5.155162
TRS:
 {                   f(true(), x) -> f(greatereq_int(ack(pos s s s s s s s s s s 0(), pos s s s s s s s s s s 0()), x), plus_int(pos s 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),
              cond1(true(), x, y) -> plus_int(pos s 0(), y),
             cond1(false(), x, y) -> cond2(equal_int(y, pos 0()), x, y),
             ackNat(true(), x, y) -> cond1(equal_int(x, pos 0()), x, y),
            ackNat(false(), x, y) -> pos 0(),
              and(true(), true()) -> true(),
             and(true(), false()) -> false(),
             and(false(), true()) -> false(),
            and(false(), false()) -> false(),
    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(),
                        ack(x, y) -> ackNat(and(greatereq_int(x, pos 0()), greatereq_int(y, pos 0())), x, y),
          minus_int(pos x, pos y) -> minus_nat(x, y),
          minus_int(pos x, neg y) -> pos plus_nat(x, y),
          minus_int(neg x, pos y) -> neg plus_nat(x, y),
          minus_int(neg x, neg y) -> minus_nat(y, x),
              cond2(true(), x, y) -> ack(minus_int(x, pos s 0()), plus_int(pos s 0(), y)),
             cond2(false(), x, y) -> ack(minus_int(x, pos s 0()), ack(x, minus_int(y, pos s 0()))),
      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(),
              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}
 SRS: We consider a TRS.
  Trs:
   {                   f(true(), x) -> f(greatereq_int(ack(pos s s s s s s s s s s 0(), pos s s s s s s s s s s 0()), x), plus_int(pos s 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),
                cond1(true(), x, y) -> plus_int(pos s 0(), y),
               cond1(false(), x, y) -> cond2(equal_int(y, pos 0()), x, y),
               ackNat(true(), x, y) -> cond1(equal_int(x, pos 0()), x, y),
              ackNat(false(), x, y) -> pos 0(),
                and(true(), true()) -> true(),
               and(true(), false()) -> false(),
               and(false(), true()) -> false(),
              and(false(), false()) -> false(),
      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(),
                          ack(x, y) -> ackNat(and(greatereq_int(x, pos 0()), greatereq_int(y, pos 0())), x, y),
            minus_int(pos x, pos y) -> minus_nat(x, y),
            minus_int(pos x, neg y) -> pos plus_nat(x, y),
            minus_int(neg x, pos y) -> neg plus_nat(x, y),
            minus_int(neg x, neg y) -> minus_nat(y, x),
                cond2(true(), x, y) -> ack(minus_int(x, pos s 0()), plus_int(pos s 0(), y)),
               cond2(false(), x, y) -> ack(minus_int(x, pos s 0()), ack(x, minus_int(y, pos s 0()))),
        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(),
                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}
  Fail