MAYBE Time: 0.427862 TRS: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} DP: DP: { g#(x, x, x) -> g#(c(), d(), e()), g#(x, y, x) -> g#(c(), d(), e()), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> s# y, f#(h(a(), y), g(x, b(), a())) -> s# b(), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), s# f(x, y) -> f#(y, f(s s x, a())), s# f(x, y) -> f#(s s x, a()), s# f(x, y) -> s# x, s# f(x, y) -> s# s x, h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())), h#(f(x, s y), b()) -> f#(s x, a()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(f(x, s y), b()) -> s# x, h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} TRS: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} UR: { g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} EDG: { (g#(x, x, x) -> g#(c(), d(), e()), g#(x, y, x) -> g#(c(), d(), e())) (g#(x, x, x) -> g#(c(), d(), e()), g#(x, x, x) -> g#(c(), d(), e())) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(h(a(), y), g(x, b(), a())) -> s# b()) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(h(a(), y), g(x, b(), a())) -> s# y) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b())) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (s# f(x, y) -> s# s x, s# f(x, y) -> s# s x) (s# f(x, y) -> s# s x, s# f(x, y) -> s# x) (s# f(x, y) -> s# s x, s# f(x, y) -> f#(s s x, a())) (s# f(x, y) -> s# s x, s# f(x, y) -> f#(y, f(s s x, a()))) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(h(a(), y), g(x, b(), a())) -> s# b()) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(h(a(), y), g(x, b(), a())) -> s# y) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(y, b())) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (h#(f(x, s y), b()) -> f#(s x, a()), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (h#(f(x, s y), b()) -> f#(s x, a()), f#(h(a(), y), g(x, b(), a())) -> s# b()) (h#(f(x, s y), b()) -> f#(s x, a()), f#(h(a(), y), g(x, b(), a())) -> s# y) (h#(f(x, s y), b()) -> f#(s x, a()), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (h#(f(x, s y), b()) -> f#(s x, a()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (h#(f(x, s y), b()) -> f#(s x, a()), f#(x, f(y, f(x, y))) -> f#(y, b())) (h#(f(x, s y), b()) -> f#(s x, a()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (h#(f(x, s y), b()) -> f#(s x, a()), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (h#(f(x, s y), b()) -> f#(s x, a()), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (h#(f(x, s y), b()) -> f#(s x, a()), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())), g#(x, y, x) -> g#(c(), d(), e())) (h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())), g#(x, x, x) -> g#(c(), d(), e())) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> s# b()) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> s# y) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(y, b())) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (s# f(x, y) -> s# x, s# f(x, y) -> s# s x) (s# f(x, y) -> s# x, s# f(x, y) -> s# x) (s# f(x, y) -> s# x, s# f(x, y) -> f#(s s x, a())) (s# f(x, y) -> s# x, s# f(x, y) -> f#(y, f(s s x, a()))) (h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))) (h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(a(), y)) (h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(a(), x)) (h#(h(x, a()), y) -> h#(a(), y), h#(f(x, s y), b()) -> s# x) (h#(h(x, a()), y) -> h#(a(), y), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))) (h#(h(x, a()), y) -> h#(a(), y), h#(f(x, s y), b()) -> f#(s x, a())) (h#(h(x, a()), y) -> h#(a(), y), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a()))) (h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))) (h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y)) (h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), x)) (h#(h(x, a()), y) -> h#(a(), x), h#(f(x, s y), b()) -> s# x) (h#(h(x, a()), y) -> h#(a(), x), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))) (h#(h(x, a()), y) -> h#(a(), x), h#(f(x, s y), b()) -> f#(s x, a())) (h#(h(x, a()), y) -> h#(a(), x), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a()))) (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> s# s x) (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> s# x) (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> f#(s s x, a())) (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> f#(y, f(s s x, a()))) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a()))) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(s x, a())) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> s# x) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(h(x, a()), y) -> h#(a(), x)) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(h(x, a()), y) -> h#(a(), y)) (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, f(y, f(x, y))) -> f#(y, b())) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> s# y) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> s# b()) (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y), g#(x, x, x) -> g#(c(), d(), e())) (f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y), g#(x, y, x) -> g#(c(), d(), e())) (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> f#(y, f(s s x, a()))) (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> f#(s s x, a())) (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> s# x) (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> s# s x) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a()))) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(f(x, s y), b()) -> f#(s x, a())) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(f(x, s y), b()) -> s# x) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(h(x, a()), y) -> h#(a(), x)) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(h(x, a()), y) -> h#(a(), y)) (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, f(y, f(x, y))) -> f#(y, b())) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(h(a(), y), g(x, b(), a())) -> s# y) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(h(a(), y), g(x, b(), a())) -> s# b()) (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, f(y, f(x, y))) -> f#(y, b())) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> s# y) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> s# b()) (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (s# f(x, y) -> f#(s s x, a()), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (s# f(x, y) -> f#(s s x, a()), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (s# f(x, y) -> f#(s s x, a()), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (s# f(x, y) -> f#(s s x, a()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (s# f(x, y) -> f#(s s x, a()), f#(x, f(y, f(x, y))) -> f#(y, b())) (s# f(x, y) -> f#(s s x, a()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (s# f(x, y) -> f#(s s x, a()), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (s# f(x, y) -> f#(s s x, a()), f#(h(a(), y), g(x, b(), a())) -> s# y) (s# f(x, y) -> f#(s s x, a()), f#(h(a(), y), g(x, b(), a())) -> s# b()) (s# f(x, y) -> f#(s s x, a()), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a()))) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> f#(s x, a())) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> s# x) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(h(x, a()), y) -> h#(a(), x)) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(h(x, a()), y) -> h#(a(), y)) (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))) (s# f(x, y) -> f#(y, f(s s x, a())), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y)) (s# f(x, y) -> f#(y, f(s s x, a())), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y))) (s# f(x, y) -> f#(y, f(s s x, a())), f#(x, g(x, a(), f(s x, y))) -> h#(x, b())) (s# f(x, y) -> f#(y, f(s s x, a())), f#(x, f(y, f(x, y))) -> f#(x, f(y, b()))) (s# f(x, y) -> f#(y, f(s s x, a())), f#(x, f(y, f(x, y))) -> f#(y, b())) (s# f(x, y) -> f#(y, f(s s x, a())), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))) (s# f(x, y) -> f#(y, f(s s x, a())), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y)) (s# f(x, y) -> f#(y, f(s s x, a())), f#(h(a(), y), g(x, b(), a())) -> s# y) (s# f(x, y) -> f#(y, f(s s x, a())), f#(h(a(), y), g(x, b(), a())) -> s# b()) (s# f(x, y) -> f#(y, f(s s x, a())), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b())) (g#(x, y, x) -> g#(c(), d(), e()), g#(x, x, x) -> g#(c(), d(), e())) (g#(x, y, x) -> g#(c(), d(), e()), g#(x, y, x) -> g#(c(), d(), e())) (f#(h(a(), y), g(x, b(), a())) -> s# b(), s# f(x, y) -> f#(y, f(s s x, a()))) (f#(h(a(), y), g(x, b(), a())) -> s# b(), s# f(x, y) -> f#(s s x, a())) (f#(h(a(), y), g(x, b(), a())) -> s# b(), s# f(x, y) -> s# x) (f#(h(a(), y), g(x, b(), a())) -> s# b(), s# f(x, y) -> s# s x) } STATUS: arrows: 0.710775 SCCS (2): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> s# y, f#(h(a(), y), g(x, b(), a())) -> s# b(), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), s# f(x, y) -> f#(y, f(s s x, a())), s# f(x, y) -> f#(s s x, a()), s# f(x, y) -> s# x, s# f(x, y) -> s# s x, h#(f(x, s y), b()) -> f#(s x, a()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(f(x, s y), b()) -> s# x, h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Scc: {g#(x, x, x) -> g#(c(), d(), e()), g#(x, y, x) -> g#(c(), d(), e())} SCC (19): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> s# y, f#(h(a(), y), g(x, b(), a())) -> s# b(), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), s# f(x, y) -> f#(y, f(s s x, a())), s# f(x, y) -> f#(s s x, a()), s# f(x, y) -> s# x, s# f(x, y) -> s# s x, h#(f(x, s y), b()) -> f#(s x, a()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(f(x, s y), b()) -> s# x, h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1, x2) = 1, [f](x0, x1) = 0, [h](x0, x1) = 0, [s](x0) = 1, [c] = 0, [d] = 0, [e] = 0, [a] = 0, [b] = 0, [f#](x0, x1) = x0, [h#](x0, x1) = 1, [s#](x0) = 1 Strict: h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)) 1 + 0x + 0y >= 1 + 0x + 0y h#(h(x, a()), y) -> h#(a(), y) 1 + 0x + 0y >= 1 + 0y h#(h(x, a()), y) -> h#(a(), x) 1 + 0x + 0y >= 1 + 0x h#(f(x, s y), b()) -> s# x 1 + 0x + 0y >= 1 + 0x h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y h#(f(x, s y), b()) -> f#(s x, a()) 1 + 0x + 0y >= 0 + 0x s# f(x, y) -> s# s x 1 + 0x + 0y >= 1 + 0x s# f(x, y) -> s# x 1 + 0x + 0y >= 1 + 0x s# f(x, y) -> f#(s s x, a()) 1 + 0x + 0y >= 0 + 0x s# f(x, y) -> f#(y, f(s s x, a())) 1 + 0x + 0y >= 0 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> s# b() 1 + 0x + 0y >= 1 f#(h(a(), y), g(x, b(), a())) -> s# y 1 + 0x + 0y >= 1 + 0y f#(h(a(), y), g(x, b(), a())) -> f#(x, s y) 1 + 0x + 0y >= 1 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(y, b()) 0 + 0x + 0y >= 0 + 0y f#(x, f(y, f(x, y))) -> f#(x, f(y, b())) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, g(x, a(), f(s x, y))) -> h#(x, b()) 1 + 0x + 0y >= 1 + 0x f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)) 1 + 0x + 0y >= 1 + 0x + 0y Weak: h(h(x, a()), y) -> h(h(a(), y), h(a(), x)) 0 + 0x + 0y >= 0 + 0x + 0y h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))) 0 + 0x + 0y >= 0 + 0x + 0y s f(x, y) -> f(y, f(s s x, a())) 1 + 0x + 0y >= 0 + 0x + 0y s y -> b() 1 + 0y >= 0 f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()) 0 + 0x + 0y >= 0 + 0x + 0y f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))) 0 + 0x + 0y >= 0 + 0x + 0y f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)) 0 + 0x + 0y >= 0 + 0x + 0y g(x, y, x) -> g(c(), d(), e()) 1 + 0x + 0y >= 1 g(x, x, x) -> g(c(), d(), e()) 1 + 0x >= 1 SCCS (2): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Scc: {s# f(x, y) -> s# x, s# f(x, y) -> s# s x} SCC (11): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1, x2) = 1, [f](x0, x1) = 0, [h](x0, x1) = 0, [s](x0) = 0, [c] = 0, [d] = 0, [e] = 0, [a] = 0, [b] = 0, [f#](x0, x1) = x0, [h#](x0, x1) = 1 Strict: h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)) 1 + 0x + 0y >= 1 + 0x + 0y h#(h(x, a()), y) -> h#(a(), y) 1 + 0x + 0y >= 1 + 0y h#(h(x, a()), y) -> h#(a(), x) 1 + 0x + 0y >= 1 + 0x h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> f#(x, s y) 1 + 0x + 0y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(y, b()) 0 + 0x + 0y >= 0 + 0y f#(x, f(y, f(x, y))) -> f#(x, f(y, b())) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, g(x, a(), f(s x, y))) -> h#(x, b()) 1 + 0x + 0y >= 1 + 0x f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)) 1 + 0x + 0y >= 1 + 0x + 0y Weak: h(h(x, a()), y) -> h(h(a(), y), h(a(), x)) 0 + 0x + 0y >= 0 + 0x + 0y h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))) 0 + 0x + 0y >= 0 + 0x + 0y s f(x, y) -> f(y, f(s s x, a())) 0 + 0x + 0y >= 0 + 0x + 0y s y -> b() 0 + 0y >= 0 f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()) 0 + 0x + 0y >= 0 + 0x + 0y f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))) 0 + 0x + 0y >= 0 + 0x + 0y f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)) 0 + 0x + 0y >= 0 + 0x + 0y g(x, y, x) -> g(c(), d(), e()) 1 + 0x + 0y >= 1 g(x, x, x) -> g(c(), d(), e()) 1 + 0x >= 1 SCCS (1): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} SCC (10): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1, x2) = 1, [f](x0, x1) = x0, [h](x0, x1) = x0, [s](x0) = 1, [c] = 0, [d] = 0, [e] = 0, [a] = 0, [b] = 0, [f#](x0, x1) = x0 + x1, [h#](x0, x1) = x0 Strict: h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)) 0 + 1x + 0y >= 0 + 0x + 0y h#(h(x, a()), y) -> h#(a(), y) 0 + 1x + 0y >= 0 + 0y h#(h(x, a()), y) -> h#(a(), x) 0 + 1x + 0y >= 0 + 0x h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))) 0 + 1x + 1y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(y, b()) 0 + 1x + 1y >= 0 + 1y f#(x, f(y, f(x, y))) -> f#(x, f(y, b())) 0 + 1x + 1y >= 0 + 1x + 0y f#(x, g(x, a(), f(s x, y))) -> h#(x, b()) 1 + 1x + 0y >= 0 + 1x f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)) 1 + 1x + 0y >= 1 + 1x + 0y Weak: h(h(x, a()), y) -> h(h(a(), y), h(a(), x)) 0 + 1x + 0y >= 0 + 0x + 0y h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y s f(x, y) -> f(y, f(s s x, a())) 1 + 0x + 0y >= 0 + 0x + 0y s y -> b() 1 + 0y >= 0 f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))) 0 + 0x + 1y >= 0 + 0x + 0y f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)) 1 + 0x + 0y >= 1 + 0x + 0y g(x, y, x) -> g(c(), d(), e()) 1 + 0x + 0y >= 1 g(x, x, x) -> g(c(), d(), e()) 1 + 0x >= 1 SCCS (1): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} SCC (9): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(y, b()), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1, x2) = 0, [f](x0, x1) = 1, [h](x0, x1) = x0, [s](x0) = 0, [c] = 0, [d] = 0, [e] = 0, [a] = 0, [b] = 0, [f#](x0, x1) = x0, [h#](x0, x1) = 0 Strict: h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)) 0 + 0x + 0y >= 0 + 0x + 0y h#(h(x, a()), y) -> h#(a(), y) 0 + 0x + 0y >= 0 + 0y h#(h(x, a()), y) -> h#(a(), x) 0 + 0x + 0y >= 0 + 0x h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))) 0 + 0x + 0y >= 0 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))) 1 + 0x + 0y >= 1 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(y, b()) 1 + 0x + 0y >= 0 + 0y f#(x, f(y, f(x, y))) -> f#(x, f(y, b())) 1 + 0x + 0y >= 1 + 0x + 0y f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)) 0 + 0x + 0y >= 0 + 0x + 0y Weak: h(h(x, a()), y) -> h(h(a(), y), h(a(), x)) 0 + 1x + 0y >= 0 + 0x + 0y h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y s f(x, y) -> f(y, f(s s x, a())) 0 + 0x + 0y >= 1 + 0x + 0y s y -> b() 0 + 0y >= 0 f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))) 1 + 0x + 0y >= 1 + 0x + 0y f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)) 1 + 0x + 0y >= 1 + 0x + 0y g(x, y, x) -> g(c(), d(), e()) 0 + 0x + 0y >= 0 g(x, x, x) -> g(c(), d(), e()) 0 + 0x >= 0 SCCS (1): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} SCC (8): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1, x2) = 0, [f](x0, x1) = x0 + 1, [h](x0, x1) = 1, [s](x0) = 0, [c] = 0, [d] = 0, [e] = 0, [a] = 0, [b] = 0, [f#](x0, x1) = x0, [h#](x0, x1) = 0 Strict: h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)) 0 + 0x + 0y >= 0 + 0x + 0y h#(h(x, a()), y) -> h#(a(), y) 0 + 0x + 0y >= 0 + 0y h#(h(x, a()), y) -> h#(a(), x) 0 + 0x + 0y >= 0 + 0x h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))) 0 + 0x + 0y >= 0 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))) 2 + 0x + 1y >= 2 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(x, f(y, b())) 2 + 0x + 1y >= 1 + 0x + 0y f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)) 0 + 0x + 0y >= 0 + 0x + 0y Weak: h(h(x, a()), y) -> h(h(a(), y), h(a(), x)) 1 + 0x + 0y >= 1 + 0x + 0y h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y s f(x, y) -> f(y, f(s s x, a())) 0 + 0x + 0y >= 2 + 0x + 0y s y -> b() 0 + 0y >= 0 f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))) 3 + 0x + 1y >= 3 + 0x + 0y f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)) 1 + 0x + 0y >= 1 + 0x + 0y g(x, y, x) -> g(c(), d(), e()) 0 + 0x + 0y >= 0 g(x, x, x) -> g(c(), d(), e()) 0 + 0x >= 0 SCCS (1): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} SCC (7): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(a(), x), h#(h(x, a()), y) -> h#(a(), y), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1, x2) = 1, [f](x0, x1) = x0, [h](x0, x1) = 1, [s](x0) = 0, [c] = 0, [d] = 0, [e] = 0, [a] = 0, [b] = 0, [f#](x0, x1) = 0, [h#](x0, x1) = x0 Strict: h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)) 1 + 0x + 0y >= 1 + 0x + 0y h#(h(x, a()), y) -> h#(a(), y) 1 + 0x + 0y >= 0 + 0y h#(h(x, a()), y) -> h#(a(), x) 1 + 0x + 0y >= 0 + 0x h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))) 0 + 0x + 0y >= 0 + 0x + 0y f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))) 0 + 0x + 0y >= 0 + 0x + 0y f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)) 0 + 0x + 0y >= 0 + 0x + 0y Weak: h(h(x, a()), y) -> h(h(a(), y), h(a(), x)) 1 + 0x + 0y >= 1 + 0x + 0y h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))) 1 + 0x + 0y >= 1 + 0x + 0y s f(x, y) -> f(y, f(s s x, a())) 0 + 0x + 0y >= 0 + 0x + 0y s y -> b() 0 + 0y >= 0 f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()) 1 + 0x + 0y >= 1 + 0x + 0y f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))) 0 + 0x + 1y >= 0 + 0x + 0y f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)) 1 + 0x + 0y >= 1 + 0x + 0y g(x, y, x) -> g(c(), d(), e()) 1 + 0x + 0y >= 1 g(x, x, x) -> g(c(), d(), e()) 1 + 0x >= 1 SCCS (1): Scc: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} SCC (5): Strict: { f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} Fail SCC (2): Strict: {s# f(x, y) -> s# x, s# f(x, y) -> s# s x} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} Fail SCC (2): Strict: {g#(x, x, x) -> g#(c(), d(), e()), g#(x, y, x) -> g#(c(), d(), e())} Weak: { g(x, x, x) -> g(c(), d(), e()), g(x, y, x) -> g(c(), d(), e()), f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)), f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))), f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()), s y -> b(), s f(x, y) -> f(y, f(s s x, a())), h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))), h(h(x, a()), y) -> h(h(a(), y), h(a(), x))} Fail