Confluence Competition

CoCo 2016


September 8, 2016: Competition finished.
August 29, 2016: Added entrants.
August 19, 2016: Added detail of the execution platform.
July 26, 2016: Added detail of demostration categories.
March 20, 2016: 2nd CFP is announced.
March 19, 2016: Added detail of the registration.
March 17, 2016: The type of problems for the CTRS category is fixed to oriented CTRSs of type 3.
Jan 15, 2016: 1st CFP is announced.
Jan 7, 2016: This page is created


Slides, details, details on StarExec, and results of CoCo 2016. Congratulations to the winners: CSI (TRS category), ConCon (CTRS category), CSI+CeTA/ConCon+CeTA (CPF category), and CSI^ho (HRS category).


This site lists relevant information for the 5th Confluence Competition (CoCo 2016), collocated with CLA 2016 in Obergurgl, Austria. The competition will run live during the 5th International Workshop on Confluence (IWC 2016). We invite everyone developing confluence (and related) tools to join CoCo 2016, to share problems and challenges.


The following categories will be run:

Furthermore, the following demonstration categories will be run:

Besides these categories, new categories will be considered if there are tools and problems dedicated to those categories. We welcome requests for categories. We solicit new categories for the competition (competition categories) as well as demonstration categories. Demonstration categories are one-time events for demonstrating new attempts and/or merit of particular tools, where a problem set need not to stem from Cops. For instance, the next categories are in the scope of demonstration: right-ground TRSs, CTRSs of specific condition type, eTRSs, ground confluence and the unique normal form property.


request for competition categoriesFebruary 28, 2016
request for demonstration categoriesJune 30, 2016
tool registrationAugust 21, 2016
tool submissionAugust 28, 2016, extended: August 30, 2016
problem submissionAugust 30, 2016, extended: September 1, 2016
competitionSeptember 8, 2016


These problems will be considered for CoCo 2016. Only problems of oriented CTRSs of type 3 are considered in the CTRS category. Submissions of new confluence problems are welcome. Submissions are via Cops. Problems submitted after the problem submission deadline will not be considered for the competition.

Execution Platform

CoCo 2016 will run on StarExec, a high-end cross-community competition platform. The 64-bit operating system will be Red Hat Enterprise Linux Workstation. Details of the specification are available here. CoCo 2016 will use nodes 0 - 32. For each problem a tool will have 60 seconds access to a single node (consisting of a quad-core Intel(R) Xeon(R) processors E5-2609 0 running at a clock rate of 2.40 GHz and 128 GB of main memory).

Request for Categories

Request for new categories is via the contact email address. Please send us the following information at your earliest convenience:

It is preferable that a prototype of the tool and sample problems are available at the time of the request. Please note that for competition categories we presume integration of problem collections into our database for running the competition. Requests for categories may be rejected for technical reasons.


Tools must be able to run on the designated execution platform and read problems as input. The output of the tools must contain an answer in the first line followed by some proof argument understandable for human experts. Valid answers are YES (the input is confluent) and NO (the input is not confluent). Every other answer is interpreted as the tool could not determine the status of the input.

For the CPF category, each participant should output certifiable proofs as well as the result of certification: YES followed by a certifiable proof (e.g. a proof in cpf format) if confluence proof is certified, and NO followed by a certifiable proof if non-confluence proof is certified. A tool should output UNSUPPORTED in place of YES/NO for input (C)TRSs in classes that the tool does not support; in particular, a tool that is not registered to any TRS (CTRS) category should output UNSUPPORTED for any input of CTRSs (resp. TRSs).

It is encouraged that tools are open source and that binaries of the competition versions of the tools can be archived on the competition website.


Tool registration must be made electronically through the EasyChair system at: Specify tool name as the title and tool authors as the authors. Please use the following form for the abstract:

Categories to enter: TRS/CTRS/CPF/HRS/Demo  (leave appropriate ones)
URL of tool's website:                      (if there is one)
Please submit one page system description in EasyChair LaTeX class style highlighting the distinctive features of the prover (in a single latex file). System descriptions will be included in the proceedings of IWC 2016. Tool submission will be via StarExec. For the demonstration categories, the problem submission is via uploading the problem collection to StarExec together with the tool.


The score is computed in percent of solved vs. supported problems (i.e. number of YES/NO answers vs. total – number of UNSUPPORTED answers). In case of a draw there might be more winners. The tool with the maximal score wins. An answer is plausible if it was not falsified (automatically or manually). A tool with at least one non-plausible answer cannot be a winner.


ACP TRS/CPF Takahito Aoto (Niigata University)
Yoshihito Toyama (Tohoku University)
paper slides tools:
ACPH HRS Kouta Onozawa (Tohoku University)
Kentaro Kikuchi (Tohoku University)
Takahito Aoto (Niigata University)
Yoshihito Toyama (Tohoku University)
paper slides tool
AGCP Demo(GCR) Takahito Aoto (Tohoku University)
Yoshihito Toyama (Tohoku University)
paper slides tool
CeTA CPF Julian Nagele (University of Innsbruck)
Christian Sternagel (University of Innsbruck)
Thomas Sternagel (University of Innsbruck)
paper slides tools:
ACP and CeTA,
ConCon and CeTA,
CSI and CeTA
CO3 CTRS Naoki Nishida (Nagoya University)
Takayuki Kuroda (Nagoya University)
Karl Gmeiner (UAS Technikum Wien)
paper slides tool
CoLL-Saigawa TRS Nao Hirokawa (JAIST)
Kiraku Shintani (JAIST)
paper slides tool
ConCon CTRS/CPF Thomas Sternagel (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tools:
ConCon, ConCon and CeTA
CoScart CTRS Karl Gmeiner (UAS Technikum Wien) paper tool
CRC TRS/CTRS/Demo(EOSCS-MT) Francisco Durán (University of Málaga) paper (withdrawn)
CSI TRS/CPF/Demo(UN) Bertram Felgenhauer (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
Julian Nagele (University of Innsbruck)
paper slides tools:
CSI^ho HRS Julian Nagele (University of Innsbruck) paper slides tool
FORT Demo(UN)/Demo(GCR) Franziska Rapp (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tool
Nrbox Demo(NRS) Takahito Aoto (Tohoku University)
Kentaro Kikuchi (Tohoku University)
paper slides tool

Organising Committee