begin_problem(null).

list_of_descriptions.
name({*null*}).
author({*null*}).
status(unknown).
description({*null*}).
date({*null*}).
end_of_list.

list_of_symbols.
functions[(d,2),(s,2),(p,2),(q,1),(a,0),(b,0)].
% functions[(d,d,false,0),(s,s,false,0),(p,p,false,0),(q,q,false,0),(a,a,false,0),(b,b,false,0)].
end_of_list.

list_of_formulae(axioms).
formula(forall([x],forall([y],and(equal(s(x,y),s(y,x)),equal(p(x,y),p(y,x)))))). % name({*commutativa*})
formula(forall([x],forall([y],forall([z],equal(p(x,s(y,z)),s(p(x,y),p(x,z))))))). % name({*distributiva*})
formula(forall([x],equal(p(x,x),q(x)))). % name({*quadrato*})
formula(forall([x],forall([y],forall([z],and(equal(s(x,s(y,z)),s(s(x,y),z)),equal(p(x,p(y,z)),p(p(x,y),z))))))). % name({*associativa*})
formula(forall([x],forall([y],forall([z],and(equal(d(x,y),d(s(x,z),s(y,z))),equal(d(x,y),d(d(x,z),d(y,z)))))))). % name({*invariantiva*})
formula(forall([x],forall([y],not(equal(d(x,y),d(y,x)))))). % name({*differenza_non_commutativa*})
end_of_list.

list_of_formulae(conjectures).
formula(equal(d(a,b),d(b,a))). % name({*sol*})
end_of_list.

list_of_settings(SPASS).
{*
set_precedence(p,q,s,d).
*}
end_of_list.

end_problem.