%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV422-1.405 : TPTP v9.3.1. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:13:40 PM UTC 2026 % Result : Timeout 299.01s 42.89s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV422-1.405 : TPTP v9.3.1. Released v3.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n011.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 11:02:15 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.75/1.94 % (3322087)Input is clausal, will run a generic CNF schedule. % 7.75/1.94 % (3322098)dis-21_1_sil=8000:lcm=predicate:random_seed=3881612856:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 7.75/1.94 % (3322098)Instruction limit reached! % 7.75/1.94 % (3322098)------------------------------ % 7.75/1.94 % (3322098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.75/1.94 % (3322098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.94 % (3322098)CaDiCaL version: 2.1.3 % 7.75/1.94 % (3322098)Termination reason: Instruction limit % 7.75/1.94 % (3322098)Termination phase: Saturation % 7.75/1.94 % (3322098)Time elapsed: 0.031 s % 7.75/1.94 % (3322098)Peak memory usage: 89 MB % 7.75/1.94 % (3322098)Instructions burned: 121 (million) % 7.75/1.94 % (3322097)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1698459404:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 7.75/1.94 % (3322095)lrs+10_1_sil=8000:sp=occurrence:random_seed=3615770272:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 7.75/1.94 % (3322092)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1190499093:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 7.75/1.94 % (3322093)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2400377851:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 7.75/1.94 % (3322094)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=917319403:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 7.75/1.94 % (3322096)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2381366299:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 7.75/1.94 % (3322095)Instruction limit reached! % 7.75/1.94 % (3322095)------------------------------ % 7.75/1.94 % (3322095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.75/1.94 % (3322095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.94 % (3322095)CaDiCaL version: 2.1.3 % 7.75/1.94 % (3322095)Termination reason: Instruction limit % 7.75/1.94 % (3322095)Termination phase: Saturation % 7.75/1.94 % (3322095)Time elapsed: 0.046 s % 7.75/1.94 % (3322095)Peak memory usage: 90 MB % 7.75/1.94 % (3322095)Instructions burned: 110 (million) % 7.75/1.94 % (3322096)Instruction limit reached! % 7.75/1.94 % (3322096)------------------------------ % 7.75/1.94 % (3322096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.75/1.94 % (3322096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.94 % (3322096)CaDiCaL version: 2.1.3 % 7.75/1.94 % (3322096)Termination reason: Instruction limit % 7.75/1.94 % (3322096)Termination phase: Saturation % 7.75/1.94 % (3322096)Time elapsed: 0.046 s % 7.75/1.94 % (3322096)Peak memory usage: 90 MB % 7.75/1.94 % (3322096)Instructions burned: 116 (million) % 7.75/1.94 % (3322097)Instruction limit reached! % 7.75/1.94 % (3322097)------------------------------ % 7.75/1.94 % (3322097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.75/1.94 % (3322097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.94 % (3322097)CaDiCaL version: 2.1.3 % 7.75/1.94 % (3322097)Termination reason: Instruction limit % 7.75/1.94 % (3322097)Termination phase: Saturation % 7.75/1.94 % (3322097)Time elapsed: 0.087 s % 7.75/1.94 % (3322097)Peak memory usage: 90 MB % 7.75/1.94 % (3322097)Instructions burned: 182 (million) % 7.75/1.94 % (3322100)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1611194883:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 7.75/1.94 % (3322100)Instruction limit reached! % 7.75/1.94 % (3322100)------------------------------ % 7.75/1.94 % (3322100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.75/1.94 % (3322100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.94 % (3322100)CaDiCaL version: 2.1.3 % 7.75/1.94 % (3322100)Termination reason: Instruction limit % 7.75/1.94 % (3322100)Termination phase: Saturation % 7.75/1.94 % (3322100)Time elapsed: 0.032 s % 7.75/1.94 % (3322100)Peak memory usage: 92 MB % 7.75/1.94 % (3322100)Instructions burned: 147 (million) % 7.75/1.94 % (3322108)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1627929337:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 19.60/3.47 % (3322107)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3054519418:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 19.60/3.47 % (3322109)lrs+10_64_to=lpo:sil=8000:random_seed=744445486:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 19.60/3.47 % (3322111)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1153400959:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi) % 19.60/3.47 % (3322107)Refutation not found, incomplete strategy % 19.60/3.47 % (3322107)------------------------------ % 19.60/3.47 % (3322107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.47 % (3322107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.47 % (3322107)CaDiCaL version: 2.1.3 % 19.60/3.47 % (3322107)Termination reason: Refutation not found, incomplete strategy % 19.60/3.47 % (3322107)Time elapsed: 0.050 s % 19.60/3.47 % (3322107)Peak memory usage: 89 MB % 19.60/3.47 % (3322107)Instructions burned: 105 (million) % 19.60/3.47 % (3322109)Instruction limit reached! % 19.60/3.47 % (3322109)------------------------------ % 19.60/3.47 % (3322109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.47 % (3322109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.47 % (3322109)CaDiCaL version: 2.1.3 % 19.60/3.47 % (3322109)Termination reason: Instruction limit % 19.60/3.47 % (3322109)Termination phase: Saturation % 19.60/3.47 % (3322109)Time elapsed: 0.052 s % 19.60/3.47 % (3322109)Peak memory usage: 91 MB % 19.60/3.47 % (3322109)Instructions burned: 128 (million) % 19.60/3.47 % (3322108)Instruction limit reached! % 19.60/3.47 % (3322108)------------------------------ % 19.60/3.47 % (3322108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.47 % (3322108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.47 % (3322108)CaDiCaL version: 2.1.3 % 19.60/3.47 % (3322108)Termination reason: Instruction limit % 19.60/3.47 % (3322108)Termination phase: Saturation % 19.60/3.47 % (3322108)Time elapsed: 0.091 s % 19.60/3.47 % (3322108)Peak memory usage: 93 MB % 19.60/3.47 % (3322108)Instructions burned: 219 (million) % 19.60/3.47 % (3322111)Instruction limit reached! % 19.60/3.47 % (3322111)------------------------------ % 19.60/3.47 % (3322111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.47 % (3322111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.47 % (3322111)CaDiCaL version: 2.1.3 % 19.60/3.47 % (3322111)Termination reason: Instruction limit % 19.60/3.47 % (3322111)Termination phase: Saturation % 19.60/3.47 % (3322111)Time elapsed: 0.051 s % 19.60/3.47 % (3322111)Peak memory usage: 89 MB % 19.60/3.47 % (3322111)Instructions burned: 196 (million) % 19.60/3.47 % (3322118)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=4231838330:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi) % 19.60/3.47 % (3322116)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=784549999:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 19.60/3.47 % (3322118)Instruction limit reached! % 19.60/3.47 % (3322118)------------------------------ % 19.60/3.47 % (3322118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.47 % (3322118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.47 % (3322118)CaDiCaL version: 2.1.3 % 19.60/3.47 % (3322118)Termination reason: Instruction limit % 19.60/3.47 % (3322118)Termination phase: Saturation % 19.60/3.47 % (3322118)Time elapsed: 0.027 s % 19.60/3.47 % (3322118)Peak memory usage: 90 MB % 19.60/3.47 % (3322118)Instructions burned: 109 (million) % 19.60/3.47 % (3322117)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3087536196:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi) % 19.60/3.47 % (3322107)------------------------------ % 19.60/3.47 % (3322107)------------------------------ % 19.60/3.47 % (3322116)Instruction limit reached! % 19.60/3.47 % (3322116)------------------------------ % 19.60/3.47 % (3322116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.60/3.47 % (3322116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.08/5.18 % (3322116)CaDiCaL version: 2.1.3 % 32.08/5.18 % (3322116)Termination reason: Instruction limit % 32.08/5.18 % (3322116)Termination phase: Saturation % 32.08/5.18 % (3322116)Time elapsed: 0.077 s % 32.08/5.18 % (3322116)Peak memory usage: 92 MB % 32.08/5.18 % (3322116)Instructions burned: 159 (million) % 32.08/5.18 % (3322121)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2909689357:i=107_2993 on theBenchmark for (2993ds/107Mi) % 32.08/5.18 % (3322121)Instruction limit reached! % 32.08/5.18 % (3322121)------------------------------ % 32.08/5.18 % (3322121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.08/5.18 % (3322121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.08/5.18 % (3322121)CaDiCaL version: 2.1.3 % 32.08/5.18 % (3322121)Termination reason: Instruction limit % 32.08/5.18 % (3322121)Termination phase: Saturation % 32.08/5.18 % (3322121)Time elapsed: 0.029 s % 32.08/5.18 % (3322121)Peak memory usage: 93 MB % 32.08/5.18 % (3322121)Instructions burned: 111 (million) % 32.08/5.18 % (3322123)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=140167144:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 32.08/5.18 % (3322124)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3884173864:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 32.08/5.18 % (3322126)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2991090200:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi) % 32.08/5.18 % (3322126)Instruction limit reached! % 32.08/5.18 % (3322126)------------------------------ % 32.08/5.18 % (3322126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.08/5.18 % (3322126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.08/5.18 % (3322126)CaDiCaL version: 2.1.3 % 32.08/5.18 % (3322126)Termination reason: Instruction limit % 32.08/5.18 % (3322126)Termination phase: Saturation % 32.08/5.18 % (3322126)Time elapsed: 0.035 s % 32.08/5.18 % (3322126)Peak memory usage: 89 MB % 32.08/5.18 % (3322126)Instructions burned: 139 (million) % 32.08/5.18 % (3322123)Instruction limit reached! % 32.08/5.18 % (3322123)------------------------------ % 32.08/5.18 % (3322123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.08/5.18 % (3322123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.08/5.18 % (3322123)CaDiCaL version: 2.1.3 % 32.08/5.18 % (3322123)Termination reason: Instruction limit % 32.08/5.18 % (3322123)Termination phase: Saturation % 32.08/5.18 % (3322123)Time elapsed: 0.105 s % 32.08/5.18 % (3322123)Peak memory usage: 88 MB % 32.08/5.18 % (3322123)Instructions burned: 243 (million) % 32.08/5.18 % (3322130)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1874196754:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 32.08/5.18 % (3322131)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1251536714:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi) % 32.08/5.18 % (3322130)Instruction limit reached! % 32.08/5.18 % (3322130)------------------------------ % 32.08/5.18 % (3322130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.08/5.18 % (3322130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.08/5.18 % (3322130)CaDiCaL version: 2.1.3 % 32.08/5.18 % (3322130)Termination reason: Instruction limit % 32.08/5.18 % (3322130)Termination phase: Saturation % 32.08/5.18 % (3322130)Time elapsed: 0.113 s % 32.08/5.18 % (3322130)Peak memory usage: 95 MB % 32.08/5.18 % (3322130)Instructions burned: 500 (million) % 32.08/5.18 % (3322131)Instruction limit reached! % 32.08/5.18 % (3322131)------------------------------ % 32.08/5.18 % (3322131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.08/5.18 % (3322131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.08/5.18 % (3322131)CaDiCaL version: 2.1.3 % 32.08/5.18 % (3322131)Termination reason: Instruction limit % 32.08/5.18 % (3322131)Termination phase: Saturation % 32.08/5.18 % (3322131)Time elapsed: 0.081 s % 32.08/5.18 % (3322131)Peak memory usage: 92 MB % 32.08/5.18 % (3322131)Instructions burned: 192 (million) % 32.08/5.18 % (3322134)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3149282989:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 47.17/7.33 % (3322134)Instruction limit reached! % 47.17/7.33 % (3322134)------------------------------ % 47.17/7.33 % (3322134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.33 % (3322134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.33 % (3322134)CaDiCaL version: 2.1.3 % 47.17/7.33 % (3322134)Termination reason: Instruction limit % 47.17/7.33 % (3322134)Termination phase: Saturation % 47.17/7.33 % (3322134)Time elapsed: 0.058 s % 47.17/7.33 % (3322134)Peak memory usage: 92 MB % 47.17/7.33 % (3322134)Instructions burned: 268 (million) % 47.17/7.33 % (3322135)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3711042201:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi) % 47.17/7.33 % (3322135)Instruction limit reached! % 47.17/7.33 % (3322135)------------------------------ % 47.17/7.33 % (3322135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.33 % (3322135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.33 % (3322135)CaDiCaL version: 2.1.3 % 47.17/7.33 % (3322135)Termination reason: Instruction limit % 47.17/7.33 % (3322135)Termination phase: Saturation % 47.17/7.33 % (3322135)Time elapsed: 0.052 s % 47.17/7.33 % (3322135)Peak memory usage: 88 MB % 47.17/7.33 % (3322135)Instructions burned: 156 (million) % 47.17/7.33 % (3322137)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1546722623:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi) % 47.17/7.33 % (3322139)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=81107294:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi) % 47.17/7.33 % (3322139)Instruction limit reached! % 47.17/7.33 % (3322139)------------------------------ % 47.17/7.33 % (3322139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.33 % (3322139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.33 % (3322139)CaDiCaL version: 2.1.3 % 47.17/7.33 % (3322139)Termination reason: Instruction limit % 47.17/7.33 % (3322139)Termination phase: Saturation % 47.17/7.33 % (3322139)Time elapsed: 0.247 s % 47.17/7.33 % (3322139)Peak memory usage: 88 MB % 47.17/7.33 % (3322139)Instructions burned: 539 (million) % 47.17/7.33 % (3322142)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1044830629:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi) % 47.17/7.33 % (3322142)Instruction limit reached! % 47.17/7.33 % (3322142)------------------------------ % 47.17/7.33 % (3322142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.33 % (3322142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.33 % (3322142)CaDiCaL version: 2.1.3 % 47.17/7.33 % (3322142)Termination reason: Instruction limit % 47.17/7.33 % (3322142)Termination phase: Saturation % 47.17/7.33 % (3322142)Time elapsed: 0.079 s % 47.17/7.33 % (3322142)Peak memory usage: 90 MB % 47.17/7.33 % (3322142)Instructions burned: 183 (million) % 47.17/7.33 % (3322144)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1821351093:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi) % 47.17/7.33 % (3322137)Instruction limit reached! % 47.17/7.33 % (3322137)------------------------------ % 47.17/7.33 % (3322137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.33 % (3322137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.33 % (3322137)CaDiCaL version: 2.1.3 % 47.17/7.33 % (3322137)Termination reason: Instruction limit % 47.17/7.33 % (3322137)Termination phase: Saturation % 47.17/7.33 % (3322137)Time elapsed: 1.114 s % 47.17/7.33 % (3322137)Peak memory usage: 152 MB % 47.17/7.33 % (3322137)Instructions burned: 3257 (million) % 47.17/7.33 % (3322146)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2301489054:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi) % 47.17/7.33 % (3322146)Instruction limit reached! % 47.17/7.33 % (3322146)------------------------------ % 47.17/7.33 % (3322146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.17/7.33 % (3322146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.17/7.33 % (3322146)CaDiCaL version: 2.1.3 % 69.59/10.57 % (3322146)Termination reason: Instruction limit % 69.59/10.57 % (3322146)Termination phase: Saturation % 69.59/10.57 % (3322146)Time elapsed: 0.098 s % 69.59/10.57 % (3322146)Peak memory usage: 96 MB % 69.59/10.57 % (3322146)Instructions burned: 413 (million) % 69.59/10.57 % (3322148)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1818253103:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi) % 69.59/10.57 % (3322117)Instruction limit reached! % 69.59/10.57 % (3322117)------------------------------ % 69.59/10.57 % (3322117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.59/10.57 % (3322117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.59/10.57 % (3322117)CaDiCaL version: 2.1.3 % 69.59/10.57 % (3322117)Termination reason: Instruction limit % 69.59/10.57 % (3322117)Termination phase: Saturation % 69.59/10.57 % (3322117)Time elapsed: 2.323 s % 69.59/10.57 % (3322117)Peak memory usage: 153 MB % 69.59/10.57 % (3322117)Instructions burned: 3394 (million) % 69.59/10.57 % (3322150)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3721752699:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi) % 69.59/10.57 % (3322150)Instruction limit reached! % 69.59/10.57 % (3322150)------------------------------ % 69.59/10.57 % (3322150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.59/10.57 % (3322150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.59/10.57 % (3322150)CaDiCaL version: 2.1.3 % 69.59/10.57 % (3322150)Termination reason: Instruction limit % 69.59/10.57 % (3322150)Termination phase: Saturation % 69.59/10.57 % (3322150)Time elapsed: 0.154 s % 69.59/10.57 % (3322150)Peak memory usage: 94 MB % 69.59/10.57 % (3322150)Instructions burned: 305 (million) % 69.59/10.57 % (3322152)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3360500920:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi) % 69.59/10.57 % (3322152)Instruction limit reached! % 69.59/10.57 % (3322152)------------------------------ % 69.59/10.57 % (3322152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.59/10.57 % (3322152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.59/10.57 % (3322152)CaDiCaL version: 2.1.3 % 69.59/10.57 % (3322152)Termination reason: Instruction limit % 69.59/10.57 % (3322152)Termination phase: Saturation % 69.59/10.57 % (3322152)Time elapsed: 0.338 s % 69.59/10.57 % (3322152)Peak memory usage: 96 MB % 69.59/10.57 % (3322152)Instructions burned: 720 (million) % 69.59/10.57 % (3322154)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2836061870:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi) % 69.59/10.57 % (3322154)Instruction limit reached! % 69.59/10.57 % (3322154)------------------------------ % 69.59/10.57 % (3322154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.59/10.57 % (3322154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.59/10.57 % (3322154)CaDiCaL version: 2.1.3 % 69.59/10.57 % (3322154)Termination reason: Instruction limit % 69.59/10.57 % (3322154)Termination phase: Saturation % 69.59/10.57 % (3322154)Time elapsed: 0.219 s % 69.59/10.57 % (3322154)Peak memory usage: 92 MB % 69.59/10.57 % (3322154)Instructions burned: 599 (million) % 69.59/10.57 % (3322156)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3501892526:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi) % 69.59/10.57 % (3322124)Instruction limit reached! % 69.59/10.57 % (3322124)------------------------------ % 69.59/10.57 % (3322124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.59/10.57 % (3322124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.59/10.57 % (3322124)CaDiCaL version: 2.1.3 % 69.59/10.57 % (3322124)Termination reason: Instruction limit % 69.59/10.57 % (3322124)Termination phase: Saturation % 69.59/10.57 % (3322124)Time elapsed: 3.505 s % 69.59/10.57 % (3322124)Peak memory usage: 167 MB % 69.59/10.57 % (3322124)Instructions burned: 5209 (million) % 69.59/10.57 % (3322158)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1847046735:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi) % 96.80/14.37 % (3322148)Instruction limit reached! % 96.80/14.37 % (3322148)------------------------------ % 96.80/14.37 % (3322148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.80/14.37 % (3322148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.80/14.37 % (3322148)CaDiCaL version: 2.1.3 % 96.80/14.37 % (3322148)Termination reason: Instruction limit % 96.80/14.37 % (3322148)Termination phase: Saturation % 96.80/14.37 % (3322148)Time elapsed: 2.747 s % 96.80/14.37 % (3322148)Peak memory usage: 194 MB % 96.80/14.37 % (3322148)Instructions burned: 8482 (million) % 96.80/14.37 % (3322161)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1096447654:i=2088:bd=preordered:av=off_2943 on theBenchmark for (2943ds/2088Mi) % 96.80/14.37 % (3322158)Instruction limit reached! % 96.80/14.37 % (3322158)------------------------------ % 96.80/14.37 % (3322158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.80/14.37 % (3322158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.80/14.37 % (3322158)CaDiCaL version: 2.1.3 % 96.80/14.37 % (3322158)Termination reason: Instruction limit % 96.80/14.37 % (3322158)Termination phase: Saturation % 96.80/14.37 % (3322158)Time elapsed: 1.349 s % 96.80/14.37 % (3322158)Peak memory usage: 135 MB % 96.80/14.37 % (3322158)Instructions burned: 1998 (million) % 96.80/14.37 % (3322163)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=396486446:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi) % 96.80/14.37 % (3322156)Instruction limit reached! % 96.80/14.37 % (3322156)------------------------------ % 96.80/14.37 % (3322156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.80/14.37 % (3322156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.80/14.37 % (3322156)CaDiCaL version: 2.1.3 % 96.80/14.37 % (3322156)Termination reason: Instruction limit % 96.80/14.37 % (3322156)Termination phase: Saturation % 96.80/14.37 % (3322156)Time elapsed: 1.977 s % 96.80/14.37 % (3322156)Peak memory usage: 146 MB % 96.80/14.37 % (3322156)Instructions burned: 2991 (million) % 96.80/14.37 % (3322163)Instruction limit reached! % 96.80/14.37 % (3322163)------------------------------ % 96.80/14.37 % (3322163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.80/14.37 % (3322163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.80/14.37 % (3322163)CaDiCaL version: 2.1.3 % 96.80/14.37 % (3322163)Termination reason: Instruction limit % 96.80/14.37 % (3322163)Termination phase: Saturation % 96.80/14.37 % (3322163)Time elapsed: 0.415 s % 96.80/14.37 % (3322163)Peak memory usage: 99 MB % 96.80/14.37 % (3322163)Instructions burned: 1100 (million) % 96.80/14.37 % (3322165)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1223558947:i=433:bd=preordered_2936 on theBenchmark for (2936ds/433Mi) % 96.80/14.37 % (3322161)Instruction limit reached! % 96.80/14.37 % (3322161)------------------------------ % 96.80/14.37 % (3322161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.80/14.37 % (3322161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.80/14.37 % (3322161)CaDiCaL version: 2.1.3 % 96.80/14.37 % (3322161)Termination reason: Instruction limit % 96.80/14.37 % (3322161)Termination phase: Saturation % 96.80/14.37 % (3322161)Time elapsed: 0.729 s % 96.80/14.37 % (3322161)Peak memory usage: 141 MB % 96.80/14.37 % (3322161)Instructions burned: 2089 (million) % 96.80/14.37 % (3322166)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1954294091:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2935 on theBenchmark for (2935ds/2942Mi) % 96.80/14.37 % (3322168)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3287733251:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2934 on theBenchmark for (2934ds/6922Mi) % 96.80/14.37 % (3322165)Instruction limit reached! % 96.80/14.37 % (3322165)------------------------------ % 96.80/14.37 % (3322165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.80/14.37 % (3322165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.80/14.37 % (3322165)CaDiCaL version: 2.1.3 % 96.80/14.37 % (3322165)Termination reason: Instruction limit % 96.80/14.37 % (3322165)Termination phase: Saturation % 96.80/14.37 % (3322165)Time elapsed: 0.168 s % 114.34/16.87 % (3322165)Peak memory usage: 91 MB % 114.34/16.87 % (3322165)Instructions burned: 434 (million) % 114.34/16.87 % (3322171)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2408926939:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2933 on theBenchmark for (2933ds/596Mi) % 114.34/16.87 % (3322171)Instruction limit reached! % 114.34/16.87 % (3322171)------------------------------ % 114.34/16.87 % (3322171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.34/16.87 % (3322171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.87 % (3322171)CaDiCaL version: 2.1.3 % 114.34/16.87 % (3322171)Termination reason: Instruction limit % 114.34/16.87 % (3322171)Termination phase: Saturation % 114.34/16.87 % (3322171)Time elapsed: 0.303 s % 114.34/16.87 % (3322171)Peak memory usage: 96 MB % 114.34/16.87 % (3322171)Instructions burned: 597 (million) % 114.34/16.87 % (3322173)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2494056518:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2928 on theBenchmark for (2928ds/4123Mi) % 114.34/16.87 % (3322166)Instruction limit reached! % 114.34/16.87 % (3322166)------------------------------ % 114.34/16.87 % (3322166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.34/16.87 % (3322166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.87 % (3322166)CaDiCaL version: 2.1.3 % 114.34/16.87 % (3322166)Termination reason: Instruction limit % 114.34/16.87 % (3322166)Termination phase: Saturation % 114.34/16.87 % (3322166)Time elapsed: 1.812 s % 114.34/16.87 % (3322166)Peak memory usage: 158 MB % 114.34/16.87 % (3322166)Instructions burned: 2943 (million) % 114.34/16.87 % (3322175)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2835955070:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2915 on theBenchmark for (2915ds/16411Mi) % 114.34/16.87 % (3322144)Instruction limit reached! % 114.34/16.87 % (3322144)------------------------------ % 114.34/16.87 % (3322144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.34/16.87 % (3322144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.88 % (3322144)CaDiCaL version: 2.1.3 % 114.34/16.88 % (3322144)Termination reason: Instruction limit % 114.34/16.88 % (3322144)Termination phase: Saturation % 114.34/16.88 % (3322144)Time elapsed: 7.059 s % 114.34/16.88 % (3322144)Peak memory usage: 207 MB % 114.34/16.88 % (3322144)Instructions burned: 10307 (million) % 114.34/16.88 % (3322168)Instruction limit reached! % 114.34/16.88 % (3322168)------------------------------ % 114.34/16.88 % (3322168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.34/16.88 % (3322168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.88 % (3322168)CaDiCaL version: 2.1.3 % 114.34/16.88 % (3322168)Termination reason: Instruction limit % 114.34/16.88 % (3322168)Termination phase: Saturation % 114.34/16.88 % (3322168)Time elapsed: 2.722 s % 114.34/16.88 % (3322168)Peak memory usage: 178 MB % 114.34/16.88 % (3322168)Instructions burned: 6923 (million) % 114.34/16.88 % (3322177)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=4218229430:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2906 on theBenchmark for (2906ds/1670Mi) % 114.34/16.88 % (3322178)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3553105920:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2906 on theBenchmark for (2906ds/1722Mi) % 114.34/16.88 % (3322173)Instruction limit reached! % 114.34/16.88 % (3322173)------------------------------ % 114.34/16.88 % (3322173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.34/16.88 % (3322173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.88 % (3322173)CaDiCaL version: 2.1.3 % 114.34/16.88 % (3322173)Termination reason: Instruction limit % 114.34/16.88 % (3322173)Termination phase: Saturation % 114.34/16.88 % (3322173)Time elapsed: 2.437 s % 114.34/16.88 % (3322173)Peak memory usage: 161 MB % 114.34/16.88 % (3322173)Instructions burned: 4124 (million) % 114.34/16.88 % (3322181)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3118115353:cts=off:cond=on:i=9530:bs=on:fsd=on_2902 on theBenchmark for (2902ds/9530Mi) % 141.57/20.65 % (3322178)Instruction limit reached! % 141.57/20.65 % (3322178)------------------------------ % 141.57/20.65 % (3322178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.57/20.65 % (3322178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.57/20.65 % (3322178)CaDiCaL version: 2.1.3 % 141.57/20.65 % (3322178)Termination reason: Instruction limit % 141.57/20.65 % (3322178)Termination phase: Saturation % 141.57/20.65 % (3322178)Time elapsed: 0.637 s % 141.57/20.65 % (3322178)Peak memory usage: 136 MB % 141.57/20.65 % (3322178)Instructions burned: 1725 (million) % 141.57/20.65 % (3322183)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=94284212:st=2:i=4495:sd=10:ss=included_2898 on theBenchmark for (2898ds/4495Mi) % 141.57/20.65 % (3322177)Instruction limit reached! % 141.57/20.65 % (3322177)------------------------------ % 141.57/20.65 % (3322177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.57/20.65 % (3322177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.57/20.65 % (3322177)CaDiCaL version: 2.1.3 % 141.57/20.65 % (3322177)Termination reason: Instruction limit % 141.57/20.65 % (3322177)Termination phase: Saturation % 141.57/20.65 % (3322177)Time elapsed: 1.183 s % 141.57/20.65 % (3322177)Peak memory usage: 135 MB % 141.57/20.65 % (3322177)Instructions burned: 1671 (million) % 141.57/20.65 % (3322185)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=86960951:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2893 on theBenchmark for (2893ds/4920Mi) % 141.57/20.65 % (3322183)Instruction limit reached! % 141.57/20.65 % (3322183)------------------------------ % 141.57/20.65 % (3322183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.57/20.65 % (3322183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.57/20.65 % (3322183)CaDiCaL version: 2.1.3 % 141.57/20.65 % (3322183)Termination reason: Instruction limit % 141.57/20.65 % (3322183)Termination phase: Saturation % 141.57/20.65 % (3322183)Time elapsed: 1.593 s % 141.57/20.65 % (3322183)Peak memory usage: 158 MB % 141.57/20.65 % (3322183)Instructions burned: 4496 (million) % 141.57/20.65 % (3322187)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2651509415:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2880 on theBenchmark for (2880ds/2083Mi) % 141.57/20.65 % (3322187)Instruction limit reached! % 141.57/20.65 % (3322187)------------------------------ % 141.57/20.65 % (3322187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.57/20.65 % (3322187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.57/20.65 % (3322187)CaDiCaL version: 2.1.3 % 141.57/20.65 % (3322187)Termination reason: Instruction limit % 141.57/20.65 % (3322187)Termination phase: Saturation % 141.57/20.65 % (3322187)Time elapsed: 0.707 s % 141.57/20.65 % (3322187)Peak memory usage: 137 MB % 141.57/20.65 % (3322187)Instructions burned: 2085 (million) % 141.57/20.65 % (3322189)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1395473056:i=4629:av=off:gsp=on_2872 on theBenchmark for (2872ds/4629Mi) % 141.57/20.65 % (3322185)Instruction limit reached! % 141.57/20.65 % (3322185)------------------------------ % 141.57/20.65 % (3322185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.57/20.65 % (3322185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.57/20.65 % (3322185)CaDiCaL version: 2.1.3 % 141.57/20.65 % (3322185)Termination reason: Instruction limit % 141.57/20.65 % (3322185)Termination phase: Saturation % 141.57/20.65 % (3322185)Time elapsed: 2.742 s % 141.57/20.65 % (3322185)Peak memory usage: 179 MB % 141.57/20.65 % (3322185)Instructions burned: 4922 (million) % 141.57/20.65 % (3322181)Instruction limit reached! % 141.57/20.65 % (3322181)------------------------------ % 141.57/20.65 % (3322181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.57/20.65 % (3322181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.57/20.65 % (3322181)CaDiCaL version: 2.1.3 % 141.57/20.65 % (3322181)Termination reason: Instruction limit % 141.57/20.65 % (3322181)Termination phase: Saturation % 141.57/20.65 % (3322181)Time elapsed: 3.687 s % 141.57/20.65 % (3322181)Peak memory usage: 139 MB % 141.57/20.65 % (3322181)Instructions burned: 9532 (million) % 141.57/20.65 % (3322191)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1443002491:i=1258:av=off_2864 on theBenchmark for (2864ds/1258Mi) % 155.23/22.65 % (3322192)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2664550860:i=7343:av=off:ss=included_2863 on theBenchmark for (2863ds/7343Mi) % 155.23/22.65 % (3322189)Instruction limit reached! % 155.23/22.65 % (3322189)------------------------------ % 155.23/22.65 % (3322189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.23/22.65 % (3322189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.23/22.65 % (3322189)CaDiCaL version: 2.1.3 % 155.23/22.65 % (3322189)Termination reason: Instruction limit % 155.23/22.65 % (3322189)Termination phase: Saturation % 155.23/22.65 % (3322189)Time elapsed: 1.237 s % 155.23/22.65 % (3322189)Peak memory usage: 138 MB % 155.23/22.65 % (3322189)Instructions burned: 4630 (million) % 155.23/22.65 % (3322195)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1366450079:i=1325:sd=2:ss=axioms:sgt=16_2858 on theBenchmark for (2858ds/1325Mi) % 155.23/22.65 % (3322191)Instruction limit reached! % 155.23/22.65 % (3322191)------------------------------ % 155.23/22.65 % (3322191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.23/22.65 % (3322191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.23/22.65 % (3322191)CaDiCaL version: 2.1.3 % 155.23/22.65 % (3322191)Termination reason: Instruction limit % 155.23/22.65 % (3322191)Termination phase: Saturation % 155.23/22.65 % (3322191)Time elapsed: 0.637 s % 155.23/22.65 % (3322191)Peak memory usage: 113 MB % 155.23/22.65 % (3322191)Instructions burned: 1258 (million) % 155.23/22.65 % (3322195)Instruction limit reached! % 155.23/22.65 % (3322195)------------------------------ % 155.23/22.65 % (3322195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.23/22.65 % (3322195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.23/22.65 % (3322195)CaDiCaL version: 2.1.3 % 155.23/22.65 % (3322195)Termination reason: Instruction limit % 155.23/22.65 % (3322195)Termination phase: Saturation % 155.23/22.65 % (3322195)Time elapsed: 0.249 s % 155.23/22.65 % (3322195)Peak memory usage: 96 MB % 155.23/22.65 % (3322195)Instructions burned: 1333 (million) % 155.23/22.65 % (3322197)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2080385010:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2856 on theBenchmark for (2856ds/2646Mi) % 155.23/22.65 % (3322198)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3083851850:i=1489:sd=2:ep=R:ss=axioms_2854 on theBenchmark for (2854ds/1489Mi) % 155.23/22.65 % (3322198)Instruction limit reached! % 155.23/22.65 % (3322198)------------------------------ % 155.23/22.65 % (3322198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.23/22.65 % (3322198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.23/22.65 % (3322198)CaDiCaL version: 2.1.3 % 155.23/22.65 % (3322198)Termination reason: Instruction limit % 155.23/22.65 % (3322198)Termination phase: Saturation % 155.23/22.65 % (3322198)Time elapsed: 0.533 s % 155.23/22.65 % (3322198)Peak memory usage: 132 MB % 155.23/22.65 % (3322198)Instructions burned: 1489 (million) % 155.23/22.65 % (3322201)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=1061276966:i=1503_2848 on theBenchmark for (2848ds/1503Mi) % 155.23/22.65 % (3322201)Instruction limit reached! % 155.23/22.65 % (3322201)------------------------------ % 155.23/22.65 % (3322201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.23/22.65 % (3322201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.23/22.65 % (3322201)CaDiCaL version: 2.1.3 % 155.23/22.65 % (3322201)Termination reason: Instruction limit % 155.23/22.65 % (3322201)Termination phase: Saturation % 155.23/22.65 % (3322201)Time elapsed: 0.569 s % 155.23/22.65 % (3322201)Peak memory usage: 134 MB % 155.23/22.65 % (3322201)Instructions burned: 1505 (million) % 155.23/22.65 % (3322203)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=518029596:i=13942:kws=frequency_2841 on theBenchmark for (2841ds/13942Mi) % 155.23/22.65 % (3322197)Instruction limit reached! % 155.23/22.65 % (3322197)------------------------------ % 155.23/22.65 % (3322197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.23/22.65 % (3322197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.76/25.35 % (3322197)CaDiCaL version: 2.1.3 % 174.76/25.35 % (3322197)Termination reason: Instruction limit % 174.76/25.35 % (3322197)Termination phase: Saturation % 174.76/25.35 % (3322197)Time elapsed: 1.698 s % 174.76/25.35 % (3322197)Peak memory usage: 139 MB % 174.76/25.35 % (3322197)Instructions burned: 2646 (million) % 174.76/25.35 % (3322205)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3603552802:i=3604:fsr=off:er=filter_2837 on theBenchmark for (2837ds/3604Mi) % 174.76/25.35 % (3322175)Instruction limit reached! % 174.76/25.35 % (3322175)------------------------------ % 174.76/25.35 % (3322175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.76/25.35 % (3322175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.76/25.35 % (3322175)CaDiCaL version: 2.1.3 % 174.76/25.35 % (3322175)Termination reason: Instruction limit % 174.76/25.35 % (3322175)Termination phase: Saturation % 174.76/25.35 % (3322175)Time elapsed: 8.907 s % 174.76/25.35 % (3322175)Peak memory usage: 180 MB % 174.76/25.35 % (3322175)Instructions burned: 16411 (million) % 174.76/25.35 % (3322207)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=42983592:i=1876:sd=1:ss=included:sgt=32_2824 on theBenchmark for (2824ds/1876Mi) % 174.76/25.35 % (3322205)Instruction limit reached! % 174.76/25.35 % (3322205)------------------------------ % 174.76/25.35 % (3322205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.76/25.35 % (3322205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.76/25.35 % (3322205)CaDiCaL version: 2.1.3 % 174.76/25.35 % (3322205)Termination reason: Instruction limit % 174.76/25.35 % (3322205)Termination phase: Saturation % 174.76/25.35 % (3322205)Time elapsed: 2.413 s % 174.76/25.35 % (3322205)Peak memory usage: 155 MB % 174.76/25.35 % (3322205)Instructions burned: 3604 (million) % 174.76/25.35 % (3322207)Instruction limit reached! % 174.76/25.35 % (3322207)------------------------------ % 174.76/25.35 % (3322207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.76/25.35 % (3322207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.76/25.35 % (3322207)CaDiCaL version: 2.1.3 % 174.76/25.35 % (3322207)Termination reason: Instruction limit % 174.76/25.35 % (3322207)Termination phase: Saturation % 174.76/25.35 % (3322207)Time elapsed: 1.186 s % 174.76/25.35 % (3322207)Peak memory usage: 138 MB % 174.76/25.35 % (3322207)Instructions burned: 1877 (million) % 174.76/25.35 % (3322192)Instruction limit reached! % 174.76/25.35 % (3322192)------------------------------ % 174.76/25.35 % (3322192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.76/25.35 % (3322192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.76/25.35 % (3322192)CaDiCaL version: 2.1.3 % 174.76/25.35 % (3322192)Termination reason: Instruction limit % 174.76/25.35 % (3322192)Termination phase: Saturation % 174.76/25.35 % (3322192)Time elapsed: 5.161 s % 174.76/25.35 % (3322192)Peak memory usage: 184 MB % 174.76/25.35 % (3322192)Instructions burned: 7343 (million) % 174.76/25.35 % (3322209)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1536989319:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2811 on theBenchmark for (2811ds/1932Mi) % 174.76/25.35 % (3322210)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=553796809:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2811 on theBenchmark for (2811ds/1980Mi) % 174.76/25.35 % (3322211)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=3207817823:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2810 on theBenchmark for (2810ds/3902Mi) % 174.76/25.35 % (3322211)Refutation not found, incomplete strategy % 174.76/25.35 % (3322211)------------------------------ % 174.76/25.35 % (3322211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.76/25.35 % (3322211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.76/25.35 % (3322211)CaDiCaL version: 2.1.3 % 174.76/25.35 % (3322211)Termination reason: Refutation not found, incomplete strategy % 174.76/25.35 % (3322211)Time elapsed: 0.632 s % 174.76/25.35 % (3322211)Peak memory usage: 130 MB % 174.76/25.35 % (3322211)Instructions burned: 979 (million) % 174.76/25.35 % (3322211)------------------------------ % 198.40/28.78 % (3322211)------------------------------ % 198.40/28.78 % (3322209)Refutation not found, incomplete strategy % 198.40/28.78 % (3322209)------------------------------ % 198.40/28.78 % (3322209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.40/28.78 % (3322209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.40/28.78 % (3322209)CaDiCaL version: 2.1.3 % 198.40/28.78 % (3322209)Termination reason: Refutation not found, incomplete strategy % 198.40/28.78 % (3322209)Time elapsed: 1.130 s % 198.40/28.78 % (3322209)Peak memory usage: 136 MB % 198.40/28.78 % (3322209)Instructions burned: 1649 (million) % 198.40/28.78 % (3322215)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2837538089:avsq=on:i=3916:aac=none:amm=off_2800 on theBenchmark for (2800ds/3916Mi) % 198.40/28.78 % (3322210)Instruction limit reached! % 198.40/28.78 % (3322210)------------------------------ % 198.40/28.78 % (3322210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.40/28.78 % (3322210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.40/28.78 % (3322210)CaDiCaL version: 2.1.3 % 198.40/28.78 % (3322210)Termination reason: Instruction limit % 198.40/28.78 % (3322210)Termination phase: Saturation % 198.40/28.78 % (3322210)Time elapsed: 1.273 s % 198.40/28.78 % (3322210)Peak memory usage: 139 MB % 198.40/28.78 % (3322210)Instructions burned: 1982 (million) % 198.40/28.78 % (3322209)------------------------------ % 198.40/28.78 % (3322209)------------------------------ % 198.40/28.78 % (3322217)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=632898460:cond=on:i=3940:av=off:er=known_2796 on theBenchmark for (2796ds/3940Mi) % 198.40/28.78 % (3322218)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1660080932:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2796 on theBenchmark for (2796ds/3980Mi) % 198.40/28.78 % (3322203)Instruction limit reached! % 198.40/28.78 % (3322203)------------------------------ % 198.40/28.78 % (3322203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.40/28.78 % (3322203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.40/28.78 % (3322203)CaDiCaL version: 2.1.3 % 198.40/28.78 % (3322203)Termination reason: Instruction limit % 198.40/28.78 % (3322203)Termination phase: Saturation % 198.40/28.78 % (3322203)Time elapsed: 4.702 s % 198.40/28.78 % (3322203)Peak memory usage: 195 MB % 198.40/28.78 % (3322203)Instructions burned: 13943 (million) % 198.40/28.78 % (3322221)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=4099035109:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2792 on theBenchmark for (2792ds/2087Mi) % 198.40/28.78 % (3322221)Instruction limit reached! % 198.40/28.78 % (3322221)------------------------------ % 198.40/28.78 % (3322221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.40/28.78 % (3322221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.40/28.78 % (3322221)CaDiCaL version: 2.1.3 % 198.40/28.78 % (3322221)Termination reason: Instruction limit % 198.40/28.78 % (3322221)Termination phase: Saturation % 198.40/28.78 % (3322221)Time elapsed: 0.669 s % 198.40/28.78 % (3322221)Peak memory usage: 135 MB % 198.40/28.78 % (3322221)Instructions burned: 2090 (million) % 198.40/28.78 % (3322223)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1212450541:cts=off:cond=on:i=4272:bs=on:fsd=on_2784 on theBenchmark for (2784ds/4272Mi) % 198.40/28.78 % (3322215)Instruction limit reached! % 198.40/28.78 % (3322215)------------------------------ % 198.40/28.78 % (3322215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.40/28.78 % (3322215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.40/28.78 % (3322215)CaDiCaL version: 2.1.3 % 198.40/28.78 % (3322215)Termination reason: Instruction limit % 198.40/28.78 % (3322215)Termination phase: Saturation % 198.40/28.78 % (3322215)Time elapsed: 1.660 s % 198.40/28.78 % (3322215)Peak memory usage: 99 MB % 198.40/28.78 % (3322215)Instructions burned: 3917 (million) % 198.40/28.78 % (3322225)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3097923505:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2781 on theBenchmark for (2781ds/2197Mi) % 245.14/35.20 % (3322223)Instruction limit reached! % 245.14/35.20 % (3322223)------------------------------ % 245.14/35.20 % (3322223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.14/35.20 % (3322223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.14/35.20 % (3322223)CaDiCaL version: 2.1.3 % 245.14/35.20 % (3322223)Termination reason: Instruction limit % 245.14/35.20 % (3322223)Termination phase: Saturation % 245.14/35.20 % (3322223)Time elapsed: 1.160 s % 245.14/35.20 % (3322223)Peak memory usage: 140 MB % 245.14/35.20 % (3322223)Instructions burned: 4274 (million) % 245.14/35.20 % (3322218)Instruction limit reached! % 245.14/35.20 % (3322218)------------------------------ % 245.14/35.20 % (3322218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.14/35.20 % (3322218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.14/35.20 % (3322218)CaDiCaL version: 2.1.3 % 245.14/35.20 % (3322218)Termination reason: Instruction limit % 245.14/35.20 % (3322218)Termination phase: Saturation % 245.14/35.20 % (3322218)Time elapsed: 2.366 s % 245.14/35.20 % (3322218)Peak memory usage: 155 MB % 245.14/35.20 % (3322218)Instructions burned: 3982 (million) % 245.14/35.20 % (3322227)dis+21_1_sil=8000:spb=goal_then_units:random_seed=72192016:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2771 on theBenchmark for (2771ds/6508Mi) % 245.14/35.20 % (3322217)Instruction limit reached! % 245.14/35.20 % (3322217)------------------------------ % 245.14/35.20 % (3322217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.14/35.20 % (3322217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.14/35.20 % (3322217)CaDiCaL version: 2.1.3 % 245.14/35.20 % (3322217)Termination reason: Instruction limit % 245.14/35.20 % (3322217)Termination phase: Saturation % 245.14/35.20 % (3322217)Time elapsed: 2.604 s % 245.14/35.20 % (3322217)Peak memory usage: 155 MB % 245.14/35.20 % (3322217)Instructions burned: 3940 (million) % 245.14/35.20 % (3322228)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1433848509:i=2330:fgj=on:av=off:fsr=off_2770 on theBenchmark for (2770ds/2330Mi) % 245.14/35.20 % (3322231)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=3869674462:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2769 on theBenchmark for (2769ds/7592Mi) % 245.14/35.20 % (3322225)Instruction limit reached! % 245.14/35.20 % (3322225)------------------------------ % 245.14/35.20 % (3322225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.14/35.20 % (3322225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.14/35.20 % (3322225)CaDiCaL version: 2.1.3 % 245.14/35.20 % (3322225)Termination reason: Instruction limit % 245.14/35.20 % (3322225)Termination phase: Saturation % 245.14/35.20 % (3322225)Time elapsed: 1.492 s % 245.14/35.20 % (3322225)Peak memory usage: 139 MB % 245.14/35.20 % (3322225)Instructions burned: 2198 (million) % 245.14/35.20 % (3322233)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=3186369981:i=2693:kws=precedence:ins=1:av=off_2765 on theBenchmark for (2765ds/2693Mi) % 245.14/35.20 % (3322228)Instruction limit reached! % 245.14/35.20 % (3322228)------------------------------ % 245.14/35.20 % (3322228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.14/35.20 % (3322228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.14/35.20 % (3322228)CaDiCaL version: 2.1.3 % 245.14/35.20 % (3322228)Termination reason: Instruction limit % 245.14/35.20 % (3322228)Termination phase: Saturation % 245.14/35.20 % (3322228)Time elapsed: 1.420 s % 245.14/35.20 % (3322228)Peak memory usage: 142 MB % 245.14/35.20 % (3322228)Instructions burned: 2331 (million) % 245.14/35.20 % (3322235)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=3269323008:i=28651:sd=4:ss=included:sgt=64_2755 on theBenchmark for (2755ds/28651Mi) % 245.14/35.20 % (3322227)Instruction limit reached! % 245.14/35.20 % (3322227)------------------------------ % 245.14/35.20 % (3322227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.14/35.20 % (3322227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.14/35.20 % (3322227)CaDiCaL version: 2.1.3 % 245.14/35.20 % (3322227)Termination reason: Instruction limit % 245.14/35.20 % (3322227)Termination phase: Saturation % 245.14/35.20 % (3322227)Time elapsed: 1.751 s % 245.14/35.20 % (3322227)Peak memory usage: 113 MB % 245.14/35.20 % (3322227)Instructions burned: 6508 (million) % 299.01/42.89 % (3322237)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=3855911611:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2753 on theBenchmark for (2753ds/2700Mi) % 299.01/42.89 % (3322233)Instruction limit reached! % 299.01/42.89 % (3322233)------------------------------ % 299.01/42.89 % (3322233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.01/42.89 % (3322233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.01/42.89 % (3322233)CaDiCaL version: 2.1.3 % 299.01/42.89 % (3322233)Termination reason: Instruction limit % 299.01/42.89 % (3322233)Termination phase: Saturation % 299.01/42.89 % (3322233)Time elapsed: 1.622 s % 299.01/42.89 % (3322233)Peak memory usage: 155 MB % 299.01/42.89 % (3322233)Instructions burned: 2694 (million) % 299.01/42.89 % (3322239)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=1794083762:i=3196:nm=4_2747 on theBenchmark for (2747ds/3196Mi) % 299.01/42.89 % (3322237)Instruction limit reached! % 299.01/42.89 % (3322237)------------------------------ % 299.01/42.89 % (3322237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.01/42.89 % (3322237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.01/42.89 % (3322237)CaDiCaL version: 2.1.3 % 299.01/42.89 % (3322237)Termination reason: Instruction limit % 299.01/42.89 % (3322237)Termination phase: Saturation % 299.01/42.89 % (3322237)Time elapsed: 0.912 s % 299.01/42.89 % (3322237)Peak memory usage: 143 MB % 299.01/42.89 % (3322237)Instructions burned: 2702 (million) % 299.01/42.89 % (3322241)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1549303907:cts=off:i=3254:av=off_2742 on theBenchmark for (2742ds/3254Mi) % 299.01/42.89 % (3322231)Instruction limit reached! % 299.01/42.89 % (3322231)------------------------------ % 299.01/42.89 % (3322231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.01/42.89 % (3322231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.01/42.89 % (3322231)CaDiCaL version: 2.1.3 % 299.01/42.89 % (3322231)Termination reason: Instruction limit % 299.01/42.89 % (3322231)Termination phase: Saturation % 299.01/42.89 % (3322231)Time elapsed: 2.750 s % 299.01/42.89 % (3322231)Peak memory usage: 120 MB % 299.01/42.89 % (3322231)Instructions burned: 7593 (million) % 299.01/42.89 % (3322243)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=2783437666:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2739 on theBenchmark for (2739ds/3264Mi) % 299.01/42.89 % (3322241)Instruction limit reached! % 299.01/42.89 % (3322241)------------------------------ % 299.01/42.89 % (3322241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.01/42.89 % (3322241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.01/42.89 % (3322241)CaDiCaL version: 2.1.3 % 299.01/42.89 % (3322241)Termination reason: Instruction limit % 299.01/42.89 % (3322241)Termination phase: Saturation % 299.01/42.89 % (3322241)Time elapsed: 1.292 s % 299.01/42.89 % (3322241)Peak memory usage: 146 MB % 299.01/42.89 % (3322241)Instructions burned: 3256 (million) % 299.01/42.89 % (3322245)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=2318707744:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2728 on theBenchmark for (2728ds/9708Mi) % 299.01/42.89 % (3322239)Instruction limit reached! % 299.01/42.89 % (3322239)------------------------------ % 299.01/42.89 % (3322239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.01/42.89 % (3322239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.01/42.89 % (3322239)CaDiCaL version: 2.1.3 % 299.01/42.89 % (3322239)Termination reason: Instruction limit % 299.01/42.89 % (3322239)Termination phase: Saturation % 299.01/42.89 % (3322239)Time elapsed: 1.988 s % 299.01/42.89 % (3322239)Peak memory usage: 139 MB % 299.01/42.89 % (3322239)Instructions burned: 3197 (million) % 299.01/42.89 % (3322247)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1732642891:i=21997:s2at=5:gtg=all_2725 on theBenchmark for (2725ds/21997Mi) % 299.01/42.89 % (3322245)Refutation not found, incomplete strategy % 299.01/42.89 % (3322245)------------------------------ % 299.01/42.89 % (3322245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 1Terminated %------------------------------------------------------------------------------