%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : MSC015-1.030 : 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 : n002.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 12:05:12 PM UTC 2026 % Result : Timeout 300.07s 43.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : MSC015-1.030 : TPTP v9.3.1. Released v3.5.0. % 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.20/0.46 % Computer : n002.cluster.edu % 0.20/0.46 % Model : x86_64 x86_64 % 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.20/0.46 % Memory : 8046.5625MB % 0.20/0.46 % OS : Linux 6.8.0-71-generic % 0.20/0.46 % CPULimit : 300 % 0.20/0.46 % WCLimit : 300 % 0.20/0.46 % DateTime : Sun Sep 27 17:45:36 UTC 2026 % 0.20/0.46 % CPUTime : % 0.20/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.25/0.52 Running first-order theorem proving % 0.25/0.52 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 % 18.69/3.98 % (3769168)Input is clausal, will run a generic CNF schedule. % 18.69/3.98 % (3769176)lrs+10_1_sil=8000:sp=occurrence:random_seed=3648952209:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 18.69/3.98 % (3769176)Instruction limit reached! % 18.69/3.98 % (3769176)------------------------------ % 18.69/3.98 % (3769176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.98 % (3769176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.98 % (3769176)CaDiCaL version: 2.1.3 % 18.69/3.98 % (3769176)Termination reason: Instruction limit % 18.69/3.98 % (3769176)Termination phase: Saturation % 18.69/3.98 % (3769176)Time elapsed: 0.041 s % 18.69/3.98 % (3769176)Peak memory usage: 88 MB % 18.69/3.98 % (3769176)Instructions burned: 107 (million) % 18.69/3.98 % (3769175)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=53838262:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 18.69/3.98 % (3769173)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=42574949:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 18.69/3.98 % (3769174)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4128213858:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 18.69/3.98 % (3769177)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2442777132:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 18.69/3.98 % (3769178)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3838099151:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 18.69/3.98 % (3769179)dis-21_1_sil=8000:lcm=predicate:random_seed=3620664903: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) % 18.69/3.98 % (3769177)Instruction limit reached! % 18.69/3.98 % (3769177)------------------------------ % 18.69/3.98 % (3769177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.98 % (3769177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.98 % (3769177)CaDiCaL version: 2.1.3 % 18.69/3.98 % (3769177)Termination reason: Instruction limit % 18.69/3.98 % (3769177)Termination phase: Saturation % 18.69/3.98 % (3769177)Time elapsed: 0.085 s % 18.69/3.98 % (3769177)Peak memory usage: 88 MB % 18.69/3.98 % (3769177)Instructions burned: 115 (million) % 18.69/3.98 % (3769179)Instruction limit reached! % 18.69/3.98 % (3769179)------------------------------ % 18.69/3.98 % (3769179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.98 % (3769179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.98 % (3769179)CaDiCaL version: 2.1.3 % 18.69/3.98 % (3769179)Termination reason: Instruction limit % 18.69/3.98 % (3769179)Termination phase: Saturation % 18.69/3.98 % (3769179)Time elapsed: 0.092 s % 18.69/3.98 % (3769179)Peak memory usage: 88 MB % 18.69/3.98 % (3769179)Instructions burned: 117 (million) % 18.69/3.98 % (3769178)Instruction limit reached! % 18.69/3.98 % (3769178)------------------------------ % 18.69/3.98 % (3769178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.98 % (3769178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.98 % (3769178)CaDiCaL version: 2.1.3 % 18.69/3.98 % (3769178)Termination reason: Instruction limit % 18.69/3.98 % (3769178)Termination phase: Saturation % 18.69/3.98 % (3769178)Time elapsed: 0.143 s % 18.69/3.98 % (3769178)Peak memory usage: 89 MB % 18.69/3.98 % (3769178)Instructions burned: 181 (million) % 18.69/3.98 % (3769182)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=719045681:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 18.69/3.98 % (3769182)Refutation not found, incomplete strategy % 18.69/3.98 % (3769182)------------------------------ % 18.69/3.98 % (3769182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.69/3.98 % (3769182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.69/3.98 % (3769182)CaDiCaL version: 2.1.3 % 18.69/3.98 % (3769182)Termination reason: Refutation not found, incomplete strategy % 18.69/3.98 % (3769182)Time elapsed: 0.002 s % 18.69/3.98 % (3769182)Peak memory usage: 87 MB % 18.69/3.98 % (3769182)Instructions burned: 4 (million) % 18.69/3.98 % (3769189)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3766186238:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 39.87/6.98 % (3769190)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=912593291:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi) % 39.87/6.98 % (3769191)lrs+10_64_to=lpo:sil=8000:random_seed=2818823651:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 39.87/6.98 % (3769182)------------------------------ % 39.87/6.98 % (3769182)------------------------------ % 39.87/6.98 % (3769189)Instruction limit reached! % 39.87/6.98 % (3769189)------------------------------ % 39.87/6.98 % (3769189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.87/6.98 % (3769189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.87/6.98 % (3769189)CaDiCaL version: 2.1.3 % 39.87/6.98 % (3769189)Termination reason: Instruction limit % 39.87/6.98 % (3769189)Termination phase: Saturation % 39.87/6.98 % (3769189)Time elapsed: 0.146 s % 39.87/6.98 % (3769189)Peak memory usage: 88 MB % 39.87/6.98 % (3769189)Instructions burned: 190 (million) % 39.87/6.98 % (3769191)Instruction limit reached! % 39.87/6.98 % (3769191)------------------------------ % 39.87/6.98 % (3769191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.87/6.98 % (3769191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.87/6.98 % (3769191)CaDiCaL version: 2.1.3 % 39.87/6.98 % (3769191)Termination reason: Instruction limit % 39.87/6.98 % (3769191)Termination phase: Saturation % 39.87/6.98 % (3769191)Time elapsed: 0.101 s % 39.87/6.98 % (3769191)Peak memory usage: 88 MB % 39.87/6.98 % (3769191)Instructions burned: 126 (million) % 39.87/6.98 % (3769190)Instruction limit reached! % 39.87/6.98 % (3769190)------------------------------ % 39.87/6.98 % (3769190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.87/6.98 % (3769190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.87/6.98 % (3769190)CaDiCaL version: 2.1.3 % 39.87/6.98 % (3769190)Termination reason: Instruction limit % 39.87/6.98 % (3769190)Termination phase: Saturation % 39.87/6.98 % (3769190)Time elapsed: 0.169 s % 39.87/6.98 % (3769190)Peak memory usage: 88 MB % 39.87/6.98 % (3769190)Instructions burned: 219 (million) % 39.87/6.98 % (3769196)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=10437926:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi) % 39.87/6.98 % (3769197)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=464043959:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi) % 39.87/6.98 % (3769196)Instruction limit reached! % 39.87/6.98 % (3769196)------------------------------ % 39.87/6.98 % (3769196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.87/6.98 % (3769196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.87/6.98 % (3769196)CaDiCaL version: 2.1.3 % 39.87/6.98 % (3769196)Termination reason: Instruction limit % 39.87/6.98 % (3769196)Termination phase: Saturation % 39.87/6.98 % (3769196)Time elapsed: 0.073 s % 39.87/6.98 % (3769196)Peak memory usage: 88 MB % 39.87/6.98 % (3769196)Instructions burned: 194 (million) % 39.87/6.98 % (3769198)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=734908212:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi) % 39.87/6.98 % (3769199)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=2926362261:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi) % 39.87/6.98 % (3769197)Instruction limit reached! % 39.87/6.98 % (3769197)------------------------------ % 39.87/6.98 % (3769197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.87/6.98 % (3769197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.87/6.98 % (3769197)CaDiCaL version: 2.1.3 % 39.87/6.98 % (3769197)Termination reason: Instruction limit % 39.87/6.98 % (3769197)Termination phase: Saturation % 39.87/6.98 % (3769197)Time elapsed: 0.126 s % 39.87/6.98 % (3769197)Peak memory usage: 89 MB % 39.87/6.98 % (3769197)Instructions burned: 157 (million) % 39.87/6.98 % (3769199)Instruction limit reached! % 39.87/6.98 % (3769199)------------------------------ % 39.87/6.98 % (3769199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.87/6.98 % (3769199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.85/10.06 % (3769199)CaDiCaL version: 2.1.3 % 61.85/10.06 % (3769199)Termination reason: Instruction limit % 61.85/10.06 % (3769199)Termination phase: Saturation % 61.85/10.06 % (3769199)Time elapsed: 0.079 s % 61.85/10.06 % (3769199)Peak memory usage: 88 MB % 61.85/10.06 % (3769199)Instructions burned: 107 (million) % 61.85/10.06 % (3769202)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2323520161:i=107_2988 on theBenchmark for (2988ds/107Mi) % 61.85/10.06 % (3769202)Instruction limit reached! % 61.85/10.06 % (3769202)------------------------------ % 61.85/10.06 % (3769202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.85/10.06 % (3769202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.85/10.06 % (3769202)CaDiCaL version: 2.1.3 % 61.85/10.06 % (3769202)Termination reason: Instruction limit % 61.85/10.06 % (3769202)Termination phase: Saturation % 61.85/10.06 % (3769202)Time elapsed: 0.085 s % 61.85/10.06 % (3769202)Peak memory usage: 87 MB % 61.85/10.06 % (3769202)Instructions burned: 107 (million) % 61.85/10.06 % (3769205)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2316736950:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi) % 61.85/10.06 % (3769206)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=765968136:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi) % 61.85/10.06 % (3769205)Instruction limit reached! % 61.85/10.06 % (3769205)------------------------------ % 61.85/10.06 % (3769205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.85/10.06 % (3769205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.85/10.06 % (3769205)CaDiCaL version: 2.1.3 % 61.85/10.06 % (3769205)Termination reason: Instruction limit % 61.85/10.06 % (3769205)Termination phase: Saturation % 61.85/10.06 % (3769205)Time elapsed: 0.179 s % 61.85/10.06 % (3769205)Peak memory usage: 88 MB % 61.85/10.06 % (3769205)Instructions burned: 242 (million) % 61.85/10.06 % (3769208)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2347200340:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi) % 61.85/10.06 % (3769208)Instruction limit reached! % 61.85/10.06 % (3769208)------------------------------ % 61.85/10.06 % (3769208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.85/10.06 % (3769208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.85/10.06 % (3769208)CaDiCaL version: 2.1.3 % 61.85/10.06 % (3769208)Termination reason: Instruction limit % 61.85/10.06 % (3769208)Termination phase: Saturation % 61.85/10.06 % (3769208)Time elapsed: 0.100 s % 61.85/10.06 % (3769208)Peak memory usage: 88 MB % 61.85/10.06 % (3769208)Instructions burned: 135 (million) % 61.85/10.06 % (3769211)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2487395887:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi) % 61.85/10.06 % (3769213)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1456853718:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi) % 61.85/10.06 % (3769211)Instruction limit reached! % 61.85/10.06 % (3769211)------------------------------ % 61.85/10.06 % (3769211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.85/10.06 % (3769211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.85/10.06 % (3769211)CaDiCaL version: 2.1.3 % 61.85/10.06 % (3769211)Termination reason: Instruction limit % 61.85/10.06 % (3769211)Termination phase: Saturation % 61.85/10.06 % (3769211)Time elapsed: 0.384 s % 61.85/10.06 % (3769211)Peak memory usage: 90 MB % 61.85/10.06 % (3769211)Instructions burned: 499 (million) % 61.85/10.06 % (3769213)Instruction limit reached! % 61.85/10.06 % (3769213)------------------------------ % 61.85/10.06 % (3769213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.85/10.06 % (3769213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.85/10.06 % (3769213)CaDiCaL version: 2.1.3 % 61.85/10.06 % (3769213)Termination reason: Instruction limit % 61.85/10.06 % (3769213)Termination phase: Saturation % 61.85/10.06 % (3769213)Time elapsed: 0.160 s % 61.85/10.06 % (3769213)Peak memory usage: 89 MB % 61.85/10.06 % (3769213)Instructions burned: 192 (million) % 61.85/10.06 % (3769216)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3884130406:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi) % 110.65/16.85 % (3769217)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3834366663:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi) % 110.65/16.85 % (3769217)Instruction limit reached! % 110.65/16.85 % (3769217)------------------------------ % 110.65/16.85 % (3769217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.65/16.85 % (3769217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.65/16.85 % (3769217)CaDiCaL version: 2.1.3 % 110.65/16.85 % (3769217)Termination reason: Instruction limit % 110.65/16.85 % (3769217)Termination phase: Saturation % 110.65/16.85 % (3769217)Time elapsed: 0.129 s % 110.65/16.85 % (3769217)Peak memory usage: 88 MB % 110.65/16.85 % (3769217)Instructions burned: 156 (million) % 110.65/16.85 % (3769216)Instruction limit reached! % 110.65/16.85 % (3769216)------------------------------ % 110.65/16.85 % (3769216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.65/16.85 % (3769216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.65/16.85 % (3769216)CaDiCaL version: 2.1.3 % 110.65/16.85 % (3769216)Termination reason: Instruction limit % 110.65/16.85 % (3769216)Termination phase: Saturation % 110.65/16.85 % (3769216)Time elapsed: 0.205 s % 110.65/16.85 % (3769216)Peak memory usage: 90 MB % 110.65/16.85 % (3769216)Instructions burned: 264 (million) % 110.65/16.85 % (3769220)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=4046705502:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi) % 110.65/16.85 % (3769221)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2183935809:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi) % 110.65/16.85 % (3769221)Instruction limit reached! % 110.65/16.85 % (3769221)------------------------------ % 110.65/16.85 % (3769221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.65/16.85 % (3769221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.65/16.85 % (3769221)CaDiCaL version: 2.1.3 % 110.65/16.85 % (3769221)Termination reason: Instruction limit % 110.65/16.85 % (3769221)Termination phase: Saturation % 110.65/16.85 % (3769221)Time elapsed: 0.416 s % 110.65/16.85 % (3769221)Peak memory usage: 91 MB % 110.65/16.85 % (3769221)Instructions burned: 538 (million) % 110.65/16.85 % (3769224)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4169232543:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi) % 110.65/16.85 % (3769224)Instruction limit reached! % 110.65/16.85 % (3769224)------------------------------ % 110.65/16.85 % (3769224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.65/16.85 % (3769224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.65/16.85 % (3769224)CaDiCaL version: 2.1.3 % 110.65/16.85 % (3769224)Termination reason: Instruction limit % 110.65/16.85 % (3769224)Termination phase: Saturation % 110.65/16.85 % (3769224)Time elapsed: 0.144 s % 110.65/16.85 % (3769224)Peak memory usage: 88 MB % 110.65/16.85 % (3769224)Instructions burned: 181 (million) % 110.65/16.85 % (3769226)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=3986064520:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2959 on theBenchmark for (2959ds/10307Mi) % 110.65/16.85 % (3769198)Instruction limit reached! % 110.65/16.85 % (3769198)------------------------------ % 110.65/16.85 % (3769198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.65/16.85 % (3769198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.65/16.85 % (3769198)CaDiCaL version: 2.1.3 % 110.65/16.85 % (3769198)Termination reason: Instruction limit % 110.65/16.85 % (3769198)Termination phase: Saturation % 110.65/16.85 % (3769198)Time elapsed: 3.920 s % 110.65/16.85 % (3769198)Peak memory usage: 142 MB % 110.65/16.85 % (3769198)Instructions burned: 3394 (million) % 110.65/16.85 % (3769228)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=2914531673:i=412:gtgl=4:gtg=exists_all_2949 on theBenchmark for (2949ds/412Mi) % 110.65/16.85 % (3769228)Instruction limit reached! % 110.65/16.85 % (3769228)------------------------------ % 110.65/16.85 % (3769228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.65/16.85 % (3769228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.65/16.85 % (3769228)CaDiCaL version: 2.1.3 % 154.45/23.03 % (3769228)Termination reason: Instruction limit % 154.45/23.03 % (3769228)Termination phase: Saturation % 154.45/23.03 % (3769228)Time elapsed: 0.292 s % 154.45/23.03 % (3769228)Peak memory usage: 91 MB % 154.45/23.03 % (3769228)Instructions burned: 412 (million) % 154.45/23.03 % (3769230)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=1129124379:s2pl=no:i=8478:s2at=4:nm=6_2943 on theBenchmark for (2943ds/8478Mi) % 154.45/23.03 % (3769220)Instruction limit reached! % 154.45/23.03 % (3769220)------------------------------ % 154.45/23.03 % (3769220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.45/23.03 % (3769220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.45/23.03 % (3769220)CaDiCaL version: 2.1.3 % 154.45/23.03 % (3769220)Termination reason: Instruction limit % 154.45/23.03 % (3769220)Termination phase: Saturation % 154.45/23.03 % (3769220)Time elapsed: 3.970 s % 154.45/23.03 % (3769220)Peak memory usage: 139 MB % 154.45/23.03 % (3769220)Instructions burned: 3257 (million) % 154.45/23.03 % (3769232)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=1668109603:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2928 on theBenchmark for (2928ds/303Mi) % 154.45/23.03 % (3769206)Instruction limit reached! % 154.45/23.03 % (3769206)------------------------------ % 154.45/23.03 % (3769206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.45/23.03 % (3769206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.45/23.03 % (3769206)CaDiCaL version: 2.1.3 % 154.45/23.03 % (3769206)Termination reason: Instruction limit % 154.45/23.03 % (3769206)Termination phase: Saturation % 154.45/23.03 % (3769206)Time elapsed: 5.996 s % 154.45/23.03 % (3769206)Peak memory usage: 151 MB % 154.45/23.03 % (3769206)Instructions burned: 5209 (million) % 154.45/23.03 % (3769232)Instruction limit reached! % 154.45/23.03 % (3769232)------------------------------ % 154.45/23.03 % (3769232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.45/23.03 % (3769232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.45/23.03 % (3769232)CaDiCaL version: 2.1.3 % 154.45/23.03 % (3769232)Termination reason: Instruction limit % 154.45/23.03 % (3769232)Termination phase: Saturation % 154.45/23.03 % (3769232)Time elapsed: 0.254 s % 154.45/23.03 % (3769232)Peak memory usage: 90 MB % 154.45/23.03 % (3769232)Instructions burned: 304 (million) % 154.45/23.03 % (3769234)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=433285805:st=4:i=720:sd=3:fsr=off:ss=axioms_2924 on theBenchmark for (2924ds/720Mi) % 154.45/23.03 % (3769235)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2872733727:i=598:bs=on:bd=preordered:av=off:ss=axioms_2923 on theBenchmark for (2923ds/598Mi) % 154.45/23.03 % (3769234)Instruction limit reached! % 154.45/23.03 % (3769234)------------------------------ % 154.45/23.03 % (3769234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.45/23.03 % (3769234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.45/23.03 % (3769234)CaDiCaL version: 2.1.3 % 154.45/23.03 % (3769234)Termination reason: Instruction limit % 154.45/23.03 % (3769234)Termination phase: Saturation % 154.45/23.03 % (3769234)Time elapsed: 0.526 s % 154.45/23.03 % (3769234)Peak memory usage: 90 MB % 154.45/23.03 % (3769234)Instructions burned: 720 (million) % 154.45/23.03 % (3769235)Instruction limit reached! % 154.45/23.03 % (3769235)------------------------------ % 154.45/23.03 % (3769235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.45/23.03 % (3769235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.45/23.03 % (3769235)CaDiCaL version: 2.1.3 % 154.45/23.03 % (3769235)Termination reason: Instruction limit % 154.45/23.03 % (3769235)Termination phase: Saturation % 154.45/23.03 % (3769235)Time elapsed: 0.483 s % 154.45/23.03 % (3769235)Peak memory usage: 90 MB % 154.45/23.03 % (3769235)Instructions burned: 599 (million) % 154.45/23.03 % (3769238)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3340681785:i=2989:sd=3:ss=axioms:sgt=60_2915 on theBenchmark for (2915ds/2989Mi) % 154.45/23.03 % (3769239)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=2254434524:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2915 on theBenchmark for (2915ds/1997Mi) % 194.81/28.76 % (3769239)Instruction limit reached! % 194.81/28.76 % (3769239)------------------------------ % 194.81/28.76 % (3769239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.81/28.76 % (3769239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.81/28.76 % (3769239)CaDiCaL version: 2.1.3 % 194.81/28.76 % (3769239)Termination reason: Instruction limit % 194.81/28.76 % (3769239)Termination phase: Saturation % 194.81/28.76 % (3769239)Time elapsed: 2.299 s % 194.81/28.76 % (3769239)Peak memory usage: 133 MB % 194.81/28.76 % (3769239)Instructions burned: 1997 (million) % 194.81/28.76 % (3769242)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=2426210347:i=2088:bd=preordered:av=off_2889 on theBenchmark for (2889ds/2088Mi) % 194.81/28.76 % (3769238)Instruction limit reached! % 194.81/28.76 % (3769238)------------------------------ % 194.81/28.76 % (3769238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.81/28.76 % (3769238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.81/28.76 % (3769238)CaDiCaL version: 2.1.3 % 194.81/28.76 % (3769238)Termination reason: Instruction limit % 194.81/28.76 % (3769238)Termination phase: Saturation % 194.81/28.76 % (3769238)Time elapsed: 3.373 s % 194.81/28.76 % (3769238)Peak memory usage: 139 MB % 194.81/28.76 % (3769238)Instructions burned: 2989 (million) % 194.81/28.76 % (3769244)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1236161652:i=1098:nicw=on_2878 on theBenchmark for (2878ds/1098Mi) % 194.81/28.76 % (3769244)Instruction limit reached! % 194.81/28.76 % (3769244)------------------------------ % 194.81/28.76 % (3769244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.81/28.76 % (3769244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.81/28.76 % (3769244)CaDiCaL version: 2.1.3 % 194.81/28.76 % (3769244)Termination reason: Instruction limit % 194.81/28.76 % (3769244)Termination phase: Saturation % 194.81/28.76 % (3769244)Time elapsed: 0.717 s % 194.81/28.76 % (3769244)Peak memory usage: 94 MB % 194.81/28.76 % (3769244)Instructions burned: 1098 (million) % 194.81/28.76 % (3769246)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=259295882:i=433:bd=preordered_2868 on theBenchmark for (2868ds/433Mi) % 194.81/28.76 % (3769246)Instruction limit reached! % 194.81/28.76 % (3769246)------------------------------ % 194.81/28.76 % (3769246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.81/28.76 % (3769246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.81/28.76 % (3769246)CaDiCaL version: 2.1.3 % 194.81/28.76 % (3769246)Termination reason: Instruction limit % 194.81/28.76 % (3769246)Termination phase: Saturation % 194.81/28.76 % (3769246)Time elapsed: 0.292 s % 194.81/28.76 % (3769246)Peak memory usage: 90 MB % 194.81/28.76 % (3769246)Instructions burned: 434 (million) % 194.81/28.76 % (3769242)Instruction limit reached! % 194.81/28.76 % (3769242)------------------------------ % 194.81/28.76 % (3769242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.81/28.76 % (3769242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.81/28.76 % (3769242)CaDiCaL version: 2.1.3 % 194.81/28.76 % (3769242)Termination reason: Instruction limit % 194.81/28.76 % (3769242)Termination phase: Saturation % 194.81/28.76 % (3769242)Time elapsed: 2.478 s % 194.81/28.76 % (3769242)Peak memory usage: 133 MB % 194.81/28.76 % (3769242)Instructions burned: 2088 (million) % 194.81/28.76 % (3769248)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=176182606:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2862 on theBenchmark for (2862ds/2942Mi) % 194.81/28.76 % (3769249)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4285511276:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2861 on theBenchmark for (2861ds/6922Mi) % 194.81/28.76 % (3769230)Instruction limit reached! % 194.81/28.76 % (3769230)------------------------------ % 194.81/28.76 % (3769230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.81/28.76 % (3769230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.81/28.76 % (3769230)CaDiCaL version: 2.1.3 % 194.81/28.76 % (3769230)Termination reason: Instruction limit % 194.81/28.76 % (3769230)Termination phase: Saturation % 194.81/28.76 % (3769230)Time elapsed: 9.565 s % 225.65/33.03 % (3769230)Peak memory usage: 168 MB % 225.65/33.03 % (3769230)Instructions burned: 8478 (million) % 225.65/33.03 % (3769268)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=3724612651:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2844 on theBenchmark for (2844ds/596Mi) % 225.65/33.03 % (3769268)Instruction limit reached! % 225.65/33.03 % (3769268)------------------------------ % 225.65/33.03 % (3769268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.65/33.03 % (3769268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.65/33.03 % (3769268)CaDiCaL version: 2.1.3 % 225.65/33.03 % (3769268)Termination reason: Instruction limit % 225.65/33.03 % (3769268)Termination phase: Saturation % 225.65/33.03 % (3769268)Time elapsed: 0.482 s % 225.65/33.03 % (3769268)Peak memory usage: 91 MB % 225.65/33.03 % (3769268)Instructions burned: 596 (million) % 225.65/33.03 % (3769271)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=3389303307:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2836 on theBenchmark for (2836ds/4123Mi) % 225.65/33.03 % (3769226)Instruction limit reached! % 225.65/33.03 % (3769226)------------------------------ % 225.65/33.03 % (3769226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.65/33.03 % (3769226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.65/33.03 % (3769226)CaDiCaL version: 2.1.3 % 225.65/33.03 % (3769226)Termination reason: Instruction limit % 225.65/33.03 % (3769226)Termination phase: Saturation % 225.65/33.03 % (3769226)Time elapsed: 13.183 s % 225.65/33.03 % (3769226)Peak memory usage: 181 MB % 225.65/33.03 % (3769226)Instructions burned: 10307 (million) % 225.65/33.03 % (3769248)Instruction limit reached! % 225.65/33.03 % (3769248)------------------------------ % 225.65/33.03 % (3769248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.65/33.03 % (3769248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.65/33.03 % (3769248)CaDiCaL version: 2.1.3 % 225.65/33.03 % (3769248)Termination reason: Instruction limit % 225.65/33.03 % (3769248)Termination phase: Saturation % 225.65/33.03 % (3769248)Time elapsed: 3.626 s % 225.65/33.03 % (3769248)Peak memory usage: 139 MB % 225.65/33.03 % (3769248)Instructions burned: 2942 (million) % 225.65/33.03 % (3769273)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3851520493:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2824 on theBenchmark for (2824ds/16411Mi) % 225.65/33.03 % (3769274)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3922336794:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2823 on theBenchmark for (2823ds/1670Mi) % 225.65/33.03 % (3769274)Instruction limit reached! % 225.65/33.03 % (3769274)------------------------------ % 225.65/33.03 % (3769274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.65/33.03 % (3769274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.65/33.03 % (3769274)CaDiCaL version: 2.1.3 % 225.65/33.03 % (3769274)Termination reason: Instruction limit % 225.65/33.03 % (3769274)Termination phase: Saturation % 225.65/33.03 % (3769274)Time elapsed: 1.726 s % 225.65/33.03 % (3769274)Peak memory usage: 132 MB % 225.65/33.03 % (3769274)Instructions burned: 1670 (million) % 225.65/33.03 % (3769277)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=1177051009:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2803 on theBenchmark for (2803ds/1722Mi) % 225.65/33.03 % (3769271)Instruction limit reached! % 225.65/33.03 % (3769271)------------------------------ % 225.65/33.03 % (3769271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.65/33.03 % (3769271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.65/33.03 % (3769271)CaDiCaL version: 2.1.3 % 225.65/33.03 % (3769271)Termination reason: Instruction limit % 225.65/33.03 % (3769271)Termination phase: Saturation % 225.65/33.03 % (3769271)Time elapsed: 4.758 s % 225.65/33.03 % (3769271)Peak memory usage: 144 MB % 225.65/33.03 % (3769271)Instructions burned: 4123 (million) % 225.65/33.03 % (3769279)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=3029832030:cts=off:cond=on:i=9530:bs=on:fsd=on_2785 on theBenchmark for (2785ds/9530Mi) % 245.28/35.86 % (3769277)Instruction limit reached! % 245.28/35.86 % (3769277)------------------------------ % 245.28/35.86 % (3769277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.28/35.86 % (3769277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.28/35.86 % (3769277)CaDiCaL version: 2.1.3 % 245.28/35.86 % (3769277)Termination reason: Instruction limit % 245.28/35.86 % (3769277)Termination phase: Saturation % 245.28/35.86 % (3769277)Time elapsed: 2.010 s % 245.28/35.86 % (3769277)Peak memory usage: 133 MB % 245.28/35.86 % (3769277)Instructions burned: 1723 (million) % 245.28/35.86 % (3769286)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3286114374:st=2:i=4495:sd=10:ss=included_2780 on theBenchmark for (2780ds/4495Mi) % 245.28/35.86 % (3769249)Instruction limit reached! % 245.28/35.86 % (3769249)------------------------------ % 245.28/35.86 % (3769249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.28/35.86 % (3769249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.28/35.86 % (3769249)CaDiCaL version: 2.1.3 % 245.28/35.86 % (3769249)Termination reason: Instruction limit % 245.28/35.86 % (3769249)Termination phase: Saturation % 245.28/35.86 % (3769249)Time elapsed: 8.371 s % 245.28/35.86 % (3769249)Peak memory usage: 161 MB % 245.28/35.86 % (3769249)Instructions burned: 6923 (million) % 245.28/35.86 % (3769441)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=3128144256:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2774 on theBenchmark for (2774ds/4920Mi) % 245.28/35.86 % (3769286)Instruction limit reached! % 245.28/35.86 % (3769286)------------------------------ % 245.28/35.86 % (3769286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.28/35.86 % (3769286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.28/35.86 % (3769286)CaDiCaL version: 2.1.3 % 245.28/35.86 % (3769286)Termination reason: Instruction limit % 245.28/35.86 % (3769286)Termination phase: Saturation % 245.28/35.86 % (3769286)Time elapsed: 3.270 s % 245.28/35.86 % (3769286)Peak memory usage: 148 MB % 245.28/35.86 % (3769286)Instructions burned: 4496 (million) % 245.28/35.86 % (3769443)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=2797392028:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2745 on theBenchmark for (2745ds/2083Mi) % 245.28/35.86 % (3769441)Instruction limit reached! % 245.28/35.86 % (3769441)------------------------------ % 245.28/35.86 % (3769441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.28/35.86 % (3769441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.28/35.86 % (3769441)CaDiCaL version: 2.1.3 % 245.28/35.86 % (3769441)Termination reason: Instruction limit % 245.28/35.86 % (3769441)Termination phase: Saturation % 245.28/35.86 % (3769441)Time elapsed: 3.574 s % 245.28/35.86 % (3769441)Peak memory usage: 150 MB % 245.28/35.86 % (3769441)Instructions burned: 4920 (million) % 245.28/35.86 % (3769445)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=3096014942:i=4629:av=off:gsp=on_2737 on theBenchmark for (2737ds/4629Mi) % 245.28/35.86 % (3769443)Instruction limit reached! % 245.28/35.86 % (3769443)------------------------------ % 245.28/35.86 % (3769443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.28/35.86 % (3769443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.28/35.86 % (3769443)CaDiCaL version: 2.1.3 % 245.28/35.86 % (3769443)Termination reason: Instruction limit % 245.28/35.86 % (3769443)Termination phase: Saturation % 245.28/35.86 % (3769443)Time elapsed: 1.434 s % 245.28/35.86 % (3769443)Peak memory usage: 134 MB % 245.28/35.86 % (3769443)Instructions burned: 2083 (million) % 245.28/35.86 % (3769447)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3035566215:i=1258:av=off_2729 on theBenchmark for (2729ds/1258Mi) % 245.28/35.86 % (3769279)Instruction limit reached! % 245.28/35.86 % (3769279)------------------------------ % 245.28/35.86 % (3769279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.28/35.86 % (3769279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.28/35.86 % (3769279)CaDiCaL version: 2.1.3 % 245.28/35.86 % (3769279)Termination reason: Instruction limit % 245.28/35.86 % (3769279)Termination phase: Saturation % 279.73/40.75 % (3769279)Time elapsed: 5.734 s % 279.73/40.75 % (3769279)Peak memory usage: 151 MB % 279.73/40.75 % (3769279)Instructions burned: 9531 (million) % 279.73/40.75 % (3769449)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2354843017:i=7343:av=off:ss=included_2725 on theBenchmark for (2725ds/7343Mi) % 279.73/40.75 % (3769447)Instruction limit reached! % 279.73/40.75 % (3769447)------------------------------ % 279.73/40.75 % (3769447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.73/40.75 % (3769447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.73/40.75 % (3769447)CaDiCaL version: 2.1.3 % 279.73/40.75 % (3769447)Termination reason: Instruction limit % 279.73/40.75 % (3769447)Termination phase: Saturation % 279.73/40.75 % (3769447)Time elapsed: 0.586 s % 279.73/40.75 % (3769447)Peak memory usage: 100 MB % 279.73/40.75 % (3769447)Instructions burned: 1258 (million) % 279.73/40.75 % (3769451)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1909981403:i=1325:sd=2:ss=axioms:sgt=16_2722 on theBenchmark for (2722ds/1325Mi) % 279.73/40.75 % (3769451)Instruction limit reached! % 279.73/40.75 % (3769451)------------------------------ % 279.73/40.75 % (3769451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.73/40.75 % (3769451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.73/40.75 % (3769451)CaDiCaL version: 2.1.3 % 279.73/40.75 % (3769451)Termination reason: Instruction limit % 279.73/40.75 % (3769451)Termination phase: Saturation % 279.73/40.75 % (3769451)Time elapsed: 0.583 s % 279.73/40.75 % (3769451)Peak memory usage: 98 MB % 279.73/40.75 % (3769451)Instructions burned: 1326 (million) % 279.73/40.75 % (3769575)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=3130324007:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2714 on theBenchmark for (2714ds/2646Mi) % 279.73/40.75 % (3769445)Instruction limit reached! % 279.73/40.75 % (3769445)------------------------------ % 279.73/40.75 % (3769445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.73/40.75 % (3769445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.73/40.75 % (3769445)CaDiCaL version: 2.1.3 % 279.73/40.75 % (3769445)Termination reason: Instruction limit % 279.73/40.75 % (3769445)Termination phase: Saturation % 279.73/40.75 % (3769445)Time elapsed: 3.264 s % 279.73/40.75 % (3769445)Peak memory usage: 147 MB % 279.73/40.75 % (3769445)Instructions burned: 4630 (million) % 279.73/40.75 % (3769804)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1647984865:i=1489:sd=2:ep=R:ss=axioms_2702 on theBenchmark for (2702ds/1489Mi) % 279.73/40.75 % (3769575)Instruction limit reached! % 279.73/40.75 % (3769575)------------------------------ % 279.73/40.75 % (3769575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.73/40.75 % (3769575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.73/40.75 % (3769575)CaDiCaL version: 2.1.3 % 279.73/40.75 % (3769575)Termination reason: Instruction limit % 279.73/40.75 % (3769575)Termination phase: Saturation % 279.73/40.75 % (3769575)Time elapsed: 1.890 s % 279.73/40.75 % (3769575)Peak memory usage: 138 MB % 279.73/40.75 % (3769575)Instructions burned: 2647 (million) % 279.73/40.75 % (3769848)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=928370829:i=1503_2694 on theBenchmark for (2694ds/1503Mi) % 279.73/40.75 % (3769804)Instruction limit reached! % 279.73/40.75 % (3769804)------------------------------ % 279.73/40.75 % (3769804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.73/40.75 % (3769804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.73/40.75 % (3769804)CaDiCaL version: 2.1.3 % 279.73/40.75 % (3769804)Termination reason: Instruction limit % 279.73/40.75 % (3769804)Termination phase: Saturation % 279.73/40.75 % (3769804)Time elapsed: 0.988 s % 279.73/40.75 % (3769804)Peak memory usage: 130 MB % 279.73/40.75 % (3769804)Instructions burned: 1489 (million) % 279.73/40.75 % (3769850)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=64582926:i=13942:kws=frequency_2691 on theBenchmark for (2691ds/13942Mi) % 279.73/40.75 % (3769848)Instruction limit reached! % 279.73/40.75 % (3769848)------------------------------ % 279.73/40.75 % (3769848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.73/40.75 % (3769848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/43.53 % (3769848)CaDiCaL version: 2.1.3 % 300.07/43.53 % (3769848)Termination reason: Instruction limit % 300.07/43.53 % (3769848)Termination phase: Saturation % 300.07/43.53 % (3769848)Time elapsed: 1.012 s % 300.07/43.53 % (3769848)Peak memory usage: 130 MB % 300.07/43.53 % (3769848)Instructions burned: 1504 (million) % 300.07/43.53 % (3769273)Instruction limit reached! % 300.07/43.53 % (3769273)------------------------------ % 300.07/43.53 % (3769273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.07/43.53 % (3769273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/43.53 % (3769273)CaDiCaL version: 2.1.3 % 300.07/43.53 % (3769273)Termination reason: Instruction limit % 300.07/43.53 % (3769273)Termination phase: Saturation % 300.07/43.53 % (3769273)Time elapsed: 13.986 s % 300.07/43.53 % (3769273)Peak memory usage: 213 MB % 300.07/43.53 % (3769273)Instructions burned: 16411 (million) % 300.07/43.53 % (3769852)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=1957168546:i=3604:fsr=off:er=filter_2682 on theBenchmark for (2682ds/3604Mi) % 300.07/43.53 % (3769853)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2698393125:i=1876:sd=1:ss=included:sgt=32_2681 on theBenchmark for (2681ds/1876Mi) % 300.07/43.53 % (3769449)Instruction limit reached! % 300.07/43.53 % (3769449)------------------------------ % 300.07/43.53 % (3769449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.07/43.53 % (3769449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/43.53 % (3769449)CaDiCaL version: 2.1.3 % 300.07/43.53 % (3769449)Termination reason: Instruction limit % 300.07/43.53 % (3769449)Termination phase: Saturation % 300.07/43.53 % (3769449)Time elapsed: 5.421 s % 300.07/43.53 % (3769449)Peak memory usage: 164 MB % 300.07/43.53 % (3769449)Instructions burned: 7343 (million) % 300.07/43.53 % (3769856)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3234517413:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2669 on theBenchmark for (2669ds/1932Mi) % 300.07/43.53 % (3769853)Instruction limit reached! % 300.07/43.53 % (3769853)------------------------------ % 300.07/43.53 % (3769853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.07/43.53 % (3769853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/43.53 % (3769853)CaDiCaL version: 2.1.3 % 300.07/43.53 % (3769853)Termination reason: Instruction limit % 300.07/43.53 % (3769853)Termination phase: Saturation % 300.07/43.53 % (3769853)Time elapsed: 1.306 s % 300.07/43.53 % (3769853)Peak memory usage: 133 MB % 300.07/43.53 % (3769853)Instructions burned: 1876 (million) % 300.07/43.53 % (3769858)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=3926651592:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2666 on theBenchmark for (2666ds/1980Mi) % 300.07/43.53 % (3769852)Instruction limit reached! % 300.07/43.53 % (3769852)------------------------------ % 300.07/43.53 % (3769852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.07/43.53 % (3769852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/43.53 % (3769852)CaDiCaL version: 2.1.3 % 300.07/43.53 % (3769852)Termination reason: Instruction limit % 300.07/43.53 % (3769852)Termination phase: Saturation % 300.07/43.53 % (3769852)Time elapsed: 2.357 s % 300.07/43.53 % (3769852)Peak memory usage: 139 MB % 300.07/43.53 % (3769852)Instructions burned: 3605 (million) % 300.07/43.53 % (3769860)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=1104267863:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2656 on theBenchmark for (2656ds/3902Mi) % 300.07/43.53 % (3769856)Instruction limit reached! % 300.07/43.53 % (3769856)------------------------------ % 300.07/43.53 % (3769856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.07/43.53 % (3769856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/43.53 % (3769856)CaDiCaL version: 2.1.3 % 300.07/43.53 % (3769856)Termination reason: Instruction limit % 300.07/43.53 % (3769856)Termination phase: Saturation % 300.07/43.53 % (3769856)Time elapsed: 1.340 s % 300.07/43.53 % (3769856)Peak memory usage: 133 MB % 300.07/43.53 % (3769856)Instructions burned: 1932 (million) % 300.07/43.54 Terminated %------------------------------------------------------------------------------