%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW906+1 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n009.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:38:01 PM UTC 2026 % Result : Timeout 300.36s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW906+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.24 % Computer : n009.cluster.edu % 0.10/0.24 % Model : x86_64 x86_64 % 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.24 % Memory : 8046.5625MB % 0.10/0.24 % OS : Linux 6.8.0-71-generic % 0.10/0.24 % CPULimit : 300 % 0.10/0.24 % WCLimit : 300 % 0.10/0.24 % DateTime : Mon Sep 28 14:40:30 UTC 2026 % 0.10/0.25 % CPUTime : % 0.10/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.24/0.29 Running first-order theorem proving % 0.24/0.29 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 % 19.71/3.71 % (3077054)Detected formulas, will run a generic FOF schedule. % 19.71/3.71 % (3077066)dis-21_1_sil=8000:lcm=predicate:random_seed=1643354539:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 19.71/3.71 % (3077066)Instruction limit reached! % 19.71/3.71 % (3077066)------------------------------ % 19.71/3.71 % (3077066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.71/3.71 % (3077066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.71/3.71 % (3077066)CaDiCaL version: 2.1.3 % 19.71/3.71 % (3077066)Termination reason: Instruction limit % 19.71/3.71 % (3077066)Termination phase: Saturation % 19.71/3.71 % (3077066)Time elapsed: 0.072 s % 19.71/3.71 % (3077066)Peak memory usage: 89 MB % 19.71/3.71 % (3077066)Instructions burned: 129 (million) % 19.71/3.71 % (3077063)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2591354997:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 19.71/3.71 % (3077060)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=758578895:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 19.71/3.71 % (3077064)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=976412171:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 19.71/3.71 % (3077065)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3992938610:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 19.71/3.71 % (3077061)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=2693034800:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 19.71/3.71 % (3077062)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=3158063434:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 19.71/3.71 % (3077063)Refutation not found, incomplete strategy % 19.71/3.71 % (3077063)------------------------------ % 19.71/3.71 % (3077063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.71/3.71 % (3077063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.71/3.71 % (3077063)CaDiCaL version: 2.1.3 % 19.71/3.71 % (3077063)Termination reason: Refutation not found, incomplete strategy % 19.71/3.71 % (3077063)Time elapsed: 0.004 s % 19.71/3.71 % (3077063)Peak memory usage: 88 MB % 19.71/3.71 % (3077063)Instructions burned: 6 (million) % 19.71/3.71 % (3077064)Instruction limit reached! % 19.71/3.71 % (3077064)------------------------------ % 19.71/3.71 % (3077064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.71/3.71 % (3077064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.71/3.71 % (3077064)CaDiCaL version: 2.1.3 % 19.71/3.71 % (3077064)Termination reason: Instruction limit % 19.71/3.71 % (3077064)Termination phase: Saturation % 19.71/3.71 % (3077064)Time elapsed: 0.101 s % 19.71/3.71 % (3077064)Peak memory usage: 88 MB % 19.71/3.71 % (3077064)Instructions burned: 119 (million) % 19.71/3.71 % (3077065)Instruction limit reached! % 19.71/3.71 % (3077065)------------------------------ % 19.71/3.71 % (3077065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.71/3.71 % (3077065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.71/3.71 % (3077065)CaDiCaL version: 2.1.3 % 19.71/3.71 % (3077065)Termination reason: Instruction limit % 19.71/3.71 % (3077065)Termination phase: Saturation % 19.71/3.71 % (3077065)Time elapsed: 0.127 s % 19.71/3.71 % (3077065)Peak memory usage: 89 MB % 19.71/3.71 % (3077065)Instructions burned: 139 (million) % 19.71/3.71 % (3077068)lrs+10_1_sil=8000:sp=occurrence:random_seed=2550377525:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 19.71/3.71 % (3077063)------------------------------ % 19.71/3.71 % (3077063)------------------------------ % 19.71/3.71 % (3077075)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3523442501:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 19.71/3.71 % (3077076)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1636385088:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 19.71/3.71 % (3077078)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=883737864:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 33.76/5.71 % (3077068)Instruction limit reached! % 33.76/5.71 % (3077068)------------------------------ % 33.76/5.71 % (3077068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077068)CaDiCaL version: 2.1.3 % 33.76/5.71 % (3077068)Termination reason: Instruction limit % 33.76/5.71 % (3077068)Termination phase: Saturation % 33.76/5.71 % (3077068)Time elapsed: 0.249 s % 33.76/5.71 % (3077068)Peak memory usage: 92 MB % 33.76/5.71 % (3077068)Instructions burned: 285 (million) % 33.76/5.71 % (3077075)Instruction limit reached! % 33.76/5.71 % (3077075)------------------------------ % 33.76/5.71 % (3077075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077075)CaDiCaL version: 2.1.3 % 33.76/5.71 % (3077075)Termination reason: Instruction limit % 33.76/5.71 % (3077075)Termination phase: Saturation % 33.76/5.71 % (3077075)Time elapsed: 0.147 s % 33.76/5.71 % (3077075)Peak memory usage: 90 MB % 33.76/5.71 % (3077075)Instructions burned: 158 (million) % 33.76/5.71 % (3077078)Instruction limit reached! % 33.76/5.71 % (3077078)------------------------------ % 33.76/5.71 % (3077078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077078)CaDiCaL version: 2.1.3 % 33.76/5.71 % (3077078)Termination reason: Instruction limit % 33.76/5.71 % (3077078)Termination phase: Saturation % 33.76/5.71 % (3077078)Time elapsed: 0.124 s % 33.76/5.71 % (3077078)Peak memory usage: 91 MB % 33.76/5.71 % (3077078)Instructions burned: 250 (million) % 33.76/5.71 % (3077076)Instruction limit reached! % 33.76/5.71 % (3077076)------------------------------ % 33.76/5.71 % (3077076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077076)CaDiCaL version: 2.1.3 % 33.76/5.71 % (3077076)Termination reason: Instruction limit % 33.76/5.71 % (3077076)Termination phase: Saturation % 33.76/5.71 % (3077076)Time elapsed: 0.291 s % 33.76/5.71 % (3077076)Peak memory usage: 92 MB % 33.76/5.71 % (3077076)Instructions burned: 327 (million) % 33.76/5.71 % (3077082)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2074571178:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi) % 33.76/5.71 % (3077082)Refutation not found, incomplete strategy % 33.76/5.71 % (3077082)------------------------------ % 33.76/5.71 % (3077082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077082)CaDiCaL version: 2.1.3 % 33.76/5.71 % (3077082)Termination reason: Refutation not found, incomplete strategy % 33.76/5.71 % (3077082)Time elapsed: 0.008 s % 33.76/5.71 % (3077082)Peak memory usage: 88 MB % 33.76/5.71 % (3077082)Instructions burned: 6 (million) % 33.76/5.71 % (3077084)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2730453231:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi) % 33.76/5.71 % (3077083)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3199134591:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 33.76/5.71 % (3077084)Instruction limit reached! % 33.76/5.71 % (3077084)------------------------------ % 33.76/5.71 % (3077084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077084)CaDiCaL version: 2.1.3 % 33.76/5.71 % (3077084)Termination reason: Instruction limit % 33.76/5.71 % (3077084)Termination phase: Saturation % 33.76/5.71 % (3077084)Time elapsed: 0.054 s % 33.76/5.71 % (3077084)Peak memory usage: 89 MB % 33.76/5.71 % (3077084)Instructions burned: 113 (million) % 33.76/5.71 % (3077085)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=426946309:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi) % 33.76/5.71 % (3077085)Instruction limit reached! % 33.76/5.71 % (3077085)------------------------------ % 33.76/5.71 % (3077085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.71 % (3077085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.71 % (3077085)CaDiCaL version: 2.1.3 % 62.49/9.78 % (3077085)Termination reason: Instruction limit % 62.49/9.78 % (3077085)Termination phase: Saturation % 62.49/9.78 % (3077085)Time elapsed: 0.101 s % 62.49/9.78 % (3077085)Peak memory usage: 88 MB % 62.49/9.78 % (3077085)Instructions burned: 127 (million) % 62.49/9.78 % (3077090)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3299796445:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi) % 62.49/9.78 % (3077082)------------------------------ % 62.49/9.78 % (3077082)------------------------------ % 62.49/9.78 % (3077090)Instruction limit reached! % 62.49/9.78 % (3077090)------------------------------ % 62.49/9.78 % (3077090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.49/9.78 % (3077090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.49/9.78 % (3077090)CaDiCaL version: 2.1.3 % 62.49/9.78 % (3077090)Termination reason: Instruction limit % 62.49/9.78 % (3077090)Termination phase: Saturation % 62.49/9.78 % (3077090)Time elapsed: 0.098 s % 62.49/9.78 % (3077090)Peak memory usage: 89 MB % 62.49/9.78 % (3077090)Instructions burned: 114 (million) % 62.49/9.78 % (3077093)lrs+10_1_sil=8000:sp=occurrence:random_seed=3123918641:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi) % 62.49/9.78 % (3077095)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3330787438:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi) % 62.49/9.78 % (3077095)Refutation not found, incomplete strategy % 62.49/9.78 % (3077095)------------------------------ % 62.49/9.78 % (3077095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.49/9.78 % (3077095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.49/9.78 % (3077095)CaDiCaL version: 2.1.3 % 62.49/9.78 % (3077095)Termination reason: Refutation not found, incomplete strategy % 62.49/9.78 % (3077095)Time elapsed: 0.011 s % 62.49/9.78 % (3077095)Peak memory usage: 88 MB % 62.49/9.78 % (3077095)Instructions burned: 10 (million) % 62.49/9.78 % (3077096)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=237498314:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi) % 62.49/9.78 % (3077095)------------------------------ % 62.49/9.78 % (3077095)------------------------------ % 62.49/9.78 % (3077093)Instruction limit reached! % 62.49/9.78 % (3077093)------------------------------ % 62.49/9.78 % (3077093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.49/9.78 % (3077093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.49/9.78 % (3077093)CaDiCaL version: 2.1.3 % 62.49/9.78 % (3077093)Termination reason: Instruction limit % 62.49/9.78 % (3077093)Termination phase: Saturation % 62.49/9.78 % (3077093)Time elapsed: 0.757 s % 62.49/9.78 % (3077093)Peak memory usage: 98 MB % 62.49/9.78 % (3077093)Instructions burned: 908 (million) % 62.49/9.78 % (3077102)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=394930780:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi) % 62.49/9.78 % (3077102)Instruction limit reached! % 62.49/9.78 % (3077102)------------------------------ % 62.49/9.78 % (3077102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.49/9.78 % (3077102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.49/9.78 % (3077102)CaDiCaL version: 2.1.3 % 62.49/9.78 % (3077102)Termination reason: Instruction limit % 62.49/9.78 % (3077102)Termination phase: Saturation % 62.49/9.78 % (3077102)Time elapsed: 0.112 s % 62.49/9.78 % (3077102)Peak memory usage: 89 MB % 62.49/9.78 % (3077102)Instructions burned: 135 (million) % 62.49/9.78 % (3077103)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1361764529:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi) % 62.49/9.78 % (3077103)Refutation not found, incomplete strategy % 62.49/9.78 % (3077103)------------------------------ % 62.49/9.78 % (3077103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.49/9.78 % (3077103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.49/9.78 % (3077103)CaDiCaL version: 2.1.3 % 62.49/9.78 % (3077103)Termination reason: Refutation not found, incomplete strategy % 62.49/9.78 % (3077103)Time elapsed: 0.006 s % 62.49/9.78 % (3077103)Peak memory usage: 88 MB % 62.49/9.78 % (3077103)Instructions burned: 4 (million) % 62.49/9.78 % (3077106)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1887470561:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi) % 100.97/15.10 % (3077103)------------------------------ % 100.97/15.10 % (3077103)------------------------------ % 100.97/15.10 % (3077110)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=851468446:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi) % 100.97/15.10 % (3077083)Instruction limit reached! % 100.97/15.10 % (3077083)------------------------------ % 100.97/15.10 % (3077083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.97/15.10 % (3077083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.97/15.10 % (3077083)CaDiCaL version: 2.1.3 % 100.97/15.10 % (3077083)Termination reason: Instruction limit % 100.97/15.10 % (3077083)Termination phase: Saturation % 100.97/15.10 % (3077083)Time elapsed: 2.374 s % 100.97/15.10 % (3077083)Peak memory usage: 143 MB % 100.97/15.10 % (3077083)Instructions burned: 2350 (million) % 100.97/15.10 % (3077110)Instruction limit reached! % 100.97/15.10 % (3077110)------------------------------ % 100.97/15.10 % (3077110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.97/15.10 % (3077110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.97/15.10 % (3077110)CaDiCaL version: 2.1.3 % 100.97/15.10 % (3077110)Termination reason: Instruction limit % 100.97/15.10 % (3077110)Termination phase: Saturation % 100.97/15.10 % (3077110)Time elapsed: 0.128 s % 100.97/15.10 % (3077110)Peak memory usage: 90 MB % 100.97/15.10 % (3077110)Instructions burned: 125 (million) % 100.97/15.10 % (3077112)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3938906165:i=134:gtgl=5:slsql=off:gtg=exists_sym_2965 on theBenchmark for (2965ds/134Mi) % 100.97/15.10 % (3077113)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3445109788:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi) % 100.97/15.10 % (3077113)Refutation not found, incomplete strategy % 100.97/15.10 % (3077113)------------------------------ % 100.97/15.10 % (3077113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.97/15.10 % (3077113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.97/15.10 % (3077113)CaDiCaL version: 2.1.3 % 100.97/15.10 % (3077113)Termination reason: Refutation not found, incomplete strategy % 100.97/15.10 % (3077113)Time elapsed: 0.013 s % 100.97/15.10 % (3077113)Peak memory usage: 88 MB % 100.97/15.10 % (3077113)Instructions burned: 12 (million) % 100.97/15.10 % (3077112)Instruction limit reached! % 100.97/15.10 % (3077112)------------------------------ % 100.97/15.10 % (3077112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.97/15.10 % (3077112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.97/15.10 % (3077112)CaDiCaL version: 2.1.3 % 100.97/15.10 % (3077112)Termination reason: Instruction limit % 100.97/15.10 % (3077112)Termination phase: Saturation % 100.97/15.10 % (3077112)Time elapsed: 0.125 s % 100.97/15.10 % (3077112)Peak memory usage: 89 MB % 100.97/15.10 % (3077112)Instructions burned: 134 (million) % 100.97/15.10 % (3077116)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3306926283:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi) % 100.97/15.10 % (3077116)Refutation not found, incomplete strategy % 100.97/15.10 % (3077116)------------------------------ % 100.97/15.10 % (3077116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.97/15.10 % (3077116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.97/15.10 % (3077116)CaDiCaL version: 2.1.3 % 100.97/15.10 % (3077116)Termination reason: Refutation not found, incomplete strategy % 100.97/15.10 % (3077116)Time elapsed: 0.006 s % 100.97/15.10 % (3077116)Peak memory usage: 88 MB % 100.97/15.10 % (3077116)Instructions burned: 4 (million) % 100.97/15.10 % (3077113)------------------------------ % 100.97/15.10 % (3077113)------------------------------ % 100.97/15.10 % (3077118)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=507257970:i=6060:aac=none:ins=25_2958 on theBenchmark for (2958ds/6060Mi) % 100.97/15.10 % (3077116)------------------------------ % 100.97/15.10 % (3077116)------------------------------ % 100.97/15.10 % (3077120)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=3000744833:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi) % 139.36/20.56 % (3077120)Instruction limit reached! % 139.36/20.56 % (3077120)------------------------------ % 139.36/20.56 % (3077120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.36/20.56 % (3077120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.36/20.56 % (3077120)CaDiCaL version: 2.1.3 % 139.36/20.56 % (3077120)Termination reason: Instruction limit % 139.36/20.56 % (3077120)Termination phase: Saturation % 139.36/20.56 % (3077120)Time elapsed: 0.135 s % 139.36/20.56 % (3077120)Peak memory usage: 89 MB % 139.36/20.56 % (3077120)Instructions burned: 150 (million) % 139.36/20.56 % (3077124)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=847372455:i=14155:bd=all_2950 on theBenchmark for (2950ds/14155Mi) % 139.36/20.56 % (3077096)Instruction limit reached! % 139.36/20.56 % (3077096)------------------------------ % 139.36/20.56 % (3077096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.36/20.56 % (3077096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.36/20.56 % (3077096)CaDiCaL version: 2.1.3 % 139.36/20.56 % (3077096)Termination reason: Instruction limit % 139.36/20.56 % (3077096)Termination phase: Saturation % 139.36/20.56 % (3077096)Time elapsed: 4.654 s % 139.36/20.56 % (3077096)Peak memory usage: 159 MB % 139.36/20.56 % (3077096)Instructions burned: 5203 (million) % 139.36/20.56 % (3077128)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1328826641:i=667:av=off:fsr=off_2935 on theBenchmark for (2935ds/667Mi) % 139.36/20.56 % (3077128)Instruction limit reached! % 139.36/20.56 % (3077128)------------------------------ % 139.36/20.56 % (3077128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.36/20.56 % (3077128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.36/20.56 % (3077128)CaDiCaL version: 2.1.3 % 139.36/20.56 % (3077128)Termination reason: Instruction limit % 139.36/20.56 % (3077128)Termination phase: Saturation % 139.36/20.56 % (3077128)Time elapsed: 0.510 s % 139.36/20.56 % (3077128)Peak memory usage: 113 MB % 139.36/20.56 % (3077128)Instructions burned: 668 (million) % 139.36/20.56 % (3077130)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=2023577684:s2a=on:i=185:s2at=1.8:fdi=4_2927 on theBenchmark for (2927ds/185Mi) % 139.36/20.56 % (3077130)Instruction limit reached! % 139.36/20.56 % (3077130)------------------------------ % 139.36/20.56 % (3077130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.36/20.56 % (3077130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.36/20.56 % (3077130)CaDiCaL version: 2.1.3 % 139.36/20.56 % (3077130)Termination reason: Instruction limit % 139.36/20.56 % (3077130)Termination phase: Saturation % 139.36/20.56 % (3077130)Time elapsed: 0.157 s % 139.36/20.56 % (3077130)Peak memory usage: 90 MB % 139.36/20.56 % (3077130)Instructions burned: 186 (million) % 139.36/20.56 % (3077133)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=455339432:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2922 on theBenchmark for (2922ds/193Mi) % 139.36/20.56 % (3077133)Instruction limit reached! % 139.36/20.56 % (3077133)------------------------------ % 139.36/20.56 % (3077133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.36/20.56 % (3077133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.36/20.56 % (3077133)CaDiCaL version: 2.1.3 % 139.36/20.56 % (3077133)Termination reason: Instruction limit % 139.36/20.56 % (3077133)Termination phase: Saturation % 139.36/20.56 % (3077133)Time elapsed: 0.169 s % 139.36/20.56 % (3077133)Peak memory usage: 89 MB % 139.36/20.56 % (3077133)Instructions burned: 193 (million) % 139.36/20.56 % (3077136)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3788366096:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2918 on theBenchmark for (2918ds/4850Mi) % 139.36/20.56 % (3077136)Refutation not found, incomplete strategy % 139.36/20.56 % (3077136)------------------------------ % 139.36/20.56 % (3077136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.36/20.56 % (3077136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.36/20.56 % (3077136)CaDiCaL version: 2.1.3 % 139.36/20.56 % (3077136)Termination reason: Refutation not found, incomplete strategy % 139.36/20.56 % (3077136)Time elapsed: 0.006 s % 139.36/20.56 % (3077136)Peak memory usage: 88 MB % 139.36/20.56 % (3077136)Instructions burned: 5 (million) % 139.36/20.56 % (3077136)------------------------------ % 165.93/24.30 % (3077136)------------------------------ % 165.93/24.30 % (3077138)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3568628931:i=12111:sd=1:ss=included_2911 on theBenchmark for (2911ds/12111Mi) % 165.93/24.30 % (3077118)Instruction limit reached! % 165.93/24.30 % (3077118)------------------------------ % 165.93/24.30 % (3077118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.93/24.30 % (3077118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.93/24.30 % (3077118)CaDiCaL version: 2.1.3 % 165.93/24.30 % (3077118)Termination reason: Instruction limit % 165.93/24.30 % (3077118)Termination phase: Saturation % 165.93/24.30 % (3077118)Time elapsed: 5.983 s % 165.93/24.30 % (3077118)Peak memory usage: 180 MB % 165.93/24.30 % (3077118)Instructions burned: 6061 (million) % 165.93/24.30 % (3077140)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2500990400:i=319:kws=precedence:fsr=off_2895 on theBenchmark for (2895ds/319Mi) % 165.93/24.30 % (3077140)Instruction limit reached! % 165.93/24.30 % (3077140)------------------------------ % 165.93/24.30 % (3077140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.93/24.30 % (3077140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.93/24.30 % (3077140)CaDiCaL version: 2.1.3 % 165.93/24.30 % (3077140)Termination reason: Instruction limit % 165.93/24.30 % (3077140)Termination phase: Saturation % 165.93/24.30 % (3077140)Time elapsed: 0.249 s % 165.93/24.30 % (3077140)Peak memory usage: 89 MB % 165.93/24.30 % (3077140)Instructions burned: 320 (million) % 165.93/24.30 % (3077142)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1847595890:i=2064:ep=RST_2889 on theBenchmark for (2889ds/2064Mi) % 165.93/24.30 % (3077142)Refutation not found, incomplete strategy % 165.93/24.30 % (3077142)------------------------------ % 165.93/24.30 % (3077142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.93/24.30 % (3077142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.93/24.30 % (3077142)CaDiCaL version: 2.1.3 % 165.93/24.30 % (3077142)Termination reason: Refutation not found, incomplete strategy % 165.93/24.30 % (3077142)Time elapsed: 0.005 s % 165.93/24.30 % (3077142)Peak memory usage: 88 MB % 165.93/24.30 % (3077142)Instructions burned: 4 (million) % 165.93/24.30 % (3077142)------------------------------ % 165.93/24.30 % (3077142)------------------------------ % 165.93/24.30 % (3077144)dis-1011_128_sil=32000:random_seed=288223176:i=3706:ep=RST:av=off_2882 on theBenchmark for (2882ds/3706Mi) % 165.93/24.30 % (3077144)Instruction limit reached! % 165.93/24.30 % (3077144)------------------------------ % 165.93/24.30 % (3077144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.93/24.30 % (3077144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.93/24.30 % (3077144)CaDiCaL version: 2.1.3 % 165.93/24.30 % (3077144)Termination reason: Instruction limit % 165.93/24.30 % (3077144)Termination phase: Saturation % 165.93/24.30 % (3077144)Time elapsed: 1.685 s % 165.93/24.30 % (3077144)Peak memory usage: 91 MB % 165.93/24.30 % (3077144)Instructions burned: 3707 (million) % 165.93/24.30 % (3077106)Instruction limit reached! % 165.93/24.30 % (3077106)------------------------------ % 165.93/24.30 % (3077106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.93/24.30 % (3077106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.93/24.30 % (3077106)CaDiCaL version: 2.1.3 % 165.93/24.30 % (3077106)Termination reason: Instruction limit % 165.93/24.30 % (3077106)Termination phase: Saturation % 165.93/24.30 % (3077106)Time elapsed: 10.875 s % 165.93/24.30 % (3077106)Peak memory usage: 209 MB % 165.93/24.30 % (3077106)Instructions burned: 13193 (million) % 165.93/24.30 % (3077300)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2613434119:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2863 on theBenchmark for (2863ds/757Mi) % 165.93/24.30 % (3077301)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2644676286:i=13913:ss=axioms:sgt=8_2863 on theBenchmark for (2863ds/13913Mi) % 165.93/24.30 % (3077300)Instruction limit reached! % 165.93/24.30 % (3077300)------------------------------ % 165.93/24.30 % (3077300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.93/24.30 % (3077300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.93/24.30 % (3077300)CaDiCaL version: 2.1.3 % 165.93/24.30 % (3077300)Termination reason: Instruction limit % 165.93/24.30 % (3077300)Termination phase: Saturation % 191.52/27.89 % (3077300)Time elapsed: 0.398 s % 191.52/27.89 % (3077300)Peak memory usage: 119 MB % 191.52/27.89 % (3077300)Instructions burned: 757 (million) % 191.52/27.89 % (3077304)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2268598657:i=9925:aac=none_2858 on theBenchmark for (2858ds/9925Mi) % 191.52/27.89 % (3077124)Instruction limit reached! % 191.52/27.89 % (3077124)------------------------------ % 191.52/27.89 % (3077124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.52/27.89 % (3077124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.52/27.89 % (3077124)CaDiCaL version: 2.1.3 % 191.52/27.89 % (3077124)Termination reason: Instruction limit % 191.52/27.89 % (3077124)Termination phase: Saturation % 191.52/27.89 % (3077124)Time elapsed: 10.965 s % 191.52/27.89 % (3077124)Peak memory usage: 193 MB % 191.52/27.89 % (3077124)Instructions burned: 14155 (million) % 191.52/27.89 % (3077306)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2898876450:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2837 on theBenchmark for (2837ds/2479Mi) % 191.52/27.89 % (3077306)Refutation not found, incomplete strategy % 191.52/27.89 % (3077306)------------------------------ % 191.52/27.89 % (3077306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.52/27.89 % (3077306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.52/27.89 % (3077306)CaDiCaL version: 2.1.3 % 191.52/27.89 % (3077306)Termination reason: Refutation not found, incomplete strategy % 191.52/27.89 % (3077306)Time elapsed: 0.007 s % 191.52/27.89 % (3077306)Peak memory usage: 88 MB % 191.52/27.89 % (3077306)Instructions burned: 11 (million) % 191.52/27.89 % (3077306)------------------------------ % 191.52/27.89 % (3077306)------------------------------ % 191.52/27.89 % (3077308)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4123112182:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2833 on theBenchmark for (2833ds/440Mi) % 191.52/27.89 % (3077308)Instruction limit reached! % 191.52/27.89 % (3077308)------------------------------ % 191.52/27.89 % (3077308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.52/27.89 % (3077308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.52/27.89 % (3077308)CaDiCaL version: 2.1.3 % 191.52/27.89 % (3077308)Termination reason: Instruction limit % 191.52/27.89 % (3077308)Termination phase: Saturation % 191.52/27.89 % (3077308)Time elapsed: 0.258 s % 191.52/27.89 % (3077308)Peak memory usage: 91 MB % 191.52/27.89 % (3077308)Instructions burned: 441 (million) % 191.52/27.89 % (3077310)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3132664690:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2829 on theBenchmark for (2829ds/11145Mi) % 191.52/27.89 % (3077138)Instruction limit reached! % 191.52/27.89 % (3077138)------------------------------ % 191.52/27.89 % (3077138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.52/27.89 % (3077138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.52/27.89 % (3077138)CaDiCaL version: 2.1.3 % 191.52/27.89 % (3077138)Termination reason: Instruction limit % 191.52/27.89 % (3077138)Termination phase: Saturation % 191.52/27.89 % (3077138)Time elapsed: 8.175 s % 191.52/27.89 % (3077138)Peak memory usage: 228 MB % 191.52/27.89 % (3077138)Instructions burned: 12113 (million) % 191.52/27.89 % (3077312)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=3717041516:cts=off:i=3034:av=off:er=known:fsd=on_2827 on theBenchmark for (2827ds/3034Mi) % 191.52/27.89 % (3077312)Instruction limit reached! % 191.52/27.89 % (3077312)------------------------------ % 191.52/27.89 % (3077312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.52/27.89 % (3077312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.52/27.89 % (3077312)CaDiCaL version: 2.1.3 % 191.52/27.89 % (3077312)Termination reason: Instruction limit % 191.52/27.89 % (3077312)Termination phase: Saturation % 191.52/27.89 % (3077312)Time elapsed: 1.753 s % 191.52/27.89 % (3077312)Peak memory usage: 137 MB % 191.52/27.89 % (3077312)Instructions burned: 3034 (million) % 191.52/27.89 % (3077314)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1540837349:st=2:s2a=on:i=524:s2at=2:ss=axioms_2807 on theBenchmark for (2807ds/524Mi) % 191.52/27.89 % (3077314)Instruction limit reached! % 191.52/27.89 % (3077314)------------------------------ % 191.52/27.89 % (3077314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.42/32.80 % (3077314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.42/32.80 % (3077314)CaDiCaL version: 2.1.3 % 226.42/32.80 % (3077314)Termination reason: Instruction limit % 226.42/32.80 % (3077314)Termination phase: Saturation % 226.42/32.80 % (3077314)Time elapsed: 0.284 s % 226.42/32.80 % (3077314)Peak memory usage: 92 MB % 226.42/32.80 % (3077314)Instructions burned: 524 (million) % 226.42/32.80 % (3077304)Instruction limit reached! % 226.42/32.80 % (3077304)------------------------------ % 226.42/32.80 % (3077304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.42/32.80 % (3077304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.42/32.80 % (3077304)CaDiCaL version: 2.1.3 % 226.42/32.80 % (3077304)Termination reason: Instruction limit % 226.42/32.80 % (3077304)Termination phase: Saturation % 226.42/32.80 % (3077304)Time elapsed: 5.435 s % 226.42/32.80 % (3077304)Peak memory usage: 182 MB % 226.42/32.80 % (3077304)Instructions burned: 9927 (million) % 226.42/32.80 % (3077316)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=633742039:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2803 on theBenchmark for (2803ds/1016Mi) % 226.42/32.80 % (3077317)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4188312898:i=14123:bd=preordered:ins=4_2801 on theBenchmark for (2801ds/14123Mi) % 226.42/32.80 % (3077316)Instruction limit reached! % 226.42/32.80 % (3077316)------------------------------ % 226.42/32.80 % (3077316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.42/32.80 % (3077316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.42/32.80 % (3077316)CaDiCaL version: 2.1.3 % 226.42/32.80 % (3077316)Termination reason: Instruction limit % 226.42/32.80 % (3077316)Termination phase: Saturation % 226.42/32.80 % (3077316)Time elapsed: 0.496 s % 226.42/32.80 % (3077316)Peak memory usage: 93 MB % 226.42/32.80 % (3077316)Instructions burned: 1017 (million) % 226.42/32.80 % (3077320)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1383216123:i=5781:kws=precedence:bd=all:rawr=on_2796 on theBenchmark for (2796ds/5781Mi) % 226.42/32.80 % (3077301)Instruction limit reached! % 226.42/32.80 % (3077301)------------------------------ % 226.42/32.80 % (3077301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.42/32.80 % (3077301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.42/32.80 % (3077301)CaDiCaL version: 2.1.3 % 226.42/32.80 % (3077301)Termination reason: Instruction limit % 226.42/32.80 % (3077301)Termination phase: Saturation % 226.42/32.80 % (3077301)Time elapsed: 7.662 s % 226.42/32.80 % (3077301)Peak memory usage: 244 MB % 226.42/32.80 % (3077301)Instructions burned: 13914 (million) % 226.42/32.80 % (3077322)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2861264566:i=2448:gtgl=5:bd=preordered:gtg=all_2784 on theBenchmark for (2784ds/2448Mi) % 226.42/32.80 % (3077320)Instruction limit reached! % 226.42/32.80 % (3077320)------------------------------ % 226.42/32.80 % (3077320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.42/32.80 % (3077320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.42/32.80 % (3077320)CaDiCaL version: 2.1.3 % 226.42/32.80 % (3077320)Termination reason: Instruction limit % 226.42/32.80 % (3077320)Termination phase: Saturation % 226.42/32.80 % (3077320)Time elapsed: 2.415 s % 226.42/32.80 % (3077320)Peak memory usage: 96 MB % 226.42/32.80 % (3077320)Instructions burned: 5782 (million) % 226.42/32.80 % (3077324)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1374720310:i=3223:kws=precedence:fgj=on:av=off_2771 on theBenchmark for (2771ds/3223Mi) % 226.42/32.80 % (3077322)Instruction limit reached! % 226.42/32.80 % (3077322)------------------------------ % 226.42/32.80 % (3077322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.42/32.80 % (3077322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.42/32.80 % (3077322)CaDiCaL version: 2.1.3 % 226.42/32.80 % (3077322)Termination reason: Instruction limit % 226.42/32.80 % (3077322)Termination phase: Saturation % 226.42/32.80 % (3077322)Time elapsed: 1.494 s % 226.42/32.80 % (3077322)Peak memory usage: 142 MB % 226.42/32.80 % (3077322)Instructions burned: 2450 (million) % 226.42/32.80 % (3077326)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4122731918:st=5.6:i=2033:sd=3:ss=axioms_2767 on theBenchmark for (2767ds/2033Mi) % 271.90/39.19 % (3077310)Instruction limit reached! % 271.90/39.19 % (3077310)------------------------------ % 271.90/39.19 % (3077310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.90/39.19 % (3077310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.90/39.19 % (3077310)CaDiCaL version: 2.1.3 % 271.90/39.19 % (3077310)Termination reason: Instruction limit % 271.90/39.19 % (3077310)Termination phase: Saturation % 271.90/39.19 % (3077310)Time elapsed: 6.446 s % 271.90/39.19 % (3077310)Peak memory usage: 213 MB % 271.90/39.19 % (3077310)Instructions burned: 11147 (million) % 271.90/39.19 % (3077328)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3861966505:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2762 on theBenchmark for (2762ds/2055Mi) % 271.90/39.19 % (3077326)Instruction limit reached! % 271.90/39.19 % (3077326)------------------------------ % 271.90/39.19 % (3077326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.90/39.19 % (3077326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.90/39.19 % (3077326)CaDiCaL version: 2.1.3 % 271.90/39.19 % (3077326)Termination reason: Instruction limit % 271.90/39.19 % (3077326)Termination phase: Saturation % 271.90/39.19 % (3077326)Time elapsed: 1.230 s % 271.90/39.19 % (3077326)Peak memory usage: 136 MB % 271.90/39.19 % (3077326)Instructions burned: 2034 (million) % 271.90/39.19 % (3077330)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1592617692:i=21611:sd=3:ss=axioms_2753 on theBenchmark for (2753ds/21611Mi) % 271.90/39.19 % (3077324)Instruction limit reached! % 271.90/39.19 % (3077324)------------------------------ % 271.90/39.19 % (3077324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.90/39.19 % (3077324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.90/39.19 % (3077324)CaDiCaL version: 2.1.3 % 271.90/39.19 % (3077324)Termination reason: Instruction limit % 271.90/39.19 % (3077324)Termination phase: Saturation % 271.90/39.19 % (3077324)Time elapsed: 1.961 s % 271.90/39.19 % (3077324)Peak memory usage: 149 MB % 271.90/39.19 % (3077324)Instructions burned: 3224 (million) % 271.90/39.19 % (3077328)Instruction limit reached! % 271.90/39.19 % (3077328)------------------------------ % 271.90/39.19 % (3077328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.90/39.19 % (3077328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.90/39.19 % (3077328)CaDiCaL version: 2.1.3 % 271.90/39.19 % (3077328)Termination reason: Instruction limit % 271.90/39.19 % (3077328)Termination phase: Saturation % 271.90/39.19 % (3077328)Time elapsed: 1.248 s % 271.90/39.19 % (3077328)Peak memory usage: 136 MB % 271.90/39.19 % (3077328)Instructions burned: 2055 (million) % 271.90/39.19 % (3077332)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=72421140:i=4835:sd=13:ss=axioms:sgt=23_2749 on theBenchmark for (2749ds/4835Mi) % 271.90/39.19 % (3077333)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=294271014:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2748 on theBenchmark for (2748ds/797Mi) % 271.90/39.19 % (3077333)Instruction limit reached! % 271.90/39.19 % (3077333)------------------------------ % 271.90/39.19 % (3077333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.90/39.19 % (3077333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.90/39.19 % (3077333)CaDiCaL version: 2.1.3 % 271.90/39.19 % (3077333)Termination reason: Instruction limit % 271.90/39.19 % (3077333)Termination phase: Saturation % 271.90/39.19 % (3077333)Time elapsed: 0.366 s % 271.90/39.19 % (3077333)Peak memory usage: 89 MB % 271.90/39.19 % (3077333)Instructions burned: 797 (million) % 271.90/39.19 % (3077336)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3119869011:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2743 on theBenchmark for (2743ds/2326Mi) % 271.90/39.19 % (3077336)Instruction limit reached! % 271.90/39.19 % (3077336)------------------------------ % 271.90/39.19 % (3077336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.90/39.19 % (3077336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.90/39.19 % (3077336)CaDiCaL version: 2.1.3 % 271.90/39.19 % (3077336)Termination reason: Instruction limit % 271.90/39.19 % (3077336)TTerminated %------------------------------------------------------------------------------