Confluence Competition

CoCo 2017


September 8, 2017: Competition finished.
September 8, 2017: watch live here
July 25, 2017: Final CFP is announced.
Jun 7, 2017: 2nd CFP is announced.
Dec 27, 2016: 1st CFP is announced.
Dec 27, 2016: This page is created.


Slides, details, details on StarExec, and results of CoCo 2017. Congratulations to the winners: CSI (TRS and UN categories), ConCon (CTRS and CPF categories), AGCP (GCR category), and CSI^ho (HRS category).


This site lists relevant information for the 6th Confluence Competition (CoCo 2017). The competition will run live during the 6th International Workshop on Confluence (IWC 2017), to be collocated with the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) in Oxford, United Kingdom. We invite everyone developing confluence (and related) tools to join CoCo 2017, to share problems and challenges.


The following categories will be run:

For the details (input, problem, etc.) of each category, check the category page. The CPF and UN categories are combined categories, and all of their component categories will be run.


request for competition categoriesFebruary 28, 2017
request for demonstration categoriesJune 30, 2017
tool registrationAugust 13, 2017
tool submissionAugust 23, 2017
problem submissionAugust 27, 2017
competitionSeptember 8, 2017


Submissions of new problems are welcome. Submissions are via Cops. Problems submitted after the problem submission deadline will not be considered for the competition.

Execution Platform

CoCo 2017 will run on StarExec, a high-end cross-community competition platform. Details of the specification are available here. For each problem a tool will have 60 seconds access to a single node.

Request for Categories

We still solicit demonstration categories for CoCo 2017. See here to send your request.


Tools must be able to run on the designated execution platform. 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; they shall be used in our web interface in future.


Tool registration will be via EasyChair. Every tool registration should also contain a one page system description. 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-TRS/CPF-CTRS/HRS/GCR/UNC/UNR/NFP/Demo  (leave appropriate ones)
URL of tool's website:                      (if there is one)

Entrants for CPF-TRS or CPF-CTRS category automatically enter the CPF category, and those for UNC, UNR or NFP category automatically enter the UN category. Please submit one page system description in EasyChair LaTeX class style highlighting the distinctive features of the prover (in a single latex file). Tool submission will be via StarExec. Details for submission on StarExec will be added later.


ACP TRS/CPF-TRS 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 GCR Takahito Aoto (Tohoku University)
Yoshihito Toyama (Tohoku University)
paper slides tool
CeTA CPF-TRS/CPF-CTRS 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)
Yoshiaki Kanazawa (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-CTRS Thomas Sternagel (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tools:
ConCon, ConCon and CeTA
CSI TRS/CPF-TRS/UNC/UNR/NFP Bertram Felgenhauer (University of Innsbruck)
Julian Nagele (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tools:
CSI^ho HRS Julian Nagele (University of Innsbruck) paper slides tool
FORT GCR/UNC/UNR/NFP Franziska Rapp (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tool
SOL HRS Makoto Hamana (Gunma University)
Tatsuya Abe (Chiba Institute of Technology)
Yuito Murase (University of Tokyo)
Kazuhiko Sakaguchi (University of Tsukuba)
paper slides tool

Organising Committee