new strategies for ShHydraTf0Schedule (also, get rid of the buggy fmb…

… strat)

CASC/Schedules.cpp

@@ -2848,12 +2848,18 @@ void Schedules::getShHydraFolSchedule(const Shell::Property& property, Schedule&
 
 void Schedules::getShHydraTf0Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback)
 {
+  quick.push("ins+3_1124:43003_bsr=on:fmbas=expand:igrp=1158:fde=unused:etr=on:igrpq=1.9816:sp=reverse_frequency:sos=theory:erd=off:lma=on:spb=goal_then_units:drc=off:bce=on:fmbss=6:awrs=converge:fd=preordered:awrsf=2:nwc=2:fmbsso=preprocessed_usage:newcnf=on:cond=fast:igwr=on:fmbsr=1.22306:lcm=predicate:s2a=on:igrr=1196348/477791:bs=unit_only:s2at=3.05532:dr=on:fmbswo=argument_first:fsd=on:bd=off:nm=2:av=off:rnwc=on:igs=4:sfv=off:fsdmm=3_50");
+  quick.push("lrs+0_2868277:808668_bsr=unit_only:fmbas=expand:slsqr=918633,837268:irw=on:plsq=on:fde=none:to=lpo:sims=off:plsqr=7489544,962113:sp=reverse_arity:sos=on:erd=off:spb=goal_then_units:urr=on:s2agt=12:awrsf=3:slsq=on:nwc=8:slsqc=2:fmbsso=preprocessed_usage:newcnf=on:cond=fast:fmbsr=1.4217:lcm=reverse:s2a=on:s2at=2.3728:dr=on:ep=RSTC:fmbswo=argument_first:bd=off:nm=3:av=off:fsr=off:gs=on:rnwc=on:er=filter:fsdmm=1_50");
+  quick.push("dis+1011_254547:620852_bsr=on:fmbas=expand:slsqr=1226417,989503:irw=on:fde=unused:sims=off:avsqr=545723,716701:slsql=off:sp=occurrence:sos=theory:lma=on:spb=goal_then_units:bce=on:awrs=decay:fd=off:awrsf=70:slsq=on:slsqc=2:skr=on:flr=on:avsqc=1:lwlo=on:avsq=on:fmbsr=1.73802:lcm=reverse:avsql=on:fmbswo=argument_first:nm=7:av=off:er=filter:sfv=off_50");
+  quick.push("lrs+0_2279:628249_fmbas=function:slsqr=132255,682457:fde=none:to=lpo:avsqr=355413,74785:sp=reverse_arity:sos=theory:erd=off:lma=on:spb=units:drc=off:urr=ec_only:bce=on:fmbss=2:fmbes=smt:awrs=converge:s2agt=39:fd=preordered:awrsf=281:slsq=on:nwc=3:slsqc=1:avsqc=2:updr=off:fmbsso=input_usage:newcnf=on:lwlo=on:s2pl=on:avsq=on:st=4.14186:fmbsr=1.0275:s2a=on:bs=on:s2at=1.07135:dr=on:sd=3:ss=axioms:fmbswo=argument_first:ins=1:bsdmm=3:fsd=on:bd=preordered:nm=49:av=off:gsp=input_only:sgt=15_50");
+  quick.push("lrs+2_1446004:597505_bsr=on:slsqr=1363287,790064:irw=on:plsq=on:fde=unused:plsqc=2:sims=off:bsd=on:avsqr=628863,532321:plsqr=1561406,613233:slsql=off:sp=reverse_frequency:erd=off:fs=off:spb=units:drc=off:urr=on:bce=on:plsql=on:s2agt=7:fd=off:awrsf=4:slsq=on:slsqc=0:skr=on:updr=off:fmbsso=input_usage:newcnf=on:gsem=off:avsq=on:cond=fast:fmbsr=1.05789:lcm=reverse:s2a=on:bs=on:s2at=1.39705:fmbdsb=on:fmbswo=diagonal:bsdmm=2:nm=0:av=off:fsr=off:gs=on:gsp=input_only:gsssp=full:fsdmm=2_50");
+  quick.push("ott+0_1856:792395_anc=none:bsr=on:fmbas=function:slsqr=510704,977207:irw=on:sims=off:sp=reverse_arity:sos=on:spb=goal_then_units:abs=on:drc=off:urr=on:bce=on:fmbss=2:fmbes=smt:s2agt=14:awrsf=15:slsq=on:nwc=2:slsqc=2:alpa=false:flr=on:fmbsso=input_usage:newcnf=on:lwlo=on:nicw=on:cond=fast:st=1.61867:fmbsr=1.90834:lcm=predicate:s2a=on:bs=unit_only:s2at=1.24759:dr=on:gsaa=from_current:sd=3:aac=none:br=off:ss=included:fmbswo=argument_first:nm=3:fsr=off:gs=on:afq=1.55191:rnwc=on:sfv=off:fsdmm=1_50");
+
   quick.push("lrs+11_2672606:373061_anc=none:bsr=unit_only:fmbas=expand:ccuc=small_ones:to=lpo:sp=reverse_frequency:sos=theory:lma=on:acc=model:urr=ec_only:bce=on:atotf=0.850218:awrs=decay:s2agt=2:awrsf=39:amm=off:cond=fast:st=2.03032:fmbsr=1.87978:lcm=predicate:s2a=on:bs=on:s2at=1.51551:dr=on:afp=19253:fmbdsb=on:aac=none:ss=axioms:fmbswo=argument_first:fsd=on:bd=preordered:nm=0:fsr=off:afq=1.00387:afr=on:sfv=off:fsdmm=1_50");
   quick.push("dis+3_1310497:903997_bsr=unit_only:fmbas=function:irw=on:fde=unused:sims=off:avsqr=4284349,472039:sp=reverse_frequency:sos=theory:erd=off:lma=on:spb=goal:drc=off:fmbss=4:awrs=converge:awrsf=2:nwc=2:skr=on:avsqc=2:fmbsso=input_usage:newcnf=on:lwlo=on:avsq=on:cond=on:st=4.47056:fmbsr=1.90548:avsql=on:bs=on:dr=on:sd=1:ss=included:fmbswo=argument_first:bsdmm=1:fsd=on:bd=preordered:nm=0:av=off:gs=on:gsp=input_only:er=filter:sfv=off:sgt=17:fsdmm=2_50");
   quick.push("ott+10_1540377:823678_anc=none:fmbas=expand:slsqr=702737,984140:irw=on:fde=unused:sims=off:add=off:avsqr=176566,672333:etr=on:slsql=off:sp=reverse_frequency:sos=theory:lma=on:spb=goal_then_units:drc=off:urr=ec_only:fmbss=3:awrs=converge:awrsf=28:slsq=on:nwc=2:slsqc=2:alpa=false:flr=on:sac=on:fmbsso=input_usage:lwlo=on:amm=off:avsq=on:fmbsr=1.70442:lcm=reverse:bs=on:afp=361:aac=none:ins=1:fsd=on:bd=off:nm=15:afq=1.081:rnwc=on:gsp=input_only:sfv=off_50");
   quick.push("lrs+4_348:237371_anc=all_dependent:bsr=on:slsqr=496579,797180:ccuc=first:plsq=on:fde=none:to=lpo:bsd=on:add=large:plsqr=3817240,736499:slsql=off:sp=frequency:sos=all:erd=off:abs=on:acc=model:atotf=0.0236056:awrs=converge:s2agt=3:fd=preordered:awrsf=12:slsq=on:slsqc=0:alpa=false:skr=on:flr=on:updr=off:fmbsso=input_usage:lwlo=on:nicw=on:s2pl=no:amm=off:cond=fast:st=1.10306:fmbsr=1.67212:s2a=on:bs=on:s2at=1.39033:dr=on:sd=10:fmbdsb=on:aac=none:ss=axioms:fmbswo=argument_first:bsdmm=1:fsd=on:nm=3:afq=1.28236:afr=on:er=known:sfv=off_50");
   quick.push("ott+1010_201852:238213_anc=all_dependent:fmbas=off:ccuc=first:irw=on:fde=none:to=lpo:bsd=on:add=off:etr=on:sp=reverse_frequency:sos=all:lma=on:spb=goal_then_units:abs=on:drc=off:acc=model:fmbss=3:s2agt=51:fd=off:awrsf=1:nwc=3:alpa=true:updr=off:sac=on:newcnf=on:nicw=on:st=2.92595:fmbsr=1.87876:lcm=reverse:s2a=on:bs=on:s2at=2.42529:afp=497:fmbdsb=on:ep=RS:ss=axioms:fmbswo=argument_first:ins=1:fsd=on:nm=0:aer=off:afq=1.86926:gsp=input_only:sfv=off_50");
-  quick.push("fmb+1_1473:930133_bsr=unit_only:fmbas=function:irw=on:bsd=on:avsqr=5419031,624300:etr=on:sp=frequency:sos=all:lma=on:fs=off:drc=off:urr=on:bce=on:fmbes=contour:awrs=decay:awrsf=12:flr=on:avsqc=2:fmbswr=7:lwlo=on:gsem=off:avsq=on:fmbsr=1.43447:fmbswo=diagonal:ins=2:bd=preordered:nm=11:av=off:fsr=off:gs=on:gsp=input_only_50");
 }