YES Time: 0.000382 TRS: {f g(f a(), h(a(), f a())) -> f h(g(f a(), a()), g(f a(), f a()))} DP: DP: {f# g(f a(), h(a(), f a())) -> f# h(g(f a(), a()), g(f a(), f a()))} TRS: {f g(f a(), h(a(), f a())) -> f h(g(f a(), a()), g(f a(), f a()))} EDG: {} SCCS (0): Qed