%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV524-1.050 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:16:42 PM UTC 2026 % Result : Timeout 300.76s 43.06s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV524-1.050 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n018.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 11:33:39 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 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 % 7.61/1.97 % (3315853)Input is clausal, will run a generic CNF schedule. % 7.61/1.97 % (3315864)dis-21_1_sil=8000:lcm=predicate:random_seed=349371100: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) % 7.61/1.97 % (3315864)Refutation not found, incomplete strategy % 7.61/1.97 % (3315864)------------------------------ % 7.61/1.97 % (3315864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.61/1.97 % (3315864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.97 % (3315864)CaDiCaL version: 2.1.3 % 7.61/1.97 % (3315864)Termination reason: Refutation not found, incomplete strategy % 7.61/1.97 % (3315864)Time elapsed: 0.018 s % 7.61/1.97 % (3315864)Peak memory usage: 89 MB % 7.61/1.97 % (3315864)Instructions burned: 66 (million) % 7.61/1.97 % (3315863)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3846520744:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 7.61/1.97 % (3315858)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=1322958713:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 7.61/1.97 % (3315860)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=650474248:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 7.61/1.97 % (3315861)lrs+10_1_sil=8000:sp=occurrence:random_seed=2806935876:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 7.61/1.97 % (3315862)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1660522339:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 7.61/1.97 % (3315859)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3216615763:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 7.61/1.97 % (3315861)Instruction limit reached! % 7.61/1.97 % (3315861)------------------------------ % 7.61/1.97 % (3315861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.61/1.97 % (3315861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.97 % (3315861)CaDiCaL version: 2.1.3 % 7.61/1.97 % (3315861)Termination reason: Instruction limit % 7.61/1.97 % (3315861)Termination phase: Saturation % 7.61/1.97 % (3315861)Time elapsed: 0.057 s % 7.61/1.97 % (3315861)Peak memory usage: 89 MB % 7.61/1.97 % (3315861)Instructions burned: 107 (million) % 7.61/1.97 % (3315862)Instruction limit reached! % 7.61/1.97 % (3315862)------------------------------ % 7.61/1.97 % (3315862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.61/1.97 % (3315862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.97 % (3315862)CaDiCaL version: 2.1.3 % 7.61/1.97 % (3315862)Termination reason: Instruction limit % 7.61/1.97 % (3315862)Termination phase: Saturation % 7.61/1.97 % (3315862)Time elapsed: 0.057 s % 7.61/1.97 % (3315862)Peak memory usage: 89 MB % 7.61/1.97 % (3315862)Instructions burned: 116 (million) % 7.61/1.97 % (3315863)Instruction limit reached! % 7.61/1.97 % (3315863)------------------------------ % 7.61/1.97 % (3315863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.61/1.97 % (3315863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.61/1.97 % (3315863)CaDiCaL version: 2.1.3 % 7.61/1.97 % (3315863)Termination reason: Instruction limit % 7.61/1.97 % (3315863)Termination phase: Saturation % 7.61/1.97 % (3315863)Time elapsed: 0.122 s % 7.61/1.97 % (3315863)Peak memory usage: 90 MB % 7.61/1.97 % (3315863)Instructions burned: 182 (million) % 7.61/1.97 % (3315864)------------------------------ % 7.61/1.97 % (3315864)------------------------------ % 7.61/1.97 % (3315872)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=3595988389:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 7.61/1.97 % (3315873)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1619560823: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) % 7.61/1.97 % (3315875)lrs+10_64_to=lpo:sil=8000:random_seed=1157991702:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 7.61/1.97 % (3315875)Instruction limit reached! % 7.61/1.97 % (3315875)------------------------------ % 7.61/1.97 % (3315875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.38 % (3315875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.38 % (3315875)CaDiCaL version: 2.1.3 % 18.90/3.38 % (3315875)Termination reason: Instruction limit % 18.90/3.38 % (3315875)Termination phase: Saturation % 18.90/3.38 % (3315875)Time elapsed: 0.036 s % 18.90/3.38 % (3315875)Peak memory usage: 90 MB % 18.90/3.38 % (3315875)Instructions burned: 129 (million) % 18.90/3.38 % (3315872)Instruction limit reached! % 18.90/3.38 % (3315872)------------------------------ % 18.90/3.38 % (3315872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.38 % (3315872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.38 % (3315872)CaDiCaL version: 2.1.3 % 18.90/3.38 % (3315872)Termination reason: Instruction limit % 18.90/3.38 % (3315872)Termination phase: Saturation % 18.90/3.38 % (3315872)Time elapsed: 0.063 s % 18.90/3.38 % (3315872)Peak memory usage: 89 MB % 18.90/3.38 % (3315872)Instructions burned: 145 (million) % 18.90/3.38 % (3315874)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=819586753:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi) % 18.90/3.38 % (3315873)Instruction limit reached! % 18.90/3.38 % (3315873)------------------------------ % 18.90/3.38 % (3315873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.38 % (3315873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.38 % (3315873)CaDiCaL version: 2.1.3 % 18.90/3.38 % (3315873)Termination reason: Instruction limit % 18.90/3.38 % (3315873)Termination phase: Saturation % 18.90/3.38 % (3315873)Time elapsed: 0.104 s % 18.90/3.38 % (3315873)Peak memory usage: 91 MB % 18.90/3.38 % (3315873)Instructions burned: 190 (million) % 18.90/3.38 % (3315874)Instruction limit reached! % 18.90/3.38 % (3315874)------------------------------ % 18.90/3.38 % (3315874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.38 % (3315874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.38 % (3315874)CaDiCaL version: 2.1.3 % 18.90/3.38 % (3315874)Termination reason: Instruction limit % 18.90/3.38 % (3315874)Termination phase: Saturation % 18.90/3.38 % (3315874)Time elapsed: 0.088 s % 18.90/3.38 % (3315874)Peak memory usage: 89 MB % 18.90/3.38 % (3315874)Instructions burned: 221 (million) % 18.90/3.38 % (3315879)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2534966240:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 18.90/3.38 % (3315880)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2080255006:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 18.90/3.38 % (3315879)Instruction limit reached! % 18.90/3.38 % (3315879)------------------------------ % 18.90/3.38 % (3315879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.38 % (3315879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.38 % (3315879)CaDiCaL version: 2.1.3 % 18.90/3.38 % (3315879)Termination reason: Instruction limit % 18.90/3.38 % (3315879)Termination phase: Saturation % 18.90/3.38 % (3315879)Time elapsed: 0.055 s % 18.90/3.38 % (3315879)Peak memory usage: 91 MB % 18.90/3.38 % (3315879)Instructions burned: 197 (million) % 18.90/3.38 % (3315882)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3940502223:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 18.90/3.38 % (3315880)Instruction limit reached! % 18.90/3.38 % (3315880)------------------------------ % 18.90/3.38 % (3315880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.38 % (3315880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.38 % (3315880)CaDiCaL version: 2.1.3 % 18.90/3.38 % (3315880)Termination reason: Instruction limit % 18.90/3.38 % (3315880)Termination phase: Saturation % 18.90/3.38 % (3315880)Time elapsed: 0.084 s % 18.90/3.38 % (3315880)Peak memory usage: 93 MB % 18.90/3.38 % (3315880)Instructions burned: 158 (million) % 18.90/3.38 % (3315883)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=4172058774:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 18.90/3.38 % (3315887)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2345332762:i=107_2993 on theBenchmark for (2993ds/107Mi) % 18.90/3.38 % (3315883)Instruction limit reached! % 18.90/3.38 % (3315883)------------------------------ % 29.72/4.93 % (3315883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.72/4.93 % (3315883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.72/4.93 % (3315883)CaDiCaL version: 2.1.3 % 29.72/4.93 % (3315883)Termination reason: Instruction limit % 29.72/4.93 % (3315883)Termination phase: Saturation % 29.72/4.93 % (3315883)Time elapsed: 0.052 s % 29.72/4.93 % (3315883)Peak memory usage: 90 MB % 29.72/4.93 % (3315883)Instructions burned: 107 (million) % 29.72/4.93 % (3315887)Instruction limit reached! % 29.72/4.93 % (3315887)------------------------------ % 29.72/4.93 % (3315887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.72/4.93 % (3315887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.72/4.93 % (3315887)CaDiCaL version: 2.1.3 % 29.72/4.93 % (3315887)Termination reason: Instruction limit % 29.72/4.93 % (3315887)Termination phase: Saturation % 29.72/4.93 % (3315887)Time elapsed: 0.025 s % 29.72/4.93 % (3315887)Peak memory usage: 89 MB % 29.72/4.93 % (3315887)Instructions burned: 108 (million) % 29.72/4.93 % (3315889)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1562598901:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 29.72/4.93 % (3315893)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1896945721:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi) % 29.72/4.93 % (3315893)Instruction limit reached! % 29.72/4.93 % (3315893)------------------------------ % 29.72/4.93 % (3315893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.72/4.93 % (3315893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.72/4.93 % (3315893)CaDiCaL version: 2.1.3 % 29.72/4.93 % (3315893)Termination reason: Instruction limit % 29.72/4.93 % (3315893)Termination phase: Saturation % 29.72/4.93 % (3315893)Time elapsed: 0.041 s % 29.72/4.93 % (3315893)Peak memory usage: 90 MB % 29.72/4.93 % (3315893)Instructions burned: 138 (million) % 29.72/4.93 % (3315892)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=192698137:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 29.72/4.93 % (3315889)Instruction limit reached! % 29.72/4.93 % (3315889)------------------------------ % 29.72/4.93 % (3315889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.72/4.93 % (3315889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.72/4.93 % (3315889)CaDiCaL version: 2.1.3 % 29.72/4.93 % (3315889)Termination reason: Instruction limit % 29.72/4.93 % (3315889)Termination phase: Saturation % 29.72/4.93 % (3315889)Time elapsed: 0.126 s % 29.72/4.93 % (3315889)Peak memory usage: 91 MB % 29.72/4.93 % (3315889)Instructions burned: 242 (million) % 29.72/4.93 % (3315896)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1713876168:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 29.72/4.93 % (3315898)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1856817923:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi) % 29.72/4.93 % (3315896)Instruction limit reached! % 29.72/4.93 % (3315896)------------------------------ % 29.72/4.93 % (3315896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.72/4.93 % (3315896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.72/4.93 % (3315896)CaDiCaL version: 2.1.3 % 29.72/4.93 % (3315896)Termination reason: Instruction limit % 29.72/4.93 % (3315896)Termination phase: Saturation % 29.72/4.93 % (3315896)Time elapsed: 0.141 s % 29.72/4.93 % (3315896)Peak memory usage: 95 MB % 29.72/4.93 % (3315896)Instructions burned: 501 (million) % 29.72/4.93 % (3315898)Instruction limit reached! % 29.72/4.93 % (3315898)------------------------------ % 29.72/4.93 % (3315898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.72/4.93 % (3315898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.72/4.93 % (3315898)CaDiCaL version: 2.1.3 % 29.72/4.93 % (3315898)Termination reason: Instruction limit % 29.72/4.93 % (3315898)Termination phase: Saturation % 29.72/4.93 % (3315898)Time elapsed: 0.104 s % 29.72/4.93 % (3315898)Peak memory usage: 91 MB % 29.72/4.93 % (3315898)Instructions burned: 191 (million) % 29.72/4.93 % (3315901)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3596370768:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 44.07/6.91 % (3315901)Instruction limit reached! % 44.07/6.91 % (3315901)------------------------------ % 44.07/6.91 % (3315901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/6.91 % (3315901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/6.91 % (3315901)CaDiCaL version: 2.1.3 % 44.07/6.91 % (3315901)Termination reason: Instruction limit % 44.07/6.91 % (3315901)Termination phase: Saturation % 44.07/6.91 % (3315901)Time elapsed: 0.063 s % 44.07/6.91 % (3315901)Peak memory usage: 92 MB % 44.07/6.91 % (3315901)Instructions burned: 264 (million) % 44.07/6.91 % (3315902)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2674487115:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi) % 44.07/6.91 % (3315904)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=379925079:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi) % 44.07/6.91 % (3315902)Instruction limit reached! % 44.07/6.91 % (3315902)------------------------------ % 44.07/6.91 % (3315902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/6.91 % (3315902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/6.91 % (3315902)CaDiCaL version: 2.1.3 % 44.07/6.91 % (3315902)Termination reason: Instruction limit % 44.07/6.91 % (3315902)Termination phase: Saturation % 44.07/6.91 % (3315902)Time elapsed: 0.088 s % 44.07/6.91 % (3315902)Peak memory usage: 90 MB % 44.07/6.91 % (3315902)Instructions burned: 157 (million) % 44.07/6.91 % (3315907)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=752688655:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 44.07/6.91 % (3315907)Instruction limit reached! % 44.07/6.91 % (3315907)------------------------------ % 44.07/6.91 % (3315907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/6.91 % (3315907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/6.91 % (3315907)CaDiCaL version: 2.1.3 % 44.07/6.91 % (3315907)Termination reason: Instruction limit % 44.07/6.91 % (3315907)Termination phase: Saturation % 44.07/6.91 % (3315907)Time elapsed: 0.287 s % 44.07/6.91 % (3315907)Peak memory usage: 93 MB % 44.07/6.91 % (3315907)Instructions burned: 538 (million) % 44.07/6.91 % (3315909)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1681214346:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi) % 44.07/6.91 % (3315909)Instruction limit reached! % 44.07/6.91 % (3315909)------------------------------ % 44.07/6.91 % (3315909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/6.91 % (3315909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/6.91 % (3315909)CaDiCaL version: 2.1.3 % 44.07/6.91 % (3315909)Termination reason: Instruction limit % 44.07/6.91 % (3315909)Termination phase: Saturation % 44.07/6.91 % (3315909)Time elapsed: 0.083 s % 44.07/6.91 % (3315909)Peak memory usage: 91 MB % 44.07/6.91 % (3315909)Instructions burned: 182 (million) % 44.07/6.91 % (3315911)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=469352455:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi) % 44.07/6.91 % (3315882)Instruction limit reached! % 44.07/6.91 % (3315882)------------------------------ % 44.07/6.91 % (3315882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/6.91 % (3315882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/6.91 % (3315882)CaDiCaL version: 2.1.3 % 44.07/6.91 % (3315882)Termination reason: Instruction limit % 44.07/6.91 % (3315882)Termination phase: Saturation % 44.07/6.91 % (3315882)Time elapsed: 1.890 s % 44.07/6.91 % (3315882)Peak memory usage: 149 MB % 44.07/6.91 % (3315882)Instructions burned: 3395 (million) % 44.07/6.91 % (3315904)Instruction limit reached! % 44.07/6.91 % (3315904)------------------------------ % 44.07/6.91 % (3315904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/6.91 % (3315904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/6.91 % (3315904)CaDiCaL version: 2.1.3 % 44.07/6.91 % (3315904)Termination reason: Instruction limit % 44.07/6.91 % (3315904)Termination phase: Saturation % 44.07/6.91 % (3315904)Time elapsed: 1.178 s % 44.07/6.91 % (3315904)Peak memory usage: 152 MB % 44.07/6.91 % (3315904)Instructions burned: 3257 (million) % 44.07/6.91 % (3315913)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=2234325482:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi) % 69.17/10.43 % (3315914)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=1581972085:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi) % 69.17/10.43 % (3315913)Instruction limit reached! % 69.17/10.43 % (3315913)------------------------------ % 69.17/10.43 % (3315913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.17/10.43 % (3315913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.17/10.43 % (3315913)CaDiCaL version: 2.1.3 % 69.17/10.43 % (3315913)Termination reason: Instruction limit % 69.17/10.43 % (3315913)Termination phase: Saturation % 69.17/10.43 % (3315913)Time elapsed: 0.207 s % 69.17/10.43 % (3315913)Peak memory usage: 97 MB % 69.17/10.43 % (3315913)Instructions burned: 413 (million) % 69.17/10.43 % (3315917)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=4153824190:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi) % 69.17/10.43 % (3315917)Instruction limit reached! % 69.17/10.43 % (3315917)------------------------------ % 69.17/10.43 % (3315917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.17/10.43 % (3315917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.17/10.43 % (3315917)CaDiCaL version: 2.1.3 % 69.17/10.43 % (3315917)Termination reason: Instruction limit % 69.17/10.43 % (3315917)Termination phase: Saturation % 69.17/10.43 % (3315917)Time elapsed: 0.117 s % 69.17/10.43 % (3315917)Peak memory usage: 91 MB % 69.17/10.43 % (3315917)Instructions burned: 304 (million) % 69.17/10.43 % (3315919)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3673459023:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi) % 69.17/10.43 % (3315892)Instruction limit reached! % 69.17/10.43 % (3315892)------------------------------ % 69.17/10.43 % (3315892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.17/10.43 % (3315892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.17/10.43 % (3315892)CaDiCaL version: 2.1.3 % 69.17/10.43 % (3315892)Termination reason: Instruction limit % 69.17/10.43 % (3315892)Termination phase: Saturation % 69.17/10.43 % (3315892)Time elapsed: 2.708 s % 69.17/10.43 % (3315892)Peak memory usage: 146 MB % 69.17/10.43 % (3315892)Instructions burned: 5208 (million) % 69.17/10.43 % (3315919)Instruction limit reached! % 69.17/10.43 % (3315919)------------------------------ % 69.17/10.43 % (3315919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.17/10.43 % (3315919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.17/10.43 % (3315919)CaDiCaL version: 2.1.3 % 69.17/10.43 % (3315919)Termination reason: Instruction limit % 69.17/10.43 % (3315919)Termination phase: Saturation % 69.17/10.43 % (3315919)Time elapsed: 0.407 s % 69.17/10.43 % (3315919)Peak memory usage: 98 MB % 69.17/10.43 % (3315919)Instructions burned: 721 (million) % 69.17/10.43 % (3315921)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=796083522:i=598:bs=on:bd=preordered:av=off:ss=axioms_2963 on theBenchmark for (2963ds/598Mi) % 69.17/10.43 % (3315922)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=975662370:i=2989:sd=3:ss=axioms:sgt=60_2962 on theBenchmark for (2962ds/2989Mi) % 69.17/10.43 % (3315921)Instruction limit reached! % 69.17/10.43 % (3315921)------------------------------ % 69.17/10.43 % (3315921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.17/10.43 % (3315921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.17/10.43 % (3315921)CaDiCaL version: 2.1.3 % 69.17/10.43 % (3315921)Termination reason: Instruction limit % 69.17/10.43 % (3315921)Termination phase: Saturation % 69.17/10.43 % (3315921)Time elapsed: 0.293 s % 69.17/10.43 % (3315921)Peak memory usage: 95 MB % 69.17/10.43 % (3315921)Instructions burned: 598 (million) % 69.17/10.43 % (3315925)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=746496314:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2959 on theBenchmark for (2959ds/1997Mi) % 95.09/14.04 % (3315914)Instruction limit reached! % 95.09/14.04 % (3315914)------------------------------ % 95.09/14.04 % (3315914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.09/14.04 % (3315914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.09/14.04 % (3315914)CaDiCaL version: 2.1.3 % 95.09/14.04 % (3315914)Termination reason: Instruction limit % 95.09/14.04 % (3315914)Termination phase: Saturation % 95.09/14.04 % (3315914)Time elapsed: 2.294 s % 95.09/14.04 % (3315914)Peak memory usage: 153 MB % 95.09/14.04 % (3315914)Instructions burned: 8481 (million) % 95.09/14.04 % (3315927)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=1587691835:i=2088:bd=preordered:av=off_2949 on theBenchmark for (2949ds/2088Mi) % 95.09/14.04 % (3315925)Instruction limit reached! % 95.09/14.04 % (3315925)------------------------------ % 95.09/14.04 % (3315925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.09/14.04 % (3315925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.09/14.04 % (3315925)CaDiCaL version: 2.1.3 % 95.09/14.04 % (3315925)Termination reason: Instruction limit % 95.09/14.04 % (3315925)Termination phase: Saturation % 95.09/14.04 % (3315925)Time elapsed: 1.260 s % 95.09/14.04 % (3315925)Peak memory usage: 141 MB % 95.09/14.04 % (3315925)Instructions burned: 1998 (million) % 95.09/14.04 % (3315922)Instruction limit reached! % 95.09/14.04 % (3315922)------------------------------ % 95.09/14.04 % (3315922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.09/14.04 % (3315922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.09/14.04 % (3315922)CaDiCaL version: 2.1.3 % 95.09/14.04 % (3315922)Termination reason: Instruction limit % 95.09/14.04 % (3315922)Termination phase: Saturation % 95.09/14.04 % (3315922)Time elapsed: 1.669 s % 95.09/14.04 % (3315922)Peak memory usage: 146 MB % 95.09/14.04 % (3315922)Instructions burned: 2990 (million) % 95.09/14.04 % (3315929)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4264837368:i=1098:nicw=on_2944 on theBenchmark for (2944ds/1098Mi) % 95.09/14.04 % (3315930)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1949499898:i=433:bd=preordered_2943 on theBenchmark for (2943ds/433Mi) % 95.09/14.04 % (3315930)Refutation not found, incomplete strategy % 95.09/14.04 % (3315930)------------------------------ % 95.09/14.04 % (3315930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.09/14.04 % (3315930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.09/14.04 % (3315930)CaDiCaL version: 2.1.3 % 95.09/14.04 % (3315930)Termination reason: Refutation not found, incomplete strategy % 95.09/14.04 % (3315930)Time elapsed: 0.044 s % 95.09/14.04 % (3315930)Peak memory usage: 91 MB % 95.09/14.04 % (3315930)Instructions burned: 84 (million) % 95.09/14.04 % (3315927)Instruction limit reached! % 95.09/14.04 % (3315927)------------------------------ % 95.09/14.04 % (3315927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.09/14.04 % (3315927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.09/14.04 % (3315927)CaDiCaL version: 2.1.3 % 95.09/14.04 % (3315927)Termination reason: Instruction limit % 95.09/14.04 % (3315927)Termination phase: Saturation % 95.09/14.04 % (3315927)Time elapsed: 0.717 s % 95.09/14.04 % (3315927)Peak memory usage: 141 MB % 95.09/14.04 % (3315927)Instructions burned: 2090 (million) % 95.09/14.04 % (3315930)------------------------------ % 95.09/14.04 % (3315930)------------------------------ % 95.09/14.04 % (3315933)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1055635142:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2940 on theBenchmark for (2940ds/2942Mi) % 95.09/14.04 % (3315929)Instruction limit reached! % 95.09/14.04 % (3315929)------------------------------ % 95.09/14.04 % (3315929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.09/14.04 % (3315929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.09/14.04 % (3315929)CaDiCaL version: 2.1.3 % 95.09/14.04 % (3315929)Termination reason: Instruction limit % 95.09/14.04 % (3315929)Termination phase: Saturation % 95.09/14.04 % (3315929)Time elapsed: 0.524 s % 95.09/14.04 % (3315929)Peak memory usage: 102 MB % 95.09/14.04 % (3315929)Instructions burned: 1099 (million) % 95.09/14.04 % (3315935)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3495900980:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi) % 111.02/16.32 % (3315936)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=3501495702:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2937 on theBenchmark for (2937ds/596Mi) % 111.02/16.32 % (3315936)Refutation not found, incomplete strategy % 111.02/16.32 % (3315936)------------------------------ % 111.02/16.32 % (3315936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.02/16.32 % (3315936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/16.32 % (3315936)CaDiCaL version: 2.1.3 % 111.02/16.32 % (3315936)Termination reason: Refutation not found, incomplete strategy % 111.02/16.32 % (3315936)Time elapsed: 0.107 s % 111.02/16.32 % (3315936)Peak memory usage: 91 MB % 111.02/16.32 % (3315936)Instructions burned: 236 (million) % 111.02/16.32 % (3315936)------------------------------ % 111.02/16.32 % (3315936)------------------------------ % 111.02/16.32 % (3315939)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=4292335165:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2932 on theBenchmark for (2932ds/4123Mi) % 111.02/16.32 % (3315933)Instruction limit reached! % 111.02/16.32 % (3315933)------------------------------ % 111.02/16.32 % (3315933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.02/16.32 % (3315933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/16.32 % (3315933)CaDiCaL version: 2.1.3 % 111.02/16.32 % (3315933)Termination reason: Instruction limit % 111.02/16.32 % (3315933)Termination phase: Saturation % 111.02/16.32 % (3315933)Time elapsed: 0.934 s % 111.02/16.32 % (3315933)Peak memory usage: 146 MB % 111.02/16.32 % (3315933)Instructions burned: 2945 (million) % 111.02/16.32 % (3315941)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3801727897:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2929 on theBenchmark for (2929ds/16411Mi) % 111.02/16.32 % (3315911)Instruction limit reached! % 111.02/16.32 % (3315911)------------------------------ % 111.02/16.32 % (3315911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.02/16.32 % (3315911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/16.32 % (3315911)CaDiCaL version: 2.1.3 % 111.02/16.32 % (3315911)Termination reason: Instruction limit % 111.02/16.32 % (3315911)Termination phase: Saturation % 111.02/16.32 % (3315911)Time elapsed: 5.104 s % 111.02/16.32 % (3315911)Peak memory usage: 158 MB % 111.02/16.32 % (3315911)Instructions burned: 10309 (million) % 111.02/16.32 % (3315943)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3298543721:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2924 on theBenchmark for (2924ds/1670Mi) % 111.02/16.32 % (3315943)Instruction limit reached! % 111.02/16.32 % (3315943)------------------------------ % 111.02/16.32 % (3315943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.02/16.32 % (3315943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/16.32 % (3315943)CaDiCaL version: 2.1.3 % 111.02/16.32 % (3315943)Termination reason: Instruction limit % 111.02/16.32 % (3315943)Termination phase: Saturation % 111.02/16.32 % (3315943)Time elapsed: 1.039 s % 111.02/16.32 % (3315943)Peak memory usage: 138 MB % 111.02/16.32 % (3315943)Instructions burned: 1670 (million) % 111.02/16.32 % (3315945)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=2251377773:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2912 on theBenchmark for (2912ds/1722Mi) % 111.02/16.32 % (3315939)Instruction limit reached! % 111.02/16.32 % (3315939)------------------------------ % 111.02/16.32 % (3315939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.02/16.32 % (3315939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.02/16.32 % (3315939)CaDiCaL version: 2.1.3 % 111.02/16.32 % (3315939)Termination reason: Instruction limit % 111.02/16.32 % (3315939)Termination phase: Saturation % 111.02/16.32 % (3315939)Time elapsed: 2.677 s % 111.02/16.32 % (3315939)Peak memory usage: 159 MB % 111.02/16.32 % (3315939)Instructions burned: 4125 (million) % 111.02/16.32 % (3315947)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=929856822:cts=off:cond=on:i=9530:bs=on:fsd=on_2904 on theBenchmark for (2904ds/9530Mi) % 128.72/19.01 % (3315945)Instruction limit reached! % 128.72/19.01 % (3315945)------------------------------ % 128.72/19.01 % (3315945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.72/19.01 % (3315945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.72/19.01 % (3315945)CaDiCaL version: 2.1.3 % 128.72/19.01 % (3315945)Termination reason: Instruction limit % 128.72/19.01 % (3315945)Termination phase: Saturation % 128.72/19.01 % (3315945)Time elapsed: 0.971 s % 128.72/19.01 % (3315945)Peak memory usage: 136 MB % 128.72/19.01 % (3315945)Instructions burned: 1725 (million) % 128.72/19.01 % (3315949)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1824855384:st=2:i=4495:sd=10:ss=included_2901 on theBenchmark for (2901ds/4495Mi) % 128.72/19.01 % (3315935)Instruction limit reached! % 128.72/19.01 % (3315935)------------------------------ % 128.72/19.01 % (3315935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.72/19.01 % (3315935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.72/19.01 % (3315935)CaDiCaL version: 2.1.3 % 128.72/19.01 % (3315935)Termination reason: Instruction limit % 128.72/19.01 % (3315935)Termination phase: Saturation % 128.72/19.01 % (3315935)Time elapsed: 4.0000 s % 128.72/19.01 % (3315935)Peak memory usage: 219 MB % 128.72/19.01 % (3315935)Instructions burned: 6924 (million) % 128.72/19.01 % (3315951)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=977175035:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2897 on theBenchmark for (2897ds/4920Mi) % 128.72/19.01 % (3315941)Instruction limit reached! % 128.72/19.01 % (3315941)------------------------------ % 128.72/19.01 % (3315941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.72/19.01 % (3315941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.72/19.01 % (3315941)CaDiCaL version: 2.1.3 % 128.72/19.01 % (3315941)Termination reason: Instruction limit % 128.72/19.01 % (3315941)Termination phase: Saturation % 128.72/19.01 % (3315941)Time elapsed: 4.836 s % 128.72/19.01 % (3315941)Peak memory usage: 283 MB % 128.72/19.01 % (3315941)Instructions burned: 16415 (million) % 128.72/19.01 % (3315953)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=1045641137:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2880 on theBenchmark for (2880ds/2083Mi) % 128.72/19.01 % (3315949)Instruction limit reached! % 128.72/19.01 % (3315949)------------------------------ % 128.72/19.01 % (3315949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.72/19.01 % (3315949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.72/19.01 % (3315949)CaDiCaL version: 2.1.3 % 128.72/19.01 % (3315949)Termination reason: Instruction limit % 128.72/19.01 % (3315949)Termination phase: Saturation % 128.72/19.01 % (3315949)Time elapsed: 2.509 s % 128.72/19.01 % (3315949)Peak memory usage: 165 MB % 128.72/19.01 % (3315949)Instructions burned: 4496 (million) % 128.72/19.01 % (3315955)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=3870202151:i=4629:av=off:gsp=on_2874 on theBenchmark for (2874ds/4629Mi) % 128.72/19.01 % (3315953)Instruction limit reached! % 128.72/19.01 % (3315953)------------------------------ % 128.72/19.01 % (3315953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.72/19.01 % (3315953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.72/19.01 % (3315953)CaDiCaL version: 2.1.3 % 128.72/19.01 % (3315953)Termination reason: Instruction limit % 128.72/19.01 % (3315953)Termination phase: Saturation % 128.72/19.01 % (3315953)Time elapsed: 0.751 s % 128.72/19.01 % (3315953)Peak memory usage: 139 MB % 128.72/19.01 % (3315953)Instructions burned: 2083 (million) % 128.72/19.01 % (3315957)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=10512722:i=1258:av=off_2871 on theBenchmark for (2871ds/1258Mi) % 128.72/19.01 % (3315957)Instruction limit reached! % 128.72/19.01 % (3315957)------------------------------ % 128.72/19.01 % (3315957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 128.72/19.01 % (3315957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.38/21.68 % (3315957)CaDiCaL version: 2.1.3 % 148.38/21.68 % (3315957)Termination reason: Instruction limit % 148.38/21.68 % (3315957)Termination phase: Saturation % 148.38/21.68 % (3315957)Time elapsed: 0.373 s % 148.38/21.68 % (3315957)Peak memory usage: 101 MB % 148.38/21.68 % (3315957)Instructions burned: 1259 (million) % 148.38/21.68 % (3315959)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2610482301:i=7343:av=off:ss=included_2866 on theBenchmark for (2866ds/7343Mi) % 148.38/21.68 % (3315951)Instruction limit reached! % 148.38/21.68 % (3315951)------------------------------ % 148.38/21.68 % (3315951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.38/21.68 % (3315951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.38/21.68 % (3315951)CaDiCaL version: 2.1.3 % 148.38/21.68 % (3315951)Termination reason: Instruction limit % 148.38/21.68 % (3315951)Termination phase: Saturation % 148.38/21.68 % (3315951)Time elapsed: 3.108 s % 148.38/21.68 % (3315951)Peak memory usage: 158 MB % 148.38/21.68 % (3315951)Instructions burned: 4922 (million) % 148.38/21.68 % (3315961)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1084359808:i=1325:sd=2:ss=axioms:sgt=16_2864 on theBenchmark for (2864ds/1325Mi) % 148.38/21.68 % (3315961)Instruction limit reached! % 148.38/21.68 % (3315961)------------------------------ % 148.38/21.68 % (3315961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.38/21.68 % (3315961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.38/21.68 % (3315961)CaDiCaL version: 2.1.3 % 148.38/21.68 % (3315961)Termination reason: Instruction limit % 148.38/21.68 % (3315961)Termination phase: Saturation % 148.38/21.68 % (3315961)Time elapsed: 0.527 s % 148.38/21.68 % (3315961)Peak memory usage: 93 MB % 148.38/21.68 % (3315961)Instructions burned: 1325 (million) % 148.38/21.68 % (3315963)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=3389663796:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2857 on theBenchmark for (2857ds/2646Mi) % 148.38/21.68 % (3315947)Instruction limit reached! % 148.38/21.68 % (3315947)------------------------------ % 148.38/21.68 % (3315947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.38/21.68 % (3315947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.38/21.68 % (3315947)CaDiCaL version: 2.1.3 % 148.38/21.68 % (3315947)Termination reason: Instruction limit % 148.38/21.68 % (3315947)Termination phase: Saturation % 148.38/21.68 % (3315947)Time elapsed: 4.725 s % 148.38/21.68 % (3315947)Peak memory usage: 149 MB % 148.38/21.68 % (3315947)Instructions burned: 9530 (million) % 148.38/21.68 % (3316031)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1214073175:i=1489:sd=2:ep=R:ss=axioms_2855 on theBenchmark for (2855ds/1489Mi) % 148.38/21.68 % (3315955)Instruction limit reached! % 148.38/21.68 % (3315955)------------------------------ % 148.38/21.68 % (3315955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.38/21.68 % (3315955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.38/21.68 % (3315955)CaDiCaL version: 2.1.3 % 148.38/21.68 % (3315955)Termination reason: Instruction limit % 148.38/21.68 % (3315955)Termination phase: Saturation % 148.38/21.68 % (3315955)Time elapsed: 2.105 s % 148.38/21.68 % (3315955)Peak memory usage: 164 MB % 148.38/21.68 % (3315955)Instructions burned: 4631 (million) % 148.38/21.68 % (3316119)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=1701797819:i=1503_2851 on theBenchmark for (2851ds/1503Mi) % 148.38/21.68 % (3315959)Instruction limit reached! % 148.38/21.68 % (3315959)------------------------------ % 148.38/21.68 % (3315959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.38/21.68 % (3315959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.38/21.68 % (3315959)CaDiCaL version: 2.1.3 % 148.38/21.68 % (3315959)Termination reason: Instruction limit % 148.38/21.68 % (3315959)Termination phase: Saturation % 148.38/21.68 % (3315959)Time elapsed: 2.011 s % 148.38/21.68 % (3315959)Peak memory usage: 151 MB % 148.38/21.68 % (3315959)Instructions burned: 7349 (million) % 148.38/21.68 % (3316121)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3177053882:i=13942:kws=frequency_2844 on theBenchmark for (2844ds/13942Mi) % 148.38/21.68 % (3316031)Instruction limit reached! % 148.38/21.68 % (3316031)------------------------------ % 167.13/24.23 % (3316031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.13/24.23 % (3316031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.13/24.23 % (3316031)CaDiCaL version: 2.1.3 % 167.13/24.23 % (3316031)Termination reason: Instruction limit % 167.13/24.23 % (3316031)Termination phase: Saturation % 167.13/24.23 % (3316031)Time elapsed: 1.010 s % 167.13/24.23 % (3316031)Peak memory usage: 137 MB % 167.13/24.23 % (3316031)Instructions burned: 1489 (million) % 167.13/24.23 % (3316123)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=4062849449:i=3604:fsr=off:er=filter_2843 on theBenchmark for (2843ds/3604Mi) % 167.13/24.23 % (3315963)Instruction limit reached! % 167.13/24.23 % (3315963)------------------------------ % 167.13/24.23 % (3315963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.13/24.23 % (3315963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.13/24.23 % (3315963)CaDiCaL version: 2.1.3 % 167.13/24.23 % (3315963)Termination reason: Instruction limit % 167.13/24.23 % (3315963)Termination phase: Saturation % 167.13/24.23 % (3315963)Time elapsed: 1.457 s % 167.13/24.23 % (3315963)Peak memory usage: 140 MB % 167.13/24.23 % (3315963)Instructions burned: 2646 (million) % 167.13/24.23 % (3316119)Instruction limit reached! % 167.13/24.23 % (3316119)------------------------------ % 167.13/24.23 % (3316119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.13/24.23 % (3316119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.13/24.23 % (3316119)CaDiCaL version: 2.1.3 % 167.13/24.23 % (3316119)Termination reason: Instruction limit % 167.13/24.23 % (3316119)Termination phase: Saturation % 167.13/24.23 % (3316119)Time elapsed: 0.976 s % 167.13/24.23 % (3316119)Peak memory usage: 136 MB % 167.13/24.23 % (3316119)Instructions burned: 1503 (million) % 167.13/24.23 % (3316125)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2605531711:i=1876:sd=1:ss=included:sgt=32_2841 on theBenchmark for (2841ds/1876Mi) % 167.13/24.23 % (3316126)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=881363327:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2840 on theBenchmark for (2840ds/1932Mi) % 167.13/24.23 % (3316125)Instruction limit reached! % 167.13/24.23 % (3316125)------------------------------ % 167.13/24.23 % (3316125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.13/24.23 % (3316125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.13/24.23 % (3316125)CaDiCaL version: 2.1.3 % 167.13/24.23 % (3316125)Termination reason: Instruction limit % 167.13/24.23 % (3316125)Termination phase: Saturation % 167.13/24.23 % (3316125)Time elapsed: 1.083 s % 167.13/24.23 % (3316125)Peak memory usage: 138 MB % 167.13/24.23 % (3316125)Instructions burned: 1878 (million) % 167.13/24.23 % (3316129)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=3051795487:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2828 on theBenchmark for (2828ds/1980Mi) % 167.13/24.23 % (3316126)Instruction limit reached! % 167.13/24.23 % (3316126)------------------------------ % 167.13/24.23 % (3316126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.13/24.23 % (3316126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.13/24.23 % (3316126)CaDiCaL version: 2.1.3 % 167.13/24.23 % (3316126)Termination reason: Instruction limit % 167.13/24.23 % (3316126)Termination phase: Saturation % 167.13/24.23 % (3316126)Time elapsed: 1.267 s % 167.13/24.23 % (3316126)Peak memory usage: 139 MB % 167.13/24.23 % (3316126)Instructions burned: 1932 (million) % 167.13/24.23 % (3316131)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=3590544003:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2825 on theBenchmark for (2825ds/3902Mi) % 167.13/24.23 % (3316123)Instruction limit reached! % 167.13/24.23 % (3316123)------------------------------ % 167.13/24.23 % (3316123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.13/24.23 % (3316123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.13/24.23 % (3316123)CaDiCaL version: 2.1.3 % 167.13/24.23 % (3316123)Termination reason: Instruction limit % 195.49/28.24 % (3316123)Termination phase: Saturation % 195.49/28.24 % (3316123)Time elapsed: 2.530 s % 195.49/28.24 % (3316123)Peak memory usage: 150 MB % 195.49/28.24 % (3316123)Instructions burned: 3604 (million) % 195.49/28.24 % (3316129)Instruction limit reached! % 195.49/28.24 % (3316129)------------------------------ % 195.49/28.24 % (3316129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.49/28.24 % (3316129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.49/28.24 % (3316129)CaDiCaL version: 2.1.3 % 195.49/28.24 % (3316129)Termination reason: Instruction limit % 195.49/28.24 % (3316129)Termination phase: Saturation % 195.49/28.24 % (3316129)Time elapsed: 1.149 s % 195.49/28.24 % (3316129)Peak memory usage: 146 MB % 195.49/28.24 % (3316129)Instructions burned: 1981 (million) % 195.49/28.24 % (3316133)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1333400160:avsq=on:i=3916:aac=none:amm=off_2816 on theBenchmark for (2816ds/3916Mi) % 195.49/28.24 % (3316134)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=1386377205:cond=on:i=3940:av=off:er=known_2815 on theBenchmark for (2815ds/3940Mi) % 195.49/28.24 % (3316121)Instruction limit reached! % 195.49/28.24 % (3316121)------------------------------ % 195.49/28.24 % (3316121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.49/28.24 % (3316121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.49/28.24 % (3316121)CaDiCaL version: 2.1.3 % 195.49/28.24 % (3316121)Termination reason: Instruction limit % 195.49/28.24 % (3316121)Termination phase: Saturation % 195.49/28.24 % (3316121)Time elapsed: 4.040 s % 195.49/28.24 % (3316121)Peak memory usage: 176 MB % 195.49/28.24 % (3316121)Instructions burned: 13945 (million) % 195.49/28.24 % (3316137)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=258236437:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2803 on theBenchmark for (2803ds/3980Mi) % 195.49/28.24 % (3316131)Instruction limit reached! % 195.49/28.24 % (3316131)------------------------------ % 195.49/28.24 % (3316131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.49/28.24 % (3316131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.49/28.24 % (3316131)CaDiCaL version: 2.1.3 % 195.49/28.24 % (3316131)Termination reason: Instruction limit % 195.49/28.24 % (3316131)Termination phase: Saturation % 195.49/28.24 % (3316131)Time elapsed: 2.752 s % 195.49/28.24 % (3316131)Peak memory usage: 153 MB % 195.49/28.24 % (3316131)Instructions burned: 3902 (million) % 195.49/28.24 % (3316139)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=3044765316:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2796 on theBenchmark for (2796ds/2087Mi) % 195.49/28.24 % (3316134)Instruction limit reached! % 195.49/28.24 % (3316134)------------------------------ % 195.49/28.24 % (3316134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.49/28.24 % (3316134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.49/28.24 % (3316134)CaDiCaL version: 2.1.3 % 195.49/28.24 % (3316134)Termination reason: Instruction limit % 195.49/28.24 % (3316134)Termination phase: Saturation % 195.49/28.24 % (3316134)Time elapsed: 2.064 s % 195.49/28.24 % (3316134)Peak memory usage: 141 MB % 195.49/28.24 % (3316134)Instructions burned: 3941 (million) % 195.49/28.24 % (3316141)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=2793120649:cts=off:cond=on:i=4272:bs=on:fsd=on_2793 on theBenchmark for (2793ds/4272Mi) % 195.49/28.24 % (3316133)Instruction limit reached! % 195.49/28.24 % (3316133)------------------------------ % 195.49/28.24 % (3316133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.49/28.24 % (3316133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.49/28.24 % (3316133)CaDiCaL version: 2.1.3 % 195.49/28.24 % (3316133)Termination reason: Instruction limit % 195.49/28.24 % (3316133)Termination phase: Saturation % 195.49/28.24 % (3316133)Time elapsed: 2.338 s % 195.49/28.24 % (3316133)Peak memory usage: 117 MB % 195.49/28.24 % (3316133)Instructions burned: 3917 (million) % 195.49/28.24 % (3316143)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=459299230:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2791 on theBenchmark for (2791ds/2197Mi) % 251.07/36.10 % (3316137)Instruction limit reached! % 251.07/36.10 % (3316137)------------------------------ % 251.07/36.10 % (3316137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.07/36.10 % (3316137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.07/36.10 % (3316137)CaDiCaL version: 2.1.3 % 251.07/36.10 % (3316137)Termination reason: Instruction limit % 251.07/36.10 % (3316137)Termination phase: Saturation % 251.07/36.10 % (3316137)Time elapsed: 1.205 s % 251.07/36.10 % (3316137)Peak memory usage: 161 MB % 251.07/36.10 % (3316137)Instructions burned: 3982 (million) % 251.07/36.10 % (3316145)dis+21_1_sil=8000:spb=goal_then_units:random_seed=893776427:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2789 on theBenchmark for (2789ds/6508Mi) % 251.07/36.10 % (3316139)Instruction limit reached! % 251.07/36.10 % (3316139)------------------------------ % 251.07/36.10 % (3316139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.07/36.10 % (3316139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.07/36.10 % (3316139)CaDiCaL version: 2.1.3 % 251.07/36.10 % (3316139)Termination reason: Instruction limit % 251.07/36.10 % (3316139)Termination phase: Saturation % 251.07/36.10 % (3316139)Time elapsed: 1.323 s % 251.07/36.10 % (3316139)Peak memory usage: 140 MB % 251.07/36.10 % (3316139)Instructions burned: 2089 (million) % 251.07/36.10 % (3316147)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=85644247:i=2330:fgj=on:av=off:fsr=off_2781 on theBenchmark for (2781ds/2330Mi) % 251.07/36.10 % (3316143)Instruction limit reached! % 251.07/36.10 % (3316143)------------------------------ % 251.07/36.10 % (3316143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.07/36.10 % (3316143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.07/36.10 % (3316143)CaDiCaL version: 2.1.3 % 251.07/36.10 % (3316143)Termination reason: Instruction limit % 251.07/36.10 % (3316143)Termination phase: Saturation % 251.07/36.10 % (3316143)Time elapsed: 1.480 s % 251.07/36.10 % (3316143)Peak memory usage: 141 MB % 251.07/36.10 % (3316143)Instructions burned: 2198 (million) % 251.07/36.10 % (3316145)Instruction limit reached! % 251.07/36.10 % (3316145)------------------------------ % 251.07/36.10 % (3316145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.07/36.10 % (3316145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.07/36.10 % (3316145)CaDiCaL version: 2.1.3 % 251.07/36.10 % (3316145)Termination reason: Instruction limit % 251.07/36.10 % (3316145)Termination phase: Saturation % 251.07/36.10 % (3316145)Time elapsed: 1.457 s % 251.07/36.10 % (3316145)Peak memory usage: 102 MB % 251.07/36.10 % (3316145)Instructions burned: 6510 (million) % 251.07/36.10 % (3316149)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2555251266:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2774 on theBenchmark for (2774ds/7592Mi) % 251.07/36.10 % (3316150)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=3021393661:i=2693:kws=precedence:ins=1:av=off_2773 on theBenchmark for (2773ds/2693Mi) % 251.07/36.10 % (3316147)Instruction limit reached! % 251.07/36.10 % (3316147)------------------------------ % 251.07/36.10 % (3316147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.07/36.10 % (3316147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.07/36.10 % (3316147)CaDiCaL version: 2.1.3 % 251.07/36.10 % (3316147)Termination reason: Instruction limit % 251.07/36.10 % (3316147)Termination phase: Saturation % 251.07/36.10 % (3316147)Time elapsed: 1.342 s % 251.07/36.10 % (3316147)Peak memory usage: 141 MB % 251.07/36.10 % (3316147)Instructions burned: 2332 (million) % 251.07/36.10 % (3316153)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2898657329:i=28651:sd=4:ss=included:sgt=64_2766 on theBenchmark for (2766ds/28651Mi) % 251.07/36.10 % (3316141)Instruction limit reached! % 251.07/36.10 % (3316141)------------------------------ % 251.07/36.10 % (3316141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.07/36.10 % (3316141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.07/36.10 % (3316141)CaDiCaL version: 2.1.3 % 251.07/36.10 % (3316141)Termination reason: Instruction limit % 251.07/36.10 % (3316141)Termination phase: Saturation % 251.07/36.10 % (3316141)Time elapsed: 2.727 s % 251.07/36.10 % (3316141)Peak memory usage: 149 MB % 251.07/36.10 % (3316141)Instructions burned: 4274 (million) % 300.76/43.06 % (3316150)Instruction limit reached! % 300.76/43.06 % (3316150)------------------------------ % 300.76/43.06 % (3316150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.06 % (3316150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.06 % (3316150)CaDiCaL version: 2.1.3 % 300.76/43.06 % (3316150)Termination reason: Instruction limit % 300.76/43.06 % (3316150)Termination phase: Saturation % 300.76/43.06 % (3316150)Time elapsed: 0.918 s % 300.76/43.06 % (3316150)Peak memory usage: 152 MB % 300.76/43.06 % (3316150)Instructions burned: 2694 (million) % 300.76/43.06 % (3316155)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1171007992:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2764 on theBenchmark for (2764ds/2700Mi) % 300.76/43.06 % (3316156)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=2835600747:i=3196:nm=4_2763 on theBenchmark for (2763ds/3196Mi) % 300.76/43.06 % (3316156)Instruction limit reached! % 300.76/43.06 % (3316156)------------------------------ % 300.76/43.06 % (3316156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.06 % (3316156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.06 % (3316156)CaDiCaL version: 2.1.3 % 300.76/43.06 % (3316156)Termination reason: Instruction limit % 300.76/43.06 % (3316156)Termination phase: Saturation % 300.76/43.06 % (3316156)Time elapsed: 1.209 s % 300.76/43.06 % (3316156)Peak memory usage: 148 MB % 300.76/43.06 % (3316156)Instructions burned: 3197 (million) % 300.76/43.06 % (3316159)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3074882916:cts=off:i=3254:av=off_2750 on theBenchmark for (2750ds/3254Mi) % 300.76/43.06 % (3316155)Instruction limit reached! % 300.76/43.06 % (3316155)------------------------------ % 300.76/43.06 % (3316155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.06 % (3316155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.06 % (3316155)CaDiCaL version: 2.1.3 % 300.76/43.06 % (3316155)Termination reason: Instruction limit % 300.76/43.06 % (3316155)Termination phase: Saturation % 300.76/43.06 % (3316155)Time elapsed: 1.652 s % 300.76/43.06 % (3316155)Peak memory usage: 147 MB % 300.76/43.06 % (3316155)Instructions burned: 2700 (million) % 300.76/43.06 % (3316161)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=887550767:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2746 on theBenchmark for (2746ds/3264Mi) % 300.76/43.06 % (3316159)Instruction limit reached! % 300.76/43.06 % (3316159)------------------------------ % 300.76/43.06 % (3316159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.06 % (3316159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.06 % (3316159)CaDiCaL version: 2.1.3 % 300.76/43.06 % (3316159)Termination reason: Instruction limit % 300.76/43.06 % (3316159)Termination phase: Saturation % 300.76/43.06 % (3316159)Time elapsed: 1.080 s % 300.76/43.06 % (3316159)Peak memory usage: 143 MB % 300.76/43.06 % (3316159)Instructions burned: 3255 (million) % 300.76/43.06 % (3316163)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=3308274195:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2738 on theBenchmark for (2738ds/9708Mi) % 300.76/43.06 % (3316149)Instruction limit reached! % 300.76/43.06 % (3316149)------------------------------ % 300.76/43.06 % (3316149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.06 % (3316149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.06 % (3316149)CaDiCaL version: 2.1.3 % 300.76/43.06 % (3316149)Termination reason: Instruction limit % 300.76/43.06 % (3316149)Termination phase: Saturation % 300.76/43.06 % (3316149)Time elapsed: 3.913 s % 300.76/43.06 % (3316149)Peak memory usage: 125 MB % 300.76/43.06 % (3316149)Instructions burned: 7592 (million) % 300.76/43.06 % (3316165)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3840842285:i=21997:s2at=5:gtg=all_2734 on theBenchmark for (2734ds/21997Mi) % 300.76/43.06 % (3316161)Instruction limit reached! % 300.76/43.06 % (3316161)------------------------------ % 300.76/43.06 % (3316161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.07 Terminated %------------------------------------------------------------------------------