Time: 5.115229
TRS:
 {         condAcc(false(), x, y) -> sqrtAcc(x, plus_int(pos s 0(), y)),
            condAcc(true(), x, y) -> y,
             or(false(), false()) -> false(),
              or(false(), true()) -> true(),
              or(true(), false()) -> true(),
               or(true(), true()) -> true(),
    greatereq_int(pos x, pos 0()) -> true(),
      greatereq_int(pos x, neg y) -> true(),
  greatereq_int(pos 0(), pos s y) -> false(),
  greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
    greatereq_int(neg x, pos s y) -> false(),
  greatereq_int(neg 0(), pos 0()) -> true(),
    greatereq_int(neg 0(), neg y) -> true(),
  greatereq_int(neg s x, pos 0()) -> false(),
  greatereq_int(neg s x, neg 0()) -> false(),
  greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg 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),
       less_int(pos 0(), pos 0()) -> false(),
       less_int(pos 0(), pos s y) -> true(),
       less_int(pos 0(), neg 0()) -> false(),
       less_int(pos 0(), neg s y) -> false(),
       less_int(pos s x, pos 0()) -> false(),
       less_int(pos s x, pos s y) -> less_int(pos x, pos y),
       less_int(pos s x, neg 0()) -> false(),
       less_int(pos s x, neg s y) -> false(),
       less_int(neg 0(), pos 0()) -> false(),
       less_int(neg 0(), pos s y) -> true(),
       less_int(neg 0(), neg 0()) -> false(),
       less_int(neg 0(), neg s y) -> false(),
       less_int(neg s x, pos 0()) -> true(),
       less_int(neg s x, pos s y) -> true(),
       less_int(neg s x, neg 0()) -> true(),
       less_int(neg s x, neg s y) -> less_int(neg x, neg y),
                    sqrtAcc(x, y) -> condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos 0())), x, y),
           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),
                           sqrt x -> sqrtAcc(x, pos 0()),
                 mult_nat(0(), y) -> 0(),
               mult_nat(s x, 0()) -> 0(),
               mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                 plus_nat(0(), x) -> x,
                 plus_nat(s x, y) -> s plus_nat(x, y),
              minus_nat(0(), 0()) -> pos 0(),
              minus_nat(0(), s y) -> neg s y,
              minus_nat(s x, 0()) -> pos s x,
              minus_nat(s x, s y) -> minus_nat(x, y)}
 SRS: We consider a TRS.
  Trs:
   {         condAcc(false(), x, y) -> sqrtAcc(x, plus_int(pos s 0(), y)),
              condAcc(true(), x, y) -> y,
               or(false(), false()) -> false(),
                or(false(), true()) -> true(),
                or(true(), false()) -> true(),
                 or(true(), true()) -> true(),
      greatereq_int(pos x, pos 0()) -> true(),
        greatereq_int(pos x, neg y) -> true(),
    greatereq_int(pos 0(), pos s y) -> false(),
    greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
      greatereq_int(neg x, pos s y) -> false(),
    greatereq_int(neg 0(), pos 0()) -> true(),
      greatereq_int(neg 0(), neg y) -> true(),
    greatereq_int(neg s x, pos 0()) -> false(),
    greatereq_int(neg s x, neg 0()) -> false(),
    greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg 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),
         less_int(pos 0(), pos 0()) -> false(),
         less_int(pos 0(), pos s y) -> true(),
         less_int(pos 0(), neg 0()) -> false(),
         less_int(pos 0(), neg s y) -> false(),
         less_int(pos s x, pos 0()) -> false(),
         less_int(pos s x, pos s y) -> less_int(pos x, pos y),
         less_int(pos s x, neg 0()) -> false(),
         less_int(pos s x, neg s y) -> false(),
         less_int(neg 0(), pos 0()) -> false(),
         less_int(neg 0(), pos s y) -> true(),
         less_int(neg 0(), neg 0()) -> false(),
         less_int(neg 0(), neg s y) -> false(),
         less_int(neg s x, pos 0()) -> true(),
         less_int(neg s x, pos s y) -> true(),
         less_int(neg s x, neg 0()) -> true(),
         less_int(neg s x, neg s y) -> less_int(neg x, neg y),
                      sqrtAcc(x, y) -> condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos 0())), x, y),
             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),
                             sqrt x -> sqrtAcc(x, pos 0()),
                   mult_nat(0(), y) -> 0(),
                 mult_nat(s x, 0()) -> 0(),
                 mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                   plus_nat(0(), x) -> x,
                   plus_nat(s x, y) -> s plus_nat(x, y),
                minus_nat(0(), 0()) -> pos 0(),
                minus_nat(0(), s y) -> neg s y,
                minus_nat(s x, 0()) -> pos s x,
                minus_nat(s x, s y) -> minus_nat(x, y)}
  Fail