In[]:=
polist=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕a,a
a
,
a
⊗a
b
⊗b,
a
⊕a
b
⊕b,
a⊕b

a
⊗
b
,
a⊗b

a
⊕
b
,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)];
In[]:=
pounion=GraphUnion@@(removeEvents/@polist);
In[]:=
GraphUnion[pounion,VertexLabels->(#->If[!FreeQ[#,a],#,None]&/@VertexList[pounion]),VertexSize->#->If[!FreeQ[#,a|a.],1.5,0.8]&/@VertexList[pounion],EdgeStyle->Opacity[.2],VertexStyle->{_List->Orange},GraphLayout"LayeredDigraphEmbedding",AspectRatio.7]
Out[]=
In[]:=
polist=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕a,a
a
,
a
⊗a
b
⊗b,
a
⊕a
b
⊕b,
a⊕b

a
⊗
b
,
a⊗b

a
⊕
b
,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)];
In[]:=
pounion=GraphUnion@@(VertexReplace[#,{"Event",__}:>{"Event",CreateUUID[]}]&/@polist);
In[]:=
GraphUnion[pounion,VertexLabels->(#->If[!FreeQ[#,a],#,None]&/@VertexList[pounion]),VertexSize->#->If[!FreeQ[#,a|a.],1.5,0.8]&/@VertexList[pounion],EdgeStyle->Opacity[.2],VertexStyle->{_List->Orange},GraphLayout"LayeredDigraphEmbedding",AspectRatio.7]
Out[]=

With Background Theorems

ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕a,a
a
,
a
⊗a
b
⊗b,
a
⊕a
b
⊕b,
a⊕b

a
⊗
b
,
a⊗b

a
⊕
b
,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)]
In[]:=
CloudGet["https://wolfr.am/PO7vasDF"];
In[]:=
Take[data53,40]/.{Vee->CirclePlus,Wedge->CircleTimes,Square->OverBar}
Out[]=
aa⊗a,aa⊕a,a⊗aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a
a
,a⊗a
a
,a⊕a
a
,
a
⊗aa⊗
a
,
a
⊕aa⊕
a
,
a

a⊗a
,
a

a⊕a
,
a⊗a

a⊕a
,a⊗
b

b
⊗a,
a
⊗bb⊗
a
,a⊕
b

b
⊕a,
a
⊕bb⊕
a
,
a⊗b

b⊗a
,
a⊕b

b⊕a
,
a
⊗a
b
⊗b,a⊗
a

b
⊗b,
a
⊗ab⊗
b
,a⊗
a
b⊗
b
,
a
⊕a
b
⊕b,a⊕
a

b
⊕b,
a
⊕ab⊕
b
,a⊕
a
b⊕
b
,
a

a
⊗
a
,
a⊗a

a
⊗
a
,
a⊕a

a
⊗
a
,
a

a
⊕
a
,
a⊗a

a
⊕
a
,
a⊕a

a
⊕
a
,
a
⊗
a

a
⊕
a
,
a⊕b

a
⊗
b
,
a⊗b

a
⊕
b
,
a⊕b

b
⊗
a
,
a
⊗
b

b
⊗
a
,
a⊗b

b
⊕
a
,
a
⊕
b

b
⊕
a

In[]:=
background=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,data53/.{Vee->CirclePlus,Wedge->CircleTimes,Square->OverBar}];
In[]:=
GraphUnion@@(removeEvents/@background)
Out[]=
In[]:=
polist=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕a,a
a
,
a
⊗a
b
⊗b,
a
⊕a
b
⊕b,
a⊕b

a
⊗
b
,
a⊗b

a
⊕
b
,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)];
In[]:=
pounion=GraphUnion@@(removeEvents/@polist);
In[]:=
Graph[GraphUnion@@Join[(removeEvents/@polist),(removeEvents/@background)],VertexStyle->Thread[aa⊗a,aa⊕a,a
a
,
a
⊗a
b
⊗b,
a
⊕a
b
⊕b,
a⊕b

a
⊗
b
,
a⊗b

a
⊕
b
,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)->Red]]
Out[]=
The “eyes” are probably commutativity....