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.·(b.·(b.·b.))a.·a.,(a.·(b.·c.))·(a.·(b.·c.))((b.·b.)·a.)·((c.·c.)·a.)
∀
a.
∀
{a.,b.}
∀
{a.,b.,c.}
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