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