ParallelEvaluate[1]
In[]:=
{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}
Out[]=
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]
In[]:=
{{12}}
Out[]=
EnumerateRuleSignatures[6]
In[]:=
{{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}}
Out[]=
EnumerateRuleSignatures[7,1]
In[]:=
{{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}}
Out[]=
#->FindMinPaths[#,"A",5]&/@ResourceFunction["EnumerateSubstitutionSystemRules"][{12},2]
In[]:=
{{AAA}{∞,∞,2,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞},{AAB}{∞,∞,∞,2,∞,∞,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞},{ABB}{∞,∞,∞,∞,∞,2,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞}}
Out[]=
Directory[]
In[]:=
/Users/sw
Out[]=
SetDirectory["/Users/sw/Dropbox/Physics/Data/Metamathematics/ProofLengths"]
In[]:=
/Users/sw/Dropbox/Physics/Data/Metamathematics/ProofLengths
Out[]=
doall[n_]:=Export["A-"<>ToString[n]<>".wxf",((#->FindMinPathsX[#,"A",5])&/@ResourceFunction["EnumerateSubstitutionSystemRules"][#,2])&/@EnumerateRuleSignatures[n,1]]
In[]:=
doall[1]
In[]:=
A-1.wxf
Out[]=
doall[3]
In[]:=
A-3.wxf
Out[]=
Now
In[]:=
Sun 23 Aug 2020 01:23:29GMT-4.
Out[]=
doall[4]
In[]:=
A-4.wxf
Out[]=
Now
In[]:=
Sun 23 Aug 2020 01:23:59GMT-4.
Out[]=
doall[5]
In[]:=
A-5.wxf
Out[]=
Now
In[]:=
Sun 23 Aug 2020 01:25:23GMT-4.
Out[]=
doall[6]
In[]:=
A-6.wxf
Out[]=
Now
In[]:=
Sun 23 Aug 2020 01:34:42GMT-4.
Out[]=
doall[7]
In[]:=
A-7.wxf
Out[]=
Now
In[]:=
Sun 23 Aug 2020 02:30:22GMT-4.
Out[]=
doall[8]
In[]:=
[[[ overnight run timed out ]]]
Now
doall[9]
Now
EnumerateRuleSignatures[9]
In[]:=
{{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}}
Out[]=
​
doallABB[n_]:=Export["ABB-"<>ToString[n]<>".wxf",((#->FindMinPathsX[#,"ABB",5])&/@ResourceFunction["EnumerateSubstitutionSystemRules"][#,2])&/@EnumerateRuleSignatures[n,3]]
doallABB[1]
A-1.wxf
Out[]=
doallABB[3]
Now
In[]:=
Sun 23 Aug 2020 01:13:17GMT-4.
Out[]=
doallABB[4]
4.wxf
Out[]=
Now
In[]:=
Sun 23 Aug 2020 01:14:16GMT-4.
Out[]=
doallABB[5]
Now
doallABB[6]
Now
doallABB[7]
Now
doallABB[8]
Now
doallABB[9]
Now