Confluence Competition

CoCo 2019 Results

category 1st place 2nd place 3rd place
COM FORT
CPF-CTRS ConCon+CeTA
CPF-TRS CSI+CeTA ACP+CeTA
CTRS ACP
GCR AGCP FORT
HRS CSI^ho
INF infChecker nonreach Moca
NFP CSI FORT
SRS CSI noko-leipzig ACP
TRS ACP CSI
UNC ACP CSI FORT
UNR CSI FORT

Detailed results are available. The same holds for the LiveView of CoCo 2019 upon completion. Tools with incorrect results (observed during the live competition due to a YES/NO conflict, or communicated afterwards by the tool authors to the SC) are excluded from the results table. This concerns ACP and COLL in the COM category, CO3 and ConCon in the CTRS category, ConCon in the INF category, and CoLL-Saigawa in the TRS category.


Problem Selection

The problems were selected using the following COPS queries. Here s is the number 273 composed of the three random digits 2 (Hubert Garavel), 7 (Geoff Sutcliffe), 3 (Akihisa Yamada) provided by the panel members. The numbers on some of the last lines refer to the secret problems submitted to CoCo 2019.


categories   queries
COM limit:100,s 1..1124 commutation !duplicate
CPF-TRS
TRS
limit:99,s 1..1124 trs !srs !duplicate {!confluent !non_confluent}
limit:72,s 1..1124 trs !srs !duplicate !{!confluent !non_confluent}
1133
CPF-CTRS
CTRS
limit:100,s 1..1124 3_ctrs oriented !duplicate {!confluent !non_confluent}
limit:66,s 1..1124 3_ctrs oriented !duplicate !{!confluent !non_confluent}
GCR limit:100,s 1..1124 !srs {trs OR mstrs} !duplicate {!ground_confluent
!non_ground_confluent}
HRS limit:100,s 1..1124 hrs !duplicate {!confluent !non_confluent}
limit:46,s 1..1124 hrs !duplicate !{!confluent !non_confluent}
INF limit:94,s 1..1124 infeasibility !duplicate
1125 OR 1126 OR 1128 OR 1130 OR 1136 OR 1137
NFP limit:100,s 1..1124 trs !srs !confluent !duplicate {!nfp !non_nfp}
limit:40,s 1..1124 trs !srs !confluent !duplicate !{!nfp !non_nfp}
SRS limit:98,s 1..1124 srs !duplicate {!confluent !non_confluent}
1131 OR 1132
UNC limit:100,s 1..1124 trs !srs !nfp !duplicate {!unc !non_unc}
limit:65,s 1..1124 trs !srs !nfp !duplicate !{!unc !non_unc}
UNR limit:100,s 1..1124 trs !srs !unc !duplicate {!unr !non_unr}
limit:57,s 1..1124 trs !srs !unc !duplicate !{!unr !non_unr}