From 592c226abbfcc77ca90f2256b1b9232b55c8cd9a Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 12 Jul 2023 10:01:21 +0000 Subject: [PATCH] after-casc SLH2 sched v5 --- CASC/Schedules.cpp | 550 ++++++++++++++++++++++++--------------------- 1 file changed, 294 insertions(+), 256 deletions(-) diff --git a/CASC/Schedules.cpp b/CASC/Schedules.cpp index bba8c3c21c..bec87fbfa5 100644 --- a/CASC/Schedules.cpp +++ b/CASC/Schedules.cpp @@ -5735,429 +5735,467 @@ void Schedules::getSnakeSlhSchedule(const Shell::Property& property, Schedule& q void Schedules::getSnakeSlh2Schedule(const Shell::Property& property, Schedule& quick) { // Sub-schedule for 10000Mi strat cap / 10000Mi overall limit quick.push("lrs+1002_1:1_au=on:av=off:fd=off:fde=unused:ntd=on:sos=on:sp=frequency:ss=axioms:i=763:si=on:rtra=on_0"); - quick.push("dis+10_1:3_au=on:cnfonf=lazy_pi_sigma_gen:i=15:si=on:rtra=on_0"); - quick.push("lrs+21_1:1_bd=off:bsd=on:fde=unused:hud=5:nwc=10.0:sac=on:sp=weighted_frequency:ss=axioms:i=2:si=on:rtra=on_0"); - quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=822:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_aac=none:fde=none:hud=10:kws=arity_squared:sos=on:tnu=1:i=2:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:sd=1:sos=all:ss=axioms:st=1.5:i=617:si=on:rtra=on_0"); + quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=817:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:sd=1:sos=all:ss=axioms:st=1.5:i=618:si=on:rtra=on_0"); quick.push("lrs+1010_1:1_e2e=on:ntd=on:nwc=5.0:sac=on:sd=1:sgt=16:spb=units:ss=axioms:i=538:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_au=on:bd=off:e2e=on:ins=3:sos=on:ss=axioms:i=836:si=on:rtra=on_0"); quick.push("dis+1002_1:1_au=on:kws=inv_precedence:nwc=5.0:sd=1:sgt=32:ss=axioms:i=947:si=on:rtra=on_0"); quick.push("lrs+10_1:1_au=on:bd=off:cnfonf=off:fd=off:sos=all:i=1520:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:avsq=on:avsqr=1,16:kws=arity_squared:nm=20:sd=1:sp=const_frequency:ss=axioms:i=134:si=on:rtra=on_0"); quick.push("dis+1010_3:1_acc=on:au=on:chr=on:cnfonf=off:fd=preordered:nwc=10.0:s2a=on:i=707:si=on:rtra=on_0"); quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=1259:si=on:rtra=on_0"); + quick.push("lrs+666_1:1_au=on:bs=unit_only:e2e=on:sd=1:sp=frequency:ss=axioms:i=2:si=on:rtra=on_0"); quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=1363:si=on:rtra=on_0"); + quick.push("lrs+1010_1:5_cnfonf=lazy_pi_sigma_gen:kws=precedence:nm=32:nwc=10.0:sp=const_frequency:i=15:si=on:rtra=on_0"); quick.push("dis+10_8:1_au=on:e2e=on:sgt=8:ss=axioms:i=482:si=on:rtra=on_0"); - // Improves by expected 2225.3486777788794 probs costing 9859 Mi + // Improves by expected 2226.0263882194936 probs costing 9987 Mi // Sub-schedule for 20000Mi strat cap / 20000Mi overall limit - quick.push("lrs+1002_1:1_fsr=off:prag=on:sos=on:ss=axioms:i=736:si=on:rtra=on_0"); - quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=2909:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:sd=1:sos=all:ss=axioms:st=1.5:i=1186:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_e2e=on:fd=off:fe=off:prag=on:sos=on:i=1906:si=on:rtra=on_0"); - quick.push("lrs+2_1:3_au=on:bd=off:e2e=on:sos=on:ss=axioms:i=504:si=on:rtra=on_0"); - quick.push("lrs+0_1:1_au=on:ins=3:kws=precedence:ntd=on:sos=on:sp=const_max:ss=axioms:i=1328:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=3224:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_sd=1:sgt=30:sp=reverse_arity:ss=axioms:tgt=full:i=590:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:s2a=on:s2agt=8:i=481:si=on:rtra=on_0"); + quick.push("dis+2_1:1_apa=on:au=on:bd=off:c=on:cnfonf=off:fsr=off:sd=1:sos=on:ss=axioms:i=571:si=on:rtra=on_0"); + quick.push("dis+1004_1:4_av=off:e2e=on:hud=3:prag=on:sos=on:ss=axioms:i=761:si=on:rtra=on_0"); + quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=2133:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=443:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:sd=1:sos=all:ss=axioms:st=1.5:i=1081:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_e2e=on:fd=off:fe=off:prag=on:sos=on:i=1788:si=on:rtra=on_0"); + quick.push("lrs+0_1:1_au=on:ins=3:kws=precedence:ntd=on:sos=on:sp=const_max:ss=axioms:i=1271:si=on:rtra=on_0"); + quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=3919:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_kws=precedence:sos=on:sp=frequency:ss=axioms:i=751:si=on:rtra=on_0"); + quick.push("ott+1002_1:1_au=on:fde=none:nm=10:sos=on:i=802:si=on:rtra=on_0"); quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=1182:si=on:rtra=on_0"); - quick.push("ott+2_1:128_bd=off:ins=3:kws=precedence:sd=1:sos=on:sp=frequency:ss=axioms:st=5.0:i=300:si=on:rtra=on_0"); + quick.push("ott+2_1:128_bd=off:ins=3:kws=precedence:sd=1:sos=on:sp=frequency:ss=axioms:st=5.0:i=282:si=on:rtra=on_0"); quick.push("lrs+20_1:1_au=on:bd=off:erd=off:fde=none:sos=on:i=532:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:cbe=off:nm=10:sd=1:sos=all:ss=axioms:st=3.0:i=538:si=on:rtra=on_0"); + quick.push("dis+10_1:1_au=on:cbe=off:nm=10:sd=1:sos=all:ss=axioms:st=3.0:i=423:si=on:rtra=on_0"); quick.push("dis+10_1:1_cnfonf=off:fe=off:nwc=10.0:s2a=on:s2agt=8:sd=1:ss=axioms:st=5.0:i=357:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_av=off:kws=precedence:sos=on:sp=reverse_arity:ss=axioms:i=439:si=on:rtra=on_0"); - quick.push("lrs+1010_1:4_au=on:hfsq=on:sd=2:sgt=8:ss=axioms:i=900:si=on:rtra=on_0"); - quick.push("dis+21_1:1_au=on:c=on:cnfonf=off:e2e=on:ins=1:kws=precedence:ntd=on:sd=2:sos=on:ss=axioms:st=2.0:i=584:si=on:rtra=on_0"); - quick.push("lrs+1010_4:1_amm=off:awrs=decay:bsr=on:cbe=off:e2e=on:fde=none:fe=axiom:nwc=5.0:prag=on:sac=on:sd=1:spb=goal_then_units:ss=axioms:i=1657:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_sd=2:slsq=on:slsqc=1:ss=axioms:i=492:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_c=on:cnfonf=off:hud=15:rawr=on:sd=1:sos=all:ss=axioms:i=168:si=on:rtra=on_0"); - // Improves by expected 225.82507538958157 probs costing 19993 Mi + quick.push("lrs+1010_1:4_au=on:hfsq=on:sd=2:sgt=8:ss=axioms:i=808:si=on:rtra=on_0"); + quick.push("lrs+1010_4:1_amm=off:awrs=decay:bsr=on:cbe=off:e2e=on:fde=none:fe=axiom:nwc=5.0:prag=on:sac=on:sd=1:spb=goal_then_units:ss=axioms:i=1665:si=on:rtra=on_0"); + quick.push("dis+21_1:1_bd=off:e2e=on:s2a=on:s2agt=32:sfv=off:ss=axioms:st=2.0:i=1153:si=on:rtra=on_0"); + // Improves by expected 226.7572876818416 probs costing 19904 Mi // Sub-schedule for 30000Mi strat cap / 30000Mi overall limit quick.push("dis+10_4:1_e2e=on:fde=none:hfsq=on:s2a=on:s2at=3.0:slsq=on:slsqc=1:i=1101:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:fde=none:kws=inv_precedence:nwc=5.0:plsq=on:plsqc=1:plsqr=6,1:prag=on:s2a=on:i=1357:si=on:rtra=on_0"); + quick.push("dis+10_1:1_cs=on:e2e=on:hfsq=on:i=290:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_au=on:av=off:fd=off:fde=unused:ntd=on:sos=on:sp=frequency:ss=axioms:i=2134:si=on:rtra=on_0"); + quick.push("dis+10_1:1_cnfonf=lazy_pi_sigma_gen:hfsq=on:sd=1:ss=axioms:i=265:si=on:rtra=on_0"); quick.push("lrs+10_8:1_cbe=off:e2e=on:hud=10:sd=1:ss=axioms:st=3.0:tgt=ground:i=251:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=4228:si=on:rtra=on_0"); + quick.push("dis-1010_1:1_au=on:e2e=on:hfsq=on:nm=0:s2a=on:s2at=1.5:i=2473:si=on:rtra=on_0"); quick.push("dis+1010_1:1_apa=on:bsr=on:cnfonf=off:hud=10:ins=2:kws=inv_frequency:sd=2:slsq=on:slsqc=5:sos=on:ss=axioms:i=240:si=on:rtra=on_0"); quick.push("lrs+2_1:64_bd=off:nwc=5.0:sd=2:ss=axioms:i=290:si=on:rtra=on_0"); - quick.push("dis+1002_1:2_cnfonf=lazy_pi_sigma_gen:ins=1:nm=32:ntd=on:nwc=10.0:prag=on:s2at=3.0:slsq=on:slsqr=1,16:i=873:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=435:si=on:rtra=on_0"); + quick.push("lrs+10_8:1_bd=off:fd=off:kws=inv_precedence:sos=on:ss=axioms:i=358:si=on:rtra=on_0"); quick.push("lrs+1002_1:128_bd=off:e2e=on:ins=1:sac=on:sd=1:sos=on:ss=axioms:st=2.0:i=585:si=on:rtra=on_0"); - quick.push("dis+1002_2:3_aac=none:au=on:cbe=off:fde=none:hfsq=on:hfsqc=2:hfsqr=8,1:lcm=predicate:nm=32:prag=on:sos=on:sp=unary_first:ss=axioms:st=2.0:i=1579:si=on:rtra=on_0"); + quick.push("dis+1002_2:3_aac=none:au=on:cbe=off:fde=none:hfsq=on:hfsqc=2:hfsqr=8,1:lcm=predicate:nm=32:prag=on:sos=on:sp=unary_first:ss=axioms:st=2.0:i=1609:si=on:rtra=on_0"); quick.push("dis+10_5:1_au=on:hfsq=on:ss=axioms:i=990:si=on:rtra=on_0"); quick.push("lrs+4_1:1_fd=off:fs=off:fsr=off:sac=on:sos=on:ss=axioms:i=413:si=on:rtra=on_0"); - quick.push("dis+10_8:1_cs=on:e2e=on:s2a=on:i=400:si=on:rtra=on_0"); - quick.push("lrs+1010_1:5_au=on:bd=off:cnfonf=off:nm=10:sos=on:i=602:si=on:rtra=on_0"); + quick.push("lrs+21_1:1_au=on:e2e=on:hud=10:sd=4:sos=on:ss=axioms:st=2.0:i=1265:si=on:rtra=on_0"); quick.push("lrs+21_1:1_erd=off:ins=3:sd=1:sos=on:ss=axioms:i=263:si=on:rtra=on_0"); quick.push("dis+10_3:1_avsq=on:sd=1:ss=axioms:st=2.0:tgt=ground:i=278:si=on:rtra=on_0"); + quick.push("dis+1010_8:1_au=on:cbe=off:hfsq=on:plsq=on:plsqc=1:plsqr=32,1:rawr=on:rp=on:sd=2:ss=axioms:st=3.0:i=1965:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_bd=off:e2e=on:ins=2:sd=1:sos=all:ss=axioms:st=3.0:i=326:si=on:rtra=on_0"); quick.push("lrs+31_1:1_au=on:cnfonf=off:ins=3:plsq=on:sd=1:sgt=32:sos=on:ss=axioms:i=494:si=on:rtra=on_0"); quick.push("lrs+10_1:128_fd=off:hud=20:sos=on:ss=axioms:tnu=2:i=289:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_bsd=on:fsd=on:nwc=10.0:sd=1:ss=axioms:i=404:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_bsd=on:fsd=on:nwc=10.0:sd=1:ss=axioms:i=243:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_sd=1:sgt=30:sp=reverse_arity:ss=axioms:tgt=full:i=633:si=on:rtra=on_0"); quick.push("dis+2_1:1_cnfonf=off:e2e=on:kws=inv_frequency:nm=0:nwc=5.0:s2a=on:s2agt=32:ss=axioms:i=487:si=on:rtra=on_0"); - quick.push("ott+1002_1:1_au=on:fde=none:nm=10:sos=on:i=877:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:av=off:fd=off:fde=none:fsr=off:ntd=on:sos=on:sp=occurrence:i=1084:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:bd=off:cnfonf=off:nm=0:sac=on:sd=1:sp=unary_frequency:ss=axioms:st=3.0:i=762:si=on:rtra=on_0"); quick.push("lrs+10_1:1_er=filter:fd=off:flr=on:nwc=10.0:ss=axioms:st=3.0:i=365:si=on:rtra=on_0"); quick.push("dis+2_1:1_au=on:hfsq=on:hfsqc=5:nm=0:sd=1:ss=axioms:i=556:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:sd=1:slsq=on:ss=axioms:i=1133:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_bd=off:fde=unused:fe=off:fs=off:fsr=off:hud=10:sos=on:i=719:si=on:rtra=on_0"); - quick.push("dis+10_1:1_hud=5:nm=16:prag=on:sac=on:sos=on:ss=axioms:tnu=2:i=1029:si=on:rtra=on_0"); + quick.push("dis+10_1:1_hud=5:nm=16:prag=on:sac=on:sos=on:ss=axioms:tnu=2:i=1097:si=on:rtra=on_0"); + quick.push("dis+21_1:1_au=on:c=on:cnfonf=off:e2e=on:ins=1:kws=precedence:ntd=on:sd=2:sos=on:ss=axioms:st=2.0:i=640:si=on:rtra=on_0"); quick.push("dis+10_1:32_fd=off:kws=precedence:sd=2:sos=on:ss=axioms:i=237:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_sd=2:slsq=on:slsqc=1:ss=axioms:i=751:si=on:rtra=on_0"); quick.push("lrs+10_1:1_hud=10:ins=2:sos=all:ss=axioms:tnu=1:i=229:si=on:rtra=on_0"); - quick.push("ott+10_1:1_atotf=0.1:au=on:cnfonf=off:e2e=on:fsr=off:ins=4:kws=precedence:s2a=on:i=2278:si=on:rtra=on_0"); - quick.push("ott+10_16:1_aac=none:au=on:cnfonf=off:nm=20:s2a=on:ss=axioms:i=4574:si=on:rtra=on_0"); - quick.push("dis+21_1:1_bd=off:e2e=on:s2a=on:s2agt=32:sfv=off:ss=axioms:st=2.0:i=1321:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_bd=off:e2e=on:ins=2:sd=1:sos=all:ss=axioms:st=3.0:i=316:si=on:rtra=on_0"); - // Improves by expected 129.5337591178251 probs costing 29938 Mi + quick.push("dis+10_1:3_aac=none:bd=off:cnfonf=off:fde=unused:ins=2:ntd=on:s2a=on:sac=on:i=437:si=on:rtra=on_0"); + quick.push("ott+10_16:1_aac=none:au=on:cnfonf=off:nm=20:s2a=on:ss=axioms:i=4485:si=on:rtra=on_0"); + // Improves by expected 130.432668654497 probs costing 29925 Mi // Sub-schedule for 60000Mi strat cap / 60000Mi overall limit - quick.push("lrs+10_1:1_au=on:cnfonf=off:sd=1:sos=all:ss=axioms:st=3.0:i=541:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:fde=none:fsr=off:sos=on:sp=const_frequency:i=854:si=on:rtra=on_0"); - quick.push("dis+10_1:1_acc=on:fde=none:kws=inv_precedence:nwc=5.0:plsq=on:plsqc=1:plsqr=6,1:prag=on:s2a=on:i=1345:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:cnfonf=off:sd=1:sos=all:ss=axioms:st=3.0:i=501:si=on:rtra=on_0"); + quick.push("lrs+10_1:28_au=on:lma=on:sgt=8:sos=all:ss=axioms:i=1106:si=on:rtra=on_0"); + quick.push("ott+1010_3:1_bd=preordered:cbe=off:e2e=on:fe=axiom:hud=5:s2a=on:s2agt=60:slsq=on:ss=axioms:tnu=1:i=7349:si=on:rtra=on_0"); quick.push("dis+1010_1:1_au=on:c=on:ins=3:plsq=on:plsqc=5:sd=1:sos=on:ss=axioms:i=567:si=on:rtra=on_0"); quick.push("lrs+1010_1:1_bsr=on:e2e=on:fde=unused:nm=7:sac=on:sos=on:sp=frequency:tnu=9:i=731:si=on:rtra=on_0"); - quick.push("dis+2_1:1_apa=on:au=on:bd=off:c=on:cnfonf=off:fsr=off:sd=1:sos=on:ss=axioms:i=565:si=on:rtra=on_0"); + quick.push("ott+10_5:4_au=on:bs=unit_only:bsr=unit_only:fsr=off:hfsq=on:hfsqr=5,1:ins=3:kws=arity:sd=1:sos=all:ss=axioms:i=1276:si=on:rtra=on_0"); quick.push("dis+10_1:1_au=on:avsq=on:avsqr=16,1:fd=off:nm=2:sos=all:i=890:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=6294:si=on:rtra=on_0"); quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=1035:si=on:rtra=on_0"); - quick.push("dis-1010_1:1_au=on:e2e=on:hfsq=on:nm=0:s2a=on:s2at=1.5:i=2447:si=on:rtra=on_0"); quick.push("dis+1010_1:1_apa=on:bsr=on:cnfonf=off:hud=10:ins=2:kws=inv_frequency:sd=2:slsq=on:slsqc=5:sos=on:ss=axioms:i=240:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_afp=1010:fde=unused:fe=off:hud=10:kws=arity_squared:prag=on:sos=on:sp=reverse_arity:i=1043:si=on:rtra=on_0"); + quick.push("dis+1010_1:28_chr=on:cnfonf=lazy_not_be_gen:fde=none:hud=5:ins=2:kws=precedence:prag=on:sos=on:sp=occurrence:spb=goal_then_units:ss=axioms:i=1301:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_afp=1010:fde=unused:fe=off:hud=10:kws=arity_squared:prag=on:sos=on:sp=reverse_arity:i=1046:si=on:rtra=on_0"); quick.push("dis+1010_4:1_amm=off:bs=on:c=on:cbe=off:nm=64:nwc=6.0:s2a=on:s2at=5.0:sac=on:slsq=on:slsqr=1,8:i=1108:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=1097:si=on:rtra=on_0"); - quick.push("lrs+21_1:1_au=on:e2e=on:hud=10:sd=4:sos=on:ss=axioms:st=2.0:i=1334:si=on:rtra=on_0"); - quick.push("lrs+1010_1:4_au=on:e2e=on:hud=10:nm=32:plsq=on:plsqc=1:plsqr=32,1:sac=on:sos=on:i=1493:si=on:rtra=on_0"); + quick.push("ott+1010_1:4_au=on:avsq=on:avsqc=1:cnfonf=off:e2e=on:fsr=off:ins=1:nwc=10.0:s2a=on:s2at=2.5:sac=on:sp=const_min:i=2840:si=on:rtra=on_0"); + quick.push("lrs+21_1:1_av=off:bd=off:fd=off:kws=inv_frequency:sos=on:i=766:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_e2e=on:nwc=5.0:sd=1:sgt=30:ss=axioms:i=870:si=on:rtra=on_0"); + quick.push("lrs+1010_1:4_au=on:e2e=on:hud=10:nm=32:plsq=on:plsqc=1:plsqr=32,1:sac=on:sos=on:i=1526:si=on:rtra=on_0"); + quick.push("lrs+2_1:3_au=on:bd=off:e2e=on:sos=on:ss=axioms:i=2642:si=on:rtra=on_0"); quick.push("dis+10_5:1_cnfonf=off:slsq=on:sp=const_max:i=571:si=on:rtra=on_0"); quick.push("dis+1002_1:1_cnfonf=lazy_not_gen_be_off:kws=precedence:prag=on:s2a=on:sp=frequency:ss=axioms:i=569:si=on:rtra=on_0"); - quick.push("lrs+10_2:1_fde=none:prag=on:sd=2:sgt=8:ss=axioms:tgt=ground:i=348:si=on:rtra=on_0"); quick.push("lrs+2_1:1_aac=none:cbe=off:cnfonf=lazy_pi_sigma_gen:sos=all:sp=const_max:uhcvi=on:i=753:si=on:rtra=on_0"); - quick.push("lrs+1002_1:3_au=on:e2e=on:fsr=off:ins=3:sos=on:sp=unary_frequency:i=3548:si=on:rtra=on_0"); - quick.push("dis+22_1:1_au=on:fe=axiom:ntd=on:nwc=10.0:s2a=on:i=1406:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_e2e=on:sd=1:ss=axioms:st=3.0:i=2033:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_cbe=off:cnfonf=lazy_not_be_gen:fs=off:fsr=off:nwc=12.0:ss=axioms:i=458:si=on:rtra=on_0"); + quick.push("dis+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:s2a=on:s2agt=8:i=1101:si=on:rtra=on_0"); + quick.push("ott+1010_8:1_e2e=on:plsq=on:plsqr=32,1:sgt=8:ss=axioms:i=1749:si=on:rtra=on_0"); + quick.push("dis+22_1:1_au=on:fe=axiom:ntd=on:nwc=10.0:s2a=on:i=6442:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:avsq=on:avsqr=1,16:kws=arity_squared:nm=20:sd=1:sp=const_frequency:ss=axioms:i=638:si=on:rtra=on_0"); quick.push("dis+10_1:12_cnfonf=conj_eager:ss=axioms:st=3.0:tgt=full:i=620:si=on:rtra=on_0"); - quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=10717:si=on:rtra=on_0"); - quick.push("lrs+1010_16:1_acc=on:anc=all_dependent:fde=unused:hfsq=on:hfsql=off:hfsqr=4,1:hud=1:ins=2:piset=all_but_not_eq:prag=on:sac=on:i=6854:si=on:rtra=on_0"); + quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=4043:si=on:rtra=on_0"); quick.push("lrs+10_5:1_cnfonf=lazy_not_gen_be_off:hud=5:sd=1:ss=axioms:i=597:si=on:rtra=on_0"); - quick.push("dis+2_2:3_e2e=on:fsr=off:prag=on:sos=on:ss=axioms:i=2291:si=on:rtra=on_0"); quick.push("dis+1002_1:1_au=on:cnfonf=off:sd=1:sgt=16:sp=occurrence:ss=axioms:i=1367:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_av=off:bd=off:fde=none:plsq=on:plsqc=2:plsqr=10,1:s2a=on:s2agt=16:i=652:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:s2a=on:i=769:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_bs=on:e2e=on:prag=on:sos=on:ss=axioms:i=973:si=on:rtra=on_0"); - quick.push("lrs+1666_1:4_cnfonf=off:fde=none:hfsq=on:nm=2:ntd=on:prag=on:sd=7:sos=on:ss=axioms:tnu=5:i=246:si=on:rtra=on_0"); - quick.push("lrs+1010_1:4_au=on:hfsq=on:sd=2:sgt=8:ss=axioms:i=3168:si=on:rtra=on_0"); - quick.push("lrs-1002_1:1_au=on:ins=2:sos=on:ss=axioms:st=1.5:i=337:si=on:rtra=on_0"); - quick.push("lrs+21_1:128_acc=model:au=on:cbe=off:e2e=on:pe=on:piset=small_set:sos=on:sp=occurrence:ss=axioms:i=1105:si=on:rtra=on_0"); - quick.push("ott+1010_1:4_au=on:avsq=on:avsqc=1:cnfonf=off:e2e=on:fsr=off:ins=1:nwc=10.0:s2a=on:s2at=2.5:sac=on:sp=const_min:i=3885:si=on:rtra=on_0"); - quick.push("ott+1010_8:1_e2e=on:plsq=on:plsqr=32,1:sgt=8:ss=axioms:i=834:si=on:rtra=on_0"); - quick.push("dis+10_1:5_bsr=on:cnfonf=lazy_not_be_gen:hud=5:sd=1:sos=all:ss=axioms:i=988:si=on:rtra=on_0"); - // Improves by expected 118.70614219626505 probs costing 59883 Mi + quick.push("lrs+10_1:1_av=off:bd=off:fde=none:plsq=on:plsqc=2:plsqr=10,1:s2a=on:s2agt=16:i=1231:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_bs=on:e2e=on:prag=on:sos=on:ss=axioms:i=924:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:sd=1:slsq=on:ss=axioms:i=1554:si=on:rtra=on_0"); + quick.push("dis+1010_1:16_amm=sco:cnfonf=off:sd=1:ss=axioms:st=2.0:tgt=full:tnu=5:i=1806:si=on:rtra=on_0"); + quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nm=0:nwc=5.0:i=977:si=on:rtra=on_0"); + quick.push("lrs-1002_1:1_au=on:ins=2:sos=on:ss=axioms:st=1.5:i=533:si=on:rtra=on_0"); + quick.push("ott+10_1:1_atotf=0.1:au=on:cnfonf=off:e2e=on:fsr=off:ins=4:kws=precedence:s2a=on:i=1905:si=on:rtra=on_0"); + // Improves by expected 122.54912416632952 probs costing 59889 Mi // Sub-schedule for 120000Mi strat cap / 120000Mi overall limit - quick.push("dis+10_4:1_e2e=on:fde=none:hfsq=on:s2a=on:s2at=3.0:slsq=on:slsqc=1:i=5420:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:cnfonf=off:sd=1:sos=all:ss=axioms:st=3.0:i=6494:si=on:rtra=on_0"); - quick.push("lrs+10_1:28_au=on:lma=on:sgt=8:sos=all:ss=axioms:i=689:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:cnfonf=off:sd=1:sos=all:ss=axioms:st=3.0:i=501:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:fde=none:fsr=off:sos=on:sp=const_frequency:i=854:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=1016:si=on:rtra=on_0"); + quick.push("ott+10_5:4_au=on:bs=unit_only:bsr=unit_only:fsr=off:hfsq=on:hfsqr=5,1:ins=3:kws=arity:sd=1:sos=all:ss=axioms:i=629:si=on:rtra=on_0"); + quick.push("dis+10_1:1_fd=off:fde=unused:prag=on:sos=all:i=661:si=on:rtra=on_0"); quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=1035:si=on:rtra=on_0"); - quick.push("dis+10_4:1_av=off:cnfonf=off:hud=5:nwc=10.0:s2a=on:s2agt=16:i=2731:si=on:rtra=on_0"); quick.push("lrs+1010_1:1_bd=off:cnfonf=off:hud=10:nm=32:sac=on:sd=1:sims=off:sos=all:ss=axioms:st=2.0:i=1511:si=on:rtra=on_0"); - quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=6172:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_e2e=on:ntd=on:nwc=5.0:sac=on:sd=1:sgt=16:spb=units:ss=axioms:i=8496:si=on:rtra=on_0"); - quick.push("lrs+1010_3:1_au=on:bd=off:fde=none:lecc=1.5:nwc=10.0:i=8557:si=on:rtra=on_0"); + quick.push("lrs+1002_4:1_au=on:cnfonf=off:ins=1:nm=2:ntd=on:slsq=on:slsqc=4:sos=on:i=1257:si=on:rtra=on_0"); + quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=6340:si=on:rtra=on_0"); + quick.push("dis+1002_1:2_cnfonf=lazy_pi_sigma_gen:ins=1:nm=32:ntd=on:nwc=10.0:prag=on:s2at=3.0:slsq=on:slsqr=1,16:i=1080:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=1955:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_e2e=on:ntd=on:nwc=5.0:sac=on:sd=1:sgt=16:spb=units:ss=axioms:i=3906:si=on:rtra=on_0"); + quick.push("lrs+1010_3:1_au=on:bd=off:fde=none:lecc=1.5:nwc=10.0:i=9473:si=on:rtra=on_0"); quick.push("dis+1002_1:1_au=on:kws=inv_precedence:nwc=5.0:sd=1:sgt=32:ss=axioms:i=3722:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:bd=off:cnfonf=off:fd=off:sos=all:i=1066:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_acc=on:au=on:bd=off:bsr=unit_only:cnfonf=off:fsr=off:nm=2:sos=all:i=5071:si=on:rtra=on_0"); - quick.push("lrs+2_1:3_au=on:bd=off:e2e=on:sos=on:ss=axioms:i=2642:si=on:rtra=on_0"); + quick.push("dis+10_1:1_atotf=0.5:fe=axiom:fsr=off:sd=1:sgt=16:sos=all:ss=axioms:i=491:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_bd=off:sd=2:sos=on:ss=axioms:i=296:si=on:rtra=on_0"); quick.push("lrs+2_1:6_au=on:cnfonf=off:ss=axioms:st=1.5:i=1438:si=on:rtra=on_0"); - quick.push("lrs+10_2:1_fde=none:prag=on:sd=2:sgt=8:ss=axioms:tgt=ground:i=5019:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=5488:si=on:rtra=on_0"); + quick.push("lrs+10_2:1_fde=none:prag=on:sd=2:sgt=8:ss=axioms:tgt=ground:i=2915:si=on:rtra=on_0"); + quick.push("ott+1002_2:1_au=on:cnfonf=lazy_gen:fde=none:nm=32:s2a=on:sp=const_min:i=2104:si=on:rtra=on_0"); quick.push("dis+10_1:128_av=off:fde=unused:hud=1:prag=on:sos=all:ss=axioms:i=3425:si=on:rtra=on_0"); quick.push("dis+3_7:4_bsr=on:c=on:erd=off:fde=none:hud=10:lma=on:nwc=5.0:sac=on:sos=on:sp=frequency:i=2203:si=on:rtra=on_0"); - quick.push("lrs+1010_4:1_acc=on:au=on:bd=off:sfv=off:ss=axioms:i=11028:si=on:rtra=on_0"); - quick.push("lrs+31_1:1_au=on:cnfonf=off:ins=3:plsq=on:sd=1:sgt=32:sos=on:ss=axioms:i=2685:si=on:rtra=on_0"); + quick.push("lrs+1010_4:1_acc=on:au=on:bd=off:sfv=off:ss=axioms:i=13488:si=on:rtra=on_0"); quick.push("dis+1010_3:1_bd=off:e2e=on:s2a=on:s2agt=10:sp=unary_first:i=835:si=on:rtra=on_0"); - quick.push("lrs+10_1:128_fd=off:hud=20:sos=on:ss=axioms:tnu=2:i=1063:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_bsd=on:fsd=on:nwc=10.0:sd=1:ss=axioms:i=401:si=on:rtra=on_0"); + quick.push("ott+2_1:1024_apa=on:atotf=0.2:bd=off:cnfonf=off:erd=off:fd=off:nm=0:sos=all:i=1782:si=on:rtra=on_0"); quick.push("lrs+10_1:128_bd=off:chr=on:erd=off:fd=off:fe=axiom:hud=10:sac=on:sos=on:i=538:si=on:rtra=on_0"); quick.push("lrs+1010_8:1_c=on:fsr=off:hud=0:kws=inv_arity:ntd=on:sos=on:sp=occurrence:i=1098:si=on:rtra=on_0"); - quick.push("ott+10_1:1_s2a=on:s2at=2.0:sd=2:ss=axioms:i=767:si=on:rtra=on_0"); + quick.push("ott+10_1:1_s2a=on:s2at=2.0:sd=2:ss=axioms:i=1790:si=on:rtra=on_0"); + quick.push("dis+21_1:4_avsq=on:avsqr=924271,1048576:c=on:e2e=on:fs=off:fsr=off:piset=and:plsq=on:plsqr=32,1:sd=10:sos=on:sp=unary_first:ss=axioms:st=1.5:tnu=2:i=791:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_e2e=on:sd=1:ss=axioms:st=3.0:i=6281:si=on:rtra=on_0"); quick.push("ott+1002_2:1_au=on:ins=1:nm=2:sac=on:sos=all:i=1084:si=on:rtra=on_0"); quick.push("dis+1010_3:1_acc=on:au=on:chr=on:cnfonf=off:fd=preordered:nwc=10.0:s2a=on:i=938:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_atotf=0.2:au=on:bd=off:cnfonf=off:e2e=on:sos=all:i=3373:si=on:rtra=on_0"); - quick.push("dis+10_1:1_cnfonf=off:fde=none:ss=axioms:i=1579:si=on:rtra=on_0"); - quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=445:si=on:rtra=on_0"); - quick.push("lrs+10_5:1_cnfonf=lazy_not_gen_be_off:hud=5:sd=1:ss=axioms:i=1486:si=on:rtra=on_0"); - quick.push("ott+2_1:128_bd=off:ins=3:kws=precedence:sd=1:sos=on:sp=frequency:ss=axioms:st=5.0:i=290:si=on:rtra=on_0"); - quick.push("dis+10_1:2_au=on:cnfonf=lazy_pi_sigma_gen:ss=axioms:st=1.2:tgt=ground:i=937:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_atotf=0.2:au=on:bd=off:cnfonf=off:e2e=on:sos=all:i=7500:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=775:si=on:rtra=on_0"); + quick.push("dis+2_2:3_e2e=on:fsr=off:prag=on:sos=on:ss=axioms:i=2291:si=on:rtra=on_0"); + quick.push("ott+2_1:128_bd=off:ins=3:kws=precedence:sd=1:sos=on:sp=frequency:ss=axioms:st=5.0:i=282:si=on:rtra=on_0"); + quick.push("ott+1010_41:4_bd=off:cnfonf=off:hud=14:ntd=on:s2a=on:i=1745:si=on:rtra=on_0"); + quick.push("dis+10_1:2_au=on:cnfonf=lazy_pi_sigma_gen:ss=axioms:st=1.2:tgt=ground:i=938:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_e2e=on:hfsq=on:hfsqr=1,2:hud=18:nm=2:rp=on:sos=all:sp=reverse_frequency:ss=axioms:i=1320:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_bs=on:e2e=on:prag=on:sos=on:ss=axioms:i=5115:si=on:rtra=on_0"); quick.push("lrs+10_1:1_av=off:bd=off:kws=precedence:sos=on:sp=frequency:ss=axioms:st=3.0:i=728:si=on:rtra=on_0"); - quick.push("dis+10_4:1_cnfonf=lazy_simp:gs=on:hud=22:sd=1:ss=axioms:tnu=1:i=2117:si=on:rtra=on_0"); - quick.push("dis+1010_1:16_amm=sco:cnfonf=off:sd=1:ss=axioms:st=2.0:tgt=full:tnu=5:i=1701:si=on:rtra=on_0"); - quick.push("lrs+1002_4:1_au=on:cnfonf=off:er=filter:fde=none:ntd=on:nwc=10.0:i=1227:si=on:rtra=on_0"); + quick.push("lrs+1002_4:1_au=on:cnfonf=off:er=filter:fde=none:ntd=on:nwc=10.0:i=1234:si=on:rtra=on_0"); quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=9524:si=on:rtra=on_0"); quick.push("dis+1010_3:1_au=on:bd=off:cnfonf=lazy_gen:fde=none:sd=1:ss=axioms:i=2759:si=on:rtra=on_0"); + quick.push("lrs+1010_4:1_amm=off:awrs=decay:bsr=on:cbe=off:e2e=on:fde=none:fe=axiom:nwc=5.0:prag=on:sac=on:sd=1:spb=goal_then_units:ss=axioms:i=3701:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_bd=preordered:hud=15:kws=precedence:nm=16:sd=3:sgt=16:sos=on:sp=frequency:ss=axioms:i=637:si=on:rtra=on_0"); quick.push("lrs+21_1:1_cnfonf=off:fde=unused:prag=on:sos=all:i=2076:si=on:rtra=on_0"); - quick.push("dis+21_1:4_avsq=on:avsqr=924271,1048576:c=on:e2e=on:fs=off:fsr=off:piset=and:plsq=on:plsqr=32,1:sd=10:sos=on:sp=unary_first:ss=axioms:st=1.5:tnu=2:i=569:si=on:rtra=on_0"); - // Improves by expected 101.05529103372135 probs costing 119985 Mi + quick.push("lrs+21_1:128_acc=model:au=on:cbe=off:e2e=on:pe=on:piset=small_set:sos=on:sp=occurrence:ss=axioms:i=1179:si=on:rtra=on_0"); + quick.push("dis+21_1:1_bd=off:e2e=on:s2a=on:s2agt=32:sfv=off:ss=axioms:st=2.0:i=2186:si=on:rtra=on_0"); + // Improves by expected 101.99492211575122 probs costing 119779 Mi // Sub-schedule for 240000Mi strat cap / 240000Mi overall limit - quick.push("dis+10_1:1_acc=on:fde=none:kws=inv_precedence:nwc=5.0:plsq=on:plsqc=1:plsqr=6,1:prag=on:s2a=on:i=14386:si=on:rtra=on_0"); + quick.push("dis+10_4:1_e2e=on:fde=none:hfsq=on:s2a=on:s2at=3.0:slsq=on:slsqc=1:i=1101:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:fde=none:kws=inv_precedence:nwc=5.0:plsq=on:plsqc=1:plsqr=6,1:prag=on:s2a=on:i=4577:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_au=on:av=off:fd=off:fde=unused:ntd=on:sos=on:sp=frequency:ss=axioms:i=2693:si=on:rtra=on_0"); - quick.push("lrs+10_1:128_cnfonf=off:e2e=on:fde=unused:hud=10:nm=16:pe=on:s2a=on:s2at=2.0:tgt=ground:i=2601:si=on:rtra=on_0"); + quick.push("dis+1010_8:1_cnfonf=lazy_gen:fe=off:fsr=off:hud=15:nwc=10.0:s2a=on:i=4273:si=on:rtra=on_0"); quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=1016:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:av=off:cnfonf=lazy_not_gen_be_off:fe=axiom:kws=arity:nwc=5.0:ss=axioms:i=9244:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_au=on:e2e=on:fde=none:ins=3:kws=precedence:s2a=on:s2at=5.0:sp=frequency:i=2335:si=on:rtra=on_0"); + quick.push("ott+10_5:4_au=on:bs=unit_only:bsr=unit_only:fsr=off:hfsq=on:hfsqr=5,1:ins=3:kws=arity:sd=1:sos=all:ss=axioms:i=629:si=on:rtra=on_0"); quick.push("dis+10_1:1_au=on:avsq=on:avsqr=16,1:fd=off:nm=2:sos=all:i=5800:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=8021:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=1557:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=13120:si=on:rtra=on_0"); quick.push("dis-1010_1:1_au=on:e2e=on:hfsq=on:nm=0:s2a=on:s2at=1.5:i=9390:si=on:rtra=on_0"); - quick.push("lrs+1002_4:1_au=on:cnfonf=off:ins=1:nm=2:ntd=on:slsq=on:slsqc=4:sos=on:i=1907:si=on:rtra=on_0"); - quick.push("dis+21_2:3_cnfonf=conj_eager:fsr=off:sd=1:slsq=on:ss=axioms:st=4.0:i=1790:si=on:rtra=on_0"); - quick.push("dis+1002_1:2_cnfonf=lazy_pi_sigma_gen:ins=1:nm=32:ntd=on:nwc=10.0:prag=on:s2at=3.0:slsq=on:slsqr=1,16:i=1080:si=on:rtra=on_0"); + quick.push("dis+10_4:1_av=off:cnfonf=off:hud=5:nwc=10.0:s2a=on:s2agt=16:i=2642:si=on:rtra=on_0"); + quick.push("dis+21_2:3_cnfonf=conj_eager:fsr=off:sd=1:slsq=on:ss=axioms:st=4.0:i=1845:si=on:rtra=on_0"); quick.push("dis+1010_4:1_amm=off:bs=on:c=on:cbe=off:nm=64:nwc=6.0:s2a=on:s2at=5.0:sac=on:slsq=on:slsqr=1,8:i=4828:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:av=off:cnfonf=off:sd=1:sos=all:ss=axioms:st=1.5:i=1033:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:bd=off:e2e=on:fde=none:ins=1:prag=on:sos=on:i=6109:si=on:rtra=on_0"); quick.push("dis+1002_1:1_au=on:hfsq=on:hfsqr=5,1:hud=22:ins=3:ntd=on:nwc=3.0:s2a=on:sp=weighted_frequency:i=2589:si=on:rtra=on_0"); - quick.push("dis+10_5:1_au=on:hfsq=on:ss=axioms:i=4005:si=on:rtra=on_0"); - quick.push("lrs+21_1:1_au=on:e2e=on:hud=10:sd=4:sos=on:ss=axioms:st=2.0:i=4050:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_au=on:bd=off:e2e=on:ins=3:sos=on:ss=axioms:i=1761:si=on:rtra=on_0"); - quick.push("lrs+1002_1:128_atotf=0.2:au=on:bd=off:cnfonf=off:plsq=on:plsqc=1:plsqr=1,2:prag=on:sd=1:ss=axioms:st=3.0:tgt=full:i=5381:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_e2e=on:fd=off:fe=off:prag=on:sos=on:i=6231:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_alpa=true:anc=none:atotf=0.1:au=on:cnfonf=off:ins=3:nm=64:sd=1:sp=occurrence:ss=axioms:st=5.0:i=2290:si=on:rtra=on_0"); + quick.push("lrs+21_1:1_au=on:e2e=on:hud=10:sd=4:sos=on:ss=axioms:st=2.0:i=4408:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:bd=off:cnfonf=off:fd=off:sos=all:i=1066:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_acc=on:au=on:bd=off:bsr=unit_only:cnfonf=off:fsr=off:nm=2:sos=all:i=4592:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_e2e=on:fd=off:fe=off:prag=on:sos=on:i=4280:si=on:rtra=on_0"); quick.push("lrs+1010_1:4_au=on:e2e=on:hud=10:nm=32:plsq=on:plsqc=1:plsqr=32,1:sac=on:sos=on:i=1403:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_acc=model:ccuc=small_ones:cnfonf=lazy_simp:hfsq=on:nm=16:nwc=10.0:s2a=on:sac=on:sp=const_frequency:i=2901:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_cnfonf=off:erd=off:fde=none:prag=on:sos=on:i=5675:si=on:rtra=on_0"); + quick.push("dis+10_16:1_au=on:cnfonf=conj_eager:hfsq=on:hfsqc=2:piset=equals:s2a=on:sp=occurrence:ss=axioms:i=6139:si=on:rtra=on_0"); + quick.push("dis+1010_8:1_au=on:cbe=off:hfsq=on:plsq=on:plsqc=1:plsqr=32,1:rawr=on:rp=on:sd=2:ss=axioms:st=3.0:i=5743:si=on:rtra=on_0"); + quick.push("dis+10_16:1_au=on:c=on:chr=on:hfsq=on:nm=2:sac=on:sp=unary_first:ss=axioms:i=1781:si=on:rtra=on_0"); + quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=4513:si=on:rtra=on_0"); + quick.push("lrs+31_1:1_au=on:cnfonf=off:ins=3:plsq=on:sd=1:sgt=32:sos=on:ss=axioms:i=494:si=on:rtra=on_0"); quick.push("lrs+10_5:1_avsq=on:avsqr=16,1:cnfonf=conj_eager:nwc=10.0:plsq=on:plsqc=1:plsqr=32,1:sd=2:spb=intro:ss=axioms:i=1928:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_sd=1:sgt=30:sp=reverse_arity:ss=axioms:tgt=full:i=633:si=on:rtra=on_0"); + quick.push("lrs+10_1:128_fd=off:hud=20:sos=on:ss=axioms:tnu=2:i=1063:si=on:rtra=on_0"); quick.push("lrs+1010_1:128_au=on:fsr=off:hfsq=on:ins=3:kws=frequency:sos=all:i=1460:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_bsd=on:cnfonf=off:hfsq=on:nm=10:piset=all_but_not_eq:s2a=on:s2at=6.0:sp=const_min:i=2214:si=on:rtra=on_0"); quick.push("lrs+10_1:128_bd=off:chr=on:erd=off:fd=off:fe=axiom:hud=10:sac=on:sos=on:i=538:si=on:rtra=on_0"); quick.push("dis+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:s2a=on:s2agt=8:i=2717:si=on:rtra=on_0"); - quick.push("lrs+21_8:1_cnfonf=lazy_not_gen:nm=2:nwc=10.0:plsq=on:plsqc=2:plsqr=6,1:prag=on:sgt=8:sp=unary_frequency:ss=axioms:i=10951:si=on:rtra=on_0"); + quick.push("lrs+21_8:1_cnfonf=lazy_not_gen:nm=2:nwc=10.0:plsq=on:plsqc=2:plsqr=6,1:prag=on:sgt=8:sp=unary_frequency:ss=axioms:i=10373:si=on:rtra=on_0"); quick.push("ott+1010_1:1_cnfonf=off:fd=off:rp=on:sac=on:sos=on:i=1264:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_cnfonf=lazy_not_be_gen:fs=off:fsr=off:nwc=10.0:ss=axioms:st=3.0:i=945:si=on:rtra=on_0"); quick.push("dis+10_16:1_au=on:bet=on:cbe=off:cnfonf=off:hfsq=on:ins=3:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=3847:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:avsq=on:avsqr=1,16:kws=arity_squared:nm=20:sd=1:sp=const_frequency:ss=axioms:i=1920:si=on:rtra=on_0"); quick.push("dis+1002_1:2_au=on:bs=on:bsr=unit_only:c=on:fsr=off:hud=10:kws=inv_precedence:nm=6:ntd=on:nwc=10.0:sac=on:sos=on:i=1617:si=on:rtra=on_0"); quick.push("lrs+10_1:1_fe=off:sd=2:sgt=16:ss=axioms:i=3303:si=on:rtra=on_0"); - quick.push("ott+1002_23:4_fsd=on:ins=3:nwc=10.0:prag=on:i=1671:si=on:rtra=on_0"); - quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=1537:si=on:rtra=on_0"); - quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=2241:si=on:rtra=on_0"); + quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=1501:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_atotf=0.3:au=on:cnfonf=off:ins=3:plsq=on:plsqr=208885,1048576:sos=all:spb=goal_then_units:i=2255:si=on:rtra=on_0"); quick.push("lrs+1666_1:1_bd=off:bet=on:bsd=on:bsr=unit_only:fde=none:nwc=10.0:sp=occurrence:i=2482:si=on:rtra=on_0"); - quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=3782:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_er=filter:fd=off:flr=on:nwc=10.0:ss=axioms:st=3.0:i=365:si=on:rtra=on_0"); - quick.push("ott+1010_41:4_bd=off:cnfonf=off:hud=14:ntd=on:s2a=on:i=1745:si=on:rtra=on_0"); + quick.push("dis+10_1:1_cnfonf=off:fde=none:ss=axioms:i=1579:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=15001:si=on:rtra=on_0"); + quick.push("ott+2_1:1_amm=off:atotf=0.4:cnfonf=off:fde=none:lma=on:nm=2:prag=on:sos=all:sp=const_max:tgt=ground:tnu=9:i=1635:si=on:rtra=on_0"); + quick.push("ott+1002_16:1_au=on:bsr=unit_only:fsr=off:sac=on:sos=on:i=4338:si=on:rtra=on_0"); + quick.push("lrs+10_5:1_cnfonf=lazy_not_gen_be_off:hud=5:sd=1:ss=axioms:i=1486:si=on:rtra=on_0"); quick.push("dis+2_1:1_au=on:hfsq=on:hfsqc=5:nm=0:sd=1:ss=axioms:i=556:si=on:rtra=on_0"); quick.push("lrs+21_1:1_aac=none:c=on:cnfonf=lazy_not_gen:sos=on:i=3633:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_bs=on:e2e=on:prag=on:sos=on:ss=axioms:i=2178:si=on:rtra=on_0"); quick.push("lrs+10_1:1_av=off:bd=off:kws=precedence:sos=on:sp=frequency:ss=axioms:st=3.0:i=728:si=on:rtra=on_0"); quick.push("lrs+10_1:1_au=on:cnfonf=lazy_pi_sigma_gen:sd=1:slsq=on:ss=axioms:i=568:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_bd=off:fde=unused:fe=off:fs=off:fsr=off:hud=10:sos=on:i=552:si=on:rtra=on_0"); quick.push("lrs+1002_4:1_au=on:cnfonf=off:er=filter:fde=none:ntd=on:nwc=10.0:i=18654:si=on:rtra=on_0"); quick.push("dis+21_1:1_au=on:c=on:cnfonf=off:e2e=on:ins=1:kws=precedence:ntd=on:sd=2:sos=on:ss=axioms:st=2.0:i=5301:si=on:rtra=on_0"); quick.push("dis+1010_5:1_cnfonf=lazy_pi_sigma_gen:fe=off:hud=10:sd=1:ss=axioms:st=1.5:i=2416:si=on:rtra=on_0"); - quick.push("ott+1010_16:1_cnfonf=lazy_pi_sigma_gen:fe=axiom:hud=5:prag=on:slsq=on:slsqr=4,1:i=6248:si=on:rtra=on_0"); + quick.push("lrs+1010_1:3_alpa=true:au=on:cnfonf=lazy_pi_sigma_gen:sos=on:i=694:si=on:rtra=on_0"); + quick.push("ott+1010_16:1_cnfonf=lazy_pi_sigma_gen:fe=axiom:hud=5:prag=on:slsq=on:slsqr=4,1:i=4267:si=on:rtra=on_0"); quick.push("dis+1010_73:128_bd=preordered:fsr=off:nwc=3.0:s2a=on:s2at=2.0:i=981:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=27179:si=on:rtra=on_0"); - quick.push("lrs+1010_4:1_amm=off:awrs=decay:bsr=on:cbe=off:e2e=on:fde=none:fe=axiom:nwc=5.0:prag=on:sac=on:sd=1:spb=goal_then_units:ss=axioms:i=3099:si=on:rtra=on_0"); - quick.push("lrs+10_16:1_au=on:bd=off:sac=on:sos=all:i=3526:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_sd=2:slsq=on:slsqc=1:ss=axioms:i=488:si=on:rtra=on_0"); + quick.push("lrs+10_5:1_av=off:cnfonf=lazy_pi_sigma_gen:nwc=5.0:prag=on:s2a=on:s2agt=16:i=3801:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_bd=preordered:hud=15:kws=precedence:nm=16:sd=3:sgt=16:sos=on:sp=frequency:ss=axioms:i=480:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_av=off:c=on:cnfonf=off:kws=inv_precedence:piset=and:sd=1:ss=axioms:tgt=ground:tnu=2:i=9010:si=on:rtra=on_0"); + quick.push("lrs+10_97:429_c=on:cnfonf=lazy_gen:fe=axiom:ntd=on:s2a=on:sp=const_frequency:tgt=ground:i=1342:si=on:rtra=on_0"); + quick.push("ott+10_16:1_aac=none:au=on:cnfonf=off:nm=20:s2a=on:ss=axioms:i=9075:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_cbe=off:cnfonf=lazy_not_gen:nwc=13.0:prag=on:s2a=on:sp=weighted_frequency:i=1957:si=on:rtra=on_0"); quick.push("lrs+21_1:128_acc=model:au=on:cbe=off:e2e=on:pe=on:piset=small_set:sos=on:sp=occurrence:ss=axioms:i=1179:si=on:rtra=on_0"); quick.push("lrs+2_1:1_bd=off:bs=unit_only:bsd=on:cnfonf=off:fde=unused:fsr=off:hud=5:kws=inv_arity_squared:sp=const_min:i=2235:si=on:rtra=on_0"); - quick.push("dis+21_1:1_bd=off:e2e=on:s2a=on:s2agt=32:sfv=off:ss=axioms:st=2.0:i=2186:si=on:rtra=on_0"); - quick.push("lrs+2_3:1_acc=model:cnfonf=off:e2e=on:fe=axiom:fs=off:fsr=off:hud=15:piset=all_but_not_eq:sp=const_frequency:ss=axioms:i=1701:si=on:rtra=on_0"); - quick.push("dis+21_1:4_avsq=on:avsqr=924271,1048576:c=on:e2e=on:fs=off:fsr=off:piset=and:plsq=on:plsqr=32,1:sd=10:sos=on:sp=unary_first:ss=axioms:st=1.5:tnu=2:i=568:si=on:rtra=on_0"); - quick.push("dis+1004_1:5_cs=on:e2e=on:hfsq=on:ins=2:sos=all:i=1001:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_abs=on:au=on:cnfonf=off:fde=unused:inj=on:sos=on:i=2090:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_av=off:c=on:cnfonf=off:kws=inv_precedence:piset=and:sd=1:ss=axioms:tgt=ground:tnu=2:i=18199:si=on:rtra=on_0"); - // Improves by expected 84.7709314578973 probs costing 239629 Mi + // Improves by expected 87.6986428831153 probs costing 239816 Mi // Sub-schedule for 480000Mi strat cap / 480000Mi overall limit quick.push("dis+10_4:1_e2e=on:fde=none:hfsq=on:s2a=on:s2at=3.0:slsq=on:slsqc=1:i=19923:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:fde=none:kws=inv_precedence:nwc=5.0:plsq=on:plsqc=1:plsqr=6,1:prag=on:s2a=on:i=13542:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_au=on:av=off:fd=off:fde=unused:ntd=on:sos=on:sp=frequency:ss=axioms:i=1997:si=on:rtra=on_0"); quick.push("lrs+10_1:128_cnfonf=off:e2e=on:fde=unused:hud=10:nm=16:pe=on:s2a=on:s2at=2.0:tgt=ground:i=2601:si=on:rtra=on_0"); - quick.push("dis+1010_8:1_cnfonf=lazy_gen:fe=off:fsr=off:hud=15:nwc=10.0:s2a=on:i=4273:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=6289:si=on:rtra=on_0"); - quick.push("dis+10_1:3_au=on:cnfonf=lazy_pi_sigma_gen:i=1623:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=3973:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=1016:si=on:rtra=on_0"); + quick.push("ott+10_5:4_au=on:bs=unit_only:bsr=unit_only:fsr=off:hfsq=on:hfsqr=5,1:ins=3:kws=arity:sd=1:sos=all:ss=axioms:i=1968:si=on:rtra=on_0"); quick.push("dis+10_1:1_au=on:avsq=on:avsqr=16,1:fd=off:nm=2:sos=all:i=5800:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=33885:si=on:rtra=on_0"); quick.push("lrs+10_1:1_cnfonf=lazy_pi_sigma_gen:plsq=on:sos=on:i=9176:si=on:rtra=on_0"); quick.push("ott+1010_16:1_au=on:cnfonf=off:e2e=on:i=15358:si=on:rtra=on_0"); quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=1557:si=on:rtra=on_0"); quick.push("dis+1010_1:1_fsd=on:hud=10:ntd=on:sp=reverse_arity:ss=axioms:i=13001:si=on:rtra=on_0"); - quick.push("lrs+31_1:1_au=on:bd=off:fde=none:ins=3:sos=on:sp=unary_first:i=6916:si=on:rtra=on_0"); - quick.push("lrs+1002_4:1_au=on:cnfonf=off:ins=1:nm=2:ntd=on:slsq=on:slsqc=4:sos=on:i=2410:si=on:rtra=on_0"); - quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=24601:si=on:rtra=on_0"); + quick.push("dis+1010_1:28_chr=on:cnfonf=lazy_not_be_gen:fde=none:hud=5:ins=2:kws=precedence:prag=on:sos=on:sp=occurrence:spb=goal_then_units:ss=axioms:i=1042:si=on:rtra=on_0"); + quick.push("lrs+1002_4:1_au=on:cnfonf=off:ins=1:nm=2:ntd=on:slsq=on:slsqc=4:sos=on:i=5996:si=on:rtra=on_0"); + quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=14840:si=on:rtra=on_0"); quick.push("ott+1010_16:1_av=off:fe=off:hud=10:ins=5:nwc=3.0:prag=on:rawr=on:i=4504:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=14432:si=on:rtra=on_0"); - quick.push("ott+1010_1:64_au=on:cbe=off:cnfonf=off:nwc=10.0:s2a=on:ss=axioms:i=5674:si=on:rtra=on_0"); + quick.push("ott+1010_1:64_au=on:cbe=off:cnfonf=off:nwc=10.0:s2a=on:ss=axioms:i=5101:si=on:rtra=on_0"); quick.push("dis+1010_13:15_au=on:bd=off:bet=on:cnfonf=off:fe=axiom:hud=10:nm=0:ntd=on:nwc=5.0:sp=const_max:updr=off:i=1615:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:bd=off:e2e=on:fde=none:ins=1:prag=on:sos=on:i=6109:si=on:rtra=on_0"); quick.push("ott+10_1:1_bd=preordered:bsr=on:cnfonf=lazy_gen:ntd=on:nwc=10.0:sims=off:sp=const_frequency:i=3527:si=on:rtra=on_0"); - quick.push("lrs+21_16:1_au=on:bd=preordered:fde=none:ins=2:nwc=10.0:ss=axioms:st=2.0:i=12849:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_e2e=on:ntd=on:nwc=5.0:sac=on:sd=1:sgt=16:spb=units:ss=axioms:i=12797:si=on:rtra=on_0"); + quick.push("lrs+21_1:1_au=on:e2e=on:hud=10:sd=4:sos=on:ss=axioms:st=2.0:i=3081:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_au=on:kws=inv_precedence:nwc=5.0:sd=1:sgt=32:ss=axioms:i=1332:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_acc=on:au=on:bd=off:bsr=unit_only:cnfonf=off:fsr=off:nm=2:sos=all:i=19144:si=on:rtra=on_0"); + quick.push("lrs+1002_1:128_atotf=0.2:au=on:bd=off:cnfonf=off:plsq=on:plsqc=1:plsqr=1,2:prag=on:sd=1:ss=axioms:st=3.0:tgt=full:i=4854:si=on:rtra=on_0"); quick.push("lrs+10_3:1_au=on:fsr=off:sd=1:sgt=100:ss=axioms:i=11200:si=on:rtra=on_0"); - quick.push("dis+10_16:1_au=on:cnfonf=conj_eager:hfsq=on:hfsqc=2:piset=equals:s2a=on:sp=occurrence:ss=axioms:i=4778:si=on:rtra=on_0"); - quick.push("ott+10_1:1_afp=2000:bsr=unit_only:chr=on:hfsq=on:hfsql=off:ntd=on:piset=and:sos=on:sp=weighted_frequency:i=5377:si=on:rtra=on_0"); - quick.push("dis+21_1:6_bd=off:e2e=on:ins=5:nwc=11.0:s2a=on:i=3395:si=on:rtra=on_0"); - quick.push("lrs+10_1:4_atotf=0.4:au=on:cnfonf=off:sos=all:i=6881:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_e2e=on:nwc=5.0:sd=1:sgt=30:ss=axioms:i=1488:si=on:rtra=on_0"); + quick.push("dis+2_16:1_au=on:bd=off:cbe=off:fd=preordered:fde=unused:fsr=off:hfsq=on:nwc=10.0:i=38001:si=on:rtra=on_0"); + quick.push("lrs+1010_1:6_bd=off:cnfonf=off:hfsq=on:hfsql=off:ins=2:kws=precedence:ntd=on:sp=const_frequency:spb=units:tgt=full:i=4317:si=on:rtra=on_0"); + quick.push("lrs+2_1:3_au=on:bd=off:e2e=on:sos=on:ss=axioms:i=2642:si=on:rtra=on_0"); + quick.push("dis+10_16:1_au=on:c=on:chr=on:hfsq=on:nm=2:sac=on:sp=unary_first:ss=axioms:i=1781:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_abs=on:au=on:cnfonf=off:fde=unused:inj=on:sos=on:i=3344:si=on:rtra=on_0"); quick.push("lrs+10_2:1_fde=none:prag=on:sd=2:sgt=8:ss=axioms:tgt=ground:i=14683:si=on:rtra=on_0"); + quick.push("dis+21_4:1_av=off:bsr=unit_only:cbe=off:e2e=on:hud=1:prag=on:sp=unary_first:ss=axioms:i=4170:si=on:rtra=on_0"); + quick.push("ott+1002_2:1_au=on:cnfonf=lazy_gen:fde=none:nm=32:s2a=on:sp=const_min:i=5696:si=on:rtra=on_0"); quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=2277:si=on:rtra=on_0"); quick.push("dis+3_7:4_bsr=on:c=on:erd=off:fde=none:hud=10:lma=on:nwc=5.0:sac=on:sos=on:sp=frequency:i=8152:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_av=off:prag=on:sos=all:sp=frequency:i=7003:si=on:rtra=on_0"); quick.push("lrs+1010_1:128_au=on:fsr=off:hfsq=on:ins=3:kws=frequency:sos=all:i=1460:si=on:rtra=on_0"); - quick.push("ott+1002_1:1_au=on:fde=none:nm=10:sos=on:i=7053:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_bsd=on:cnfonf=off:hfsq=on:nm=10:piset=all_but_not_eq:s2a=on:s2at=6.0:sp=const_min:i=1319:si=on:rtra=on_0"); + quick.push("ott+1002_1:1_au=on:fde=none:nm=10:sos=on:i=6719:si=on:rtra=on_0"); quick.push("ott+1010_1:1_cnfonf=off:fd=off:rp=on:sac=on:sos=on:i=1264:si=on:rtra=on_0"); - quick.push("ott+10_1:1_s2a=on:s2at=2.0:sd=2:ss=axioms:i=767:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_cnfonf=lazy_not_be_gen:fs=off:fsr=off:nwc=10.0:ss=axioms:st=3.0:i=945:si=on:rtra=on_0"); - quick.push("lrs+10_2:3_amm=off:au=on:bd=off:fde=unused:fe=off:fsr=off:nm=16:ntd=on:s2a=on:s2at=2.0:ss=axioms:st=3.0:i=5915:si=on:rtra=on_0"); + quick.push("dis+21_1:4_avsq=on:avsqr=924271,1048576:c=on:e2e=on:fs=off:fsr=off:piset=and:plsq=on:plsqr=32,1:sd=10:sos=on:sp=unary_first:ss=axioms:st=1.5:tnu=2:i=791:si=on:rtra=on_0"); quick.push("dis+1002_1:2_au=on:bs=on:bsr=unit_only:c=on:fsr=off:hud=10:kws=inv_precedence:nm=6:ntd=on:nwc=10.0:sac=on:sos=on:i=1617:si=on:rtra=on_0"); - quick.push("ott+1002_23:4_fsd=on:ins=3:nwc=10.0:prag=on:i=1671:si=on:rtra=on_0"); - quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=8901:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_bs=on:cnfonf=lazy_not_be_gen:kws=inv_frequency:nwc=10.0:rawr=on:slsq=on:sp=weighted_frequency:uhcvi=on:i=2154:si=on:rtra=on_0"); + quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=8947:si=on:rtra=on_0"); quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=21393:si=on:rtra=on_0"); quick.push("lrs+1666_1:1_bd=off:bet=on:bsd=on:bsr=unit_only:fde=none:nwc=10.0:sp=occurrence:i=2482:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_atotf=0.2:au=on:bd=off:cnfonf=off:e2e=on:sos=all:i=788:si=on:rtra=on_0"); - quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=15001:si=on:rtra=on_0"); quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=3758:si=on:rtra=on_0"); - quick.push("lrs+1010_16:1_acc=on:anc=all_dependent:fde=unused:hfsq=on:hfsql=off:hfsqr=4,1:hud=1:ins=2:piset=all_but_not_eq:prag=on:sac=on:i=55998:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_au=on:cnfonf=off:sd=1:sgt=16:sp=occurrence:ss=axioms:i=1233:si=on:rtra=on_0"); + quick.push("ott+2_1:1_amm=off:atotf=0.4:cnfonf=off:fde=none:lma=on:nm=2:prag=on:sos=all:sp=const_max:tgt=ground:tnu=9:i=1540:si=on:rtra=on_0"); + quick.push("lrs+1010_16:1_acc=on:anc=all_dependent:fde=unused:hfsq=on:hfsql=off:hfsqr=4,1:hud=1:ins=2:piset=all_but_not_eq:prag=on:sac=on:i=57747:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_e2e=on:hfsq=on:hfsqr=1,2:hud=18:nm=2:rp=on:sos=all:sp=reverse_frequency:ss=axioms:i=10173:si=on:rtra=on_0"); quick.push("lrs+10_1:1_av=off:bd=off:kws=precedence:sos=on:sp=frequency:ss=axioms:st=3.0:i=728:si=on:rtra=on_0"); - quick.push("dis+1002_1:5_au=on:bsr=on:fde=unused:piset=not:sos=on:i=4675:si=on:rtra=on_0"); - quick.push("dis+10_1:1_hud=5:nm=16:prag=on:sac=on:sos=on:ss=axioms:tnu=2:i=1141:si=on:rtra=on_0"); quick.push("dis+2_1:1_bd=off:prag=on:sos=all:sp=frequency:ss=axioms:uhcvi=on:i=8613:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_au=on:bd=off:bet=on:fde=none:nm=20:sos=on:i=14011:si=on:rtra=on_0"); - quick.push("dis+1010_73:128_bd=preordered:fsr=off:nwc=3.0:s2a=on:s2at=2.0:i=7904:si=on:rtra=on_0"); quick.push("ott+2_1:1_abs=on:e2e=on:fsd=on:fsr=off:kws=inv_precedence:piset=not:prag=on:s2a=on:s2pl=no:sos=on:i=4730:si=on:rtra=on_0"); - quick.push("lrs+1010_4:1_amm=off:awrs=decay:bsr=on:cbe=off:e2e=on:fde=none:fe=axiom:nwc=5.0:prag=on:sac=on:sd=1:spb=goal_then_units:ss=axioms:i=10614:si=on:rtra=on_0"); - quick.push("lrs+1_1:50_bsd=on:hfsq=on:hud=5:piset=or:sac=on:sos=all:sp=reverse_arity:i=3563:si=on:rtra=on_0"); - quick.push("lrs+1002_2:1_fde=unused:kws=inv_frequency:ntd=on:i=8202:si=on:rtra=on_0"); - quick.push("ott+10_16:1_aac=none:au=on:cnfonf=off:nm=20:s2a=on:ss=axioms:i=25457:si=on:rtra=on_0"); + quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=45918:si=on:rtra=on_0"); + quick.push("dis+1010_3:1_au=on:bd=off:cnfonf=lazy_gen:fde=none:sd=1:ss=axioms:i=2205:si=on:rtra=on_0"); + quick.push("lrs+10_16:1_au=on:bd=off:sac=on:sos=all:i=9755:si=on:rtra=on_0"); + quick.push("ott+10_1:1_atotf=0.1:au=on:cnfonf=off:e2e=on:fsr=off:ins=4:kws=precedence:s2a=on:i=2566:si=on:rtra=on_0"); + quick.push("lrs+10_97:429_c=on:cnfonf=lazy_gen:fe=axiom:ntd=on:s2a=on:sp=const_frequency:tgt=ground:i=1342:si=on:rtra=on_0"); + quick.push("dis+10_2:3_fd=off:fde=none:hfsq=on:hfsqc=2:lcm=reverse:prag=on:sac=on:sos=on:i=5733:si=on:rtra=on_0"); quick.push("lrs+21_1:128_acc=model:au=on:cbe=off:e2e=on:pe=on:piset=small_set:sos=on:sp=occurrence:ss=axioms:i=1179:si=on:rtra=on_0"); - quick.push("dis+1004_1:5_cs=on:e2e=on:hfsq=on:ins=2:sos=all:i=1001:si=on:rtra=on_0"); - quick.push("ott+1010_1:4_au=on:avsq=on:avsqc=1:cnfonf=off:e2e=on:fsr=off:ins=1:nwc=10.0:s2a=on:s2at=2.5:sac=on:sp=const_min:i=4814:si=on:rtra=on_0"); - // Improves by expected 68.09668572816418 probs costing 479545 Mi + // Improves by expected 70.77019844793129 probs costing 478707 Mi // Sub-schedule for 960000Mi strat cap / 960000Mi overall limit - quick.push("lrs+1002_1:1_au=on:av=off:fd=off:fde=unused:ntd=on:sos=on:sp=frequency:ss=axioms:i=1997:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=6230:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_au=on:av=off:fd=off:fde=unused:ntd=on:sos=on:sp=frequency:ss=axioms:i=1982:si=on:rtra=on_0"); + quick.push("ott+1010_3:1_bd=preordered:cbe=off:e2e=on:fe=axiom:hud=5:s2a=on:s2agt=60:slsq=on:ss=axioms:tnu=1:i=6565:si=on:rtra=on_0"); + quick.push("lrs+10_1:128_cnfonf=off:e2e=on:fde=unused:hud=10:nm=16:pe=on:s2a=on:s2at=2.0:tgt=ground:i=2601:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=1016:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:av=off:cnfonf=lazy_not_gen_be_off:fe=axiom:kws=arity:nwc=5.0:ss=axioms:i=4969:si=on:rtra=on_0"); quick.push("lrs+1002_1:1_au=on:e2e=on:fde=none:ins=3:kws=precedence:s2a=on:s2at=5.0:sp=frequency:i=2967:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=3973:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:avsq=on:avsqr=16,1:fd=off:nm=2:sos=all:i=4192:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=12435:si=on:rtra=on_0"); + quick.push("dis+10_1:1_au=on:avsq=on:avsqr=16,1:fd=off:nm=2:sos=all:i=4245:si=on:rtra=on_0"); quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=68605:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_cnfonf=lazy_not_gen_be_off:fe=axiom:s2a=on:i=2895:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=1525:si=on:rtra=on_0"); - quick.push("dis-1010_1:1_au=on:e2e=on:hfsq=on:nm=0:s2a=on:s2at=1.5:i=15859:si=on:rtra=on_0"); - quick.push("lrs+1002_4:1_au=on:cnfonf=off:ins=1:nm=2:ntd=on:slsq=on:slsqc=4:sos=on:i=21066:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=1526:si=on:rtra=on_0"); + quick.push("dis-1010_1:1_au=on:e2e=on:hfsq=on:nm=0:s2a=on:s2at=1.5:i=20100:si=on:rtra=on_0"); + quick.push("lrs+31_1:1_au=on:bd=off:fde=none:ins=3:sos=on:sp=unary_first:i=6916:si=on:rtra=on_0"); + quick.push("lrs+1002_4:1_au=on:cnfonf=off:ins=1:nm=2:ntd=on:slsq=on:slsqc=4:sos=on:i=13084:si=on:rtra=on_0"); + quick.push("lrs+1010_1:64_acc=model:anc=all:bd=off:bsd=on:bsr=on:ins=3:ntd=on:prag=on:sos=all:i=40579:si=on:rtra=on_0"); + quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=41023:si=on:rtra=on_0"); quick.push("lrs+10_1:1_apa=on:au=on:cnfonf=off:fde=unused:fsr=off:ins=2:ntd=on:plsq=on:plsqc=1:plsqr=32,1:sac=on:sos=on:i=16648:si=on:rtra=on_0"); - quick.push("dis+1010_4:1_amm=off:bs=on:c=on:cbe=off:nm=64:nwc=6.0:s2a=on:s2at=5.0:sac=on:slsq=on:slsqr=1,8:i=4526:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=47582:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:cnfonf=lazy_not_be_gen:nwc=5.0:piset=and:plsq=on:plsqc=1:plsqr=1,1:sp=reverse_frequency:tgt=ground:i=4630:si=on:rtra=on_0"); + quick.push("ott+1010_1:64_au=on:cbe=off:cnfonf=off:nwc=10.0:s2a=on:ss=axioms:i=5101:si=on:rtra=on_0"); quick.push("dis+1002_2:3_aac=none:au=on:cbe=off:fde=none:hfsq=on:hfsqc=2:hfsqr=8,1:lcm=predicate:nm=32:prag=on:sos=on:sp=unary_first:ss=axioms:st=2.0:i=22803:si=on:rtra=on_0"); - quick.push("dis+1010_13:15_au=on:bd=off:bet=on:cnfonf=off:fe=axiom:hud=10:nm=0:ntd=on:nwc=5.0:sp=const_max:updr=off:i=1615:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:bd=off:e2e=on:fde=none:ins=1:prag=on:sos=on:i=6109:si=on:rtra=on_0"); quick.push("ott+10_1:1_bd=preordered:bsr=on:cnfonf=lazy_gen:ntd=on:nwc=10.0:sims=off:sp=const_frequency:i=3527:si=on:rtra=on_0"); quick.push("dis+1002_1:1_au=on:hfsq=on:hfsqr=5,1:hud=22:ins=3:ntd=on:nwc=3.0:s2a=on:sp=weighted_frequency:i=5561:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_e2e=on:ntd=on:nwc=5.0:sac=on:sd=1:sgt=16:spb=units:ss=axioms:i=62433:si=on:rtra=on_0"); - quick.push("lrs+1010_1:16_av=off:awrs=converge:cnfonf=off:nwc=4.0:plsq=on:plsqc=1:plsql=on:plsqr=3090729,1048576:ss=axioms:tgt=ground:i=60104:si=on:rtra=on_0"); - quick.push("lrs+10_4:1_au=on:cnfonf=lazy_pi_sigma_gen:nwc=10.0:i=6954:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_au=on:bd=off:cnfonf=off:fd=off:sos=all:i=9162:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_acc=on:au=on:bd=off:bsr=unit_only:cnfonf=off:fsr=off:nm=2:sos=all:i=40221:si=on:rtra=on_0"); - quick.push("lrs+1002_1:128_atotf=0.2:au=on:bd=off:cnfonf=off:plsq=on:plsqc=1:plsqr=1,2:prag=on:sd=1:ss=axioms:st=3.0:tgt=full:i=5241:si=on:rtra=on_0"); - quick.push("dis+2_16:1_au=on:bd=off:cbe=off:fd=preordered:fde=unused:fsr=off:hfsq=on:nwc=10.0:i=34715:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_e2e=on:fd=off:fe=off:prag=on:sos=on:i=5327:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_e2e=on:ntd=on:nwc=5.0:sac=on:sd=1:sgt=16:spb=units:ss=axioms:i=65701:si=on:rtra=on_0"); + quick.push("lrs+1010_1:16_av=off:awrs=converge:cnfonf=off:nwc=4.0:plsq=on:plsqc=1:plsql=on:plsqr=3090729,1048576:ss=axioms:tgt=ground:i=67668:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_au=on:bd=off:e2e=on:ins=3:sos=on:ss=axioms:i=1761:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_au=on:kws=inv_precedence:nwc=5.0:sd=1:sgt=32:ss=axioms:i=1332:si=on:rtra=on_0"); + quick.push("lrs+21_16:1_au=on:bd=preordered:fde=none:ins=2:nwc=10.0:ss=axioms:st=2.0:i=12174:si=on:rtra=on_0"); + quick.push("lrs+1002_1:128_atotf=0.2:au=on:bd=off:cnfonf=off:plsq=on:plsqc=1:plsqr=1,2:prag=on:sd=1:ss=axioms:st=3.0:tgt=full:i=4186:si=on:rtra=on_0"); quick.push("dis+10_16:1_au=on:cnfonf=conj_eager:hfsq=on:hfsqc=2:piset=equals:s2a=on:sp=occurrence:ss=axioms:i=26143:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_acc=model:ccuc=small_ones:cnfonf=lazy_simp:hfsq=on:nm=16:nwc=10.0:s2a=on:sac=on:sp=const_frequency:i=18181:si=on:rtra=on_0"); - quick.push("ott+2_1:1_au=on:cnfonf=off:sos=all:ss=axioms:st=3.0:i=15209:si=on:rtra=on_0"); - quick.push("lrs+2_1:3_au=on:bd=off:e2e=on:sos=on:ss=axioms:i=2642:si=on:rtra=on_0"); + quick.push("lrs+1010_1:6_bd=off:cnfonf=off:hfsq=on:hfsql=off:ins=2:kws=precedence:ntd=on:sp=const_frequency:spb=units:tgt=full:i=4317:si=on:rtra=on_0"); + quick.push("ott+2_1:1_au=on:cnfonf=off:sos=all:ss=axioms:st=3.0:i=17650:si=on:rtra=on_0"); + quick.push("dis+10_3:2_cnfonf=lazy_pi_sigma_gen:fe=off:nwc=5.0:prag=on:s2a=on:s2at=3.0:sp=frequency:i=9898:si=on:rtra=on_0"); quick.push("lrs+0_1:1_au=on:ins=3:kws=precedence:ntd=on:sos=on:sp=const_max:ss=axioms:i=6900:si=on:rtra=on_0"); - quick.push("lrs+10_1:4_atotf=0.4:au=on:cnfonf=off:sos=all:i=6020:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_cnfonf=off:erd=off:fde=none:prag=on:sos=on:i=5501:si=on:rtra=on_0"); quick.push("lrs+10_1:1_bd=off:cnfonf=lazy_simp:fde=none:sp=occurrence:i=14073:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=4066:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_abs=on:au=on:cnfonf=off:fde=unused:inj=on:sos=on:i=2406:si=on:rtra=on_0"); + quick.push("ott+1010_8:1_au=on:bd=preordered:e2e=on:ins=3:kws=inv_frequency:nwc=10.0:sp=const_min:i=7899:si=on:rtra=on_0"); + quick.push("ott+1002_2:1_au=on:cnfonf=lazy_gen:fde=none:nm=32:s2a=on:sp=const_min:i=9800:si=on:rtra=on_0"); + quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=2779:si=on:rtra=on_0"); quick.push("dis+3_7:4_bsr=on:c=on:erd=off:fde=none:hud=10:lma=on:nwc=5.0:sac=on:sos=on:sp=frequency:i=5088:si=on:rtra=on_0"); - quick.push("lrs+31_1:1_au=on:cnfonf=off:ins=3:plsq=on:sd=1:sgt=32:sos=on:ss=axioms:i=2685:si=on:rtra=on_0"); - quick.push("dis+10_4:1_atotf=0.3:bs=on:cnfonf=lazy_simp:fe=axiom:gs=on:nm=0:nwc=10.0:sp=const_frequency:i=25137:si=on:rtra=on_0"); + quick.push("dis+10_4:1_atotf=0.3:bs=on:cnfonf=lazy_simp:fe=axiom:gs=on:nm=0:nwc=10.0:sp=const_frequency:i=23452:si=on:rtra=on_0"); quick.push("lrs+32_1:2_au=on:cbe=off:lecc=0.75:s2a=on:s2at=6.0:tgt=ground:i=14769:si=on:rtra=on_0"); quick.push("lrs+1010_1:128_au=on:fsr=off:hfsq=on:ins=3:kws=frequency:sos=all:i=1460:si=on:rtra=on_0"); quick.push("ott+1002_1:1_au=on:fde=none:nm=10:sos=on:i=7053:si=on:rtra=on_0"); - quick.push("lrs+21_8:1_cnfonf=lazy_not_gen:nm=2:nwc=10.0:plsq=on:plsqc=2:plsqr=6,1:prag=on:sgt=8:sp=unary_frequency:ss=axioms:i=9529:si=on:rtra=on_0"); - quick.push("ott+1002_14:1_c=on:cnfonf=lazy_gen:er=tagged:fe=axiom:s2a=on:ss=included:i=14123:si=on:rtra=on_0"); + quick.push("lrs+21_8:1_cnfonf=lazy_not_gen:nm=2:nwc=10.0:plsq=on:plsqc=2:plsqr=6,1:prag=on:sgt=8:sp=unary_frequency:ss=axioms:i=9504:si=on:rtra=on_0"); + quick.push("ott+1002_14:1_c=on:cnfonf=lazy_gen:er=tagged:fe=axiom:s2a=on:ss=included:i=18879:si=on:rtra=on_0"); + quick.push("dis+22_1:1_au=on:fe=axiom:ntd=on:nwc=10.0:s2a=on:i=2308:si=on:rtra=on_0"); quick.push("ott+1010_1:1_cnfonf=off:fd=off:rp=on:sac=on:sos=on:i=1264:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_cnfonf=lazy_not_be_gen:fs=off:fsr=off:nwc=10.0:ss=axioms:st=3.0:i=945:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_e2e=on:sd=1:ss=axioms:st=3.0:i=2032:si=on:rtra=on_0"); - quick.push("ott+1002_23:4_fsd=on:ins=3:nwc=10.0:prag=on:i=1671:si=on:rtra=on_0"); - quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=1501:si=on:rtra=on_0"); - quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=50001:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:avsq=on:avsqr=1,16:kws=arity_squared:nm=20:sd=1:sp=const_frequency:ss=axioms:i=1895:si=on:rtra=on_0"); + quick.push("ott+1002_2:1_au=on:ins=1:nm=2:sac=on:sos=all:i=2811:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_bs=on:cnfonf=lazy_not_be_gen:kws=inv_frequency:nwc=10.0:rawr=on:slsq=on:sp=weighted_frequency:uhcvi=on:i=3159:si=on:rtra=on_0"); + quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=2778:si=on:rtra=on_0"); + quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=5318:si=on:rtra=on_0"); quick.push("lrs+1666_1:1_bd=off:bet=on:bsd=on:bsr=unit_only:fde=none:nwc=10.0:sp=occurrence:i=1458:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_atotf=0.2:au=on:bd=off:cnfonf=off:e2e=on:sos=all:i=788:si=on:rtra=on_0"); quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=20702:si=on:rtra=on_0"); - quick.push("dis+1002_1:4_cnfonf=off:e2e=on:fde=unused:fsr=off:sac=on:sfv=off:tgt=full:i=22513:si=on:rtra=on_0"); + quick.push("lrs+20_1:1_au=on:bd=off:erd=off:fde=none:sos=on:i=100206:si=on:rtra=on_0"); + quick.push("dis+1002_1:4_cnfonf=off:e2e=on:fde=unused:fsr=off:sac=on:sfv=off:tgt=full:i=15049:si=on:rtra=on_0"); quick.push("ott+1010_44:25_afr=on:c=on:cnfonf=off:e2e=on:fd=preordered:hfsq=on:hfsqc=3:hud=5:rawr=on:sp=frequency:spb=non_intro:tgt=full:tnu=1:i=7623:si=on:rtra=on_0"); quick.push("dis+10_1:1_cnfonf=off:fe=off:nwc=10.0:s2a=on:s2agt=8:sd=1:ss=axioms:st=5.0:i=8973:si=on:rtra=on_0"); quick.push("dis+1010_1:2_cnfonf=lazy_pi_sigma_gen:fe=axiom:hfsq=on:hfsqr=10,13:hud=10:sd=2:ss=axioms:i=3633:si=on:rtra=on_0"); - quick.push("lrs+1010_1:4_au=on:hfsq=on:sd=2:sgt=8:ss=axioms:i=3039:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_bd=off:fde=unused:fe=off:fs=off:fsr=off:hud=10:sos=on:i=8822:si=on:rtra=on_0"); - quick.push("dis+10_4:1_cnfonf=lazy_simp:gs=on:hud=22:sd=1:ss=axioms:tnu=1:i=2354:si=on:rtra=on_0"); + quick.push("dis+1002_1:5_au=on:bsr=on:fde=unused:piset=not:sos=on:i=4675:si=on:rtra=on_0"); quick.push("dis+1010_1:16_amm=sco:cnfonf=off:sd=1:ss=axioms:st=2.0:tgt=full:tnu=5:i=34824:si=on:rtra=on_0"); - quick.push("dis+21_1:1_au=on:c=on:cnfonf=off:e2e=on:ins=1:kws=precedence:ntd=on:sd=2:sos=on:ss=axioms:st=2.0:i=5301:si=on:rtra=on_0"); quick.push("dis+1010_5:1_cnfonf=lazy_pi_sigma_gen:fe=off:hud=10:sd=1:ss=axioms:st=1.5:i=2416:si=on:rtra=on_0"); + quick.push("lrs+1010_1:3_alpa=true:au=on:cnfonf=lazy_pi_sigma_gen:sos=on:i=1701:si=on:rtra=on_0"); quick.push("dis+2_1:1_bd=off:prag=on:sos=all:sp=frequency:ss=axioms:uhcvi=on:i=8613:si=on:rtra=on_0"); quick.push("ott+1010_16:1_cnfonf=lazy_pi_sigma_gen:fe=axiom:hud=5:prag=on:slsq=on:slsqr=4,1:i=23428:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_au=on:bd=off:bet=on:fde=none:nm=20:sos=on:i=15440:si=on:rtra=on_0"); quick.push("ott+2_4:1_au=on:cnfonf=lazy_pi_sigma_gen:hud=16:ins=3:nm=20:plsq=on:plsqc=1:plsqr=13,2:rawr=on:sp=reverse_arity:ss=axioms:st=3.0:i=24800:si=on:rtra=on_0"); quick.push("ott+2_1:1_abs=on:e2e=on:fsd=on:fsr=off:kws=inv_precedence:piset=not:prag=on:s2a=on:s2pl=no:sos=on:i=4730:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=45918:si=on:rtra=on_0"); - quick.push("lrs+1_1:50_bsd=on:hfsq=on:hud=5:piset=or:sac=on:sos=all:sp=reverse_arity:i=3563:si=on:rtra=on_0"); - quick.push("lrs+10_16:1_au=on:bd=off:sac=on:sos=all:i=13248:si=on:rtra=on_0"); - quick.push("lrs+2_3:2_au=on:cbe=off:hud=15:ins=3:kws=precedence:sp=reverse_arity:uhcvi=on:i=12501:si=on:rtra=on_0"); - quick.push("dis+10_2:3_fd=off:fde=none:hfsq=on:hfsqc=2:lcm=reverse:prag=on:sac=on:sos=on:i=6096:si=on:rtra=on_0"); + quick.push("lrs+1002_2:1_fde=unused:kws=inv_frequency:ntd=on:i=8145:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_av=off:c=on:cnfonf=off:kws=inv_precedence:piset=and:sd=1:ss=axioms:tgt=ground:tnu=2:i=20260:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_cbe=off:cnfonf=lazy_not_gen:nwc=13.0:prag=on:s2a=on:sp=weighted_frequency:i=1957:si=on:rtra=on_0"); quick.push("lrs+2_1:1_bd=off:bs=unit_only:bsd=on:cnfonf=off:fde=unused:fsr=off:hud=5:kws=inv_arity_squared:sp=const_min:i=2235:si=on:rtra=on_0"); - // Improves by expected 50.0573836977302 probs costing 959228 Mi + // Improves by expected 48.80301293339291 probs costing 958213 Mi // Sub-schedule for 960000Mi strat cap / 960000Mi overall limit - quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=6230:si=on:rtra=on_0"); + quick.push("dis+10_4:1_e2e=on:fde=none:hfsq=on:s2a=on:s2at=3.0:slsq=on:slsqc=1:i=18622:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:av=off:cnfonf=lazy_not_gen_be_off:fe=axiom:kws=arity:nwc=5.0:ss=axioms:i=4969:si=on:rtra=on_0"); quick.push("lrs+2_1:1_au=on:bsd=on:c=on:fde=none:piset=equals:sac=on:sp=const_min:i=76578:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=30267:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:avsq=on:avsqr=16,1:fd=off:nm=2:sos=all:i=5800:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=5884:si=on:rtra=on_0"); - quick.push("dis+10_1:1_cnfonf=lazy_simp:fde=unused:fsr=off:hud=10:nwc=10.0:s2a=on:s2at=4.0:sac=on:i=49493:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=25642:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=6251:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_atotf=0.1:au=on:cnfonf=off:inj=on:piset=and:s2a=on:sos=on:i=2325:si=on:rtra=on_0"); quick.push("dis+1010_1:1_fsd=on:hud=10:ntd=on:sp=reverse_arity:ss=axioms:i=13001:si=on:rtra=on_0"); - quick.push("ott+10_15:2_au=on:avsq=on:cnfonf=lazy_pi_sigma_gen:cs=on:fde=none:ins=2:sp=unary_first:i=18776:si=on:rtra=on_0"); - quick.push("lrs+21_16:1_au=on:bd=preordered:fde=none:ins=2:nwc=10.0:ss=axioms:st=2.0:i=12174:si=on:rtra=on_0"); - quick.push("lrs+1002_1:128_atotf=0.2:au=on:bd=off:cnfonf=off:plsq=on:plsqc=1:plsqr=1,2:prag=on:sd=1:ss=axioms:st=3.0:tgt=full:i=5779:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_acc=model:ccuc=small_ones:cnfonf=lazy_simp:hfsq=on:nm=16:nwc=10.0:s2a=on:sac=on:sp=const_frequency:i=18181:si=on:rtra=on_0"); + quick.push("ott+1002_1:2_au=on:hud=10:nwc=5.0:prag=on:sgt=20:sos=all:ss=axioms:st=4.0:i=16193:si=on:rtra=on_0"); + quick.push("ott+10_15:2_au=on:avsq=on:cnfonf=lazy_pi_sigma_gen:cs=on:fde=none:ins=2:sp=unary_first:i=21290:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=6900:si=on:rtra=on_0"); + quick.push("ott+1010_1:1_au=on:cnfonf=lazy_not_be_gen:nwc=5.0:piset=and:plsq=on:plsqc=1:plsqr=1,1:sp=reverse_frequency:tgt=ground:i=11020:si=on:rtra=on_0"); + quick.push("ott+10_1:1_cbe=off:cnfonf=lazy_gen:ins=3:nwc=10.0:s2a=on:i=10040:si=on:rtra=on_0"); + quick.push("ott+10_1:1_bd=preordered:bsr=on:cnfonf=lazy_gen:ntd=on:nwc=10.0:sims=off:sp=const_frequency:i=3527:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_au=on:bd=off:cnfonf=off:fd=off:sos=all:i=9162:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_acc=on:au=on:bd=off:bsr=unit_only:cnfonf=off:fsr=off:nm=2:sos=all:i=40221:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_e2e=on:fd=off:fe=off:prag=on:sos=on:i=4280:si=on:rtra=on_0"); + quick.push("ott+10_1:1_afp=2000:bsr=unit_only:chr=on:hfsq=on:hfsql=off:ntd=on:piset=and:sos=on:sp=weighted_frequency:i=5377:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_atotf=0.0319537:au=on:sos=on:sp=unary_frequency:i=6236:si=on:rtra=on_0"); + quick.push("dis+10_3:2_cnfonf=lazy_pi_sigma_gen:fe=off:nwc=5.0:prag=on:s2a=on:s2at=3.0:sp=frequency:i=9898:si=on:rtra=on_0"); quick.push("lrs+0_1:1_au=on:ins=3:kws=precedence:ntd=on:sos=on:sp=const_max:ss=axioms:i=6900:si=on:rtra=on_0"); - quick.push("lrs+10_1:4_atotf=0.4:au=on:cnfonf=off:sos=all:i=6020:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_cnfonf=off:erd=off:fde=none:prag=on:sos=on:i=5154:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_bd=off:cnfonf=lazy_simp:fde=none:sp=occurrence:i=9076:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_abs=on:au=on:cnfonf=off:fde=unused:inj=on:sos=on:i=2406:si=on:rtra=on_0"); + quick.push("ott+1002_2:1_au=on:cnfonf=lazy_gen:fde=none:nm=32:s2a=on:sp=const_min:i=9800:si=on:rtra=on_0"); quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=85280:si=on:rtra=on_0"); - quick.push("dis+3_7:4_bsr=on:c=on:erd=off:fde=none:hud=10:lma=on:nwc=5.0:sac=on:sos=on:sp=frequency:i=6161:si=on:rtra=on_0"); + quick.push("dis+3_7:4_bsr=on:c=on:erd=off:fde=none:hud=10:lma=on:nwc=5.0:sac=on:sos=on:sp=frequency:i=7190:si=on:rtra=on_0"); quick.push("lrs+10_5:1_avsq=on:avsqr=16,1:cnfonf=conj_eager:nwc=10.0:plsq=on:plsqc=1:plsqr=32,1:sd=2:spb=intro:ss=axioms:i=5762:si=on:rtra=on_0"); + quick.push("lrs+10_1:4_au=on:av=off:fde=unused:fsr=off:i=57910:si=on:rtra=on_0"); quick.push("ott+1002_1:1_au=on:fde=none:nm=10:sos=on:i=7053:si=on:rtra=on_0"); quick.push("ott+1002_14:1_c=on:cnfonf=lazy_gen:er=tagged:fe=axiom:s2a=on:ss=included:i=14123:si=on:rtra=on_0"); - quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=1501:si=on:rtra=on_0"); - quick.push("lrs+1666_1:1_bd=off:bet=on:bsd=on:bsr=unit_only:fde=none:nwc=10.0:sp=occurrence:i=1458:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_atotf=0.2:au=on:bd=off:cnfonf=off:e2e=on:sos=all:i=2275:si=on:rtra=on_0"); + quick.push("lrs+10_2:3_amm=off:au=on:bd=off:fde=unused:fe=off:fsr=off:nm=16:ntd=on:s2a=on:s2at=2.0:ss=axioms:st=3.0:i=5915:si=on:rtra=on_0"); + quick.push("ott+1002_2:1_au=on:ins=1:nm=2:sac=on:sos=all:i=2811:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_bs=on:cnfonf=lazy_not_be_gen:kws=inv_frequency:nwc=10.0:rawr=on:slsq=on:sp=weighted_frequency:uhcvi=on:i=2146:si=on:rtra=on_0"); + quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=2778:si=on:rtra=on_0"); + quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=5318:si=on:rtra=on_0"); + quick.push("lrs+1666_1:1_bd=off:bet=on:bsd=on:bsr=unit_only:fde=none:nwc=10.0:sp=occurrence:i=2482:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=7597:si=on:rtra=on_0"); quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=2946:si=on:rtra=on_0"); quick.push("lrs+1010_16:1_acc=on:anc=all_dependent:fde=unused:hfsq=on:hfsql=off:hfsqr=4,1:hud=1:ins=2:piset=all_but_not_eq:prag=on:sac=on:i=92639:si=on:rtra=on_0"); - quick.push("lrs+20_1:1_au=on:bd=off:erd=off:fde=none:sos=on:i=100206:si=on:rtra=on_0"); quick.push("ott+1010_44:25_afr=on:c=on:cnfonf=off:e2e=on:fd=preordered:hfsq=on:hfsqc=3:hud=5:rawr=on:sp=frequency:spb=non_intro:tgt=full:tnu=1:i=7601:si=on:rtra=on_0"); + quick.push("dis+1002_1:1_bs=on:e2e=on:prag=on:sos=on:ss=axioms:i=6177:si=on:rtra=on_0"); quick.push("dis+10_1:1_cnfonf=off:fe=off:nwc=10.0:s2a=on:s2agt=8:sd=1:ss=axioms:st=5.0:i=8973:si=on:rtra=on_0"); quick.push("dis+1010_1:2_cnfonf=lazy_pi_sigma_gen:fe=axiom:hfsq=on:hfsqr=10,13:hud=10:sd=2:ss=axioms:i=3633:si=on:rtra=on_0"); quick.push("dis+21_1:1_au=on:c=on:cnfonf=off:e2e=on:ins=1:kws=precedence:ntd=on:sd=2:sos=on:ss=axioms:st=2.0:i=25272:si=on:rtra=on_0"); quick.push("ott+1010_16:1_cnfonf=lazy_pi_sigma_gen:fe=axiom:hud=5:prag=on:slsq=on:slsqr=4,1:i=19281:si=on:rtra=on_0"); - quick.push("lrs+1002_1:1_au=on:bd=off:bet=on:fde=none:nm=20:sos=on:i=73841:si=on:rtra=on_0"); + quick.push("lrs+1002_1:1_au=on:bd=off:bet=on:fde=none:nm=20:sos=on:i=95283:si=on:rtra=on_0"); quick.push("ott+2_1:1_abs=on:e2e=on:fsd=on:fsr=off:kws=inv_precedence:piset=not:prag=on:s2a=on:s2pl=no:sos=on:i=4730:si=on:rtra=on_0"); + quick.push("lrs+1010_1:5_cnfonf=lazy_pi_sigma_gen:kws=precedence:nm=32:nwc=10.0:sp=const_frequency:i=5785:si=on:rtra=on_0"); + quick.push("lrs+1002_2:1_fde=unused:kws=inv_frequency:ntd=on:i=6161:si=on:rtra=on_0"); + quick.push("lrs+10_16:1_au=on:bd=off:sac=on:sos=all:i=44526:si=on:rtra=on_0"); + quick.push("lrs+10_5:1_av=off:cnfonf=lazy_pi_sigma_gen:nwc=5.0:prag=on:s2a=on:s2agt=16:i=3801:si=on:rtra=on_0"); + quick.push("dis+10_2:3_fd=off:fde=none:hfsq=on:hfsqc=2:lcm=reverse:prag=on:sac=on:sos=on:i=6096:si=on:rtra=on_0"); quick.push("ott+10_16:1_aac=none:au=on:cnfonf=off:nm=20:s2a=on:ss=axioms:i=85427:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_abs=on:au=on:cnfonf=off:fde=unused:inj=on:sos=on:i=151254:si=on:rtra=on_0"); - // Improves by expected 22.821208380897875 probs costing 959619 Mi + quick.push("lrs+2_1:1_e2e=on:prag=on:rawr=on:sos=on:sp=weighted_frequency:i=15115:si=on:rtra=on_0"); + // Improves by expected 21.639246074651492 probs costing 959472 Mi // Sub-schedule for 960000Mi strat cap / 960000Mi overall limit - quick.push("dis+10_4:1_e2e=on:fde=none:hfsq=on:s2a=on:s2at=3.0:slsq=on:slsqc=1:i=19923:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_fe=off:hud=10:sos=on:ss=axioms:i=6230:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=11325:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=68001:si=on:rtra=on_0"); - quick.push("lrs+1002_2:3_fde=none:hfsq=on:nwc=3.0:prag=on:sac=on:sd=2:sgt=32:sos=on:sp=unary_frequency:ss=axioms:i=57457:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_c=on:cnfonf=lazy_gen:fe=off:ins=2:nwc=5.0:s2a=on:sp=occurrence:i=8098:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_aac=none:au=on:fde=unused:nm=2:sac=on:sos=all:i=74409:si=on:rtra=on_0"); + quick.push("dis+1010_1:1_fsd=on:hud=10:ntd=on:sp=reverse_arity:ss=axioms:i=13001:si=on:rtra=on_0"); + quick.push("lrs+1010_1:64_acc=model:anc=all:bd=off:bsd=on:bsr=on:ins=3:ntd=on:prag=on:sos=all:i=40579:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_apa=on:au=on:cnfonf=off:fde=unused:fsr=off:ins=2:ntd=on:plsq=on:plsqc=1:plsqr=32,1:sac=on:sos=on:i=16648:si=on:rtra=on_0"); + quick.push("ott+10_15:2_au=on:avsq=on:cnfonf=lazy_pi_sigma_gen:cs=on:fde=none:ins=2:sp=unary_first:i=18776:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_au=on:cnfonf=off:e2e=on:piset=small_set:sac=on:sd=1:sos=all:ss=axioms:st=5.0:i=46089:si=on:rtra=on_0"); quick.push("dis+1002_2:3_aac=none:au=on:cbe=off:fde=none:hfsq=on:hfsqc=2:hfsqr=8,1:lcm=predicate:nm=32:prag=on:sos=on:sp=unary_first:ss=axioms:st=2.0:i=22803:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_acc=model:ccuc=small_ones:cnfonf=lazy_simp:hfsq=on:nm=16:nwc=10.0:s2a=on:sac=on:sp=const_frequency:i=26472:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_c=on:cnfonf=off:hud=15:rawr=on:sd=1:sos=all:ss=axioms:i=73159:si=on:rtra=on_0"); + quick.push("dis+1010_1:5_au=on:hfsq=on:hfsql=off:ins=3:nm=0:nwc=10.0:prag=on:sos=all:sp=const_frequency:i=11506:si=on:rtra=on_0"); + quick.push("lrs+21_16:1_au=on:bd=preordered:fde=none:ins=2:nwc=10.0:ss=axioms:st=2.0:i=12174:si=on:rtra=on_0"); + quick.push("lrs+1010_1:1_au=on:cnfonf=lazy_not_gen_be_off:inj=on:ins=2:nwc=5.0:s2a=on:i=12558:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_atotf=0.0319537:au=on:sos=on:sp=unary_frequency:i=6236:si=on:rtra=on_0"); + quick.push("dis+10_3:2_cnfonf=lazy_pi_sigma_gen:fe=off:nwc=5.0:prag=on:s2a=on:s2at=3.0:sp=frequency:i=9898:si=on:rtra=on_0"); quick.push("lrs+0_1:1_au=on:ins=3:kws=precedence:ntd=on:sos=on:sp=const_max:ss=axioms:i=6900:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_cnfonf=off:erd=off:fde=none:prag=on:sos=on:i=5501:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_bd=off:cnfonf=lazy_simp:fde=none:sp=occurrence:i=9076:si=on:rtra=on_0"); - quick.push("lrs+1010_8:1_au=on:cnfonf=lazy_pi_sigma_gen:fde=none:nwc=10.0:s2a=on:sac=on:i=264345:si=on:rtra=on_0"); - quick.push("lrs+10_1:4_au=on:av=off:fde=unused:fsr=off:i=57910:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_c=on:cnfonf=off:hud=10:nm=10:ntd=on:s2a=on:sac=on:sgt=30:ss=included:i=23873:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_abs=on:au=on:cnfonf=off:fde=unused:inj=on:sos=on:i=152983:si=on:rtra=on_0"); + quick.push("lrs+1010_4:1_acc=on:au=on:bd=off:sfv=off:ss=axioms:i=44097:si=on:rtra=on_0"); quick.push("lrs+21_8:1_cnfonf=lazy_not_gen:nm=2:nwc=10.0:plsq=on:plsqc=2:plsqr=6,1:prag=on:sgt=8:sp=unary_frequency:ss=axioms:i=9102:si=on:rtra=on_0"); - quick.push("ott+1002_14:1_c=on:cnfonf=lazy_gen:er=tagged:fe=axiom:s2a=on:ss=included:i=14123:si=on:rtra=on_0"); - quick.push("lrs+10_2:3_amm=off:au=on:bd=off:fde=unused:fe=off:fsr=off:nm=16:ntd=on:s2a=on:s2at=2.0:ss=axioms:st=3.0:i=9251:si=on:rtra=on_0"); - quick.push("dis+1002_16:1_au=on:ntd=on:sos=on:sp=frequency:uhcvi=on:i=2588:si=on:rtra=on_0"); - quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=98178:si=on:rtra=on_0"); - quick.push("dis+1002_1:1_atotf=0.3:au=on:cnfonf=off:ins=3:plsq=on:plsqr=208885,1048576:sos=all:spb=goal_then_units:i=16594:si=on:rtra=on_0"); + quick.push("ott+1002_14:1_c=on:cnfonf=lazy_gen:er=tagged:fe=axiom:s2a=on:ss=included:i=13047:si=on:rtra=on_0"); + quick.push("ott+1002_1:1_aac=none:au=on:bd=off:cnfonf=off:nm=0:s2at=3.0:s2pl=on:sac=on:sos=on:i=74001:si=on:rtra=on_0"); + quick.push("lrs+21_7:1_bd=preordered:c=on:cnfonf=lazy_gen:fde=unused:fe=axiom:hud=10:piset=not:s2at=3.0:slsq=on:slsqr=9,7:ss=axioms:i=71269:si=on:rtra=on_0"); quick.push("lrs+1666_1:1_bd=off:bet=on:bsd=on:bsr=unit_only:fde=none:nwc=10.0:sp=occurrence:i=2482:si=on:rtra=on_0"); - quick.push("lrs+2_1:1_atotf=0.2:au=on:bd=off:cnfonf=off:e2e=on:sos=all:i=4996:si=on:rtra=on_0"); - quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=5304:si=on:rtra=on_0"); + quick.push("dis+10_1:1_acc=on:e2e=on:hfsq=on:hfsqc=1:ixr=off:s2a=on:sd=2:sp=occurrence:ss=axioms:i=13229:si=on:rtra=on_0"); + quick.push("dis+10_3:1_acc=on:bs=unit_only:cnfonf=off:fe=axiom:hfsq=on:hfsqr=1,8:ins=3:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=20702:si=on:rtra=on_0"); + quick.push("lrs+666_1:1_au=on:bs=unit_only:e2e=on:sd=1:sp=frequency:ss=axioms:i=40189:si=on:rtra=on_0"); quick.push("dis+10_1:1_cnfonf=off:fe=off:nwc=10.0:s2a=on:s2agt=8:sd=1:ss=axioms:st=5.0:i=8973:si=on:rtra=on_0"); - quick.push("dis+1010_1:2_cnfonf=lazy_pi_sigma_gen:fe=axiom:hfsq=on:hfsqr=10,13:hud=10:sd=2:ss=axioms:i=3633:si=on:rtra=on_0"); - quick.push("lrs+10_1:1_aac=none:bet=on:cnfonf=lazy_not_be_gen:cond=on:sp=const_max:i=17264:si=on:rtra=on_0"); + quick.push("lrs+10_1:1_aac=none:bet=on:cnfonf=lazy_not_be_gen:cond=on:sp=const_max:i=18513:si=on:rtra=on_0"); quick.push("dis+21_1:1_au=on:c=on:cnfonf=off:e2e=on:ins=1:kws=precedence:ntd=on:sd=2:sos=on:ss=axioms:st=2.0:i=25272:si=on:rtra=on_0"); - quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=16139:si=on:rtra=on_0"); - quick.push("dis+1010_2:1_atotf=0.2:au=on:cnfonf=off:gs=on:nm=0:sd=2:ss=axioms:i=23766:si=on:rtra=on_0"); - quick.push("lrs+10_16:1_au=on:bd=off:sac=on:sos=all:i=44526:si=on:rtra=on_0"); - quick.push("dis+21_1:4_avsq=on:avsqr=924271,1048576:c=on:e2e=on:fs=off:fsr=off:piset=and:plsq=on:plsqr=32,1:sd=10:sos=on:sp=unary_first:ss=axioms:st=1.5:tnu=2:i=7230:si=on:rtra=on_0"); - quick.push("lrs+1010_1:1_c=on:cnfonf=off:hud=15:rawr=on:sd=1:sos=all:ss=axioms:i=85748:si=on:rtra=on_0"); - // Improves by expected 12.868905073390756 probs costing 951082 Mi - // Tue11 Overall score 3039.0840598543527 probs on average / budget 3828761 Mi + quick.push("ott+1010_16:1_cnfonf=lazy_pi_sigma_gen:fe=axiom:hud=5:prag=on:slsq=on:slsqr=4,1:i=23141:si=on:rtra=on_0"); + quick.push("dis+1010_73:128_bd=preordered:fsr=off:nwc=3.0:s2a=on:s2at=2.0:i=7904:si=on:rtra=on_0"); + quick.push("dis+10_1:1_au=on:e2e=on:fde=unused:nwc=5.0:sac=on:sos=all:sp=const_frequency:i=10798:si=on:rtra=on_0"); + quick.push("lrs+2_1:1_e2e=on:prag=on:rawr=on:sos=on:sp=weighted_frequency:i=25623:si=on:rtra=on_0"); + // Improves by expected 11.635409169854102 probs costing 957999 Mi + // Wed12 Overall score 3048.3069003468577 probs on average / budget 3833691 Mi + // Tue11 Overall score 3039.0840598543527 probs on average / budget 3828761 Mi // Mon10b Overall score 3037.186917544398 probs on average / budget 3813568 Mi // Mon10a Overall score 3000.409829293265 probs on average / budget 3825232 Mi // Sun09 Overall score 2938.863699793977 probs on average / budget 1918256 Mi