Remark: all examples can be browsed directly at github.
The two examples from the Applications section are available here:
The following two files use the congruence closure procedure to discharge goals in Group theory and Lists.
The following list contains small files used to test the congruence closure procedure.