In[]:=
FindEquationalProof[Exists[x,Mortal[x]],{ForAll[x,Implies[Man[x],Mortal[x]]],Exists[x,Man[x]]}]["ProofGraph"]
Out[]=
In[]:=
AxiomaticTheory["ShefferAxioms"]
Out[]=

∀
a.
(a.·a.)·(a.·a.)a.,
∀
{a.,b.}
a.·(b.·(b.·b.))a.·a.,
∀
{a.,b.,c.}
(a.·(b.·c.))·(a.·(b.·c.))((b.·b.)·a.)·((c.·c.)·a.)
In[]:=
FindEquationalProof[Exists[x,x⇔x·(x·x)],{​​(*ForAll[{a,b,c},a·(b·c)⇔(a·b)·c],​​ForAll[{a,b},a·b⇔b·a],*)​​Exists[{true,false},​​false·false⇔true],​​Exists[{true,false},​​false·true⇔true],​​Exists[{true,false},​​true·false⇔true],​​Exists[{true,false},​​true·true⇔false]​​​​(*&&false·true⇔true&&true·false⇔true&&true·true⇔false*)}]
Out[]=
$Aborted