fof(trivial,conjecture,fx=fx).
------------------
fof(irrelevant,conjecture,fz=fz).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(alsotrivial,conjecture,fy=fy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(alsotrivial,conjecture,fy=fy).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(alsotrivial,conjecture,fy=fy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
fof(alsotrivial1,axiom,fy=fy).
------------------
fof(trivial_biconditionals,conjecture,fy=fy).
fof(alsotrivial,axiom,![Xy]:Xy=Xy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(trivial_biconditionals,conjecture,fy=fy).
fof(trivial,axiom,![Xx]:Xx=Xx).
------------------
fof(trivial_biconditionals,conjecture,fy=fy).
fof(alsotrivial,axiom,![Xy]:Xy=Xy).
fof(irrelevant,axiom,![Xz]:Xz=Xz).
fof(trivial,axiom,![Xx]:Xx=Xx).
fof(trivial_biconditionals1,axiom,fy=fy<=>fy=fy).