%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : PLA034-1 : TPTP v9.3.1. Bugfixed v5.5.1. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:27:48 PM UTC 2026 % Result : Timeout 300.03s 43.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : PLA034-1 : TPTP v9.3.1. Bugfixed v5.5.1. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.39 % Computer : n016.cluster.edu % 0.12/0.39 % Model : x86_64 x86_64 % 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.39 % Memory : 8046.5625MB % 0.12/0.39 % OS : Linux 6.8.0-71-generic % 0.12/0.40 % CPULimit : 300 % 0.12/0.40 % WCLimit : 300 % 0.12/0.40 % DateTime : Sun Sep 27 22:18:08 UTC 2026 % 0.12/0.40 % CPUTime : % 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.44 Running first-order theorem proving % 0.12/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.10/3.03 % (3048253)Input is clausal, will run a generic CNF schedule. % 12.10/3.03 % (3048264)dis-21_1_sil=8000:lcm=predicate:random_seed=3141784565:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/117Mi) % 12.10/3.03 % (3048264)Instruction limit reached! % 12.10/3.03 % (3048264)------------------------------ % 12.10/3.03 % (3048264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/3.03 % (3048264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/3.03 % (3048264)CaDiCaL version: 2.1.3 % 12.10/3.03 % (3048264)Termination reason: Instruction limit % 12.10/3.03 % (3048264)Termination phase: Property scanning % 12.10/3.03 % (3048264)Time elapsed: 0.029 s % 12.10/3.03 % (3048264)Peak memory usage: 93 MB % 12.10/3.03 % (3048264)Instructions burned: 123 (million) % 12.10/3.03 % (3048263)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1899966746:s2a=on:i=180:gtg=position_2997 on theBenchmark for (2997ds/180Mi) % 12.10/3.03 % (3048261)lrs+10_1_sil=8000:sp=occurrence:random_seed=2157927266:i=107:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/107Mi) % 12.10/3.03 % (3048260)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=121767032:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2997 on theBenchmark for (2997ds/137899Mi) % 12.10/3.03 % (3048259)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3070242143:i=132376:av=off_2997 on theBenchmark for (2997ds/132376Mi) % 12.10/3.03 % (3048262)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4209749263:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2997 on theBenchmark for (2997ds/114Mi) % 12.10/3.03 % (3048258)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=3313759307:i=140167_2997 on theBenchmark for (2997ds/140167Mi) % 12.10/3.03 % (3048261)Refutation not found, incomplete strategy % 12.10/3.03 % (3048261)------------------------------ % 12.10/3.03 % (3048261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/3.03 % (3048261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/3.03 % (3048261)CaDiCaL version: 2.1.3 % 12.10/3.03 % (3048261)Termination reason: Refutation not found, incomplete strategy % 12.10/3.03 % (3048261)Time elapsed: 0.014 s % 12.10/3.03 % (3048261)Peak memory usage: 93 MB % 12.10/3.03 % (3048261)Instructions burned: 22 (million) % 12.10/3.03 % (3048262)Refutation not found, incomplete strategy % 12.10/3.03 % (3048262)------------------------------ % 12.10/3.03 % (3048262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/3.03 % (3048262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/3.03 % (3048262)CaDiCaL version: 2.1.3 % 12.10/3.03 % (3048262)Termination reason: Refutation not found, incomplete strategy % 12.10/3.03 % (3048262)Time elapsed: 0.019 s % 12.10/3.03 % (3048262)Peak memory usage: 93 MB % 12.10/3.03 % (3048262)Instructions burned: 33 (million) % 12.10/3.03 % (3048263)Instruction limit reached! % 12.10/3.03 % (3048263)------------------------------ % 12.10/3.03 % (3048263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/3.03 % (3048263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/3.03 % (3048263)CaDiCaL version: 2.1.3 % 12.10/3.03 % (3048263)Termination reason: Instruction limit % 12.10/3.03 % (3048263)Termination phase: Property scanning % 12.10/3.03 % (3048263)Time elapsed: 0.072 s % 12.10/3.03 % (3048263)Peak memory usage: 92 MB % 12.10/3.03 % (3048263)Instructions burned: 181 (million) % 12.10/3.03 % (3048266)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=2924105125:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi) % 12.10/3.03 % (3048266)Refutation not found, incomplete strategy % 12.10/3.03 % (3048266)------------------------------ % 12.10/3.03 % (3048266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/3.03 % (3048266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/3.03 % (3048266)CaDiCaL version: 2.1.3 % 12.10/3.03 % (3048266)Termination reason: Refutation not found, incomplete strategy % 12.10/3.03 % (3048266)Time elapsed: 0.008 s % 12.10/3.03 % (3048266)Peak memory usage: 93 MB % 12.10/3.03 % (3048266)Instructions burned: 23 (million) % 22.76/4.33 % (3048273)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1284928805:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2994 on theBenchmark for (2994ds/189Mi) % 22.76/4.33 % (3048261)------------------------------ % 22.76/4.33 % (3048261)------------------------------ % 22.76/4.33 % (3048262)------------------------------ % 22.76/4.33 % (3048262)------------------------------ % 22.76/4.33 % (3048266)------------------------------ % 22.76/4.33 % (3048266)------------------------------ % 22.76/4.33 % (3048273)Refutation not found, incomplete strategy % 22.76/4.33 % (3048273)------------------------------ % 22.76/4.33 % (3048273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/4.33 % (3048273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/4.33 % (3048273)CaDiCaL version: 2.1.3 % 22.76/4.33 % (3048273)Termination reason: Refutation not found, incomplete strategy % 22.76/4.33 % (3048273)Time elapsed: 0.034 s % 22.76/4.33 % (3048273)Peak memory usage: 93 MB % 22.76/4.33 % (3048273)Instructions burned: 64 (million) % 22.76/4.33 % (3048278)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3014337277:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi) % 22.76/4.33 % (3048277)lrs+10_64_to=lpo:sil=8000:random_seed=3480999203:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi) % 22.76/4.33 % (3048276)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=17708604:st=4:i=219:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/219Mi) % 22.76/4.33 % (3048278)Instruction limit reached! % 22.76/4.33 % (3048278)------------------------------ % 22.76/4.33 % (3048278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/4.33 % (3048278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/4.33 % (3048278)CaDiCaL version: 2.1.3 % 22.76/4.33 % (3048278)Termination reason: Instruction limit % 22.76/4.33 % (3048278)Termination phase: Saturation % 22.76/4.33 % (3048278)Time elapsed: 0.062 s % 22.76/4.33 % (3048278)Peak memory usage: 97 MB % 22.76/4.33 % (3048278)Instructions burned: 196 (million) % 22.76/4.33 % (3048276)Refutation not found, incomplete strategy % 22.76/4.33 % (3048276)------------------------------ % 22.76/4.33 % (3048276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/4.33 % (3048276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/4.33 % (3048276)CaDiCaL version: 2.1.3 % 22.76/4.33 % (3048276)Termination reason: Refutation not found, incomplete strategy % 22.76/4.33 % (3048276)Time elapsed: 0.019 s % 22.76/4.33 % (3048276)Peak memory usage: 93 MB % 22.76/4.33 % (3048276)Instructions burned: 33 (million) % 22.76/4.33 % (3048277)Instruction limit reached! % 22.76/4.33 % (3048277)------------------------------ % 22.76/4.33 % (3048277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/4.33 % (3048277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/4.33 % (3048277)CaDiCaL version: 2.1.3 % 22.76/4.33 % (3048277)Termination reason: Instruction limit % 22.76/4.33 % (3048277)Termination phase: Saturation % 22.76/4.33 % (3048277)Time elapsed: 0.079 s % 22.76/4.33 % (3048277)Peak memory usage: 95 MB % 22.76/4.33 % (3048277)Instructions burned: 127 (million) % 22.76/4.33 % (3048273)------------------------------ % 22.76/4.33 % (3048273)------------------------------ % 22.76/4.33 % (3048282)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3498083950:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi) % 22.76/4.33 % (3048282)Instruction limit reached! % 22.76/4.33 % (3048282)------------------------------ % 22.76/4.33 % (3048282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.76/4.33 % (3048282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/4.33 % (3048282)CaDiCaL version: 2.1.3 % 22.76/4.33 % (3048282)Termination reason: Instruction limit % 22.76/4.33 % (3048282)Termination phase: Saturation % 22.76/4.33 % (3048282)Time elapsed: 0.038 s % 22.76/4.33 % (3048282)Peak memory usage: 95 MB % 22.76/4.33 % (3048282)Instructions burned: 160 (million) % 22.76/4.33 % (3048283)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=867406582:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi) % 22.76/4.33 % (3048284)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=2648045348:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi) % 29.62/5.66 % (3048276)------------------------------ % 29.62/5.66 % (3048276)------------------------------ % 29.62/5.66 % (3048284)Refutation not found, incomplete strategy % 29.62/5.66 % (3048284)------------------------------ % 29.62/5.66 % (3048284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.62/5.66 % (3048284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.62/5.66 % (3048284)CaDiCaL version: 2.1.3 % 29.62/5.66 % (3048284)Termination reason: Refutation not found, incomplete strategy % 29.62/5.66 % (3048284)Time elapsed: 0.027 s % 29.62/5.66 % (3048284)Peak memory usage: 93 MB % 29.62/5.66 % (3048284)Instructions burned: 43 (million) % 29.62/5.66 % (3048286)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=220669936:i=107_2989 on theBenchmark for (2989ds/107Mi) % 29.62/5.66 % (3048286)Instruction limit reached! % 29.62/5.66 % (3048286)------------------------------ % 29.62/5.66 % (3048286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.62/5.66 % (3048286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.62/5.66 % (3048286)CaDiCaL version: 2.1.3 % 29.62/5.66 % (3048286)Termination reason: Instruction limit % 29.62/5.66 % (3048286)Termination phase: Saturation % 29.62/5.66 % (3048286)Time elapsed: 0.062 s % 29.62/5.66 % (3048286)Peak memory usage: 95 MB % 29.62/5.66 % (3048286)Instructions burned: 108 (million) % 29.62/5.66 % (3048289)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1872152842:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi) % 29.62/5.66 % (3048284)------------------------------ % 29.62/5.66 % (3048284)------------------------------ % 29.62/5.66 % (3048289)Instruction limit reached! % 29.62/5.66 % (3048289)------------------------------ % 29.62/5.66 % (3048289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.62/5.66 % (3048289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.62/5.66 % (3048289)CaDiCaL version: 2.1.3 % 29.62/5.66 % (3048289)Termination reason: Instruction limit % 29.62/5.66 % (3048289)Termination phase: Property scanning % 29.62/5.66 % (3048289)Time elapsed: 0.100 s % 29.62/5.66 % (3048289)Peak memory usage: 92 MB % 29.62/5.66 % (3048289)Instructions burned: 244 (million) % 29.62/5.66 % (3048291)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1868932476:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi) % 29.62/5.66 % (3048293)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1614136045:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi) % 29.62/5.66 % (3048293)Refutation not found, incomplete strategy % 29.62/5.66 % (3048293)------------------------------ % 29.62/5.66 % (3048293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.62/5.66 % (3048293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.62/5.66 % (3048293)CaDiCaL version: 2.1.3 % 29.62/5.66 % (3048293)Termination reason: Refutation not found, incomplete strategy % 29.62/5.66 % (3048293)Time elapsed: 0.015 s % 29.62/5.66 % (3048293)Peak memory usage: 93 MB % 29.62/5.66 % (3048293)Instructions burned: 23 (million) % 29.62/5.66 % (3048294)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3348121421:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi) % 29.62/5.66 % (3048293)------------------------------ % 29.62/5.66 % (3048293)------------------------------ % 29.62/5.66 % (3048294)Instruction limit reached! % 29.62/5.66 % (3048294)------------------------------ % 29.62/5.66 % (3048294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.62/5.66 % (3048294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.62/5.66 % (3048294)CaDiCaL version: 2.1.3 % 29.62/5.66 % (3048294)Termination reason: Instruction limit % 29.62/5.66 % (3048294)Termination phase: Saturation % 29.62/5.66 % (3048294)Time elapsed: 0.291 s % 29.62/5.66 % (3048294)Peak memory usage: 102 MB % 29.62/5.66 % (3048294)Instructions burned: 501 (million) % 29.62/5.66 % (3048298)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3021314512:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi) % 29.62/5.66 % (3048299)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4161022934:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi) % 29.62/5.66 % (3048298)Instruction limit reached! % 36.47/6.21 % (3048298)------------------------------ % 36.47/6.21 % (3048298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.47/6.21 % (3048298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.47/6.21 % (3048298)CaDiCaL version: 2.1.3 % 36.47/6.21 % (3048298)Termination reason: Instruction limit % 36.47/6.21 % (3048298)Termination phase: Saturation % 36.47/6.21 % (3048298)Time elapsed: 0.123 s % 36.47/6.21 % (3048298)Peak memory usage: 97 MB % 36.47/6.21 % (3048298)Instructions burned: 192 (million) % 36.47/6.21 % (3048299)Instruction limit reached! % 36.47/6.21 % (3048299)------------------------------ % 36.47/6.21 % (3048299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.47/6.21 % (3048299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.47/6.21 % (3048299)CaDiCaL version: 2.1.3 % 36.47/6.21 % (3048299)Termination reason: Instruction limit % 36.47/6.21 % (3048299)Termination phase: Saturation % 36.47/6.21 % (3048299)Time elapsed: 0.157 s % 36.47/6.21 % (3048299)Peak memory usage: 100 MB % 36.47/6.21 % (3048299)Instructions burned: 265 (million) % 36.47/6.21 % (3048302)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3645428611:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi) % 36.47/6.21 % (3048302)Instruction limit reached! % 36.47/6.21 % (3048302)------------------------------ % 36.47/6.21 % (3048302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.47/6.21 % (3048302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.47/6.21 % (3048302)CaDiCaL version: 2.1.3 % 36.47/6.21 % (3048302)Termination reason: Instruction limit % 36.47/6.21 % (3048302)Termination phase: Saturation % 36.47/6.21 % (3048302)Time elapsed: 0.068 s % 36.47/6.21 % (3048302)Peak memory usage: 94 MB % 36.47/6.21 % (3048302)Instructions burned: 157 (million) % 36.47/6.21 % (3048303)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=3694908593:i=3256:kws=precedence:bd=preordered:av=off_2977 on theBenchmark for (2977ds/3256Mi) % 36.47/6.21 % (3048305)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1211820826:i=537:av=off:ss=included_2975 on theBenchmark for (2975ds/537Mi) % 36.47/6.21 % (3048305)Instruction limit reached! % 36.47/6.21 % (3048305)------------------------------ % 36.47/6.21 % (3048305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.47/6.21 % (3048305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.47/6.21 % (3048305)CaDiCaL version: 2.1.3 % 36.47/6.21 % (3048305)Termination reason: Instruction limit % 36.47/6.21 % (3048305)Termination phase: Saturation % 36.47/6.21 % (3048305)Time elapsed: 0.288 s % 36.47/6.21 % (3048305)Peak memory usage: 98 MB % 36.47/6.21 % (3048305)Instructions burned: 537 (million) % 36.47/6.21 % (3048308)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2732994394:i=180:bd=preordered:av=off_2971 on theBenchmark for (2971ds/180Mi) % 36.47/6.21 % (3048308)Instruction limit reached! % 36.47/6.21 % (3048308)------------------------------ % 36.47/6.21 % (3048308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.47/6.21 % (3048308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.47/6.21 % (3048308)CaDiCaL version: 2.1.3 % 36.47/6.21 % (3048308)Termination reason: Instruction limit % 36.47/6.21 % (3048308)Termination phase: Saturation % 36.47/6.21 % (3048308)Time elapsed: 0.105 s % 36.47/6.21 % (3048308)Peak memory usage: 96 MB % 36.47/6.21 % (3048308)Instructions burned: 181 (million) % 36.47/6.21 % (3048259)Refutation not found, incomplete strategy % 36.47/6.21 % (3048259)------------------------------ % 36.47/6.21 % (3048259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.47/6.21 % (3048259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.47/6.21 % (3048259)CaDiCaL version: 2.1.3 % 36.47/6.21 % (3048259)Termination reason: Refutation not found, incomplete strategy % 36.47/6.21 % (3048259)Time elapsed: 2.764 s % 36.47/6.21 % (3048259)Peak memory usage: 333 MB % 36.47/6.21 % (3048259)Instructions burned: 3943 (million) % 36.47/6.21 % (3048310)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=2666689455:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2968 on theBenchmark for (2968ds/10307Mi) % 36.47/6.21 % (3048259)------------------------------ % 45.83/7.66 % (3048259)------------------------------ % 45.83/7.66 % (3048283)Instruction limit reached! % 45.83/7.66 % (3048283)------------------------------ % 45.83/7.66 % (3048283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.83/7.66 % (3048283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.83/7.66 % (3048283)CaDiCaL version: 2.1.3 % 45.83/7.66 % (3048283)Termination reason: Instruction limit % 45.83/7.66 % (3048283)Termination phase: Saturation % 45.83/7.66 % (3048283)Time elapsed: 2.362 s % 45.83/7.66 % (3048283)Peak memory usage: 330 MB % 45.83/7.66 % (3048283)Instructions burned: 3396 (million) % 45.83/7.66 % (3048312)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=3541931427:i=412:gtgl=4:gtg=exists_all_2965 on theBenchmark for (2965ds/412Mi) % 45.83/7.66 % (3048313)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=1492004233:s2pl=no:i=8478:s2at=4:nm=6_2965 on theBenchmark for (2965ds/8478Mi) % 45.83/7.66 % (3048312)Instruction limit reached! % 45.83/7.66 % (3048312)------------------------------ % 45.83/7.66 % (3048312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.83/7.66 % (3048312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.83/7.66 % (3048312)CaDiCaL version: 2.1.3 % 45.83/7.66 % (3048312)Termination reason: Instruction limit % 45.83/7.66 % (3048312)Termination phase: Blocked clause elimination % 45.83/7.66 % (3048312)Time elapsed: 0.171 s % 45.83/7.66 % (3048312)Peak memory usage: 93 MB % 45.83/7.66 % (3048312)Instructions burned: 414 (million) % 45.83/7.66 % (3048316)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=591948558:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2961 on theBenchmark for (2961ds/303Mi) % 45.83/7.66 % (3048316)Instruction limit reached! % 45.83/7.66 % (3048316)------------------------------ % 45.83/7.66 % (3048316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.83/7.66 % (3048316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.83/7.66 % (3048316)CaDiCaL version: 2.1.3 % 45.83/7.66 % (3048316)Termination reason: Instruction limit % 45.83/7.66 % (3048316)Termination phase: Saturation % 45.83/7.66 % (3048316)Time elapsed: 0.153 s % 45.83/7.66 % (3048316)Peak memory usage: 98 MB % 45.83/7.66 % (3048316)Instructions burned: 304 (million) % 45.83/7.66 % (3048318)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1506550580:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi) % 45.83/7.66 % (3048318)Refutation not found, incomplete strategy % 45.83/7.66 % (3048318)------------------------------ % 45.83/7.66 % (3048318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.83/7.66 % (3048318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.83/7.66 % (3048318)CaDiCaL version: 2.1.3 % 45.83/7.66 % (3048318)Termination reason: Refutation not found, incomplete strategy % 45.83/7.66 % (3048318)Time elapsed: 0.020 s % 45.83/7.66 % (3048318)Peak memory usage: 93 MB % 45.83/7.66 % (3048318)Instructions burned: 33 (million) % 45.83/7.66 % (3048318)------------------------------ % 45.83/7.66 % (3048318)------------------------------ % 45.83/7.66 % (3048303)Instruction limit reached! % 45.83/7.66 % (3048303)------------------------------ % 45.83/7.66 % (3048303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.83/7.66 % (3048303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.83/7.66 % (3048303)CaDiCaL version: 2.1.3 % 45.83/7.66 % (3048303)Termination reason: Instruction limit % 45.83/7.66 % (3048303)Termination phase: Saturation % 45.83/7.66 % (3048303)Time elapsed: 2.288 s % 45.83/7.66 % (3048303)Peak memory usage: 353 MB % 45.83/7.66 % (3048303)Instructions burned: 3257 (million) % 45.83/7.66 % (3048320)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1142007058:i=598:bs=on:bd=preordered:av=off:ss=axioms_2954 on theBenchmark for (2954ds/598Mi) % 45.83/7.66 % (3048291)Instruction limit reached! % 45.83/7.66 % (3048291)------------------------------ % 45.83/7.66 % (3048291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.83/7.66 % (3048291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.77/7.94 % (3048291)CaDiCaL version: 2.1.3 % 47.77/7.94 % (3048291)Termination reason: Instruction limit % 47.77/7.94 % (3048291)Termination phase: Saturation % 47.77/7.94 % (3048291)Time elapsed: 3.337 s % 47.77/7.94 % (3048291)Peak memory usage: 349 MB % 47.77/7.94 % (3048291)Instructions burned: 5211 (million) % 47.77/7.94 % (3048320)Refutation not found, incomplete strategy % 47.77/7.94 % (3048320)------------------------------ % 47.77/7.94 % (3048320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.77/7.94 % (3048320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.77/7.94 % (3048320)CaDiCaL version: 2.1.3 % 47.77/7.94 % (3048320)Termination reason: Refutation not found, incomplete strategy % 47.77/7.94 % (3048320)Time elapsed: 0.014 s % 47.77/7.94 % (3048320)Peak memory usage: 93 MB % 47.77/7.94 % (3048320)Instructions burned: 23 (million) % 47.77/7.94 % (3048321)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=478341085:i=2989:sd=3:ss=axioms:sgt=60_2952 on theBenchmark for (2952ds/2989Mi) % 47.77/7.94 % (3048323)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=2432339657:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2951 on theBenchmark for (2951ds/1997Mi) % 47.77/7.94 % (3048320)------------------------------ % 47.77/7.94 % (3048320)------------------------------ % 47.77/7.94 % (3048326)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=220880914:i=2088:bd=preordered:av=off_2949 on theBenchmark for (2949ds/2088Mi) % 47.77/7.94 [W927 22:18:13.342226424 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342260554 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342299314 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342312307 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342338944 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342350814 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342376207 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342388017 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. % 47.77/7.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 47.77/7.94 [W927 22:18:13.342413291 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. % 50.64/8.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.64/8.25 [W927 22:18:13.342425041 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. % 50.64/8.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.64/8.25 [W927 22:18:13.342456771 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. % 50.64/8.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.64/8.25 [W927 22:18:13.342479404 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. % 50.64/8.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.64/8.25 % (3048321)Refutation not found, incomplete strategy % 50.64/8.25 % (3048321)------------------------------ % 50.64/8.25 % (3048321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.64/8.25 % (3048321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.64/8.25 % (3048321)CaDiCaL version: 2.1.3 % 50.64/8.25 % (3048321)Termination reason: Refutation not found, incomplete strategy % 50.64/8.25 % (3048321)Time elapsed: 0.593 s % 50.64/8.25 % (3048321)Peak memory usage: 135 MB % 50.64/8.25 % (3048321)Instructions burned: 886 (million) % 50.64/8.25 % (3048321)------------------------------ % 50.64/8.25 % (3048321)------------------------------ % 50.64/8.25 % (3048328)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=867270506:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi) % 50.64/8.25 % (3048328)Instruction limit reached! % 50.64/8.25 % (3048328)------------------------------ % 50.64/8.25 % (3048328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.64/8.25 % (3048328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.64/8.25 % (3048328)CaDiCaL version: 2.1.3 % 50.64/8.25 % (3048328)Termination reason: Instruction limit % 50.64/8.25 % (3048328)Termination phase: Saturation % 50.64/8.25 % (3048328)Time elapsed: 0.459 s % 50.64/8.25 % (3048328)Peak memory usage: 104 MB % 50.64/8.25 % (3048328)Instructions burned: 1099 (million) % 50.64/8.25 % (3048323)Instruction limit reached! % 50.64/8.25 % (3048323)------------------------------ % 50.64/8.25 % (3048323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.64/8.25 % (3048323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.64/8.25 % (3048323)CaDiCaL version: 2.1.3 % 50.64/8.25 % (3048323)Termination reason: Instruction limit % 50.64/8.25 % (3048323)Termination phase: Saturation % 50.64/8.25 % (3048323)Time elapsed: 1.425 s % 50.64/8.25 % (3048323)Peak memory usage: 286 MB % 50.64/8.25 % (3048323)Instructions burned: 1998 (million) % 50.64/8.25 % (3048330)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3749992819:i=433:bd=preordered_2935 on theBenchmark for (2935ds/433Mi) % 50.64/8.25 % (3048331)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=252343510:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2935 on theBenchmark for (2935ds/2942Mi) % 50.64/8.25 % (3048330)Refutation not found, incomplete strategy % 50.64/8.25 % (3048330)------------------------------ % 50.64/8.25 % (3048330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.64/8.25 % (3048330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.64/8.25 % (3048330)CaDiCaL version: 2.1.3 % 50.64/8.25 % (3048330)Termination reason: Refutation not found, incomplete strategy % 50.64/8.25 % (3048330)Time elapsed: 0.184 s % 50.64/8.25 % (3048330)Peak memory usage: 101 MB % 50.64/8.25 % (3048330)Instructions burned: 325 (million) % 50.64/8.25 % (3048326)Instruction limit reached! % 50.64/8.25 % (3048326)------------------------------ % 50.64/8.25 % (3048326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.32/8.95 % (3048326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.32/8.95 % (3048326)CaDiCaL version: 2.1.3 % 54.32/8.95 % (3048326)Termination reason: Instruction limit % 54.32/8.95 % (3048326)Termination phase: Saturation % 54.32/8.95 % (3048326)Time elapsed: 1.574 s % 54.32/8.95 % (3048326)Peak memory usage: 332 MB % 54.32/8.95 % (3048326)Instructions burned: 2089 (million) % 54.32/8.95 % (3048334)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2418548489:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2931 on theBenchmark for (2931ds/6922Mi) % 54.32/8.95 % (3048330)------------------------------ % 54.32/8.95 % (3048330)------------------------------ % 54.32/8.95 [W927 22:18:15.073322207 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073358434 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073396757 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073408744 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073434784 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073447271 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073475311 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073487451 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073513384 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073525284 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.32/8.95 [W927 22:18:15.073551488 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.32/8.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.073563474 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 % (3048336)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=3369258323:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2929 on theBenchmark for (2929ds/596Mi) % 64.37/10.18 % (3048331)Refutation not found, incomplete strategy % 64.37/10.18 % (3048331)------------------------------ % 64.37/10.18 % (3048331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.37/10.18 % (3048331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.37/10.18 % (3048331)CaDiCaL version: 2.1.3 % 64.37/10.18 % (3048331)Termination reason: Refutation not found, incomplete strategy % 64.37/10.18 % (3048331)Time elapsed: 0.629 s % 64.37/10.18 % (3048331)Peak memory usage: 136 MB % 64.37/10.18 % (3048331)Instructions burned: 1012 (million) % 64.37/10.18 [W927 22:18:15.385405294 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385444011 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385482944 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385493914 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385518931 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385539468 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385564988 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385578641 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385602998 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. % 64.37/10.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.37/10.18 [W927 22:18:15.385614851 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 [W927 22:18:15.385640684 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 [W927 22:18:15.385650971 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 % (3048336)Instruction limit reached! % 95.66/14.63 % (3048336)------------------------------ % 95.66/14.63 % (3048336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.66/14.63 % (3048336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.66/14.63 % (3048336)CaDiCaL version: 2.1.3 % 95.66/14.63 % (3048336)Termination reason: Instruction limit % 95.66/14.63 % (3048336)Termination phase: Saturation % 95.66/14.63 % (3048336)Time elapsed: 0.258 s % 95.66/14.63 % (3048336)Peak memory usage: 99 MB % 95.66/14.63 % (3048336)Instructions burned: 597 (million) % 95.66/14.63 % (3048331)------------------------------ % 95.66/14.63 % (3048331)------------------------------ % 95.66/14.63 % (3048334)Refutation not found, incomplete strategy % 95.66/14.63 % (3048334)------------------------------ % 95.66/14.63 % (3048334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.66/14.63 % (3048334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.66/14.63 % (3048334)CaDiCaL version: 2.1.3 % 95.66/14.63 % (3048334)Termination reason: Refutation not found, incomplete strategy % 95.66/14.63 % (3048334)Time elapsed: 0.592 s % 95.66/14.63 % (3048334)Peak memory usage: 135 MB % 95.66/14.63 % (3048334)Instructions burned: 898 (million) % 95.66/14.63 % (3048338)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=221414047:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2925 on theBenchmark for (2925ds/4123Mi) % 95.66/14.63 % (3048339)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2417624240:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2925 on theBenchmark for (2925ds/16411Mi) % 95.66/14.63 % (3048334)------------------------------ % 95.66/14.63 % (3048334)------------------------------ % 95.66/14.63 % (3048343)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=451780392:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2921 on theBenchmark for (2921ds/1670Mi) % 95.66/14.63 [W927 22:18:16.083798331 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 [W927 22:18:16.083834615 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 [W927 22:18:16.083874772 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 [W927 22:18:16.083886012 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. % 95.66/14.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.66/14.63 [W927 22:18:16.083918558 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.083930662 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.083962695 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.083973495 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.083997612 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.084031295 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.084057538 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. % 107.96/16.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.31 [W927 22:18:16.084068065 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. % 107.96/16.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.96/16.32 % (3048339)Refutation not found, incomplete strategy % 107.96/16.32 % (3048339)------------------------------ % 107.96/16.32 % (3048339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.32 % (3048339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.32 % (3048339)CaDiCaL version: 2.1.3 % 107.96/16.32 % (3048339)Termination reason: Refutation not found, incomplete strategy % 107.96/16.32 % (3048339)Time elapsed: 0.579 s % 107.96/16.32 % (3048339)Peak memory usage: 135 MB % 107.96/16.32 % (3048339)Instructions burned: 884 (million) % 107.96/16.32 % (3048339)------------------------------ % 107.96/16.32 % (3048339)------------------------------ % 107.96/16.32 % (3048313)Instruction limit reached! % 107.96/16.32 % (3048313)------------------------------ % 107.96/16.32 % (3048313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.32 % (3048313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.32 % (3048313)CaDiCaL version: 2.1.3 % 107.96/16.32 % (3048313)Termination reason: Instruction limit % 107.96/16.32 % (3048313)Termination phase: Saturation % 107.96/16.32 % (3048313)Time elapsed: 4.924 s % 107.96/16.32 % (3048313)Peak memory usage: 351 MB % 107.96/16.32 % (3048313)Instructions burned: 8480 (million) % 107.96/16.32 % (3048460)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=1533382249:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2914 on theBenchmark for (2914ds/1722Mi) % 107.96/16.32 % (3048461)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=409925152:cts=off:cond=on:i=9530:bs=on:fsd=on_2913 on theBenchmark for (2913ds/9530Mi) % 107.96/16.32 % (3048343)Instruction limit reached! % 107.96/16.32 % (3048343)------------------------------ % 107.96/16.32 % (3048343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.34 % (3048343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.34 % (3048343)CaDiCaL version: 2.1.3 % 107.96/16.34 % (3048343)Termination reason: Instruction limit % 107.96/16.34 % (3048343)Termination phase: Saturation % 107.96/16.34 % (3048343)Time elapsed: 1.327 s % 107.96/16.34 % (3048343)Peak memory usage: 312 MB % 107.96/16.34 % (3048343)Instructions burned: 1670 (million) % 107.96/16.34 % (3048565)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3505766285:st=2:i=4495:sd=10:ss=included_2906 on theBenchmark for (2906ds/4495Mi) % 107.96/16.34 % (3048310)Instruction limit reached! % 107.96/16.34 % (3048310)------------------------------ % 107.96/16.34 % (3048310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.34 % (3048310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.34 % (3048310)CaDiCaL version: 2.1.3 % 107.96/16.34 % (3048310)Termination reason: Instruction limit % 107.96/16.34 % (3048310)Termination phase: Saturation % 107.96/16.34 % (3048310)Time elapsed: 6.307 s % 107.96/16.34 % (3048310)Peak memory usage: 346 MB % 107.96/16.34 % (3048310)Instructions burned: 10309 (million) % 107.96/16.34 % (3048580)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=4196555551:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2903 on theBenchmark for (2903ds/4920Mi) % 107.96/16.34 % (3048460)Instruction limit reached! % 107.96/16.34 % (3048460)------------------------------ % 107.96/16.34 % (3048460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.34 % (3048460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.34 % (3048460)CaDiCaL version: 2.1.3 % 107.96/16.34 % (3048460)Termination reason: Instruction limit % 107.96/16.34 % (3048460)Termination phase: Saturation % 107.96/16.34 % (3048460)Time elapsed: 1.457 s % 107.96/16.34 % (3048460)Peak memory usage: 375 MB % 107.96/16.34 % (3048460)Instructions burned: 1725 (million) % 107.96/16.34 % (3048582)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=2097956283:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2898 on theBenchmark for (2898ds/2083Mi) % 107.96/16.34 % (3048338)Instruction limit reached! % 107.96/16.34 % (3048338)------------------------------ % 107.96/16.34 % (3048338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.34 % (3048338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.34 % (3048338)CaDiCaL version: 2.1.3 % 107.96/16.34 % (3048338)Termination reason: Instruction limit % 107.96/16.34 % (3048338)Termination phase: Saturation % 107.96/16.34 % (3048338)Time elapsed: 3.063 s % 107.96/16.34 % (3048338)Peak memory usage: 338 MB % 107.96/16.34 % (3048338)Instructions burned: 4124 (million) % 107.96/16.34 % (3048592)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=1904433452:i=4629:av=off:gsp=on_2892 on theBenchmark for (2892ds/4629Mi) % 107.96/16.34 % (3048582)Instruction limit reached! % 107.96/16.34 % (3048582)------------------------------ % 107.96/16.34 % (3048582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.34 % (3048582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.34 % (3048582)CaDiCaL version: 2.1.3 % 107.96/16.34 % (3048582)Termination reason: Instruction limit % 107.96/16.34 % (3048582)Termination phase: Saturation % 107.96/16.34 % (3048582)Time elapsed: 2.031 s % 107.96/16.34 % (3048582)Peak memory usage: 262 MB % 107.96/16.34 % (3048582)Instructions burned: 2083 (million) % 107.96/16.34 % (3048622)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3596924326:i=1258:av=off_2875 on theBenchmark for (2875ds/1258Mi) % 107.96/16.34 % (3048565)Instruction limit reached! % 107.96/16.34 % (3048565)------------------------------ % 107.96/16.34 % (3048565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.96/16.34 % (3048565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.96/16.34 % (3048565)CaDiCaL version: 2.1.3 % 107.96/16.34 % (3048565)Termination reason: Instruction limit % 107.96/16.34 % (3048565)Termination phase: Saturation % 107.96/16.34 % (3048565)Time elapsed: 3.908 s % 107.96/16.34 % (3048565)Peak memory usage: 329 MB % 107.96/16.34 % (3048565)Instructions burned: 4496 (million) % 107.96/16.34 % (3048622)Instruction limit reached! % 107.96/16.34 % (3048622)------------------------------ % 114.42/17.32 % (3048622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.42/17.32 % (3048622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.42/17.32 % (3048622)CaDiCaL version: 2.1.3 % 114.42/17.32 % (3048622)Termination reason: Instruction limit % 114.42/17.32 % (3048622)Termination phase: Saturation % 114.42/17.32 % (3048622)Time elapsed: 0.976 s % 114.42/17.32 % (3048622)Peak memory usage: 102 MB % 114.42/17.32 % (3048622)Instructions burned: 1259 (million) % 114.42/17.32 % (3048634)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3534533324:i=7343:av=off:ss=included_2865 on theBenchmark for (2865ds/7343Mi) % 114.42/17.32 % (3048637)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1151170824:i=1325:sd=2:ss=axioms:sgt=16_2862 on theBenchmark for (2862ds/1325Mi) % 114.42/17.32 % (3048637)Refutation not found, incomplete strategy % 114.42/17.32 % (3048637)------------------------------ % 114.42/17.32 % (3048637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.42/17.32 % (3048637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.42/17.32 % (3048637)CaDiCaL version: 2.1.3 % 114.42/17.32 % (3048637)Termination reason: Refutation not found, incomplete strategy % 114.42/17.32 % (3048637)Time elapsed: 0.022 s % 114.42/17.32 % (3048637)Peak memory usage: 93 MB % 114.42/17.32 % (3048637)Instructions burned: 23 (million) % 114.42/17.32 % (3048592)Refutation not found, incomplete strategy % 114.42/17.32 % (3048592)------------------------------ % 114.42/17.32 % (3048592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.42/17.32 % (3048592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.42/17.32 % (3048592)CaDiCaL version: 2.1.3 % 114.42/17.32 % (3048592)Termination reason: Refutation not found, incomplete strategy % 114.42/17.32 % (3048592)Time elapsed: 3.171 s % 114.42/17.32 % (3048592)Peak memory usage: 314 MB % 114.42/17.32 % (3048592)Instructions burned: 2892 (million) % 114.42/17.32 % (3048637)------------------------------ % 114.42/17.32 % (3048637)------------------------------ % 114.42/17.32 % (3048580)Instruction limit reached! % 114.42/17.32 % (3048580)------------------------------ % 114.42/17.32 % (3048580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.42/17.32 % (3048580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.42/17.32 % (3048580)CaDiCaL version: 2.1.3 % 114.42/17.32 % (3048580)Termination reason: Instruction limit % 114.42/17.32 % (3048580)Termination phase: Saturation % 114.42/17.32 % (3048580)Time elapsed: 4.703 s % 114.42/17.32 % (3048580)Peak memory usage: 331 MB % 114.42/17.32 % (3048580)Instructions burned: 4920 (million) % 114.42/17.32 % (3048592)------------------------------ % 114.42/17.32 % (3048592)------------------------------ % 114.42/17.32 % (3048650)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=70631763:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2855 on theBenchmark for (2855ds/2646Mi) % 114.42/17.32 % (3048655)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2035562276:i=1489:sd=2:ep=R:ss=axioms_2854 on theBenchmark for (2854ds/1489Mi) % 114.42/17.32 % (3048656)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=162967449:i=1503_2853 on theBenchmark for (2853ds/1503Mi) % 114.42/17.32 [W927 22:18:23.446148448 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. % 114.42/17.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.42/17.32 [W927 22:18:23.446194561 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. % 114.42/17.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.42/17.32 [W927 22:18:23.446249621 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. % 114.42/17.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446268011 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446308375 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446393238 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446443785 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446459478 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446496962 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446511725 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446548192 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.446563188 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.466334757 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.466465747 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.466570641 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.466622254 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. % 123.48/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.48/18.53 [W927 22:18:23.466698881 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.466774498 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.466853761 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.466902021 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.466975094 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.467050778 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.467136428 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 [W927 22:18:23.467184155 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. % 142.35/21.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.35/21.16 % (3048650)Refutation not found, incomplete strategy % 142.35/21.16 % (3048650)------------------------------ % 142.35/21.16 % (3048650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.35/21.16 % (3048650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.35/21.16 % (3048650)CaDiCaL version: 2.1.3 % 142.35/21.16 % (3048650)Termination reason: Refutation not found, incomplete strategy % 142.35/21.16 % (3048650)Time elapsed: 0.980 s % 142.35/21.16 % (3048650)Peak memory usage: 136 MB % 142.35/21.16 % (3048650)Instructions burned: 1002 (million) % 142.35/21.16 % (3048655)Refutation not found, incomplete strategy % 142.35/21.16 % (3048655)------------------------------ % 142.35/21.16 % (3048655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.35/21.16 % (3048655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.35/21.16 % (3048655)CaDiCaL version: 2.1.3 % 142.35/21.16 % (3048655)Termination reason: Refutation not found, incomplete strategy % 142.35/21.16 % (3048655)Time elapsed: 0.898 s % 142.35/21.16 % (3048655)Peak memory usage: 132 MB % 142.35/21.16 % (3048655)Instructions burned: 883 (million) % 142.35/21.16 % (3048655)------------------------------ % 142.35/21.16 % (3048655)------------------------------ % 142.35/21.16 % (3048650)------------------------------ % 142.35/21.16 % (3048650)------------------------------ % 142.35/21.16 % (3048671)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=4255117824:i=13942:kws=frequency_2838 on theBenchmark for (2838ds/13942Mi) % 142.35/21.16 % (3048672)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=1033673867:i=3604:fsr=off:er=filter_2838 on theBenchmark for (2838ds/3604Mi) % 146.16/21.76 % (3048461)Instruction limit reached! % 146.16/21.76 % (3048461)------------------------------ % 146.16/21.76 % (3048461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.16/21.76 % (3048461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.16/21.76 % (3048461)CaDiCaL version: 2.1.3 % 146.16/21.76 % (3048461)Termination reason: Instruction limit % 146.16/21.76 % (3048461)Termination phase: Saturation % 146.16/21.76 % (3048461)Time elapsed: 7.844 s % 146.16/21.76 % (3048461)Peak memory usage: 327 MB % 146.16/21.76 % (3048461)Instructions burned: 9530 (million) % 146.16/21.76 % (3048656)Instruction limit reached! % 146.16/21.76 % (3048656)------------------------------ % 146.16/21.76 % (3048656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.16/21.76 % (3048656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.16/21.76 % (3048656)CaDiCaL version: 2.1.3 % 146.16/21.76 % (3048656)Termination reason: Instruction limit % 146.16/21.76 % (3048656)Termination phase: Saturation % 146.16/21.76 % (3048656)Time elapsed: 1.799 s % 146.16/21.76 % (3048656)Peak memory usage: 294 MB % 146.16/21.76 % (3048656)Instructions burned: 1504 (million) % 146.16/21.76 % (3048677)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2010834105:i=1876:sd=1:ss=included:sgt=32_2833 on theBenchmark for (2833ds/1876Mi) % 146.16/21.76 % (3048678)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=128600307:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2832 on theBenchmark for (2832ds/1932Mi) % 146.16/21.76 [W927 22:18:26.664328891 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664452334 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664549944 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664592968 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664655988 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664695955 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664757028 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664796281 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. % 146.16/21.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.16/21.76 [W927 22:18:26.664858278 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. % 173.06/25.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.06/25.55 [W927 22:18:26.664938632 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. % 173.06/25.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.06/25.55 [W927 22:18:26.665015092 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. % 173.06/25.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.06/25.55 [W927 22:18:26.665057735 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. % 173.06/25.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.06/25.55 % (3048678)Refutation not found, incomplete strategy % 173.06/25.55 % (3048678)------------------------------ % 173.06/25.55 % (3048678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.06/25.55 % (3048678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/25.55 % (3048678)CaDiCaL version: 2.1.3 % 173.06/25.55 % (3048678)Termination reason: Refutation not found, incomplete strategy % 173.06/25.55 % (3048678)Time elapsed: 0.886 s % 173.06/25.55 % (3048678)Peak memory usage: 135 MB % 173.06/25.55 % (3048678)Instructions burned: 887 (million) % 173.06/25.55 % (3048678)------------------------------ % 173.06/25.55 % (3048678)------------------------------ % 173.06/25.55 % (3048685)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=2108751331:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2816 on theBenchmark for (2816ds/1980Mi) % 173.06/25.55 % (3048677)Instruction limit reached! % 173.06/25.55 % (3048677)------------------------------ % 173.06/25.55 % (3048677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.06/25.55 % (3048677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/25.55 % (3048677)CaDiCaL version: 2.1.3 % 173.06/25.55 % (3048677)Termination reason: Instruction limit % 173.06/25.55 % (3048677)Termination phase: Saturation % 173.06/25.55 % (3048677)Time elapsed: 2.358 s % 173.06/25.55 % (3048677)Peak memory usage: 364 MB % 173.06/25.55 % (3048677)Instructions burned: 1876 (million) % 173.06/25.55 % (3048689)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=3332904921:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2806 on theBenchmark for (2806ds/3902Mi) % 173.06/25.55 % (3048672)Instruction limit reached! % 173.06/25.55 % (3048672)------------------------------ % 173.06/25.55 % (3048672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.06/25.55 % (3048672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.06/25.55 % (3048672)CaDiCaL version: 2.1.3 % 173.06/25.55 % (3048672)Termination reason: Instruction limit % 173.06/25.55 % (3048672)Termination phase: Saturation % 173.06/25.55 % (3048672)Time elapsed: 3.554 s % 173.06/25.55 % (3048672)Peak memory usage: 312 MB % 173.06/25.55 % (3048672)Instructions burned: 3604 (million) % 173.06/25.55 [W927 22:18:28.292771902 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. % 173.06/25.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.06/25.55 [W927 22:18:28.292817812 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. % 173.06/25.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.06/25.55 [W927 22:18:28.292873639 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.292891809 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.292932592 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.292963232 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.293014049 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.293030872 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.293069559 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.293085786 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.293124126 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 [W927 22:18:28.293140193 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. % 178.04/26.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 178.04/26.21 % (3048693)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1005032825:avsq=on:i=3916:aac=none:amm=off_2799 on theBenchmark for (2799ds/3916Mi) % 178.04/26.21 % (3048689)Refutation not found, incomplete strategy % 178.04/26.21 % (3048689)------------------------------ % 178.04/26.21 % (3048689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.04/26.21 % (3048689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.04/26.21 % (3048689)CaDiCaL version: 2.1.3 % 178.04/26.21 % (3048689)Termination reason: Refutation not found, incomplete strategy % 178.04/26.21 % (3048689)Time elapsed: 0.846 s % 178.04/26.21 % (3048689)Peak memory usage: 132 MB % 178.04/26.21 % (3048689)Instructions burned: 888 (million) % 178.04/26.21 % (3048685)Instruction limit reached! % 178.04/26.21 % (3048685)------------------------------ % 178.04/26.21 % (3048685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.04/26.21 % (3048685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.04/26.21 % (3048685)CaDiCaL version: 2.1.3 % 178.04/26.21 % (3048685)Termination reason: Instruction limit % 178.04/26.21 % (3048685)Termination phase: Saturation % 178.04/26.21 % (3048685)Time elapsed: 2.289 s % 178.04/26.21 % (3048685)Peak memory usage: 312 MB % 220.41/32.19 % (3048685)Instructions burned: 1980 (million) % 220.41/32.19 % (3048689)------------------------------ % 220.41/32.19 % (3048689)------------------------------ % 220.41/32.19 % (3048634)Instruction limit reached! % 220.41/32.19 % (3048634)------------------------------ % 220.41/32.19 % (3048634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.41/32.19 % (3048634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.41/32.19 % (3048634)CaDiCaL version: 2.1.3 % 220.41/32.19 % (3048634)Termination reason: Instruction limit % 220.41/32.19 % (3048634)Termination phase: Saturation % 220.41/32.19 % (3048634)Time elapsed: 7.344 s % 220.41/32.19 % (3048634)Peak memory usage: 326 MB % 220.41/32.19 % (3048634)Instructions burned: 7345 (million) % 220.41/32.19 % (3048699)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3398292713:cond=on:i=3940:av=off:er=known_2790 on theBenchmark for (2790ds/3940Mi) % 220.41/32.19 % (3048700)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=579599688:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2790 on theBenchmark for (2790ds/3980Mi) % 220.41/32.19 % (3048703)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=3889735922:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2788 on theBenchmark for (2788ds/2087Mi) % 220.41/32.19 % (3048703)Instruction limit reached! % 220.41/32.19 % (3048703)------------------------------ % 220.41/32.19 % (3048703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.41/32.19 % (3048703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.41/32.19 % (3048703)CaDiCaL version: 2.1.3 % 220.41/32.19 % (3048703)Termination reason: Instruction limit % 220.41/32.19 % (3048703)Termination phase: Saturation % 220.41/32.19 % (3048703)Time elapsed: 2.105 s % 220.41/32.19 % (3048703)Peak memory usage: 264 MB % 220.41/32.19 % (3048703)Instructions burned: 2089 (million) % 220.41/32.19 % (3048693)Instruction limit reached! % 220.41/32.19 % (3048693)------------------------------ % 220.41/32.19 % (3048693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.41/32.19 % (3048693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.41/32.19 % (3048693)CaDiCaL version: 2.1.3 % 220.41/32.19 % (3048693)Termination reason: Instruction limit % 220.41/32.19 % (3048693)Termination phase: Saturation % 220.41/32.19 % (3048693)Time elapsed: 3.260 s % 220.41/32.19 % (3048693)Peak memory usage: 115 MB % 220.41/32.19 % (3048693)Instructions burned: 3916 (million) % 220.41/32.19 % (3048717)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=2204736151:cts=off:cond=on:i=4272:bs=on:fsd=on_2764 on theBenchmark for (2764ds/4272Mi) % 220.41/32.19 % (3048718)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2010463300:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2763 on theBenchmark for (2763ds/2197Mi) % 220.41/32.19 [W927 22:18:33.681517076 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. % 220.41/32.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.41/32.19 [W927 22:18:33.681569073 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. % 220.41/32.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.41/32.19 [W927 22:18:33.681637389 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. % 220.41/32.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.41/32.19 [W927 22:18:33.681660406 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. % 220.41/32.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681710923 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681731169 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681778526 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681799476 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681844253 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681861946 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681907023 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 [W927 22:18:33.681924383 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. % 238.87/35.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/35.00 % (3048718)Refutation not found, incomplete strategy % 238.87/35.00 % (3048718)------------------------------ % 238.87/35.00 % (3048718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.87/35.00 % (3048718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/35.00 % (3048718)CaDiCaL version: 2.1.3 % 238.87/35.00 % (3048718)Termination reason: Refutation not found, incomplete strategy % 238.87/35.00 % (3048718)Time elapsed: 0.975 s % 238.87/35.00 % (3048718)Peak memory usage: 136 MB % 238.87/35.00 % (3048718)Instructions burned: 895 (million) % 238.87/35.00 % (3048700)Instruction limit reached! % 238.87/35.00 % (3048700)------------------------------ % 238.87/35.00 % (3048700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.87/35.00 % (3048700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/35.00 % (3048700)CaDiCaL version: 2.1.3 % 238.87/35.00 % (3048700)Termination reason: Instruction limit % 238.87/35.00 % (3048700)Termination phase: Saturation % 238.87/35.00 % (3048700)Time elapsed: 3.808 s % 238.87/35.00 % (3048700)Peak memory usage: 312 MB % 238.87/35.00 % (3048700)Instructions burned: 3981 (million) % 238.87/35.00 % (3048718)------------------------------ % 238.87/35.00 % (3048718)------------------------------ % 238.87/35.00 % (3048699)Instruction limit reached! % 238.87/35.00 % (3048699)------------------------------ % 238.87/35.00 % (3048699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.87/35.00 % (3048699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/35.00 % (3048699)CaDiCaL version: 2.1.3 % 238.87/35.00 % (3048699)Termination reason: Instruction limit % 238.87/35.00 % (3048699)Termination phase: Saturation % 238.87/35.00 % (3048699)Time elapsed: 4.165 s % 251.04/36.50 % (3048699)Peak memory usage: 335 MB % 251.04/36.50 % (3048699)Instructions burned: 3940 (million) % 251.04/36.50 % (3048723)dis+21_1_sil=8000:spb=goal_then_units:random_seed=982641427:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2748 on theBenchmark for (2748ds/6508Mi) % 251.04/36.50 % (3048726)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1499889738:i=2330:fgj=on:av=off:fsr=off_2746 on theBenchmark for (2746ds/2330Mi) % 251.04/36.50 % (3048727)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=3181681005:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2746 on theBenchmark for (2746ds/7592Mi) % 251.04/36.50 % (3048717)Instruction limit reached! % 251.04/36.50 % (3048717)------------------------------ % 251.04/36.50 % (3048717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.04/36.50 % (3048717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.04/36.50 % (3048717)CaDiCaL version: 2.1.3 % 251.04/36.50 % (3048717)Termination reason: Instruction limit % 251.04/36.50 % (3048717)Termination phase: Saturation % 251.04/36.50 % (3048717)Time elapsed: 4.169 s % 251.04/36.50 % (3048717)Peak memory usage: 318 MB % 251.04/36.50 % (3048717)Instructions burned: 4273 (million) % 251.04/36.50 % (3048726)Instruction limit reached! % 251.04/36.50 % (3048726)------------------------------ % 251.04/36.50 % (3048726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.04/36.50 % (3048726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.04/36.50 % (3048726)CaDiCaL version: 2.1.3 % 251.04/36.50 % (3048726)Termination reason: Instruction limit % 251.04/36.50 % (3048726)Termination phase: Saturation % 251.04/36.50 % (3048726)Time elapsed: 2.547 s % 251.04/36.50 % (3048726)Peak memory usage: 272 MB % 251.04/36.50 % (3048726)Instructions burned: 2330 (million) % 251.04/36.50 % (3048747)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=3515399159:i=2693:kws=precedence:ins=1:av=off_2720 on theBenchmark for (2720ds/2693Mi) % 251.04/36.50 % (3048749)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=895304976:i=28651:sd=4:ss=included:sgt=64_2717 on theBenchmark for (2717ds/28651Mi) % 251.04/36.50 % (3048671)Instruction limit reached! % 251.04/36.50 % (3048671)------------------------------ % 251.04/36.50 % (3048671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.04/36.50 % (3048671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.04/36.50 % (3048671)CaDiCaL version: 2.1.3 % 251.04/36.50 % (3048671)Termination reason: Instruction limit % 251.04/36.50 % (3048671)Termination phase: Saturation % 251.04/36.50 % (3048671)Time elapsed: 13.117 s % 251.04/36.50 % (3048671)Peak memory usage: 335 MB % 251.04/36.50 % (3048671)Instructions burned: 13942 (million) % 251.04/36.50 % (3048758)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=382546241:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2703 on theBenchmark for (2703ds/2700Mi) % 251.04/36.50 % (3048723)Instruction limit reached! % 251.04/36.50 % (3048723)------------------------------ % 251.04/36.50 % (3048723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.04/36.50 % (3048723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.04/36.50 % (3048723)CaDiCaL version: 2.1.3 % 251.04/36.50 % (3048723)Termination reason: Instruction limit % 251.04/36.50 % (3048723)Termination phase: Saturation % 251.04/36.50 % (3048723)Time elapsed: 5.039 s % 251.04/36.50 % (3048723)Peak memory usage: 124 MB % 251.04/36.50 % (3048723)Instructions burned: 6508 (million) % 251.04/36.50 % (3048763)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=4253236533:i=3196:nm=4_2695 on theBenchmark for (2695ds/3196Mi) % 251.04/36.50 % (3048747)Instruction limit reached! % 251.04/36.50 % (3048747)------------------------------ % 251.04/36.50 % (3048747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.04/36.50 % (3048747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.04/36.50 % (3048747)CaDiCaL version: 2.1.3 % 251.04/36.50 % (3048747)Termination reason: Instruction limit % 251.04/36.50 % (3048747)Termination phase: Saturation % 251.04/36.50 % (3048747)Time elapsed: 2.721 s % 251.04/36.50 % (3048747)Peak memory usage: 299 MB % 251.04/36.50 % (3048747)Instructions burned: 2693 (million) % 251.04/36.50 % (3048767)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3867241027:cts=off:i=3254:av=off_2689 on theBenchmark for (2689ds/3254Mi) % 300.03/43.44 % (3048727)Instruction limit reached! % 300.03/43.44 % (3048727)------------------------------ % 300.03/43.44 % (3048727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.03/43.44 % (3048727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.03/43.44 % (3048727)CaDiCaL version: 2.1.3 % 300.03/43.44 % (3048727)Termination reason: Instruction limit % 300.03/43.44 % (3048727)Termination phase: Saturation % 300.03/43.44 % (3048727)Time elapsed: 6.850 s % 300.03/43.44 % (3048727)Peak memory usage: 127 MB % 300.03/43.44 % (3048727)Instructions burned: 7592 (million) % 300.03/43.44 % (3048771)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=4202071636:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2674 on theBenchmark for (2674ds/3264Mi) % 300.03/43.44 % (3048758)Instruction limit reached! % 300.03/43.44 % (3048758)------------------------------ % 300.03/43.44 % (3048758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.03/43.44 % (3048758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.03/43.44 % (3048758)CaDiCaL version: 2.1.3 % 300.03/43.44 % (3048758)Termination reason: Instruction limit % 300.03/43.44 % (3048758)Termination phase: Saturation % 300.03/43.44 % (3048758)Time elapsed: 3.135 s % 300.03/43.44 % (3048758)Peak memory usage: 355 MB % 300.03/43.44 % (3048758)Instructions burned: 2701 (million) % 300.03/43.44 % (3048773)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=3074495196:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2668 on theBenchmark for (2668ds/9708Mi) % 300.03/43.44 % (3048763)Refutation not found, incomplete strategy % 300.03/43.44 % (3048763)------------------------------ % 300.03/43.44 % (3048763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.03/43.44 % (3048763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.03/43.44 % (3048763)CaDiCaL version: 2.1.3 % 300.03/43.44 % (3048763)Termination reason: Refutation not found, incomplete strategy % 300.03/43.44 % (3048763)Time elapsed: 3.013 s % 300.03/43.44 % (3048763)Peak memory usage: 342 MB % 300.03/43.44 % (3048763)Instructions burned: 2728 (million) % 300.03/43.44 [W927 22:18:42.131025523 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. % 300.03/43.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.03/43.44 [W927 22:18:42.131088510 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. % 300.03/43.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.03/43.44 [W927 22:18:42.131153783 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. % 300.03/43.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.03/43.44 [W927 22:18:42.131172320 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. % 300.03/43.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.03/43.44 [W927 22:18:42.131219860 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. % 300.03/43.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.03/43.44 [W927 22:18:42.131238206 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. % 300.03/43.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.03/43.44 [W % 300.03/43.45 Terminated %------------------------------------------------------------------------------