%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV723-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n001.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:19:20 PM UTC 2026 % Result : Timeout 301.04s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV723-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.18 % Computer : n001.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 12:27:48 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 10.95/2.27 % (313747)Input is clausal, will run a generic CNF schedule. % 10.95/2.27 % (313753)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3708978540:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 10.95/2.27 % (313755)lrs+10_1_sil=8000:sp=occurrence:random_seed=198622411:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 10.95/2.27 % (313756)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=386863610:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 10.95/2.27 % (313757)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2378406666:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 10.95/2.27 % (313752)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=2007812025:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 10.95/2.27 % (313758)dis-21_1_sil=8000:lcm=predicate:random_seed=2452916420: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) % 10.95/2.27 % (313754)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1880992682:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 10.95/2.27 % (313758)Instruction limit reached! % 10.95/2.27 % (313758)------------------------------ % 10.95/2.27 % (313758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.95/2.27 % (313758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.95/2.27 % (313758)CaDiCaL version: 2.1.3 % 10.95/2.27 % (313758)Termination reason: Instruction limit % 10.95/2.27 % (313758)Termination phase: Saturation % 10.95/2.27 % (313758)Time elapsed: 0.067 s % 10.95/2.27 % (313758)Peak memory usage: 89 MB % 10.95/2.27 % (313758)Instructions burned: 117 (million) % 10.95/2.27 % (313755)Instruction limit reached! % 10.95/2.27 % (313755)------------------------------ % 10.95/2.27 % (313755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.95/2.27 % (313755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.95/2.27 % (313755)CaDiCaL version: 2.1.3 % 10.95/2.27 % (313755)Termination reason: Instruction limit % 10.95/2.27 % (313755)Termination phase: Saturation % 10.95/2.27 % (313755)Time elapsed: 0.074 s % 10.95/2.27 % (313755)Peak memory usage: 90 MB % 10.95/2.27 % (313755)Instructions burned: 108 (million) % 10.95/2.27 % (313756)Instruction limit reached! % 10.95/2.27 % (313756)------------------------------ % 10.95/2.27 % (313756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.95/2.27 % (313756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.95/2.27 % (313756)CaDiCaL version: 2.1.3 % 10.95/2.27 % (313756)Termination reason: Instruction limit % 10.95/2.27 % (313756)Termination phase: Saturation % 10.95/2.27 % (313756)Time elapsed: 0.078 s % 10.95/2.27 % (313756)Peak memory usage: 89 MB % 10.95/2.27 % (313756)Instructions burned: 114 (million) % 10.95/2.27 % (313757)Instruction limit reached! % 10.95/2.27 % (313757)------------------------------ % 10.95/2.27 % (313757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.95/2.27 % (313757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.95/2.27 % (313757)CaDiCaL version: 2.1.3 % 10.95/2.27 % (313757)Termination reason: Instruction limit % 10.95/2.27 % (313757)Termination phase: Saturation % 10.95/2.27 % (313757)Time elapsed: 0.116 s % 10.95/2.27 % (313757)Peak memory usage: 90 MB % 10.95/2.27 % (313757)Instructions burned: 181 (million) % 10.95/2.27 % (313767)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1268459978: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) % 10.95/2.27 % (313766)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=1110530931:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 10.95/2.27 % (313768)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3417063154:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 10.95/2.27 % (313766)Refutation not found, incomplete strategy % 10.95/2.27 % (313766)------------------------------ % 10.95/2.27 % (313766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.95/2.27 % (313766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.08/4.02 % (313766)CaDiCaL version: 2.1.3 % 22.08/4.02 % (313766)Termination reason: Refutation not found, incomplete strategy % 22.08/4.02 % (313766)Time elapsed: 0.017 s % 22.08/4.02 % (313766)Peak memory usage: 89 MB % 22.08/4.02 % (313766)Instructions burned: 26 (million) % 22.08/4.02 % (313768)Refutation not found, incomplete strategy % 22.08/4.02 % (313768)------------------------------ % 22.08/4.02 % (313768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.08/4.02 % (313768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.08/4.02 % (313768)CaDiCaL version: 2.1.3 % 22.08/4.02 % (313768)Termination reason: Refutation not found, incomplete strategy % 22.08/4.02 % (313768)Time elapsed: 0.018 s % 22.08/4.02 % (313768)Peak memory usage: 89 MB % 22.08/4.02 % (313768)Instructions burned: 29 (million) % 22.08/4.02 % (313769)lrs+10_64_to=lpo:sil=8000:random_seed=1193404409:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 22.08/4.02 % (313767)Instruction limit reached! % 22.08/4.02 % (313767)------------------------------ % 22.08/4.02 % (313767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.08/4.02 % (313767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.08/4.02 % (313767)CaDiCaL version: 2.1.3 % 22.08/4.02 % (313767)Termination reason: Instruction limit % 22.08/4.02 % (313767)Termination phase: Saturation % 22.08/4.02 % (313767)Time elapsed: 0.106 s % 22.08/4.02 % (313767)Peak memory usage: 91 MB % 22.08/4.02 % (313767)Instructions burned: 189 (million) % 22.08/4.02 % (313769)Instruction limit reached! % 22.08/4.02 % (313769)------------------------------ % 22.08/4.02 % (313769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.08/4.02 % (313769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.08/4.02 % (313769)CaDiCaL version: 2.1.3 % 22.08/4.02 % (313769)Termination reason: Instruction limit % 22.08/4.02 % (313769)Termination phase: Saturation % 22.08/4.02 % (313769)Time elapsed: 0.076 s % 22.08/4.02 % (313769)Peak memory usage: 90 MB % 22.08/4.02 % (313769)Instructions burned: 126 (million) % 22.08/4.02 % (313774)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=924132844:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 22.08/4.02 % (313775)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1013087448:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 22.08/4.02 % (313766)------------------------------ % 22.08/4.02 % (313766)------------------------------ % 22.08/4.02 % (313768)------------------------------ % 22.08/4.02 % (313768)------------------------------ % 22.08/4.02 % (313775)Instruction limit reached! % 22.08/4.02 % (313775)------------------------------ % 22.08/4.02 % (313775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.08/4.02 % (313775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.08/4.02 % (313775)CaDiCaL version: 2.1.3 % 22.08/4.02 % (313775)Termination reason: Instruction limit % 22.08/4.02 % (313775)Termination phase: Saturation % 22.08/4.02 % (313775)Time elapsed: 0.106 s % 22.08/4.02 % (313775)Peak memory usage: 91 MB % 22.08/4.02 % (313775)Instructions burned: 157 (million) % 22.08/4.02 % (313774)Instruction limit reached! % 22.08/4.02 % (313774)------------------------------ % 22.08/4.02 % (313774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.08/4.02 % (313774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.08/4.02 % (313774)CaDiCaL version: 2.1.3 % 22.08/4.02 % (313774)Termination reason: Instruction limit % 22.08/4.02 % (313774)Termination phase: Saturation % 22.08/4.02 % (313774)Time elapsed: 0.120 s % 22.08/4.02 % (313774)Peak memory usage: 91 MB % 22.08/4.02 % (313774)Instructions burned: 196 (million) % 22.08/4.02 % (313779)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=1275731284:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 22.08/4.02 % (313778)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3219407153:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi) % 22.08/4.02 % (313779)Instruction limit reached! % 22.08/4.02 % (313779)------------------------------ % 22.08/4.02 % (313779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.08/4.02 % (313779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.98/6.80 % (313779)CaDiCaL version: 2.1.3 % 42.98/6.80 % (313779)Termination reason: Instruction limit % 42.98/6.80 % (313779)Termination phase: Saturation % 42.98/6.80 % (313779)Time elapsed: 0.059 s % 42.98/6.80 % (313779)Peak memory usage: 89 MB % 42.98/6.80 % (313779)Instructions burned: 107 (million) % 42.98/6.80 % (313780)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2821666310:i=107_2992 on theBenchmark for (2992ds/107Mi) % 42.98/6.80 % (313781)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3351225599:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 42.98/6.80 % (313780)Instruction limit reached! % 42.98/6.80 % (313780)------------------------------ % 42.98/6.80 % (313780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.98/6.80 % (313780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.98/6.80 % (313780)CaDiCaL version: 2.1.3 % 42.98/6.80 % (313780)Termination reason: Instruction limit % 42.98/6.80 % (313780)Termination phase: Saturation % 42.98/6.80 % (313780)Time elapsed: 0.066 s % 42.98/6.80 % (313780)Peak memory usage: 90 MB % 42.98/6.80 % (313780)Instructions burned: 108 (million) % 42.98/6.80 % (313784)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3864920867:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 42.98/6.80 % (313781)Instruction limit reached! % 42.98/6.80 % (313781)------------------------------ % 42.98/6.80 % (313781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.98/6.80 % (313781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.98/6.80 % (313781)CaDiCaL version: 2.1.3 % 42.98/6.80 % (313781)Termination reason: Instruction limit % 42.98/6.80 % (313781)Termination phase: Saturation % 42.98/6.80 % (313781)Time elapsed: 0.152 s % 42.98/6.80 % (313781)Peak memory usage: 90 MB % 42.98/6.80 % (313781)Instructions burned: 242 (million) % 42.98/6.80 % (313787)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3762812561:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi) % 42.98/6.80 % (313787)Instruction limit reached! % 42.98/6.80 % (313787)------------------------------ % 42.98/6.80 % (313787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.98/6.80 % (313787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.98/6.80 % (313787)CaDiCaL version: 2.1.3 % 42.98/6.80 % (313787)Termination reason: Instruction limit % 42.98/6.80 % (313787)Termination phase: Saturation % 42.98/6.80 % (313787)Time elapsed: 0.089 s % 42.98/6.80 % (313787)Peak memory usage: 90 MB % 42.98/6.80 % (313787)Instructions burned: 135 (million) % 42.98/6.80 % (313789)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2168822780:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 42.98/6.80 % (313791)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4051555586:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi) % 42.98/6.80 % (313791)Instruction limit reached! % 42.98/6.80 % (313791)------------------------------ % 42.98/6.80 % (313791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.98/6.80 % (313791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.98/6.80 % (313791)CaDiCaL version: 2.1.3 % 42.98/6.80 % (313791)Termination reason: Instruction limit % 42.98/6.80 % (313791)Termination phase: Saturation % 42.98/6.80 % (313791)Time elapsed: 0.126 s % 42.98/6.80 % (313791)Peak memory usage: 91 MB % 42.98/6.80 % (313791)Instructions burned: 193 (million) % 42.98/6.80 % (313789)Instruction limit reached! % 42.98/6.80 % (313789)------------------------------ % 42.98/6.80 % (313789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.98/6.80 % (313789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.98/6.80 % (313789)CaDiCaL version: 2.1.3 % 42.98/6.80 % (313789)Termination reason: Instruction limit % 42.98/6.80 % (313789)Termination phase: Saturation % 42.98/6.80 % (313789)Time elapsed: 0.314 s % 42.98/6.80 % (313789)Peak memory usage: 96 MB % 42.98/6.80 % (313789)Instructions burned: 500 (million) % 42.98/6.80 % (313794)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3934475711:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi) % 42.98/6.80 % (313795)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1705982404:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi) % 59.50/9.03 % (313795)Instruction limit reached! % 59.50/9.03 % (313795)------------------------------ % 59.50/9.03 % (313795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.50/9.03 % (313795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.50/9.03 % (313795)CaDiCaL version: 2.1.3 % 59.50/9.03 % (313795)Termination reason: Instruction limit % 59.50/9.03 % (313795)Termination phase: Saturation % 59.50/9.03 % (313795)Time elapsed: 0.106 s % 59.50/9.03 % (313795)Peak memory usage: 90 MB % 59.50/9.03 % (313795)Instructions burned: 157 (million) % 59.50/9.03 % (313794)Instruction limit reached! % 59.50/9.03 % (313794)------------------------------ % 59.50/9.03 % (313794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.50/9.03 % (313794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.50/9.03 % (313794)CaDiCaL version: 2.1.3 % 59.50/9.03 % (313794)Termination reason: Instruction limit % 59.50/9.03 % (313794)Termination phase: Saturation % 59.50/9.03 % (313794)Time elapsed: 0.170 s % 59.50/9.03 % (313794)Peak memory usage: 91 MB % 59.50/9.03 % (313794)Instructions burned: 265 (million) % 59.50/9.03 % (313798)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=650919208:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi) % 59.50/9.03 % (313799)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1480742022:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi) % 59.50/9.03 % (313799)Instruction limit reached! % 59.50/9.03 % (313799)------------------------------ % 59.50/9.03 % (313799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.50/9.03 % (313799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.50/9.03 % (313799)CaDiCaL version: 2.1.3 % 59.50/9.03 % (313799)Termination reason: Instruction limit % 59.50/9.03 % (313799)Termination phase: Saturation % 59.50/9.03 % (313799)Time elapsed: 0.287 s % 59.50/9.03 % (313799)Peak memory usage: 90 MB % 59.50/9.03 % (313799)Instructions burned: 538 (million) % 59.50/9.03 % (313802)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3081971356:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi) % 59.50/9.03 % (313802)Instruction limit reached! % 59.50/9.03 % (313802)------------------------------ % 59.50/9.03 % (313802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.50/9.03 % (313802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.50/9.03 % (313802)CaDiCaL version: 2.1.3 % 59.50/9.03 % (313802)Termination reason: Instruction limit % 59.50/9.03 % (313802)Termination phase: Saturation % 59.50/9.03 % (313802)Time elapsed: 0.097 s % 59.50/9.03 % (313802)Peak memory usage: 90 MB % 59.50/9.03 % (313802)Instructions burned: 181 (million) % 59.50/9.03 % (313804)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=1582197342:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi) % 59.50/9.03 % (313778)Instruction limit reached! % 59.50/9.03 % (313778)------------------------------ % 59.50/9.03 % (313778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.50/9.03 % (313778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.50/9.03 % (313778)CaDiCaL version: 2.1.3 % 59.50/9.03 % (313778)Termination reason: Instruction limit % 59.50/9.03 % (313778)Termination phase: Saturation % 59.50/9.03 % (313778)Time elapsed: 2.213 s % 59.50/9.03 % (313778)Peak memory usage: 150 MB % 59.50/9.03 % (313778)Instructions burned: 3394 (million) % 59.50/9.03 % (313806)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=775424840:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi) % 59.50/9.03 % (313806)Instruction limit reached! % 59.50/9.03 % (313806)------------------------------ % 59.50/9.03 % (313806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.50/9.03 % (313806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.50/9.03 % (313806)CaDiCaL version: 2.1.3 % 59.50/9.03 % (313806)Termination reason: Instruction limit % 59.50/9.03 % (313806)Termination phase: Saturation % 59.50/9.03 % (313806)Time elapsed: 0.237 s % 59.50/9.03 % (313806)Peak memory usage: 91 MB % 86.79/12.95 % (313806)Instructions burned: 413 (million) % 86.79/12.95 % (313808)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=2305215945:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi) % 86.79/12.95 % (313798)Instruction limit reached! % 86.79/12.95 % (313798)------------------------------ % 86.79/12.95 % (313798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.79/12.95 % (313798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.79/12.95 % (313798)CaDiCaL version: 2.1.3 % 86.79/12.95 % (313798)Termination reason: Instruction limit % 86.79/12.95 % (313798)Termination phase: Saturation % 86.79/12.95 % (313798)Time elapsed: 1.970 s % 86.79/12.95 % (313798)Peak memory usage: 151 MB % 86.79/12.95 % (313798)Instructions burned: 3257 (million) % 86.79/12.95 % (313810)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=1631073685:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2961 on theBenchmark for (2961ds/303Mi) % 86.79/12.95 % (313810)Instruction limit reached! % 86.79/12.95 % (313810)------------------------------ % 86.79/12.95 % (313810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.79/12.95 % (313810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.79/12.95 % (313810)CaDiCaL version: 2.1.3 % 86.79/12.95 % (313810)Termination reason: Instruction limit % 86.79/12.95 % (313810)Termination phase: Saturation % 86.79/12.95 % (313810)Time elapsed: 0.189 s % 86.79/12.95 % (313810)Peak memory usage: 93 MB % 86.79/12.95 % (313810)Instructions burned: 304 (million) % 86.79/12.95 % (313784)Instruction limit reached! % 86.79/12.95 % (313784)------------------------------ % 86.79/12.95 % (313784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.79/12.95 % (313784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.79/12.95 % (313784)CaDiCaL version: 2.1.3 % 86.79/12.95 % (313784)Termination reason: Instruction limit % 86.79/12.95 % (313784)Termination phase: Saturation % 86.79/12.95 % (313784)Time elapsed: 3.191 s % 86.79/12.95 % (313784)Peak memory usage: 163 MB % 86.79/12.95 % (313784)Instructions burned: 5209 (million) % 86.79/12.95 % (313812)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3213025275:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi) % 86.79/12.95 % (313813)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=509796986:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi) % 86.79/12.95 % (313812)Instruction limit reached! % 86.79/12.95 % (313812)------------------------------ % 86.79/12.95 % (313812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.79/12.95 % (313812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.79/12.95 % (313812)CaDiCaL version: 2.1.3 % 86.79/12.95 % (313812)Termination reason: Instruction limit % 86.79/12.95 % (313812)Termination phase: Saturation % 86.79/12.95 % (313812)Time elapsed: 0.397 s % 86.79/12.95 % (313812)Peak memory usage: 94 MB % 86.79/12.95 % (313812)Instructions burned: 721 (million) % 86.79/12.95 % (313813)Instruction limit reached! % 86.79/12.95 % (313813)------------------------------ % 86.79/12.95 % (313813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.79/12.95 % (313813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.79/12.95 % (313813)CaDiCaL version: 2.1.3 % 86.79/12.95 % (313813)Termination reason: Instruction limit % 86.79/12.95 % (313813)Termination phase: Saturation % 86.79/12.95 % (313813)Time elapsed: 0.388 s % 86.79/12.95 % (313813)Peak memory usage: 95 MB % 86.79/12.95 % (313813)Instructions burned: 598 (million) % 86.79/12.95 % (313816)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2480658960:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi) % 86.79/12.95 % (313817)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=143827647:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi) % 86.79/12.95 % (313817)Instruction limit reached! % 86.79/12.95 % (313817)------------------------------ % 86.79/12.95 % (313817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.79/12.95 % (313817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.76/20.87 % (313817)CaDiCaL version: 2.1.3 % 142.76/20.87 % (313817)Termination reason: Instruction limit % 142.76/20.87 % (313817)Termination phase: Saturation % 142.76/20.87 % (313817)Time elapsed: 1.296 s % 142.76/20.87 % (313817)Peak memory usage: 139 MB % 142.76/20.87 % (313817)Instructions burned: 1998 (million) % 142.76/20.87 % (313820)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=4193070534:i=2088:bd=preordered:av=off_2938 on theBenchmark for (2938ds/2088Mi) % 142.76/20.87 % (313816)Instruction limit reached! % 142.76/20.87 % (313816)------------------------------ % 142.76/20.87 % (313816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.76/20.87 % (313816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.76/20.87 % (313816)CaDiCaL version: 2.1.3 % 142.76/20.87 % (313816)Termination reason: Instruction limit % 142.76/20.87 % (313816)Termination phase: Saturation % 142.76/20.87 % (313816)Time elapsed: 1.879 s % 142.76/20.87 % (313816)Peak memory usage: 146 MB % 142.76/20.87 % (313816)Instructions burned: 2990 (million) % 142.76/20.87 % (313822)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=935711376:i=1098:nicw=on_2933 on theBenchmark for (2933ds/1098Mi) % 142.76/20.87 % (313822)Instruction limit reached! % 142.76/20.87 % (313822)------------------------------ % 142.76/20.87 % (313822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.76/20.87 % (313822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.76/20.87 % (313822)CaDiCaL version: 2.1.3 % 142.76/20.87 % (313822)Termination reason: Instruction limit % 142.76/20.87 % (313822)Termination phase: Saturation % 142.76/20.87 % (313822)Time elapsed: 0.645 s % 142.76/20.87 % (313822)Peak memory usage: 102 MB % 142.76/20.87 % (313822)Instructions burned: 1098 (million) % 142.76/20.87 % (313824)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2699665574:i=433:bd=preordered_2925 on theBenchmark for (2925ds/433Mi) % 142.76/20.87 % (313820)Instruction limit reached! % 142.76/20.87 % (313820)------------------------------ % 142.76/20.87 % (313820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.76/20.87 % (313820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.76/20.87 % (313820)CaDiCaL version: 2.1.3 % 142.76/20.87 % (313820)Termination reason: Instruction limit % 142.76/20.87 % (313820)Termination phase: Saturation % 142.76/20.87 % (313820)Time elapsed: 1.352 s % 142.76/20.87 % (313820)Peak memory usage: 139 MB % 142.76/20.87 % (313820)Instructions burned: 2088 (million) % 142.76/20.87 % (313826)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3563363027:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2923 on theBenchmark for (2923ds/2942Mi) % 142.76/20.87 % (313824)Instruction limit reached! % 142.76/20.87 % (313824)------------------------------ % 142.76/20.87 % (313824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.76/20.87 % (313824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.76/20.87 % (313824)CaDiCaL version: 2.1.3 % 142.76/20.87 % (313824)Termination reason: Instruction limit % 142.76/20.87 % (313824)Termination phase: Saturation % 142.76/20.87 % (313824)Time elapsed: 0.283 s % 142.76/20.87 % (313824)Peak memory usage: 95 MB % 142.76/20.87 % (313824)Instructions burned: 434 (million) % 142.76/20.87 % (313828)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3850904178:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2921 on theBenchmark for (2921ds/6922Mi) % 142.76/20.87 % (313808)Instruction limit reached! % 142.76/20.87 % (313808)------------------------------ % 142.76/20.87 % (313808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.76/20.87 % (313808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.76/20.87 % (313808)CaDiCaL version: 2.1.3 % 142.76/20.87 % (313808)Termination reason: Instruction limit % 142.76/20.87 % (313808)Termination phase: Saturation % 142.76/20.87 % (313808)Time elapsed: 4.736 s % 142.76/20.87 % (313808)Peak memory usage: 202 MB % 142.76/20.87 % (313808)Instructions burned: 8478 (million) % 142.76/20.87 % (313830)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=1678967031:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2917 on theBenchmark for (2917ds/596Mi) % 175.51/25.48 % (313830)Instruction limit reached! % 175.51/25.48 % (313830)------------------------------ % 175.51/25.48 % (313830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.51/25.48 % (313830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.51/25.48 % (313830)CaDiCaL version: 2.1.3 % 175.51/25.48 % (313830)Termination reason: Instruction limit % 175.51/25.48 % (313830)Termination phase: Saturation % 175.51/25.48 % (313830)Time elapsed: 0.342 s % 175.51/25.48 % (313830)Peak memory usage: 96 MB % 175.51/25.48 % (313830)Instructions burned: 597 (million) % 175.51/25.48 % (313832)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=1283741958:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2912 on theBenchmark for (2912ds/4123Mi) % 175.51/25.48 % (313804)Instruction limit reached! % 175.51/25.48 % (313804)------------------------------ % 175.51/25.48 % (313804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.51/25.48 % (313804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.51/25.48 % (313804)CaDiCaL version: 2.1.3 % 175.51/25.48 % (313804)Termination reason: Instruction limit % 175.51/25.48 % (313804)Termination phase: Saturation % 175.51/25.48 % (313804)Time elapsed: 6.965 s % 175.51/25.48 % (313804)Peak memory usage: 201 MB % 175.51/25.48 % (313804)Instructions burned: 10308 (million) % 175.51/25.48 % (313834)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1342230955:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2905 on theBenchmark for (2905ds/16411Mi) % 175.51/25.48 % (313826)Instruction limit reached! % 175.51/25.48 % (313826)------------------------------ % 175.51/25.48 % (313826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.51/25.48 % (313826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.51/25.48 % (313826)CaDiCaL version: 2.1.3 % 175.51/25.48 % (313826)Termination reason: Instruction limit % 175.51/25.48 % (313826)Termination phase: Saturation % 175.51/25.48 % (313826)Time elapsed: 2.047 s % 175.51/25.48 % (313826)Peak memory usage: 146 MB % 175.51/25.48 % (313826)Instructions burned: 2942 (million) % 175.51/25.48 % (313836)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1601104137:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2902 on theBenchmark for (2902ds/1670Mi) % 175.51/25.48 % (313836)Instruction limit reached! % 175.51/25.48 % (313836)------------------------------ % 175.51/25.48 % (313836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.51/25.48 % (313836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.51/25.48 % (313836)CaDiCaL version: 2.1.3 % 175.51/25.48 % (313836)Termination reason: Instruction limit % 175.51/25.48 % (313836)Termination phase: Saturation % 175.51/25.48 % (313836)Time elapsed: 1.087 s % 175.51/25.48 % (313836)Peak memory usage: 137 MB % 175.51/25.48 % (313836)Instructions burned: 1671 (million) % 175.51/25.48 % (313838)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=1528616023:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2889 on theBenchmark for (2889ds/1722Mi) % 175.51/25.48 % (313832)Instruction limit reached! % 175.51/25.48 % (313832)------------------------------ % 175.51/25.48 % (313832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.51/25.48 % (313832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.51/25.48 % (313832)CaDiCaL version: 2.1.3 % 175.51/25.48 % (313832)Termination reason: Instruction limit % 175.51/25.48 % (313832)Termination phase: Saturation % 175.51/25.48 % (313832)Time elapsed: 2.408 s % 175.51/25.48 % (313832)Peak memory usage: 161 MB % 175.51/25.48 % (313832)Instructions burned: 4123 (million) % 175.51/25.48 % (313840)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=367727510:cts=off:cond=on:i=9530:bs=on:fsd=on_2887 on theBenchmark for (2887ds/9530Mi) % 175.51/25.48 % (313828)Instruction limit reached! % 175.51/25.48 % (313828)------------------------------ % 175.51/25.48 % (313828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.51/25.48 % (313828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.51/25.48 % (313828)CaDiCaL version: 2.1.3 % 213.30/30.71 % (313828)Termination reason: Instruction limit % 213.30/30.71 % (313828)Termination phase: Saturation % 213.30/30.71 % (313828)Time elapsed: 4.245 s % 213.30/30.71 % (313828)Peak memory usage: 187 MB % 213.30/30.71 % (313828)Instructions burned: 6924 (million) % 213.30/30.71 % (313838)Instruction limit reached! % 213.30/30.71 % (313838)------------------------------ % 213.30/30.71 % (313838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.30/30.71 % (313838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.71 % (313838)CaDiCaL version: 2.1.3 % 213.30/30.71 % (313838)Termination reason: Instruction limit % 213.30/30.71 % (313838)Termination phase: Saturation % 213.30/30.71 % (313838)Time elapsed: 1.117 s % 213.30/30.71 % (313838)Peak memory usage: 136 MB % 213.30/30.71 % (313838)Instructions burned: 1723 (million) % 213.30/30.71 % (313842)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1678031835:st=2:i=4495:sd=10:ss=included_2877 on theBenchmark for (2877ds/4495Mi) % 213.30/30.71 % (313843)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=1729840822:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2877 on theBenchmark for (2877ds/4920Mi) % 213.30/30.71 % (313842)Instruction limit reached! % 213.30/30.71 % (313842)------------------------------ % 213.30/30.71 % (313842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.30/30.71 % (313842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.71 % (313842)CaDiCaL version: 2.1.3 % 213.30/30.71 % (313842)Termination reason: Instruction limit % 213.30/30.71 % (313842)Termination phase: Saturation % 213.30/30.71 % (313842)Time elapsed: 3.809 s % 213.30/30.71 % (313842)Peak memory usage: 160 MB % 213.30/30.71 % (313842)Instructions burned: 4495 (million) % 213.30/30.71 % (314157)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=54797185:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2837 on theBenchmark for (2837ds/2083Mi) % 213.30/30.71 % (313843)Instruction limit reached! % 213.30/30.71 % (313843)------------------------------ % 213.30/30.71 % (313843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.30/30.71 % (313843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.71 % (313843)CaDiCaL version: 2.1.3 % 213.30/30.71 % (313843)Termination reason: Instruction limit % 213.30/30.71 % (313843)Termination phase: Saturation % 213.30/30.71 % (313843)Time elapsed: 4.129 s % 213.30/30.71 % (313843)Peak memory usage: 162 MB % 213.30/30.71 % (313843)Instructions burned: 4920 (million) % 213.30/30.71 % (314159)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=88479394:i=4629:av=off:gsp=on_2834 on theBenchmark for (2834ds/4629Mi) % 213.30/30.71 % (314157)Instruction limit reached! % 213.30/30.71 % (314157)------------------------------ % 213.30/30.71 % (314157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.30/30.71 % (314157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.71 % (314157)CaDiCaL version: 2.1.3 % 213.30/30.71 % (314157)Termination reason: Instruction limit % 213.30/30.71 % (314157)Termination phase: Saturation % 213.30/30.71 % (314157)Time elapsed: 2.356 s % 213.30/30.71 % (314157)Peak memory usage: 138 MB % 213.30/30.71 % (314157)Instructions burned: 2083 (million) % 213.30/30.71 % (314169)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3389194683:i=1258:av=off_2811 on theBenchmark for (2811ds/1258Mi) % 213.30/30.71 % (313840)Instruction limit reached! % 213.30/30.71 % (313840)------------------------------ % 213.30/30.71 % (313840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.30/30.71 % (313840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.30/30.71 % (313840)CaDiCaL version: 2.1.3 % 213.30/30.71 % (313840)Termination reason: Instruction limit % 213.30/30.71 % (313840)Termination phase: Saturation % 213.30/30.71 % (313840)Time elapsed: 8.501 s % 213.30/30.71 % (313840)Peak memory usage: 188 MB % 213.30/30.71 % (313840)Instructions burned: 9530 (million) % 213.30/30.71 % (314171)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1649377119:i=7343:av=off:ss=included_2800 on theBenchmark for (2800ds/7343Mi) % 213.30/30.71 % (314169)Instruction limit reached! % 213.30/30.71 % (314169)------------------------------ % 213.30/30.71 % (314169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.20/37.61 % (314169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.20/37.61 % (314169)CaDiCaL version: 2.1.3 % 262.20/37.61 % (314169)Termination reason: Instruction limit % 262.20/37.61 % (314169)Termination phase: Saturation % 262.20/37.61 % (314169)Time elapsed: 1.131 s % 262.20/37.61 % (314169)Peak memory usage: 92 MB % 262.20/37.61 % (314169)Instructions burned: 1258 (million) % 262.20/37.61 % (314173)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3754001854:i=1325:sd=2:ss=axioms:sgt=16_2797 on theBenchmark for (2797ds/1325Mi) % 262.20/37.61 % (314173)Refutation not found, incomplete strategy % 262.20/37.61 % (314173)------------------------------ % 262.20/37.61 % (314173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.20/37.61 % (314173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.20/37.61 % (314173)CaDiCaL version: 2.1.3 % 262.20/37.61 % (314173)Termination reason: Refutation not found, incomplete strategy % 262.20/37.61 % (314173)Time elapsed: 0.029 s % 262.20/37.61 % (314173)Peak memory usage: 89 MB % 262.20/37.61 % (314173)Instructions burned: 28 (million) % 262.20/37.61 % (314173)------------------------------ % 262.20/37.61 % (314173)------------------------------ % 262.20/37.61 % (314177)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=1210431384:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2791 on theBenchmark for (2791ds/2646Mi) % 262.20/37.61 % (314159)Instruction limit reached! % 262.20/37.61 % (314159)------------------------------ % 262.20/37.61 % (314159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.20/37.61 % (314159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.20/37.61 % (314159)CaDiCaL version: 2.1.3 % 262.20/37.61 % (314159)Termination reason: Instruction limit % 262.20/37.61 % (314159)Termination phase: Saturation % 262.20/37.61 % (314159)Time elapsed: 4.628 s % 262.20/37.61 % (314159)Peak memory usage: 155 MB % 262.20/37.61 % (314159)Instructions burned: 4629 (million) % 262.20/37.61 % (314179)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=536144226:i=1489:sd=2:ep=R:ss=axioms_2785 on theBenchmark for (2785ds/1489Mi) % 262.20/37.61 % (314179)Instruction limit reached! % 262.20/37.61 % (314179)------------------------------ % 262.20/37.61 % (314179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.20/37.61 % (314179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.20/37.61 % (314179)CaDiCaL version: 2.1.3 % 262.20/37.61 % (314179)Termination reason: Instruction limit % 262.20/37.61 % (314179)Termination phase: Saturation % 262.20/37.61 % (314179)Time elapsed: 1.514 s % 262.20/37.61 % (314179)Peak memory usage: 135 MB % 262.20/37.61 % (314179)Instructions burned: 1489 (million) % 262.20/37.61 % (314187)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=967643706:i=1503_2768 on theBenchmark for (2768ds/1503Mi) % 262.20/37.61 % (314177)Instruction limit reached! % 262.20/37.61 % (314177)------------------------------ % 262.20/37.61 % (314177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.20/37.61 % (314177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.20/37.61 % (314177)CaDiCaL version: 2.1.3 % 262.20/37.61 % (314177)Termination reason: Instruction limit % 262.20/37.61 % (314177)Termination phase: Saturation % 262.20/37.61 % (314177)Time elapsed: 2.906 s % 262.20/37.61 % (314177)Peak memory usage: 143 MB % 262.20/37.61 % (314177)Instructions burned: 2647 (million) % 262.20/37.61 % (314189)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1561657356:i=13942:kws=frequency_2760 on theBenchmark for (2760ds/13942Mi) % 262.20/37.61 % (313834)Instruction limit reached! % 262.20/37.61 % (313834)------------------------------ % 262.20/37.61 % (313834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.20/37.61 % (313834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.20/37.61 % (313834)CaDiCaL version: 2.1.3 % 262.20/37.61 % (313834)Termination reason: Instruction limit % 262.20/37.61 % (313834)Termination phase: Saturation % 262.20/37.61 % (313834)Time elapsed: 14.956 s % 262.20/37.61 % (313834)Peak memory usage: 263 MB % 262.20/37.61 % (313834)Instructions burned: 16412 (million) % 262.20/37.61 % (314193)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=Terminated %------------------------------------------------------------------------------