YES 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'()))} RUF: Strict: {f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))} Weak: {} DP: Strict: {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(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))} EDG: {} SCCS: Qed