The following table collects results obtained with TTT2 running different versions of AC-KBO. A tarball containing all input problems can be found here.

Results in one row were obtained in parallel and run on a server equipped with eight dual-core AMD Opteron processors 885 running at a clock rate of 2.6GHz with 64GB of main memory, for each setting with a timeout of 60 seconds.

For the following experiments, different variants of AC-KBO were applied in the AC-dependency pair framework. More precisely, the strategy comprised (unmarked) AC-dependency pair computation, an AC-dependency graph estimation, SCCs, and a variant of AC-KBO with argument filterings and usable rules. The reduction pair processor was applied iteratively. The columns correspond to the following settings. Column ACRPO applies AC-RPO for comparison. Column ACKBO applies our new AC-KBO. Column ST corresponds to Steinbach's order while columns KV and KV' use Korovin and Voronkov's order and our modified variant. The last column applies our AC-KBO with subterm coefficients. In all settings 3 input and 4 output bits, were allowed, and partial precedences allowed.