In[]:=
proofE=
;
In[]:=
proofTwee=
;
In[]:=
proofVampire=
;
In[]:=
proofWaldmeister=
;
In[]:=
proofTwee
Out[]=
{cnf[c1,negated_conjecture,nand[a,b]≠nand[b,a],Axiom[commutativity]],cnf[c2,axiom,nand[nand[nand[A,B],C],nand[A,nand[nand[A,C],A]]]C,Axiom[wolfram]],
⋯299⋯
,cnf[c302,plain,nand[b,a]nand[a,b],Inference[substitution,{Lemma[c301]}]],cnf[c303,plain,$false,Inference[resolution,{Lemma[c1],Lemma[c302]}]]}
Full expression not available
(
original memory size:
0.8 MB)
In[]:=
%[[All,3]]
Out[]=
{nand[a,b]≠nand[b,a],nand[nand[nand[A,B],C],nand[A,nand[nand[A,C],A]]]C,nand[nand[nand[A2,B2],C2],nand[A2,nand[nand[A2,C2],A2]]]C2,nand[nand[nand[A2,B2],C2],nand[A2,nand[nand[A2,C2],A2]]]C2,
⋯295⋯
,nand[X,nand[nand[X,X2],X]]nand[X,X2],nand[X2,X]nand[X,X2],nand[b,a]nand[a,b],$false}
Full expression not available
(
original memory size:
0.6 MB)
LeafCount/@%
Out[]=
{7,15,15,15,15,15,25,69,19,35,59,39,23,53,31,31,59,15,51,35,15,27,39,59,15,19,59,37,25,43,31,31,19,35,21,17,33,49,77,25,29,57,41,19,53,39,27,101,85,23,27,79,15,19,23,27,47,47,51,71,75,95,55,43,31,19,43,39,57,43,139,39,59,47,67,43,39,35,55,75,91,51,37,57,85,19,23,11,15,39,71,23,27,31,35,59,71,75,99,115,139,81,61,41,21,63,27,27,19,23,27,31,23,15,19,23,15,11,15,11,19,27,35,47,51,23,31,39,51,27,35,43,55,55,41,29,41,15,33,29,29,29,25,69,19,27,35,39,29,25,21,25,29,37,19,27,13,9,27,45,17,29,33,53,41,15,23,31,25,53,57,61,65,101,105,109,149,153,101,79,57,35,59,35,39,43,63,29,11,19,17,21,37,17,29,25,11,41,27,13,9,9,17,25,41,21,25,29,37,41,27,13,27,21,15,15,19,23,43,19,27,39,23,11,19,11,23,19,11,19,27,35,11,15,23,31,39,47,19,47,39,23,35,31,27,19,11,11,15,31,31,43,55,19,27,39,51,63,75,59,19,43,35,23,11,19,23,39,27,19,11,11,15,19,23,39,43,15,19,35,39,35,39,31,35,15,19,23,23,23,27,11,11,23,27,15,19,15,19,11,7,7,1}
In[]:=
ListStepPlot[%318]
Out[]=
In[]:=
LeafCount[f[a,b]]
Out[]=
3
In[]:=
proofE=
;
In[]:=
proofTwee=
;
In[]:=
proofVampire=
;
In[]:=
proofWaldmeister=
;
In[]:=
proofDependencies//Clear​​proofDependencies[proof_,inftype_]:=Replace[​​proof,​​{​​"Inference"[type_,deps_List,___]:>type[Unique[]]->Map[proofDependencies[#,inftype]&,deps],​​("Axiom"|"Plain")[name_]:>Replace[inftype,{"axiom"->"Axiom","negated_conjecture"->"Hypothesis"}][name],​​"Lemma"[name_]:>name,​​"Theory"[_]:>Nothing,​​name_:>name​​}​​]
In[]:=
TPTPProofGraph[proofExpr_,mult_:1,opts___]:=With{formulas=Association@Cases[proofExpr,_[name_,_,formula_,___]:>name->(formula/.{"nand"->CenterDot,"$false"->False,"X1"->"a","X2"->"b","X3"->"c","X4"->"d"})]},WeaklyConnectedGraphComponentsGraphUnion##,​​opts,VertexShapeFunction->FunctionInsetReplace#2,lemma:x_[_]:>ClickToCopyFramedStyle[x,Black],Background->
[◼]
MetamathematicsStyleData
["SubstitutionColor"],RoundingRadius->5,lemma,x_:>FramedTooltip[Style[x,Black,8],Lookup[formulas,x,None]],Background->
[◼]
MetamathematicsStyleData
["TokenStyle"],FrameStyle->Black,FrameMargins->Tiny,#1,#3,​​VertexStyle->_->
[◼]
MetamathematicsStyleData
["TokenStyle"],_[_]->
[◼]
MetamathematicsStyleData
["SubstitutionStyle"],​​VertexLabels->{x_:>Placed[Replace[Lookup[formulas,x],_Missing->x],Tooltip]},VertexSize->{_[_]mult1,r_:>mult.5Sqrt@LeafCount[formulas[r]]},​​EdgeStyle->
[◼]
MetamathematicsStyleData
["TokenEventEdgeStyle"],​​GraphLayout->{"LayeredDigraphEmbedding","Orientation"->"Top"},PerformanceGoal->"Quality",AspectRatio->3&@@Cases[proofExpr,_[name_,type_,formula_,proof_,___]:>VertexReplace[ReverseGraph[TreeGraph@RulesTree[name->{proofDependencies[proof,type]}]],​​{x_,_}:>x​​]]​​[[1]]​​
In[]:=
TPTPProofGraph[proofVampire,2.5,VertexShapeFunction->Automatic]
Out[]=
In[]:=
TPTPProofGraph[proofTwee,1,VertexShapeFunction->Automatic]
Out[]=