Time: 5.131908
TRS:
 {                       f x -> Cond_f(less_int(mult_int(x, x), pos 0()), x),
           Cond_f(true(), x) -> f x,
  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),
      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),
            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)}
 SRS: We consider a TRS.
  Trs:
   {                       f x -> Cond_f(less_int(mult_int(x, x), pos 0()), x),
             Cond_f(true(), x) -> f x,
    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),
        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),
              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)}
  Fail