set(prolog_style_variables).

formulas(assumptions).
(all X all Y coprod(X,Y) = coprod(Y,X)).
(all X all Y all Z coprod(X,coprod(Y,Z)) = coprod(coprod(X,Y),Z)).
t1 = coprod(t0,t2).
t2 = coprod(t1,t3).
t3 = coprod(t2,t4).
t4 = coprod(t3,t5).
t5 = coprod(t4,t6).
t6 = coprod(t5,t7).
t7 = coprod(t6,t8).
t8 = coprod(t7,t9).
end_of_list.

formulas(goals).
t1 = t7.
end_of_list.
