Experiments
The set of systems (in the modified TRS format) we used in our experiments may be downloaded here and is also available from the confluence problems database.
The experiments we describe here were carried out with ConCon 1.1.0.0 on a 64bit GNU/Linux machine with an Intel® Core™ i7-3520M processor clocked at 2.90GHz and 8GB of RAM. The kernel version is 3.14.1-1-ARCH. The version of Java on this machine is 1.7.0_55. We increased the stack size of the JVM to 20MB by setting the flag -Xss20M to prevent stack overflows caused by parsing deep terms like in the file 313.trs.
The following external tools have been used during the experiments:
We used the tool parallel to run the experiments with a maximum of 1 job at the same time.
Confluence
topFor this test series all input systems were interpreted as oriented systems. The timeout was set to 60 seconds. The numbers in the table indicate the time it took ConCon to reach a conclusion in seconds.
The last line of the table sums up the overall results. The value before the slash gives the total number of systems while the value after the slash gives the number of systems which could be proved confluent.
The cells of the following table are color-coded as follows:
| the system is confluent | |
| ConCon could not decide if the system is confluent |
Quasi-Decreasingness
topFor this test series all input systems were interpreted as oriented systems. The timeout was set to 60 seconds.
The cells of the following table are color-coded as follows:
| the system is quasi-decreasing | |
| ConCon could not decide if the system is quasi-decreasing |