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