%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM199-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n003.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 12:11:54 PM UTC 2026 % Result : Timeout 300.19s 43.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM199-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.14/0.41 % Computer : n003.cluster.edu % 0.14/0.41 % Model : x86_64 x86_64 % 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.41 % Memory : 8046.5625MB % 0.14/0.41 % OS : Linux 6.8.0-71-generic % 0.14/0.41 % CPULimit : 300 % 0.14/0.41 % WCLimit : 300 % 0.14/0.41 % DateTime : Sun Sep 27 19:11:26 UTC 2026 % 0.14/0.41 % CPUTime : % 0.14/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.14/0.47 Running first-order theorem proving % 0.14/0.47 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 % 20.09/3.98 % (866872)Input is clausal, will run a generic CNF schedule. % 20.09/3.98 % (866884)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=2208544909:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 20.09/3.98 % (866886)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1175247506:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 20.09/3.98 % (866887)lrs+10_1_sil=8000:sp=occurrence:random_seed=4267599832:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 20.09/3.98 % (866889)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2507276921:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 20.09/3.98 % (866885)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3790869962:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 20.09/3.98 % (866888)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3041671637:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 20.09/3.98 % (866890)dis-21_1_sil=8000:lcm=predicate:random_seed=157474501:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 20.09/3.98 % (866887)Instruction limit reached! % 20.09/3.98 % (866887)------------------------------ % 20.09/3.98 % (866887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.09/3.98 % (866887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.09/3.98 % (866887)CaDiCaL version: 2.1.3 % 20.09/3.98 % (866887)Termination reason: Instruction limit % 20.09/3.98 % (866887)Termination phase: Saturation % 20.09/3.98 % (866887)Time elapsed: 0.116 s % 20.09/3.98 % (866887)Peak memory usage: 90 MB % 20.09/3.98 % (866887)Instructions burned: 107 (million) % 20.09/3.98 % (866890)Instruction limit reached! % 20.09/3.98 % (866890)------------------------------ % 20.09/3.98 % (866890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.09/3.98 % (866890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.09/3.98 % (866890)CaDiCaL version: 2.1.3 % 20.09/3.98 % (866890)Termination reason: Instruction limit % 20.09/3.98 % (866890)Termination phase: Saturation % 20.09/3.98 % (866890)Time elapsed: 0.089 s % 20.09/3.98 % (866890)Peak memory usage: 89 MB % 20.09/3.98 % (866890)Instructions burned: 117 (million) % 20.09/3.98 % (866888)Instruction limit reached! % 20.09/3.98 % (866888)------------------------------ % 20.09/3.98 % (866888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.09/3.98 % (866888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.09/3.98 % (866888)CaDiCaL version: 2.1.3 % 20.09/3.98 % (866888)Termination reason: Instruction limit % 20.09/3.98 % (866888)Termination phase: Saturation % 20.09/3.98 % (866888)Time elapsed: 0.122 s % 20.09/3.98 % (866888)Peak memory usage: 89 MB % 20.09/3.98 % (866888)Instructions burned: 115 (million) % 20.09/3.98 % (866889)Instruction limit reached! % 20.09/3.98 % (866889)------------------------------ % 20.09/3.98 % (866889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.09/3.98 % (866889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.09/3.98 % (866889)CaDiCaL version: 2.1.3 % 20.09/3.98 % (866889)Termination reason: Instruction limit % 20.09/3.98 % (866889)Termination phase: Saturation % 20.09/3.98 % (866889)Time elapsed: 0.207 s % 20.09/3.98 % (866889)Peak memory usage: 90 MB % 20.09/3.98 % (866889)Instructions burned: 180 (million) % 20.09/3.98 % (866899)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4051597385:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 20.09/3.98 % (866898)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=351186342:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi) % 20.09/3.98 % (866898)Refutation not found, incomplete strategy % 20.09/3.98 % (866898)------------------------------ % 20.09/3.98 % (866898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.09/3.98 % (866898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.09/3.98 % (866898)CaDiCaL version: 2.1.3 % 20.09/3.98 % (866898)Termination reason: Refutation not found, incomplete strategy % 37.80/6.36 % (866898)Time elapsed: 0.008 s % 37.80/6.36 % (866898)Peak memory usage: 88 MB % 37.80/6.36 % (866898)Instructions burned: 5 (million) % 37.80/6.36 % (866900)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3400598224:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi) % 37.80/6.36 % (866900)Refutation not found, incomplete strategy % 37.80/6.36 % (866900)------------------------------ % 37.80/6.36 % (866900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.80/6.36 % (866900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.80/6.36 % (866900)CaDiCaL version: 2.1.3 % 37.80/6.36 % (866900)Termination reason: Refutation not found, incomplete strategy % 37.80/6.36 % (866900)Time elapsed: 0.007 s % 37.80/6.36 % (866900)Peak memory usage: 88 MB % 37.80/6.36 % (866900)Instructions burned: 5 (million) % 37.80/6.36 % (866901)lrs+10_64_to=lpo:sil=8000:random_seed=3059268829:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 37.80/6.36 % (866899)Instruction limit reached! % 37.80/6.36 % (866899)------------------------------ % 37.80/6.36 % (866899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.80/6.36 % (866899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.80/6.36 % (866899)CaDiCaL version: 2.1.3 % 37.80/6.36 % (866899)Termination reason: Instruction limit % 37.80/6.36 % (866899)Termination phase: Saturation % 37.80/6.36 % (866899)Time elapsed: 0.172 s % 37.80/6.36 % (866899)Peak memory usage: 91 MB % 37.80/6.36 % (866899)Instructions burned: 189 (million) % 37.80/6.36 % (866901)Instruction limit reached! % 37.80/6.36 % (866901)------------------------------ % 37.80/6.36 % (866901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.80/6.36 % (866901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.80/6.36 % (866901)CaDiCaL version: 2.1.3 % 37.80/6.36 % (866901)Termination reason: Instruction limit % 37.80/6.36 % (866901)Termination phase: Saturation % 37.80/6.36 % (866901)Time elapsed: 0.134 s % 37.80/6.36 % (866901)Peak memory usage: 90 MB % 37.80/6.36 % (866901)Instructions burned: 126 (million) % 37.80/6.36 % (866908)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2057283073:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi) % 37.80/6.36 % (866898)------------------------------ % 37.80/6.36 % (866898)------------------------------ % 37.80/6.36 % (866908)Instruction limit reached! % 37.80/6.36 % (866908)------------------------------ % 37.80/6.36 % (866908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.80/6.36 % (866908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.80/6.36 % (866908)CaDiCaL version: 2.1.3 % 37.80/6.36 % (866908)Termination reason: Instruction limit % 37.80/6.36 % (866908)Termination phase: Saturation % 37.80/6.36 % (866908)Time elapsed: 0.158 s % 37.80/6.36 % (866908)Peak memory usage: 89 MB % 37.80/6.36 % (866908)Instructions burned: 195 (million) % 37.80/6.36 % (866900)------------------------------ % 37.80/6.36 % (866900)------------------------------ % 37.80/6.36 % (866910)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3697115504:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi) % 37.80/6.36 % (866912)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3152365470:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi) % 37.80/6.36 % (866914)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1310776908:i=107_2988 on theBenchmark for (2988ds/107Mi) % 37.80/6.36 % (866913)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=4023912543:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi) % 37.80/6.36 % (866910)Instruction limit reached! % 37.80/6.36 % (866910)------------------------------ % 37.80/6.36 % (866910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.80/6.36 % (866910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.80/6.36 % (866910)CaDiCaL version: 2.1.3 % 37.80/6.36 % (866910)Termination reason: Instruction limit % 37.80/6.36 % (866910)Termination phase: Saturation % 37.80/6.36 % (866910)Time elapsed: 0.171 s % 37.80/6.36 % (866910)Peak memory usage: 91 MB % 37.80/6.36 % (866910)Instructions burned: 157 (million) % 37.80/6.36 % (866914)Instruction limit reached! % 37.80/6.36 % (866914)------------------------------ % 37.80/6.36 % (866914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.64/11.60 % (866914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.64/11.60 % (866914)CaDiCaL version: 2.1.3 % 74.64/11.60 % (866914)Termination reason: Instruction limit % 74.64/11.60 % (866914)Termination phase: Saturation % 74.64/11.60 % (866914)Time elapsed: 0.084 s % 74.64/11.60 % (866914)Peak memory usage: 90 MB % 74.64/11.60 % (866914)Instructions burned: 108 (million) % 74.64/11.60 % (866913)Instruction limit reached! % 74.64/11.60 % (866913)------------------------------ % 74.64/11.60 % (866913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.64/11.60 % (866913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.64/11.60 % (866913)CaDiCaL version: 2.1.3 % 74.64/11.60 % (866913)Termination reason: Instruction limit % 74.64/11.60 % (866913)Termination phase: Saturation % 74.64/11.60 % (866913)Time elapsed: 0.113 s % 74.64/11.60 % (866913)Peak memory usage: 90 MB % 74.64/11.60 % (866913)Instructions burned: 106 (million) % 74.64/11.60 % (866920)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3307377878:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi) % 74.64/11.60 % (866921)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2702307450:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi) % 74.64/11.60 % (866922)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3321503993:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi) % 74.64/11.60 % (866920)Instruction limit reached! % 74.64/11.60 % (866920)------------------------------ % 74.64/11.60 % (866920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.64/11.60 % (866920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.64/11.60 % (866920)CaDiCaL version: 2.1.3 % 74.64/11.60 % (866920)Termination reason: Instruction limit % 74.64/11.60 % (866920)Termination phase: Saturation % 74.64/11.60 % (866920)Time elapsed: 0.249 s % 74.64/11.60 % (866920)Peak memory usage: 91 MB % 74.64/11.60 % (866920)Instructions burned: 243 (million) % 74.64/11.60 % (866922)Instruction limit reached! % 74.64/11.60 % (866922)------------------------------ % 74.64/11.60 % (866922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.64/11.60 % (866922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.64/11.60 % (866922)CaDiCaL version: 2.1.3 % 74.64/11.60 % (866922)Termination reason: Instruction limit % 74.64/11.60 % (866922)Termination phase: Saturation % 74.64/11.60 % (866922)Time elapsed: 0.157 s % 74.64/11.60 % (866922)Peak memory usage: 90 MB % 74.64/11.60 % (866922)Instructions burned: 134 (million) % 74.64/11.60 % (866927)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3034519357:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi) % 74.64/11.60 % (866928)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2050082616:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi) % 74.64/11.60 % (866928)Instruction limit reached! % 74.64/11.60 % (866928)------------------------------ % 74.64/11.60 % (866928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.64/11.60 % (866928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.64/11.60 % (866928)CaDiCaL version: 2.1.3 % 74.64/11.60 % (866928)Termination reason: Instruction limit % 74.64/11.60 % (866928)Termination phase: Saturation % 74.64/11.60 % (866928)Time elapsed: 0.189 s % 74.64/11.60 % (866928)Peak memory usage: 89 MB % 74.64/11.60 % (866928)Instructions burned: 191 (million) % 74.64/11.60 % (866927)Instruction limit reached! % 74.64/11.60 % (866927)------------------------------ % 74.64/11.60 % (866927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.64/11.60 % (866927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.64/11.60 % (866927)CaDiCaL version: 2.1.3 % 74.64/11.60 % (866927)Termination reason: Instruction limit % 74.64/11.60 % (866927)Termination phase: Saturation % 74.64/11.60 % (866927)Time elapsed: 0.517 s % 74.64/11.60 % (866927)Peak memory usage: 96 MB % 74.64/11.60 % (866927)Instructions burned: 499 (million) % 74.64/11.60 % (866932)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1320235888:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi) % 74.64/11.60 % (866932)Instruction limit reached! % 74.64/11.60 % (866932)------------------------------ % 74.64/11.60 % (866932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.95/14.68 % (866932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.95/14.68 % (866932)CaDiCaL version: 2.1.3 % 95.95/14.68 % (866932)Termination reason: Instruction limit % 95.95/14.68 % (866932)Termination phase: Saturation % 95.95/14.68 % (866932)Time elapsed: 0.279 s % 95.95/14.68 % (866932)Peak memory usage: 92 MB % 95.95/14.68 % (866932)Instructions burned: 264 (million) % 95.95/14.68 % (866934)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3752001091:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi) % 95.95/14.68 % (866934)Instruction limit reached! % 95.95/14.68 % (866934)------------------------------ % 95.95/14.68 % (866934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.95/14.68 % (866934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.95/14.68 % (866934)CaDiCaL version: 2.1.3 % 95.95/14.68 % (866934)Termination reason: Instruction limit % 95.95/14.68 % (866934)Termination phase: Saturation % 95.95/14.68 % (866934)Time elapsed: 0.182 s % 95.95/14.68 % (866934)Peak memory usage: 90 MB % 95.95/14.68 % (866934)Instructions burned: 156 (million) % 95.95/14.68 % (866937)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=837467052:i=3256:kws=precedence:bd=preordered:av=off_2970 on theBenchmark for (2970ds/3256Mi) % 95.95/14.68 % (866938)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2082550422:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi) % 95.95/14.68 % (866938)Instruction limit reached! % 95.95/14.68 % (866938)------------------------------ % 95.95/14.68 % (866938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.95/14.68 % (866938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.95/14.68 % (866938)CaDiCaL version: 2.1.3 % 95.95/14.68 % (866938)Termination reason: Instruction limit % 95.95/14.68 % (866938)Termination phase: Saturation % 95.95/14.68 % (866938)Time elapsed: 0.452 s % 95.95/14.68 % (866938)Peak memory usage: 89 MB % 95.95/14.68 % (866938)Instructions burned: 537 (million) % 95.95/14.68 % (866945)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3524400634:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi) % 95.95/14.68 % (866945)Instruction limit reached! % 95.95/14.68 % (866945)------------------------------ % 95.95/14.68 % (866945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.95/14.68 % (866945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.95/14.68 % (866945)CaDiCaL version: 2.1.3 % 95.95/14.68 % (866945)Termination reason: Instruction limit % 95.95/14.68 % (866945)Termination phase: Saturation % 95.95/14.68 % (866945)Time elapsed: 0.168 s % 95.95/14.68 % (866945)Peak memory usage: 90 MB % 95.95/14.68 % (866945)Instructions burned: 180 (million) % 95.95/14.68 % (866947)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=496831682:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2956 on theBenchmark for (2956ds/10307Mi) % 95.95/14.68 % (866912)Instruction limit reached! % 95.95/14.68 % (866912)------------------------------ % 95.95/14.68 % (866912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.95/14.68 % (866912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.95/14.69 % (866912)CaDiCaL version: 2.1.3 % 95.95/14.69 % (866912)Termination reason: Instruction limit % 95.95/14.69 % (866912)Termination phase: Saturation % 95.95/14.69 % (866912)Time elapsed: 3.410 s % 95.95/14.69 % (866912)Peak memory usage: 144 MB % 95.95/14.69 % (866912)Instructions burned: 3394 (million) % 95.95/14.69 % (866952)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3691643965:i=412:gtgl=4:gtg=exists_all_2952 on theBenchmark for (2952ds/412Mi) % 95.95/14.69 % (866952)Instruction limit reached! % 95.95/14.69 % (866952)------------------------------ % 95.95/14.69 % (866952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.95/14.69 % (866952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.95/14.69 % (866952)CaDiCaL version: 2.1.3 % 95.95/14.69 % (866952)Termination reason: Instruction limit % 95.95/14.69 % (866952)Termination phase: Saturation % 95.95/14.69 % (866952)Time elapsed: 0.320 s % 95.95/14.69 % (866952)Peak memory usage: 90 MB % 131.85/19.62 % (866952)Instructions burned: 413 (million) % 131.85/19.62 % (866955)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3929254062:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi) % 131.85/19.62 % (866937)Instruction limit reached! % 131.85/19.62 % (866937)------------------------------ % 131.85/19.62 % (866937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.85/19.62 % (866937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.62 % (866937)CaDiCaL version: 2.1.3 % 131.85/19.62 % (866937)Termination reason: Instruction limit % 131.85/19.62 % (866937)Termination phase: Saturation % 131.85/19.62 % (866937)Time elapsed: 3.230 s % 131.85/19.62 % (866937)Peak memory usage: 149 MB % 131.85/19.62 % (866937)Instructions burned: 3257 (million) % 131.85/19.62 % (866961)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2699884373:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2935 on theBenchmark for (2935ds/303Mi) % 131.85/19.62 % (866961)Instruction limit reached! % 131.85/19.62 % (866961)------------------------------ % 131.85/19.62 % (866961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.85/19.62 % (866961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.62 % (866961)CaDiCaL version: 2.1.3 % 131.85/19.62 % (866961)Termination reason: Instruction limit % 131.85/19.62 % (866961)Termination phase: Saturation % 131.85/19.62 % (866961)Time elapsed: 0.198 s % 131.85/19.62 % (866961)Peak memory usage: 88 MB % 131.85/19.62 % (866961)Instructions burned: 304 (million) % 131.85/19.62 % (866921)Instruction limit reached! % 131.85/19.62 % (866921)------------------------------ % 131.85/19.62 % (866921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.85/19.62 % (866921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.62 % (866921)CaDiCaL version: 2.1.3 % 131.85/19.62 % (866921)Termination reason: Instruction limit % 131.85/19.62 % (866921)Termination phase: Saturation % 131.85/19.62 % (866921)Time elapsed: 5.513 s % 131.85/19.62 % (866921)Peak memory usage: 159 MB % 131.85/19.62 % (866921)Instructions burned: 5208 (million) % 131.85/19.62 % (866963)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2288023470:st=4:i=720:sd=3:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/720Mi) % 131.85/19.62 % (866964)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2795847223:i=598:bs=on:bd=preordered:av=off:ss=axioms_2928 on theBenchmark for (2928ds/598Mi) % 131.85/19.62 % (866963)Instruction limit reached! % 131.85/19.62 % (866963)------------------------------ % 131.85/19.62 % (866963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.85/19.62 % (866963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.62 % (866963)CaDiCaL version: 2.1.3 % 131.85/19.62 % (866963)Termination reason: Instruction limit % 131.85/19.62 % (866963)Termination phase: Saturation % 131.85/19.62 % (866963)Time elapsed: 0.700 s % 131.85/19.62 % (866963)Peak memory usage: 98 MB % 131.85/19.62 % (866963)Instructions burned: 721 (million) % 131.85/19.62 % (866964)Instruction limit reached! % 131.85/19.62 % (866964)------------------------------ % 131.85/19.62 % (866964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.85/19.62 % (866964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.62 % (866964)CaDiCaL version: 2.1.3 % 131.85/19.62 % (866964)Termination reason: Instruction limit % 131.85/19.62 % (866964)Termination phase: Saturation % 131.85/19.62 % (866964)Time elapsed: 0.597 s % 131.85/19.62 % (866964)Peak memory usage: 94 MB % 131.85/19.62 % (866964)Instructions burned: 598 (million) % 131.85/19.62 % (866967)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=932618355:i=2989:sd=3:ss=axioms:sgt=60_2919 on theBenchmark for (2919ds/2989Mi) % 131.85/19.62 % (866968)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3634606345:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2919 on theBenchmark for (2919ds/1997Mi) % 131.85/19.62 % (866968)Instruction limit reached! % 131.85/19.62 % (866968)------------------------------ % 131.85/19.62 % (866968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.85/19.62 % (866968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.92/27.03 % (866968)CaDiCaL version: 2.1.3 % 183.92/27.03 % (866968)Termination reason: Instruction limit % 183.92/27.03 % (866968)Termination phase: Saturation % 183.92/27.03 % (866968)Time elapsed: 2.182 s % 183.92/27.03 % (866968)Peak memory usage: 138 MB % 183.92/27.03 % (866968)Instructions burned: 1997 (million) % 183.92/27.03 % (866977)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1106164186:i=2088:bd=preordered:av=off_2894 on theBenchmark for (2894ds/2088Mi) % 183.92/27.03 % (866967)Instruction limit reached! % 183.92/27.03 % (866967)------------------------------ % 183.92/27.03 % (866967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.92/27.03 % (866967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.92/27.03 % (866967)CaDiCaL version: 2.1.3 % 183.92/27.03 % (866967)Termination reason: Instruction limit % 183.92/27.03 % (866967)Termination phase: Saturation % 183.92/27.03 % (866967)Time elapsed: 3.033 s % 183.92/27.03 % (866967)Peak memory usage: 146 MB % 183.92/27.03 % (866967)Instructions burned: 2989 (million) % 183.92/27.03 % (866982)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1298638144:i=1098:nicw=on_2887 on theBenchmark for (2887ds/1098Mi) % 183.92/27.03 % (866982)Instruction limit reached! % 183.92/27.03 % (866982)------------------------------ % 183.92/27.03 % (866982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.92/27.03 % (866982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.92/27.03 % (866982)CaDiCaL version: 2.1.3 % 183.92/27.03 % (866982)Termination reason: Instruction limit % 183.92/27.03 % (866982)Termination phase: Saturation % 183.92/27.03 % (866982)Time elapsed: 1.101 s % 183.92/27.03 % (866982)Peak memory usage: 103 MB % 183.92/27.03 % (866982)Instructions burned: 1098 (million) % 183.92/27.03 % (866955)Instruction limit reached! % 183.92/27.03 % (866955)------------------------------ % 183.92/27.03 % (866955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.92/27.03 % (866955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.92/27.03 % (866955)CaDiCaL version: 2.1.3 % 183.92/27.03 % (866955)Termination reason: Instruction limit % 183.92/27.03 % (866955)Termination phase: Saturation % 183.92/27.03 % (866955)Time elapsed: 7.058 s % 183.92/27.03 % (866955)Peak memory usage: 176 MB % 183.92/27.03 % (866955)Instructions burned: 8479 (million) % 183.92/27.03 % (866987)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1757974713:i=433:bd=preordered_2873 on theBenchmark for (2873ds/433Mi) % 183.92/27.03 % (866977)Instruction limit reached! % 183.92/27.03 % (866977)------------------------------ % 183.92/27.03 % (866977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.92/27.03 % (866977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.92/27.03 % (866977)CaDiCaL version: 2.1.3 % 183.92/27.03 % (866977)Termination reason: Instruction limit % 183.92/27.03 % (866977)Termination phase: Saturation % 183.92/27.03 % (866977)Time elapsed: 2.088 s % 183.92/27.03 % (866977)Peak memory usage: 136 MB % 183.92/27.03 % (866977)Instructions burned: 2088 (million) % 183.92/27.03 % (866988)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2775135566:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2872 on theBenchmark for (2872ds/2942Mi) % 183.92/27.03 % (866990)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2972119412:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2870 on theBenchmark for (2870ds/6922Mi) % 183.92/27.03 % (866987)Instruction limit reached! % 183.92/27.03 % (866987)------------------------------ % 183.92/27.03 % (866987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.92/27.03 % (866987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.92/27.03 % (866987)CaDiCaL version: 2.1.3 % 183.92/27.03 % (866987)Termination reason: Instruction limit % 183.92/27.03 % (866987)Termination phase: Saturation % 183.92/27.03 % (866987)Time elapsed: 0.432 s % 183.92/27.03 % (866987)Peak memory usage: 93 MB % 183.92/27.03 % (866987)Instructions burned: 434 (million) % 183.92/27.03 % (866993)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1146553894:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2866 on theBenchmark for (2866ds/596Mi) % 203.75/29.87 % (866993)Instruction limit reached! % 203.75/29.87 % (866993)------------------------------ % 203.75/29.87 % (866993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.75/29.87 % (866993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.75/29.87 % (866993)CaDiCaL version: 2.1.3 % 203.75/29.87 % (866993)Termination reason: Instruction limit % 203.75/29.87 % (866993)Termination phase: Saturation % 203.75/29.87 % (866993)Time elapsed: 0.527 s % 203.75/29.87 % (866993)Peak memory usage: 99 MB % 203.75/29.87 % (866993)Instructions burned: 597 (million) % 203.75/29.87 % (866997)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=301279390:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2858 on theBenchmark for (2858ds/4123Mi) % 203.75/29.87 % (866947)Instruction limit reached! % 203.75/29.87 % (866947)------------------------------ % 203.75/29.87 % (866947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.75/29.87 % (866947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.75/29.87 % (866947)CaDiCaL version: 2.1.3 % 203.75/29.87 % (866947)Termination reason: Instruction limit % 203.75/29.87 % (866947)Termination phase: Saturation % 203.75/29.87 % (866947)Time elapsed: 11.286 s % 203.75/29.87 % (866947)Peak memory usage: 164 MB % 203.75/29.87 % (866947)Instructions burned: 10307 (million) % 203.75/29.87 % (866988)Instruction limit reached! % 203.75/29.87 % (866988)------------------------------ % 203.75/29.87 % (866988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.75/29.87 % (866988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.75/29.87 % (866988)CaDiCaL version: 2.1.3 % 203.75/29.87 % (866988)Termination reason: Instruction limit % 203.75/29.87 % (866988)Termination phase: Saturation % 203.75/29.87 % (866988)Time elapsed: 3.205 s % 203.75/29.87 % (866988)Peak memory usage: 146 MB % 203.75/29.87 % (866988)Instructions burned: 2942 (million) % 203.75/29.87 % (867003)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1760917692:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2840 on theBenchmark for (2840ds/16411Mi) % 203.75/29.87 % (867005)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3138168153:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2837 on theBenchmark for (2837ds/1670Mi) % 203.75/29.87 % (866990)Instruction limit reached! % 203.75/29.87 % (866990)------------------------------ % 203.75/29.87 % (866990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.75/29.87 % (866990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.75/29.87 % (866990)CaDiCaL version: 2.1.3 % 203.75/29.87 % (866990)Termination reason: Instruction limit % 203.75/29.87 % (866990)Termination phase: Saturation % 203.75/29.87 % (866990)Time elapsed: 4.316 s % 203.75/29.87 % (866990)Peak memory usage: 188 MB % 203.75/29.87 % (866990)Instructions burned: 6925 (million) % 203.75/29.87 % (867012)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2397519355:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2824 on theBenchmark for (2824ds/1722Mi) % 203.75/29.87 % (867005)Instruction limit reached! % 203.75/29.87 % (867005)------------------------------ % 203.75/29.87 % (867005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.75/29.87 % (867005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.75/29.87 % (867005)CaDiCaL version: 2.1.3 % 203.75/29.87 % (867005)Termination reason: Instruction limit % 203.75/29.87 % (867005)Termination phase: Saturation % 203.75/29.87 % (867005)Time elapsed: 1.718 s % 203.75/29.87 % (867005)Peak memory usage: 137 MB % 203.75/29.87 % (867005)Instructions burned: 1670 (million) % 203.75/29.87 % (867015)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3559165890:cts=off:cond=on:i=9530:bs=on:fsd=on_2817 on theBenchmark for (2817ds/9530Mi) % 203.75/29.87 % (866997)Instruction limit reached! % 203.75/29.87 % (866997)------------------------------ % 203.75/29.87 % (866997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.75/29.87 % (866997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.75/29.87 % (866997)CaDiCaL version: 2.1.3 % 227.71/33.15 % (866997)Termination reason: Instruction limit % 227.71/33.15 % (866997)Termination phase: Saturation % 227.71/33.15 % (866997)Time elapsed: 4.102 s % 227.71/33.15 % (866997)Peak memory usage: 157 MB % 227.71/33.15 % (866997)Instructions burned: 4123 (million) % 227.71/33.15 % (867012)Instruction limit reached! % 227.71/33.15 % (867012)------------------------------ % 227.71/33.15 % (867012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.71/33.15 % (867012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/33.15 % (867012)CaDiCaL version: 2.1.3 % 227.71/33.15 % (867012)Termination reason: Instruction limit % 227.71/33.15 % (867012)Termination phase: Saturation % 227.71/33.15 % (867012)Time elapsed: 1.022 s % 227.71/33.15 % (867012)Peak memory usage: 133 MB % 227.71/33.15 % (867012)Instructions burned: 1724 (million) % 227.71/33.15 % (867017)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4092203211:st=2:i=4495:sd=10:ss=included_2813 on theBenchmark for (2813ds/4495Mi) % 227.71/33.15 % (867018)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1699454326:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2812 on theBenchmark for (2812ds/4920Mi) % 227.71/33.15 % (867018)Instruction limit reached! % 227.71/33.15 % (867018)------------------------------ % 227.71/33.15 % (867018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.71/33.15 % (867018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/33.15 % (867018)CaDiCaL version: 2.1.3 % 227.71/33.15 % (867018)Termination reason: Instruction limit % 227.71/33.15 % (867018)Termination phase: Saturation % 227.71/33.15 % (867018)Time elapsed: 4.474 s % 227.71/33.15 % (867018)Peak memory usage: 154 MB % 227.71/33.15 % (867018)Instructions burned: 4921 (million) % 227.71/33.15 % (867015)Instruction limit reached! % 227.71/33.15 % (867015)------------------------------ % 227.71/33.15 % (867015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.71/33.15 % (867015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/33.15 % (867015)CaDiCaL version: 2.1.3 % 227.71/33.15 % (867015)Termination reason: Instruction limit % 227.71/33.15 % (867015)Termination phase: Saturation % 227.71/33.15 % (867015)Time elapsed: 4.934 s % 227.71/33.15 % (867015)Peak memory usage: 153 MB % 227.71/33.15 % (867015)Instructions burned: 9531 (million) % 227.71/33.15 % (867017)Instruction limit reached! % 227.71/33.15 % (867017)------------------------------ % 227.71/33.15 % (867017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.71/33.15 % (867017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/33.15 % (867017)CaDiCaL version: 2.1.3 % 227.71/33.15 % (867017)Termination reason: Instruction limit % 227.71/33.15 % (867017)Termination phase: Saturation % 227.71/33.15 % (867017)Time elapsed: 4.681 s % 227.71/33.15 % (867017)Peak memory usage: 159 MB % 227.71/33.15 % (867017)Instructions burned: 4496 (million) % 227.71/33.15 % (867028)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1725229463:i=4629:av=off:gsp=on_2764 on theBenchmark for (2764ds/4629Mi) % 227.71/33.15 % (867027)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1576589778:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2765 on theBenchmark for (2765ds/2083Mi) % 227.71/33.15 % (867029)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=99047606:i=1258:av=off_2764 on theBenchmark for (2764ds/1258Mi) % 227.71/33.15 % (867029)Instruction limit reached! % 227.71/33.15 % (867029)------------------------------ % 227.71/33.15 % (867029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.71/33.15 % (867029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/33.15 % (867029)CaDiCaL version: 2.1.3 % 227.71/33.15 % (867029)Termination reason: Instruction limit % 227.71/33.15 % (867029)Termination phase: Saturation % 227.71/33.15 % (867029)Time elapsed: 1.095 s % 227.71/33.15 % (867029)Peak memory usage: 95 MB % 227.71/33.15 % (867029)Instructions burned: 1258 (million) % 227.71/33.15 % (867035)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4016646392:i=7343:av=off:ss=included_2751 on theBenchmark for (2751ds/7343Mi) % 227.71/33.15 % (867027)Instruction limit reached! % 227.71/33.15 % (867027)------------------------------ % 227.71/33.15 % (867027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.53/36.17 % (867027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.53/36.17 % (867027)CaDiCaL version: 2.1.3 % 248.53/36.17 % (867027)Termination reason: Instruction limit % 248.53/36.17 % (867027)Termination phase: Saturation % 248.53/36.17 % (867027)Time elapsed: 2.259 s % 248.53/36.17 % (867027)Peak memory usage: 137 MB % 248.53/36.17 % (867027)Instructions burned: 2083 (million) % 248.53/36.17 % (867028)Instruction limit reached! % 248.53/36.17 % (867028)------------------------------ % 248.53/36.17 % (867028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.53/36.17 % (867028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.53/36.17 % (867028)CaDiCaL version: 2.1.3 % 248.53/36.17 % (867028)Termination reason: Instruction limit % 248.53/36.17 % (867028)Termination phase: Saturation % 248.53/36.17 % (867028)Time elapsed: 2.340 s % 248.53/36.17 % (867028)Peak memory usage: 144 MB % 248.53/36.17 % (867028)Instructions burned: 4629 (million) % 248.53/36.17 % (867039)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1873637973:i=1325:sd=2:ss=axioms:sgt=16_2739 on theBenchmark for (2739ds/1325Mi) % 248.53/36.17 % (867039)Refutation not found, incomplete strategy % 248.53/36.17 % (867039)------------------------------ % 248.53/36.17 % (867039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.53/36.17 % (867039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.53/36.17 % (867039)CaDiCaL version: 2.1.3 % 248.53/36.17 % (867039)Termination reason: Refutation not found, incomplete strategy % 248.53/36.17 % (867039)Time elapsed: 0.010 s % 248.53/36.17 % (867039)Peak memory usage: 88 MB % 248.53/36.17 % (867039)Instructions burned: 9 (million) % 248.53/36.17 % (867040)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2456610320:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2739 on theBenchmark for (2739ds/2646Mi) % 248.53/36.17 % (867039)------------------------------ % 248.53/36.17 % (867039)------------------------------ % 248.53/36.17 % (867043)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=823034311:i=1489:sd=2:ep=R:ss=axioms_2733 on theBenchmark for (2733ds/1489Mi) % 248.53/36.17 % (867043)Instruction limit reached! % 248.53/36.17 % (867043)------------------------------ % 248.53/36.17 % (867043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.53/36.17 % (867043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.53/36.17 % (867043)CaDiCaL version: 2.1.3 % 248.53/36.17 % (867043)Termination reason: Instruction limit % 248.53/36.17 % (867043)Termination phase: Saturation % 248.53/36.17 % (867043)Time elapsed: 1.212 s % 248.53/36.17 % (867043)Peak memory usage: 135 MB % 248.53/36.17 % (867043)Instructions burned: 1490 (million) % 248.53/36.17 % (867069)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3309930307:i=1503_2717 on theBenchmark for (2717ds/1503Mi) % 248.53/36.17 % (867040)Instruction limit reached! % 248.53/36.17 % (867040)------------------------------ % 248.53/36.17 % (867040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.53/36.17 % (867040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.53/36.17 % (867040)CaDiCaL version: 2.1.3 % 248.53/36.17 % (867040)Termination reason: Instruction limit % 248.53/36.17 % (867040)Termination phase: Saturation % 248.53/36.17 % (867040)Time elapsed: 2.223 s % 248.53/36.17 % (867040)Peak memory usage: 138 MB % 248.53/36.17 % (867040)Instructions burned: 2646 (million) % 248.53/36.17 % (867035)Instruction limit reached! % 248.53/36.17 % (867035)------------------------------ % 248.53/36.17 % (867035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.53/36.17 % (867035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.53/36.17 % (867035)CaDiCaL version: 2.1.3 % 248.53/36.17 % (867035)Termination reason: Instruction limit % 248.53/36.17 % (867035)Termination phase: Saturation % 248.53/36.17 % (867035)Time elapsed: 3.503 s % 248.53/36.17 % (867035)Peak memory usage: 192 MB % 248.53/36.17 % (867035)Instructions burned: 7346 (million) % 248.53/36.17 % (867124)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=900443188:i=13942:kws=frequency_2714 on theBenchmark for (2714ds/13942Mi) % 248.53/36.17 % (867125)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3547263269:i=3604:fsr=off:er=filter_2712 on theBenchmark for (2712ds/3604Mi) % 273.37/39.76 % (867069)Instruction limit reached! % 273.37/39.76 % (867069)------------------------------ % 273.37/39.76 % (867069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.37/39.76 % (867069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.37/39.76 % (867069)CaDiCaL version: 2.1.3 % 273.37/39.76 % (867069)Termination reason: Instruction limit % 273.37/39.76 % (867069)Termination phase: Saturation % 273.37/39.76 % (867069)Time elapsed: 0.920 s % 273.37/39.76 % (867069)Peak memory usage: 135 MB % 273.37/39.76 % (867069)Instructions burned: 1504 (million) % 273.37/39.76 % (867159)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2982718339:i=1876:sd=1:ss=included:sgt=32_2706 on theBenchmark for (2706ds/1876Mi) % 273.37/39.76 % (867125)Instruction limit reached! % 273.37/39.76 % (867125)------------------------------ % 273.37/39.76 % (867125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.37/39.76 % (867125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.37/39.76 % (867125)CaDiCaL version: 2.1.3 % 273.37/39.76 % (867125)Termination reason: Instruction limit % 273.37/39.76 % (867125)Termination phase: Saturation % 273.37/39.76 % (867125)Time elapsed: 1.225 s % 273.37/39.76 % (867125)Peak memory usage: 154 MB % 273.37/39.76 % (867125)Instructions burned: 3606 (million) % 273.37/39.76 % (867208)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1710517859:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2699 on theBenchmark for (2699ds/1932Mi) % 273.37/39.76 % (867003)Instruction limit reached! % 273.37/39.76 % (867003)------------------------------ % 273.37/39.76 % (867003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.37/39.76 % (867003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.37/39.76 % (867003)CaDiCaL version: 2.1.3 % 273.37/39.76 % (867003)Termination reason: Instruction limit % 273.37/39.76 % (867003)Termination phase: Saturation % 273.37/39.76 % (867003)Time elapsed: 14.423 s % 273.37/39.76 % (867003)Peak memory usage: 238 MB % 273.37/39.76 % (867003)Instructions burned: 16412 (million) % 273.37/39.76 % (867208)Instruction limit reached! % 273.37/39.76 % (867208)------------------------------ % 273.37/39.76 % (867208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.37/39.76 % (867208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.37/39.76 % (867208)CaDiCaL version: 2.1.3 % 273.37/39.76 % (867208)Termination reason: Instruction limit % 273.37/39.76 % (867208)Termination phase: Saturation % 273.37/39.76 % (867208)Time elapsed: 0.608 s % 273.37/39.76 % (867208)Peak memory usage: 139 MB % 273.37/39.76 % (867208)Instructions burned: 1935 (million) % 273.37/39.76 % (867210)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=3238804826:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2692 on theBenchmark for (2692ds/1980Mi) % 273.37/39.76 % (867211)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=2963209312:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2691 on theBenchmark for (2691ds/3902Mi) % 273.37/39.76 % (867159)Instruction limit reached! % 273.37/39.76 % (867159)------------------------------ % 273.37/39.76 % (867159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.37/39.76 % (867159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.37/39.76 % (867159)CaDiCaL version: 2.1.3 % 273.37/39.76 % (867159)Termination reason: Instruction limit % 273.37/39.76 % (867159)Termination phase: Saturation % 273.37/39.76 % (867159)Time elapsed: 1.566 s % 273.37/39.76 % (867159)Peak memory usage: 130 MB % 273.37/39.76 % (867159)Instructions burned: 1876 (million) % 273.37/39.76 % (867214)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2920187272:avsq=on:i=3916:aac=none:amm=off_2689 on theBenchmark for (2689ds/3916Mi) % 273.37/39.76 % (867211)Instruction limit reached! % 273.37/39.76 % (867211)------------------------------ % 273.37/39.76 % (867211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.37/39.76 % (867211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3cTerminated %------------------------------------------------------------------------------