%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : TOP031+3 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n007.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 02:33:56 PM UTC 2026 % Result : Timeout 300.26s 43.35s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP031+3 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.24 % Computer : n007.cluster.edu % 0.09/0.24 % Model : x86_64 x86_64 % 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.24 % Memory : 8046.5625MB % 0.09/0.24 % OS : Linux 6.8.0-71-generic % 0.09/0.24 % CPULimit : 300 % 0.09/0.24 % WCLimit : 300 % 0.09/0.24 % DateTime : Mon Sep 28 18:54:42 UTC 2026 % 0.09/0.25 % CPUTime : % 0.09/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.24/0.30 Running first-order theorem proving % 0.24/0.30 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 % 23.32/4.31 % (2692299)Detected formulas, will run a generic FOF schedule. % 23.32/4.31 % (2692307)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1343532171:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi) % 23.32/4.31 % (2692304)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=1954235809:i=141193_2995 on theBenchmark for (2995ds/141193Mi) % 23.32/4.31 % (2692310)dis-21_1_sil=8000:lcm=predicate:random_seed=289448434:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi) % 23.32/4.31 % (2692309)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1707642557:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi) % 23.32/4.31 % (2692305)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=680883929:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi) % 23.32/4.31 % (2692308)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4183004814:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi) % 23.32/4.31 % (2692306)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=530447128:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi) % 23.32/4.31 % (2692307)Instruction limit reached! % 23.32/4.31 % (2692307)------------------------------ % 23.32/4.31 % (2692307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.32/4.31 % (2692307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.32/4.31 % (2692307)CaDiCaL version: 2.1.3 % 23.32/4.31 % (2692307)Termination reason: Instruction limit % 23.32/4.31 % (2692307)Termination phase: Saturation % 23.32/4.31 % (2692307)Time elapsed: 0.083 s % 23.32/4.31 % (2692307)Peak memory usage: 107 MB % 23.32/4.31 % (2692307)Instructions burned: 110 (million) % 23.32/4.31 % (2692309)Instruction limit reached! % 23.32/4.31 % (2692309)------------------------------ % 23.32/4.31 % (2692309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.32/4.31 % (2692309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.32/4.31 % (2692309)CaDiCaL version: 2.1.3 % 23.32/4.31 % (2692309)Termination reason: Instruction limit % 23.32/4.31 % (2692309)Termination phase: Property scanning % 23.32/4.31 % (2692309)Time elapsed: 0.115 s % 23.32/4.31 % (2692309)Peak memory usage: 102 MB % 23.32/4.31 % (2692309)Instructions burned: 139 (million) % 23.32/4.31 % (2692310)Instruction limit reached! % 23.32/4.31 % (2692310)------------------------------ % 23.32/4.31 % (2692310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.32/4.31 % (2692310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.32/4.31 % (2692310)CaDiCaL version: 2.1.3 % 23.32/4.31 % (2692310)Termination reason: Instruction limit % 23.32/4.31 % (2692310)Termination phase: Preprocessing 1 % 23.32/4.31 % (2692310)Time elapsed: 0.140 s % 23.32/4.31 % (2692310)Peak memory usage: 103 MB % 23.32/4.31 % (2692310)Instructions burned: 129 (million) % 23.32/4.31 % (2692308)Instruction limit reached! % 23.32/4.31 % (2692308)------------------------------ % 23.32/4.31 % (2692308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.32/4.31 % (2692308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.32/4.31 % (2692308)CaDiCaL version: 2.1.3 % 23.32/4.31 % (2692308)Termination reason: Instruction limit % 23.32/4.31 % (2692308)Termination phase: Preprocessing 3 % 23.32/4.31 % (2692308)Time elapsed: 0.152 s % 23.32/4.31 % (2692308)Peak memory usage: 106 MB % 23.32/4.31 % (2692308)Instructions burned: 120 (million) % 23.32/4.31 % (2692318)lrs+10_1_sil=8000:sp=occurrence:random_seed=1710849885:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi) % 23.32/4.31 % (2692320)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3629438104:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi) % 23.32/4.31 % (2692319)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1500844330:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/157Mi) % 23.32/4.31 % (2692321)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1578913001:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi) % 23.32/4.31 % (2692318)Instruction limit reached! % 35.61/6.09 % (2692318)------------------------------ % 35.61/6.09 % (2692318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692318)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692318)Termination reason: Instruction limit % 35.61/6.09 % (2692318)Termination phase: Saturation % 35.61/6.09 % (2692318)Time elapsed: 0.151 s % 35.61/6.09 % (2692318)Peak memory usage: 110 MB % 35.61/6.09 % (2692318)Instructions burned: 286 (million) % 35.61/6.09 % (2692319)Instruction limit reached! % 35.61/6.09 % (2692319)------------------------------ % 35.61/6.09 % (2692319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692319)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692319)Termination reason: Instruction limit % 35.61/6.09 % (2692319)Termination phase: Property scanning % 35.61/6.09 % (2692319)Time elapsed: 0.129 s % 35.61/6.09 % (2692319)Peak memory usage: 102 MB % 35.61/6.09 % (2692319)Instructions burned: 157 (million) % 35.61/6.09 % (2692321)Instruction limit reached! % 35.61/6.09 % (2692321)------------------------------ % 35.61/6.09 % (2692321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692321)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692321)Termination reason: Instruction limit % 35.61/6.09 % (2692321)Termination phase: SInE selection % 35.61/6.09 % (2692321)Time elapsed: 0.210 s % 35.61/6.09 % (2692321)Peak memory usage: 103 MB % 35.61/6.09 % (2692321)Instructions burned: 249 (million) % 35.61/6.09 % (2692320)Instruction limit reached! % 35.61/6.09 % (2692320)------------------------------ % 35.61/6.09 % (2692320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692320)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692320)Termination reason: Instruction limit % 35.61/6.09 % (2692320)Termination phase: Saturation % 35.61/6.09 % (2692320)Time elapsed: 0.331 s % 35.61/6.09 % (2692320)Peak memory usage: 110 MB % 35.61/6.09 % (2692320)Instructions burned: 325 (million) % 35.61/6.09 % (2692327)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2289321371:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi) % 35.61/6.09 % (2692328)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=510991155:i=2350_2988 on theBenchmark for (2988ds/2350Mi) % 35.61/6.09 % (2692327)Instruction limit reached! % 35.61/6.09 % (2692327)------------------------------ % 35.61/6.09 % (2692327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692327)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692327)Termination reason: Instruction limit % 35.61/6.09 % (2692327)Termination phase: Property scanning % 35.61/6.09 % (2692327)Time elapsed: 0.183 s % 35.61/6.09 % (2692327)Peak memory usage: 109 MB % 35.61/6.09 % (2692327)Instructions burned: 296 (million) % 35.61/6.09 % (2692331)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1547661199:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi) % 35.61/6.09 % (2692333)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2939139421:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi) % 35.61/6.09 % (2692331)Instruction limit reached! % 35.61/6.09 % (2692331)------------------------------ % 35.61/6.09 % (2692331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692331)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692331)Termination reason: Instruction limit % 35.61/6.09 % (2692331)Termination phase: Naming % 35.61/6.09 % (2692331)Time elapsed: 0.150 s % 35.61/6.09 % (2692331)Peak memory usage: 105 MB % 35.61/6.09 % (2692331)Instructions burned: 113 (million) % 35.61/6.09 % (2692333)Instruction limit reached! % 35.61/6.09 % (2692333)------------------------------ % 35.61/6.09 % (2692333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/6.09 % (2692333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/6.09 % (2692333)CaDiCaL version: 2.1.3 % 35.61/6.09 % (2692333)Termination reason: Instruction limit % 97.98/14.81 % (2692333)Termination phase: Preprocessing 2 % 97.98/14.81 % (2692333)Time elapsed: 0.178 s % 97.98/14.81 % (2692333)Peak memory usage: 106 MB % 97.98/14.81 % (2692333)Instructions burned: 127 (million) % 97.98/14.81 % (2692336)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=386861593:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi) % 97.98/14.81 % (2692336)Instruction limit reached! % 97.98/14.81 % (2692336)------------------------------ % 97.98/14.81 % (2692336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.98/14.81 % (2692336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.98/14.81 % (2692336)CaDiCaL version: 2.1.3 % 97.98/14.81 % (2692336)Termination reason: Instruction limit % 97.98/14.81 % (2692336)Termination phase: Property scanning % 97.98/14.81 % (2692336)Time elapsed: 0.049 s % 97.98/14.81 % (2692336)Peak memory usage: 102 MB % 97.98/14.81 % (2692336)Instructions burned: 115 (million) % 97.98/14.81 % (2692339)lrs+10_1_sil=8000:sp=occurrence:random_seed=1209244987:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi) % 97.98/14.81 % (2692341)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3738121011:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi) % 97.98/14.81 % (2692342)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2509095731:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi) % 97.98/14.81 % (2692339)Instruction limit reached! % 97.98/14.81 % (2692339)------------------------------ % 97.98/14.81 % (2692339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.98/14.81 % (2692339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.98/14.81 % (2692339)CaDiCaL version: 2.1.3 % 97.98/14.81 % (2692339)Termination reason: Instruction limit % 97.98/14.81 % (2692339)Termination phase: Saturation % 97.98/14.81 % (2692339)Time elapsed: 0.586 s % 97.98/14.81 % (2692339)Peak memory usage: 121 MB % 97.98/14.81 % (2692339)Instructions burned: 908 (million) % 97.98/14.81 % (2692341)Instruction limit reached! % 97.98/14.81 % (2692341)------------------------------ % 97.98/14.81 % (2692341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.98/14.81 % (2692341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.98/14.81 % (2692341)CaDiCaL version: 2.1.3 % 97.98/14.81 % (2692341)Termination reason: Instruction limit % 97.98/14.81 % (2692341)Termination phase: Saturation % 97.98/14.81 % (2692341)Time elapsed: 0.460 s % 97.98/14.81 % (2692341)Peak memory usage: 112 MB % 97.98/14.81 % (2692341)Instructions burned: 437 (million) % 97.98/14.81 % (2692347)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1889945082:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2974 on theBenchmark for (2974ds/134Mi) % 97.98/14.81 % (2692349)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2307343334:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi) % 97.98/14.81 % (2692347)Instruction limit reached! % 97.98/14.81 % (2692347)------------------------------ % 97.98/14.81 % (2692347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.98/14.81 % (2692347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.98/14.81 % (2692347)CaDiCaL version: 2.1.3 % 97.98/14.81 % (2692347)Termination reason: Instruction limit % 97.98/14.81 % (2692347)Termination phase: Property scanning % 97.98/14.81 % (2692347)Time elapsed: 0.101 s % 97.98/14.81 % (2692347)Peak memory usage: 106 MB % 97.98/14.81 % (2692347)Instructions burned: 136 (million) % 97.98/14.81 % (2692352)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2265631064:st=3:i=13193:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/13193Mi) % 97.98/14.81 % (2692349)Instruction limit reached! % 97.98/14.81 % (2692349)------------------------------ % 97.98/14.81 % (2692349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.98/14.81 % (2692349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.98/14.81 % (2692349)CaDiCaL version: 2.1.3 % 97.98/14.81 % (2692349)Termination reason: Instruction limit % 97.98/14.81 % (2692349)Termination phase: Property scanning % 97.98/14.81 % (2692349)Time elapsed: 0.384 s % 97.98/14.81 % (2692349)Peak memory usage: 124 MB % 97.98/14.81 % (2692349)Instructions burned: 593 (million) % 97.98/14.81 % (2692354)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1420506415:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/125Mi) % 140.95/21.01 % (2692354)Instruction limit reached! % 140.95/21.01 % (2692354)------------------------------ % 140.95/21.01 % (2692354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/21.01 % (2692354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/21.01 % (2692354)CaDiCaL version: 2.1.3 % 140.95/21.01 % (2692354)Termination reason: Instruction limit % 140.95/21.01 % (2692354)Termination phase: Property scanning % 140.95/21.01 % (2692354)Time elapsed: 0.104 s % 140.95/21.01 % (2692354)Peak memory usage: 102 MB % 140.95/21.01 % (2692354)Instructions burned: 125 (million) % 140.95/21.01 % (2692328)Instruction limit reached! % 140.95/21.01 % (2692328)------------------------------ % 140.95/21.01 % (2692328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/21.01 % (2692328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/21.01 % (2692328)CaDiCaL version: 2.1.3 % 140.95/21.01 % (2692328)Termination reason: Instruction limit % 140.95/21.01 % (2692328)Termination phase: Saturation % 140.95/21.01 % (2692328)Time elapsed: 2.398 s % 140.95/21.01 % (2692328)Peak memory usage: 239 MB % 140.95/21.01 % (2692328)Instructions burned: 2351 (million) % 140.95/21.01 % (2692356)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=684549712:i=134:gtgl=5:slsql=off:gtg=exists_sym_2962 on theBenchmark for (2962ds/134Mi) % 140.95/21.01 % (2692357)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1627090544:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/141Mi) % 140.95/21.01 % (2692356)Instruction limit reached! % 140.95/21.01 % (2692356)------------------------------ % 140.95/21.01 % (2692356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/21.01 % (2692356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/21.01 % (2692356)CaDiCaL version: 2.1.3 % 140.95/21.01 % (2692356)Termination reason: Instruction limit % 140.95/21.01 % (2692356)Termination phase: Property scanning % 140.95/21.01 % (2692356)Time elapsed: 0.110 s % 140.95/21.01 % (2692356)Peak memory usage: 102 MB % 140.95/21.01 % (2692356)Instructions burned: 135 (million) % 140.95/21.01 % (2692357)Instruction limit reached! % 140.95/21.01 % (2692357)------------------------------ % 140.95/21.01 % (2692357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/21.01 % (2692357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/21.01 % (2692357)CaDiCaL version: 2.1.3 % 140.95/21.01 % (2692357)Termination reason: Instruction limit % 140.95/21.01 % (2692357)Termination phase: Saturation % 140.95/21.01 % (2692357)Time elapsed: 0.151 s % 140.95/21.01 % (2692357)Peak memory usage: 108 MB % 140.95/21.01 % (2692357)Instructions burned: 142 (million) % 140.95/21.01 % (2692360)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1816176107:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2958 on theBenchmark for (2958ds/431Mi) % 140.95/21.01 % (2692361)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=804983067:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi) % 140.95/21.01 % (2692360)Instruction limit reached! % 140.95/21.01 % (2692360)------------------------------ % 140.95/21.01 % (2692360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/21.01 % (2692360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/21.01 % (2692360)CaDiCaL version: 2.1.3 % 140.95/21.01 % (2692360)Termination reason: Instruction limit % 140.95/21.01 % (2692360)Termination phase: Saturation % 140.95/21.01 % (2692360)Time elapsed: 0.457 s % 140.95/21.01 % (2692360)Peak memory usage: 110 MB % 140.95/21.01 % (2692360)Instructions burned: 431 (million) % 140.95/21.01 % (2692366)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=239288983:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi) % 140.95/21.01 % (2692366)Instruction limit reached! % 140.95/21.01 % (2692366)------------------------------ % 140.95/21.01 % (2692366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/21.01 % (2692366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/21.01 % (2692366)CaDiCaL version: 2.1.3 % 140.95/21.01 % (2692366)Termination reason: Instruction limit % 212.30/30.93 % (2692366)Termination phase: Preprocessing 1 % 212.30/30.93 % (2692366)Time elapsed: 0.179 s % 212.30/30.93 % (2692366)Peak memory usage: 103 MB % 212.30/30.93 % (2692366)Instructions burned: 150 (million) % 212.30/30.93 % (2692368)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3475607103:i=14155:bd=all_2945 on theBenchmark for (2945ds/14155Mi) % 212.30/30.93 % (2692342)Instruction limit reached! % 212.30/30.93 % (2692342)------------------------------ % 212.30/30.93 % (2692342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.93 % (2692342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.93 % (2692342)CaDiCaL version: 2.1.3 % 212.30/30.93 % (2692342)Termination reason: Instruction limit % 212.30/30.93 % (2692342)Termination phase: Saturation % 212.30/30.93 % (2692342)Time elapsed: 5.233 s % 212.30/30.93 % (2692342)Peak memory usage: 213 MB % 212.30/30.93 % (2692342)Instructions burned: 5202 (million) % 212.30/30.93 % (2692370)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3783849948:i=667:av=off:fsr=off_2925 on theBenchmark for (2925ds/667Mi) % 212.30/30.93 % (2692370)Instruction limit reached! % 212.30/30.93 % (2692370)------------------------------ % 212.30/30.93 % (2692370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.93 % (2692370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.93 % (2692370)CaDiCaL version: 2.1.3 % 212.30/30.93 % (2692370)Termination reason: Instruction limit % 212.30/30.93 % (2692370)Termination phase: NewCNF % 212.30/30.93 % (2692370)Time elapsed: 0.730 s % 212.30/30.93 % (2692370)Peak memory usage: 135 MB % 212.30/30.93 % (2692370)Instructions burned: 667 (million) % 212.30/30.93 % (2692374)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=689938165:s2a=on:i=185:s2at=1.8:fdi=4_2915 on theBenchmark for (2915ds/185Mi) % 212.30/30.93 % (2692374)Instruction limit reached! % 212.30/30.93 % (2692374)------------------------------ % 212.30/30.93 % (2692374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.93 % (2692374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.93 % (2692374)CaDiCaL version: 2.1.3 % 212.30/30.93 % (2692374)Termination reason: Instruction limit % 212.30/30.93 % (2692374)Termination phase: Preprocessing 1 % 212.30/30.93 % (2692374)Time elapsed: 0.210 s % 212.30/30.93 % (2692374)Peak memory usage: 103 MB % 212.30/30.93 % (2692374)Instructions burned: 185 (million) % 212.30/30.93 % (2692376)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3591455717:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2910 on theBenchmark for (2910ds/193Mi) % 212.30/30.93 % (2692376)Instruction limit reached! % 212.30/30.93 % (2692376)------------------------------ % 212.30/30.93 % (2692376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.93 % (2692376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.93 % (2692376)CaDiCaL version: 2.1.3 % 212.30/30.93 % (2692376)Termination reason: Instruction limit % 212.30/30.93 % (2692376)Termination phase: Preprocessing 3 % 212.30/30.93 % (2692376)Time elapsed: 0.226 s % 212.30/30.93 % (2692376)Peak memory usage: 106 MB % 212.30/30.93 % (2692376)Instructions burned: 193 (million) % 212.30/30.93 % (2692378)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3704492375:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2905 on theBenchmark for (2905ds/4850Mi) % 212.30/30.93 % (2692361)Instruction limit reached! % 212.30/30.93 % (2692361)------------------------------ % 212.30/30.93 % (2692361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.93 % (2692361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.93 % (2692361)CaDiCaL version: 2.1.3 % 212.30/30.93 % (2692361)Termination reason: Instruction limit % 212.30/30.93 % (2692361)Termination phase: Saturation % 212.30/30.93 % (2692361)Time elapsed: 7.015 s % 212.30/30.93 % (2692361)Peak memory usage: 562 MB % 212.30/30.93 % (2692361)Instructions burned: 6061 (million) % 212.30/30.93 % (2692386)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2842193405:i=12111:sd=1:ss=included_2883 on theBenchmark for (2883ds/12111Mi) % 212.30/30.93 % (2692378)Instruction limit reached! % 212.30/30.93 % (2692378)------------------------------ % 212.30/30.93 % (2692378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.93 % (2692378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/37.08 % (2692378)CaDiCaL version: 2.1.3 % 255.78/37.08 % (2692378)Termination reason: Instruction limit % 255.78/37.08 % (2692378)Termination phase: Saturation % 255.78/37.08 % (2692378)Time elapsed: 4.375 s % 255.78/37.08 % (2692378)Peak memory usage: 174 MB % 255.78/37.08 % (2692378)Instructions burned: 4850 (million) % 255.78/37.08 % (2692391)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=322424208:i=319:kws=precedence:fsr=off_2858 on theBenchmark for (2858ds/319Mi) % 255.78/37.08 % (2692391)Instruction limit reached! % 255.78/37.08 % (2692391)------------------------------ % 255.78/37.08 % (2692391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.78/37.08 % (2692391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/37.08 % (2692391)CaDiCaL version: 2.1.3 % 255.78/37.08 % (2692391)Termination reason: Instruction limit % 255.78/37.08 % (2692391)Termination phase: Preprocessing 3 % 255.78/37.08 % (2692391)Time elapsed: 0.338 s % 255.78/37.08 % (2692391)Peak memory usage: 121 MB % 255.78/37.08 % (2692391)Instructions burned: 320 (million) % 255.78/37.08 % (2692395)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=898411158:i=2064:ep=RST_2852 on theBenchmark for (2852ds/2064Mi) % 255.78/37.08 % (2692395)Instruction limit reached! % 255.78/37.08 % (2692395)------------------------------ % 255.78/37.08 % (2692395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.78/37.08 % (2692395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/37.08 % (2692395)CaDiCaL version: 2.1.3 % 255.78/37.08 % (2692395)Termination reason: Instruction limit % 255.78/37.08 % (2692395)Termination phase: Saturation % 255.78/37.08 % (2692395)Time elapsed: 1.717 s % 255.78/37.08 % (2692395)Peak memory usage: 147 MB % 255.78/37.08 % (2692395)Instructions burned: 2064 (million) % 255.78/37.08 % (2692352)Instruction limit reached! % 255.78/37.08 % (2692352)------------------------------ % 255.78/37.08 % (2692352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.78/37.08 % (2692352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/37.08 % (2692352)CaDiCaL version: 2.1.3 % 255.78/37.08 % (2692352)Termination reason: Instruction limit % 255.78/37.08 % (2692352)Termination phase: Saturation % 255.78/37.08 % (2692352)Time elapsed: 13.767 s % 255.78/37.08 % (2692352)Peak memory usage: 276 MB % 255.78/37.08 % (2692352)Instructions burned: 13193 (million) % 255.78/37.08 % (2692400)dis-1011_128_sil=32000:random_seed=2972685084:i=3706:ep=RST:av=off_2832 on theBenchmark for (2832ds/3706Mi) % 255.78/37.08 % (2692402)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2868983050:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2830 on theBenchmark for (2830ds/757Mi) % 255.78/37.08 % (2692402)Instruction limit reached! % 255.78/37.08 % (2692402)------------------------------ % 255.78/37.08 % (2692402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.78/37.08 % (2692402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/37.08 % (2692402)CaDiCaL version: 2.1.3 % 255.78/37.08 % (2692402)Termination reason: Instruction limit % 255.78/37.08 % (2692402)Termination phase: Saturation % 255.78/37.08 % (2692402)Time elapsed: 0.820 s % 255.78/37.08 % (2692402)Peak memory usage: 117 MB % 255.78/37.08 % (2692402)Instructions burned: 757 (million) % 255.78/37.08 % (2692406)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1172791916:i=13913:ss=axioms:sgt=8_2819 on theBenchmark for (2819ds/13913Mi) % 255.78/37.08 % (2692368)Instruction limit reached! % 255.78/37.08 % (2692368)------------------------------ % 255.78/37.08 % (2692368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.78/37.08 % (2692368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/37.08 % (2692368)CaDiCaL version: 2.1.3 % 255.78/37.08 % (2692368)Termination reason: Instruction limit % 255.78/37.08 % (2692368)Termination phase: Saturation % 255.78/37.08 % (2692368)Time elapsed: 14.149 s % 255.78/37.08 % (2692368)Peak memory usage: 521 MB % 255.78/37.08 % (2692368)Instructions burned: 14156 (million) % 255.78/37.08 % (2692410)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3529542473:i=9925:aac=none_2800 on theBenchmark for (2800ds/9925Mi) % 255.78/37.08 % (2692400)Instruction limit reached! % 255.78/37.08 % (2692400)------------------------------ % 255.78/37.08 % (2692400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.15/41.11 % (2692400)CaDiCaL version: 2.1.3 % 284.15/41.11 % (2692400)Termination reason: Instruction limit % 284.15/41.11 % (2692400)Termination phase: Saturation % 284.15/41.11 % (2692400)Time elapsed: 3.407 s % 284.15/41.11 % (2692400)Peak memory usage: 164 MB % 284.15/41.11 % (2692400)Instructions burned: 3706 (million) % 284.15/41.11 % (2692412)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1908826543:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2796 on theBenchmark for (2796ds/2479Mi) % 284.15/41.11 % (2692412)Instruction limit reached! % 284.15/41.11 % (2692412)------------------------------ % 284.15/41.11 % (2692412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.15/41.11 % (2692412)CaDiCaL version: 2.1.3 % 284.15/41.11 % (2692412)Termination reason: Instruction limit % 284.15/41.11 % (2692412)Termination phase: Saturation % 284.15/41.11 % (2692412)Time elapsed: 2.338 s % 284.15/41.11 % (2692412)Peak memory usage: 129 MB % 284.15/41.11 % (2692412)Instructions burned: 2479 (million) % 284.15/41.11 % (2692420)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1771706173:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2770 on theBenchmark for (2770ds/440Mi) % 284.15/41.11 % (2692420)Instruction limit reached! % 284.15/41.11 % (2692420)------------------------------ % 284.15/41.11 % (2692420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.15/41.11 % (2692420)CaDiCaL version: 2.1.3 % 284.15/41.11 % (2692420)Termination reason: Instruction limit % 284.15/41.11 % (2692420)Termination phase: Preprocessing 1 % 284.15/41.11 % (2692420)Time elapsed: 0.228 s % 284.15/41.11 % (2692420)Peak memory usage: 103 MB % 284.15/41.11 % (2692420)Instructions burned: 440 (million) % 284.15/41.11 % (2692424)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2573760454:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2765 on theBenchmark for (2765ds/11145Mi) % 284.15/41.11 % (2692386)Instruction limit reached! % 284.15/41.11 % (2692386)------------------------------ % 284.15/41.11 % (2692386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.15/41.11 % (2692386)CaDiCaL version: 2.1.3 % 284.15/41.11 % (2692386)Termination reason: Instruction limit % 284.15/41.11 % (2692386)Termination phase: Saturation % 284.15/41.11 % (2692386)Time elapsed: 13.598 s % 284.15/41.11 % (2692386)Peak memory usage: 260 MB % 284.15/41.11 % (2692386)Instructions burned: 12111 (million) % 284.15/41.11 % (2692428)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=477212196:cts=off:i=3034:av=off:er=known:fsd=on_2744 on theBenchmark for (2744ds/3034Mi) % 284.15/41.11 % (2692428)Instruction limit reached! % 284.15/41.11 % (2692428)------------------------------ % 284.15/41.11 % (2692428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.15/41.11 % (2692428)CaDiCaL version: 2.1.3 % 284.15/41.11 % (2692428)Termination reason: Instruction limit % 284.15/41.11 % (2692428)Termination phase: Saturation % 284.15/41.11 % (2692428)Time elapsed: 3.421 s % 284.15/41.11 % (2692428)Peak memory usage: 399 MB % 284.15/41.11 % (2692428)Instructions burned: 3034 (million) % 284.15/41.11 % (2692436)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=998661723:st=2:s2a=on:i=524:s2at=2:ss=axioms_2707 on theBenchmark for (2707ds/524Mi) % 284.15/41.11 % (2692410)Instruction limit reached! % 284.15/41.11 % (2692410)------------------------------ % 284.15/41.11 % (2692410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.15/41.11 % (2692410)CaDiCaL version: 2.1.3 % 284.15/41.11 % (2692410)Termination reason: Instruction limit % 284.15/41.11 % (2692410)Termination phase: Saturation % 284.15/41.11 % (2692410)Time elapsed: 9.968 s % 284.15/41.11 % (2692410)Peak memory usage: 476 MB % 284.15/41.11 % (2692410)Instructions burned: 9925 (million) % 284.15/41.11 % (2692436)Instruction limit reached! % 284.15/41.11 % (2692436)------------------------------ % 284.15/41.11 % (2692436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.15/41.11 % (2692Terminated %------------------------------------------------------------------------------