YES Time: 0.136788 TRS: {f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())), f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))} DP: DP: {f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'())} TRS: {f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())), f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))} UR: {} EDG: {(f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'())) (f#(g(h(a(), b()), c()), d()) -> f#(c(), d'()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'())) (f#(g(h(a(), b()), c()), d()) -> f#(c(), d'()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d())) (f#(g(h(a(), b()), c()), d()) -> f#(c(), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'())) (f#(g(h(a(), b()), c()), d()) -> f#(c(), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'())) (f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'())) (f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'())) (f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d())) (f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d())) (f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'()))} STATUS: arrows: 0.000000 SCCS (1): Scc: {f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'())} SCC (4): Strict: {f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()), f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()), f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()), f#(g(h(a(), b()), c()), d()) -> f#(c(), d'())} Weak: {f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())), f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [i](x0, x1, x2) = x0 + 1, [f](x0, x1) = 0, [.](x0, x1) = x0, [g](x0, x1) = x0, [h](x0, x1) = 0, [e] = 1, [b] = 1, [c] = 0, [d'] = 0, [b'] = 1, [a] = 1, [d] = 1, [f#](x0, x1) = x0 + 1 Strict: f#(g(h(a(), b()), c()), d()) -> f#(c(), d'()) 2 >= 1 f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()) 2 >= 2 f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b'(), c()), d'()) 2 >= 1 f#(g(i(a(), b(), b'()), c()), d()) -> f#(.(b(), c()), d'()) 2 >= 1 Weak: f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) 0 >= 2 f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())) 0 >= 2 SCCS (1): Scc: {f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d())} SCC (1): Strict: {f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d())} Weak: {f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())), f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1, [i](x0, x1, x2) = 0, [f](x0, x1) = x0 + x1, [.](x0, x1) = 0, [g](x0, x1) = x0, [h](x0, x1) = 0, [e] = 1, [b] = 0, [c] = 1, [d'] = 1, [b'] = 0, [a] = 0, [d] = 0, [f#](x0, x1) = x0 + 1 Strict: f#(g(h(a(), b()), c()), d()) -> f#(.(b(), g(h(a(), b()), c())), d()) 2 >= 1 Weak: f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) 1 >= 3 f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())) 1 >= 2 Qed