set(print_models_portable).
assign(iterate_up_to, 7).

clauses(theory).

d(d(d(y,y),d(d(w,x),z)),d(x,w)) = z.  % candidate 8

d(x,x) = 0.    % additional constraint.

d(X,d(d(d(d(X,X),Y),Z),d(d(d(X,X),X),Z)))!=Y.  % denial of GT single axiom

end_of_list.