Time: 5.142695
TRS:
 {       Cond_isdiv(true(), x, y) -> isdiv(neg_int x, 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),
                      isdiv(x, y) -> Cond_isdiv(greater_int(pos 0(), x), x, y),
                      isdiv(x, y) -> Cond_isdiv3(greater_int(pos 0(), y), x, y),
                      isdiv(x, y) -> Cond_isdiv1(and(greater_int(x, y), greater_int(y, pos 0())), x, y),
                      isdiv(x, y) -> Cond_isdiv4(and(greatereq_int(y, x), greater_int(x, pos 0())), x, y),
                isdiv(x, pos 0()) -> Cond_isdiv2(greater_int(x, pos 0()), x),
          if_2(false(), x, y, zs) -> cons(x, filter(x, zs)),
                 filter(x, nil()) -> nil(),
           filter(x, cons(y, zs)) -> if_2(isdiv(x, y), x, y, zs),
           filter(x, cons(y, zs)) -> if_1(isdiv(x, y), x, y, zs),
      Cond_mem1(true(), x, y, zs) -> true(),
       Cond_mem(true(), x, y, zs) -> mem(x, zs),
                    mem(x, nil()) -> false(),
              mem(x, cons(y, zs)) -> Cond_mem1(equal_int(x, y), x, y, zs),
              mem(x, cons(y, zs)) -> Cond_mem(greater_int(y, x), x, y, zs),
              mem(x, cons(y, zs)) -> Cond_mem2(greater_int(x, y), x, y, zs),
           if_1(true(), x, y, zs) -> filter(x, zs),
                    neg_int pos x -> neg x,
                    neg_int neg x -> pos x,
        Cond_isdiv3(true(), x, y) -> isdiv(x, neg_int y),
        Cond_isdiv1(true(), x, y) -> false(),
           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),
        Cond_isdiv4(true(), x, y) -> isdiv(x, plus_int(neg_int x, y)),
         Cond_nats2(true(), x, y) -> cons(x, nil()),
      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),
                       nats(x, y) -> Cond_nats2(equal_int(x, y), x, y),
                       nats(x, y) -> Cond_nats1(greater_int(x, y), x, y),
                       nats(x, y) -> Cond_nats(greater_int(y, x), x, y),
                      sieve nil() -> nil(),
                sieve cons(x, ys) -> cons(x, sieve filter(x, ys)),
                         primes x -> sieve nats(pos s s 0(), x),
                        isprime x -> mem(x, primes x),
         Cond_nats1(true(), x, y) -> nil(),
          Cond_nats(true(), x, y) -> cons(x, nats(plus_int(pos s 0(), x), y)),
      Cond_mem2(true(), x, y, zs) -> mem(x, zs),
              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 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),
           Cond_isdiv2(true(), x) -> true(),
              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_isdiv(true(), x, y) -> isdiv(neg_int x, 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),
                        isdiv(x, y) -> Cond_isdiv(greater_int(pos 0(), x), x, y),
                        isdiv(x, y) -> Cond_isdiv3(greater_int(pos 0(), y), x, y),
                        isdiv(x, y) -> Cond_isdiv1(and(greater_int(x, y), greater_int(y, pos 0())), x, y),
                        isdiv(x, y) -> Cond_isdiv4(and(greatereq_int(y, x), greater_int(x, pos 0())), x, y),
                  isdiv(x, pos 0()) -> Cond_isdiv2(greater_int(x, pos 0()), x),
            if_2(false(), x, y, zs) -> cons(x, filter(x, zs)),
                   filter(x, nil()) -> nil(),
             filter(x, cons(y, zs)) -> if_2(isdiv(x, y), x, y, zs),
             filter(x, cons(y, zs)) -> if_1(isdiv(x, y), x, y, zs),
        Cond_mem1(true(), x, y, zs) -> true(),
         Cond_mem(true(), x, y, zs) -> mem(x, zs),
                      mem(x, nil()) -> false(),
                mem(x, cons(y, zs)) -> Cond_mem1(equal_int(x, y), x, y, zs),
                mem(x, cons(y, zs)) -> Cond_mem(greater_int(y, x), x, y, zs),
                mem(x, cons(y, zs)) -> Cond_mem2(greater_int(x, y), x, y, zs),
             if_1(true(), x, y, zs) -> filter(x, zs),
                      neg_int pos x -> neg x,
                      neg_int neg x -> pos x,
          Cond_isdiv3(true(), x, y) -> isdiv(x, neg_int y),
          Cond_isdiv1(true(), x, y) -> false(),
             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),
          Cond_isdiv4(true(), x, y) -> isdiv(x, plus_int(neg_int x, y)),
           Cond_nats2(true(), x, y) -> cons(x, nil()),
        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),
                         nats(x, y) -> Cond_nats2(equal_int(x, y), x, y),
                         nats(x, y) -> Cond_nats1(greater_int(x, y), x, y),
                         nats(x, y) -> Cond_nats(greater_int(y, x), x, y),
                        sieve nil() -> nil(),
                  sieve cons(x, ys) -> cons(x, sieve filter(x, ys)),
                           primes x -> sieve nats(pos s s 0(), x),
                          isprime x -> mem(x, primes x),
           Cond_nats1(true(), x, y) -> nil(),
            Cond_nats(true(), x, y) -> cons(x, nats(plus_int(pos s 0(), x), y)),
        Cond_mem2(true(), x, y, zs) -> mem(x, zs),
                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 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),
             Cond_isdiv2(true(), x) -> true(),
                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