Time: 5.147286 TRS: { f(x, y) -> Cond_f(greater_int(x, y), x, y), Cond_f(true(), x, y) -> f(plus_int(pos s 0(), x), plus_int(pos s s 0(), y)), greater_int(pos s x, pos s y) -> greater_int(pos x, pos y), greater_int(pos s x, pos 0()) -> true(), greater_int(pos s x, neg s y) -> true(), greater_int(pos s x, neg 0()) -> true(), greater_int(pos 0(), pos s y) -> false(), greater_int(pos 0(), pos 0()) -> false(), greater_int(pos 0(), neg s y) -> true(), greater_int(pos 0(), neg 0()) -> false(), greater_int(neg s x, pos s y) -> false(), greater_int(neg s x, pos 0()) -> false(), greater_int(neg s x, neg s y) -> greater_int(neg x, neg y), greater_int(neg s x, neg 0()) -> false(), greater_int(neg 0(), pos s y) -> false(), greater_int(neg 0(), pos 0()) -> false(), greater_int(neg 0(), neg s y) -> true(), greater_int(neg 0(), neg 0()) -> 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), minus_nat(s x, s y) -> minus_nat(x, y), minus_nat(s x, 0()) -> pos s x, minus_nat(0(), s y) -> neg s y, minus_nat(0(), 0()) -> pos 0(), plus_nat(s x, y) -> s plus_nat(x, y), plus_nat(0(), x) -> x} SRS: We consider a TRS. Trs: { f(x, y) -> Cond_f(greater_int(x, y), x, y), Cond_f(true(), x, y) -> f(plus_int(pos s 0(), x), plus_int(pos s s 0(), y)), greater_int(pos s x, pos s y) -> greater_int(pos x, pos y), greater_int(pos s x, pos 0()) -> true(), greater_int(pos s x, neg s y) -> true(), greater_int(pos s x, neg 0()) -> true(), greater_int(pos 0(), pos s y) -> false(), greater_int(pos 0(), pos 0()) -> false(), greater_int(pos 0(), neg s y) -> true(), greater_int(pos 0(), neg 0()) -> false(), greater_int(neg s x, pos s y) -> false(), greater_int(neg s x, pos 0()) -> false(), greater_int(neg s x, neg s y) -> greater_int(neg x, neg y), greater_int(neg s x, neg 0()) -> false(), greater_int(neg 0(), pos s y) -> false(), greater_int(neg 0(), pos 0()) -> false(), greater_int(neg 0(), neg s y) -> true(), greater_int(neg 0(), neg 0()) -> 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), minus_nat(s x, s y) -> minus_nat(x, y), minus_nat(s x, 0()) -> pos s x, minus_nat(0(), s y) -> neg s y, minus_nat(0(), 0()) -> pos 0(), plus_nat(s x, y) -> s plus_nat(x, y), plus_nat(0(), x) -> x} Fail