fof( coprod_comm, axiom, ![X,Y] : coprod(X,Y) = coprod(Y,X) ).
fof( coprod_assoc, axiom, ![X,Y,Z] : coprod(X,coprod(Y,Z)) = coprod(coprod(X,Y),Z) ).
fof( prod_comm, axiom, ![X,Y] : prod(X,Y) = prod(Y,X) ).
fof( prod_assoc, axiom, ![X,Y,Z] : prod(X,prod(Y,Z)) = prod(prod(X,Y),Z) ).
fof( dist, axiom, ![X,Y,Z] : prod(X,coprod(Y,Z)) = coprod(prod(X,Y),prod(X,Z)) ).
fof( prod_unit, axiom, ![X] : prod(one, X) = X ).
fof( t, axiom, t = coprod(one, prod(t, t)) ).

fof( seven_trees, conjecture, t = prod(t,prod(t,prod(t,prod(t,prod(t,prod(t,t)))))) ).