Completion Experiments
The following table collects results obtained with mkbtt running normalized completion with different versions of AC-KBO. A tarball containing all input systems 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 200 seconds. Each termination call had a timeout of 1.5 seconds, and the primality critical pair criterion was used.
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 | ./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'acrpo -direct' |
1 | ./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -nt' |
2 | ./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -sc -nt' |
3 | ./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'matrix -ac -ib 2 -ob 3 -dim 1 -direct' |
4 | ./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'matrix -ac -ib 2 -ob 3 -dim 2 -direct' |