%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM177-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 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:11:52 PM UTC 2026 % Result : Timeout 300.14s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM177-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.37 % Computer : n016.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sun Sep 27 19:10:17 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.41 Running first-order theorem proving % 0.11/0.41 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 % 9.75/2.24 % (2935956)Input is clausal, will run a generic CNF schedule. % 9.75/2.24 % (2935964)lrs+10_1_sil=8000:sp=occurrence:random_seed=2513642671:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.75/2.24 % (2935961)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=1327685529:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.75/2.24 % (2935965)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=86861988:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.75/2.24 % (2935963)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1049700414:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.75/2.24 % (2935967)dis-21_1_sil=8000:lcm=predicate:random_seed=2666451105: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.75/2.24 % (2935962)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2036375013:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.75/2.24 % (2935966)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=384831079:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.75/2.24 % (2935964)Instruction limit reached! % 9.75/2.24 % (2935964)------------------------------ % 9.75/2.24 % (2935964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.24 % (2935964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.24 % (2935964)CaDiCaL version: 2.1.3 % 9.75/2.24 % (2935964)Termination reason: Instruction limit % 9.75/2.24 % (2935964)Termination phase: Saturation % 9.75/2.24 % (2935964)Time elapsed: 0.042 s % 9.75/2.24 % (2935964)Peak memory usage: 90 MB % 9.75/2.24 % (2935964)Instructions burned: 109 (million) % 9.75/2.24 % (2935965)Instruction limit reached! % 9.75/2.24 % (2935965)------------------------------ % 9.75/2.24 % (2935965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.24 % (2935965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.24 % (2935965)CaDiCaL version: 2.1.3 % 9.75/2.24 % (2935965)Termination reason: Instruction limit % 9.75/2.24 % (2935965)Termination phase: Saturation % 9.75/2.24 % (2935965)Time elapsed: 0.071 s % 9.75/2.24 % (2935965)Peak memory usage: 88 MB % 9.75/2.24 % (2935965)Instructions burned: 115 (million) % 9.75/2.24 % (2935967)Instruction limit reached! % 9.75/2.24 % (2935967)------------------------------ % 9.75/2.24 % (2935967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.24 % (2935967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.24 % (2935967)CaDiCaL version: 2.1.3 % 9.75/2.24 % (2935967)Termination reason: Instruction limit % 9.75/2.24 % (2935967)Termination phase: Saturation % 9.75/2.24 % (2935967)Time elapsed: 0.072 s % 9.75/2.24 % (2935967)Peak memory usage: 89 MB % 9.75/2.24 % (2935967)Instructions burned: 118 (million) % 9.75/2.24 % (2935975)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=1633973638:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 9.75/2.24 % (2935975)Refutation not found, incomplete strategy % 9.75/2.24 % (2935975)------------------------------ % 9.75/2.24 % (2935975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.24 % (2935975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.24 % (2935975)CaDiCaL version: 2.1.3 % 9.75/2.24 % (2935975)Termination reason: Refutation not found, incomplete strategy % 9.75/2.24 % (2935975)Time elapsed: 0.002 s % 9.75/2.24 % (2935975)Peak memory usage: 88 MB % 9.75/2.24 % (2935975)Instructions burned: 4 (million) % 9.75/2.24 % (2935966)Instruction limit reached! % 9.75/2.24 % (2935966)------------------------------ % 9.75/2.24 % (2935966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.75/2.24 % (2935966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.75/2.24 % (2935966)CaDiCaL version: 2.1.3 % 9.75/2.24 % (2935966)Termination reason: Instruction limit % 9.75/2.24 % (2935966)Termination phase: Saturation % 9.75/2.24 % (2935966)Time elapsed: 0.142 s % 9.75/2.24 % (2935966)Peak memory usage: 90 MB % 9.75/2.24 % (2935966)Instructions burned: 181 (million) % 9.75/2.24 % (2935977)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1662803991:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 19.77/3.76 % (2935976)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1988058422:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 19.77/3.76 % (2935975)------------------------------ % 19.77/3.76 % (2935975)------------------------------ % 19.77/3.76 % (2935979)lrs+10_64_to=lpo:sil=8000:random_seed=2549763538:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 19.77/3.76 % (2935976)Instruction limit reached! % 19.77/3.76 % (2935976)------------------------------ % 19.77/3.76 % (2935976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.77/3.76 % (2935976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.77/3.76 % (2935976)CaDiCaL version: 2.1.3 % 19.77/3.76 % (2935976)Termination reason: Instruction limit % 19.77/3.76 % (2935976)Termination phase: Saturation % 19.77/3.76 % (2935976)Time elapsed: 0.094 s % 19.77/3.76 % (2935976)Peak memory usage: 90 MB % 19.77/3.76 % (2935976)Instructions burned: 190 (million) % 19.77/3.76 % (2935977)Instruction limit reached! % 19.77/3.76 % (2935977)------------------------------ % 19.77/3.76 % (2935977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.77/3.76 % (2935977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.77/3.76 % (2935977)CaDiCaL version: 2.1.3 % 19.77/3.76 % (2935977)Termination reason: Instruction limit % 19.77/3.76 % (2935977)Termination phase: Saturation % 19.77/3.76 % (2935977)Time elapsed: 0.130 s % 19.77/3.76 % (2935977)Peak memory usage: 89 MB % 19.77/3.76 % (2935977)Instructions burned: 219 (million) % 19.77/3.76 % (2935982)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3366829338:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 19.77/3.76 % (2935979)Instruction limit reached! % 19.77/3.76 % (2935979)------------------------------ % 19.77/3.76 % (2935979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.77/3.76 % (2935979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.77/3.76 % (2935979)CaDiCaL version: 2.1.3 % 19.77/3.76 % (2935979)Termination reason: Instruction limit % 19.77/3.76 % (2935979)Termination phase: Saturation % 19.77/3.76 % (2935979)Time elapsed: 0.081 s % 19.77/3.76 % (2935979)Peak memory usage: 89 MB % 19.77/3.76 % (2935979)Instructions burned: 126 (million) % 19.77/3.76 % (2935982)Instruction limit reached! % 19.77/3.76 % (2935982)------------------------------ % 19.77/3.76 % (2935982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.77/3.76 % (2935982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.77/3.76 % (2935982)CaDiCaL version: 2.1.3 % 19.77/3.76 % (2935982)Termination reason: Instruction limit % 19.77/3.76 % (2935982)Termination phase: Saturation % 19.77/3.76 % (2935982)Time elapsed: 0.050 s % 19.77/3.76 % (2935982)Peak memory usage: 90 MB % 19.77/3.76 % (2935982)Instructions burned: 195 (million) % 19.77/3.76 % (2935984)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3131969541:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 19.77/3.76 % (2935985)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1393247513:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 19.77/3.76 % (2935987)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=479938080:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 19.77/3.76 % (2935988)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2744737422:i=107_2993 on theBenchmark for (2993ds/107Mi) % 19.77/3.76 % (2935984)Instruction limit reached! % 19.77/3.76 % (2935984)------------------------------ % 19.77/3.76 % (2935984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.77/3.76 % (2935984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.77/3.76 % (2935984)CaDiCaL version: 2.1.3 % 19.77/3.76 % (2935984)Termination reason: Instruction limit % 19.77/3.76 % (2935984)Termination phase: Saturation % 19.77/3.76 % (2935984)Time elapsed: 0.114 s % 19.77/3.76 % (2935984)Peak memory usage: 91 MB % 19.77/3.76 % (2935984)Instructions burned: 158 (million) % 19.77/3.76 % (2935988)Instruction limit reached! % 19.77/3.76 % (2935988)------------------------------ % 28.85/5.03 % (2935988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.85/5.03 % (2935988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.85/5.03 % (2935988)CaDiCaL version: 2.1.3 % 28.85/5.03 % (2935988)Termination reason: Instruction limit % 28.85/5.03 % (2935988)Termination phase: Saturation % 28.85/5.03 % (2935988)Time elapsed: 0.041 s % 28.85/5.03 % (2935988)Peak memory usage: 89 MB % 28.85/5.03 % (2935988)Instructions burned: 109 (million) % 28.85/5.03 % (2935987)Instruction limit reached! % 28.85/5.03 % (2935987)------------------------------ % 28.85/5.03 % (2935987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.85/5.03 % (2935987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.85/5.03 % (2935987)CaDiCaL version: 2.1.3 % 28.85/5.03 % (2935987)Termination reason: Instruction limit % 28.85/5.03 % (2935987)Termination phase: Saturation % 28.85/5.03 % (2935987)Time elapsed: 0.066 s % 28.85/5.03 % (2935987)Peak memory usage: 90 MB % 28.85/5.03 % (2935987)Instructions burned: 108 (million) % 28.85/5.03 % (2935993)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1904896576:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 28.85/5.03 % (2935994)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3981856517:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 28.85/5.03 % (2935995)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=18878068:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi) % 28.85/5.03 % (2935993)Instruction limit reached! % 28.85/5.03 % (2935993)------------------------------ % 28.85/5.03 % (2935993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.85/5.03 % (2935993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.85/5.03 % (2935993)CaDiCaL version: 2.1.3 % 28.85/5.03 % (2935993)Termination reason: Instruction limit % 28.85/5.03 % (2935993)Termination phase: Saturation % 28.85/5.03 % (2935993)Time elapsed: 0.088 s % 28.85/5.03 % (2935993)Peak memory usage: 90 MB % 28.85/5.03 % (2935993)Instructions burned: 244 (million) % 28.85/5.03 % (2935995)Instruction limit reached! % 28.85/5.03 % (2935995)------------------------------ % 28.85/5.03 % (2935995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.85/5.03 % (2935995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.85/5.03 % (2935995)CaDiCaL version: 2.1.3 % 28.85/5.03 % (2935995)Termination reason: Instruction limit % 28.85/5.03 % (2935995)Termination phase: Saturation % 28.85/5.03 % (2935995)Time elapsed: 0.051 s % 28.85/5.03 % (2935995)Peak memory usage: 88 MB % 28.85/5.03 % (2935995)Instructions burned: 134 (million) % 28.85/5.03 % (2935999)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=748950118:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 28.85/5.03 % (2936000)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=549861015:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi) % 28.85/5.03 % (2936000)Instruction limit reached! % 28.85/5.03 % (2936000)------------------------------ % 28.85/5.03 % (2936000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.85/5.03 % (2935999)Instruction limit reached! % 28.85/5.03 % (2935999)------------------------------ % 28.85/5.03 % (2935999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.85/5.03 % (2935999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.85/5.03 % (2935999)CaDiCaL version: 2.1.3 % 28.85/5.03 % (2935999)Termination reason: Instruction limit % 28.85/5.03 % (2935999)Termination phase: Saturation % 28.85/5.03 % (2935999)Time elapsed: 0.167 s % 28.85/5.03 % (2935999)Peak memory usage: 95 MB % 28.85/5.03 % (2935999)Instructions burned: 500 (million) % 28.85/5.03 % (2936000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.85/5.03 % (2936000)CaDiCaL version: 2.1.3 % 28.85/5.03 % (2936000)Termination reason: Instruction limit % 28.85/5.03 % (2936000)Termination phase: Saturation % 28.85/5.03 % (2936000)Time elapsed: 0.111 s % 28.85/5.03 % (2936000)Peak memory usage: 89 MB % 28.85/5.03 % (2936000)Instructions burned: 192 (million) % 28.85/5.03 % (2936004)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3509430247:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi) % 45.23/7.29 % (2936003)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2125567486:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi) % 45.23/7.29 % (2936004)Instruction limit reached! % 45.23/7.29 % (2936004)------------------------------ % 45.23/7.29 % (2936004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.23/7.29 % (2936004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.23/7.29 % (2936004)CaDiCaL version: 2.1.3 % 45.23/7.29 % (2936004)Termination reason: Instruction limit % 45.23/7.29 % (2936004)Termination phase: Saturation % 45.23/7.29 % (2936004)Time elapsed: 0.050 s % 45.23/7.29 % (2936004)Peak memory usage: 89 MB % 45.23/7.29 % (2936004)Instructions burned: 159 (million) % 45.23/7.29 % (2936003)Instruction limit reached! % 45.23/7.29 % (2936003)------------------------------ % 45.23/7.29 % (2936003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.23/7.29 % (2936003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.23/7.29 % (2936003)CaDiCaL version: 2.1.3 % 45.23/7.29 % (2936003)Termination reason: Instruction limit % 45.23/7.29 % (2936003)Termination phase: Saturation % 45.23/7.29 % (2936003)Time elapsed: 0.166 s % 45.23/7.29 % (2936003)Peak memory usage: 92 MB % 45.23/7.29 % (2936003)Instructions burned: 265 (million) % 45.23/7.29 % (2936007)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=537885622:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi) % 45.23/7.29 % (2936008)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3062248212:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi) % 45.23/7.29 % (2936008)Instruction limit reached! % 45.23/7.29 % (2936008)------------------------------ % 45.23/7.29 % (2936008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.23/7.29 % (2936008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.23/7.29 % (2936008)CaDiCaL version: 2.1.3 % 45.23/7.29 % (2936008)Termination reason: Instruction limit % 45.23/7.29 % (2936008)Termination phase: Saturation % 45.23/7.29 % (2936008)Time elapsed: 0.205 s % 45.23/7.29 % (2936008)Peak memory usage: 88 MB % 45.23/7.29 % (2936008)Instructions burned: 538 (million) % 45.23/7.29 % (2936011)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=823319397:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi) % 45.23/7.29 % (2936011)Instruction limit reached! % 45.23/7.29 % (2936011)------------------------------ % 45.23/7.29 % (2936011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.23/7.29 % (2936011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.23/7.29 % (2936011)CaDiCaL version: 2.1.3 % 45.23/7.29 % (2936011)Termination reason: Instruction limit % 45.23/7.29 % (2936011)Termination phase: Saturation % 45.23/7.29 % (2936011)Time elapsed: 0.092 s % 45.23/7.29 % (2936011)Peak memory usage: 90 MB % 45.23/7.29 % (2936011)Instructions burned: 180 (million) % 45.23/7.29 % (2936013)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=1502203485:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi) % 45.23/7.29 % (2935985)Instruction limit reached! % 45.23/7.29 % (2935985)------------------------------ % 45.23/7.29 % (2935985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.23/7.29 % (2935985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.23/7.29 % (2935985)CaDiCaL version: 2.1.3 % 45.23/7.29 % (2935985)Termination reason: Instruction limit % 45.23/7.29 % (2935985)Termination phase: Saturation % 45.23/7.29 % (2935985)Time elapsed: 2.012 s % 45.23/7.29 % (2935985)Peak memory usage: 145 MB % 45.23/7.29 % (2935985)Instructions burned: 3395 (million) % 45.23/7.29 % (2936015)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=904899234:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi) % 45.23/7.29 % (2935994)Instruction limit reached! % 45.23/7.29 % (2935994)------------------------------ % 45.23/7.29 % (2935994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.23/7.29 % (2935994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.23/7.29 % (2935994)CaDiCaL version: 2.1.3 % 71.06/10.97 % (2935994)Termination reason: Instruction limit % 71.06/10.97 % (2935994)Termination phase: Saturation % 71.06/10.97 % (2935994)Time elapsed: 1.980 s % 71.06/10.97 % (2935994)Peak memory usage: 156 MB % 71.06/10.97 % (2935994)Instructions burned: 5210 (million) % 71.06/10.97 % (2936017)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=1776655818:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi) % 71.06/10.97 % (2936015)Instruction limit reached! % 71.06/10.97 % (2936015)------------------------------ % 71.06/10.97 % (2936015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.06/10.97 % (2936015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.06/10.97 % (2936015)CaDiCaL version: 2.1.3 % 71.06/10.97 % (2936015)Termination reason: Instruction limit % 71.06/10.97 % (2936015)Termination phase: Saturation % 71.06/10.97 % (2936015)Time elapsed: 0.189 s % 71.06/10.97 % (2936015)Peak memory usage: 90 MB % 71.06/10.97 % (2936015)Instructions burned: 415 (million) % 71.06/10.97 % (2936019)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=3530363749:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi) % 71.06/10.97 % (2936019)Instruction limit reached! % 71.06/10.97 % (2936019)------------------------------ % 71.06/10.97 % (2936019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.06/10.97 % (2936019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.06/10.97 % (2936019)CaDiCaL version: 2.1.3 % 71.06/10.97 % (2936019)Termination reason: Instruction limit % 71.06/10.97 % (2936019)Termination phase: Saturation % 71.06/10.97 % (2936019)Time elapsed: 0.111 s % 71.06/10.97 % (2936019)Peak memory usage: 88 MB % 71.06/10.97 % (2936019)Instructions burned: 304 (million) % 71.06/10.97 % (2936007)Instruction limit reached! % 71.06/10.97 % (2936007)------------------------------ % 71.06/10.97 % (2936007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.06/10.97 % (2936007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.06/10.97 % (2936007)CaDiCaL version: 2.1.3 % 71.06/10.97 % (2936007)Termination reason: Instruction limit % 71.06/10.97 % (2936007)Termination phase: Saturation % 71.06/10.97 % (2936007)Time elapsed: 1.885 s % 71.06/10.97 % (2936007)Peak memory usage: 150 MB % 71.06/10.97 % (2936007)Instructions burned: 3258 (million) % 71.06/10.97 % (2936021)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1958714115:st=4:i=720:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/720Mi) % 71.06/10.97 % (2936022)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3844492072:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi) % 71.06/10.97 % (2936021)Instruction limit reached! % 71.06/10.97 % (2936021)------------------------------ % 71.06/10.97 % (2936021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.06/10.97 % (2936021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.06/10.97 % (2936021)CaDiCaL version: 2.1.3 % 71.06/10.97 % (2936021)Termination reason: Instruction limit % 71.06/10.97 % (2936021)Termination phase: Saturation % 71.06/10.97 % (2936021)Time elapsed: 0.381 s % 71.06/10.97 % (2936021)Peak memory usage: 97 MB % 71.06/10.97 % (2936021)Instructions burned: 721 (million) % 71.06/10.97 % (2936022)Instruction limit reached! % 71.06/10.97 % (2936022)------------------------------ % 71.06/10.97 % (2936022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.06/10.97 % (2936022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.06/10.97 % (2936022)CaDiCaL version: 2.1.3 % 71.06/10.97 % (2936022)Termination reason: Instruction limit % 71.06/10.97 % (2936022)Termination phase: Saturation % 71.06/10.97 % (2936022)Time elapsed: 0.345 s % 71.06/10.97 % (2936022)Peak memory usage: 95 MB % 71.06/10.97 % (2936022)Instructions burned: 599 (million) % 71.06/10.97 % (2936025)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3565875992:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi) % 71.06/10.97 % (2936026)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=2661574598:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2959 on theBenchmark for (2959ds/1997Mi) % 95.11/14.85 % (2936017)Instruction limit reached! % 95.11/14.85 % (2936017)------------------------------ % 95.11/14.85 % (2936017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.11/14.85 % (2936017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.11/14.85 % (2936017)CaDiCaL version: 2.1.3 % 95.11/14.85 % (2936017)Termination reason: Instruction limit % 95.11/14.85 % (2936017)Termination phase: Saturation % 95.11/14.85 % (2936017)Time elapsed: 2.115 s % 95.11/14.85 % (2936017)Peak memory usage: 169 MB % 95.11/14.85 % (2936017)Instructions burned: 8481 (million) % 95.11/14.85 % (2936029)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=3258553033:i=2088:bd=preordered:av=off_2948 on theBenchmark for (2948ds/2088Mi) % 95.11/14.85 % (2936026)Instruction limit reached! % 95.11/14.85 % (2936026)------------------------------ % 95.11/14.85 % (2936026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.11/14.85 % (2936026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.11/14.85 % (2936026)CaDiCaL version: 2.1.3 % 95.11/14.85 % (2936026)Termination reason: Instruction limit % 95.11/14.85 % (2936026)Termination phase: Saturation % 95.11/14.85 % (2936026)Time elapsed: 1.318 s % 95.11/14.85 % (2936026)Peak memory usage: 138 MB % 95.11/14.85 % (2936026)Instructions burned: 1997 (million) % 95.11/14.85 % (2936031)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2779194023:i=1098:nicw=on_2945 on theBenchmark for (2945ds/1098Mi) % 95.11/14.85 % (2936025)Instruction limit reached! % 95.11/14.85 % (2936025)------------------------------ % 95.11/14.85 % (2936025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.11/14.85 % (2936025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.11/14.85 % (2936025)CaDiCaL version: 2.1.3 % 95.11/14.85 % (2936025)Termination reason: Instruction limit % 95.11/14.85 % (2936025)Termination phase: Saturation % 95.11/14.85 % (2936025)Time elapsed: 1.789 s % 95.11/14.85 % (2936025)Peak memory usage: 141 MB % 95.11/14.85 % (2936025)Instructions burned: 2990 (million) % 95.11/14.85 % (2936033)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1910060002:i=433:bd=preordered_2941 on theBenchmark for (2941ds/433Mi) % 95.11/14.85 % (2936029)Instruction limit reached! % 95.11/14.85 % (2936029)------------------------------ % 95.11/14.85 % (2936029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.11/14.85 % (2936029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.11/14.85 % (2936029)CaDiCaL version: 2.1.3 % 95.11/14.85 % (2936029)Termination reason: Instruction limit % 95.11/14.85 % (2936029)Termination phase: Saturation % 95.11/14.85 % (2936029)Time elapsed: 0.730 s % 95.11/14.85 % (2936029)Peak memory usage: 138 MB % 95.11/14.85 % (2936029)Instructions burned: 2089 (million) % 95.11/14.85 % (2936035)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4066568094:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2939 on theBenchmark for (2939ds/2942Mi) % 95.11/14.85 % (2936033)Instruction limit reached! % 95.11/14.85 % (2936033)------------------------------ % 95.11/14.85 % (2936033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.11/14.85 % (2936033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.11/14.85 % (2936033)CaDiCaL version: 2.1.3 % 95.11/14.85 % (2936033)Termination reason: Instruction limit % 95.11/14.85 % (2936033)Termination phase: Saturation % 95.11/14.85 % (2936033)Time elapsed: 0.262 s % 95.11/14.85 % (2936033)Peak memory usage: 94 MB % 95.11/14.85 % (2936033)Instructions burned: 434 (million) % 95.11/14.85 % (2936031)Instruction limit reached! % 95.11/14.85 % (2936031)------------------------------ % 95.11/14.85 % (2936031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.11/14.85 % (2936031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.11/14.85 % (2936031)CaDiCaL version: 2.1.3 % 95.11/14.85 % (2936031)Termination reason: Instruction limit % 95.11/14.85 % (2936031)Termination phase: Saturation % 95.11/14.85 % (2936031)Time elapsed: 0.673 s % 95.11/14.85 % (2936031)Peak memory usage: 102 MB % 95.11/14.85 % (2936031)Instructions burned: 1099 (million) % 95.11/14.85 % (2936037)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=646547149:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2937 on theBenchmark for (2937ds/6922Mi) % 117.50/17.44 % (2936038)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=2907744340:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2936 on theBenchmark for (2936ds/596Mi) % 117.50/17.44 % (2936038)Instruction limit reached! % 117.50/17.44 % (2936038)------------------------------ % 117.50/17.44 % (2936038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.50/17.44 % (2936038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/17.44 % (2936038)CaDiCaL version: 2.1.3 % 117.50/17.44 % (2936038)Termination reason: Instruction limit % 117.50/17.44 % (2936038)Termination phase: Saturation % 117.50/17.44 % (2936038)Time elapsed: 0.321 s % 117.50/17.44 % (2936038)Peak memory usage: 98 MB % 117.50/17.44 % (2936038)Instructions burned: 597 (million) % 117.50/17.44 % (2936041)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=1472086729:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2931 on theBenchmark for (2931ds/4123Mi) % 117.50/17.44 % (2936035)Instruction limit reached! % 117.50/17.44 % (2936035)------------------------------ % 117.50/17.44 % (2936035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.50/17.44 % (2936035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/17.44 % (2936035)CaDiCaL version: 2.1.3 % 117.50/17.44 % (2936035)Termination reason: Instruction limit % 117.50/17.44 % (2936035)Termination phase: Saturation % 117.50/17.44 % (2936035)Time elapsed: 1.061 s % 117.50/17.44 % (2936035)Peak memory usage: 143 MB % 117.50/17.44 % (2936035)Instructions burned: 2945 (million) % 117.50/17.44 % (2936043)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2794625075:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2927 on theBenchmark for (2927ds/16411Mi) % 117.50/17.44 % (2936013)Instruction limit reached! % 117.50/17.44 % (2936013)------------------------------ % 117.50/17.44 % (2936013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.50/17.44 % (2936013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/17.44 % (2936013)CaDiCaL version: 2.1.3 % 117.50/17.44 % (2936013)Termination reason: Instruction limit % 117.50/17.44 % (2936013)Termination phase: Saturation % 117.50/17.44 % (2936013)Time elapsed: 6.444 s % 117.50/17.44 % (2936013)Peak memory usage: 160 MB % 117.50/17.44 % (2936013)Instructions burned: 10308 (million) % 117.50/17.44 % (2936045)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2985675059:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2911 on theBenchmark for (2911ds/1670Mi) % 117.50/17.44 % (2936041)Instruction limit reached! % 117.50/17.44 % (2936041)------------------------------ % 117.50/17.44 % (2936041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.50/17.44 % (2936041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/17.44 % (2936041)CaDiCaL version: 2.1.3 % 117.50/17.44 % (2936041)Termination reason: Instruction limit % 117.50/17.44 % (2936041)Termination phase: Saturation % 117.50/17.44 % (2936041)Time elapsed: 2.559 s % 117.50/17.44 % (2936041)Peak memory usage: 154 MB % 117.50/17.44 % (2936041)Instructions burned: 4123 (million) % 117.50/17.44 % (2936047)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=4038978342:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2904 on theBenchmark for (2904ds/1722Mi) % 117.50/17.44 % (2936045)Instruction limit reached! % 117.50/17.44 % (2936045)------------------------------ % 117.50/17.44 % (2936045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.50/17.44 % (2936045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.50/17.44 % (2936045)CaDiCaL version: 2.1.3 % 117.50/17.44 % (2936045)Termination reason: Instruction limit % 117.50/17.44 % (2936045)Termination phase: Saturation % 117.50/17.44 % (2936045)Time elapsed: 1.042 s % 117.50/17.44 % (2936045)Peak memory usage: 137 MB % 117.50/17.44 % (2936045)Instructions burned: 1670 (million) % 117.50/17.44 % (2936037)Instruction limit reached! % 117.50/17.44 % (2936037)------------------------------ % 117.50/17.44 % (2936037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.50/17.44 % (2936037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.97/19.60 % (2936037)CaDiCaL version: 2.1.3 % 131.97/19.60 % (2936037)Termination reason: Instruction limit % 131.97/19.60 % (2936037)Termination phase: Saturation % 131.97/19.60 % (2936037)Time elapsed: 3.679 s % 131.97/19.60 % (2936037)Peak memory usage: 185 MB % 131.97/19.60 % (2936037)Instructions burned: 6923 (million) % 131.97/19.60 % (2936049)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=1207674215:cts=off:cond=on:i=9530:bs=on:fsd=on_2899 on theBenchmark for (2899ds/9530Mi) % 131.97/19.60 % (2936050)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2857861131:st=2:i=4495:sd=10:ss=included_2898 on theBenchmark for (2898ds/4495Mi) % 131.97/19.60 % (2936047)Instruction limit reached! % 131.97/19.60 % (2936047)------------------------------ % 131.97/19.60 % (2936047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.97/19.60 % (2936047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.97/19.60 % (2936047)CaDiCaL version: 2.1.3 % 131.97/19.60 % (2936047)Termination reason: Instruction limit % 131.97/19.60 % (2936047)Termination phase: Saturation % 131.97/19.60 % (2936047)Time elapsed: 0.954 s % 131.97/19.60 % (2936047)Peak memory usage: 130 MB % 131.97/19.60 % (2936047)Instructions burned: 1725 (million) % 131.97/19.60 % (2936053)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=747020431:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2893 on theBenchmark for (2893ds/4920Mi) % 131.97/19.60 % (2936043)Instruction limit reached! % 131.97/19.60 % (2936043)------------------------------ % 131.97/19.60 % (2936043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.97/19.60 % (2936043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.97/19.60 % (2936043)CaDiCaL version: 2.1.3 % 131.97/19.60 % (2936043)Termination reason: Instruction limit % 131.97/19.60 % (2936043)Termination phase: Saturation % 131.97/19.60 % (2936043)Time elapsed: 5.668 s % 131.97/19.60 % (2936043)Peak memory usage: 216 MB % 131.97/19.60 % (2936043)Instructions burned: 16411 (million) % 131.97/19.60 % (2936055)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=1352271570:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2869 on theBenchmark for (2869ds/2083Mi) % 131.97/19.60 % (2936050)Instruction limit reached! % 131.97/19.60 % (2936050)------------------------------ % 131.97/19.60 % (2936050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.97/19.60 % (2936050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.97/19.60 % (2936050)CaDiCaL version: 2.1.3 % 131.97/19.60 % (2936050)Termination reason: Instruction limit % 131.97/19.60 % (2936050)Termination phase: Saturation % 131.97/19.60 % (2936050)Time elapsed: 2.871 s % 131.97/19.60 % (2936050)Peak memory usage: 159 MB % 131.97/19.60 % (2936050)Instructions burned: 4496 (million) % 131.97/19.60 % (2936057)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=1407231116:i=4629:av=off:gsp=on_2868 on theBenchmark for (2868ds/4629Mi) % 131.97/19.60 % (2936055)Instruction limit reached! % 131.97/19.60 % (2936055)------------------------------ % 131.97/19.60 % (2936055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.97/19.60 % (2936055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.97/19.60 % (2936055)CaDiCaL version: 2.1.3 % 131.97/19.60 % (2936055)Termination reason: Instruction limit % 131.97/19.60 % (2936055)Termination phase: Saturation % 131.97/19.60 % (2936055)Time elapsed: 0.714 s % 131.97/19.60 % (2936055)Peak memory usage: 138 MB % 131.97/19.60 % (2936055)Instructions burned: 2085 (million) % 131.97/19.60 % (2936053)Instruction limit reached! % 131.97/19.60 % (2936053)------------------------------ % 131.97/19.60 % (2936053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.97/19.60 % (2936053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.97/19.60 % (2936053)CaDiCaL version: 2.1.3 % 131.97/19.60 % (2936053)Termination reason: Instruction limit % 131.97/19.60 % (2936053)Termination phase: Saturation % 131.97/19.60 % (2936053)Time elapsed: 3.104 s % 131.97/19.60 % (2936053)Peak memory usage: 152 MB % 131.97/19.60 % (2936053)Instructions burned: 4921 (million) % 131.97/19.60 % (2936059)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2582509113:i=1258:av=off_2861 on theBenchmark for (2861ds/1258Mi) % 158.65/23.25 % (2936060)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1850772912:i=7343:av=off:ss=included_2860 on theBenchmark for (2860ds/7343Mi) % 158.65/23.25 % (2936059)Instruction limit reached! % 158.65/23.25 % (2936059)------------------------------ % 158.65/23.25 % (2936059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.65/23.25 % (2936059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.65/23.25 % (2936059)CaDiCaL version: 2.1.3 % 158.65/23.25 % (2936059)Termination reason: Instruction limit % 158.65/23.25 % (2936059)Termination phase: Saturation % 158.65/23.25 % (2936059)Time elapsed: 0.300 s % 158.65/23.25 % (2936059)Peak memory usage: 93 MB % 158.65/23.25 % (2936059)Instructions burned: 1261 (million) % 158.65/23.25 % (2936063)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3524105809:i=1325:sd=2:ss=axioms:sgt=16_2857 on theBenchmark for (2857ds/1325Mi) % 158.65/23.25 % (2936063)Instruction limit reached! % 158.65/23.25 % (2936063)------------------------------ % 158.65/23.25 % (2936063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.65/23.25 % (2936063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.65/23.25 % (2936063)CaDiCaL version: 2.1.3 % 158.65/23.25 % (2936063)Termination reason: Instruction limit % 158.65/23.25 % (2936063)Termination phase: Saturation % 158.65/23.25 % (2936063)Time elapsed: 0.332 s % 158.65/23.25 % (2936063)Peak memory usage: 90 MB % 158.65/23.25 % (2936063)Instructions burned: 1325 (million) % 158.65/23.25 % (2936065)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=1134584116:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2852 on theBenchmark for (2852ds/2646Mi) % 158.65/23.25 % (2936065)Instruction limit reached! % 158.65/23.25 % (2936065)------------------------------ % 158.65/23.25 % (2936065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.65/23.25 % (2936065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.65/23.25 % (2936065)CaDiCaL version: 2.1.3 % 158.65/23.25 % (2936065)Termination reason: Instruction limit % 158.65/23.25 % (2936065)Termination phase: Saturation % 158.65/23.25 % (2936065)Time elapsed: 0.972 s % 158.65/23.25 % (2936065)Peak memory usage: 143 MB % 158.65/23.25 % (2936065)Instructions burned: 2647 (million) % 158.65/23.25 % (2936067)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2564916017:i=1489:sd=2:ep=R:ss=axioms_2841 on theBenchmark for (2841ds/1489Mi) % 158.65/23.25 % (2936057)Instruction limit reached! % 158.65/23.25 % (2936057)------------------------------ % 158.65/23.25 % (2936057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.65/23.25 % (2936057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.65/23.25 % (2936057)CaDiCaL version: 2.1.3 % 158.65/23.25 % (2936057)Termination reason: Instruction limit % 158.65/23.25 % (2936057)Termination phase: Saturation % 158.65/23.25 % (2936057)Time elapsed: 2.677 s % 158.65/23.25 % (2936057)Peak memory usage: 143 MB % 158.65/23.25 % (2936057)Instructions burned: 4629 (million) % 158.65/23.25 % (2936069)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=2513938394:i=1503_2839 on theBenchmark for (2839ds/1503Mi) % 158.65/23.25 % (2936049)Instruction limit reached! % 158.65/23.25 % (2936049)------------------------------ % 158.65/23.25 % (2936049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.65/23.25 % (2936049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.65/23.25 % (2936049)CaDiCaL version: 2.1.3 % 158.65/23.25 % (2936049)Termination reason: Instruction limit % 158.65/23.25 % (2936049)Termination phase: Saturation % 158.65/23.25 % (2936049)Time elapsed: 6.258 s % 158.65/23.25 % (2936049)Peak memory usage: 180 MB % 158.65/23.25 % (2936049)Instructions burned: 9531 (million) % 158.65/23.25 % (2936067)Instruction limit reached! % 158.65/23.25 % (2936067)------------------------------ % 158.65/23.25 % (2936067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.65/23.25 % (2936067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.65/23.25 % (2936067)CaDiCaL version: 2.1.3 % 158.65/23.25 % (2936067)Termination reason: Instruction limit % 158.65/23.25 % (2936067)Termination phase: Saturation % 184.82/26.99 % (2936067)Time elapsed: 0.596 s % 184.82/26.99 % (2936067)Peak memory usage: 134 MB % 184.82/26.99 % (2936067)Instructions burned: 1491 (million) % 184.82/26.99 % (2936071)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3019935452:i=13942:kws=frequency_2835 on theBenchmark for (2835ds/13942Mi) % 184.82/26.99 % (2936072)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=2090108071:i=3604:fsr=off:er=filter_2834 on theBenchmark for (2834ds/3604Mi) % 184.82/26.99 % (2936069)Instruction limit reached! % 184.82/26.99 % (2936069)------------------------------ % 184.82/26.99 % (2936069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.82/26.99 % (2936069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.82/26.99 % (2936069)CaDiCaL version: 2.1.3 % 184.82/26.99 % (2936069)Termination reason: Instruction limit % 184.82/26.99 % (2936069)Termination phase: Saturation % 184.82/26.99 % (2936069)Time elapsed: 0.942 s % 184.82/26.99 % (2936069)Peak memory usage: 135 MB % 184.82/26.99 % (2936069)Instructions burned: 1503 (million) % 184.82/26.99 % (2936075)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3479400097:i=1876:sd=1:ss=included:sgt=32_2828 on theBenchmark for (2828ds/1876Mi) % 184.82/26.99 % (2936075)Refutation not found, incomplete strategy % 184.82/26.99 % (2936075)------------------------------ % 184.82/26.99 % (2936075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.82/26.99 % (2936075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.82/26.99 % (2936075)CaDiCaL version: 2.1.3 % 184.82/26.99 % (2936075)Termination reason: Refutation not found, incomplete strategy % 184.82/26.99 % (2936075)Time elapsed: 0.596 s % 184.82/26.99 % (2936075)Peak memory usage: 128 MB % 184.82/26.99 % (2936075)Instructions burned: 905 (million) % 184.82/26.99 % (2936072)Instruction limit reached! % 184.82/26.99 % (2936072)------------------------------ % 184.82/26.99 % (2936072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.82/26.99 % (2936072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.82/26.99 % (2936072)CaDiCaL version: 2.1.3 % 184.82/26.99 % (2936072)Termination reason: Instruction limit % 184.82/26.99 % (2936072)Termination phase: Saturation % 184.82/26.99 % (2936072)Time elapsed: 1.235 s % 184.82/26.99 % (2936072)Peak memory usage: 150 MB % 184.82/26.99 % (2936072)Instructions burned: 3604 (million) % 184.82/26.99 % (2936077)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2513315217:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2820 on theBenchmark for (2820ds/1932Mi) % 184.82/26.99 % (2936060)Instruction limit reached! % 184.82/26.99 % (2936060)------------------------------ % 184.82/26.99 % (2936060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.82/26.99 % (2936060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.82/26.99 % (2936060)CaDiCaL version: 2.1.3 % 184.82/26.99 % (2936060)Termination reason: Instruction limit % 184.82/26.99 % (2936060)Termination phase: Saturation % 184.82/26.99 % (2936060)Time elapsed: 4.005 s % 184.82/26.99 % (2936060)Peak memory usage: 193 MB % 184.82/26.99 % (2936060)Instructions burned: 7344 (million) % 184.82/26.99 % (2936075)------------------------------ % 184.82/26.99 % (2936075)------------------------------ % 184.82/26.99 % (2936079)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=3805467968:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2818 on theBenchmark for (2818ds/1980Mi) % 184.82/26.99 % (2936080)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=749075863:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2818 on theBenchmark for (2818ds/3902Mi) % 184.82/26.99 % (2936077)Instruction limit reached! % 184.82/26.99 % (2936077)------------------------------ % 184.82/26.99 % (2936077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.82/26.99 % (2936077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.82/26.99 % (2936077)CaDiCaL version: 2.1.3 % 184.82/26.99 % (2936077)Termination reason: Instruction limit % 184.82/26.99 % (2936077)Termination phase: Saturation % 184.82/26.99 % (2936077)Time elapsed: 0.658 s % 184.82/26.99 % (2936077)Peak memory usage: 139 MB % 215.42/31.21 % (2936077)Instructions burned: 1935 (million) % 215.42/31.21 % (2936083)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=4243045359:avsq=on:i=3916:aac=none:amm=off_2812 on theBenchmark for (2812ds/3916Mi) % 215.42/31.21 % (2936079)Instruction limit reached! % 215.42/31.21 % (2936079)------------------------------ % 215.42/31.21 % (2936079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.42/31.21 % (2936079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.42/31.21 % (2936079)CaDiCaL version: 2.1.3 % 215.42/31.21 % (2936079)Termination reason: Instruction limit % 215.42/31.21 % (2936079)Termination phase: Saturation % 215.42/31.21 % (2936079)Time elapsed: 1.273 s % 215.42/31.21 % (2936079)Peak memory usage: 137 MB % 215.42/31.21 % (2936079)Instructions burned: 1981 (million) % 215.42/31.21 % (2936085)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2991369528:cond=on:i=3940:av=off:er=known_2804 on theBenchmark for (2804ds/3940Mi) % 215.42/31.21 % (2936083)Instruction limit reached! % 215.42/31.21 % (2936083)------------------------------ % 215.42/31.21 % (2936083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.42/31.21 % (2936083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.42/31.21 % (2936083)CaDiCaL version: 2.1.3 % 215.42/31.21 % (2936083)Termination reason: Instruction limit % 215.42/31.21 % (2936083)Termination phase: Saturation % 215.42/31.21 % (2936083)Time elapsed: 1.107 s % 215.42/31.21 % (2936083)Peak memory usage: 107 MB % 215.42/31.21 % (2936083)Instructions burned: 3919 (million) % 215.42/31.21 % (2936087)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2194117751:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2800 on theBenchmark for (2800ds/3980Mi) % 215.42/31.21 % (2936080)Instruction limit reached! % 215.42/31.21 % (2936080)------------------------------ % 215.42/31.21 % (2936080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.42/31.21 % (2936080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.42/31.21 % (2936080)CaDiCaL version: 2.1.3 % 215.42/31.21 % (2936080)Termination reason: Instruction limit % 215.42/31.21 % (2936080)Termination phase: Saturation % 215.42/31.21 % (2936080)Time elapsed: 2.222 s % 215.42/31.21 % (2936080)Peak memory usage: 158 MB % 215.42/31.21 % (2936080)Instructions burned: 3903 (million) % 215.42/31.21 % (2936089)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=2787640342:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2794 on theBenchmark for (2794ds/2087Mi) % 215.42/31.21 % (2936085)Instruction limit reached! % 215.42/31.21 % (2936085)------------------------------ % 215.42/31.21 % (2936085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.42/31.21 % (2936085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.42/31.21 % (2936085)CaDiCaL version: 2.1.3 % 215.42/31.21 % (2936085)Termination reason: Instruction limit % 215.42/31.21 % (2936085)Termination phase: Saturation % 215.42/31.21 % (2936085)Time elapsed: 1.537 s % 215.42/31.21 % (2936085)Peak memory usage: 151 MB % 215.42/31.21 % (2936085)Instructions burned: 3943 (million) % 215.42/31.21 % (2936091)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=2696352413:cts=off:cond=on:i=4272:bs=on:fsd=on_2787 on theBenchmark for (2787ds/4272Mi) % 215.42/31.21 % (2936089)Instruction limit reached! % 215.42/31.21 % (2936089)------------------------------ % 215.42/31.21 % (2936089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.42/31.21 % (2936089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.42/31.21 % (2936089)CaDiCaL version: 2.1.3 % 215.42/31.21 % (2936089)Termination reason: Instruction limit % 215.42/31.21 % (2936089)Termination phase: Saturation % 215.42/31.21 % (2936089)Time elapsed: 1.377 s % 215.42/31.21 % (2936089)Peak memory usage: 138 MB % 215.42/31.21 % (2936089)Instructions burned: 2089 (million) % 215.42/31.21 % (2936093)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3634906368:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2778 on theBenchmark for (2778ds/2197Mi) % 215.42/31.21 % (2936087)Instruction limit reached! % 266.47/38.48 % (2936087)------------------------------ % 266.47/38.48 % (2936087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.47/38.48 % (2936087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.47/38.48 % (2936087)CaDiCaL version: 2.1.3 % 266.47/38.48 % (2936087)Termination reason: Instruction limit % 266.47/38.48 % (2936087)Termination phase: Saturation % 266.47/38.48 % (2936087)Time elapsed: 2.285 s % 266.47/38.48 % (2936087)Peak memory usage: 156 MB % 266.47/38.48 % (2936087)Instructions burned: 3981 (million) % 266.47/38.48 % (2936095)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1197813064:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2775 on theBenchmark for (2775ds/6508Mi) % 266.47/38.48 % (2936091)Instruction limit reached! % 266.47/38.48 % (2936091)------------------------------ % 266.47/38.48 % (2936091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.47/38.48 % (2936091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.47/38.48 % (2936091)CaDiCaL version: 2.1.3 % 266.47/38.48 % (2936091)Termination reason: Instruction limit % 266.47/38.48 % (2936091)Termination phase: Saturation % 266.47/38.48 % (2936091)Time elapsed: 1.594 s % 266.47/38.48 % (2936091)Peak memory usage: 153 MB % 266.47/38.48 % (2936091)Instructions burned: 4273 (million) % 266.47/38.48 % (2936097)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3460915687:i=2330:fgj=on:av=off:fsr=off_2769 on theBenchmark for (2769ds/2330Mi) % 266.47/38.48 % (2936093)Instruction limit reached! % 266.47/38.48 % (2936093)------------------------------ % 266.47/38.48 % (2936093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.47/38.48 % (2936093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.47/38.48 % (2936093)CaDiCaL version: 2.1.3 % 266.47/38.48 % (2936093)Termination reason: Instruction limit % 266.47/38.48 % (2936093)Termination phase: Saturation % 266.47/38.48 % (2936093)Time elapsed: 1.317 s % 266.47/38.48 % (2936093)Peak memory usage: 141 MB % 266.47/38.48 % (2936093)Instructions burned: 2199 (million) % 266.47/38.48 % (2936099)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1079692401:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2763 on theBenchmark for (2763ds/7592Mi) % 266.47/38.48 % (2936097)Instruction limit reached! % 266.47/38.48 % (2936097)------------------------------ % 266.47/38.48 % (2936097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.47/38.48 % (2936097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.47/38.48 % (2936097)CaDiCaL version: 2.1.3 % 266.47/38.48 % (2936097)Termination reason: Instruction limit % 266.47/38.48 % (2936097)Termination phase: Saturation % 266.47/38.48 % (2936097)Time elapsed: 0.767 s % 266.47/38.48 % (2936097)Peak memory usage: 137 MB % 266.47/38.48 % (2936097)Instructions burned: 2331 (million) % 266.47/38.48 % (2936101)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=993316508:i=2693:kws=precedence:ins=1:av=off_2760 on theBenchmark for (2760ds/2693Mi) % 266.47/38.48 % (2936101)Instruction limit reached! % 266.47/38.48 % (2936101)------------------------------ % 266.47/38.48 % (2936101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.47/38.48 % (2936101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.47/38.48 % (2936101)CaDiCaL version: 2.1.3 % 266.47/38.48 % (2936101)Termination reason: Instruction limit % 266.47/38.48 % (2936101)Termination phase: Saturation % 266.47/38.48 % (2936101)Time elapsed: 0.937 s % 266.47/38.48 % (2936101)Peak memory usage: 143 MB % 266.47/38.48 % (2936101)Instructions burned: 2693 (million) % 266.47/38.48 % (2936103)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=634376748:i=28651:sd=4:ss=included:sgt=64_2750 on theBenchmark for (2750ds/28651Mi) % 266.47/38.48 % (2936071)Instruction limit reached! % 266.47/38.48 % (2936071)------------------------------ % 266.47/38.48 % (2936071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.47/38.48 % (2936071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.47/38.48 % (2936071)CaDiCaL version: 2.1.3 % 266.47/38.48 % (2936071)Termination reason: Instruction limit % 266.47/38.48 % (2936071)Termination phase: Saturation % 266.47/38.48 % (2936071)Time elapsed: 9.302 s % 266.47/38.48 % (2936071)Peak memory usage: 240 MB % 266.47/38.48 % (2936071)Instructions burned: 13942 (million) % 266.47/38.48 % (2936105)lrs-1010_1_ncem=casc2026/models/loop5.pTerminated %------------------------------------------------------------------------------