In[]:=
ParallelEvaluate[1]
Out[]=
{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1}
In[]:=
FindMinPathsX[ru_,init_,maxlen_]:=ResourceFunction["ParallelMapMonitored"][If[Head[#]===Failure,Infinity,Length[#]]&[FindStringReplacePath[ru,init,#]]&,Catenate[Table[ResourceFunction["StringTuples"]["AB",i],{i,maxlen}]]]
In[]:=
EnumerateRuleSignatures[3]
Out[]=
{{12}}
In[]:=
EnumerateRuleSignatures[6]
Out[]=
{{11,11,11},{11,22},{12,12},{22,11},{33},{11,13},{13,11},{24},{15}}
In[]:=
EnumerateRuleSignatures[7,1]
Out[]=
{{12,22},{22,12},{11,11,12},{11,12,11},{12,11,11},{11,23},{12,13},{13,12},{23,11},{11,14},{14,11},{16}}
In[]:=
#->FindMinPaths[#,"A",5]&/@ResourceFunction["EnumerateSubstitutionSystemRules"][{12},2]
Out[]=
{{AAA}{∞,∞,2,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞},{AAB}{∞,∞,∞,2,∞,∞,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞},{ABB}{∞,∞,∞,∞,∞,2,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞}}
In[]:=
Directory[]
Out[]=
/Users/sw
In[]:=
SetDirectory["/Users/sw/Dropbox/Physics/Data/Metamathematics/ProofLengths"]
Out[]=
/Users/sw/Dropbox/Physics/Data/Metamathematics/ProofLengths
In[]:=
doall[n_]:=Export["A-"<>ToString[n]<>".wxf",((#->FindMinPathsX[#,"A",5])&/@ResourceFunction["EnumerateSubstitutionSystemRules"][#,2])&/@EnumerateRuleSignatures[n,1]]
In[]:=
doall[1]
Out[]=
A-1.wxf
In[]:=
doall[3]
Out[]=
A-3.wxf
In[]:=
Now
Out[]=
Sun 23 Aug 2020 01:23:29GMT-4.
In[]:=
doall[4]
Out[]=
A-4.wxf
In[]:=
Now
Out[]=
Sun 23 Aug 2020 01:23:59GMT-4.
In[]:=
doall[5]
Out[]=
A-5.wxf
In[]:=
Now
Out[]=
Sun 23 Aug 2020 01:25:23GMT-4.
In[]:=
doall[6]
Out[]=
A-6.wxf
In[]:=
Now
Out[]=
Sun 23 Aug 2020 01:34:42GMT-4.
In[]:=
doall[7]
Out[]=
A-7.wxf
In[]:=
Now
Out[]=
Sun 23 Aug 2020 02:30:22GMT-4.
In[]:=
doall[8]
[[[ overnight run timed out ]]]
Now
doall[9]
Now
In[]:=
EnumerateRuleSignatures[9]
Out[]=
{{11,12,22},{11,22,12},{12,11,22},{12,12,12},{12,22,11},{22,11,12},{22,12,11},{11,11,11,12},{11,11,12,11},{11,12,11,11},{12,11,11,11},{12,33},{13,23},{22,23},{23,13},{23,22},{33,12},{11,11,23},{11,12,13},{11,13,12},{11,23,11},{12,11,13},{12,13,11},{13,11,12},{13,12,11},{23,11,11},{11,34},{12,24},{13,14},{14,13},{14,22},{22,14},{24,12},{34,11},{11,11,14},{11,14,11},{14,11,11},{45},{11,25},{12,15},{15,12},{25,11},{36},{11,16},{16,11},{27},{18}}
​
doallABB[n_]:=Export["ABB-"<>ToString[n]<>".wxf",((#->FindMinPathsX[#,"ABB",5])&/@ResourceFunction["EnumerateSubstitutionSystemRules"][#,2])&/@EnumerateRuleSignatures[n,3]]
doallABB[1]
Out[]=
A-1.wxf
doallABB[3]
In[]:=
Now
Out[]=
Sun 23 Aug 2020 01:13:17GMT-4.
doallABB[4]
Out[]=
4.wxf
In[]:=
Now
Out[]=
Sun 23 Aug 2020 01:14:16GMT-4.
doallABB[5]
Now
doallABB[6]
Now
doallABB[7]
Now
doallABB[8]
Now
doallABB[9]
Now