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)).
(all X all Y prod(X,Y) = prod(Y,X)).
(all X all Y all Z prod(X,prod(Y,Z)) = prod(prod(X,Y),Z)).
(all X all Y all Z prod(X,coprod(Y,Z)) = coprod(prod(X,Y),prod(X,Z))).
(all X prod(one,X) = X).
t = coprod(one,prod(t,t)).
end_of_list.

formulas(goals).
t = prod(t,prod(t,prod(t,prod(t,prod(t,prod(t,t)))))).
end_of_list.
