%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV519-1.030 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.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:16:39 PM UTC 2026 % Result : Timeout 291.01s 41.78s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV519-1.030 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 11:27:34 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.13 Running first-order theorem proving % 0.08/0.13 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.33/1.61 % (3322593)Input is clausal, will run a generic CNF schedule. % 8.33/1.61 % (3322601)lrs+10_1_sil=8000:sp=occurrence:random_seed=3616881368:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 8.33/1.61 % (3322600)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3570863574:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 8.33/1.61 % (3322603)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3697059248:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 8.33/1.61 % (3322604)dis-21_1_sil=8000:lcm=predicate:random_seed=1147952338: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) % 8.33/1.61 % (3322599)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=578666659:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 8.33/1.61 % (3322598)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=2036374197:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 8.33/1.61 % (3322602)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1260035287:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 8.33/1.61 % (3322601)Refutation not found, incomplete strategy % 8.33/1.61 % (3322601)------------------------------ % 8.33/1.61 % (3322601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.33/1.61 % (3322601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.61 % (3322601)CaDiCaL version: 2.1.3 % 8.33/1.61 % (3322601)Termination reason: Refutation not found, incomplete strategy % 8.33/1.61 % (3322601)Time elapsed: 0.005 s % 8.33/1.61 % (3322601)Peak memory usage: 88 MB % 8.33/1.61 % (3322601)Instructions burned: 17 (million) % 8.33/1.61 % (3322604)Refutation not found, incomplete strategy % 8.33/1.61 % (3322604)------------------------------ % 8.33/1.61 % (3322604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.33/1.61 % (3322604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.61 % (3322604)CaDiCaL version: 2.1.3 % 8.33/1.61 % (3322604)Termination reason: Refutation not found, incomplete strategy % 8.33/1.61 % (3322604)Time elapsed: 0.007 s % 8.33/1.61 % (3322604)Peak memory usage: 88 MB % 8.33/1.61 % (3322604)Instructions burned: 23 (million) % 8.33/1.61 % (3322602)Refutation not found, incomplete strategy % 8.33/1.61 % (3322602)------------------------------ % 8.33/1.61 % (3322602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.33/1.61 % (3322602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.61 % (3322602)CaDiCaL version: 2.1.3 % 8.33/1.61 % (3322602)Termination reason: Refutation not found, incomplete strategy % 8.33/1.61 % (3322602)Time elapsed: 0.010 s % 8.33/1.61 % (3322602)Peak memory usage: 88 MB % 8.33/1.61 % (3322602)Instructions burned: 37 (million) % 8.33/1.61 % (3322603)Instruction limit reached! % 8.33/1.61 % (3322603)------------------------------ % 8.33/1.61 % (3322603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.33/1.61 % (3322603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.61 % (3322603)CaDiCaL version: 2.1.3 % 8.33/1.61 % (3322603)Termination reason: Instruction limit % 8.33/1.61 % (3322603)Termination phase: Saturation % 8.33/1.61 % (3322603)Time elapsed: 0.052 s % 8.33/1.61 % (3322603)Peak memory usage: 89 MB % 8.33/1.61 % (3322603)Instructions burned: 182 (million) % 8.33/1.61 % (3322601)------------------------------ % 8.33/1.61 % (3322601)------------------------------ % 8.33/1.61 % (3322604)------------------------------ % 8.33/1.61 % (3322604)------------------------------ % 8.33/1.61 % (3322602)------------------------------ % 8.33/1.61 % (3322602)------------------------------ % 8.33/1.61 % (3322612)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=2464317613:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 8.33/1.61 % (3322612)Refutation not found, incomplete strategy % 8.33/1.61 % (3322612)------------------------------ % 8.33/1.61 % (3322612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.33/1.61 % (3322612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.34 % (3322612)CaDiCaL version: 2.1.3 % 13.84/2.34 % (3322612)Termination reason: Refutation not found, incomplete strategy % 13.84/2.34 % (3322612)Time elapsed: 0.006 s % 13.84/2.34 % (3322612)Peak memory usage: 88 MB % 13.84/2.34 % (3322612)Instructions burned: 20 (million) % 13.84/2.34 % (3322613)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1753653885: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) % 13.84/2.34 % (3322614)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=980393741:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 13.84/2.34 % (3322614)Refutation not found, incomplete strategy % 13.84/2.34 % (3322614)------------------------------ % 13.84/2.34 % (3322614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.34 % (3322614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.34 % (3322614)CaDiCaL version: 2.1.3 % 13.84/2.34 % (3322614)Termination reason: Refutation not found, incomplete strategy % 13.84/2.34 % (3322614)Time elapsed: 0.006 s % 13.84/2.34 % (3322614)Peak memory usage: 88 MB % 13.84/2.34 % (3322614)Instructions burned: 21 (million) % 13.84/2.34 % (3322613)Refutation not found, incomplete strategy % 13.84/2.34 % (3322613)------------------------------ % 13.84/2.34 % (3322613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.34 % (3322613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.34 % (3322613)CaDiCaL version: 2.1.3 % 13.84/2.34 % (3322613)Termination reason: Refutation not found, incomplete strategy % 13.84/2.34 % (3322613)Time elapsed: 0.014 s % 13.84/2.34 % (3322613)Peak memory usage: 88 MB % 13.84/2.34 % (3322613)Instructions burned: 52 (million) % 13.84/2.34 % (3322615)lrs+10_64_to=lpo:sil=8000:random_seed=2392327188:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 13.84/2.34 % (3322615)Instruction limit reached! % 13.84/2.34 % (3322615)------------------------------ % 13.84/2.34 % (3322615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.34 % (3322615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.34 % (3322615)CaDiCaL version: 2.1.3 % 13.84/2.34 % (3322615)Termination reason: Instruction limit % 13.84/2.34 % (3322615)Termination phase: Saturation % 13.84/2.34 % (3322615)Time elapsed: 0.031 s % 13.84/2.34 % (3322615)Peak memory usage: 88 MB % 13.84/2.34 % (3322615)Instructions burned: 129 (million) % 13.84/2.34 % (3322612)------------------------------ % 13.84/2.34 % (3322612)------------------------------ % 13.84/2.34 % (3322614)------------------------------ % 13.84/2.34 % (3322614)------------------------------ % 13.84/2.34 % (3322613)------------------------------ % 13.84/2.34 % (3322613)------------------------------ % 13.84/2.34 % (3322620)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1042139279:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 13.84/2.34 % (3322621)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2204848225:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 13.84/2.34 % (3322620)Instruction limit reached! % 13.84/2.34 % (3322620)------------------------------ % 13.84/2.34 % (3322620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.34 % (3322620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.34 % (3322620)CaDiCaL version: 2.1.3 % 13.84/2.34 % (3322620)Termination reason: Instruction limit % 13.84/2.34 % (3322620)Termination phase: Saturation % 13.84/2.34 % (3322620)Time elapsed: 0.060 s % 13.84/2.34 % (3322620)Peak memory usage: 91 MB % 13.84/2.34 % (3322620)Instructions burned: 194 (million) % 13.84/2.34 % (3322621)Instruction limit reached! % 13.84/2.34 % (3322621)------------------------------ % 13.84/2.34 % (3322621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.34 % (3322621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.34 % (3322621)CaDiCaL version: 2.1.3 % 13.84/2.34 % (3322621)Termination reason: Instruction limit % 13.84/2.34 % (3322621)Termination phase: Saturation % 13.84/2.34 % (3322621)Time elapsed: 0.048 s % 13.84/2.34 % (3322621)Peak memory usage: 92 MB % 13.84/2.34 % (3322621)Instructions burned: 158 (million) % 13.84/2.34 % (3322623)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=3323526122:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 20.93/3.39 % (3322622)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2581216583:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 20.93/3.39 % (3322623)Refutation not found, incomplete strategy % 20.93/3.39 % (3322623)------------------------------ % 20.93/3.39 % (3322623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/3.39 % (3322623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.39 % (3322623)CaDiCaL version: 2.1.3 % 20.93/3.39 % (3322623)Termination reason: Refutation not found, incomplete strategy % 20.93/3.39 % (3322623)Time elapsed: 0.008 s % 20.93/3.39 % (3322623)Peak memory usage: 88 MB % 20.93/3.39 % (3322623)Instructions burned: 27 (million) % 20.93/3.39 % (3322627)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=495815226:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 20.93/3.39 % (3322626)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3889743434:i=107_2993 on theBenchmark for (2993ds/107Mi) % 20.93/3.39 % (3322626)Instruction limit reached! % 20.93/3.39 % (3322626)------------------------------ % 20.93/3.39 % (3322626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/3.39 % (3322626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.39 % (3322626)CaDiCaL version: 2.1.3 % 20.93/3.39 % (3322626)Termination reason: Instruction limit % 20.93/3.39 % (3322626)Termination phase: Saturation % 20.93/3.39 % (3322626)Time elapsed: 0.036 s % 20.93/3.39 % (3322626)Peak memory usage: 88 MB % 20.93/3.39 % (3322626)Instructions burned: 107 (million) % 20.93/3.39 % (3322627)Instruction limit reached! % 20.93/3.39 % (3322627)------------------------------ % 20.93/3.39 % (3322627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/3.39 % (3322627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.39 % (3322627)CaDiCaL version: 2.1.3 % 20.93/3.39 % (3322627)Termination reason: Instruction limit % 20.93/3.39 % (3322627)Termination phase: Saturation % 20.93/3.39 % (3322627)Time elapsed: 0.071 s % 20.93/3.39 % (3322627)Peak memory usage: 91 MB % 20.93/3.39 % (3322627)Instructions burned: 243 (million) % 20.93/3.39 % (3322623)------------------------------ % 20.93/3.39 % (3322623)------------------------------ % 20.93/3.39 % (3322632)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3275609331:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 20.93/3.39 % (3322633)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3123950418:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi) % 20.93/3.39 % (3322633)Refutation not found, incomplete strategy % 20.93/3.39 % (3322633)------------------------------ % 20.93/3.39 % (3322633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/3.39 % (3322633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.39 % (3322633)CaDiCaL version: 2.1.3 % 20.93/3.39 % (3322633)Termination reason: Refutation not found, incomplete strategy % 20.93/3.39 % (3322633)Time elapsed: 0.005 s % 20.93/3.39 % (3322633)Peak memory usage: 88 MB % 20.93/3.39 % (3322633)Instructions burned: 17 (million) % 20.93/3.39 % (3322634)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1476071009:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi) % 20.93/3.39 % (3322633)------------------------------ % 20.93/3.39 % (3322633)------------------------------ % 20.93/3.39 % (3322634)Instruction limit reached! % 20.93/3.39 % (3322634)------------------------------ % 20.93/3.39 % (3322634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.93/3.39 % (3322634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.39 % (3322634)CaDiCaL version: 2.1.3 % 20.93/3.39 % (3322634)Termination reason: Instruction limit % 20.93/3.39 % (3322634)Termination phase: Saturation % 20.93/3.39 % (3322634)Time elapsed: 0.174 s % 20.93/3.39 % (3322634)Peak memory usage: 95 MB % 20.93/3.39 % (3322634)Instructions burned: 500 (million) % 20.93/3.39 % (3322638)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2609959511:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi) % 20.93/3.39 % (3322639)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3185593014:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 29.32/4.52 % (3322638)Instruction limit reached! % 29.32/4.52 % (3322638)------------------------------ % 29.32/4.52 % (3322638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.32/4.52 % (3322638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.32/4.52 % (3322638)CaDiCaL version: 2.1.3 % 29.32/4.52 % (3322638)Termination reason: Instruction limit % 29.32/4.52 % (3322638)Termination phase: Saturation % 29.32/4.52 % (3322638)Time elapsed: 0.049 s % 29.32/4.52 % (3322638)Peak memory usage: 89 MB % 29.32/4.52 % (3322638)Instructions burned: 195 (million) % 29.32/4.52 % (3322639)Instruction limit reached! % 29.32/4.52 % (3322639)------------------------------ % 29.32/4.52 % (3322639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.32/4.52 % (3322639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.32/4.52 % (3322639)CaDiCaL version: 2.1.3 % 29.32/4.52 % (3322639)Termination reason: Instruction limit % 29.32/4.52 % (3322639)Termination phase: Saturation % 29.32/4.52 % (3322639)Time elapsed: 0.073 s % 29.32/4.52 % (3322639)Peak memory usage: 92 MB % 29.32/4.52 % (3322639)Instructions burned: 264 (million) % 29.32/4.52 % (3322642)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2323008075:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 29.32/4.52 % (3322642)Instruction limit reached! % 29.32/4.52 % (3322642)------------------------------ % 29.32/4.52 % (3322642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.32/4.52 % (3322642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.32/4.52 % (3322642)CaDiCaL version: 2.1.3 % 29.32/4.52 % (3322642)Termination reason: Instruction limit % 29.32/4.52 % (3322642)Termination phase: Saturation % 29.32/4.52 % (3322642)Time elapsed: 0.045 s % 29.32/4.52 % (3322642)Peak memory usage: 90 MB % 29.32/4.52 % (3322642)Instructions burned: 160 (million) % 29.32/4.52 % (3322643)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=2920747562:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi) % 29.32/4.52 % (3322645)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2645913931:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi) % 29.32/4.52 % (3322645)Instruction limit reached! % 29.32/4.52 % (3322645)------------------------------ % 29.32/4.52 % (3322645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.32/4.52 % (3322645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.32/4.52 % (3322645)CaDiCaL version: 2.1.3 % 29.32/4.52 % (3322645)Termination reason: Instruction limit % 29.32/4.52 % (3322645)Termination phase: Saturation % 29.32/4.52 % (3322645)Time elapsed: 0.149 s % 29.32/4.52 % (3322645)Peak memory usage: 93 MB % 29.32/4.52 % (3322645)Instructions burned: 537 (million) % 29.32/4.52 % (3322648)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=96271039:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi) % 29.32/4.52 % (3322622)Instruction limit reached! % 29.32/4.52 % (3322622)------------------------------ % 29.32/4.52 % (3322622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.32/4.52 % (3322622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.32/4.52 % (3322622)CaDiCaL version: 2.1.3 % 29.32/4.52 % (3322622)Termination reason: Instruction limit % 29.32/4.52 % (3322622)Termination phase: Saturation % 29.32/4.52 % (3322622)Time elapsed: 1.194 s % 29.32/4.52 % (3322622)Peak memory usage: 150 MB % 29.32/4.52 % (3322622)Instructions burned: 3395 (million) % 29.32/4.52 % (3322648)Instruction limit reached! % 29.32/4.52 % (3322648)------------------------------ % 29.32/4.52 % (3322648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.32/4.52 % (3322648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.32/4.52 % (3322648)CaDiCaL version: 2.1.3 % 29.32/4.52 % (3322648)Termination reason: Instruction limit % 29.32/4.52 % (3322648)Termination phase: Saturation % 29.32/4.52 % (3322648)Time elapsed: 0.044 s % 29.32/4.52 % (3322648)Peak memory usage: 89 MB % 29.32/4.52 % (3322648)Instructions burned: 180 (million) % 29.32/4.52 % (3322650)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=3675463747:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi) % 33.68/5.18 % (3322651)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=1328545451:i=412:gtgl=4:gtg=exists_all_2980 on theBenchmark for (2980ds/412Mi) % 33.68/5.18 % (3322651)Instruction limit reached! % 33.68/5.18 % (3322651)------------------------------ % 33.68/5.18 % (3322651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.68/5.18 % (3322651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.68/5.18 % (3322651)CaDiCaL version: 2.1.3 % 33.68/5.18 % (3322651)Termination reason: Instruction limit % 33.68/5.18 % (3322651)Termination phase: Saturation % 33.68/5.18 % (3322651)Time elapsed: 0.131 s % 33.68/5.18 % (3322651)Peak memory usage: 95 MB % 33.68/5.18 % (3322651)Instructions burned: 414 (million) % 33.68/5.18 % (3322654)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=4136272313:s2pl=no:i=8478:s2at=4:nm=6_2978 on theBenchmark for (2978ds/8478Mi) % 33.68/5.18 % (3322632)Instruction limit reached! % 33.68/5.18 % (3322632)------------------------------ % 33.68/5.18 % (3322632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.68/5.18 % (3322632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.68/5.18 % (3322632)CaDiCaL version: 2.1.3 % 33.68/5.18 % (3322632)Termination reason: Instruction limit % 33.68/5.18 % (3322632)Termination phase: Saturation % 33.68/5.18 % (3322632)Time elapsed: 1.670 s % 33.68/5.18 % (3322632)Peak memory usage: 170 MB % 33.68/5.18 % (3322632)Instructions burned: 5212 (million) % 33.68/5.18 % (3322643)Instruction limit reached! % 33.68/5.18 % (3322643)------------------------------ % 33.68/5.18 % (3322643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.68/5.18 % (3322643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.68/5.18 % (3322643)CaDiCaL version: 2.1.3 % 33.68/5.18 % (3322643)Termination reason: Instruction limit % 33.68/5.18 % (3322643)Termination phase: Saturation % 33.68/5.18 % (3322643)Time elapsed: 1.138 s % 33.68/5.18 % (3322643)Peak memory usage: 150 MB % 33.68/5.18 % (3322643)Instructions burned: 3256 (million) % 33.68/5.18 % (3322656)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=1546535974:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2973 on theBenchmark for (2973ds/303Mi) % 33.68/5.18 % (3322657)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3035694828:st=4:i=720:sd=3:fsr=off:ss=axioms_2973 on theBenchmark for (2973ds/720Mi) % 33.68/5.18 % (3322657)Refutation not found, incomplete strategy % 33.68/5.18 % (3322657)------------------------------ % 33.68/5.18 % (3322657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.68/5.18 % (3322657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.68/5.18 % (3322657)CaDiCaL version: 2.1.3 % 33.68/5.18 % (3322657)Termination reason: Refutation not found, incomplete strategy % 33.68/5.18 % (3322657)Time elapsed: 0.006 s % 33.68/5.18 % (3322657)Peak memory usage: 88 MB % 33.68/5.18 % (3322657)Instructions burned: 24 (million) % 33.68/5.18 % (3322656)Refutation not found, incomplete strategy % 33.68/5.18 % (3322656)------------------------------ % 33.68/5.18 % (3322656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.68/5.18 % (3322656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.68/5.18 % (3322656)CaDiCaL version: 2.1.3 % 33.68/5.18 % (3322656)Termination reason: Refutation not found, incomplete strategy % 33.68/5.18 % (3322656)Time elapsed: 0.040 s % 33.68/5.18 % (3322656)Peak memory usage: 90 MB % 33.68/5.18 % (3322656)Instructions burned: 177 (million) % 33.68/5.18 % (3322656)------------------------------ % 33.68/5.18 % (3322656)------------------------------ % 33.68/5.18 % (3322657)------------------------------ % 33.68/5.18 % (3322657)------------------------------ % 33.68/5.18 % (3322661)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3041952926:i=2989:sd=3:ss=axioms:sgt=60_2970 on theBenchmark for (2970ds/2989Mi) % 33.68/5.18 % (3322660)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=526932241:i=598:bs=on:bd=preordered:av=off:ss=axioms_2970 on theBenchmark for (2970ds/598Mi) % 33.68/5.18 % (3322660)Refutation not found, incomplete strategy % 34.72/5.32 % (3322660)------------------------------ % 34.72/5.32 % (3322660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.72/5.32 % (3322660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.32 % (3322660)CaDiCaL version: 2.1.3 % 34.72/5.32 % (3322660)Termination reason: Refutation not found, incomplete strategy % 34.72/5.32 % (3322660)Time elapsed: 0.007 s % 34.72/5.32 % (3322660)Peak memory usage: 88 MB % 34.72/5.32 % (3322660)Instructions burned: 28 (million) % 34.72/5.32 % (3322660)------------------------------ % 34.72/5.32 % (3322660)------------------------------ % 34.72/5.32 [W928 11:27:37.450788546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.72/5.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.72/5.32 [W928 11:27:37.450811122 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.72/5.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.72/5.32 [W928 11:27:37.450832523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.72/5.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.72/5.32 [W928 11:27:37.450840163 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.72/5.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.72/5.32 [W928 11:27:37.450855402 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.72/5.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.72/5.32 [W928 11:27:37.450862079 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.72/5.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.72/5.32 % (3322664)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=1895076092:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2967 on theBenchmark for (2967ds/1997Mi) % 34.72/5.32 % (3322661)Refutation not found, incomplete strategy % 34.72/5.32 % (3322661)------------------------------ % 34.72/5.32 % (3322661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.72/5.32 % (3322661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.32 % (3322661)CaDiCaL version: 2.1.3 % 34.72/5.32 % (3322661)Termination reason: Refutation not found, incomplete strategy % 34.72/5.32 % (3322661)Time elapsed: 0.351 s % 34.72/5.32 % (3322661)Peak memory usage: 133 MB % 34.72/5.32 % (3322661)Instructions burned: 973 (million) % 34.72/5.32 % (3322661)------------------------------ % 34.72/5.32 % (3322661)------------------------------ % 34.72/5.32 % (3322666)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=3902496028:i=2088:bd=preordered:av=off_2964 on theBenchmark for (2964ds/2088Mi) % 34.72/5.32 % (3322664)Instruction limit reached! % 34.72/5.32 % (3322664)------------------------------ % 34.72/5.32 % (3322664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.72/5.32 % (3322664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.32 % (3322664)CaDiCaL version: 2.1.3 % 34.72/5.32 % (3322664)Termination reason: Instruction limit % 34.72/5.32 % (3322664)Termination phase: Saturation % 34.72/5.32 % (3322664)Time elapsed: 0.697 s % 34.72/5.32 % (3322664)Peak memory usage: 138 MB % 34.72/5.32 % (3322664)Instructions burned: 1997 (million) % 34.72/5.32 % (3322668)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=859640839:i=1098:nicw=on_2959 on theBenchmark for (2959ds/1098Mi) % 37.00/5.80 % (3322666)Instruction limit reached! % 37.00/5.80 % (3322666)------------------------------ % 37.00/5.80 % (3322666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.00/5.80 % (3322666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.00/5.80 % (3322666)CaDiCaL version: 2.1.3 % 37.00/5.80 % (3322666)Termination reason: Instruction limit % 37.00/5.80 % (3322666)Termination phase: Saturation % 37.00/5.80 % (3322666)Time elapsed: 0.712 s % 37.00/5.80 % (3322666)Peak memory usage: 139 MB % 37.00/5.80 % (3322666)Instructions burned: 2088 (million) % 37.00/5.80 % (3322650)Instruction limit reached! % 37.00/5.80 % (3322650)------------------------------ % 37.00/5.80 % (3322650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.00/5.80 % (3322650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.00/5.80 % (3322650)CaDiCaL version: 2.1.3 % 37.00/5.80 % (3322650)Termination reason: Instruction limit % 37.00/5.80 % (3322650)Termination phase: Saturation % 37.00/5.80 % (3322650)Time elapsed: 2.504 s % 37.00/5.80 % (3322650)Peak memory usage: 144 MB % 37.00/5.80 % (3322650)Instructions burned: 10310 (million) % 37.00/5.80 % (3322668)Instruction limit reached! % 37.00/5.80 % (3322668)------------------------------ % 37.00/5.80 % (3322668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.00/5.80 % (3322668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.00/5.80 % (3322668)CaDiCaL version: 2.1.3 % 37.00/5.80 % (3322668)Termination reason: Instruction limit % 37.00/5.80 % (3322668)Termination phase: Saturation % 37.00/5.80 % (3322668)Time elapsed: 0.362 s % 37.00/5.80 % (3322668)Peak memory usage: 107 MB % 37.00/5.80 % (3322668)Instructions burned: 1098 (million) % 37.00/5.80 % (3322670)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1738891073:i=433:bd=preordered_2955 on theBenchmark for (2955ds/433Mi) % 37.00/5.80 % (3322671)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3747809396:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2954 on theBenchmark for (2954ds/2942Mi) % 37.00/5.80 % (3322670)Instruction limit reached! % 37.00/5.80 % (3322670)------------------------------ % 37.00/5.80 % (3322670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.00/5.80 % (3322670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.00/5.80 % (3322670)CaDiCaL version: 2.1.3 % 37.00/5.80 % (3322670)Termination reason: Instruction limit % 37.00/5.80 % (3322670)Termination phase: Saturation % 37.00/5.80 % (3322670)Time elapsed: 0.112 s % 37.00/5.80 % (3322670)Peak memory usage: 91 MB % 37.00/5.80 % (3322670)Instructions burned: 433 (million) % 37.00/5.80 % (3322673)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2866505165:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2954 on theBenchmark for (2954ds/6922Mi) % 37.00/5.80 % (3322676)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=2667102908:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2953 on theBenchmark for (2953ds/596Mi) % 37.00/5.80 % (3322676)Refutation not found, incomplete strategy % 37.00/5.80 % (3322676)------------------------------ % 37.00/5.80 % (3322676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.00/5.80 % (3322676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.00/5.80 % (3322676)CaDiCaL version: 2.1.3 % 37.00/5.80 % (3322676)Termination reason: Refutation not found, incomplete strategy % 37.00/5.80 % (3322676)Time elapsed: 0.022 s % 37.00/5.80 % (3322676)Peak memory usage: 89 MB % 37.00/5.80 % (3322676)Instructions burned: 84 (million) % 37.00/5.80 [W928 11:27:39.035926915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.00/5.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.00/5.80 [W928 11:27:39.035948054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.035986539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.035998028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.036020505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.036026305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.067440588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.067478877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.067498924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.067504910 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.067518400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 [W928 11:27:39.067524950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.18/8.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.18/8.03 % (3322654)Instruction limit reached! % 54.18/8.03 % (3322654)------------------------------ % 54.18/8.03 % (3322654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.18/8.03 % (3322654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.18/8.03 % (3322654)CaDiCaL version: 2.1.3 % 54.18/8.03 % (3322654)Termination reason: Instruction limit % 54.18/8.03 % (3322654)Termination phase: Saturation % 54.18/8.03 % (3322654)Time elapsed: 2.602 s % 54.18/8.03 % (3322654)Peak memory usage: 182 MB % 54.18/8.03 % (3322654)Instructions burned: 8478 (million) % 54.18/8.03 % (3322676)------------------------------ % 54.18/8.03 % (3322676)------------------------------ % 54.18/8.03 % (3322671)Refutation not found, incomplete strategy % 54.18/8.03 % (3322671)------------------------------ % 54.18/8.03 % (3322671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.18/8.03 % (3322671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.15/8.96 % (3322671)CaDiCaL version: 2.1.3 % 59.15/8.96 % (3322671)Termination reason: Refutation not found, incomplete strategy % 59.15/8.96 % (3322671)Time elapsed: 0.353 s % 59.15/8.96 % (3322671)Peak memory usage: 133 MB % 59.15/8.96 % (3322671)Instructions burned: 980 (million) % 59.15/8.96 % (3322673)Refutation not found, incomplete strategy % 59.15/8.96 % (3322673)------------------------------ % 59.15/8.96 % (3322673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.15/8.96 % (3322673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.15/8.96 % (3322673)CaDiCaL version: 2.1.3 % 59.15/8.96 % (3322673)Termination reason: Refutation not found, incomplete strategy % 59.15/8.96 % (3322673)Time elapsed: 0.358 s % 59.15/8.96 % (3322673)Peak memory usage: 132 MB % 59.15/8.96 % (3322673)Instructions burned: 981 (million) % 59.15/8.96 % (3322679)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=130672010:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2950 on theBenchmark for (2950ds/4123Mi) % 59.15/8.96 % (3322680)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3557670091:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2950 on theBenchmark for (2950ds/16411Mi) % 59.15/8.96 % (3322671)------------------------------ % 59.15/8.96 % (3322671)------------------------------ % 59.15/8.96 % (3322673)------------------------------ % 59.15/8.96 % (3322673)------------------------------ % 59.15/8.96 % (3322683)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3560447196:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2948 on theBenchmark for (2948ds/1670Mi) % 59.15/8.96 % (3322684)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=2587321045:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2948 on theBenchmark for (2948ds/1722Mi) % 59.15/8.96 [W928 11:27:39.517464851 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.15/8.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.15/8.96 [W928 11:27:39.517481013 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.15/8.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.15/8.96 [W928 11:27:39.517508114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.15/8.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.15/8.96 [W928 11:27:39.517514451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.15/8.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.15/8.96 [W928 11:27:39.517526751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.15/8.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.15/8.96 [W928 11:27:39.517532551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.15/8.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.15/8.96 % (3322680)Refutation not found, incomplete strategy % 59.15/8.96 % (3322680)------------------------------ % 59.15/8.96 % (3322680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.15/8.96 % (3322680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.15/8.96 % (3322680)CaDiCaL version: 2.1.3 % 73.07/10.73 % (3322680)Termination reason: Refutation not found, incomplete strategy % 73.07/10.73 % (3322680)Time elapsed: 0.352 s % 73.07/10.73 % (3322680)Peak memory usage: 132 MB % 73.07/10.73 % (3322680)Instructions burned: 975 (million) % 73.07/10.73 % (3322680)------------------------------ % 73.07/10.73 % (3322680)------------------------------ % 73.07/10.73 % (3322687)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=1096432816:cts=off:cond=on:i=9530:bs=on:fsd=on_2943 on theBenchmark for (2943ds/9530Mi) % 73.07/10.73 % (3322683)Instruction limit reached! % 73.07/10.73 % (3322683)------------------------------ % 73.07/10.73 % (3322683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.07/10.73 % (3322683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.07/10.73 % (3322683)CaDiCaL version: 2.1.3 % 73.07/10.73 % (3322683)Termination reason: Instruction limit % 73.07/10.73 % (3322683)Termination phase: Saturation % 73.07/10.73 % (3322683)Time elapsed: 0.608 s % 73.07/10.73 % (3322683)Peak memory usage: 134 MB % 73.07/10.73 % (3322683)Instructions burned: 1670 (million) % 73.07/10.73 % (3322684)Instruction limit reached! % 73.07/10.73 % (3322684)------------------------------ % 73.07/10.73 % (3322684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.07/10.73 % (3322684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.07/10.73 % (3322684)CaDiCaL version: 2.1.3 % 73.07/10.73 % (3322684)Termination reason: Instruction limit % 73.07/10.73 % (3322684)Termination phase: Saturation % 73.07/10.73 % (3322684)Time elapsed: 0.586 s % 73.07/10.73 % (3322684)Peak memory usage: 135 MB % 73.07/10.73 % (3322684)Instructions burned: 1725 (million) % 73.07/10.73 % (3322689)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=211945444:st=2:i=4495:sd=10:ss=included_2941 on theBenchmark for (2941ds/4495Mi) % 73.07/10.73 % (3322690)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=2068158638:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2940 on theBenchmark for (2940ds/4920Mi) % 73.07/10.73 % (3322679)Instruction limit reached! % 73.07/10.73 % (3322679)------------------------------ % 73.07/10.73 % (3322679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.07/10.73 % (3322679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.07/10.73 % (3322679)CaDiCaL version: 2.1.3 % 73.07/10.73 % (3322679)Termination reason: Instruction limit % 73.07/10.73 % (3322679)Termination phase: Saturation % 73.07/10.73 % (3322679)Time elapsed: 1.347 s % 73.07/10.73 % (3322679)Peak memory usage: 160 MB % 73.07/10.73 % (3322679)Instructions burned: 4127 (million) % 73.07/10.73 % (3322693)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=2893103895:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2935 on theBenchmark for (2935ds/2083Mi) % 73.07/10.73 % (3322693)Instruction limit reached! % 73.07/10.73 % (3322693)------------------------------ % 73.07/10.73 % (3322693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.07/10.73 % (3322693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.07/10.73 % (3322693)CaDiCaL version: 2.1.3 % 73.07/10.73 % (3322693)Termination reason: Instruction limit % 73.07/10.73 % (3322693)Termination phase: Saturation % 73.07/10.73 % (3322693)Time elapsed: 0.750 s % 73.07/10.73 % (3322693)Peak memory usage: 139 MB % 73.07/10.73 % (3322693)Instructions burned: 2083 (million) % 73.07/10.73 % (3322695)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=598990533:i=4629:av=off:gsp=on_2927 on theBenchmark for (2927ds/4629Mi) % 73.07/10.73 % (3322689)Instruction limit reached! % 73.07/10.73 % (3322689)------------------------------ % 73.07/10.73 % (3322689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.07/10.73 % (3322689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.07/10.73 % (3322689)CaDiCaL version: 2.1.3 % 73.07/10.73 % (3322689)Termination reason: Instruction limit % 73.07/10.73 % (3322689)Termination phase: Saturation % 73.07/10.73 % (3322689)Time elapsed: 1.602 s % 73.07/10.73 % (3322689)Peak memory usage: 160 MB % 73.07/10.73 % (3322689)Instructions burned: 4498 (million) % 73.07/10.73 % (3322690)Instruction limit reached! % 76.54/11.23 % (3322690)------------------------------ % 76.54/11.23 % (3322690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.54/11.23 % (3322690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.54/11.23 % (3322690)CaDiCaL version: 2.1.3 % 76.54/11.23 % (3322690)Termination reason: Instruction limit % 76.54/11.23 % (3322690)Termination phase: Saturation % 76.54/11.23 % (3322690)Time elapsed: 1.659 s % 76.54/11.23 % (3322690)Peak memory usage: 164 MB % 76.54/11.23 % (3322690)Instructions burned: 4922 (million) % 76.54/11.23 % (3322697)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=273359116:i=1258:av=off_2923 on theBenchmark for (2923ds/1258Mi) % 76.54/11.23 % (3322698)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3875392726:i=7343:av=off:ss=included_2922 on theBenchmark for (2922ds/7343Mi) % 76.54/11.23 % (3322697)Instruction limit reached! % 76.54/11.23 % (3322697)------------------------------ % 76.54/11.23 % (3322697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.54/11.23 % (3322697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.54/11.23 % (3322697)CaDiCaL version: 2.1.3 % 76.54/11.23 % (3322697)Termination reason: Instruction limit % 76.54/11.23 % (3322697)Termination phase: Saturation % 76.54/11.23 % (3322697)Time elapsed: 0.394 s % 76.54/11.23 % (3322697)Peak memory usage: 101 MB % 76.54/11.23 % (3322697)Instructions burned: 1260 (million) % 76.54/11.23 % (3322687)Instruction limit reached! % 76.54/11.23 % (3322687)------------------------------ % 76.54/11.23 % (3322687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.54/11.23 % (3322687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.54/11.23 % (3322687)CaDiCaL version: 2.1.3 % 76.54/11.23 % (3322687)Termination reason: Instruction limit % 76.54/11.23 % (3322687)Termination phase: Saturation % 76.54/11.23 % (3322687)Time elapsed: 2.513 s % 76.54/11.23 % (3322687)Peak memory usage: 147 MB % 76.54/11.23 % (3322687)Instructions burned: 9532 (million) % 76.54/11.23 % (3322701)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=507266577:i=1325:sd=2:ss=axioms:sgt=16_2918 on theBenchmark for (2918ds/1325Mi) % 76.54/11.23 % (3322701)Refutation not found, incomplete strategy % 76.54/11.23 % (3322701)------------------------------ % 76.54/11.23 % (3322701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.54/11.23 % (3322701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.54/11.23 % (3322701)CaDiCaL version: 2.1.3 % 76.54/11.23 % (3322701)Termination reason: Refutation not found, incomplete strategy % 76.54/11.23 % (3322701)Time elapsed: 0.005 s % 76.54/11.23 % (3322701)Peak memory usage: 88 MB % 76.54/11.23 % (3322701)Instructions burned: 21 (million) % 76.54/11.23 % (3322703)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=2367623023:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2917 on theBenchmark for (2917ds/2646Mi) % 76.54/11.23 % (3322701)------------------------------ % 76.54/11.23 % (3322701)------------------------------ % 76.54/11.23 % (3322705)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3697820556:i=1489:sd=2:ep=R:ss=axioms_2915 on theBenchmark for (2915ds/1489Mi) % 76.54/11.23 [W928 11:27:43.815475201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.54/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.54/11.23 [W928 11:27:43.815495312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.54/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.54/11.23 [W928 11:27:43.815531941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.54/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.54/11.23 [W928 11:27:43.815538225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.54/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.54/11.76 [W928 11:27:43.815555821 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.54/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.54/11.76 [W928 11:27:43.815561307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.54/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.54/11.76 % (3322703)Refutation not found, incomplete strategy % 79.54/11.76 % (3322703)------------------------------ % 79.54/11.76 % (3322703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.54/11.76 % (3322703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.54/11.76 % (3322703)CaDiCaL version: 2.1.3 % 79.54/11.76 % (3322703)Termination reason: Refutation not found, incomplete strategy % 79.54/11.76 % (3322703)Time elapsed: 0.350 s % 79.54/11.76 % (3322703)Peak memory usage: 133 MB % 79.54/11.76 % (3322703)Instructions burned: 975 (million) % 79.54/11.76 % (3322703)------------------------------ % 79.54/11.76 % (3322703)------------------------------ % 79.54/11.76 % (3322705)Refutation not found, incomplete strategy % 79.54/11.76 % (3322705)------------------------------ % 79.54/11.76 % (3322705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.54/11.76 % (3322705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.54/11.76 % (3322705)CaDiCaL version: 2.1.3 % 79.54/11.76 % (3322705)Termination reason: Refutation not found, incomplete strategy % 79.54/11.76 % (3322705)Time elapsed: 0.353 s % 79.54/11.76 % (3322705)Peak memory usage: 131 MB % 79.54/11.76 % (3322705)Instructions burned: 970 (million) % 79.54/11.76 % (3322707)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=2401511409:i=1503_2910 on theBenchmark for (2910ds/1503Mi) % 79.54/11.76 % (3322705)------------------------------ % 79.54/11.76 % (3322705)------------------------------ % 79.54/11.76 % (3322695)Instruction limit reached! % 79.54/11.76 % (3322695)------------------------------ % 79.54/11.76 % (3322695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.54/11.76 % (3322695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.54/11.76 % (3322695)CaDiCaL version: 2.1.3 % 79.54/11.76 % (3322695)Termination reason: Instruction limit % 79.54/11.76 % (3322695)Termination phase: Saturation % 79.54/11.76 % (3322695)Time elapsed: 1.729 s % 79.54/11.76 % (3322695)Peak memory usage: 156 MB % 79.54/11.76 % (3322695)Instructions burned: 4630 (million) % 79.54/11.76 % (3322709)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1450878496:i=13942:kws=frequency_2908 on theBenchmark for (2908ds/13942Mi) % 79.54/11.76 % (3322710)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=1466797342:i=3604:fsr=off:er=filter_2908 on theBenchmark for (2908ds/3604Mi) % 79.54/11.76 % (3322707)Instruction limit reached! % 79.54/11.76 % (3322707)------------------------------ % 79.54/11.76 % (3322707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.54/11.76 % (3322707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.54/11.76 % (3322707)CaDiCaL version: 2.1.3 % 79.54/11.76 % (3322707)Termination reason: Instruction limit % 79.54/11.76 % (3322707)Termination phase: Saturation % 79.54/11.76 % (3322707)Time elapsed: 0.564 s % 79.54/11.76 % (3322707)Peak memory usage: 134 MB % 79.54/11.76 % (3322707)Instructions burned: 1503 (million) % 79.54/11.76 % (3322713)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2438531917:i=1876:sd=1:ss=included:sgt=32_2903 on theBenchmark for (2903ds/1876Mi) % 79.54/11.76 % (3322698)Instruction limit reached! % 79.54/11.76 % (3322698)------------------------------ % 79.54/11.76 % (3322698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.54/11.76 % (3322698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.31/14.03 % (3322698)CaDiCaL version: 2.1.3 % 96.31/14.03 % (3322698)Termination reason: Instruction limit % 96.31/14.03 % (3322698)Termination phase: Saturation % 96.31/14.03 % (3322698)Time elapsed: 2.554 s % 96.31/14.03 % (3322698)Peak memory usage: 185 MB % 96.31/14.03 % (3322698)Instructions burned: 7343 (million) % 96.31/14.03 % (3322713)Instruction limit reached! % 96.31/14.03 % (3322713)------------------------------ % 96.31/14.03 % (3322713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.31/14.03 % (3322713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.31/14.03 % (3322713)CaDiCaL version: 2.1.3 % 96.31/14.03 % (3322713)Termination reason: Instruction limit % 96.31/14.03 % (3322713)Termination phase: Saturation % 96.31/14.03 % (3322713)Time elapsed: 0.688 s % 96.31/14.03 % (3322713)Peak memory usage: 137 MB % 96.31/14.03 % (3322713)Instructions burned: 1878 (million) % 96.31/14.03 % (3322715)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=71412355:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2895 on theBenchmark for (2895ds/1932Mi) % 96.31/14.03 % (3322710)Instruction limit reached! % 96.31/14.03 % (3322710)------------------------------ % 96.31/14.03 % (3322710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.31/14.03 % (3322710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.31/14.03 % (3322710)CaDiCaL version: 2.1.3 % 96.31/14.03 % (3322710)Termination reason: Instruction limit % 96.31/14.03 % (3322710)Termination phase: Saturation % 96.31/14.03 % (3322710)Time elapsed: 1.280 s % 96.31/14.03 % (3322710)Peak memory usage: 152 MB % 96.31/14.03 % (3322710)Instructions burned: 3606 (million) % 96.31/14.03 % (3322716)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=336920415:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2895 on theBenchmark for (2895ds/1980Mi) % 96.31/14.03 % (3322718)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=3571502433:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2894 on theBenchmark for (2894ds/3902Mi) % 96.31/14.03 [W928 11:27:45.950092847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.31/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.31/14.03 [W928 11:27:45.950114699 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.31/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.31/14.03 [W928 11:27:45.950135047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.31/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.31/14.03 [W928 11:27:45.950142309 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.31/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.31/14.03 [W928 11:27:45.950157539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.31/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.31/14.03 [W928 11:27:45.950163930 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.31/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.31/14.03 [W928 11:27:45.085348812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.53/16.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.53/16.52 [W928 11:27:45.085390249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.53/16.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.53/16.52 [W928 11:27:45.085411532 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.53/16.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.53/16.52 [W928 11:27:45.085417662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.53/16.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.53/16.52 [W928 11:27:45.085431040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.53/16.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.53/16.52 [W928 11:27:45.085437189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.53/16.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.53/16.52 % (3322715)Refutation not found, incomplete strategy % 113.53/16.52 % (3322715)------------------------------ % 113.53/16.52 % (3322715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.53/16.52 % (3322715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.53/16.52 % (3322715)CaDiCaL version: 2.1.3 % 113.53/16.52 % (3322715)Termination reason: Refutation not found, incomplete strategy % 113.53/16.52 % (3322715)Time elapsed: 0.374 s % 113.53/16.52 % (3322715)Peak memory usage: 133 MB % 113.53/16.52 % (3322715)Instructions burned: 973 (million) % 113.53/16.52 % (3322718)Refutation not found, incomplete strategy % 113.53/16.52 % (3322718)------------------------------ % 113.53/16.52 % (3322718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.53/16.52 % (3322718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.53/16.52 % (3322718)CaDiCaL version: 2.1.3 % 113.53/16.52 % (3322718)Termination reason: Refutation not found, incomplete strategy % 113.53/16.52 % (3322718)Time elapsed: 0.356 s % 113.53/16.52 % (3322718)Peak memory usage: 133 MB % 113.53/16.52 % (3322718)Instructions burned: 977 (million) % 113.53/16.52 % (3322715)------------------------------ % 113.53/16.52 % (3322715)------------------------------ % 113.53/16.52 % (3322721)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3475784361:avsq=on:i=3916:aac=none:amm=off_2889 on theBenchmark for (2889ds/3916Mi) % 113.53/16.52 % (3322718)------------------------------ % 113.53/16.52 % (3322718)------------------------------ % 113.53/16.52 % (3322716)Instruction limit reached! % 113.53/16.52 % (3322716)------------------------------ % 113.53/16.52 % (3322716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.53/16.52 % (3322716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.53/16.52 % (3322716)CaDiCaL version: 2.1.3 % 113.53/16.52 % (3322716)Termination reason: Instruction limit % 113.53/16.52 % (3322716)Termination phase: Saturation % 113.53/16.52 % (3322716)Time elapsed: 0.716 s % 113.53/16.52 % (3322716)Peak memory usage: 138 MB % 113.53/16.52 % (3322716)Instructions burned: 1981 (million) % 113.53/16.52 % (3322723)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3038604723:cond=on:i=3940:av=off:er=known_2887 on theBenchmark for (2887ds/3940Mi) % 113.53/16.52 % (3322724)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2896033343:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2887 on theBenchmark for (2887ds/3980Mi) % 121.03/17.60 % (3322723)Instruction limit reached! % 121.03/17.60 % (3322723)------------------------------ % 121.03/17.60 % (3322723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.03/17.60 % (3322723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.03/17.60 % (3322723)CaDiCaL version: 2.1.3 % 121.03/17.60 % (3322723)Termination reason: Instruction limit % 121.03/17.60 % (3322723)Termination phase: Saturation % 121.03/17.60 % (3322723)Time elapsed: 1.231 s % 121.03/17.60 % (3322723)Peak memory usage: 155 MB % 121.03/17.60 % (3322723)Instructions burned: 3943 (million) % 121.03/17.60 % (3322721)Instruction limit reached! % 121.03/17.60 % (3322721)------------------------------ % 121.03/17.60 % (3322721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.03/17.60 % (3322721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.03/17.60 % (3322721)CaDiCaL version: 2.1.3 % 121.03/17.60 % (3322721)Termination reason: Instruction limit % 121.03/17.60 % (3322721)Termination phase: Saturation % 121.03/17.60 % (3322721)Time elapsed: 1.420 s % 121.03/17.60 % (3322721)Peak memory usage: 114 MB % 121.03/17.60 % (3322721)Instructions burned: 3919 (million) % 121.03/17.60 % (3322724)Instruction limit reached! % 121.03/17.60 % (3322724)------------------------------ % 121.03/17.60 % (3322724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.03/17.60 % (3322724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.03/17.60 % (3322724)CaDiCaL version: 2.1.3 % 121.03/17.60 % (3322724)Termination reason: Instruction limit % 121.03/17.60 % (3322724)Termination phase: Saturation % 121.03/17.60 % (3322724)Time elapsed: 1.240 s % 121.03/17.60 % (3322724)Peak memory usage: 159 MB % 121.03/17.60 % (3322724)Instructions burned: 3984 (million) % 121.03/17.60 % (3322728)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=226861358:cts=off:cond=on:i=4272:bs=on:fsd=on_2873 on theBenchmark for (2873ds/4272Mi) % 121.03/17.60 % (3322727)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=3606185921:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2873 on theBenchmark for (2873ds/2087Mi) % 121.03/17.60 % (3322729)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=352636518:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2873 on theBenchmark for (2873ds/2197Mi) % 121.03/17.60 % (3322727)Instruction limit reached! % 121.03/17.60 % (3322727)------------------------------ % 121.03/17.60 % (3322727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.03/17.60 % (3322727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.03/17.60 % (3322727)CaDiCaL version: 2.1.3 % 121.03/17.60 % (3322727)Termination reason: Instruction limit % 121.03/17.60 % (3322727)Termination phase: Saturation % 121.03/17.60 % (3322727)Time elapsed: 0.739 s % 121.03/17.60 % (3322727)Peak memory usage: 138 MB % 121.03/17.60 % (3322727)Instructions burned: 2090 (million) % 121.03/17.60 % (3322709)Instruction limit reached! % 121.03/17.60 % (3322709)------------------------------ % 121.03/17.60 % (3322709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.03/17.60 % (3322709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.03/17.60 % (3322709)CaDiCaL version: 2.1.3 % 121.03/17.60 % (3322709)Termination reason: Instruction limit % 121.03/17.60 % (3322709)Termination phase: Saturation % 121.03/17.60 % (3322709)Time elapsed: 4.335 s % 121.03/17.60 % (3322709)Peak memory usage: 184 MB % 121.03/17.60 % (3322709)Instructions burned: 13945 (million) % 121.03/17.60 % (3322729)Instruction limit reached! % 121.03/17.60 % (3322729)------------------------------ % 121.03/17.60 % (3322729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.03/17.60 % (3322729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.03/17.60 % (3322729)CaDiCaL version: 2.1.3 % 121.03/17.60 % (3322729)Termination reason: Instruction limit % 121.03/17.60 % (3322729)Termination phase: Saturation % 121.03/17.60 % (3322729)Time elapsed: 0.799 s % 121.03/17.60 % (3322729)Peak memory usage: 141 MB % 121.03/17.60 % (3322729)Instructions burned: 2198 (million) % 121.03/17.60 % (3322733)dis+21_1_sil=8000:spb=goal_then_units:random_seed=4275050791:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2865 on theBenchmark for (2865ds/6508Mi) % 121.03/17.60 % (3322734)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3746706379:i=2330:fgj=on:av=off:fsr=off_2864 on theBenchmark for (2864ds/2330Mi) % 164.52/23.77 % (3322735)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2845000100:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2863 on theBenchmark for (2863ds/7592Mi) % 164.52/23.77 % (3322728)Instruction limit reached! % 164.52/23.77 % (3322728)------------------------------ % 164.52/23.77 % (3322728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.52/23.77 % (3322728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.52/23.77 % (3322728)CaDiCaL version: 2.1.3 % 164.52/23.77 % (3322728)Termination reason: Instruction limit % 164.52/23.77 % (3322728)Termination phase: Saturation % 164.52/23.77 % (3322728)Time elapsed: 1.316 s % 164.52/23.77 % (3322728)Peak memory usage: 140 MB % 164.52/23.77 % (3322728)Instructions burned: 4274 (million) % 164.52/23.77 % (3322739)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=986373234:i=2693:kws=precedence:ins=1:av=off_2859 on theBenchmark for (2859ds/2693Mi) % 164.52/23.77 % (3322734)Instruction limit reached! % 164.52/23.77 % (3322734)------------------------------ % 164.52/23.77 % (3322734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.52/23.77 % (3322734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.52/23.77 % (3322734)CaDiCaL version: 2.1.3 % 164.52/23.77 % (3322734)Termination reason: Instruction limit % 164.52/23.77 % (3322734)Termination phase: Saturation % 164.52/23.77 % (3322734)Time elapsed: 0.742 s % 164.52/23.77 % (3322734)Peak memory usage: 138 MB % 164.52/23.77 % (3322734)Instructions burned: 2332 (million) % 164.52/23.77 % (3322741)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=4058941001:i=28651:sd=4:ss=included:sgt=64_2855 on theBenchmark for (2855ds/28651Mi) % 164.52/23.77 % (3322739)Instruction limit reached! % 164.52/23.77 % (3322739)------------------------------ % 164.52/23.77 % (3322739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.52/23.77 % (3322739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.52/23.77 % (3322739)CaDiCaL version: 2.1.3 % 164.52/23.77 % (3322739)Termination reason: Instruction limit % 164.52/23.77 % (3322739)Termination phase: Saturation % 164.52/23.77 % (3322739)Time elapsed: 0.901 s % 164.52/23.77 % (3322739)Peak memory usage: 150 MB % 164.52/23.77 % (3322739)Instructions burned: 2695 (million) % 164.52/23.77 % (3322743)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2097401443:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2848 on theBenchmark for (2848ds/2700Mi) % 164.52/23.77 % (3322733)Instruction limit reached! % 164.52/23.77 % (3322733)------------------------------ % 164.52/23.77 % (3322733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.52/23.77 % (3322733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.52/23.77 % (3322733)CaDiCaL version: 2.1.3 % 164.52/23.77 % (3322733)Termination reason: Instruction limit % 164.52/23.77 % (3322733)Termination phase: Saturation % 164.52/23.77 % (3322733)Time elapsed: 1.826 s % 164.52/23.77 % (3322733)Peak memory usage: 139 MB % 164.52/23.77 % (3322733)Instructions burned: 6513 (million) % 164.52/23.77 % (3322745)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=114646655:i=3196:nm=4_2845 on theBenchmark for (2845ds/3196Mi) % 164.52/23.77 % (3322735)Instruction limit reached! % 164.52/23.77 % (3322735)------------------------------ % 164.52/23.77 % (3322735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.52/23.77 % (3322735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.52/23.77 % (3322735)CaDiCaL version: 2.1.3 % 164.52/23.77 % (3322735)Termination reason: Instruction limit % 164.52/23.77 % (3322735)Termination phase: Saturation % 164.52/23.77 % (3322735)Time elapsed: 2.189 s % 164.52/23.77 % (3322735)Peak memory usage: 155 MB % 164.52/23.77 % (3322735)Instructions burned: 7594 (million) % 164.52/23.77 % (3322747)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=2141709053:cts=off:i=3254:av=off_2840 on theBenchmark for (2840ds/3254Mi) % 164.52/23.77 % (3322743)Instruction limit reached! % 164.52/23.77 % (3322743)------------------------------ % 164.52/23.77 % (3322743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.44/26.77 % (3322743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.44/26.77 % (3322743)CaDiCaL version: 2.1.3 % 185.44/26.77 % (3322743)Termination reason: Instruction limit % 185.44/26.77 % (3322743)Termination phase: Saturation % 185.44/26.77 % (3322743)Time elapsed: 0.944 s % 185.44/26.77 % (3322743)Peak memory usage: 143 MB % 185.44/26.77 % (3322743)Instructions burned: 2700 (million) % 185.44/26.77 % (3322749)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=2519331434:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2838 on theBenchmark for (2838ds/3264Mi) % 185.44/26.77 % (3322745)Instruction limit reached! % 185.44/26.77 % (3322745)------------------------------ % 185.44/26.77 % (3322745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.44/26.77 % (3322745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.44/26.77 % (3322745)CaDiCaL version: 2.1.3 % 185.44/26.77 % (3322745)Termination reason: Instruction limit % 185.44/26.77 % (3322745)Termination phase: Saturation % 185.44/26.77 % (3322745)Time elapsed: 1.184 s % 185.44/26.77 % (3322745)Peak memory usage: 149 MB % 185.44/26.77 % (3322745)Instructions burned: 3198 (million) % 185.44/26.77 % (3322751)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=281862594:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2832 on theBenchmark for (2832ds/9708Mi) % 185.44/26.77 [W928 11:27:51.315150328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 185.44/26.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 185.44/26.77 [W928 11:27:51.315172252 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 185.44/26.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 185.44/26.77 [W928 11:27:51.315191912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 185.44/26.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 185.44/26.77 [W928 11:27:51.315198775 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 185.44/26.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 185.44/26.77 [W928 11:27:51.315213685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 185.44/26.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 185.44/26.77 [W928 11:27:51.315220310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 185.44/26.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 185.44/26.77 % (3322747)Instruction limit reached! % 185.44/26.77 % (3322747)------------------------------ % 185.44/26.77 % (3322747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.44/26.77 % (3322747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.44/26.77 % (3322747)CaDiCaL version: 2.1.3 % 185.44/26.77 % (3322747)Termination reason: Instruction limit % 185.44/26.77 % (3322747)Termination phase: Saturation % 185.44/26.77 % (3322747)Time elapsed: 1.181 s % 185.44/26.77 % (3322747)Peak memory usage: 147 MB % 185.44/26.77 % (3322747)Instructions burned: 3257 (million) % 185.44/26.77 % (3322751)Refutation not found, incomplete strategy % 185.44/26.77 % (3322751)------------------------------ % 185.44/26.77 % (3322751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.44/26.77 % (3322751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.44/26.77 % (3322751)CaDiCaL version: 2.1.3 % 238.54/34.23 % (3322751)Termination reason: Refutation not found, incomplete strategy % 238.54/34.23 % (3322751)Time elapsed: 0.349 s % 238.54/34.23 % (3322751)Peak memory usage: 133 MB % 238.54/34.23 % (3322751)Instructions burned: 971 (million) % 238.54/34.23 % (3322753)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1744676533:i=21997:s2at=5:gtg=all_2827 on theBenchmark for (2827ds/21997Mi) % 238.54/34.23 % (3322751)------------------------------ % 238.54/34.23 % (3322751)------------------------------ % 238.54/34.23 % (3322749)Instruction limit reached! % 238.54/34.23 % (3322749)------------------------------ % 238.54/34.23 % (3322749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.54/34.23 % (3322749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.54/34.23 % (3322749)CaDiCaL version: 2.1.3 % 238.54/34.23 % (3322749)Termination reason: Instruction limit % 238.54/34.23 % (3322749)Termination phase: Saturation % 238.54/34.23 % (3322749)Time elapsed: 1.117 s % 238.54/34.23 % (3322749)Peak memory usage: 148 MB % 238.54/34.23 % (3322749)Instructions burned: 3265 (million) % 238.54/34.23 % (3322756)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=829040532:i=8924:sd=1:ss=included_2825 on theBenchmark for (2825ds/8924Mi) % 238.54/34.23 % (3322755)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2141427156:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2825 on theBenchmark for (2825ds/7551Mi) % 238.54/34.23 % (3322755)Instruction limit reached! % 238.54/34.23 % (3322755)------------------------------ % 238.54/34.23 % (3322755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.54/34.23 % (3322755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.54/34.23 % (3322755)CaDiCaL version: 2.1.3 % 238.54/34.23 % (3322755)Termination reason: Instruction limit % 238.54/34.23 % (3322755)Termination phase: Saturation % 238.54/34.23 % (3322755)Time elapsed: 2.256 s % 238.54/34.23 % (3322755)Peak memory usage: 145 MB % 238.54/34.23 % (3322755)Instructions burned: 7552 (million) % 238.54/34.23 % (3322759)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=3991786809:i=9638:kws=frequency:bd=preordered_2801 on theBenchmark for (2801ds/9638Mi) % 238.54/34.23 % (3322756)Instruction limit reached! % 238.54/34.23 % (3322756)------------------------------ % 238.54/34.23 % (3322756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.54/34.23 % (3322756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.54/34.23 % (3322756)CaDiCaL version: 2.1.3 % 238.54/34.23 % (3322756)Termination reason: Instruction limit % 238.54/34.23 % (3322756)Termination phase: Saturation % 238.54/34.23 % (3322756)Time elapsed: 3.348 s % 238.54/34.23 % (3322756)Peak memory usage: 201 MB % 238.54/34.23 % (3322756)Instructions burned: 8925 (million) % 238.54/34.23 % (3322761)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=1347599508:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2790 on theBenchmark for (2790ds/5177Mi) % 238.54/34.23 % (3322761)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 238.54/34.23 % (3322761)------------------------------ % 238.54/34.23 % (3322761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.54/34.23 % (3322761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.54/34.23 % (3322761)CaDiCaL version: 2.1.3 % 238.54/34.23 % (3322761)Termination reason: Unknown % 238.54/34.23 % (3322761)Termination phase: Saturation % 238.54/34.23 % (3322761)Time elapsed: 0.364 s % 238.54/34.23 % (3322761)Peak memory usage: 133 MB % 238.54/34.23 % (3322761)Instructions burned: 1025 (million) % 238.54/34.23 % (3322763)lrs-1011_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:sas=cadical:sp=unary_first:acc=on:alpa=false:random_seed=999823008:i=6464:aac=none:ins=10_2785 on theBenchmark for (2785ds/6464Mi) % 238.54/34.23 % (3322759)Instruction limit reached! % 238.54/34.23 % (3322759)------------------------------ % 238.54/34.23 % (3322759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.54/34.23 % (3322759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.54/34.23 % (3322759)CaDiCaL version: 2.1.3 % 238.54/34.23 % (3322759)Termination reason: Instruction limit % 238.54/34.23 % (3322759)Termination phase: Saturation % 238.54/34.23 % (3322759)Time elapsed: 3.452 s % 280.81/40.23 % (3322759)Peak memory usage: 209 MB % 280.81/40.23 % (3322759)Instructions burned: 9641 (million) % 280.81/40.23 % (3322765)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:erd=off:urr=on:bsr=on:fd=preordered:random_seed=892713147:i=19192:av=off_2765 on theBenchmark for (2765ds/19192Mi) % 280.81/40.23 % (3322741)Instruction limit reached! % 280.81/40.23 % (3322741)------------------------------ % 280.81/40.23 % (3322741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.81/40.23 % (3322741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.81/40.23 % (3322741)CaDiCaL version: 2.1.3 % 280.81/40.23 % (3322741)Termination reason: Instruction limit % 280.81/40.23 % (3322741)Termination phase: Saturation % 280.81/40.23 % (3322741)Time elapsed: 9.057 s % 280.81/40.23 % (3322741)Peak memory usage: 337 MB % 280.81/40.23 % (3322741)Instructions burned: 28653 (million) % 280.81/40.23 % (3322767)lrs+10_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=8000:npcc=on:prc=on:fde=unused:sp=const_min:random_seed=586127996:i=7136:fgj=on:bd=preordered:ins=3:ss=included_2763 on theBenchmark for (2763ds/7136Mi) % 280.81/40.23 % (3322763)Instruction limit reached! % 280.81/40.23 % (3322763)------------------------------ % 280.81/40.23 % (3322763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.81/40.23 % (3322763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.81/40.23 % (3322763)CaDiCaL version: 2.1.3 % 280.81/40.23 % (3322763)Termination reason: Instruction limit % 280.81/40.23 % (3322763)Termination phase: Saturation % 280.81/40.23 % (3322763)Time elapsed: 2.368 s % 280.81/40.23 % (3322763)Peak memory usage: 178 MB % 280.81/40.23 % (3322763)Instructions burned: 6464 (million) % 280.81/40.23 % (3322769)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop6.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=3078262870:cts=off:cond=on:i=7540:bs=on:fsd=on_2760 on theBenchmark for (2760ds/7540Mi) % 280.81/40.23 % (3322753)Instruction limit reached! % 280.81/40.23 % (3322753)------------------------------ % 280.81/40.23 % (3322753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.81/40.23 % (3322753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.81/40.23 % (3322753)CaDiCaL version: 2.1.3 % 280.81/40.23 % (3322753)Termination reason: Instruction limit % 280.81/40.23 % (3322753)Termination phase: Saturation % 280.81/40.23 % (3322753)Time elapsed: 7.327 s % 280.81/40.23 % (3322753)Peak memory usage: 314 MB % 280.81/40.23 % (3322753)Instructions burned: 22000 (million) % 280.81/40.23 % (3322771)ott+1011_1_to=lpo:ncem=casc2026/models/loop5.pt:sil=64000:tgt=ground:npcc=on:drc=off:sp=const_frequency:random_seed=2382394562:i=15570:s2at=5:gtgl=4:gtg=exists_sym_2752 on theBenchmark for (2752ds/15570Mi) % 280.81/40.23 % (3322767)Instruction limit reached! % 280.81/40.23 % (3322767)------------------------------ % 280.81/40.23 % (3322767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.81/40.23 % (3322767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.81/40.23 % (3322767)CaDiCaL version: 2.1.3 % 280.81/40.23 % (3322767)Termination reason: Instruction limit % 280.81/40.23 % (3322767)Termination phase: Saturation % 280.81/40.23 % (3322767)Time elapsed: 2.384 s % 280.81/40.23 % (3322767)Peak memory usage: 194 MB % 280.81/40.23 % (3322767)Instructions burned: 7137 (million) % 280.81/40.23 % (3322769)Instruction limit reached! % 280.81/40.23 % (3322769)------------------------------ % 280.81/40.23 % (3322769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.81/40.23 % (3322769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.81/40.23 % (3322769)CaDiCaL version: 2.1.3 % 280.81/40.23 % (3322769)Termination reason: Instruction limit % 280.81/40.23 % (3322769)Termination phase: Saturation % 280.81/40.23 % (3322769)Time elapsed: 2.194 s % 280.81/40.23 % (3322769)Peak memory usage: 149 MB % 280.81/40.23 % (3322769)Instructions burned: 7545 (million) % 280.81/40.23 % (3322773)lrs+1011_1_anc=none:to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lsd=20:bce=on:bsr=on:fd=preordered:gs=on:random_seed=4187634086:i=15957:add=on:fgj=on_2738 on theBenchmark for (2738ds/15957Mi) % 280.81/40.23 % (3322774)lrs+1010_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=32000:tgt=full:npcc=on:prc=on:drc=ordering:fde=none:sp=arity:spb=intro:urr=ec_only:s2agt=40:random_seed=718122296:cond=on:i=8289:erml=3:bd=preordered:er=filter:proc=on_2736 on theBenchmark for (2736ds/8289Mi) % 291.01/41.78 % (3322774)Instruction limit reached! % 291.01/41.78 % (3322774)------------------------------ % 291.01/41.78 % (3322774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.01/41.78 % (3322774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.01/41.78 % (3322774)CaDiCaL version: 2.1.3 % 291.01/41.78 % (3322774)Termination reason: Instruction limit % 291.01/41.78 % (3322774)Termination phase: Saturation % 291.01/41.78 % (3322774)Time elapsed: 2.754 s % 291.01/41.78 % (3322774)Peak memory usage: 207 MB % 291.01/41.78 % (3322774)Instructions burned: 8291 (million) % 291.01/41.78 % (3322777)lrs+4_4_to=lpo:sil=128000:flr=on:sac=on:lwlo=on:random_seed=8015504:i=16865:nicw=on:bs=unit_only_2707 on theBenchmark for (2707ds/16865Mi) % 291.01/41.78 % (3322771)Instruction limit reached! % 291.01/41.78 % (3322771)------------------------------ % 291.01/41.78 % (3322771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.01/41.78 % (3322771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.01/41.78 % (3322771)CaDiCaL version: 2.1.3 % 291.01/41.78 % (3322771)Termination reason: Instruction limit % 291.01/41.78 % (3322771)Termination phase: Saturation % 291.01/41.78 % (3322771)Time elapsed: 4.889 s % 291.01/41.78 % (3322771)Peak memory usage: 259 MB % 291.01/41.78 % (3322771)Instructions burned: 15573 (million) % 291.01/41.78 % (3322779)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2675981617:i=67727:sd=2:fgj=on:ss=axioms:sgt=64_2702 on theBenchmark for (2702ds/67727Mi) % 291.01/41.78 % (3322765)Instruction limit reached! % 291.01/41.78 % (3322765)------------------------------ % 291.01/41.78 % (3322765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.01/41.78 % (3322765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.01/41.78 % (3322765)CaDiCaL version: 2.1.3 % 291.01/41.78 % (3322765)Termination reason: Instruction limit % 291.01/41.78 % (3322765)Termination phase: Saturation % 291.01/41.78 % (3322765)Time elapsed: 6.310 s % 291.01/41.78 % (3322765)Peak memory usage: 295 MB % 291.01/41.78 % (3322765)Instructions burned: 19195 (million) % 291.01/41.78 % (3322781)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=4093885380:cond=on:i=17955:s2at=3:aac=none:fsd=on_2700 on theBenchmark for (2700ds/17955Mi) % 291.01/41.78 % (3322773)Instruction limit reached! % 291.01/41.78 % (3322773)------------------------------ % 291.01/41.78 % (3322773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.01/41.78 % (3322773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.01/41.78 % (3322773)CaDiCaL version: 2.1.3 % 291.01/41.78 % (3322773)Termination reason: Instruction limit % 291.01/41.78 % (3322773)Termination phase: Saturation % 291.01/41.78 % (3322773)Time elapsed: 5.557 s % 291.01/41.78 % (3322773)Peak memory usage: 250 MB % 291.01/41.78 % (3322773)Instructions burned: 15959 (million) % 291.01/41.78 % (3322783)dis-1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:irw=on:npcc=on:sac=on:random_seed=4017719000:i=10108:bd=preordered_2681 on theBenchmark for (2681ds/10108Mi) % 291.01/41.78 % (3322598)Instruction limit reached! % 291.01/41.78 % (3322598)------------------------------ % 291.01/41.78 % (3322598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.01/41.78 % (3322598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.01/41.78 % (3322598)CaDiCaL version: 2.1.3 % 291.01/41.78 % (3322598)Termination reason: Instruction limit % 291.01/41.78 % (3322598)Termination phase: Saturation % 291.01/41.78 % (3322598)Time elapsed: 32.903 s % 291.01/41.78 % (3322598)Peak memory usage: 538 MB % 291.01/41.78 % (3322598)Instructions burned: 140169 (million) % 291.01/41.78 % (3322785)lrs+2_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:spb=goal:lcm=predicate:random_seed=3541642466:i=10307:kws=inv_arity_2669 on theBenchmark for (2669ds/10307Mi) % 291.01/41.78 % (3322781)Instruction limit reached! % 291.01/41.78 % (3322781)------------------------------ % 291.01/41.78 % (3322781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.01/41.78 % (3322781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.01/41.78 % (3322781)CaDiCaL version: 2.1.3 % 291.01/41.78 % (3322781)Termination reason: Instruction limit % 291.01/41.78 % (3322781)Termination phase: Saturation % 291.01/41.78 % (3322781)Time elapsed: 3.856 s % 291.01/41.78 % (3322781)Peak memory usage: 142 MB % 291.01/41.78 % (3322781)Instructions burned: 1Terminated % 300.71/43.06 % Vampire exiting % 300.71/43.06 Terminated %------------------------------------------------------------------------------