In[]:=
Take[stmts,4]
Out[]=
wphvhyp[wph,{wff,ph}],wpsvhyp[wps,{wff,ps}],wchvhyp[wch,{wff,ch}],wthvhyp[wth,{wff,th}]
In[]:=
Count[stmts,_thm]
Out[]=
38840
In[]:=
Length[stmts]
Out[]=
87335
In[]:=
Counts[Head/@stmts]
Out[]=
vhyp353,hyp48142,thm38840
In[]:=
Count[stmts,thm[_,_,_]]
Out[]=
2559
In[]:=
Take[Cases[stmts,thm[_,_,_]],10]
Out[]=
{thm[wn,{wff,-.,ph},{{},{vhyp[wph,{wff,ph}]},{}}],thm[wi,{wff,(,ph,->,ps,)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}],thm[ax-mp,{|-,ps},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{hyp[min,{|-,ph}],hyp[maj,{|-,(,ph,->,ps,)}]}}],thm[ax-1,{|-,(,ph,->,(,ps,->,ph,),)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}],thm[ax-2,{|-,(,(,ph,->,(,ps,->,ch,),),->,(,(,ph,->,ps,),->,(,ph,->,ch,),),)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}],vhyp[wch,{wff,ch}]},{}}],thm[ax-3,{|-,(,(,-.,ph,->,-.,ps,),->,(,ps,->,ph,),)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}],thm[wb,{wff,(,ph,<->,ps,)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}],thm[df-bi,{|-,-.,(,(,(,ph,<->,ps,),->,-.,(,(,ph,->,ps,),->,-.,(,ps,->,ph,),),),->,-.,(,-.,(,(,ph,->,ps,),->,-.,(,ps,->,ph,),),->,(,ph,<->,ps,),),)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}],thm[wo,{wff,(,ph,\/,ps,)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}],thm[wa,{wff,(,ph,/\,ps,)},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}]},{}}]}
In[]:=
Take[Cases[stmts,thm[_,_,_,_]],10]
Out[]=
In[]:=
Subgraph[proofGraph,VertexOutComponent[proofGraph,"wn",1],GraphLayout->"SpringElectricalEmbedding",PlotTheme->"Monochrome",ImageSizeLarge]Subgraph[labeledProofGraph,VertexOutComponent[proofGraph,"2p2e4",1],GraphLayout->"SpringElectricalEmbedding",PlotTheme->"Monochrome",ImageSizeLarge]
Out[]=
Out[]=
$Aborted
In[]:=
Take[VertexList[labeledProofGraph],5]
Out[]=
{dummylink,dummylink.1,idi,idi.1,mp2}
In[]:=
stmts["mp2"]
Out[]=
thm[mp2,{|-,ch},{{},{vhyp[wph,{wff,ph}],vhyp[wps,{wff,ps}],vhyp[wch,{wff,ch}]},{hyp[mp2.1,{|-,ph}],hyp[mp2.2,{|-,ps}],hyp[mp2.3,{|-,(,ph,->,(,ps,->,ch,),)}]}},proof[{{wps,{wff,ps}},{wch,{wff,ch}},{mp2.2,{|-,ps}},{wph,{wff,ph}},{wps,{wff,ps}},{wch,{wff,ch}},{wi,{wff,(,ps,->,ch,)}},{mp2.1,{|-,ph}},{mp2.3,{|-,(,ph,->,(,ps,->,ch,),)}},{ax-mp,{|-,(,ps,->,ch,)}},{ax-mp,{|-,ch}}}]]
In[]:=
Subgraph[proofGraph,VertexOutComponent[proofGraph,"2p2e4",2],GraphLayout->"SpringElectricalEmbedding",PlotTheme->"Monochrome",ImageSizeLarge]
Out[]=
In[]:=
Subgraph[proofGraph,VertexOutComponent[proofGraph,"2p2e4",2],VertexLabelsNone,EdgeLabelsNone,GraphLayout"SpringElectricalEmbedding"]
Out[]=
In[]:=
Subgraph[proofGraph,VertexOutComponent[proofGraph,"2p2e4",3],VertexLabelsNone,EdgeLabelsNone,GraphLayout"SpringElectricalEmbedding"]
Out[]=