In[]:=
ptms=Sort/@DeleteCasesReleaseHold/@CanonicalizeSymbols/@ResourceFunction["UnformalizeSymbols"]NormalValuesProofObject
Logic: EquationalLogic
Steps: 104
Theorem: p·qq·p
["ProofDataset"][All,1],True
Out[]=
In[]:=
ParallelMap[Length[ResourceFunction["FindFiniteModels"][#,2,Method->"BruteForce"]]&,ptms]
Out[]=
{2,8,6,2,4,8,2,2,2,2,2,2,2,6,6,8,8,10,6,10,10,10,7,10,7,2,8,12,13,13,12,11,16,11,11,11,13,14,13,8,12,9,10,8,8,7,10,8,12,7,13,12,9,11,12,13,13,8,13,13,13,13,10,7,8,5,16,5,9,4,6,12,8,4,10,8,13,6,4,6,9,11,16,14,14,13,11,11,10,10,5,10,10,8,8,6,6,9,10,6,8,9,8}
In[]:=
ResourceFunction["FindFiniteModels"][a((b·c)·a)·(b·((b·a)·b)),2,Method->"BruteForce"]
Out[]=
{8}CenterDot{{1,0},{0,0}},{14}CenterDot{{1,1},{1,0}}
In[]:=
ResourceFunction["FindFiniteModels"][a·bb·a,2,Method->"BruteForce"]
Out[]=
{0}CenterDot{{0,0},{0,0}},{1}CenterDot{{0,0},{0,1}},{6}CenterDot{{0,1},{1,0}},{7}CenterDot{{0,1},{1,1}},{8}CenterDot{{1,0},{0,0}},{9}CenterDot{{1,0},{0,1}},{14}CenterDot{{1,1},{1,0}},{15}CenterDot{{1,1},{1,1}}
In[]:=
Take[SortBy[%229,LeafCount],10]
Out[]=
{a·bb·a,a·bb·a,a(a·a)·(a·a),a(a·b)·(a·(a·b)),a(a·b)·((a·b)·a),a((a·b)·a)·(a·a),a((a·b)·a)·(a·b),a·aa·(a·(a·a)),a·aa·((a·a)·a),a·aa·((a·a)·a)}
In[]:=
ParallelMapResourceFunction["FindFiniteModels"][#,2,Method->"BruteForce"]&,

Out[]=
In[]:=
Length/@%
Out[]=
{8,8,8,6,10,5,5,16,13,13}
In[]:=
ResourceFunction["FindFiniteModels"][(a·((a·c)·a))·(c·((c·(((a·b)·c)·(c·((a·b)·c))))·c))((a·b)·c)·(c·((a·b)·c)),2,Method->"BruteForce"]
Out[]=
{0}CenterDot{{0,0},{0,0}},{1}CenterDot{{0,0},{0,1}},{3}CenterDot{{0,0},{1,1}},{4}CenterDot{{0,1},{0,0}},{5}CenterDot{{0,1},{0,1}},{7}CenterDot{{0,1},{1,1}},{8}CenterDot{{1,0},{0,0}},{10}CenterDot{{1,0},{1,0}},{13}CenterDot{{1,1},{0,1}},{14}CenterDot{{1,1},{1,0}},{15}CenterDot{{1,1},{1,1}}
(a·((a·c)·a))·(c·((c·(((a·b)·c)·(c·((a·b)·c))))·c))((a·b)·c)·(c·((a·b)·c))
In[]:=
ProofObject
Logic: EquationalLogic
Steps: 104
Theorem: p·qq·p
["TokenEventProofGraph","TokenLabeling"->False,AspectRatio->1.5]
Out[]=
In[]:=
NormalValuesProofObject
Logic: EquationalLogic
Steps: 104
Theorem: p·qq·p
["ProofDataset"][All,1]
Out[]=
In[]:=
ParallelMapLength[ResourceFunction["FindFiniteModels"][ReleaseHold[#],2,Method->"BruteForce"]]&,

Out[]=
{2,8,6,2,4,8,2,2,2,2,2,2,2,6,6,8,8,10,6,10,10,10,7,10,7,2,8,12,13,13,12,11,16,11,11,11,13,14,13,8,12,9,10,8,8,7,10,8,12,7,13,12,9,11,12,13,13,8,13,13,13,13,10,7,8,5,16,5,9,4,6,12,8,4,10,8,13,6,4,6,9,11,16,14,14,13,11,11,10,10,5,10,10,8,8,6,6,9,10,6,8,9,8,0}
In[]:=
Graph
,VertexLabels->Thread
->

Out[]=
In[]:=
Graph
,VertexSize->Thread
->.5

Out[]=

Popular Lemmas