fof(prop1,conjecture,fa=fa).
------------------
fof(prop2,conjecture,fb=fb).
fof(prop1,axiom,![Xa]:Xa=Xa).
------------------
fof(prop3,conjecture,fc=fc).
fof(prop1,axiom,![Xa]:Xa=Xa).
------------------
fof(prop4,conjecture,![Xd]:Xd=Xd).
fof(prop1,axiom,![Xa]:Xa=Xa).
------------------
fof(prop4,conjecture,fe=fe).
fof(prop3,axiom,![Xc]:Xc=Xc).
fof(prop2,axiom,![Xb]:Xb=Xb).
fof(prop1,axiom,![Xa]:Xa=Xa).
fof(prop41,axiom,![Xd]:Xd=Xd).
------------------
fof(prop5,conjecture,ff=ff).
fof(prop4,axiom,![Xe]:Xe=Xe).
fof(prop3,axiom,![Xc]:Xc=Xc).
fof(prop2,axiom,![Xb]:Xb=Xb).
fof(prop1,axiom,![Xa]:Xa=Xa).