Confluence Competition

CoCo 2015


Aug 2, 2015: Competition finished.
Jun 21, 2015: Added detail of the execution platform.
Jun 21, 2015: Added entrants.
Jun 20, 2015: Information about CPF category revised.
May 13, 2015: Tool registration method is updated and system description format is specified.
Jan 06, 2015: First HRSs added to Cops
Dec 10, 2014: Detail information is added
Dec 08, 2014: This page is created


Slides, details, and results of CoCo 2015. A report at CADE-25.
The following answers turn out to be incorrect: Cops ♯455 by ACPH and Cops ♯262 by CoScart.
Congratulations to the winners: ACP and CSI (TRS category), ConCon (CTRS category), and CSI+CeTA (CPF category) and CSI^ho (HRS category).


This site lists relevant information for the 4th Confluence Competition (CoCo 2015), collocated with CADE-25 in Berlin, Germany. The competition will run live during the 4th International Workshop on Confluence (IWC 2015). We invite everyone developing confluence (and related) tools to join CoCo 2015, to share problems and challenges.


The following categories will be run:

Furthermore, the following demonstration categories will be run: new!

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 categoriesJanuary 31, 2015
request for demonstration categoriesMay 31, 2015
tool registrationJuly 19, 2015
tool submissionJuly 26, 2015
problem submissionJuly 28, 2015
competitionAugust 2, 2015


These problems will be considered for CoCo 2015. 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 2015 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 2015 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.

Every problem in the CTRS category is classified by the pair of

A tool should output UNSUPPORTED in place of YES/NO for input CTRSs in classes that the tool does not support.

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)
(Un)supported classes for CTRS category:  (if there are)
Coupled tools for CPF category:           (if there are) 
URL of tool's website:                    (if there is one)
Please submit one page system description in EasyChair style highlighting the distinctive features of the prover (in a single latex file). System descriptions will be included in the proceedings of IWC 2015. Tool submission is via StarExec.


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 (Tohoku University)
Yoshihito Toyama (Tohoku University)
paper slides tools:
ACPH HRS Kouta Onozawa (Tohoku University)
Kentaro Kikuchi (Tohoku University)
Takahito Aoto (Tohoku 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)
René Thiemann (University of Innsbruck)
Sarah Winkler (University of Innsbruck)
Harald Zankl (University of Innsbruck)
paper slides tools:
ACP and CeTA,
ConCon and CeTA,
CSI and CeTA
CO3 CTRS (oriented, type 1) Naoki Nishida (Nagoya University)
Takayuki Kuroda (Nagoya University)
Makishi Yanagisawa (Nagoya University)
Karl Gmeiner (UAS Technikum Wien)
paper slides tool
CoLL-Saigawa TRS Nao Hirokawa (JAIST)
Kiraku Shintani (JAIST)
paper slides tool
ConCon CTRS (oriented, types 1-4)/CPF Thomas Sternagel (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tools:
ConCon, ConCon and CeTA
CoScart TRS/CTRS(oriented, type 1-3) Karl Gmeiner (UAS Technikum Wien) paper slides tool
CSI TRS/CPF Bertram Felgenhauer (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
Julian Nagele (University of Innsbruck)
Harald Zankl (University of Innsbruck)
paper slides tools:
CSI^ho HRS Julian Nagele (University of Innsbruck) paper slides tool
NoCo Demo(NRS) Takaki Suzuki (Tohoku University)
Kentaro Kikuchi (Tohoku University)
Takahito Aoto (Tohoku University)
paper slides tool

Organising Committee