The following color code is used in the table below:
YES, we have termination and exponential/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 were conducted using the incremental search strategy of cdiprover2 and cdiprover3 ("-i" flag). The maximal bound for all coefficient variables has been set to 31 ("-b 31" flag), which corresponds to using at most 5 bits each in a SAT encoding.