MAYBE Time: 1.550926 TRS: {not false() -> true(), not true() -> false(), odd 0() -> false(), odd s x -> not odd x, +(x, 0()) -> x, +(x, s y) -> s +(x, y), +(s x, y) -> s +(x, y)} DP: DP: { odd# s x -> not# odd x, odd# s x -> odd# x, +#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y)} TRS: {not false() -> true(), not true() -> false(), odd 0() -> false(), odd s x -> not odd x, +(x, 0()) -> x, +(x, s y) -> s +(x, y), +(s x, y) -> s +(x, y)} UR: {not false() -> true(), not true() -> false(), odd 0() -> false(), odd s x -> not odd x} EDG: {(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (+#(s x, y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y)) (odd# s x -> odd# x, odd# s x -> not# odd x) (odd# s x -> odd# x, odd# s x -> odd# x)} STATUS: arrows: 0.625000 SCCS (2): Scc: {+#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y)} Scc: {odd# s x -> odd# x} SCC (2): Strict: {+#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y)} Weak: {not false() -> true(), not true() -> false(), odd 0() -> false(), odd s x -> not odd x, +(x, 0()) -> x, +(x, s y) -> s +(x, y), +(s x, y) -> s +(x, y)} Open SCC (1): Strict: {odd# s x -> odd# x} Weak: {not false() -> true(), not true() -> false(), odd 0() -> false(), odd s x -> not odd x, +(x, 0()) -> x, +(x, s y) -> s +(x, y), +(s x, y) -> s +(x, y)} Open