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, in the latter case with subterm coefficients. For both cases partial precedences were allowed. Column 3 applies linear polynomials and column 4 applies two-dimensional matrix interpretations. In the settings corresponding to columns 2 to 4 four bits were allowed for coefficients, and five bits to represent the result.
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 -sc -direct -nt' |
3 | ./ttt2 -t -s 'matrix -ac -dim 1 -ib 4 -ob 5 -direct' |
4 | ./ttt2 -t -s 'matrix -ac -dim 2 -ib 4 -ob 5 -direct' |