In[]:=
ParallelMap[Normal[Values[KeySelect[FindEquationalProof[#,"BooleanAxioms"]["ProofDataset"],First[#]==="Axiom"&][All,"Statement"]]]&,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)]
Out[]=
{{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3)},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3)},{x1x1⊕x2⊗
x2
,x1⊕x2x2⊕x1,x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1⊗x2x2⊗x1,x1⊕x2x2⊕x1},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3,x1⊕x2x2⊕x1},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3),x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3,x1⊕x2x2⊕x1},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3),x1⊗x2x2⊗x1},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3),x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3,x1⊕x2x2⊕x1}}
In[]:=
Length/@%
Out[]=
{3,3,6,3,3,6,6,6,6,6,6}
In[]:=
Length[%]
Out[]=
11
In[]:=
Counts[%148]
Out[]=
34,67
In[]:=
7/11.
Out[]=
0.636364
In[]:=
Select[{{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3)},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3)},{x1x1⊕x2⊗
x2
,x1⊕x2x2⊕x1,x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1⊗x2x2⊗x1,x1⊕x2x2⊕x1},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3,x1⊕x2x2⊕x1},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3),x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3,x1⊕x2x2⊕x1},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3),x1⊗x2x2⊗x1},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊕x2⊗x3(x1⊕x2)⊗(x1⊕x3),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3),x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,x1⊗x2x2⊗x1,x1⊗(x2⊕x3)x1⊗x2⊕x1⊗x3,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3,x1⊕x2x2⊕x1}},Length[#]==3&]
Out[]=
{{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3)},{x1x1⊗(x2⊕
x2
),x1x1⊕x2⊗
x2
,(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3},{x1x1⊕x2⊗
x2
,x1⊕x2x2⊕x1,x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1⊗x2x2⊗x1,x1⊕x2x2⊕x1}}
In[]:=
Sort/@%
Out[]=
{{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),x1⊗x2⊕x1⊗x3x1⊗(x2⊕x3)},{x1x1⊕x2⊗
x2
,x1x1⊗(x2⊕
x2
),(x1⊕x2)⊗(x1⊕x3)x1⊕x2⊗x3},{x1x1⊕x2⊗
x2
,x1⊕x2x2⊕x1,x1⊗x2x2⊗x1},{x1x1⊗(x2⊕
x2
),x1⊕x2x2⊕x1,x1⊗x2x2⊗x1}}
In[]:=
255./465
Out[]=
0.548387