%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW888+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 : n026.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:37:59 PM UTC 2026 % Result : Timeout 295.11s 42.30s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW888+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.18 % Computer : n026.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 14:40:56 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.22 Running first-order theorem proving % 0.07/0.22 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 % 10.30/2.13 % (3896156)Detected formulas, will run a generic FOF schedule. % 10.30/2.13 % (3896165)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=5402659:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.30/2.13 % (3896165)Refutation not found, incomplete strategy % 10.30/2.13 % (3896165)------------------------------ % 10.30/2.13 % (3896165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.30/2.13 % (3896165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.30/2.13 % (3896165)CaDiCaL version: 2.1.3 % 10.30/2.13 % (3896165)Termination reason: Refutation not found, incomplete strategy % 10.30/2.13 % (3896165)Time elapsed: 0.001 s % 10.30/2.13 % (3896165)Peak memory usage: 88 MB % 10.30/2.13 % (3896165)Instructions burned: 2 (million) % 10.30/2.13 % (3896162)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=4264372446:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.30/2.13 % (3896163)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=157555776:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.30/2.13 % (3896161)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=104979610:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.30/2.13 % (3896164)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3636803207:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.30/2.13 % (3896166)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3559335581:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.30/2.13 % (3896167)dis-21_1_sil=8000:lcm=predicate:random_seed=2645964039: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) % 10.30/2.13 % (3896164)Refutation not found, incomplete strategy % 10.30/2.13 % (3896164)------------------------------ % 10.30/2.13 % (3896164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.30/2.13 % (3896164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.30/2.13 % (3896164)CaDiCaL version: 2.1.3 % 10.30/2.13 % (3896164)Termination reason: Refutation not found, incomplete strategy % 10.30/2.13 % (3896164)Time elapsed: 0.002 s % 10.30/2.13 % (3896164)Peak memory usage: 88 MB % 10.30/2.13 % (3896164)Instructions burned: 2 (million) % 10.30/2.13 % (3896167)Instruction limit reached! % 10.30/2.13 % (3896167)------------------------------ % 10.30/2.13 % (3896167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.30/2.13 % (3896167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.30/2.13 % (3896167)CaDiCaL version: 2.1.3 % 10.30/2.13 % (3896167)Termination reason: Instruction limit % 10.30/2.13 % (3896167)Termination phase: Property scanning % 10.30/2.13 % (3896167)Time elapsed: 0.047 s % 10.30/2.13 % (3896167)Peak memory usage: 87 MB % 10.30/2.13 % (3896167)Instructions burned: 131 (million) % 10.30/2.13 % (3896166)Instruction limit reached! % 10.30/2.13 % (3896166)------------------------------ % 10.30/2.13 % (3896166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.30/2.13 % (3896166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.30/2.13 % (3896166)CaDiCaL version: 2.1.3 % 10.30/2.13 % (3896166)Termination reason: Instruction limit % 10.30/2.13 % (3896166)Termination phase: Saturation % 10.30/2.13 % (3896166)Time elapsed: 0.052 s % 10.30/2.13 % (3896166)Peak memory usage: 88 MB % 10.30/2.13 % (3896166)Instructions burned: 141 (million) % 10.30/2.13 % (3896165)------------------------------ % 10.30/2.13 % (3896165)------------------------------ % 10.30/2.13 % (3896175)lrs+10_1_sil=8000:sp=occurrence:random_seed=1269590064:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 10.30/2.13 % (3896176)lrs+10_1_sil=32000:urr=on:br=off:random_seed=74166272:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 10.30/2.13 % (3896177)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4160171214:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 10.30/2.13 % (3896176)Instruction limit reached! % 10.30/2.13 % (3896176)------------------------------ % 10.30/2.13 % (3896176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.86/2.60 % (3896176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.86/2.60 % (3896176)CaDiCaL version: 2.1.3 % 12.86/2.60 % (3896176)Termination reason: Instruction limit % 12.86/2.60 % (3896176)Termination phase: Saturation % 12.86/2.60 % (3896176)Time elapsed: 0.059 s % 12.86/2.60 % (3896176)Peak memory usage: 89 MB % 12.86/2.60 % (3896176)Instructions burned: 157 (million) % 12.86/2.60 % (3896164)------------------------------ % 12.86/2.60 % (3896164)------------------------------ % 12.86/2.60 % (3896177)Instruction limit reached! % 12.86/2.60 % (3896177)------------------------------ % 12.86/2.60 % (3896177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.86/2.60 % (3896177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.86/2.60 % (3896177)CaDiCaL version: 2.1.3 % 12.86/2.60 % (3896177)Termination reason: Instruction limit % 12.86/2.60 % (3896177)Termination phase: Saturation % 12.86/2.60 % (3896177)Time elapsed: 0.078 s % 12.86/2.60 % (3896177)Peak memory usage: 90 MB % 12.86/2.60 % (3896177)Instructions burned: 329 (million) % 12.86/2.60 % (3896175)Instruction limit reached! % 12.86/2.60 % (3896175)------------------------------ % 12.86/2.60 % (3896175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.86/2.60 % (3896175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.86/2.60 % (3896175)CaDiCaL version: 2.1.3 % 12.86/2.60 % (3896175)Termination reason: Instruction limit % 12.86/2.60 % (3896175)Termination phase: Saturation % 12.86/2.60 % (3896175)Time elapsed: 0.116 s % 12.86/2.60 % (3896175)Peak memory usage: 89 MB % 12.86/2.60 % (3896175)Instructions burned: 287 (million) % 12.86/2.60 % (3896183)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3230562471:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 12.86/2.60 % (3896181)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=323317389:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 12.86/2.60 % (3896182)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3970042585:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 12.86/2.60 % (3896184)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3427025442:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 12.86/2.60 % (3896181)Instruction limit reached! % 12.86/2.60 % (3896181)------------------------------ % 12.86/2.60 % (3896181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.86/2.60 % (3896181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.86/2.60 % (3896181)CaDiCaL version: 2.1.3 % 12.86/2.60 % (3896181)Termination reason: Instruction limit % 12.86/2.60 % (3896181)Termination phase: Saturation % 12.86/2.60 % (3896181)Time elapsed: 0.109 s % 12.86/2.60 % (3896181)Peak memory usage: 90 MB % 12.86/2.60 % (3896181)Instructions burned: 248 (million) % 12.86/2.60 % (3896182)Refutation not found, incomplete strategy % 12.86/2.60 % (3896182)------------------------------ % 12.86/2.60 % (3896182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.86/2.60 % (3896182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.86/2.60 % (3896182)CaDiCaL version: 2.1.3 % 12.86/2.60 % (3896182)Termination reason: Refutation not found, incomplete strategy % 12.86/2.60 % (3896182)Time elapsed: 0.086 s % 12.86/2.60 % (3896182)Peak memory usage: 89 MB % 12.86/2.60 % (3896182)Instructions burned: 239 (million) % 12.86/2.60 % (3896184)Instruction limit reached! % 12.86/2.60 % (3896184)------------------------------ % 12.86/2.60 % (3896184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.86/2.60 % (3896184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.86/2.60 % (3896184)CaDiCaL version: 2.1.3 % 12.86/2.60 % (3896184)Termination reason: Instruction limit % 12.86/2.60 % (3896184)Termination phase: Property scanning % 12.86/2.60 % (3896184)Time elapsed: 0.042 s % 12.86/2.60 % (3896184)Peak memory usage: 87 MB % 12.86/2.60 % (3896184)Instructions burned: 115 (million) % 12.86/2.60 % (3896190)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1231609317:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi) % 12.86/2.60 % (3896189)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1676465438:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 12.86/2.60 % (3896190)Instruction limit reached! % 25.09/4.24 % (3896190)------------------------------ % 25.09/4.24 % (3896190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.09/4.24 % (3896190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.09/4.24 % (3896190)CaDiCaL version: 2.1.3 % 25.09/4.24 % (3896190)Termination reason: Instruction limit % 25.09/4.24 % (3896190)Termination phase: Property scanning % 25.09/4.24 % (3896190)Time elapsed: 0.045 s % 25.09/4.24 % (3896190)Peak memory usage: 88 MB % 25.09/4.24 % (3896190)Instructions burned: 117 (million) % 25.09/4.24 % (3896189)Instruction limit reached! % 25.09/4.24 % (3896189)------------------------------ % 25.09/4.24 % (3896189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.09/4.24 % (3896189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.09/4.24 % (3896189)CaDiCaL version: 2.1.3 % 25.09/4.24 % (3896189)Termination reason: Instruction limit % 25.09/4.24 % (3896189)Termination phase: Blocked clause elimination % 25.09/4.24 % (3896189)Time elapsed: 0.047 s % 25.09/4.24 % (3896189)Peak memory usage: 87 MB % 25.09/4.24 % (3896189)Instructions burned: 127 (million) % 25.09/4.24 % (3896182)------------------------------ % 25.09/4.24 % (3896182)------------------------------ % 25.09/4.24 % (3896193)lrs+10_1_sil=8000:sp=occurrence:random_seed=14419127:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 25.09/4.24 % (3896194)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3916358623:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi) % 25.09/4.24 % (3896195)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1905845394:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 25.09/4.24 % (3896194)Refutation not found, incomplete strategy % 25.09/4.24 % (3896194)------------------------------ % 25.09/4.24 % (3896194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.09/4.24 % (3896194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.09/4.24 % (3896194)CaDiCaL version: 2.1.3 % 25.09/4.24 % (3896194)Termination reason: Refutation not found, incomplete strategy % 25.09/4.24 % (3896194)Time elapsed: 0.074 s % 25.09/4.24 % (3896194)Peak memory usage: 90 MB % 25.09/4.24 % (3896194)Instructions burned: 186 (million) % 25.09/4.24 % (3896194)------------------------------ % 25.09/4.24 % (3896194)------------------------------ % 25.09/4.24 % (3896183)Instruction limit reached! % 25.09/4.24 % (3896183)------------------------------ % 25.09/4.24 % (3896183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.09/4.24 % (3896183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.09/4.24 % (3896183)CaDiCaL version: 2.1.3 % 25.09/4.24 % (3896183)Termination reason: Instruction limit % 25.09/4.24 % (3896183)Termination phase: Saturation % 25.09/4.24 % (3896183)Time elapsed: 0.752 s % 25.09/4.24 % (3896183)Peak memory usage: 149 MB % 25.09/4.24 % (3896183)Instructions burned: 2351 (million) % 25.09/4.24 % (3896193)Instruction limit reached! % 25.09/4.24 % (3896193)------------------------------ % 25.09/4.24 % (3896193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.09/4.24 % (3896193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.09/4.24 % (3896193)CaDiCaL version: 2.1.3 % 25.09/4.24 % (3896193)Termination reason: Instruction limit % 25.09/4.24 % (3896193)Termination phase: Saturation % 25.09/4.24 % (3896193)Time elapsed: 0.374 s % 25.09/4.24 % (3896193)Peak memory usage: 90 MB % 25.09/4.24 % (3896193)Instructions burned: 907 (million) % 25.09/4.24 % (3896200)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=407069814:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi) % 25.09/4.24 % (3896199)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=649811461:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 25.09/4.24 % (3896199)Instruction limit reached! % 25.09/4.24 % (3896199)------------------------------ % 25.09/4.24 % (3896199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.09/4.24 % (3896199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.09/4.24 % (3896199)CaDiCaL version: 2.1.3 % 25.09/4.24 % (3896199)Termination reason: Instruction limit % 25.09/4.24 % (3896199)Termination phase: Property scanning % 25.09/4.24 % (3896199)Time elapsed: 0.052 s % 25.09/4.24 % (3896199)Peak memory usage: 86 MB % 25.09/4.24 % (3896199)Instructions burned: 135 (million) % 25.09/4.24 % (3896201)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1078433845:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 39.90/6.36 % (3896200)Instruction limit reached! % 39.90/6.36 % (3896200)------------------------------ % 39.90/6.36 % (3896200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.90/6.36 % (3896200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.90/6.36 % (3896200)CaDiCaL version: 2.1.3 % 39.90/6.36 % (3896200)Termination reason: Instruction limit % 39.90/6.36 % (3896200)Termination phase: Saturation % 39.90/6.36 % (3896200)Time elapsed: 0.140 s % 39.90/6.36 % (3896200)Peak memory usage: 91 MB % 39.90/6.36 % (3896200)Instructions burned: 592 (million) % 39.90/6.36 % (3896205)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=570612196:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi) % 39.90/6.36 % (3896206)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=236358331:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 39.90/6.36 % (3896206)Instruction limit reached! % 39.90/6.36 % (3896206)------------------------------ % 39.90/6.36 % (3896206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.90/6.36 % (3896206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.90/6.36 % (3896206)CaDiCaL version: 2.1.3 % 39.90/6.36 % (3896206)Termination reason: Instruction limit % 39.90/6.36 % (3896206)Termination phase: Property scanning % 39.90/6.36 % (3896206)Time elapsed: 0.026 s % 39.90/6.36 % (3896206)Peak memory usage: 87 MB % 39.90/6.36 % (3896206)Instructions burned: 136 (million) % 39.90/6.36 % (3896205)Instruction limit reached! % 39.90/6.36 % (3896205)------------------------------ % 39.90/6.36 % (3896205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.90/6.36 % (3896205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.90/6.36 % (3896205)CaDiCaL version: 2.1.3 % 39.90/6.36 % (3896205)Termination reason: Instruction limit % 39.90/6.36 % (3896205)Termination phase: Property scanning % 39.90/6.36 % (3896205)Time elapsed: 0.047 s % 39.90/6.36 % (3896205)Peak memory usage: 87 MB % 39.90/6.36 % (3896205)Instructions burned: 128 (million) % 39.90/6.36 % (3896209)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=281345417:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi) % 39.90/6.36 % (3896209)Instruction limit reached! % 39.90/6.36 % (3896209)------------------------------ % 39.90/6.36 % (3896209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.90/6.36 % (3896209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.90/6.36 % (3896209)CaDiCaL version: 2.1.3 % 39.90/6.36 % (3896209)Termination reason: Instruction limit % 39.90/6.36 % (3896209)Termination phase: Property scanning % 39.90/6.36 % (3896209)Time elapsed: 0.027 s % 39.90/6.36 % (3896209)Peak memory usage: 86 MB % 39.90/6.36 % (3896209)Instructions burned: 143 (million) % 39.90/6.36 % (3896210)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4042852075:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi) % 39.90/6.36 % (3896212)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=2769009487:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi) % 39.90/6.36 % (3896163)Refutation not found, incomplete strategy % 39.90/6.36 % (3896163)------------------------------ % 39.90/6.36 % (3896163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.90/6.36 % (3896163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.90/6.36 % (3896163)CaDiCaL version: 2.1.3 % 39.90/6.36 % (3896163)Termination reason: Refutation not found, incomplete strategy % 39.90/6.36 % (3896163)Time elapsed: 1.735 s % 39.90/6.36 % (3896163)Peak memory usage: 181 MB % 39.90/6.36 % (3896163)Instructions burned: 3537 (million) % 39.90/6.36 % (3896210)Instruction limit reached! % 39.90/6.36 % (3896210)------------------------------ % 39.90/6.36 % (3896210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.90/6.36 % (3896210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.90/6.36 % (3896210)CaDiCaL version: 2.1.3 % 39.90/6.36 % (3896210)Termination reason: Instruction limit % 56.23/8.79 % (3896210)Termination phase: Saturation % 56.23/8.79 % (3896210)Time elapsed: 0.168 s % 56.23/8.79 % (3896210)Peak memory usage: 89 MB % 56.23/8.79 % (3896210)Instructions burned: 433 (million) % 56.23/8.79 % (3896215)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=1002858464:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi) % 56.23/8.79 % (3896215)Instruction limit reached! % 56.23/8.79 % (3896215)------------------------------ % 56.23/8.79 % (3896215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.23/8.79 % (3896215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.23/8.79 % (3896215)CaDiCaL version: 2.1.3 % 56.23/8.79 % (3896215)Termination reason: Instruction limit % 56.23/8.79 % (3896215)Termination phase: General splitting % 56.23/8.79 % (3896215)Time elapsed: 0.056 s % 56.23/8.79 % (3896215)Peak memory usage: 87 MB % 56.23/8.79 % (3896215)Instructions burned: 152 (million) % 56.23/8.79 % (3896163)------------------------------ % 56.23/8.79 % (3896163)------------------------------ % 56.23/8.79 % (3896217)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2164062130:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi) % 56.23/8.79 % (3896218)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3480567196:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi) % 56.23/8.79 % (3896218)Refutation not found, incomplete strategy % 56.23/8.79 % (3896218)------------------------------ % 56.23/8.79 % (3896218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.23/8.79 % (3896218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.23/8.79 % (3896218)CaDiCaL version: 2.1.3 % 56.23/8.79 % (3896218)Termination reason: Refutation not found, incomplete strategy % 56.23/8.79 % (3896218)Time elapsed: 0.252 s % 56.23/8.79 % (3896218)Peak memory usage: 91 MB % 56.23/8.79 % (3896218)Instructions burned: 611 (million) % 56.23/8.79 % (3896218)------------------------------ % 56.23/8.79 % (3896218)------------------------------ % 56.23/8.79 % (3896221)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=2437879299:s2a=on:i=185:s2at=1.8:fdi=4_2971 on theBenchmark for (2971ds/185Mi) % 56.23/8.79 % (3896221)Instruction limit reached! % 56.23/8.79 % (3896221)------------------------------ % 56.23/8.79 % (3896221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.23/8.79 % (3896221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.23/8.79 % (3896221)CaDiCaL version: 2.1.3 % 56.23/8.79 % (3896221)Termination reason: Instruction limit % 56.23/8.79 % (3896221)Termination phase: Saturation % 56.23/8.79 % (3896221)Time elapsed: 0.066 s % 56.23/8.79 % (3896221)Peak memory usage: 87 MB % 56.23/8.79 % (3896221)Instructions burned: 185 (million) % 56.23/8.79 % (3896223)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=647639064:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2969 on theBenchmark for (2969ds/193Mi) % 56.23/8.79 % (3896223)Refutation not found, incomplete strategy % 56.23/8.79 % (3896223)------------------------------ % 56.23/8.79 % (3896223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.23/8.79 % (3896223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.23/8.79 % (3896223)CaDiCaL version: 2.1.3 % 56.23/8.79 % (3896223)Termination reason: Refutation not found, incomplete strategy % 56.23/8.79 % (3896223)Time elapsed: 0.003 s % 56.23/8.79 % (3896223)Peak memory usage: 88 MB % 56.23/8.79 % (3896223)Instructions burned: 5 (million) % 56.23/8.79 % (3896223)------------------------------ % 56.23/8.79 % (3896223)------------------------------ % 56.23/8.79 % (3896225)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3806843975:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2966 on theBenchmark for (2966ds/4850Mi) % 56.23/8.79 % (3896225)Refutation not found, incomplete strategy % 56.23/8.79 % (3896225)------------------------------ % 56.23/8.79 % (3896225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.23/8.79 % (3896225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.23/8.79 % (3896225)CaDiCaL version: 2.1.3 % 56.23/8.79 % (3896225)Termination reason: Refutation not found, incomplete strategy % 71.46/11.01 % (3896225)Time elapsed: 0.059 s % 71.46/11.01 % (3896225)Peak memory usage: 89 MB % 71.46/11.01 % (3896225)Instructions burned: 156 (million) % 71.46/11.01 % (3896212)Instruction limit reached! % 71.46/11.01 % (3896212)------------------------------ % 71.46/11.01 % (3896212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.46/11.01 % (3896212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/11.01 % (3896212)CaDiCaL version: 2.1.3 % 71.46/11.01 % (3896212)Termination reason: Instruction limit % 71.46/11.01 % (3896212)Termination phase: Saturation % 71.46/11.01 % (3896212)Time elapsed: 1.878 s % 71.46/11.01 % (3896212)Peak memory usage: 200 MB % 71.46/11.01 % (3896212)Instructions burned: 6061 (million) % 71.46/11.01 % (3896225)------------------------------ % 71.46/11.01 % (3896225)------------------------------ % 71.46/11.01 % (3896227)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2472768426:i=12111:sd=1:ss=included_2962 on theBenchmark for (2962ds/12111Mi) % 71.46/11.01 % (3896195)Instruction limit reached! % 71.46/11.01 % (3896195)------------------------------ % 71.46/11.01 % (3896195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.46/11.01 % (3896195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/11.01 % (3896195)CaDiCaL version: 2.1.3 % 71.46/11.01 % (3896195)Termination reason: Instruction limit % 71.46/11.01 % (3896195)Termination phase: Saturation % 71.46/11.01 % (3896195)Time elapsed: 2.881 s % 71.46/11.01 % (3896195)Peak memory usage: 155 MB % 71.46/11.01 % (3896195)Instructions burned: 5202 (million) % 71.46/11.01 % (3896229)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4036229384:i=319:kws=precedence:fsr=off_2961 on theBenchmark for (2961ds/319Mi) % 71.46/11.01 % (3896230)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3080950288:i=2064:ep=RST_2960 on theBenchmark for (2960ds/2064Mi) % 71.46/11.01 % (3896229)Instruction limit reached! % 71.46/11.01 % (3896229)------------------------------ % 71.46/11.01 % (3896229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.46/11.01 % (3896229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/11.01 % (3896229)CaDiCaL version: 2.1.3 % 71.46/11.01 % (3896229)Termination reason: Instruction limit % 71.46/11.01 % (3896229)Termination phase: Saturation % 71.46/11.01 % (3896229)Time elapsed: 0.141 s % 71.46/11.01 % (3896229)Peak memory usage: 90 MB % 71.46/11.01 % (3896229)Instructions burned: 320 (million) % 71.46/11.01 % (3896233)dis-1011_128_sil=32000:random_seed=3796887533:i=3706:ep=RST:av=off_2959 on theBenchmark for (2959ds/3706Mi) % 71.46/11.01 % (3896230)Instruction limit reached! % 71.46/11.01 % (3896230)------------------------------ % 71.46/11.01 % (3896230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.46/11.01 % (3896230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/11.01 % (3896230)CaDiCaL version: 2.1.3 % 71.46/11.01 % (3896230)Termination reason: Instruction limit % 71.46/11.01 % (3896230)Termination phase: Saturation % 71.46/11.01 % (3896230)Time elapsed: 0.879 s % 71.46/11.01 % (3896230)Peak memory usage: 94 MB % 71.46/11.01 % (3896230)Instructions burned: 2067 (million) % 71.46/11.01 % (3896235)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1155782294:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2950 on theBenchmark for (2950ds/757Mi) % 71.46/11.01 % (3896235)Refutation not found, incomplete strategy % 71.46/11.01 % (3896235)------------------------------ % 71.46/11.01 % (3896235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.46/11.01 % (3896235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.46/11.01 % (3896235)CaDiCaL version: 2.1.3 % 71.46/11.01 % (3896235)Termination reason: Refutation not found, incomplete strategy % 71.46/11.01 % (3896235)Time elapsed: 0.080 s % 71.46/11.01 % (3896235)Peak memory usage: 89 MB % 71.46/11.01 % (3896235)Instructions burned: 218 (million) % 71.46/11.01 % (3896235)------------------------------ % 71.46/11.01 % (3896235)------------------------------ % 71.46/11.01 % (3896237)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=738099319:i=13913:ss=axioms:sgt=8_2945 on theBenchmark for (2945ds/13913Mi) % 71.46/11.01 % (3896233)Instruction limit reached! % 71.46/11.01 % (3896233)------------------------------ % 71.46/11.01 % (3896233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.46/11.01 % (3896233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.60/12.51 % (3896233)CaDiCaL version: 2.1.3 % 83.60/12.51 % (3896233)Termination reason: Instruction limit % 83.60/12.51 % (3896233)Termination phase: Saturation % 83.60/12.51 % (3896233)Time elapsed: 1.473 s % 83.60/12.51 % (3896233)Peak memory usage: 92 MB % 83.60/12.51 % (3896233)Instructions burned: 3707 (million) % 83.60/12.51 % (3896239)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3041020426:i=9925:aac=none_2942 on theBenchmark for (2942ds/9925Mi) % 83.60/12.51 % (3896239)Refutation not found, incomplete strategy % 83.60/12.51 % (3896239)------------------------------ % 83.60/12.51 % (3896239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.60/12.51 % (3896239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.60/12.51 % (3896239)CaDiCaL version: 2.1.3 % 83.60/12.51 % (3896239)Termination reason: Refutation not found, incomplete strategy % 83.60/12.51 % (3896239)Time elapsed: 0.851 s % 83.60/12.51 % (3896239)Peak memory usage: 150 MB % 83.60/12.51 % (3896239)Instructions burned: 1422 (million) % 83.60/12.51 % (3896239)------------------------------ % 83.60/12.51 % (3896239)------------------------------ % 83.60/12.51 % (3896241)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=868385855:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2930 on theBenchmark for (2930ds/2479Mi) % 83.60/12.51 % (3896241)Refutation not found, incomplete strategy % 83.60/12.51 % (3896241)------------------------------ % 83.60/12.51 % (3896241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.60/12.51 % (3896241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.60/12.51 % (3896241)CaDiCaL version: 2.1.3 % 83.60/12.51 % (3896241)Termination reason: Refutation not found, incomplete strategy % 83.60/12.51 % (3896241)Time elapsed: 0.003 s % 83.60/12.51 % (3896241)Peak memory usage: 88 MB % 83.60/12.51 % (3896241)Instructions burned: 5 (million) % 83.60/12.51 % (3896241)------------------------------ % 83.60/12.51 % (3896241)------------------------------ % 83.60/12.51 % (3896243)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=308208183:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2926 on theBenchmark for (2926ds/440Mi) % 83.60/12.51 % (3896227)Instruction limit reached! % 83.60/12.51 % (3896227)------------------------------ % 83.60/12.51 % (3896227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.60/12.51 % (3896227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.60/12.51 % (3896227)CaDiCaL version: 2.1.3 % 83.60/12.51 % (3896227)Termination reason: Instruction limit % 83.60/12.51 % (3896227)Termination phase: Saturation % 83.60/12.51 % (3896227)Time elapsed: 3.688 s % 83.60/12.51 % (3896227)Peak memory usage: 241 MB % 83.60/12.51 % (3896227)Instructions burned: 12111 (million) % 83.60/12.51 % (3896245)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=588298964:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2924 on theBenchmark for (2924ds/11145Mi) % 83.60/12.51 % (3896243)Instruction limit reached! % 83.60/12.51 % (3896243)------------------------------ % 83.60/12.51 % (3896243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.60/12.51 % (3896243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.60/12.51 % (3896243)CaDiCaL version: 2.1.3 % 83.60/12.51 % (3896243)Termination reason: Instruction limit % 83.60/12.51 % (3896243)Termination phase: Property scanning % 83.60/12.51 % (3896243)Time elapsed: 0.160 s % 83.60/12.51 % (3896243)Peak memory usage: 87 MB % 83.60/12.51 % (3896243)Instructions burned: 440 (million) % 83.60/12.51 % (3896247)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=1574513957:cts=off:i=3034:av=off:er=known:fsd=on_2923 on theBenchmark for (2923ds/3034Mi) % 83.60/12.51 % (3896245)Refutation not found, incomplete strategy % 83.60/12.51 % (3896245)------------------------------ % 83.60/12.51 % (3896245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.60/12.51 % (3896245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.60/12.51 % (3896245)CaDiCaL version: 2.1.3 % 83.60/12.51 % (3896245)Termination reason: Refutation not found, incomplete strategy % 83.60/12.51 % (3896245)Time elapsed: 0.372 s % 83.60/12.51 % (3896245)Peak memory usage: 128 MB % 83.60/12.51 % (3896245)Instructions burned: 920 (million) % 83.60/12.51 % (3896245)------------------------------ % 83.60/12.51 % (3896245)------------------------------ % 90.91/13.70 % (3896249)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=4128264001:st=2:s2a=on:i=524:s2at=2:ss=axioms_2918 on theBenchmark for (2918ds/524Mi) % 90.91/13.70 % (3896249)Instruction limit reached! % 90.91/13.70 % (3896249)------------------------------ % 90.91/13.70 % (3896249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.91/13.70 % (3896249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.91/13.70 % (3896249)CaDiCaL version: 2.1.3 % 90.91/13.70 % (3896249)Termination reason: Instruction limit % 90.91/13.70 % (3896249)Termination phase: Saturation % 90.91/13.70 % (3896249)Time elapsed: 0.117 s % 90.91/13.70 % (3896249)Peak memory usage: 89 MB % 90.91/13.70 % (3896249)Instructions burned: 538 (million) % 90.91/13.70 % (3896251)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1170263170:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2916 on theBenchmark for (2916ds/1016Mi) % 90.91/13.70 % (3896251)Refutation not found, incomplete strategy % 90.91/13.70 % (3896251)------------------------------ % 90.91/13.70 % (3896251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.91/13.70 % (3896251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.91/13.70 % (3896251)CaDiCaL version: 2.1.3 % 90.91/13.70 % (3896251)Termination reason: Refutation not found, incomplete strategy % 90.91/13.70 % (3896251)Time elapsed: 0.001 s % 90.91/13.70 % (3896251)Peak memory usage: 89 MB % 90.91/13.70 % (3896251)Instructions burned: 2 (million) % 90.91/13.70 % (3896201)Instruction limit reached! % 90.91/13.70 % (3896201)------------------------------ % 90.91/13.70 % (3896201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.91/13.70 % (3896201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.91/13.70 % (3896201)CaDiCaL version: 2.1.3 % 90.91/13.70 % (3896201)Termination reason: Instruction limit % 90.91/13.70 % (3896201)Termination phase: Saturation % 90.91/13.70 % (3896201)Time elapsed: 7.090 s % 90.91/13.70 % (3896201)Peak memory usage: 206 MB % 90.91/13.70 % (3896201)Instructions burned: 13193 (million) % 90.91/13.70 % (3896251)------------------------------ % 90.91/13.70 % (3896251)------------------------------ % 90.91/13.70 % (3896253)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4041073726:i=14123:bd=preordered:ins=4_2914 on theBenchmark for (2914ds/14123Mi) % 90.91/13.70 % (3896254)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1483816446:i=5781:kws=precedence:bd=all:rawr=on_2913 on theBenchmark for (2913ds/5781Mi) % 90.91/13.70 % (3896247)Instruction limit reached! % 90.91/13.70 % (3896247)------------------------------ % 90.91/13.70 % (3896247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.91/13.70 % (3896247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.91/13.70 % (3896247)CaDiCaL version: 2.1.3 % 90.91/13.70 % (3896247)Termination reason: Instruction limit % 90.91/13.70 % (3896247)Termination phase: Saturation % 90.91/13.70 % (3896247)Time elapsed: 1.783 s % 90.91/13.70 % (3896247)Peak memory usage: 149 MB % 90.91/13.70 % (3896247)Instructions burned: 3034 (million) % 90.91/13.70 % (3896257)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=1894590993:i=2448:gtgl=5:bd=preordered:gtg=all_2904 on theBenchmark for (2904ds/2448Mi) % 90.91/13.70 % (3896217)Instruction limit reached! % 90.91/13.70 % (3896217)------------------------------ % 90.91/13.70 % (3896217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.91/13.70 % (3896217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.91/13.70 % (3896217)CaDiCaL version: 2.1.3 % 90.91/13.70 % (3896217)Termination reason: Instruction limit % 90.91/13.70 % (3896217)Termination phase: Saturation % 90.91/13.70 % (3896217)Time elapsed: 7.584 s % 90.91/13.70 % (3896217)Peak memory usage: 237 MB % 90.91/13.70 % (3896217)Instructions burned: 14155 (million) % 90.91/13.70 % (3896259)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3183761342:i=3223:kws=precedence:fgj=on:av=off_2901 on theBenchmark for (2901ds/3223Mi) % 90.91/13.70 % (3896254)Instruction limit reached! % 90.91/13.70 % (3896254)------------------------------ % 90.91/13.70 % (3896254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.91/13.70 % (3896254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896254)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896254)Termination reason: Instruction limit % 107.15/15.87 % (3896254)Termination phase: Saturation % 107.15/15.87 % (3896254)Time elapsed: 1.469 s % 107.15/15.87 % (3896254)Peak memory usage: 123 MB % 107.15/15.87 % (3896254)Instructions burned: 5791 (million) % 107.15/15.87 % (3896261)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2089477203:st=5.6:i=2033:sd=3:ss=axioms_2896 on theBenchmark for (2896ds/2033Mi) % 107.15/15.87 % (3896261)Refutation not found, incomplete strategy % 107.15/15.87 % (3896261)------------------------------ % 107.15/15.87 % (3896261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.15/15.87 % (3896261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896261)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896261)Termination reason: Refutation not found, incomplete strategy % 107.15/15.87 % (3896261)Time elapsed: 0.446 s % 107.15/15.87 % (3896261)Peak memory usage: 144 MB % 107.15/15.87 % (3896261)Instructions burned: 1166 (million) % 107.15/15.87 % (3896257)Instruction limit reached! % 107.15/15.87 % (3896257)------------------------------ % 107.15/15.87 % (3896257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.15/15.87 % (3896257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896257)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896257)Termination reason: Instruction limit % 107.15/15.87 % (3896257)Termination phase: Saturation % 107.15/15.87 % (3896257)Time elapsed: 1.276 s % 107.15/15.87 % (3896257)Peak memory usage: 146 MB % 107.15/15.87 % (3896257)Instructions burned: 2448 (million) % 107.15/15.87 % (3896261)------------------------------ % 107.15/15.87 % (3896261)------------------------------ % 107.15/15.87 % (3896263)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3277743753:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2890 on theBenchmark for (2890ds/2055Mi) % 107.15/15.87 % (3896264)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=3711559201:i=21611:sd=3:ss=axioms_2889 on theBenchmark for (2889ds/21611Mi) % 107.15/15.87 % (3896264)Refutation not found, incomplete strategy % 107.15/15.87 % (3896264)------------------------------ % 107.15/15.87 % (3896264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.15/15.87 % (3896264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896264)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896264)Termination reason: Refutation not found, incomplete strategy % 107.15/15.87 % (3896264)Time elapsed: 0.332 s % 107.15/15.87 % (3896264)Peak memory usage: 128 MB % 107.15/15.87 % (3896264)Instructions burned: 874 (million) % 107.15/15.87 % (3896264)------------------------------ % 107.15/15.87 % (3896264)------------------------------ % 107.15/15.87 % (3896263)Refutation not found, incomplete strategy % 107.15/15.87 % (3896263)------------------------------ % 107.15/15.87 % (3896263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.15/15.87 % (3896263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896263)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896263)Termination reason: Refutation not found, incomplete strategy % 107.15/15.87 % (3896263)Time elapsed: 0.578 s % 107.15/15.87 % (3896263)Peak memory usage: 128 MB % 107.15/15.87 % (3896263)Instructions burned: 873 (million) % 107.15/15.87 % (3896267)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1060630950:i=4835:sd=13:ss=axioms:sgt=23_2883 on theBenchmark for (2883ds/4835Mi) % 107.15/15.87 % (3896267)Refutation not found, incomplete strategy % 107.15/15.87 % (3896267)------------------------------ % 107.15/15.87 % (3896267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.15/15.87 % (3896267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896267)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896267)Termination reason: Refutation not found, incomplete strategy % 107.15/15.87 % (3896267)Time elapsed: 0.095 s % 107.15/15.87 % (3896267)Peak memory usage: 91 MB % 107.15/15.87 % (3896267)Instructions burned: 433 (million) % 107.15/15.87 % (3896259)Instruction limit reached! % 107.15/15.87 % (3896259)------------------------------ % 107.15/15.87 % (3896259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.15/15.87 % (3896259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.15/15.87 % (3896259)CaDiCaL version: 2.1.3 % 107.15/15.87 % (3896259)Termination reason: Instruction limit % 126.54/18.61 % (3896259)Termination phase: Saturation % 126.54/18.61 % (3896259)Time elapsed: 1.833 s % 126.54/18.61 % (3896259)Peak memory usage: 159 MB % 126.54/18.61 % (3896259)Instructions burned: 3223 (million) % 126.54/18.61 % (3896263)------------------------------ % 126.54/18.61 % (3896263)------------------------------ % 126.54/18.61 % (3896267)------------------------------ % 126.54/18.61 % (3896267)------------------------------ % 126.54/18.61 % (3896269)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=2501523047:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2881 on theBenchmark for (2881ds/797Mi) % 126.54/18.61 % (3896271)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2222935971:i=6038:nm=6_2880 on theBenchmark for (2880ds/6038Mi) % 126.54/18.61 % (3896270)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2943891013:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2880 on theBenchmark for (2880ds/2326Mi) % 126.54/18.61 % (3896270)Refutation not found, incomplete strategy % 126.54/18.61 % (3896270)------------------------------ % 126.54/18.61 % (3896270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.54/18.61 % (3896270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.54/18.61 % (3896270)CaDiCaL version: 2.1.3 % 126.54/18.61 % (3896270)Termination reason: Refutation not found, incomplete strategy % 126.54/18.61 % (3896270)Time elapsed: 0.169 s % 126.54/18.61 % (3896270)Peak memory usage: 91 MB % 126.54/18.61 % (3896270)Instructions burned: 457 (million) % 126.54/18.61 % (3896269)Instruction limit reached! % 126.54/18.61 % (3896269)------------------------------ % 126.54/18.61 % (3896269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.54/18.61 % (3896269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.54/18.61 % (3896269)CaDiCaL version: 2.1.3 % 126.54/18.61 % (3896269)Termination reason: Instruction limit % 126.54/18.61 % (3896269)Termination phase: Saturation % 126.54/18.61 % (3896269)Time elapsed: 0.336 s % 126.54/18.61 % (3896269)Peak memory usage: 89 MB % 126.54/18.61 % (3896269)Instructions burned: 797 (million) % 126.54/18.61 % (3896275)lrs+10_1_sil=32000:sp=occurrence:random_seed=585161660:st=2:i=33334:sd=3:ss=included:sgt=32_2876 on theBenchmark for (2876ds/33334Mi) % 126.54/18.61 % (3896270)------------------------------ % 126.54/18.61 % (3896270)------------------------------ % 126.54/18.61 % (3896271)Refutation not found, incomplete strategy % 126.54/18.61 % (3896271)------------------------------ % 126.54/18.61 % (3896271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.54/18.61 % (3896271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.54/18.61 % (3896271)CaDiCaL version: 2.1.3 % 126.54/18.61 % (3896271)Termination reason: Refutation not found, incomplete strategy % 126.54/18.61 % (3896271)Time elapsed: 0.457 s % 126.54/18.61 % (3896271)Peak memory usage: 139 MB % 126.54/18.61 % (3896271)Instructions burned: 1435 (million) % 126.54/18.61 % (3896277)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2650174718:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2875 on theBenchmark for (2875ds/1008Mi) % 126.54/18.61 % (3896271)------------------------------ % 126.54/18.61 % (3896271)------------------------------ % 126.54/18.61 % (3896279)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2154167975:i=8327:s2at=5:bd=preordered_2873 on theBenchmark for (2873ds/8327Mi) % 126.54/18.61 % (3896237)Instruction limit reached! % 126.54/18.61 % (3896237)------------------------------ % 126.54/18.61 % (3896237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.54/18.61 % (3896237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.54/18.61 % (3896237)CaDiCaL version: 2.1.3 % 126.54/18.61 % (3896237)Termination reason: Instruction limit % 126.54/18.61 % (3896237)Termination phase: Saturation % 126.54/18.61 % (3896237)Time elapsed: 7.471 s % 126.54/18.61 % (3896237)Peak memory usage: 216 MB % 126.54/18.61 % (3896237)Instructions burned: 13915 (million) % 126.54/18.61 % (3896277)Instruction limit reached! % 126.54/18.61 % (3896277)------------------------------ % 126.54/18.61 % (3896277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.54/18.61 % (3896277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.61/22.29 % (3896277)CaDiCaL version: 2.1.3 % 152.61/22.29 % (3896277)Termination reason: Instruction limit % 152.61/22.29 % (3896277)Termination phase: Saturation % 152.61/22.29 % (3896277)Time elapsed: 0.426 s % 152.61/22.29 % (3896277)Peak memory usage: 91 MB % 152.61/22.29 % (3896277)Instructions burned: 1009 (million) % 152.61/22.29 % (3896282)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2844346786:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2869 on theBenchmark for (2869ds/1084Mi) % 152.61/22.29 % (3896281)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2677713352:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2869 on theBenchmark for (2869ds/1083Mi) % 152.61/22.29 % (3896281)Instruction limit reached! % 152.61/22.29 % (3896281)------------------------------ % 152.61/22.29 % (3896281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.61/22.29 % (3896281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.61/22.29 % (3896281)CaDiCaL version: 2.1.3 % 152.61/22.29 % (3896281)Termination reason: Instruction limit % 152.61/22.29 % (3896281)Termination phase: Saturation % 152.61/22.29 % (3896281)Time elapsed: 0.413 s % 152.61/22.29 % (3896281)Peak memory usage: 92 MB % 152.61/22.29 % (3896281)Instructions burned: 1085 (million) % 152.61/22.29 % (3896282)Instruction limit reached! % 152.61/22.29 % (3896282)------------------------------ % 152.61/22.29 % (3896282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.61/22.29 % (3896282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.61/22.29 % (3896282)CaDiCaL version: 2.1.3 % 152.61/22.29 % (3896282)Termination reason: Instruction limit % 152.61/22.29 % (3896282)Termination phase: Saturation % 152.61/22.29 % (3896282)Time elapsed: 0.474 s % 152.61/22.29 % (3896282)Peak memory usage: 94 MB % 152.61/22.29 % (3896282)Instructions burned: 1085 (million) % 152.61/22.29 % (3896285)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3289168538:i=6995:s2at=5:gtg=all_2864 on theBenchmark for (2864ds/6995Mi) % 152.61/22.29 % (3896286)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1951038549:st=2:i=6225:sd=15:ss=axioms_2863 on theBenchmark for (2863ds/6225Mi) % 152.61/22.29 % (3896286)Refutation not found, incomplete strategy % 152.61/22.29 % (3896286)------------------------------ % 152.61/22.29 % (3896286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.61/22.29 % (3896286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.61/22.29 % (3896286)CaDiCaL version: 2.1.3 % 152.61/22.29 % (3896286)Termination reason: Refutation not found, incomplete strategy % 152.61/22.29 % (3896286)Time elapsed: 0.085 s % 152.61/22.29 % (3896286)Peak memory usage: 90 MB % 152.61/22.29 % (3896286)Instructions burned: 215 (million) % 152.61/22.29 % (3896286)------------------------------ % 152.61/22.29 % (3896286)------------------------------ % 152.61/22.29 % (3896289)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2936824514:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2858 on theBenchmark for (2858ds/3372Mi) % 152.61/22.29 % (3896289)Refutation not found, incomplete strategy % 152.61/22.29 % (3896289)------------------------------ % 152.61/22.29 % (3896289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.61/22.29 % (3896289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.61/22.29 % (3896289)CaDiCaL version: 2.1.3 % 152.61/22.29 % (3896289)Termination reason: Refutation not found, incomplete strategy % 152.61/22.29 % (3896289)Time elapsed: 0.579 s % 152.61/22.29 % (3896289)Peak memory usage: 128 MB % 152.61/22.29 % (3896289)Instructions burned: 877 (million) % 152.61/22.29 % (3896289)------------------------------ % 152.61/22.29 % (3896289)------------------------------ % 152.61/22.29 % (3896279)Instruction limit reached! % 152.61/22.29 % (3896279)------------------------------ % 152.61/22.29 % (3896279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.61/22.29 % (3896279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.61/22.29 % (3896279)CaDiCaL version: 2.1.3 % 152.61/22.29 % (3896279)Termination reason: Instruction limit % 152.61/22.29 % (3896279)Termination phase: Saturation % 152.61/22.29 % (3896279)Time elapsed: 2.419 s % 152.61/22.29 % (3896279)Peak memory usage: 180 MB % 152.61/22.29 % (3896279)Instructions burned: 8330 (million) % 152.61/22.29 % (3896291)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=46218275:st=2.3:i=26457:sd=10:ss=included:sgt=8_2849 on theBenchmark for (2849ds/26457Mi) % 190.93/27.68 % (3896292)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=865480623:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2848 on theBenchmark for (2848ds/13494Mi) % 190.93/27.68 % (3896291)Refutation not found, incomplete strategy % 190.93/27.68 % (3896291)------------------------------ % 190.93/27.68 % (3896291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.93/27.68 % (3896291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.68 % (3896291)CaDiCaL version: 2.1.3 % 190.93/27.68 % (3896291)Termination reason: Refutation not found, incomplete strategy % 190.93/27.68 % (3896291)Time elapsed: 0.832 s % 190.93/27.68 % (3896291)Peak memory usage: 139 MB % 190.93/27.68 % (3896291)Instructions burned: 1424 (million) % 190.93/27.68 % (3896291)------------------------------ % 190.93/27.68 % (3896291)------------------------------ % 190.93/27.68 % (3896253)Instruction limit reached! % 190.93/27.68 % (3896253)------------------------------ % 190.93/27.68 % (3896253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.93/27.68 % (3896253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.68 % (3896253)CaDiCaL version: 2.1.3 % 190.93/27.68 % (3896253)Termination reason: Instruction limit % 190.93/27.68 % (3896253)Termination phase: Saturation % 190.93/27.68 % (3896253)Time elapsed: 7.576 s % 190.93/27.68 % (3896253)Peak memory usage: 177 MB % 190.93/27.68 % (3896253)Instructions burned: 14123 (million) % 190.93/27.68 % (3896295)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1895576383:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2837 on theBenchmark for (2837ds/2503Mi) % 190.93/27.68 % (3896296)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2587844055:i=2559:sd=1:ep=RSTC:ss=axioms_2836 on theBenchmark for (2836ds/2559Mi) % 190.93/27.68 % (3896296)Refutation not found, incomplete strategy % 190.93/27.68 % (3896296)------------------------------ % 190.93/27.68 % (3896296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.93/27.68 % (3896296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.68 % (3896296)CaDiCaL version: 2.1.3 % 190.93/27.68 % (3896296)Termination reason: Refutation not found, incomplete strategy % 190.93/27.68 % (3896296)Time elapsed: 0.593 s % 190.93/27.68 % (3896296)Peak memory usage: 128 MB % 190.93/27.68 % (3896296)Instructions burned: 904 (million) % 190.93/27.68 % (3896296)------------------------------ % 190.93/27.68 % (3896296)------------------------------ % 190.93/27.68 % (3896299)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4010376709:i=30753:av=off:ss=included_2827 on theBenchmark for (2827ds/30753Mi) % 190.93/27.68 % (3896285)Instruction limit reached! % 190.93/27.68 % (3896285)------------------------------ % 190.93/27.68 % (3896285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.93/27.68 % (3896285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.68 % (3896285)CaDiCaL version: 2.1.3 % 190.93/27.68 % (3896285)Termination reason: Instruction limit % 190.93/27.68 % (3896285)Termination phase: Saturation % 190.93/27.68 % (3896285)Time elapsed: 3.789 s % 190.93/27.68 % (3896285)Peak memory usage: 194 MB % 190.93/27.68 % (3896285)Instructions burned: 6996 (million) % 190.93/27.68 % (3896301)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3572834718:i=26473:ep=RSTC_2824 on theBenchmark for (2824ds/26473Mi) % 190.93/27.68 % (3896295)Instruction limit reached! % 190.93/27.68 % (3896295)------------------------------ % 190.93/27.68 % (3896295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.93/27.68 % (3896295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.68 % (3896295)CaDiCaL version: 2.1.3 % 190.93/27.68 % (3896295)Termination reason: Instruction limit % 190.93/27.68 % (3896295)Termination phase: Saturation % 190.93/27.68 % (3896295)Time elapsed: 1.392 s % 190.93/27.68 % (3896295)Peak memory usage: 146 MB % 190.93/27.68 % (3896295)Instructions burned: 2503 (million) % 190.93/27.68 % (3896303)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=4093693555:cts=off:i=2759:kws=inv_arity:fgj=on_2821 on theBenchmark for (2821ds/2759Mi) % 220.63/31.85 % (3896303)Refutation not found, incomplete strategy % 220.63/31.85 % (3896303)------------------------------ % 220.63/31.85 % (3896303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/31.85 % (3896303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/31.85 % (3896303)CaDiCaL version: 2.1.3 % 220.63/31.85 % (3896303)Termination reason: Refutation not found, incomplete strategy % 220.63/31.85 % (3896303)Time elapsed: 0.777 s % 220.63/31.85 % (3896303)Peak memory usage: 147 MB % 220.63/31.85 % (3896303)Instructions burned: 1292 (million) % 220.63/31.85 % (3896303)------------------------------ % 220.63/31.85 % (3896303)------------------------------ % 220.63/31.85 % (3896305)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2598339852:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2810 on theBenchmark for (2810ds/5665Mi) % 220.63/31.85 % (3896292)Instruction limit reached! % 220.63/31.85 % (3896292)------------------------------ % 220.63/31.85 % (3896292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/31.85 % (3896292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/31.85 % (3896292)CaDiCaL version: 2.1.3 % 220.63/31.85 % (3896292)Termination reason: Instruction limit % 220.63/31.85 % (3896292)Termination phase: Saturation % 220.63/31.85 % (3896292)Time elapsed: 3.987 s % 220.63/31.85 % (3896292)Peak memory usage: 255 MB % 220.63/31.85 % (3896292)Instructions burned: 13494 (million) % 220.63/31.85 % (3896307)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=1647239555:i=1532:ep=RS:ss=axioms_2807 on theBenchmark for (2807ds/1532Mi) % 220.63/31.85 % (3896307)Refutation not found, incomplete strategy % 220.63/31.85 % (3896307)------------------------------ % 220.63/31.85 % (3896307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/31.85 % (3896307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/31.85 % (3896307)CaDiCaL version: 2.1.3 % 220.63/31.85 % (3896307)Termination reason: Refutation not found, incomplete strategy % 220.63/31.85 % (3896307)Time elapsed: 0.353 s % 220.63/31.85 % (3896307)Peak memory usage: 128 MB % 220.63/31.85 % (3896307)Instructions burned: 891 (million) % 220.63/31.85 % (3896307)------------------------------ % 220.63/31.85 % (3896307)------------------------------ % 220.63/31.85 % (3896309)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=4287485738:i=1565:sd=2:ss=axioms:sgt=32_2801 on theBenchmark for (2801ds/1565Mi) % 220.63/31.85 % (3896309)Instruction limit reached! % 220.63/31.85 % (3896309)------------------------------ % 220.63/31.85 % (3896309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/31.85 % (3896309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/31.85 % (3896309)CaDiCaL version: 2.1.3 % 220.63/31.85 % (3896309)Termination reason: Instruction limit % 220.63/31.85 % (3896309)Termination phase: Saturation % 220.63/31.85 % (3896309)Time elapsed: 0.536 s % 220.63/31.85 % (3896309)Peak memory usage: 179 MB % 220.63/31.85 % (3896309)Instructions burned: 1568 (million) % 220.63/31.85 % (3896311)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=4046767241:i=1572:fgj=on:gsp=on_2794 on theBenchmark for (2794ds/1572Mi) % 220.63/31.85 % (3896311)Instruction limit reached! % 220.63/31.85 % (3896311)------------------------------ % 220.63/31.85 % (3896311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/31.85 % (3896311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/31.85 % (3896311)CaDiCaL version: 2.1.3 % 220.63/31.85 % (3896311)Termination reason: Instruction limit % 220.63/31.85 % (3896311)Termination phase: Saturation % 220.63/31.85 % (3896311)Time elapsed: 0.488 s % 220.63/31.85 % (3896311)Peak memory usage: 144 MB % 220.63/31.85 % (3896311)Instructions burned: 1577 (million) % 220.63/31.85 % (3896313)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2084374410:i=6052:sd=4:ss=axioms:sgt=24_2789 on theBenchmark for (2789ds/6052Mi) % 220.63/31.85 % (3896313)Refutation not found, incomplete strategy % 220.63/31.85 % (3896313)------------------------------ % 220.63/31.85 % (3896313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.42/36.89 % (3896313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.42/36.89 % (3896313)CaDiCaL version: 2.1.3 % 255.42/36.89 % (3896313)Termination reason: Refutation not found, incomplete strategy % 255.42/36.89 % (3896313)Time elapsed: 0.451 s % 255.42/36.89 % (3896313)Peak memory usage: 146 MB % 255.42/36.89 % (3896313)Instructions burned: 1306 (million) % 255.42/36.89 % (3896313)------------------------------ % 255.42/36.89 % (3896313)------------------------------ % 255.42/36.89 % (3896315)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=1352294387:i=3500:sd=1:bd=preordered:sup=off:ss=included_2782 on theBenchmark for (2782ds/3500Mi) % 255.42/36.89 % (3896315)Refutation not found, incomplete strategy % 255.42/36.89 % (3896315)------------------------------ % 255.42/36.89 % (3896315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.42/36.89 % (3896315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.42/36.89 % (3896315)CaDiCaL version: 2.1.3 % 255.42/36.89 % (3896315)Termination reason: Refutation not found, incomplete strategy % 255.42/36.89 % (3896315)Time elapsed: 0.509 s % 255.42/36.89 % (3896315)Peak memory usage: 149 MB % 255.42/36.89 % (3896315)Instructions burned: 1501 (million) % 255.42/36.89 % (3896315)------------------------------ % 255.42/36.89 % (3896315)------------------------------ % 255.42/36.89 % (3896317)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=2418846709:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2774 on theBenchmark for (2774ds/1842Mi) % 255.42/36.89 % (3896317)Instruction limit reached! % 255.42/36.89 % (3896317)------------------------------ % 255.42/36.89 % (3896317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.42/36.89 % (3896317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.42/36.89 % (3896317)CaDiCaL version: 2.1.3 % 255.42/36.89 % (3896317)Termination reason: Instruction limit % 255.42/36.89 % (3896317)Termination phase: Saturation % 255.42/36.89 % (3896317)Time elapsed: 0.443 s % 255.42/36.89 % (3896317)Peak memory usage: 114 MB % 255.42/36.89 % (3896317)Instructions burned: 1843 (million) % 255.42/36.89 % (3896319)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1551369891:i=66096:add=on_2769 on theBenchmark for (2769ds/66096Mi) % 255.42/36.89 % (3896305)Instruction limit reached! % 255.42/36.89 % (3896305)------------------------------ % 255.42/36.89 % (3896305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.42/36.89 % (3896305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.42/36.89 % (3896305)CaDiCaL version: 2.1.3 % 255.42/36.89 % (3896305)Termination reason: Instruction limit % 255.42/36.89 % (3896305)Termination phase: Saturation % 255.42/36.89 % (3896305)Time elapsed: 4.212 s % 255.42/36.89 % (3896305)Peak memory usage: 158 MB % 255.42/36.89 % (3896305)Instructions burned: 5665 (million) % 255.42/36.89 % (3896321)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=971651022:i=1884:sd=1:nm=60:ss=axioms_2766 on theBenchmark for (2766ds/1884Mi) % 255.42/36.89 % (3896321)Refutation not found, incomplete strategy % 255.42/36.89 % (3896321)------------------------------ % 255.42/36.89 % (3896321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.42/36.89 % (3896321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.42/36.89 % (3896321)CaDiCaL version: 2.1.3 % 255.42/36.89 % (3896321)Termination reason: Refutation not found, incomplete strategy % 255.42/36.89 % (3896321)Time elapsed: 0.567 s % 255.42/36.89 % (3896321)Peak memory usage: 128 MB % 255.42/36.89 % (3896321)Instructions burned: 863 (million) % 255.42/36.89 % (3896321)------------------------------ % 255.42/36.89 % (3896321)------------------------------ % 255.42/36.89 % (3896323)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2034778775:cts=off:i=5469:bs=on:fsr=off_2757 on theBenchmark for (2757ds/5469Mi) % 255.42/36.89 % (3896323)Instruction limit reached! % 255.42/36.89 % (3896323)------------------------------ % 255.42/36.89 % (3896323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.42/36.89 % (3896323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.42/36.89 % (3896323)CaDiCaL version: 2.1.3 % 255.42/36.89 % (3896323)Termination reason: Instruction limit % 269.48/38.87 % (3896323)Termination phase: Saturation % 269.48/38.87 % (3896323)Time elapsed: 2.607 s % 269.48/38.87 % (3896323)Peak memory usage: 106 MB % 269.48/38.87 % (3896323)Instructions burned: 5470 (million) % 269.48/38.87 % (3896325)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=1573959543:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2729 on theBenchmark for (2729ds/2037Mi) % 269.48/38.87 % (3896275)Instruction limit reached! % 269.48/38.87 % (3896275)------------------------------ % 269.48/38.87 % (3896275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.48/38.87 % (3896275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.48/38.87 % (3896275)CaDiCaL version: 2.1.3 % 269.48/38.87 % (3896275)Termination reason: Instruction limit % 269.48/38.87 % (3896275)Termination phase: Saturation % 269.48/38.87 % (3896275)Time elapsed: 15.500 s % 269.48/38.87 % (3896275)Peak memory usage: 120 MB % 269.48/38.87 % (3896275)Instructions burned: 33334 (million) % 269.48/38.87 % (3896327)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=664829660:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2720 on theBenchmark for (2720ds/2110Mi) % 269.48/38.87 % (3896325)Instruction limit reached! % 269.48/38.87 % (3896325)------------------------------ % 269.48/38.87 % (3896325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.48/38.87 % (3896325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.48/38.87 % (3896325)CaDiCaL version: 2.1.3 % 269.48/38.87 % (3896325)Termination reason: Instruction limit % 269.48/38.87 % (3896325)Termination phase: Saturation % 269.48/38.87 % (3896325)Time elapsed: 1.074 s % 269.48/38.87 % (3896325)Peak memory usage: 148 MB % 269.48/38.87 % (3896325)Instructions burned: 2039 (million) % 269.48/38.87 % (3896329)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=2999348334:i=2430:add=off:aac=none:nm=16_2717 on theBenchmark for (2717ds/2430Mi) % 269.48/38.87 % (3896327)Instruction limit reached! % 269.48/38.87 % (3896327)------------------------------ % 269.48/38.87 % (3896327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.48/38.87 % (3896327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.48/38.87 % (3896327)CaDiCaL version: 2.1.3 % 269.48/38.87 % (3896327)Termination reason: Instruction limit % 269.48/38.87 % (3896327)Termination phase: Saturation % 269.48/38.87 % (3896327)Time elapsed: 1.174 s % 269.48/38.87 % (3896327)Peak memory usage: 150 MB % 269.48/38.87 % (3896327)Instructions burned: 2110 (million) % 269.48/38.87 % (3896331)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=315657022:cond=fast:i=4891_2707 on theBenchmark for (2707ds/4891Mi) % 269.48/38.87 % (3896329)Instruction limit reached! % 269.48/38.87 % (3896329)------------------------------ % 269.48/38.87 % (3896329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.48/38.87 % (3896329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.48/38.87 % (3896329)CaDiCaL version: 2.1.3 % 269.48/38.87 % (3896329)Termination reason: Instruction limit % 269.48/38.87 % (3896329)Termination phase: Saturation % 269.48/38.87 % (3896329)Time elapsed: 1.371 s % 269.48/38.87 % (3896329)Peak memory usage: 160 MB % 269.48/38.87 % (3896329)Instructions burned: 2431 (million) % 269.48/38.87 % (3896333)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=2734251631:st=2:i=14845:sd=2:ss=included:fsd=on_2702 on theBenchmark for (2702ds/14845Mi) % 269.48/38.87 % (3896333)Refutation not found, incomplete strategy % 269.48/38.87 % (3896333)------------------------------ % 269.48/38.87 % (3896333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.48/38.87 % (3896333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.48/38.87 % (3896333)CaDiCaL version: 2.1.3 % 269.48/38.87 % (3896333)Termination reason: Refutation not found, incomplete strategy % 269.48/38.87 % (3896333)Time elapsed: 0.935 s % 269.48/38.87 % (3896333)Peak memory usage: 167 MB % 269.48/38.87 % (3896333)Instructions burned: 1622 (million) % 269.48/38.87 % (3896333)------------------------------ % 269.48/38.87 % (3896333)------------------------------ % 269.48/38.87 % (3896335)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=274053278:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2689 on theBenchmark for (2689ds/7534Mi) % 295.11/42.30 % (3896301)Instruction limit reached! % 295.11/42.30 % (3896301)------------------------------ % 295.11/42.30 % (3896301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.11/42.30 % (3896301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.11/42.30 % (3896301)CaDiCaL version: 2.1.3 % 295.11/42.30 % (3896301)Termination reason: Instruction limit % 295.11/42.30 % (3896301)Termination phase: Saturation % 295.11/42.30 % (3896301)Time elapsed: 13.790 s % 295.11/42.30 % (3896301)Peak memory usage: 672 MB % 295.11/42.30 % (3896301)Instructions burned: 26475 (million) % 295.11/42.30 % (3896337)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=1018330776:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2684 on theBenchmark for (2684ds/10353Mi) % 295.11/42.30 % (3896331)Instruction limit reached! % 295.11/42.30 % (3896331)------------------------------ % 295.11/42.30 % (3896331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.11/42.30 % (3896331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.11/42.30 % (3896331)CaDiCaL version: 2.1.3 % 295.11/42.30 % (3896331)Termination reason: Instruction limit % 295.11/42.30 % (3896331)Termination phase: Saturation % 295.11/42.30 % (3896331)Time elapsed: 2.825 s % 295.11/42.30 % (3896331)Peak memory usage: 170 MB % 295.11/42.30 % (3896331)Instructions burned: 4891 (million) % 295.11/42.30 % (3896339)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1117633270:i=7860_2677 on theBenchmark for (2677ds/7860Mi) % 295.11/42.30 % (3896339)Refutation not found, incomplete strategy % 295.11/42.30 % (3896339)------------------------------ % 295.11/42.30 % (3896339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.11/42.30 % (3896339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.11/42.30 % (3896339)CaDiCaL version: 2.1.3 % 295.11/42.30 % (3896339)Termination reason: Refutation not found, incomplete strategy % 295.11/42.30 % (3896339)Time elapsed: 0.073 s % 295.11/42.30 % (3896339)Peak memory usage: 90 MB % 295.11/42.30 % (3896339)Instructions burned: 185 (million) % 295.11/42.30 % (3896339)------------------------------ % 295.11/42.30 % (3896339)------------------------------ % 295.11/42.30 % (3896341)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=30749725:i=7896:sd=2:bs=on:ss=included:sgt=20_2672 on theBenchmark for (2672ds/7896Mi) % 295.11/42.30 % (3896299)Instruction limit reached! % 295.11/42.30 % (3896299)------------------------------ % 295.11/42.30 % (3896299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.11/42.30 % (3896299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.11/42.30 % (3896299)CaDiCaL version: 2.1.3 % 295.11/42.30 % (3896299)Termination reason: Instruction limit % 295.11/42.30 % (3896299)Termination phase: Saturation % 295.11/42.30 % (3896299)Time elapsed: 16.067 s % 295.11/42.30 % (3896299)Peak memory usage: 339 MB % 295.11/42.30 % (3896299)Instructions burned: 30754 (million) % 295.11/42.30 % (3896343)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1368949272:i=5812:gtgl=2:gtg=all_2664 on theBenchmark for (2664ds/5812Mi) % 295.11/42.30 % (3896335)Instruction limit reached! % 295.11/42.30 % (3896335)------------------------------ % 295.11/42.30 % (3896335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.11/42.30 % (3896335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.11/42.30 % (3896335)CaDiCaL version: 2.1.3 % 295.11/42.30 % (3896335)Termination reason: Instruction limit % 295.11/42.30 % (3896335)Termination phase: Saturation % 295.11/42.30 % (3896335)Time elapsed: 4.156 s % 295.11/42.30 % (3896335)Peak memory usage: 184 MB % 295.11/42.30 % (3896335)Instructions burned: 7535 (million) % 295.11/42.30 % (3896345)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=3160478641:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2646 on theBenchmark for (2646ds/2965Mi) % 295.11/42.30 % (3896345)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 295.11/42.30 % (3896345)------------------------------ % 295.11/42.30 % (3896345)Version: Vampire 5.0.1 (ReTerminated %------------------------------------------------------------------------------