fof( comm, axiom, ![X,Y] : coprod(X,Y) = coprod(Y,X) ).
fof( assoc, axiom, ![X,Y,Z] : coprod(X,coprod(Y,Z)) = coprod(coprod(X,Y),Z) ).
fof( t1, axiom, t1 = coprod(t0, t2) ).
fof( t2, axiom, t2 = coprod(t1, t3) ).
fof( t3, axiom, t3 = coprod(t2, t4) ).
fof( t4, axiom, t4 = coprod(t3, t5) ).
fof( t5, axiom, t5 = coprod(t4, t6) ).
fof( t6, axiom, t6 = coprod(t5, t7) ).
fof( t7, axiom, t7 = coprod(t6, t8) ).
fof( t8, axiom, t8 = coprod(t7, t9) ).

fof( seven_trees, conjecture, t1 = t7 ).