The following color code is used in the table below:
YES, we have termination and linear/quadratic derivational complexity |
MAYBE, no proof found |
A TIMEOUT has occurred |
An error has occurred |
The tests were run single-threaded on a server equipped with 8 AMD Opteron 2.8 GHz dual core processors with 64GB of RAM. The time limit for this table is 60 seconds. All times are given in seconds. All tests on cdiprover3 were conducted using the incremental search strategy of cdiprover3 ("-i" flag). The maximal bound for all coefficient variables in cdiprover3 has been set to 31 ("-b 31" flag), which corresponds to using at most 5 bits each in a SAT encoding. TTT2 was called with the strategy 'if duplicating then fail else bounds[60]'.