In[]:=
ggg=Last@TwoWayMultiReplaceGraphList[AxiomaticTheoryTWP[AxiomaticTheory["WolframAxioms"]],2,"MaxLeafCount"->119,"MaxDepth"->14,"Deduplicate"->True,"SubstitutionLemmas"->True,"CoSubstitutionLemmas"->False]
Out[]=
In[]:=
VertexList[%]
Out[]=
{((b_·c_)·a_)·(b_·((b_·a_)·b_))a_,a_a_,(((((b_·c_)·b_)·(b_·((b_·b_)·b_)))·c_)·a_)·(b_·((b_·a_)·b_))a_,
⋯1100⋯
,((b_·c_)·a_)·(b_·((b_·(((b_·c_)·(((b_·c_)·a_)·(b_·((b_·a_)·b_))))·(b_·((b_·a_)·b_))))·b_))a_,((b_·c_)·a_)·(b_·((b_·(((b_·c_)·a_)·((((b_·c_)·b_)·(b_·((b_·b_)·b_)))·((b_·a_)·b_))))·b_))a_}
large output
show less
show more
show all
set size limit...
In[]:=
booleanCombinations=Map[Apply[Verbatim[Pattern][Symbol[#1],_]->#2&]]/@Tuples[Thread[{#,{True,False}}]&/@Alphabet[][[;;7]]];
In[]:=
And@@AllTrue[booleanCombinations,SortBy[VertexList@ggg,LeafCount]/.{CenterDot->Nand,TwoWayRule->Equal,Splice@#}&][[1]]
Out[]=
True