Confluence Competition

Categories – TRS

This is the oldest CoCo category. It is concerned with confluence of first-order rewrite systems.


The input is a first-order rewrite system without conditions, specified in the ARI TRS format. The question to be answered is whether the rewrite system is confluent.


  1. (format TRS)
    (fun a 0)
    (fun b 0)
    (fun f 1)
    (rule (f a) b)
    (rule (f (f x)) a)
    The correct answer is NO.
  2. (format TRS)
    (fun Ap 2)
    (fun I 0)
    (fun K 0)
    (fun S 0)
    (rule (Ap (Ap (Ap S x) y) z) (Ap (Ap x z) (Ap y z)))
    (rule (Ap (Ap K x) y) x)
    (rule (Ap I x) x)
    The correct answer is YES.

Problem Selection

Problems are selected from those in the ARI database with the 'trs' tag.