Termination Experiments
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.
The columns correspond to the following settings. Column 0 applies AC-RPO. Columns 1 and 2 apply our version of AC-KBO and Steinbach's AC-KBO, where for both cases partial precedences were allowed. Columns 3 and 4 correspond to Korovin & Voronkov's AC-KBO >kv and the simplification order >'kv, respectively. Finally, 5 corresponds to our AC-KBO with subterm coefficients, where again partial precedences are allowed. For all settings we used 4 input and 5 output bits.
Legend | |
0 | ./ttt2 -t -s 'acrpo -direct' |
1 | ./ttt2 -t -s 'ackbo -ib 4 -ob 5 -direct -nt' |
2 | ./ttt2 -t -s 'ackbo -ib 4 -ob 5 -st -nt -direct' |
3 | ./ttt2 -t -s 'ackbo -ib 4 -ob 5 -kv -direct' |
4 | ./ttt2 -t -s 'ackbo -ib 4 -ob 5 -kv2 -direct' |
5 | ./ttt2 -t -s 'ackbo -ib 4 -ob 5 -sc -direct -nt' |