Time: 5.241131
TRS:
 {     Cond_rand2(true(), x, y) -> y,
                     rand(x, y) -> Cond_rand2(equal_int(x, pos 0()), x, y),
                     rand(x, y) -> Cond_rand(greater_int(x, pos 0()), x, y),
                     rand(x, y) -> Cond_rand1(greater_int(pos 0(), x), x, y),
                       random x -> rand(x, pos 0()),
        Cond_rand(true(), x, y) -> rand(plus_int(pos s 0(), neg_int x), id_inc 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),
       Cond_rand1(true(), x, y) -> rand(minus_int(neg_int x, pos s 0()), id_dec 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),
                  neg_int pos x -> neg x,
                  neg_int neg x -> pos x,
                       id_inc x -> x,
                       id_inc x -> plus_int(pos s 0(), x),
                       id_dec x -> x,
                       id_dec x -> minus_int(x, pos s 0()),
        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),
    equal_int(pos 0(), pos 0()) -> true(),
    equal_int(pos 0(), pos s y) -> false(),
    equal_int(pos 0(), neg 0()) -> true(),
    equal_int(pos 0(), neg s y) -> false(),
    equal_int(pos s x, pos 0()) -> false(),
    equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
    equal_int(pos s x, neg 0()) -> false(),
    equal_int(pos s x, neg s y) -> false(),
    equal_int(neg 0(), pos 0()) -> true(),
    equal_int(neg 0(), pos s y) -> false(),
    equal_int(neg 0(), neg 0()) -> true(),
    equal_int(neg 0(), neg s y) -> false(),
    equal_int(neg s x, pos 0()) -> false(),
    equal_int(neg s x, pos s y) -> false(),
    equal_int(neg s x, neg 0()) -> false(),
    equal_int(neg s x, neg s y) -> equal_int(neg x, neg 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),
               plus_nat(0(), x) -> x,
               plus_nat(s x, y) -> s plus_nat(x, y)}
 SRS: We consider a TRS.
  Trs:
   {     Cond_rand2(true(), x, y) -> y,
                       rand(x, y) -> Cond_rand2(equal_int(x, pos 0()), x, y),
                       rand(x, y) -> Cond_rand(greater_int(x, pos 0()), x, y),
                       rand(x, y) -> Cond_rand1(greater_int(pos 0(), x), x, y),
                         random x -> rand(x, pos 0()),
          Cond_rand(true(), x, y) -> rand(plus_int(pos s 0(), neg_int x), id_inc 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),
         Cond_rand1(true(), x, y) -> rand(minus_int(neg_int x, pos s 0()), id_dec 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),
                    neg_int pos x -> neg x,
                    neg_int neg x -> pos x,
                         id_inc x -> x,
                         id_inc x -> plus_int(pos s 0(), x),
                         id_dec x -> x,
                         id_dec x -> minus_int(x, pos s 0()),
          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),
      equal_int(pos 0(), pos 0()) -> true(),
      equal_int(pos 0(), pos s y) -> false(),
      equal_int(pos 0(), neg 0()) -> true(),
      equal_int(pos 0(), neg s y) -> false(),
      equal_int(pos s x, pos 0()) -> false(),
      equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
      equal_int(pos s x, neg 0()) -> false(),
      equal_int(pos s x, neg s y) -> false(),
      equal_int(neg 0(), pos 0()) -> true(),
      equal_int(neg 0(), pos s y) -> false(),
      equal_int(neg 0(), neg 0()) -> true(),
      equal_int(neg 0(), neg s y) -> false(),
      equal_int(neg s x, pos 0()) -> false(),
      equal_int(neg s x, pos s y) -> false(),
      equal_int(neg s x, neg 0()) -> false(),
      equal_int(neg s x, neg s y) -> equal_int(neg x, neg 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),
                 plus_nat(0(), x) -> x,
                 plus_nat(s x, y) -> s plus_nat(x, y)}
  Fail