%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM229-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n014.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:11:56 PM UTC 2026 % Result : Timeout 300.63s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM229-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.13/0.39 % Computer : n014.cluster.edu % 0.13/0.39 % Model : x86_64 x86_64 % 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.39 % Memory : 8046.5625MB % 0.13/0.39 % OS : Linux 6.8.0-71-generic % 0.13/0.39 % CPULimit : 300 % 0.13/0.39 % WCLimit : 300 % 0.13/0.39 % DateTime : Sun Sep 27 19:14:32 UTC 2026 % 0.13/0.39 % CPUTime : % 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.13/0.42 Running first-order theorem proving % 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.32/2.17 % (1110665)Input is clausal, will run a generic CNF schedule. % 9.32/2.17 % (1110673)lrs+10_1_sil=8000:sp=occurrence:random_seed=787656208:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.32/2.17 % (1110673)Instruction limit reached! % 9.32/2.17 % (1110673)------------------------------ % 9.32/2.17 % (1110673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.32/2.17 % (1110673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.32/2.17 % (1110673)CaDiCaL version: 2.1.3 % 9.32/2.17 % (1110673)Termination reason: Instruction limit % 9.32/2.17 % (1110673)Termination phase: Saturation % 9.32/2.17 % (1110673)Time elapsed: 0.038 s % 9.32/2.17 % (1110673)Peak memory usage: 90 MB % 9.32/2.17 % (1110673)Instructions burned: 110 (million) % 9.32/2.17 % (1110671)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=533902386:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.32/2.17 % (1110670)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=100642574:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.32/2.17 % (1110675)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3464166332:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.32/2.17 % (1110674)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1640012516:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.32/2.17 % (1110676)dis-21_1_sil=8000:lcm=predicate:random_seed=1933946755:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 9.32/2.17 % (1110672)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1544994247:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.32/2.17 % (1110676)Instruction limit reached! % 9.32/2.17 % (1110676)------------------------------ % 9.32/2.17 % (1110676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.32/2.17 % (1110676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.32/2.17 % (1110676)CaDiCaL version: 2.1.3 % 9.32/2.17 % (1110676)Termination reason: Instruction limit % 9.32/2.17 % (1110676)Termination phase: Saturation % 9.32/2.17 % (1110676)Time elapsed: 0.061 s % 9.32/2.17 % (1110676)Peak memory usage: 89 MB % 9.32/2.17 % (1110676)Instructions burned: 118 (million) % 9.32/2.17 % (1110674)Instruction limit reached! % 9.32/2.17 % (1110674)------------------------------ % 9.32/2.17 % (1110674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.32/2.17 % (1110674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.32/2.17 % (1110674)CaDiCaL version: 2.1.3 % 9.32/2.17 % (1110674)Termination reason: Instruction limit % 9.32/2.17 % (1110674)Termination phase: Saturation % 9.32/2.17 % (1110674)Time elapsed: 0.073 s % 9.32/2.17 % (1110674)Peak memory usage: 89 MB % 9.32/2.17 % (1110674)Instructions burned: 116 (million) % 9.32/2.17 % (1110678)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=762681171:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 9.32/2.17 % (1110678)Instruction limit reached! % 9.32/2.17 % (1110678)------------------------------ % 9.32/2.17 % (1110678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.32/2.17 % (1110678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.32/2.17 % (1110678)CaDiCaL version: 2.1.3 % 9.32/2.17 % (1110678)Termination reason: Instruction limit % 9.32/2.17 % (1110678)Termination phase: Saturation % 9.32/2.17 % (1110678)Time elapsed: 0.055 s % 9.32/2.17 % (1110678)Peak memory usage: 90 MB % 9.32/2.17 % (1110678)Instructions burned: 146 (million) % 9.32/2.17 % (1110675)Instruction limit reached! % 9.32/2.17 % (1110675)------------------------------ % 9.32/2.17 % (1110675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.32/2.17 % (1110675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.32/2.17 % (1110675)CaDiCaL version: 2.1.3 % 9.32/2.17 % (1110675)Termination reason: Instruction limit % 9.32/2.17 % (1110675)Termination phase: Saturation % 9.32/2.17 % (1110675)Time elapsed: 0.139 s % 9.32/2.17 % (1110675)Peak memory usage: 90 MB % 9.32/2.17 % (1110675)Instructions burned: 181 (million) % 9.32/2.17 % (1110685)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2719004422:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 14.19/3.04 % (1110686)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1444633639:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 14.19/3.04 % (1110686)Refutation not found, incomplete strategy % 14.19/3.04 % (1110686)------------------------------ % 14.19/3.04 % (1110686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.19/3.04 % (1110686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.19/3.04 % (1110686)CaDiCaL version: 2.1.3 % 14.19/3.04 % (1110686)Termination reason: Refutation not found, incomplete strategy % 14.19/3.04 % (1110686)Time elapsed: 0.004 s % 14.19/3.04 % (1110686)Peak memory usage: 88 MB % 14.19/3.04 % (1110686)Instructions burned: 5 (million) % 14.19/3.04 % (1110688)lrs+10_64_to=lpo:sil=8000:random_seed=3034276109:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 14.19/3.04 % (1110688)Instruction limit reached! % 14.19/3.04 % (1110688)------------------------------ % 14.19/3.04 % (1110688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.19/3.04 % (1110688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.19/3.04 % (1110688)CaDiCaL version: 2.1.3 % 14.19/3.04 % (1110688)Termination reason: Instruction limit % 14.19/3.04 % (1110688)Termination phase: Saturation % 14.19/3.04 % (1110688)Time elapsed: 0.044 s % 14.19/3.04 % (1110688)Peak memory usage: 89 MB % 14.19/3.04 % (1110688)Instructions burned: 128 (million) % 14.19/3.04 % (1110689)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2319120932:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi) % 14.19/3.04 % (1110685)Instruction limit reached! % 14.19/3.04 % (1110685)------------------------------ % 14.19/3.04 % (1110685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.19/3.04 % (1110685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.19/3.04 % (1110685)CaDiCaL version: 2.1.3 % 14.19/3.04 % (1110685)Termination reason: Instruction limit % 14.19/3.04 % (1110685)Termination phase: Saturation % 14.19/3.04 % (1110685)Time elapsed: 0.109 s % 14.19/3.04 % (1110685)Peak memory usage: 91 MB % 14.19/3.04 % (1110685)Instructions burned: 190 (million) % 14.19/3.04 % (1110693)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1479582434:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 14.19/3.04 % (1110689)Instruction limit reached! % 14.19/3.04 % (1110689)------------------------------ % 14.19/3.04 % (1110689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.19/3.04 % (1110689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.19/3.04 % (1110689)CaDiCaL version: 2.1.3 % 14.19/3.04 % (1110689)Termination reason: Instruction limit % 14.19/3.04 % (1110689)Termination phase: Saturation % 14.19/3.04 % (1110689)Time elapsed: 0.101 s % 14.19/3.04 % (1110689)Peak memory usage: 90 MB % 14.19/3.04 % (1110689)Instructions burned: 194 (million) % 14.19/3.04 % (1110693)Instruction limit reached! % 14.19/3.04 % (1110693)------------------------------ % 14.19/3.04 % (1110693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.19/3.04 % (1110693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.19/3.04 % (1110693)CaDiCaL version: 2.1.3 % 14.19/3.04 % (1110693)Termination reason: Instruction limit % 14.19/3.04 % (1110693)Termination phase: Saturation % 14.19/3.04 % (1110693)Time elapsed: 0.061 s % 14.19/3.04 % (1110693)Peak memory usage: 91 MB % 14.19/3.04 % (1110693)Instructions burned: 159 (million) % 14.19/3.04 % (1110695)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3448975902:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi) % 14.19/3.04 % (1110686)------------------------------ % 14.19/3.04 % (1110686)------------------------------ % 14.19/3.04 % (1110698)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=361275078:i=107_2994 on theBenchmark for (2994ds/107Mi) % 14.19/3.04 % (1110697)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=3526397813:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 14.19/3.04 % (1110698)Instruction limit reached! % 14.19/3.04 % (1110698)------------------------------ % 31.63/5.30 % (1110698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.63/5.30 % (1110698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.63/5.30 % (1110698)CaDiCaL version: 2.1.3 % 31.63/5.30 % (1110698)Termination reason: Instruction limit % 31.63/5.30 % (1110698)Termination phase: Saturation % 31.63/5.30 % (1110698)Time elapsed: 0.041 s % 31.63/5.30 % (1110698)Peak memory usage: 90 MB % 31.63/5.30 % (1110698)Instructions burned: 109 (million) % 31.63/5.30 % (1110697)Instruction limit reached! % 31.63/5.30 % (1110697)------------------------------ % 31.63/5.30 % (1110697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.63/5.30 % (1110697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.63/5.30 % (1110697)CaDiCaL version: 2.1.3 % 31.63/5.30 % (1110697)Termination reason: Instruction limit % 31.63/5.30 % (1110697)Termination phase: Saturation % 31.63/5.30 % (1110697)Time elapsed: 0.061 s % 31.63/5.30 % (1110697)Peak memory usage: 89 MB % 31.63/5.30 % (1110697)Instructions burned: 106 (million) % 31.63/5.30 % (1110700)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2890113293:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 31.63/5.30 % (1110703)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3090496236:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 31.63/5.30 % (1110704)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2551841053:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi) % 31.63/5.30 % (1110700)Instruction limit reached! % 31.63/5.30 % (1110700)------------------------------ % 31.63/5.30 % (1110700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.63/5.30 % (1110700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.63/5.30 % (1110700)CaDiCaL version: 2.1.3 % 31.63/5.30 % (1110700)Termination reason: Instruction limit % 31.63/5.30 % (1110700)Termination phase: Saturation % 31.63/5.30 % (1110700)Time elapsed: 0.155 s % 31.63/5.30 % (1110700)Peak memory usage: 91 MB % 31.63/5.30 % (1110700)Instructions burned: 242 (million) % 31.63/5.30 % (1110704)Instruction limit reached! % 31.63/5.30 % (1110704)------------------------------ % 31.63/5.30 % (1110704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.63/5.30 % (1110704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.63/5.30 % (1110704)CaDiCaL version: 2.1.3 % 31.63/5.30 % (1110704)Termination reason: Instruction limit % 31.63/5.30 % (1110704)Termination phase: Saturation % 31.63/5.30 % (1110704)Time elapsed: 0.082 s % 31.63/5.30 % (1110704)Peak memory usage: 89 MB % 31.63/5.30 % (1110704)Instructions burned: 135 (million) % 31.63/5.30 % (1110708)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4038756446:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi) % 31.63/5.30 % (1110709)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=695795102:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi) % 31.63/5.30 % (1110709)Instruction limit reached! % 31.63/5.30 % (1110709)------------------------------ % 31.63/5.30 % (1110709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.63/5.30 % (1110709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.63/5.30 % (1110709)CaDiCaL version: 2.1.3 % 31.63/5.30 % (1110709)Termination reason: Instruction limit % 31.63/5.30 % (1110709)Termination phase: Saturation % 31.63/5.30 % (1110709)Time elapsed: 0.114 s % 31.63/5.30 % (1110709)Peak memory usage: 90 MB % 31.63/5.30 % (1110709)Instructions burned: 191 (million) % 31.63/5.30 % (1110712)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=441177291:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 31.63/5.30 % (1110708)Instruction limit reached! % 31.63/5.30 % (1110708)------------------------------ % 31.63/5.30 % (1110708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.63/5.30 % (1110708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.63/5.30 % (1110708)CaDiCaL version: 2.1.3 % 31.63/5.30 % (1110708)Termination reason: Instruction limit % 31.63/5.30 % (1110708)Termination phase: Saturation % 31.63/5.30 % (1110708)Time elapsed: 0.286 s % 31.63/5.30 % (1110708)Peak memory usage: 97 MB % 31.63/5.30 % (1110708)Instructions burned: 500 (million) % 44.14/7.04 % (1110714)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3840322652:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 44.14/7.04 % (1110712)Instruction limit reached! % 44.14/7.04 % (1110712)------------------------------ % 44.14/7.04 % (1110712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.14/7.04 % (1110712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.14/7.04 % (1110712)CaDiCaL version: 2.1.3 % 44.14/7.04 % (1110712)Termination reason: Instruction limit % 44.14/7.04 % (1110712)Termination phase: Saturation % 44.14/7.04 % (1110712)Time elapsed: 0.177 s % 44.14/7.04 % (1110712)Peak memory usage: 92 MB % 44.14/7.04 % (1110712)Instructions burned: 265 (million) % 44.14/7.04 % (1110714)Instruction limit reached! % 44.14/7.04 % (1110714)------------------------------ % 44.14/7.04 % (1110714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.14/7.04 % (1110714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.14/7.04 % (1110714)CaDiCaL version: 2.1.3 % 44.14/7.04 % (1110714)Termination reason: Instruction limit % 44.14/7.04 % (1110714)Termination phase: Saturation % 44.14/7.04 % (1110714)Time elapsed: 0.091 s % 44.14/7.04 % (1110714)Peak memory usage: 89 MB % 44.14/7.04 % (1110714)Instructions burned: 157 (million) % 44.14/7.04 % (1110716)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=1234677731:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi) % 44.14/7.04 % (1110717)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=951441988:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 44.14/7.04 % (1110695)Instruction limit reached! % 44.14/7.04 % (1110695)------------------------------ % 44.14/7.04 % (1110695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.14/7.04 % (1110695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.14/7.04 % (1110695)CaDiCaL version: 2.1.3 % 44.14/7.04 % (1110695)Termination reason: Instruction limit % 44.14/7.04 % (1110695)Termination phase: Saturation % 44.14/7.04 % (1110695)Time elapsed: 1.281 s % 44.14/7.04 % (1110695)Peak memory usage: 147 MB % 44.14/7.04 % (1110695)Instructions burned: 3396 (million) % 44.14/7.04 % (1110720)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2125805819:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi) % 44.14/7.04 % (1110717)Instruction limit reached! % 44.14/7.04 % (1110717)------------------------------ % 44.14/7.04 % (1110717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.14/7.04 % (1110717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.14/7.04 % (1110717)CaDiCaL version: 2.1.3 % 44.14/7.04 % (1110717)Termination reason: Instruction limit % 44.14/7.04 % (1110717)Termination phase: Saturation % 44.14/7.04 % (1110717)Time elapsed: 0.274 s % 44.14/7.04 % (1110717)Peak memory usage: 88 MB % 44.14/7.04 % (1110717)Instructions burned: 538 (million) % 44.14/7.04 % (1110720)Instruction limit reached! % 44.14/7.04 % (1110720)------------------------------ % 44.14/7.04 % (1110720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.14/7.04 % (1110720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.14/7.04 % (1110720)CaDiCaL version: 2.1.3 % 44.14/7.04 % (1110720)Termination reason: Instruction limit % 44.14/7.04 % (1110720)Termination phase: Saturation % 44.14/7.04 % (1110720)Time elapsed: 0.053 s % 44.14/7.04 % (1110720)Peak memory usage: 90 MB % 44.14/7.04 % (1110720)Instructions burned: 182 (million) % 44.14/7.04 % (1110722)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=2593646319:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi) % 44.14/7.04 % (1110723)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=2603661835:i=412:gtgl=4:gtg=exists_all_2980 on theBenchmark for (2980ds/412Mi) % 44.14/7.04 % (1110723)Instruction limit reached! % 44.14/7.04 % (1110723)------------------------------ % 44.14/7.04 % (1110723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.14/7.04 % (1110723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.14/7.04 % (1110723)CaDiCaL version: 2.1.3 % 64.35/9.97 % (1110723)Termination reason: Instruction limit % 64.35/9.97 % (1110723)Termination phase: Saturation % 64.35/9.97 % (1110723)Time elapsed: 0.099 s % 64.35/9.97 % (1110723)Peak memory usage: 90 MB % 64.35/9.97 % (1110723)Instructions burned: 413 (million) % 64.35/9.97 % (1110726)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=718644056:s2pl=no:i=8478:s2at=4:nm=6_2978 on theBenchmark for (2978ds/8478Mi) % 64.35/9.97 % (1110716)Instruction limit reached! % 64.35/9.97 % (1110716)------------------------------ % 64.35/9.97 % (1110716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.97 % (1110716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.97 % (1110716)CaDiCaL version: 2.1.3 % 64.35/9.97 % (1110716)Termination reason: Instruction limit % 64.35/9.97 % (1110716)Termination phase: Saturation % 64.35/9.97 % (1110716)Time elapsed: 1.946 s % 64.35/9.97 % (1110716)Peak memory usage: 148 MB % 64.35/9.97 % (1110716)Instructions burned: 3257 (million) % 64.35/9.97 % (1110728)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=3293295957:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi) % 64.35/9.97 % (1110703)Instruction limit reached! % 64.35/9.97 % (1110703)------------------------------ % 64.35/9.97 % (1110703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.97 % (1110703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.97 % (1110703)CaDiCaL version: 2.1.3 % 64.35/9.97 % (1110703)Termination reason: Instruction limit % 64.35/9.97 % (1110703)Termination phase: Saturation % 64.35/9.97 % (1110703)Time elapsed: 3.019 s % 64.35/9.97 % (1110703)Peak memory usage: 159 MB % 64.35/9.97 % (1110703)Instructions burned: 5209 (million) % 64.35/9.97 % (1110728)Instruction limit reached! % 64.35/9.97 % (1110728)------------------------------ % 64.35/9.97 % (1110728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.97 % (1110728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.97 % (1110728)CaDiCaL version: 2.1.3 % 64.35/9.97 % (1110728)Termination reason: Instruction limit % 64.35/9.97 % (1110728)Termination phase: Saturation % 64.35/9.97 % (1110728)Time elapsed: 0.166 s % 64.35/9.97 % (1110728)Peak memory usage: 92 MB % 64.35/9.97 % (1110728)Instructions burned: 304 (million) % 64.35/9.97 % (1110730)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1911177561:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi) % 64.35/9.97 % (1110731)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2808470964:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi) % 64.35/9.97 % (1110731)Instruction limit reached! % 64.35/9.97 % (1110731)------------------------------ % 64.35/9.97 % (1110731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.97 % (1110731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.97 % (1110731)CaDiCaL version: 2.1.3 % 64.35/9.97 % (1110731)Termination reason: Instruction limit % 64.35/9.97 % (1110731)Termination phase: Saturation % 64.35/9.97 % (1110731)Time elapsed: 0.324 s % 64.35/9.97 % (1110731)Peak memory usage: 94 MB % 64.35/9.97 % (1110731)Instructions burned: 599 (million) % 64.35/9.97 % (1110730)Instruction limit reached! % 64.35/9.97 % (1110730)------------------------------ % 64.35/9.97 % (1110730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.97 % (1110730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.97 % (1110730)CaDiCaL version: 2.1.3 % 64.35/9.97 % (1110730)Termination reason: Instruction limit % 64.35/9.97 % (1110730)Termination phase: Saturation % 64.35/9.97 % (1110730)Time elapsed: 0.378 s % 64.35/9.97 % (1110730)Peak memory usage: 98 MB % 64.35/9.97 % (1110730)Instructions burned: 721 (million) % 64.35/9.97 % (1110734)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2535850415:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi) % 64.35/9.97 % (1110735)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=1483814187:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi) % 94.51/14.16 % (1110726)Instruction limit reached! % 94.51/14.16 % (1110726)------------------------------ % 94.51/14.16 % (1110726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.16 % (1110726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.16 % (1110726)CaDiCaL version: 2.1.3 % 94.51/14.16 % (1110726)Termination reason: Instruction limit % 94.51/14.16 % (1110726)Termination phase: Saturation % 94.51/14.16 % (1110726)Time elapsed: 2.359 s % 94.51/14.16 % (1110726)Peak memory usage: 189 MB % 94.51/14.16 % (1110726)Instructions burned: 8481 (million) % 94.51/14.16 % (1110738)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=1523347547:i=2088:bd=preordered:av=off_2953 on theBenchmark for (2953ds/2088Mi) % 94.51/14.16 % (1110734)Instruction limit reached! % 94.51/14.16 % (1110734)------------------------------ % 94.51/14.16 % (1110734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.16 % (1110734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.16 % (1110734)CaDiCaL version: 2.1.3 % 94.51/14.16 % (1110734)Termination reason: Instruction limit % 94.51/14.16 % (1110734)Termination phase: Saturation % 94.51/14.16 % (1110734)Time elapsed: 1.212 s % 94.51/14.16 % (1110734)Peak memory usage: 143 MB % 94.51/14.16 % (1110734)Instructions burned: 2990 (million) % 94.51/14.16 % (1110740)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=743234741:i=1098:nicw=on_2943 on theBenchmark for (2943ds/1098Mi) % 94.51/14.16 % (1110735)Instruction limit reached! % 94.51/14.16 % (1110735)------------------------------ % 94.51/14.16 % (1110735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.16 % (1110735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.16 % (1110735)CaDiCaL version: 2.1.3 % 94.51/14.16 % (1110735)Termination reason: Instruction limit % 94.51/14.16 % (1110735)Termination phase: Saturation % 94.51/14.16 % (1110735)Time elapsed: 1.304 s % 94.51/14.16 % (1110735)Peak memory usage: 137 MB % 94.51/14.16 % (1110735)Instructions burned: 1997 (million) % 94.51/14.16 % (1110738)Instruction limit reached! % 94.51/14.16 % (1110738)------------------------------ % 94.51/14.16 % (1110738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.16 % (1110738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.16 % (1110738)CaDiCaL version: 2.1.3 % 94.51/14.16 % (1110738)Termination reason: Instruction limit % 94.51/14.16 % (1110738)Termination phase: Saturation % 94.51/14.16 % (1110738)Time elapsed: 1.073 s % 94.51/14.16 % (1110738)Peak memory usage: 137 MB % 94.51/14.16 % (1110738)Instructions burned: 2089 (million) % 94.51/14.16 % (1110742)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4160975352:i=433:bd=preordered_2942 on theBenchmark for (2942ds/433Mi) % 94.51/14.16 % (1110743)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3462542312:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2941 on theBenchmark for (2941ds/2942Mi) % 94.51/14.16 % (1110740)Instruction limit reached! % 94.51/14.16 % (1110740)------------------------------ % 94.51/14.16 % (1110740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.16 % (1110740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.16 % (1110740)CaDiCaL version: 2.1.3 % 94.51/14.16 % (1110740)Termination reason: Instruction limit % 94.51/14.16 % (1110740)Termination phase: Saturation % 94.51/14.16 % (1110740)Time elapsed: 0.358 s % 94.51/14.16 % (1110740)Peak memory usage: 103 MB % 94.51/14.16 % (1110740)Instructions burned: 1098 (million) % 94.51/14.16 % (1110742)Instruction limit reached! % 94.51/14.16 % (1110742)------------------------------ % 94.51/14.16 % (1110742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.16 % (1110742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.16 % (1110742)CaDiCaL version: 2.1.3 % 94.51/14.16 % (1110742)Termination reason: Instruction limit % 94.51/14.16 % (1110742)Termination phase: Saturation % 94.51/14.16 % (1110742)Time elapsed: 0.275 s % 94.51/14.16 % (1110742)Peak memory usage: 93 MB % 94.51/14.16 % (1110742)Instructions burned: 434 (million) % 94.51/14.16 % (1110746)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1058836531:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi) % 111.26/16.53 % (1110747)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=1077721066:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2938 on theBenchmark for (2938ds/596Mi) % 111.26/16.53 % (1110747)Instruction limit reached! % 111.26/16.53 % (1110747)------------------------------ % 111.26/16.53 % (1110747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.26/16.53 % (1110747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.26/16.53 % (1110747)CaDiCaL version: 2.1.3 % 111.26/16.53 % (1110747)Termination reason: Instruction limit % 111.26/16.53 % (1110747)Termination phase: Saturation % 111.26/16.53 % (1110747)Time elapsed: 0.315 s % 111.26/16.53 % (1110747)Peak memory usage: 99 MB % 111.26/16.53 % (1110747)Instructions burned: 597 (million) % 111.26/16.53 % (1110750)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=239063850:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2933 on theBenchmark for (2933ds/4123Mi) % 111.26/16.53 % (1110743)Instruction limit reached! % 111.26/16.53 % (1110743)------------------------------ % 111.26/16.53 % (1110743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.26/16.53 % (1110743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.26/16.53 % (1110743)CaDiCaL version: 2.1.3 % 111.26/16.53 % (1110743)Termination reason: Instruction limit % 111.26/16.53 % (1110743)Termination phase: Saturation % 111.26/16.53 % (1110743)Time elapsed: 1.929 s % 111.26/16.53 % (1110743)Peak memory usage: 146 MB % 111.26/16.53 % (1110743)Instructions burned: 2943 (million) % 111.26/16.53 % (1110752)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2336257420:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2921 on theBenchmark for (2921ds/16411Mi) % 111.26/16.53 % (1110746)Instruction limit reached! % 111.26/16.53 % (1110746)------------------------------ % 111.26/16.53 % (1110746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.26/16.53 % (1110746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.26/16.53 % (1110746)CaDiCaL version: 2.1.3 % 111.26/16.53 % (1110746)Termination reason: Instruction limit % 111.26/16.53 % (1110746)Termination phase: Saturation % 111.26/16.53 % (1110746)Time elapsed: 2.178 s % 111.26/16.53 % (1110746)Peak memory usage: 187 MB % 111.26/16.53 % (1110746)Instructions burned: 6923 (million) % 111.26/16.53 % (1110754)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=90810555:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2916 on theBenchmark for (2916ds/1670Mi) % 111.26/16.53 % (1110722)Instruction limit reached! % 111.26/16.53 % (1110722)------------------------------ % 111.26/16.53 % (1110722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.26/16.53 % (1110722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.26/16.53 % (1110722)CaDiCaL version: 2.1.3 % 111.26/16.53 % (1110722)Termination reason: Instruction limit % 111.26/16.53 % (1110722)Termination phase: Saturation % 111.26/16.53 % (1110722)Time elapsed: 6.812 s % 111.26/16.53 % (1110722)Peak memory usage: 162 MB % 111.26/16.53 % (1110722)Instructions burned: 10308 (million) % 111.26/16.53 % (1110756)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=2925022711:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2911 on theBenchmark for (2911ds/1722Mi) % 111.26/16.53 % (1110754)Instruction limit reached! % 111.26/16.53 % (1110754)------------------------------ % 111.26/16.53 % (1110754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.26/16.53 % (1110754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.26/16.53 % (1110754)CaDiCaL version: 2.1.3 % 111.26/16.53 % (1110754)Termination reason: Instruction limit % 111.26/16.53 % (1110754)Termination phase: Saturation % 111.26/16.53 % (1110754)Time elapsed: 0.572 s % 111.26/16.53 % (1110754)Peak memory usage: 136 MB % 111.26/16.53 % (1110754)Instructions burned: 1671 (million) % 111.26/16.53 % (1110758)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=2728249277:cts=off:cond=on:i=9530:bs=on:fsd=on_2909 on theBenchmark for (2909ds/9530Mi) % 136.33/20.06 % (1110750)Instruction limit reached! % 136.33/20.06 % (1110750)------------------------------ % 136.33/20.06 % (1110750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.33/20.06 % (1110750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.33/20.06 % (1110750)CaDiCaL version: 2.1.3 % 136.33/20.06 % (1110750)Termination reason: Instruction limit % 136.33/20.06 % (1110750)Termination phase: Saturation % 136.33/20.06 % (1110750)Time elapsed: 2.535 s % 136.33/20.06 % (1110750)Peak memory usage: 156 MB % 136.33/20.06 % (1110750)Instructions burned: 4123 (million) % 136.33/20.06 % (1110760)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1376868016:st=2:i=4495:sd=10:ss=included_2907 on theBenchmark for (2907ds/4495Mi) % 136.33/20.06 % (1110756)Instruction limit reached! % 136.33/20.06 % (1110756)------------------------------ % 136.33/20.06 % (1110756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.33/20.06 % (1110756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.33/20.06 % (1110756)CaDiCaL version: 2.1.3 % 136.33/20.06 % (1110756)Termination reason: Instruction limit % 136.33/20.06 % (1110756)Termination phase: Saturation % 136.33/20.06 % (1110756)Time elapsed: 1.085 s % 136.33/20.06 % (1110756)Peak memory usage: 134 MB % 136.33/20.06 % (1110756)Instructions burned: 1724 (million) % 136.33/20.06 % (1110762)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=2443717442:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2898 on theBenchmark for (2898ds/4920Mi) % 136.33/20.06 % (1110760)Instruction limit reached! % 136.33/20.06 % (1110760)------------------------------ % 136.33/20.06 % (1110760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.33/20.06 % (1110760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.33/20.06 % (1110760)CaDiCaL version: 2.1.3 % 136.33/20.06 % (1110760)Termination reason: Instruction limit % 136.33/20.06 % (1110760)Termination phase: Saturation % 136.33/20.06 % (1110760)Time elapsed: 2.439 s % 136.33/20.06 % (1110760)Peak memory usage: 162 MB % 136.33/20.06 % (1110760)Instructions burned: 4495 (million) % 136.33/20.06 % (1110764)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=2704129473:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2881 on theBenchmark for (2881ds/2083Mi) % 136.33/20.06 % (1110758)Instruction limit reached! % 136.33/20.06 % (1110758)------------------------------ % 136.33/20.06 % (1110758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.33/20.06 % (1110758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.33/20.06 % (1110758)CaDiCaL version: 2.1.3 % 136.33/20.06 % (1110758)Termination reason: Instruction limit % 136.33/20.06 % (1110758)Termination phase: Saturation % 136.33/20.06 % (1110758)Time elapsed: 3.349 s % 136.33/20.06 % (1110758)Peak memory usage: 171 MB % 136.33/20.06 % (1110758)Instructions burned: 9532 (million) % 136.33/20.06 % (1110766)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=3514126682:i=4629:av=off:gsp=on_2875 on theBenchmark for (2875ds/4629Mi) % 136.33/20.06 % (1110762)Instruction limit reached! % 136.33/20.06 % (1110762)------------------------------ % 136.33/20.06 % (1110762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.33/20.06 % (1110762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.33/20.06 % (1110762)CaDiCaL version: 2.1.3 % 136.33/20.06 % (1110762)Termination reason: Instruction limit % 136.33/20.06 % (1110762)Termination phase: Saturation % 136.33/20.06 % (1110762)Time elapsed: 2.881 s % 136.33/20.06 % (1110762)Peak memory usage: 149 MB % 136.33/20.06 % (1110762)Instructions burned: 4921 (million) % 136.33/20.06 % (1110768)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3397303476:i=1258:av=off_2868 on theBenchmark for (2868ds/1258Mi) % 136.33/20.06 % (1110764)Instruction limit reached! % 136.33/20.06 % (1110764)------------------------------ % 136.33/20.06 % (1110764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.33/20.06 % (1110764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.33/20.06 % (1110764)CaDiCaL version: 2.1.3 % 136.33/20.06 % (1110764)Termination reason: Instruction limit % 136.33/20.06 % (1110764)Termination phase: Saturation % 155.21/23.03 % (1110764)Time elapsed: 1.301 s % 155.21/23.03 % (1110764)Peak memory usage: 138 MB % 155.21/23.03 % (1110764)Instructions burned: 2083 (million) % 155.21/23.03 % (1110770)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2577510543:i=7343:av=off:ss=included_2866 on theBenchmark for (2866ds/7343Mi) % 155.21/23.03 % (1110768)Instruction limit reached! % 155.21/23.03 % (1110768)------------------------------ % 155.21/23.03 % (1110768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.21/23.03 % (1110768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.21/23.03 % (1110768)CaDiCaL version: 2.1.3 % 155.21/23.03 % (1110768)Termination reason: Instruction limit % 155.21/23.03 % (1110768)Termination phase: Saturation % 155.21/23.03 % (1110768)Time elapsed: 0.624 s % 155.21/23.03 % (1110768)Peak memory usage: 94 MB % 155.21/23.03 % (1110768)Instructions burned: 1260 (million) % 155.21/23.03 % (1110772)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1863476200:i=1325:sd=2:ss=axioms:sgt=16_2861 on theBenchmark for (2861ds/1325Mi) % 155.21/23.03 % (1110772)Refutation not found, incomplete strategy % 155.21/23.03 % (1110772)------------------------------ % 155.21/23.03 % (1110772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.21/23.03 % (1110772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.21/23.03 % (1110772)CaDiCaL version: 2.1.3 % 155.21/23.03 % (1110772)Termination reason: Refutation not found, incomplete strategy % 155.21/23.03 % (1110772)Time elapsed: 0.004 s % 155.21/23.03 % (1110772)Peak memory usage: 88 MB % 155.21/23.03 % (1110772)Instructions burned: 5 (million) % 155.21/23.03 % (1110766)Instruction limit reached! % 155.21/23.03 % (1110766)------------------------------ % 155.21/23.03 % (1110766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.21/23.03 % (1110766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.21/23.03 % (1110766)CaDiCaL version: 2.1.3 % 155.21/23.03 % (1110766)Termination reason: Instruction limit % 155.21/23.03 % (1110766)Termination phase: Saturation % 155.21/23.03 % (1110766)Time elapsed: 1.529 s % 155.21/23.03 % (1110766)Peak memory usage: 153 MB % 155.21/23.03 % (1110766)Instructions burned: 4630 (million) % 155.21/23.03 % (1110774)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=3006860829:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2859 on theBenchmark for (2859ds/2646Mi) % 155.21/23.03 % (1110772)------------------------------ % 155.21/23.03 % (1110772)------------------------------ % 155.21/23.03 % (1110776)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=177207578:i=1489:sd=2:ep=R:ss=axioms_2857 on theBenchmark for (2857ds/1489Mi) % 155.21/23.03 % (1110776)Instruction limit reached! % 155.21/23.03 % (1110776)------------------------------ % 155.21/23.03 % (1110776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.21/23.03 % (1110776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.21/23.03 % (1110776)CaDiCaL version: 2.1.3 % 155.21/23.03 % (1110776)Termination reason: Instruction limit % 155.21/23.03 % (1110776)Termination phase: Saturation % 155.21/23.03 % (1110776)Time elapsed: 0.576 s % 155.21/23.03 % (1110776)Peak memory usage: 134 MB % 155.21/23.03 % (1110776)Instructions burned: 1493 (million) % 155.21/23.03 % (1110778)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=2840171869:i=1503_2850 on theBenchmark for (2850ds/1503Mi) % 155.21/23.03 % (1110778)Instruction limit reached! % 155.21/23.03 % (1110778)------------------------------ % 155.21/23.03 % (1110778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.21/23.03 % (1110778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.21/23.03 % (1110778)CaDiCaL version: 2.1.3 % 155.21/23.03 % (1110778)Termination reason: Instruction limit % 155.21/23.03 % (1110778)Termination phase: Saturation % 155.21/23.03 % (1110778)Time elapsed: 0.559 s % 155.21/23.03 % (1110778)Peak memory usage: 135 MB % 155.21/23.03 % (1110778)Instructions burned: 1505 (million) % 155.21/23.03 % (1110774)Instruction limit reached! % 155.21/23.03 % (1110774)------------------------------ % 155.21/23.03 % (1110774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.21/23.03 % (1110774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.21/23.03 % (1110774)CaDiCaL version: 2.1.3 % 173.33/25.39 % (1110774)Termination reason: Instruction limit % 173.33/25.39 % (1110774)Termination phase: Saturation % 173.33/25.39 % (1110774)Time elapsed: 1.496 s % 173.33/25.39 % (1110774)Peak memory usage: 139 MB % 173.33/25.39 % (1110774)Instructions burned: 2646 (million) % 173.33/25.39 % (1110780)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3279352860:i=13942:kws=frequency_2843 on theBenchmark for (2843ds/13942Mi) % 173.33/25.39 % (1110781)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=2743499270:i=3604:fsr=off:er=filter_2843 on theBenchmark for (2843ds/3604Mi) % 173.33/25.39 % (1110770)Instruction limit reached! % 173.33/25.39 % (1110770)------------------------------ % 173.33/25.39 % (1110770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.33/25.39 % (1110770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.33/25.39 % (1110770)CaDiCaL version: 2.1.3 % 173.33/25.39 % (1110770)Termination reason: Instruction limit % 173.33/25.39 % (1110770)Termination phase: Saturation % 173.33/25.39 % (1110770)Time elapsed: 4.054 s % 173.33/25.39 % (1110770)Peak memory usage: 196 MB % 173.33/25.39 % (1110770)Instructions burned: 7344 (million) % 173.33/25.39 % (1110784)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1268336630:i=1876:sd=1:ss=included:sgt=32_2824 on theBenchmark for (2824ds/1876Mi) % 173.33/25.39 % (1110781)Instruction limit reached! % 173.33/25.39 % (1110781)------------------------------ % 173.33/25.39 % (1110781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.33/25.39 % (1110781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.33/25.39 % (1110781)CaDiCaL version: 2.1.3 % 173.33/25.39 % (1110781)Termination reason: Instruction limit % 173.33/25.39 % (1110781)Termination phase: Saturation % 173.33/25.39 % (1110781)Time elapsed: 2.134 s % 173.33/25.39 % (1110781)Peak memory usage: 152 MB % 173.33/25.39 % (1110781)Instructions burned: 3605 (million) % 173.33/25.39 % (1110786)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3418306917:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2820 on theBenchmark for (2820ds/1932Mi) % 173.33/25.39 % (1110752)Instruction limit reached! % 173.33/25.39 % (1110752)------------------------------ % 173.33/25.39 % (1110752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.33/25.39 % (1110752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.33/25.39 % (1110752)CaDiCaL version: 2.1.3 % 173.33/25.39 % (1110752)Termination reason: Instruction limit % 173.33/25.39 % (1110752)Termination phase: Saturation % 173.33/25.39 % (1110752)Time elapsed: 10.207 s % 173.33/25.39 % (1110752)Peak memory usage: 211 MB % 173.33/25.39 % (1110752)Instructions burned: 16412 (million) % 173.33/25.39 % (1110788)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=2712800990:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2817 on theBenchmark for (2817ds/1980Mi) % 173.33/25.39 % (1110784)Instruction limit reached! % 173.33/25.39 % (1110784)------------------------------ % 173.33/25.39 % (1110784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.33/25.39 % (1110784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.33/25.39 % (1110784)CaDiCaL version: 2.1.3 % 173.33/25.39 % (1110784)Termination reason: Instruction limit % 173.33/25.39 % (1110784)Termination phase: Saturation % 173.33/25.39 % (1110784)Time elapsed: 1.223 s % 173.33/25.39 % (1110784)Peak memory usage: 137 MB % 173.33/25.39 % (1110784)Instructions burned: 1877 (million) % 173.33/25.39 % (1110790)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=2794704435:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2811 on theBenchmark for (2811ds/3902Mi) % 173.33/25.39 % (1110786)Instruction limit reached! % 173.33/25.39 % (1110786)------------------------------ % 173.33/25.39 % (1110786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.33/25.39 % (1110786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.33/25.39 % (1110786)CaDiCaL version: 2.1.3 % 173.33/25.39 % (1110786)Termination reason: Instruction limit % 173.33/25.39 % (1110786)Termination phase: Saturation % 173.33/25.39 % (1110786)Time elapsed: 1.127 s % 173.33/25.39 % (1110786)Peak memory usage: 140 MB % 201.30/29.26 % (1110786)Instructions burned: 1933 (million) % 201.30/29.26 % (1110792)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2856668458:avsq=on:i=3916:aac=none:amm=off_2807 on theBenchmark for (2807ds/3916Mi) % 201.30/29.26 % (1110788)Instruction limit reached! % 201.30/29.26 % (1110788)------------------------------ % 201.30/29.26 % (1110788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.30/29.26 % (1110788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.30/29.26 % (1110788)CaDiCaL version: 2.1.3 % 201.30/29.26 % (1110788)Termination reason: Instruction limit % 201.30/29.26 % (1110788)Termination phase: Saturation % 201.30/29.26 % (1110788)Time elapsed: 1.254 s % 201.30/29.26 % (1110788)Peak memory usage: 138 MB % 201.30/29.26 % (1110788)Instructions burned: 1980 (million) % 201.30/29.26 % (1110794)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3125243622:cond=on:i=3940:av=off:er=known_2803 on theBenchmark for (2803ds/3940Mi) % 201.30/29.26 % (1110780)Instruction limit reached! % 201.30/29.26 % (1110780)------------------------------ % 201.30/29.26 % (1110780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.30/29.26 % (1110780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.30/29.26 % (1110780)CaDiCaL version: 2.1.3 % 201.30/29.26 % (1110780)Termination reason: Instruction limit % 201.30/29.26 % (1110780)Termination phase: Saturation % 201.30/29.26 % (1110780)Time elapsed: 4.972 s % 201.30/29.26 % (1110780)Peak memory usage: 242 MB % 201.30/29.26 % (1110780)Instructions burned: 13944 (million) % 201.30/29.26 % (1110796)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1641978742:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2793 on theBenchmark for (2793ds/3980Mi) % 201.30/29.26 % (1110790)Instruction limit reached! % 201.30/29.26 % (1110790)------------------------------ % 201.30/29.26 % (1110790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.30/29.26 % (1110790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.30/29.26 % (1110790)CaDiCaL version: 2.1.3 % 201.30/29.26 % (1110790)Termination reason: Instruction limit % 201.30/29.26 % (1110790)Termination phase: Saturation % 201.30/29.26 % (1110790)Time elapsed: 2.225 s % 201.30/29.26 % (1110790)Peak memory usage: 158 MB % 201.30/29.26 % (1110790)Instructions burned: 3902 (million) % 201.30/29.26 % (1110798)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=1390882285:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2787 on theBenchmark for (2787ds/2087Mi) % 201.30/29.26 % (1110792)Instruction limit reached! % 201.30/29.26 % (1110792)------------------------------ % 201.30/29.26 % (1110792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.30/29.26 % (1110792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.30/29.26 % (1110792)CaDiCaL version: 2.1.3 % 201.30/29.26 % (1110792)Termination reason: Instruction limit % 201.30/29.26 % (1110792)Termination phase: Saturation % 201.30/29.26 % (1110792)Time elapsed: 2.059 s % 201.30/29.26 % (1110792)Peak memory usage: 110 MB % 201.30/29.26 % (1110792)Instructions burned: 3917 (million) % 201.30/29.26 % (1110800)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=2474341757:cts=off:cond=on:i=4272:bs=on:fsd=on_2785 on theBenchmark for (2785ds/4272Mi) % 201.30/29.26 % (1110794)Instruction limit reached! % 201.30/29.26 % (1110794)------------------------------ % 201.30/29.26 % (1110794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.30/29.26 % (1110794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.30/29.26 % (1110794)CaDiCaL version: 2.1.3 % 201.30/29.26 % (1110794)Termination reason: Instruction limit % 201.30/29.26 % (1110794)Termination phase: Saturation % 201.30/29.26 % (1110794)Time elapsed: 2.396 s % 201.30/29.26 % (1110794)Peak memory usage: 152 MB % 201.30/29.26 % (1110794)Instructions burned: 3940 (million) % 201.30/29.26 % (1110796)Instruction limit reached! % 201.30/29.26 % (1110796)------------------------------ % 201.30/29.26 % (1110796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.30/29.26 % (1110796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.16/37.52 % (1110796)CaDiCaL version: 2.1.3 % 260.16/37.52 % (1110796)Termination reason: Instruction limit % 260.16/37.52 % (1110796)Termination phase: Saturation % 260.16/37.52 % (1110796)Time elapsed: 1.407 s % 260.16/37.52 % (1110796)Peak memory usage: 152 MB % 260.16/37.52 % (1110796)Instructions burned: 3980 (million) % 260.16/37.52 % (1110802)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=7429307:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2778 on theBenchmark for (2778ds/2197Mi) % 260.16/37.52 % (1110803)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2323387080:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2778 on theBenchmark for (2778ds/6508Mi) % 260.16/37.52 % (1110798)Instruction limit reached! % 260.16/37.52 % (1110798)------------------------------ % 260.16/37.52 % (1110798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.16/37.52 % (1110798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.16/37.52 % (1110798)CaDiCaL version: 2.1.3 % 260.16/37.52 % (1110798)Termination reason: Instruction limit % 260.16/37.52 % (1110798)Termination phase: Saturation % 260.16/37.52 % (1110798)Time elapsed: 1.369 s % 260.16/37.52 % (1110798)Peak memory usage: 139 MB % 260.16/37.52 % (1110798)Instructions burned: 2087 (million) % 260.16/37.52 % (1110806)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=492640555:i=2330:fgj=on:av=off:fsr=off_2772 on theBenchmark for (2772ds/2330Mi) % 260.16/37.52 % (1110802)Instruction limit reached! % 260.16/37.52 % (1110802)------------------------------ % 260.16/37.52 % (1110802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.16/37.52 % (1110802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.16/37.52 % (1110802)CaDiCaL version: 2.1.3 % 260.16/37.52 % (1110802)Termination reason: Instruction limit % 260.16/37.52 % (1110802)Termination phase: Saturation % 260.16/37.52 % (1110802)Time elapsed: 1.284 s % 260.16/37.52 % (1110802)Peak memory usage: 142 MB % 260.16/37.52 % (1110802)Instructions burned: 2198 (million) % 260.16/37.52 % (1110808)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=4013813982:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2764 on theBenchmark for (2764ds/7592Mi) % 260.16/37.52 % (1110803)Instruction limit reached! % 260.16/37.52 % (1110803)------------------------------ % 260.16/37.52 % (1110803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.16/37.52 % (1110803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.16/37.52 % (1110803)CaDiCaL version: 2.1.3 % 260.16/37.52 % (1110803)Termination reason: Instruction limit % 260.16/37.52 % (1110803)Termination phase: Saturation % 260.16/37.52 % (1110803)Time elapsed: 1.966 s % 260.16/37.52 % (1110803)Peak memory usage: 128 MB % 260.16/37.52 % (1110803)Instructions burned: 6509 (million) % 260.16/37.52 % (1110806)Instruction limit reached! % 260.16/37.52 % (1110806)------------------------------ % 260.16/37.52 % (1110806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.16/37.52 % (1110806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.16/37.52 % (1110806)CaDiCaL version: 2.1.3 % 260.16/37.52 % (1110806)Termination reason: Instruction limit % 260.16/37.52 % (1110806)Termination phase: Saturation % 260.16/37.52 % (1110806)Time elapsed: 1.416 s % 260.16/37.52 % (1110806)Peak memory usage: 138 MB % 260.16/37.52 % (1110806)Instructions burned: 2330 (million) % 260.16/37.52 % (1110810)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=1296285082:i=2693:kws=precedence:ins=1:av=off_2757 on theBenchmark for (2757ds/2693Mi) % 260.16/37.52 % (1110800)Instruction limit reached! % 260.16/37.52 % (1110800)------------------------------ % 260.16/37.52 % (1110800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.16/37.52 % (1110800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.16/37.52 % (1110800)CaDiCaL version: 2.1.3 % 260.16/37.52 % (1110800)Termination reason: Instruction limit % 260.16/37.52 % (1110800)Termination phase: Saturation % 260.16/37.52 % (1110800)Time elapsed: 2.865 s % 260.16/37.52 % (1110800)Peak memory usage: 153 MB % 260.16/37.52 % (1110800)Instructions burned: 4272 (million) % 260.16/37.52 % (1110811)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=1373639132:i=28651:sd=4:ss=included:sgt=64_2756 on theBenchmark for (2756ds/28651Mi) % 260.16/37.52 % (1110813)lrs-1010_1_ncem=casc2026/models/loop5.pt:sTerminated %------------------------------------------------------------------------------