%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC443_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n004.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:03:57 PM UTC 2026 % Result : Timeout 287.76s 41.27s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC443_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n004.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 09:38:07 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.46/1.46 % (236284)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.46/1.46 % (236331)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2462840250:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.46/1.46 % (236331)Instruction limit reached! % 4.46/1.46 % (236331)------------------------------ % 4.46/1.46 % (236331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.46/1.46 % (236331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.46/1.46 % (236331)CaDiCaL version: 2.1.3 % 4.46/1.46 % (236331)Termination reason: Instruction limit % 4.46/1.46 % (236331)Termination phase: Saturation % 4.46/1.46 % (236331)Time elapsed: 0.005 s % 4.46/1.46 % (236331)Peak memory usage: 88 MB % 4.46/1.46 % (236331)Instructions burned: 9 (million) % 4.46/1.46 % (236330)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2249268316:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.46/1.46 % (236329)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=35677626:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.46/1.46 % (236328)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=495249230:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.46/1.46 % (236334)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2408215010:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.46/1.46 % (236332)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=91795174:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.46/1.46 % (236333)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=42618101:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.46/1.46 % (236332)Instruction limit reached! % 4.46/1.46 % (236332)------------------------------ % 4.46/1.46 % (236332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.46/1.46 % (236332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.46/1.46 % (236332)CaDiCaL version: 2.1.3 % 4.46/1.46 % (236332)Termination reason: Instruction limit % 4.46/1.46 % (236332)Termination phase: Saturation % 4.46/1.46 % (236332)Time elapsed: 0.005 s % 4.46/1.46 % (236332)Peak memory usage: 89 MB % 4.46/1.46 % (236332)Instructions burned: 5 (million) % 4.46/1.46 % (236328)Instruction limit reached! % 4.46/1.46 % (236328)------------------------------ % 4.46/1.46 % (236328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.46/1.46 % (236328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.46/1.46 % (236328)CaDiCaL version: 2.1.3 % 4.46/1.46 % (236328)Termination reason: Instruction limit % 4.46/1.46 % (236328)Termination phase: Saturation % 4.46/1.46 % (236328)Time elapsed: 0.037 s % 4.46/1.46 % (236328)Peak memory usage: 115 MB % 4.46/1.46 % (236328)Instructions burned: 12 (million) % 4.46/1.46 % (236329)Refutation not found, incomplete strategy % 4.46/1.46 % (236329)------------------------------ % 4.46/1.46 % (236329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.46/1.46 % (236329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.46/1.46 % (236329)CaDiCaL version: 2.1.3 % 4.46/1.46 % (236329)Termination reason: Refutation not found, incomplete strategy % 4.46/1.46 % (236329)Time elapsed: 0.046 s % 4.46/1.46 % (236329)Peak memory usage: 116 MB % 4.46/1.46 % (236329)Instructions burned: 16 (million) % 4.46/1.46 % (236334)Instruction limit reached! % 4.46/1.46 % (236334)------------------------------ % 4.46/1.46 % (236334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.46/1.46 % (236334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.46/1.46 % (236334)CaDiCaL version: 2.1.3 % 4.46/1.46 % (236334)Termination reason: Instruction limit % 4.46/1.46 % (236334)Termination phase: Saturation % 4.46/1.46 % (236334)Time elapsed: 0.057 s % 4.46/1.46 % (236334)Peak memory usage: 116 MB % 4.46/1.46 % (236334)Instructions burned: 33 (million) % 4.46/1.46 % (236333)Instruction limit reached! % 4.46/1.46 % (236333)------------------------------ % 4.46/1.46 % (236333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.46/1.46 % (236333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.46/1.46 % (236333)CaDiCaL version: 2.1.3 % 4.46/1.46 % (236333)Termination reason: Instruction limit % 6.13/1.65 % (236333)Termination phase: Saturation % 6.13/1.65 % (236333)Time elapsed: 0.073 s % 6.13/1.65 % (236333)Peak memory usage: 115 MB % 6.13/1.65 % (236333)Instructions burned: 46 (million) % 6.13/1.65 % (236341)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1844501911:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 6.13/1.65 % (236341)Instruction limit reached! % 6.13/1.65 % (236341)------------------------------ % 6.13/1.65 % (236341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.13/1.65 % (236341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.13/1.65 % (236341)CaDiCaL version: 2.1.3 % 6.13/1.65 % (236341)Termination reason: Instruction limit % 6.13/1.65 % (236341)Termination phase: Saturation % 6.13/1.65 % (236341)Time elapsed: 0.006 s % 6.13/1.65 % (236341)Peak memory usage: 88 MB % 6.13/1.65 % (236341)Instructions burned: 15 (million) % 6.13/1.65 % (236330)Instruction limit reached! % 6.13/1.65 % (236330)------------------------------ % 6.13/1.65 % (236330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.13/1.65 % (236330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.13/1.65 % (236330)CaDiCaL version: 2.1.3 % 6.13/1.65 % (236330)Termination reason: Instruction limit % 6.13/1.65 % (236330)Termination phase: Saturation % 6.13/1.65 % (236330)Time elapsed: 0.194 s % 6.13/1.65 % (236330)Peak memory usage: 117 MB % 6.13/1.65 % (236330)Instructions burned: 201 (million) % 6.13/1.65 % (236352)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1397195812:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 6.13/1.65 % (236352)Instruction limit reached! % 6.13/1.65 % (236352)------------------------------ % 6.13/1.65 % (236352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.13/1.65 % (236352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.13/1.65 % (236352)CaDiCaL version: 2.1.3 % 6.13/1.65 % (236352)Termination reason: Instruction limit % 6.13/1.65 % (236352)Termination phase: Saturation % 6.13/1.65 % (236352)Time elapsed: 0.006 s % 6.13/1.65 % (236352)Peak memory usage: 90 MB % 6.13/1.65 % (236352)Instructions burned: 19 (million) % 6.13/1.65 % (236350)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2292686079:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.13/1.65 % (236350)Instruction limit reached! % 6.13/1.65 % (236350)------------------------------ % 6.13/1.65 % (236350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.13/1.65 % (236350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.13/1.65 % (236350)CaDiCaL version: 2.1.3 % 6.13/1.65 % (236350)Termination reason: Instruction limit % 6.13/1.65 % (236350)Termination phase: Saturation % 6.13/1.65 % (236350)Time elapsed: 0.029 s % 6.13/1.65 % (236350)Peak memory usage: 89 MB % 6.13/1.65 % (236350)Instructions burned: 30 (million) % 6.13/1.65 % (236355)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2066666716:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 6.13/1.65 % (236357)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=1746201523:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 6.13/1.65 % (236361)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=666453157:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.13/1.65 % (236355)Instruction limit reached! % 6.13/1.65 % (236355)------------------------------ % 6.13/1.65 % (236355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.13/1.65 % (236355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.13/1.65 % (236355)CaDiCaL version: 2.1.3 % 6.13/1.65 % (236355)Termination reason: Instruction limit % 6.13/1.65 % (236355)Termination phase: Saturation % 6.13/1.65 % (236355)Time elapsed: 0.024 s % 6.13/1.65 % (236355)Peak memory usage: 89 MB % 6.13/1.65 % (236355)Instructions burned: 24 (million) % 6.13/1.65 % (236369)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1298172076:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 6.13/1.65 % (236357)Instruction limit reached! % 6.13/1.65 % (236357)------------------------------ % 7.30/1.89 % (236357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.30/1.89 % (236357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.89 % (236357)CaDiCaL version: 2.1.3 % 7.30/1.89 % (236357)Termination reason: Instruction limit % 7.30/1.89 % (236357)Termination phase: Saturation % 7.30/1.89 % (236357)Time elapsed: 0.023 s % 7.30/1.89 % (236357)Peak memory usage: 89 MB % 7.30/1.89 % (236357)Instructions burned: 27 (million) % 7.30/1.89 % (236369)Refutation not found, incomplete strategy % 7.30/1.89 % (236369)------------------------------ % 7.30/1.89 % (236369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.30/1.89 % (236369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.89 % (236369)CaDiCaL version: 2.1.3 % 7.30/1.89 % (236369)Termination reason: Refutation not found, incomplete strategy % 7.30/1.89 % (236369)Time elapsed: 0.044 s % 7.30/1.89 % (236369)Peak memory usage: 90 MB % 7.30/1.89 % (236369)Instructions burned: 86 (million) % 7.30/1.89 % (236368)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=861732275:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 7.30/1.89 % (236368)Instruction limit reached! % 7.30/1.89 % (236368)------------------------------ % 7.30/1.89 % (236368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.30/1.89 % (236368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.89 % (236368)CaDiCaL version: 2.1.3 % 7.30/1.89 % (236368)Termination reason: Instruction limit % 7.30/1.89 % (236368)Termination phase: Saturation % 7.30/1.89 % (236368)Time elapsed: 0.003 s % 7.30/1.89 % (236368)Peak memory usage: 88 MB % 7.30/1.89 % (236368)Instructions burned: 2 (million) % 7.30/1.89 % (236361)Instruction limit reached! % 7.30/1.89 % (236361)------------------------------ % 7.30/1.89 % (236361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.30/1.89 % (236361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.89 % (236361)CaDiCaL version: 2.1.3 % 7.30/1.89 % (236361)Termination reason: Instruction limit % 7.30/1.89 % (236361)Termination phase: Saturation % 7.30/1.89 % (236361)Time elapsed: 0.084 s % 7.30/1.89 % (236361)Peak memory usage: 89 MB % 7.30/1.89 % (236361)Instructions burned: 85 (million) % 7.30/1.89 % (236329)------------------------------ % 7.30/1.89 % (236329)------------------------------ % 7.30/1.89 % (236371)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=640269218:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 7.30/1.89 % (236371)Instruction limit reached! % 7.30/1.89 % (236371)------------------------------ % 7.30/1.89 % (236371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.30/1.89 % (236371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.89 % (236371)CaDiCaL version: 2.1.3 % 7.30/1.89 % (236371)Termination reason: Instruction limit % 7.30/1.89 % (236371)Termination phase: Saturation % 7.30/1.89 % (236371)Time elapsed: 0.004 s % 7.30/1.89 % (236371)Peak memory usage: 89 MB % 7.30/1.89 % (236371)Instructions burned: 5 (million) % 7.30/1.89 % (236377)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1750098791:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 7.30/1.89 % (236381)lrs+10_1_thi=all:si=on:fd=off:random_seed=1320733378:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 7.30/1.89 % (236388)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2812536049:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 7.30/1.89 % (236388)Instruction limit reached! % 7.30/1.89 % (236388)------------------------------ % 7.30/1.89 % (236388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.30/1.89 % (236388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.89 % (236388)CaDiCaL version: 2.1.3 % 7.30/1.89 % (236388)Termination reason: Instruction limit % 7.30/1.89 % (236388)Termination phase: Saturation % 7.30/1.89 % (236388)Time elapsed: 0.009 s % 7.30/1.89 % (236388)Peak memory usage: 88 MB % 7.30/1.89 % (236388)Instructions burned: 8 (million) % 7.30/1.89 % (236369)------------------------------ % 7.30/1.89 % (236369)------------------------------ % 7.30/1.89 % (236389)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2650644918:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 11.07/2.22 % (236389)Instruction limit reached! % 11.07/2.22 % (236389)------------------------------ % 11.07/2.22 % (236389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236389)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236389)Termination reason: Instruction limit % 11.07/2.22 % (236389)Termination phase: Saturation % 11.07/2.22 % (236389)Time elapsed: 0.003 s % 11.07/2.22 % (236389)Peak memory usage: 88 MB % 11.07/2.22 % (236389)Instructions burned: 2 (million) % 11.07/2.22 % (236392)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2612788938:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi) % 11.07/2.22 % (236392)Instruction limit reached! % 11.07/2.22 % (236392)------------------------------ % 11.07/2.22 % (236392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236392)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236392)Termination reason: Instruction limit % 11.07/2.22 % (236392)Termination phase: Saturation % 11.07/2.22 % (236392)Time elapsed: 0.003 s % 11.07/2.22 % (236392)Peak memory usage: 88 MB % 11.07/2.22 % (236392)Instructions burned: 2 (million) % 11.07/2.22 % (236393)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=195838213:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi) % 11.07/2.22 % (236381)Instruction limit reached! % 11.07/2.22 % (236381)------------------------------ % 11.07/2.22 % (236381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236381)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236381)Termination reason: Instruction limit % 11.07/2.22 % (236381)Termination phase: Saturation % 11.07/2.22 % (236381)Time elapsed: 0.091 s % 11.07/2.22 % (236381)Peak memory usage: 116 MB % 11.07/2.22 % (236381)Instructions burned: 53 (million) % 11.07/2.22 % (236377)Instruction limit reached! % 11.07/2.22 % (236377)------------------------------ % 11.07/2.22 % (236377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236377)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236377)Termination reason: Instruction limit % 11.07/2.22 % (236377)Termination phase: Saturation % 11.07/2.22 % (236377)Time elapsed: 0.131 s % 11.07/2.22 % (236377)Peak memory usage: 134 MB % 11.07/2.22 % (236377)Instructions burned: 67 (million) % 11.07/2.22 % (236404)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2581965968:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi) % 11.07/2.22 % (236404)Refutation not found, incomplete strategy % 11.07/2.22 % (236404)------------------------------ % 11.07/2.22 % (236404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236404)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236404)Termination reason: Refutation not found, incomplete strategy % 11.07/2.22 % (236404)Time elapsed: 0.002 s % 11.07/2.22 % (236404)Peak memory usage: 89 MB % 11.07/2.22 % (236404)Instructions burned: 3 (million) % 11.07/2.22 % (236403)dis+10_1_si=on:random_seed=347140080:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 11.07/2.22 % (236403)Instruction limit reached! % 11.07/2.22 % (236403)------------------------------ % 11.07/2.22 % (236403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236403)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236403)Termination reason: Instruction limit % 11.07/2.22 % (236403)Termination phase: Saturation % 11.07/2.22 % (236403)Time elapsed: 0.010 s % 11.07/2.22 % (236403)Peak memory usage: 88 MB % 11.07/2.22 % (236403)Instructions burned: 10 (million) % 11.07/2.22 % (236393)Instruction limit reached! % 11.07/2.22 % (236393)------------------------------ % 11.07/2.22 % (236393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.07/2.22 % (236393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.07/2.22 % (236393)CaDiCaL version: 2.1.3 % 11.07/2.22 % (236393)Termination reason: Instruction limit % 11.07/2.22 % (236393)Termination phase: Saturation % 11.95/2.64 % (236393)Time elapsed: 0.146 s % 11.95/2.64 % (236393)Peak memory usage: 116 MB % 11.95/2.64 % (236393)Instructions burned: 127 (million) % 11.95/2.64 % (236411)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2221523470:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 11.95/2.64 % (236407)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=882976824:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 11.95/2.64 % (236411)Instruction limit reached! % 11.95/2.64 % (236411)------------------------------ % 11.95/2.64 % (236411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.95/2.64 % (236411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.95/2.64 % (236411)CaDiCaL version: 2.1.3 % 11.95/2.64 % (236411)Termination reason: Instruction limit % 11.95/2.64 % (236411)Termination phase: Saturation % 11.95/2.64 % (236411)Time elapsed: 0.003 s % 11.95/2.64 % (236411)Peak memory usage: 87 MB % 11.95/2.64 % (236411)Instructions burned: 2 (million) % 11.95/2.64 % (236413)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3946483087:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi) % 11.95/2.64 % (236413)Instruction limit reached! % 11.95/2.64 % (236413)------------------------------ % 11.95/2.64 % (236413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.95/2.64 % (236413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.95/2.64 % (236413)CaDiCaL version: 2.1.3 % 11.95/2.64 % (236413)Termination reason: Instruction limit % 11.95/2.64 % (236413)Termination phase: Saturation % 11.95/2.64 % (236413)Time elapsed: 0.007 s % 11.95/2.64 % (236413)Peak memory usage: 88 MB % 11.95/2.64 % (236413)Instructions burned: 8 (million) % 11.95/2.64 % (236407)Instruction limit reached! % 11.95/2.64 % (236407)------------------------------ % 11.95/2.64 % (236407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.95/2.64 % (236407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.95/2.64 % (236407)CaDiCaL version: 2.1.3 % 11.95/2.64 % (236407)Termination reason: Instruction limit % 11.95/2.64 % (236407)Termination phase: Saturation % 11.95/2.64 % (236407)Time elapsed: 0.028 s % 11.95/2.64 % (236407)Peak memory usage: 89 MB % 11.95/2.64 % (236407)Instructions burned: 36 (million) % 11.95/2.64 % (236414)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3636245411:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 11.95/2.64 % (236404)------------------------------ % 11.95/2.64 % (236404)------------------------------ % 11.95/2.64 % (236431)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=3821706985:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 11.95/2.64 % (236423)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1155828367:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 11.95/2.64 % (236425)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=800315026:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi) % 11.95/2.64 % (236430)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4041748014:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi) % 11.95/2.64 % (236423)Instruction limit reached! % 11.95/2.64 % (236423)------------------------------ % 11.95/2.64 % (236423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.95/2.64 % (236423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.95/2.64 % (236423)CaDiCaL version: 2.1.3 % 11.95/2.64 % (236423)Termination reason: Instruction limit % 11.95/2.64 % (236423)Termination phase: Saturation % 11.95/2.64 % (236423)Time elapsed: 0.041 s % 11.95/2.64 % (236423)Peak memory usage: 116 MB % 11.95/2.64 % (236423)Instructions burned: 13 (million) % 11.95/2.64 % (236429)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2238647780:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 11.95/2.64 % (236431)Instruction limit reached! % 11.95/2.64 % (236431)------------------------------ % 11.95/2.64 % (236431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236431)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236431)Termination reason: Instruction limit % 14.53/3.02 % (236431)Termination phase: Saturation % 14.53/3.02 % (236431)Time elapsed: 0.060 s % 14.53/3.02 % (236431)Peak memory usage: 90 MB % 14.53/3.02 % (236431)Instructions burned: 76 (million) % 14.53/3.02 % (236425)Refutation not found, incomplete strategy % 14.53/3.02 % (236425)------------------------------ % 14.53/3.02 % (236425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236425)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236425)Termination reason: Refutation not found, incomplete strategy % 14.53/3.02 % (236425)Time elapsed: 0.038 s % 14.53/3.02 % (236425)Peak memory usage: 116 MB % 14.53/3.02 % (236425)Instructions burned: 9 (million) % 14.53/3.02 % (236429)Instruction limit reached! % 14.53/3.02 % (236429)------------------------------ % 14.53/3.02 % (236429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236429)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236429)Termination reason: Instruction limit % 14.53/3.02 % (236429)Termination phase: Saturation % 14.53/3.02 % (236429)Time elapsed: 0.011 s % 14.53/3.02 % (236429)Peak memory usage: 88 MB % 14.53/3.02 % (236429)Instructions burned: 10 (million) % 14.53/3.02 % (236438)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3984691316:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 14.53/3.02 % (236414)Instruction limit reached! % 14.53/3.02 % (236414)------------------------------ % 14.53/3.02 % (236414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236414)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236414)Termination reason: Instruction limit % 14.53/3.02 % (236414)Termination phase: Saturation % 14.53/3.02 % (236414)Time elapsed: 0.251 s % 14.53/3.02 % (236414)Peak memory usage: 91 MB % 14.53/3.02 % (236414)Instructions burned: 370 (million) % 14.53/3.02 % (236430)Instruction limit reached! % 14.53/3.02 % (236430)------------------------------ % 14.53/3.02 % (236430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236430)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236430)Termination reason: Instruction limit % 14.53/3.02 % (236430)Termination phase: Saturation % 14.53/3.02 % (236430)Time elapsed: 0.127 s % 14.53/3.02 % (236430)Peak memory usage: 133 MB % 14.53/3.02 % (236430)Instructions burned: 71 (million) % 14.53/3.02 % (236445)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=528275685:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 14.53/3.02 % (236446)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=432970181:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 14.53/3.02 % (236447)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3383865029:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi) % 14.53/3.02 % (236438)Instruction limit reached! % 14.53/3.02 % (236438)------------------------------ % 14.53/3.02 % (236438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236438)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236438)Termination reason: Instruction limit % 14.53/3.02 % (236438)Termination phase: Saturation % 14.53/3.02 % (236438)Time elapsed: 0.158 s % 14.53/3.02 % (236438)Peak memory usage: 90 MB % 14.53/3.02 % (236438)Instructions burned: 294 (million) % 14.53/3.02 % (236450)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2365225116:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi) % 14.53/3.02 % (236447)Instruction limit reached! % 14.53/3.02 % (236447)------------------------------ % 14.53/3.02 % (236447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.53/3.02 % (236447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.53/3.02 % (236447)CaDiCaL version: 2.1.3 % 14.53/3.02 % (236447)Termination reason: Instruction limit % 18.62/3.41 % (236447)Termination phase: Saturation % 18.62/3.41 % (236447)Time elapsed: 0.095 s % 18.62/3.41 % (236447)Peak memory usage: 133 MB % 18.62/3.41 % (236447)Instructions burned: 40 (million) % 18.62/3.41 % (236456)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=49391836:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/598Mi) % 18.62/3.41 % (236445)Instruction limit reached! % 18.62/3.41 % (236445)------------------------------ % 18.62/3.41 % (236445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.62/3.41 % (236445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.62/3.41 % (236445)CaDiCaL version: 2.1.3 % 18.62/3.41 % (236445)Termination reason: Instruction limit % 18.62/3.41 % (236445)Termination phase: Saturation % 18.62/3.41 % (236445)Time elapsed: 0.146 s % 18.62/3.41 % (236445)Peak memory usage: 116 MB % 18.62/3.41 % (236445)Instructions burned: 130 (million) % 18.62/3.41 % (236446)Instruction limit reached! % 18.62/3.41 % (236446)------------------------------ % 18.62/3.41 % (236446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.62/3.41 % (236446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.62/3.41 % (236446)CaDiCaL version: 2.1.3 % 18.62/3.41 % (236446)Termination reason: Instruction limit % 18.62/3.41 % (236446)Termination phase: Saturation % 18.62/3.41 % (236446)Time elapsed: 0.148 s % 18.62/3.41 % (236446)Peak memory usage: 133 MB % 18.62/3.41 % (236446)Instructions burned: 133 (million) % 18.62/3.41 % (236425)------------------------------ % 18.62/3.41 % (236425)------------------------------ % 18.62/3.41 % (236461)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2188407292:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 18.62/3.41 % (236471)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2587252622:i=383:fsr=off:rtra=on:ev=force_2984 on theBenchmark for (2984ds/383Mi) % 18.62/3.41 % (236469)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=940801486:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi) % 18.62/3.41 % (236461)Instruction limit reached! % 18.62/3.41 % (236461)------------------------------ % 18.62/3.41 % (236461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.62/3.41 % (236461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.62/3.41 % (236461)CaDiCaL version: 2.1.3 % 18.62/3.41 % (236461)Termination reason: Instruction limit % 18.62/3.41 % (236461)Termination phase: Saturation % 18.62/3.41 % (236461)Time elapsed: 0.116 s % 18.62/3.41 % (236461)Peak memory usage: 116 MB % 18.62/3.41 % (236461)Instructions burned: 131 (million) % 18.62/3.41 % (236470)dis+10_1_si=on:random_seed=241907183:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi) % 18.62/3.41 % (236450)Instruction limit reached! % 18.62/3.41 % (236450)------------------------------ % 18.62/3.41 % (236450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.62/3.41 % (236450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.62/3.41 % (236450)CaDiCaL version: 2.1.3 % 18.62/3.41 % (236450)Termination reason: Instruction limit % 18.62/3.41 % (236450)Termination phase: Saturation % 18.62/3.41 % (236450)Time elapsed: 0.279 s % 18.62/3.41 % (236450)Peak memory usage: 92 MB % 18.62/3.41 % (236450)Instructions burned: 307 (million) % 18.62/3.41 % (236474)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2345350473:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi) % 18.62/3.41 % (236487)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=631896341:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi) % 18.62/3.41 % (236474)Instruction limit reached! % 18.62/3.41 % (236474)------------------------------ % 18.62/3.41 % (236474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.62/3.41 % (236474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.62/3.41 % (236474)CaDiCaL version: 2.1.3 % 18.62/3.41 % (236474)Termination reason: Instruction limit % 18.62/3.41 % (236474)Termination phase: Saturation % 18.62/3.41 % (236474)Time elapsed: 0.148 s % 18.62/3.41 % (236474)Peak memory usage: 90 MB % 18.62/3.41 % (236474)Instructions burned: 141 (million) % 18.62/3.41 % (236486)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4169677654:i=65:nm=16:rtra=on_2982 on theBenchmark for (2982ds/65Mi) % 20.39/3.74 % (236469)Instruction limit reached! % 20.39/3.74 % (236469)------------------------------ % 20.39/3.74 % (236469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.39/3.74 % (236469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.74 % (236469)CaDiCaL version: 2.1.3 % 20.39/3.74 % (236469)Termination reason: Instruction limit % 20.39/3.74 % (236469)Termination phase: Saturation % 20.39/3.74 % (236469)Time elapsed: 0.253 s % 20.39/3.74 % (236469)Peak memory usage: 117 MB % 20.39/3.74 % (236469)Instructions burned: 260 (million) % 20.39/3.74 % (236486)Refutation not found, incomplete strategy % 20.39/3.74 % (236486)------------------------------ % 20.39/3.74 % (236486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.39/3.74 % (236486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.74 % (236486)CaDiCaL version: 2.1.3 % 20.39/3.74 % (236486)Termination reason: Refutation not found, incomplete strategy % 20.39/3.74 % (236486)Time elapsed: 0.040 s % 20.39/3.74 % (236486)Peak memory usage: 115 MB % 20.39/3.74 % (236486)Instructions burned: 8 (million) % 20.39/3.74 % (236487)Instruction limit reached! % 20.39/3.74 % (236487)------------------------------ % 20.39/3.74 % (236487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.39/3.74 % (236487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.74 % (236487)CaDiCaL version: 2.1.3 % 20.39/3.74 % (236487)Termination reason: Instruction limit % 20.39/3.74 % (236487)Termination phase: Saturation % 20.39/3.74 % (236487)Time elapsed: 0.071 s % 20.39/3.74 % (236487)Peak memory usage: 89 MB % 20.39/3.74 % (236487)Instructions burned: 122 (million) % 20.39/3.74 % (236471)Instruction limit reached! % 20.39/3.74 % (236471)------------------------------ % 20.39/3.74 % (236471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.39/3.74 % (236471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.74 % (236471)CaDiCaL version: 2.1.3 % 20.39/3.74 % (236471)Termination reason: Instruction limit % 20.39/3.74 % (236471)Termination phase: Saturation % 20.39/3.74 % (236471)Time elapsed: 0.333 s % 20.39/3.74 % (236471)Peak memory usage: 93 MB % 20.39/3.74 % (236471)Instructions burned: 384 (million) % 20.39/3.74 % (236498)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2383138973:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi) % 20.39/3.74 % (236494)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=1612539856:s2a=on:i=128:s2at=5:ins=3:rtra=on_2980 on theBenchmark for (2980ds/128Mi) % 20.39/3.74 % (236498)Instruction limit reached! % 20.39/3.74 % (236498)------------------------------ % 20.39/3.74 % (236498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.39/3.74 % (236498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.74 % (236498)CaDiCaL version: 2.1.3 % 20.39/3.74 % (236498)Termination reason: Instruction limit % 20.39/3.74 % (236498)Termination phase: Saturation % 20.39/3.74 % (236498)Time elapsed: 0.053 s % 20.39/3.74 % (236498)Peak memory usage: 116 MB % 20.39/3.74 % (236498)Instructions burned: 39 (million) % 20.39/3.74 % (236456)Instruction limit reached! % 20.39/3.74 % (236456)------------------------------ % 20.39/3.74 % (236456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.39/3.74 % (236456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.39/3.74 % (236456)CaDiCaL version: 2.1.3 % 20.39/3.74 % (236456)Termination reason: Instruction limit % 20.39/3.74 % (236456)Termination phase: Saturation % 20.39/3.74 % (236456)Time elapsed: 0.647 s % 20.39/3.74 % (236456)Peak memory usage: 138 MB % 20.39/3.74 % (236456)Instructions burned: 598 (million) % 20.39/3.74 % (236501)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2925546962:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/329Mi) % 20.39/3.74 % (236499)dis+1010_1_to=kbo:si=on:random_seed=3433861584:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi) % 20.39/3.74 % (236494)Instruction limit reached! % 20.39/3.74 % (236494)------------------------------ % 20.39/3.74 % (236494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.89/4.28 % (236494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/4.28 % (236494)CaDiCaL version: 2.1.3 % 24.89/4.28 % (236494)Termination reason: Instruction limit % 24.89/4.28 % (236494)Termination phase: Saturation % 24.89/4.28 % (236494)Time elapsed: 0.168 s % 24.89/4.28 % (236494)Peak memory usage: 117 MB % 24.89/4.28 % (236494)Instructions burned: 128 (million) % 24.89/4.28 % (236501)Instruction limit reached! % 24.89/4.28 % (236501)------------------------------ % 24.89/4.28 % (236501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.89/4.28 % (236501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/4.28 % (236501)CaDiCaL version: 2.1.3 % 24.89/4.28 % (236501)Termination reason: Instruction limit % 24.89/4.28 % (236501)Termination phase: Saturation % 24.89/4.28 % (236501)Time elapsed: 0.136 s % 24.89/4.28 % (236501)Peak memory usage: 118 MB % 24.89/4.28 % (236501)Instructions burned: 329 (million) % 24.89/4.28 % (236486)------------------------------ % 24.89/4.28 % (236486)------------------------------ % 24.89/4.28 % (236507)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2776191890:s2a=on:i=483:doe=on:nm=32:rtra=on_2977 on theBenchmark for (2977ds/483Mi) % 24.89/4.28 % (236499)Instruction limit reached! % 24.89/4.28 % (236499)------------------------------ % 24.89/4.28 % (236499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.89/4.28 % (236499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/4.28 % (236499)CaDiCaL version: 2.1.3 % 24.89/4.28 % (236499)Termination reason: Instruction limit % 24.89/4.28 % (236499)Termination phase: Saturation % 24.89/4.28 % (236499)Time elapsed: 0.176 s % 24.89/4.28 % (236499)Peak memory usage: 91 MB % 24.89/4.28 % (236499)Instructions burned: 175 (million) % 24.89/4.28 % (236508)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=650496860:thitd=on:i=215:nm=0:rtra=on:ev=force_2977 on theBenchmark for (2977ds/215Mi) % 24.89/4.28 % (236516)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1626135890:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi) % 24.89/4.28 % (236520)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1024001561:i=281:gtgl=2:rtra=on:gtg=all_2975 on theBenchmark for (2975ds/281Mi) % 24.89/4.28 % (236516)Refutation not found, incomplete strategy % 24.89/4.28 % (236516)------------------------------ % 24.89/4.28 % (236516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.89/4.28 % (236516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/4.28 % (236516)CaDiCaL version: 2.1.3 % 24.89/4.28 % (236516)Termination reason: Refutation not found, incomplete strategy % 24.89/4.28 % (236516)Time elapsed: 0.044 s % 24.89/4.28 % (236516)Peak memory usage: 115 MB % 24.89/4.28 % (236516)Instructions burned: 9 (million) % 24.89/4.28 % (236518)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=463283444:i=328:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/328Mi) % 24.89/4.28 % (236517)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2656107824:st=2:i=295:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/295Mi) % 24.89/4.28 % (236520)Instruction limit reached! % 24.89/4.28 % (236520)------------------------------ % 24.89/4.28 % (236520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.89/4.28 % (236520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/4.28 % (236520)CaDiCaL version: 2.1.3 % 24.89/4.28 % (236520)Termination reason: Instruction limit % 24.89/4.28 % (236520)Termination phase: Saturation % 24.89/4.28 % (236520)Time elapsed: 0.149 s % 24.89/4.28 % (236520)Peak memory usage: 118 MB % 24.89/4.28 % (236520)Instructions burned: 282 (million) % 24.89/4.28 % (236508)Instruction limit reached! % 24.89/4.28 % (236508)------------------------------ % 24.89/4.28 % (236508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.89/4.28 % (236508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/4.28 % (236508)CaDiCaL version: 2.1.3 % 24.89/4.28 % (236508)Termination reason: Instruction limit % 24.89/4.28 % (236508)Termination phase: Saturation % 24.89/4.28 % (236508)Time elapsed: 0.253 s % 24.89/4.28 % (236508)Peak memory usage: 138 MB % 24.89/4.28 % (236508)Instructions burned: 215 (million) % 24.89/4.28 % (236470)Instruction limit reached! % 24.89/4.28 % (236470)------------------------------ % 24.89/4.28 % (236470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.65 % (236470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.65 % (236470)CaDiCaL version: 2.1.3 % 26.59/4.65 % (236470)Termination reason: Instruction limit % 26.59/4.65 % (236470)Termination phase: Saturation % 26.59/4.65 % (236470)Time elapsed: 0.952 s % 26.59/4.65 % (236470)Peak memory usage: 93 MB % 26.59/4.65 % (236470)Instructions burned: 1000 (million) % 26.59/4.65 % (236534)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=4027955964:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi) % 26.59/4.65 % (236517)Instruction limit reached! % 26.59/4.65 % (236517)------------------------------ % 26.59/4.65 % (236517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.65 % (236517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.65 % (236517)CaDiCaL version: 2.1.3 % 26.59/4.65 % (236517)Termination reason: Instruction limit % 26.59/4.65 % (236517)Termination phase: Saturation % 26.59/4.65 % (236517)Time elapsed: 0.243 s % 26.59/4.65 % (236517)Peak memory usage: 90 MB % 26.59/4.65 % (236517)Instructions burned: 295 (million) % 26.59/4.65 % (236518)Instruction limit reached! % 26.59/4.65 % (236518)------------------------------ % 26.59/4.65 % (236518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.65 % (236518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.65 % (236518)CaDiCaL version: 2.1.3 % 26.59/4.65 % (236518)Termination reason: Instruction limit % 26.59/4.65 % (236518)Termination phase: Saturation % 26.59/4.65 % (236518)Time elapsed: 0.272 s % 26.59/4.65 % (236518)Peak memory usage: 118 MB % 26.59/4.65 % (236518)Instructions burned: 328 (million) % 26.59/4.65 % (236536)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=510558830:i=416:rtra=on:gtg=position:ss=axioms_2972 on theBenchmark for (2972ds/416Mi) % 26.59/4.65 % (236535)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2804005638:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2973 on theBenchmark for (2973ds/321Mi) % 26.59/4.65 % (236516)------------------------------ % 26.59/4.65 % (236516)------------------------------ % 26.59/4.65 % (236536)Refutation not found, incomplete strategy % 26.59/4.65 % (236536)------------------------------ % 26.59/4.65 % (236536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.65 % (236536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.65 % (236536)CaDiCaL version: 2.1.3 % 26.59/4.65 % (236536)Termination reason: Refutation not found, incomplete strategy % 26.59/4.65 % (236536)Time elapsed: 0.041 s % 26.59/4.65 % (236536)Peak memory usage: 116 MB % 26.59/4.65 % (236536)Instructions burned: 9 (million) % 26.59/4.65 % (236507)Instruction limit reached! % 26.59/4.65 % (236507)------------------------------ % 26.59/4.65 % (236507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.65 % (236507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.65 % (236507)CaDiCaL version: 2.1.3 % 26.59/4.65 % (236507)Termination reason: Instruction limit % 26.59/4.65 % (236507)Termination phase: Saturation % 26.59/4.65 % (236507)Time elapsed: 0.556 s % 26.59/4.65 % (236507)Peak memory usage: 137 MB % 26.59/4.65 % (236507)Instructions burned: 483 (million) % 26.59/4.65 % (236534)Instruction limit reached! % 26.59/4.65 % (236534)------------------------------ % 26.59/4.65 % (236534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.65 % (236534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.65 % (236534)CaDiCaL version: 2.1.3 % 26.59/4.65 % (236534)Termination reason: Instruction limit % 26.59/4.65 % (236534)Termination phase: Saturation % 26.59/4.65 % (236534)Time elapsed: 0.221 s % 26.59/4.65 % (236534)Peak memory usage: 92 MB % 26.59/4.65 % (236534)Instructions burned: 484 (million) % 26.59/4.65 % (236539)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=332330813:i=471:thf=on:kws=precedence:rtra=on_2971 on theBenchmark for (2971ds/471Mi) % 26.59/4.65 % (236541)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=2410189303:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi) % 26.59/4.65 % (236548)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=933601382:i=375:kws=inv_arity_squared:rtra=on_2970 on theBenchmark for (2970ds/375Mi) % 28.31/5.10 % (236535)Instruction limit reached! % 28.31/5.10 % (236535)------------------------------ % 28.31/5.10 % (236535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.31/5.10 % (236535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.31/5.10 % (236535)CaDiCaL version: 2.1.3 % 28.31/5.10 % (236535)Termination reason: Instruction limit % 28.31/5.10 % (236535)Termination phase: Saturation % 28.31/5.10 % (236535)Time elapsed: 0.264 s % 28.31/5.10 % (236535)Peak memory usage: 114 MB % 28.31/5.10 % (236535)Instructions burned: 321 (million) % 28.31/5.10 % (236549)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3104580069:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/387Mi) % 28.31/5.10 % (236552)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2463483:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2969 on theBenchmark for (2969ds/513Mi) % 28.31/5.10 % (236536)------------------------------ % 28.31/5.10 % (236536)------------------------------ % 28.31/5.10 % (236561)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=643585666:i=334:rtra=on_2968 on theBenchmark for (2968ds/334Mi) % 28.31/5.10 % (236541)Instruction limit reached! % 28.31/5.10 % (236541)------------------------------ % 28.31/5.10 % (236541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.31/5.10 % (236541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.31/5.10 % (236541)CaDiCaL version: 2.1.3 % 28.31/5.10 % (236541)Termination reason: Instruction limit % 28.31/5.10 % (236541)Termination phase: Saturation % 28.31/5.10 % (236541)Time elapsed: 0.365 s % 28.31/5.10 % (236541)Peak memory usage: 134 MB % 28.31/5.10 % (236541)Instructions burned: 278 (million) % 28.31/5.10 % (236539)Instruction limit reached! % 28.31/5.10 % (236539)------------------------------ % 28.31/5.10 % (236539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.31/5.10 % (236552)Instruction limit reached! % 28.31/5.10 % (236552)------------------------------ % 28.31/5.10 % (236552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.31/5.10 % (236552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.31/5.10 % (236539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.31/5.10 % (236539)CaDiCaL version: 2.1.3 % 28.31/5.10 % (236552)CaDiCaL version: 2.1.3 % 28.31/5.10 % (236539)Termination reason: Instruction limit % 28.31/5.10 % (236539)Termination phase: Saturation % 28.31/5.10 % (236552)Termination reason: Instruction limit % 28.31/5.10 % (236552)Termination phase: Saturation % 28.31/5.10 % (236539)Time elapsed: 0.419 s % 28.31/5.10 % (236552)Time elapsed: 0.239 s % 28.31/5.10 % (236539)Peak memory usage: 118 MB % 28.31/5.10 % (236552)Peak memory usage: 94 MB % 28.31/5.10 % (236539)Instructions burned: 471 (million) % 28.31/5.10 % (236552)Instructions burned: 514 (million) % 28.31/5.10 % (236548)Instruction limit reached! % 28.31/5.10 % (236548)------------------------------ % 28.31/5.10 % (236548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.31/5.10 % (236548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.31/5.10 % (236548)CaDiCaL version: 2.1.3 % 28.31/5.10 % (236548)Termination reason: Instruction limit % 28.31/5.10 % (236548)Termination phase: Saturation % 28.31/5.10 % (236548)Time elapsed: 0.396 s % 28.31/5.10 % (236548)Peak memory usage: 118 MB % 28.31/5.10 % (236548)Instructions burned: 378 (million) % 28.31/5.10 % (236566)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=947482656:i=359:rtra=on:gtg=exists_top:ss=axioms_2966 on theBenchmark for (2966ds/359Mi) % 28.31/5.10 % (236570)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2626570394:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2965 on theBenchmark for (2965ds/341Mi) % 28.31/5.10 % (236571)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=4097587820:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/261Mi) % 28.31/5.10 % (236549)Instruction limit reached! % 28.31/5.10 % (236549)------------------------------ % 28.31/5.10 % (236549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.31/5.10 % (236549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236549)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236549)Termination reason: Instruction limit % 34.14/5.66 % (236549)Termination phase: Saturation % 34.14/5.66 % (236549)Time elapsed: 0.433 s % 34.14/5.66 % (236549)Peak memory usage: 119 MB % 34.14/5.66 % (236549)Instructions burned: 387 (million) % 34.14/5.66 % (236571)Refutation not found, incomplete strategy % 34.14/5.66 % (236571)------------------------------ % 34.14/5.66 % (236571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.14/5.66 % (236571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236571)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236571)Termination reason: Refutation not found, incomplete strategy % 34.14/5.66 % (236571)Time elapsed: 0.024 s % 34.14/5.66 % (236571)Peak memory usage: 115 MB % 34.14/5.66 % (236571)Instructions burned: 7 (million) % 34.14/5.66 % (236572)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3308858382:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2965 on theBenchmark for (2965ds/235Mi) % 34.14/5.66 % (236573)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=608092619:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2965 on theBenchmark for (2965ds/273Mi) % 34.14/5.66 % (236561)Instruction limit reached! % 34.14/5.66 % (236561)------------------------------ % 34.14/5.66 % (236561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.14/5.66 % (236561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236561)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236561)Termination reason: Instruction limit % 34.14/5.66 % (236561)Termination phase: Saturation % 34.14/5.66 % (236561)Time elapsed: 0.350 s % 34.14/5.66 % (236561)Peak memory usage: 134 MB % 34.14/5.66 % (236561)Instructions burned: 334 (million) % 34.14/5.66 % (236571)------------------------------ % 34.14/5.66 % (236571)------------------------------ % 34.14/5.66 % (236583)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2065454054:i=146:doe=on:rtra=on_2963 on theBenchmark for (2963ds/146Mi) % 34.14/5.66 % (236566)Instruction limit reached! % 34.14/5.66 % (236566)------------------------------ % 34.14/5.66 % (236566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.14/5.66 % (236566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236566)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236566)Termination reason: Instruction limit % 34.14/5.66 % (236566)Termination phase: Saturation % 34.14/5.66 % (236566)Time elapsed: 0.327 s % 34.14/5.66 % (236566)Peak memory usage: 91 MB % 34.14/5.66 % (236566)Instructions burned: 359 (million) % 34.14/5.66 % (236570)Instruction limit reached! % 34.14/5.66 % (236570)------------------------------ % 34.14/5.66 % (236570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.14/5.66 % (236570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236570)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236570)Termination reason: Instruction limit % 34.14/5.66 % (236570)Termination phase: Saturation % 34.14/5.66 % (236570)Time elapsed: 0.285 s % 34.14/5.66 % (236570)Peak memory usage: 119 MB % 34.14/5.66 % (236570)Instructions burned: 341 (million) % 34.14/5.66 % (236587)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3724276431:i=4428:doe=on:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/4428Mi) % 34.14/5.66 % (236572)Instruction limit reached! % 34.14/5.66 % (236572)------------------------------ % 34.14/5.66 % (236572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.14/5.66 % (236572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236572)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236572)Termination reason: Instruction limit % 34.14/5.66 % (236572)Termination phase: Saturation % 34.14/5.66 % (236572)Time elapsed: 0.264 s % 34.14/5.66 % (236572)Peak memory usage: 117 MB % 34.14/5.66 % (236572)Instructions burned: 236 (million) % 34.14/5.66 % (236573)Instruction limit reached! % 34.14/5.66 % (236573)------------------------------ % 34.14/5.66 % (236573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.14/5.66 % (236573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.14/5.66 % (236573)CaDiCaL version: 2.1.3 % 34.14/5.66 % (236573)Termination reason: Instruction limit % 34.14/5.66 % (236573)Termination phase: Saturation % 34.14/5.66 % (236573)Time elapsed: 0.292 s % 40.63/6.47 % (236573)Peak memory usage: 91 MB % 40.63/6.47 % (236573)Instructions burned: 274 (million) % 40.63/6.47 % (236583)Instruction limit reached! % 40.63/6.47 % (236583)------------------------------ % 40.63/6.47 % (236583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.63/6.47 % (236583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.63/6.47 % (236583)CaDiCaL version: 2.1.3 % 40.63/6.47 % (236583)Termination reason: Instruction limit % 40.63/6.47 % (236583)Termination phase: Saturation % 40.63/6.47 % (236583)Time elapsed: 0.156 s % 40.63/6.47 % (236583)Peak memory usage: 90 MB % 40.63/6.47 % (236583)Instructions burned: 146 (million) % 40.63/6.47 % (236592)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=3844258901:avsq=on:i=276:avsqr=1,2:rtra=on_2961 on theBenchmark for (2961ds/276Mi) % 40.63/6.47 % (236593)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3509588037:i=1052:rtra=on_2961 on theBenchmark for (2961ds/1052Mi) % 40.63/6.47 % (236598)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=224417260:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2960 on theBenchmark for (2960ds/1054Mi) % 40.63/6.47 % (236594)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2343732050:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2961 on theBenchmark for (2961ds/655Mi) % 40.63/6.47 % (236594)Refutation not found, incomplete strategy % 40.63/6.47 % (236594)------------------------------ % 40.63/6.47 % (236594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.63/6.47 % (236594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.63/6.47 % (236594)CaDiCaL version: 2.1.3 % 40.63/6.47 % (236594)Termination reason: Refutation not found, incomplete strategy % 40.63/6.47 % (236594)Time elapsed: 0.007 s % 40.63/6.47 % (236594)Peak memory usage: 89 MB % 40.63/6.47 % (236594)Instructions burned: 5 (million) % 40.63/6.47 % (236598)Refutation not found, incomplete strategy % 40.63/6.47 % (236598)------------------------------ % 40.63/6.47 % (236598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.63/6.47 % (236598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.63/6.47 % (236598)CaDiCaL version: 2.1.3 % 40.63/6.47 % (236598)Termination reason: Refutation not found, incomplete strategy % 40.63/6.47 % (236598)Time elapsed: 0.015 s % 40.63/6.47 % (236598)Peak memory usage: 89 MB % 40.63/6.47 % (236598)Instructions burned: 24 (million) % 40.63/6.47 % (236600)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1137156055:i=107:rtra=on_2960 on theBenchmark for (2960ds/107Mi) % 40.63/6.47 % (236601)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=375090333:s2a=on:i=450:doe=on:nm=32:rtra=on_2960 on theBenchmark for (2960ds/450Mi) % 40.63/6.47 % (236600)Refutation not found, incomplete strategy % 40.63/6.47 % (236600)------------------------------ % 40.63/6.47 % (236600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.63/6.47 % (236600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.63/6.47 % (236600)CaDiCaL version: 2.1.3 % 40.63/6.47 % (236600)Termination reason: Refutation not found, incomplete strategy % 40.63/6.47 % (236600)Time elapsed: 0.033 s % 40.63/6.47 % (236600)Peak memory usage: 116 MB % 40.63/6.47 % (236600)Instructions burned: 9 (million) % 40.63/6.47 % (236598)------------------------------ % 40.63/6.47 % (236598)------------------------------ % 40.63/6.47 % (236592)Instruction limit reached! % 40.63/6.47 % (236592)------------------------------ % 40.63/6.47 % (236592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.63/6.47 % (236592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.63/6.47 % (236592)CaDiCaL version: 2.1.3 % 40.63/6.47 % (236592)Termination reason: Instruction limit % 40.63/6.47 % (236592)Termination phase: Saturation % 40.63/6.47 % (236592)Time elapsed: 0.312 s % 40.63/6.47 % (236592)Peak memory usage: 134 MB % 40.63/6.47 % (236592)Instructions burned: 276 (million) % 40.63/6.47 % (236594)------------------------------ % 40.63/6.47 % (236594)------------------------------ % 40.63/6.47 % (236616)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 42.57/7.02 % (236616)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1899823708:i=1090:aac=none:nm=0:rtra=on:rawr=on_2957 on theBenchmark for (2957ds/1090Mi) % 42.57/7.02 % (236616)Refutation not found, incomplete strategy % 42.57/7.02 % (236616)------------------------------ % 42.57/7.02 % (236616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.57/7.02 % (236616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.57/7.02 % (236616)CaDiCaL version: 2.1.3 % 42.57/7.02 % (236616)Termination reason: Refutation not found, incomplete strategy % 42.57/7.02 % (236616)Time elapsed: 0.050 s % 42.57/7.02 % (236616)Peak memory usage: 116 MB % 42.57/7.02 % (236616)Instructions burned: 67 (million) % 42.57/7.02 % (236619)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3972635575:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2956 on theBenchmark for (2956ds/130Mi) % 42.57/7.02 % (236600)------------------------------ % 42.57/7.02 % (236600)------------------------------ % 42.57/7.02 % (236620)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2069101877:i=312:kws=inv_frequency:nm=20:rtra=on_2955 on theBenchmark for (2955ds/312Mi) % 42.57/7.02 % (236601)Instruction limit reached! % 42.57/7.02 % (236601)------------------------------ % 42.57/7.02 % (236601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.57/7.02 % (236601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.57/7.02 % (236601)CaDiCaL version: 2.1.3 % 42.57/7.02 % (236601)Termination reason: Instruction limit % 42.57/7.02 % (236601)Termination phase: Saturation % 42.57/7.02 % (236601)Time elapsed: 0.473 s % 42.57/7.02 % (236601)Peak memory usage: 137 MB % 42.57/7.02 % (236601)Instructions burned: 450 (million) % 42.57/7.02 % (236616)------------------------------ % 42.57/7.02 % (236616)------------------------------ % 42.57/7.02 % (236619)Instruction limit reached! % 42.57/7.02 % (236619)------------------------------ % 42.57/7.02 % (236619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.57/7.02 % (236619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.57/7.02 % (236619)CaDiCaL version: 2.1.3 % 42.57/7.02 % (236619)Termination reason: Instruction limit % 42.57/7.02 % (236619)Termination phase: Saturation % 42.57/7.02 % (236619)Time elapsed: 0.152 s % 42.57/7.02 % (236619)Peak memory usage: 116 MB % 42.57/7.02 % (236619)Instructions burned: 130 (million) % 42.57/7.02 % (236628)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3901555359:i=491:doe=on:rtra=on:gtg=position_2953 on theBenchmark for (2953ds/491Mi) % 42.57/7.02 % (236593)Instruction limit reached! % 42.57/7.02 % (236593)------------------------------ % 42.57/7.02 % (236593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.57/7.02 % (236593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.57/7.02 % (236593)CaDiCaL version: 2.1.3 % 42.57/7.02 % (236593)Termination reason: Instruction limit % 42.57/7.02 % (236593)Termination phase: Saturation % 42.57/7.02 % (236593)Time elapsed: 0.736 s % 42.57/7.02 % (236593)Peak memory usage: 90 MB % 42.57/7.02 % (236593)Instructions burned: 1053 (million) % 42.57/7.02 % (236633)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1065741567:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2952 on theBenchmark for (2952ds/307Mi) % 42.57/7.02 % (236631)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3934777017:s2a=on:i=835:s2at=2:rtra=on_2953 on theBenchmark for (2953ds/835Mi) % 42.57/7.02 % (236620)Instruction limit reached! % 42.57/7.02 % (236620)------------------------------ % 42.57/7.02 % (236620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.57/7.02 % (236620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.57/7.02 % (236620)CaDiCaL version: 2.1.3 % 42.57/7.02 % (236620)Termination reason: Instruction limit % 42.57/7.02 % (236620)Termination phase: Saturation % 42.57/7.02 % (236620)Time elapsed: 0.298 s % 42.57/7.02 % (236620)Peak memory usage: 118 MB % 42.57/7.02 % (236620)Instructions burned: 312 (million) % 42.57/7.02 % (236634)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1394442283:i=776:doe=on:rtra=on_2952 on theBenchmark for (2952ds/776Mi) % 42.57/7.02 % (236633)Instruction limit reached! % 42.57/7.02 % (236633)------------------------------ % 42.57/7.02 % (236633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.30/7.64 % (236633)CaDiCaL version: 2.1.3 % 48.30/7.64 % (236633)Termination reason: Instruction limit % 48.30/7.64 % (236633)Termination phase: Saturation % 48.30/7.64 % (236633)Time elapsed: 0.155 s % 48.30/7.64 % (236633)Peak memory usage: 93 MB % 48.30/7.64 % (236633)Instructions burned: 307 (million) % 48.30/7.64 % (236637)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3749538887:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2951 on theBenchmark for (2951ds/646Mi) % 48.30/7.64 % (236641)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=2337614116:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2950 on theBenchmark for (2950ds/784Mi) % 48.30/7.64 % (236645)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=1322516239:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2950 on theBenchmark for (2950ds/1131Mi) % 48.30/7.64 % (236628)Instruction limit reached! % 48.30/7.64 % (236628)------------------------------ % 48.30/7.64 % (236628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.30/7.64 % (236628)CaDiCaL version: 2.1.3 % 48.30/7.64 % (236628)Termination reason: Instruction limit % 48.30/7.64 % (236628)Termination phase: Saturation % 48.30/7.64 % (236628)Time elapsed: 0.488 s % 48.30/7.64 % (236628)Peak memory usage: 92 MB % 48.30/7.64 % (236628)Instructions burned: 491 (million) % 48.30/7.64 % (236652)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3838152499:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2946 on theBenchmark for (2946ds/246Mi) % 48.30/7.64 % (236637)Instruction limit reached! % 48.30/7.64 % (236637)------------------------------ % 48.30/7.64 % (236637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.30/7.64 % (236637)CaDiCaL version: 2.1.3 % 48.30/7.64 % (236637)Termination reason: Instruction limit % 48.30/7.64 % (236637)Termination phase: Saturation % 48.30/7.64 % (236637)Time elapsed: 0.554 s % 48.30/7.64 % (236637)Peak memory usage: 137 MB % 48.30/7.64 % (236637)Instructions burned: 646 (million) % 48.30/7.64 % (236634)Instruction limit reached! % 48.30/7.64 % (236634)------------------------------ % 48.30/7.64 % (236634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.30/7.64 % (236634)CaDiCaL version: 2.1.3 % 48.30/7.64 % (236634)Termination reason: Instruction limit % 48.30/7.64 % (236634)Termination phase: Saturation % 48.30/7.64 % (236634)Time elapsed: 0.694 s % 48.30/7.64 % (236634)Peak memory usage: 122 MB % 48.30/7.64 % (236634)Instructions burned: 776 (million) % 48.30/7.64 % (236631)Instruction limit reached! % 48.30/7.64 % (236631)------------------------------ % 48.30/7.64 % (236631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.30/7.64 % (236631)CaDiCaL version: 2.1.3 % 48.30/7.64 % (236631)Termination reason: Instruction limit % 48.30/7.64 % (236631)Termination phase: Saturation % 48.30/7.64 % (236631)Time elapsed: 0.841 s % 48.30/7.64 % (236631)Peak memory usage: 94 MB % 48.30/7.64 % (236631)Instructions burned: 836 (million) % 48.30/7.64 % (236645)Instruction limit reached! % 48.30/7.64 % (236645)------------------------------ % 48.30/7.64 % (236645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.30/7.64 % (236645)CaDiCaL version: 2.1.3 % 48.30/7.64 % (236645)Termination reason: Instruction limit % 48.30/7.64 % (236645)Termination phase: Saturation % 48.30/7.64 % (236645)Time elapsed: 0.588 s % 48.30/7.64 % (236645)Peak memory usage: 122 MB % 48.30/7.64 % (236645)Instructions burned: 1131 (million) % 48.30/7.64 % (236652)Instruction limit reached! % 48.30/7.64 % (236652)------------------------------ % 48.30/7.64 % (236652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.30/7.64 % (236652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.11/8.86 % (236652)CaDiCaL version: 2.1.3 % 57.11/8.86 % (236652)Termination reason: Instruction limit % 57.11/8.86 % (236652)Termination phase: Saturation % 57.11/8.86 % (236652)Time elapsed: 0.269 s % 57.11/8.86 % (236652)Peak memory usage: 117 MB % 57.11/8.86 % (236652)Instructions burned: 246 (million) % 57.11/8.86 % (236660)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3003459013:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2944 on theBenchmark for (2944ds/775Mi) % 57.11/8.86 % (236662)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2747720272:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2943 on theBenchmark for (2943ds/273Mi) % 57.11/8.86 % (236666)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=488089040:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2942 on theBenchmark for (2942ds/1094Mi) % 57.11/8.86 % (236664)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=470515944:i=102:nm=16:rtra=on_2942 on theBenchmark for (2942ds/102Mi) % 57.11/8.86 % (236667)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=214425226:i=6400:doe=on:fsr=off:rtra=on_2941 on theBenchmark for (2941ds/6400Mi) % 57.11/8.86 % (236641)Instruction limit reached! % 57.11/8.86 % (236641)------------------------------ % 57.11/8.86 % (236641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.11/8.86 % (236641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.11/8.86 % (236641)CaDiCaL version: 2.1.3 % 57.11/8.86 % (236641)Termination reason: Instruction limit % 57.11/8.86 % (236641)Termination phase: Saturation % 57.11/8.86 % (236641)Time elapsed: 0.864 s % 57.11/8.86 % (236641)Peak memory usage: 122 MB % 57.11/8.86 % (236641)Instructions burned: 784 (million) % 57.11/8.86 % (236664)Instruction limit reached! % 57.11/8.86 % (236664)------------------------------ % 57.11/8.86 % (236664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.11/8.86 % (236664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.11/8.86 % (236664)CaDiCaL version: 2.1.3 % 57.11/8.86 % (236664)Termination reason: Instruction limit % 57.11/8.86 % (236664)Termination phase: Saturation % 57.11/8.86 % (236664)Time elapsed: 0.094 s % 57.11/8.86 % (236664)Peak memory usage: 89 MB % 57.11/8.86 % (236664)Instructions burned: 103 (million) % 57.11/8.86 % (236662)Instruction limit reached! % 57.11/8.86 % (236662)------------------------------ % 57.11/8.86 % (236662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.11/8.86 % (236662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.11/8.86 % (236662)CaDiCaL version: 2.1.3 % 57.11/8.86 % (236662)Termination reason: Instruction limit % 57.11/8.86 % (236662)Termination phase: Saturation % 57.11/8.86 % (236662)Time elapsed: 0.294 s % 57.11/8.86 % (236662)Peak memory usage: 91 MB % 57.11/8.86 % (236662)Instructions burned: 273 (million) % 57.11/8.86 % (236677)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1612631309:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2939 on theBenchmark for (2939ds/868Mi) % 57.11/8.86 % (236678)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=1209531122:i=1846:canc=cautious:fsr=off:rtra=on_2939 on theBenchmark for (2939ds/1846Mi) % 57.11/8.86 % (236677)Refutation not found, incomplete strategy % 57.11/8.86 % (236677)------------------------------ % 57.11/8.86 % (236677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.11/8.86 % (236677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.11/8.86 % (236677)CaDiCaL version: 2.1.3 % 57.11/8.86 % (236677)Termination reason: Refutation not found, incomplete strategy % 57.11/8.86 % (236677)Time elapsed: 0.047 s % 57.11/8.86 % (236677)Peak memory usage: 116 MB % 57.11/8.86 % (236677)Instructions burned: 12 (million) % 57.11/8.86 % (236666)Instruction limit reached! % 57.11/8.86 % (236666)------------------------------ % 57.11/8.86 % (236666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.11/8.86 % (236666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.11/8.86 % (236666)CaDiCaL version: 2.1.3 % 57.11/8.86 % (236666)Termination reason: Instruction limit % 57.11/8.86 % (236666)Termination phase: Saturation % 57.11/8.86 % (236666)Time elapsed: 0.434 s % 76.58/11.51 % (236666)Peak memory usage: 92 MB % 76.58/11.51 % (236666)Instructions burned: 1097 (million) % 76.58/11.51 % (236682)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1776290630:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2938 on theBenchmark for (2938ds/36816Mi) % 76.58/11.51 % (236682)Refutation not found, incomplete strategy % 76.58/11.51 % (236682)------------------------------ % 76.58/11.51 % (236682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.58/11.51 % (236682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.58/11.51 % (236682)CaDiCaL version: 2.1.3 % 76.58/11.51 % (236682)Termination reason: Refutation not found, incomplete strategy % 76.58/11.51 % (236682)Time elapsed: 0.005 s % 76.58/11.51 % (236682)Peak memory usage: 88 MB % 76.58/11.51 % (236682)Instructions burned: 3 (million) % 76.58/11.51 % (236687)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2280957515:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2936 on theBenchmark for (2936ds/273Mi) % 76.58/11.51 % (236660)Instruction limit reached! % 76.58/11.51 % (236660)------------------------------ % 76.58/11.51 % (236660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.58/11.51 % (236660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.58/11.51 % (236660)CaDiCaL version: 2.1.3 % 76.58/11.51 % (236660)Termination reason: Instruction limit % 76.58/11.51 % (236660)Termination phase: Saturation % 76.58/11.51 % (236660)Time elapsed: 0.778 s % 76.58/11.51 % (236660)Peak memory usage: 95 MB % 76.58/11.51 % (236660)Instructions burned: 776 (million) % 76.58/11.51 % (236687)Instruction limit reached! % 76.58/11.51 % (236687)------------------------------ % 76.58/11.51 % (236687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.58/11.51 % (236687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.58/11.51 % (236687)CaDiCaL version: 2.1.3 % 76.58/11.51 % (236687)Termination reason: Instruction limit % 76.58/11.51 % (236687)Termination phase: Saturation % 76.58/11.51 % (236687)Time elapsed: 0.148 s % 76.58/11.51 % (236687)Peak memory usage: 91 MB % 76.58/11.51 % (236687)Instructions burned: 273 (million) % 76.58/11.51 % (236677)------------------------------ % 76.58/11.52 % (236677)------------------------------ % 76.58/11.52 % (236682)------------------------------ % 76.58/11.52 % (236682)------------------------------ % 76.58/11.52 % (236694)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3572292606:i=5811:kws=precedence:nm=0:rtra=on_2933 on theBenchmark for (2933ds/5811Mi) % 76.58/11.52 % (236694)Refutation not found, incomplete strategy % 76.58/11.52 % (236694)------------------------------ % 76.58/11.52 % (236694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.58/11.52 % (236694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.58/11.52 % (236694)CaDiCaL version: 2.1.3 % 76.58/11.52 % (236694)Termination reason: Refutation not found, incomplete strategy % 76.58/11.52 % (236694)Time elapsed: 0.039 s % 76.58/11.52 % (236694)Peak memory usage: 116 MB % 76.58/11.52 % (236694)Instructions burned: 46 (million) % 76.58/11.52 % (236693)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=478298289:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2933 on theBenchmark for (2933ds/863Mi) % 76.58/11.52 % (236693)Refutation not found, incomplete strategy % 76.58/11.52 % (236693)------------------------------ % 76.58/11.52 % (236693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.58/11.52 % (236693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.58/11.52 % (236693)CaDiCaL version: 2.1.3 % 76.58/11.52 % (236693)Termination reason: Refutation not found, incomplete strategy % 76.58/11.52 % (236693)Time elapsed: 0.041 s % 76.58/11.52 % (236693)Peak memory usage: 116 MB % 76.58/11.52 % (236693)Instructions burned: 13 (million) % 76.58/11.52 % (236696)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=471972610:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2933 on theBenchmark for (2933ds/2216Mi) % 76.58/11.52 % (236699)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3410642278:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2932 on theBenchmark for (2932ds/801Mi) % 76.58/11.52 % (236699)Refutation not found, incomplete strategy % 76.58/11.52 % (236699)------------------------------ % 99.86/14.89 % (236699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.86/14.89 % (236699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.86/14.89 % (236699)CaDiCaL version: 2.1.3 % 99.86/14.89 % (236699)Termination reason: Refutation not found, incomplete strategy % 99.86/14.89 % (236699)Time elapsed: 0.007 s % 99.86/14.89 % (236699)Peak memory usage: 89 MB % 99.86/14.89 % (236699)Instructions burned: 5 (million) % 99.86/14.89 % (236694)------------------------------ % 99.86/14.89 % (236694)------------------------------ % 99.86/14.89 % (236708)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2548913588:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2929 on theBenchmark for (2929ds/1026Mi) % 99.86/14.89 % (236708)Refutation not found, incomplete strategy % 99.86/14.89 % (236708)------------------------------ % 99.86/14.89 % (236708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.86/14.89 % (236708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.86/14.89 % (236708)CaDiCaL version: 2.1.3 % 99.86/14.89 % (236708)Termination reason: Refutation not found, incomplete strategy % 99.86/14.89 % (236708)Time elapsed: 0.015 s % 99.86/14.89 % (236708)Peak memory usage: 89 MB % 99.86/14.89 % (236708)Instructions burned: 24 (million) % 99.86/14.89 % (236693)------------------------------ % 99.86/14.89 % (236693)------------------------------ % 99.86/14.89 % (236699)------------------------------ % 99.86/14.89 % (236699)------------------------------ % 99.86/14.89 % (236708)------------------------------ % 99.86/14.89 % (236708)------------------------------ % 99.86/14.89 % (236712)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2865911338:i=3509:rtra=on_2927 on theBenchmark for (2927ds/3509Mi) % 99.86/14.89 % (236714)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1553477654:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2926 on theBenchmark for (2926ds/2127Mi) % 99.86/14.89 % (236716)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=903027528:i=1959:rtra=on:fsd=on:proc=on_2925 on theBenchmark for (2925ds/1959Mi) % 99.86/14.89 % (236716)Refutation not found, incomplete strategy % 99.86/14.89 % (236716)------------------------------ % 99.86/14.89 % (236716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.86/14.89 % (236716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.86/14.89 % (236716)CaDiCaL version: 2.1.3 % 99.86/14.89 % (236716)Termination reason: Refutation not found, incomplete strategy % 99.86/14.89 % (236716)Time elapsed: 0.028 s % 99.86/14.89 % (236716)Peak memory usage: 116 MB % 99.86/14.89 % (236716)Instructions burned: 11 (million) % 99.86/14.89 % (236678)Instruction limit reached! % 99.86/14.89 % (236678)------------------------------ % 99.86/14.89 % (236678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.86/14.89 % (236678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.86/14.89 % (236678)CaDiCaL version: 2.1.3 % 99.86/14.89 % (236678)Termination reason: Instruction limit % 99.86/14.89 % (236678)Termination phase: Saturation % 99.86/14.89 % (236678)Time elapsed: 1.590 s % 99.86/14.89 % (236678)Peak memory usage: 96 MB % 99.86/14.89 % (236678)Instructions burned: 1847 (million) % 99.86/14.89 % (236716)------------------------------ % 99.86/14.89 % (236716)------------------------------ % 99.86/14.89 % (236587)Instruction limit reached! % 99.86/14.89 % (236587)------------------------------ % 99.86/14.89 % (236587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.86/14.89 % (236587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.86/14.89 % (236587)CaDiCaL version: 2.1.3 % 99.86/14.89 % (236587)Termination reason: Instruction limit % 99.86/14.89 % (236587)Termination phase: Saturation % 99.86/14.89 % (236587)Time elapsed: 4.013 s % 99.86/14.89 % (236587)Peak memory usage: 113 MB % 99.86/14.89 % (236587)Instructions burned: 4428 (million) % 99.86/14.89 % (236726)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4168647184:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2921 on theBenchmark for (2921ds/3201Mi) % 99.86/14.89 % (236724)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1271055912:s2a=on:i=3553:nm=0:rtra=on_2921 on theBenchmark for (2921ds/3553Mi) % 99.86/14.89 % (236728)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=3367380614:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2920 on theBenchmark for (2920ds/4093Mi) % 149.77/21.88 % (236696)Instruction limit reached! % 149.77/21.88 % (236696)------------------------------ % 149.77/21.88 % (236696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.77/21.88 % (236696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.77/21.88 % (236696)CaDiCaL version: 2.1.3 % 149.77/21.88 % (236696)Termination reason: Instruction limit % 149.77/21.88 % (236696)Termination phase: Saturation % 149.77/21.88 % (236696)Time elapsed: 1.878 s % 149.77/21.88 % (236696)Peak memory usage: 125 MB % 149.77/21.88 % (236696)Instructions burned: 2216 (million) % 149.77/21.88 % (236726)Refutation not found, incomplete strategy % 149.77/21.88 % (236726)------------------------------ % 149.77/21.88 % (236726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.77/21.88 % (236726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.77/21.88 % (236726)CaDiCaL version: 2.1.3 % 149.77/21.88 % (236726)Termination reason: Refutation not found, incomplete strategy % 149.77/21.88 % (236726)Time elapsed: 0.918 s % 149.77/21.88 % (236726)Peak memory usage: 95 MB % 149.77/21.88 % (236726)Instructions burned: 2155 (million) % 149.77/21.88 % (236739)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=4198206048:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2912 on theBenchmark for (2912ds/21173Mi) % 149.77/21.88 % (236714)Instruction limit reached! % 149.77/21.88 % (236714)------------------------------ % 149.77/21.88 % (236714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.77/21.88 % (236714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.77/21.88 % (236714)CaDiCaL version: 2.1.3 % 149.77/21.88 % (236714)Termination reason: Instruction limit % 149.77/21.88 % (236714)Termination phase: Saturation % 149.77/21.88 % (236714)Time elapsed: 1.549 s % 149.77/21.88 % (236714)Peak memory usage: 101 MB % 149.77/21.88 % (236714)Instructions burned: 2129 (million) % 149.77/21.88 % (236726)------------------------------ % 149.77/21.88 % (236726)------------------------------ % 149.77/21.88 % (236744)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2559151911:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2908 on theBenchmark for (2908ds/10544Mi) % 149.77/21.88 % (236746)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4124143476:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2908 on theBenchmark for (2908ds/1262Mi) % 149.77/21.88 % (236746)Refutation not found, incomplete strategy % 149.77/21.88 % (236746)------------------------------ % 149.77/21.88 % (236746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.77/21.88 % (236746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.77/21.88 % (236746)CaDiCaL version: 2.1.3 % 149.77/21.88 % (236746)Termination reason: Refutation not found, incomplete strategy % 149.77/21.88 % (236746)Time elapsed: 0.025 s % 149.77/21.88 % (236746)Peak memory usage: 116 MB % 149.77/21.88 % (236746)Instructions burned: 9 (million) % 149.77/21.88 % (236746)------------------------------ % 149.77/21.88 % (236746)------------------------------ % 149.77/21.88 % (236749)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1662809837:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2904 on theBenchmark for (2904ds/775Mi) % 149.77/21.88 % (236749)Instruction limit reached! % 149.77/21.88 % (236749)------------------------------ % 149.77/21.88 % (236749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.77/21.88 % (236749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.77/21.88 % (236749)CaDiCaL version: 2.1.3 % 149.77/21.88 % (236749)Termination reason: Instruction limit % 149.77/21.88 % (236749)Termination phase: Saturation % 149.77/21.88 % (236749)Time elapsed: 0.393 s % 149.77/21.88 % (236749)Peak memory usage: 96 MB % 149.77/21.88 % (236749)Instructions burned: 775 (million) % 149.77/21.88 % (236756)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=599464662:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2898 on theBenchmark for (2898ds/270Mi) % 149.77/21.88 % (236756)Instruction limit reached! % 149.77/21.88 % (236756)------------------------------ % 149.77/21.88 % (236756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.77/21.88 % (236756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.77/25.08 % (236756)CaDiCaL version: 2.1.3 % 171.77/25.08 % (236756)Termination reason: Instruction limit % 171.77/25.08 % (236756)Termination phase: Saturation % 171.77/25.08 % (236756)Time elapsed: 0.154 s % 171.77/25.08 % (236756)Peak memory usage: 91 MB % 171.77/25.08 % (236756)Instructions burned: 270 (million) % 171.77/25.08 % (236762)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3194902314:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2891 on theBenchmark for (2891ds/17165Mi) % 171.77/25.08 % (236712)Instruction limit reached! % 171.77/25.08 % (236712)------------------------------ % 171.77/25.08 % (236712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.77/25.08 % (236712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.77/25.08 % (236712)CaDiCaL version: 2.1.3 % 171.77/25.08 % (236712)Termination reason: Instruction limit % 171.77/25.08 % (236712)Termination phase: Saturation % 171.77/25.08 % (236712)Time elapsed: 3.542 s % 171.77/25.08 % (236712)Peak memory usage: 106 MB % 171.77/25.08 % (236712)Instructions burned: 3510 (million) % 171.77/25.08 % (236764)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=137418066:s2a=on:i=13094:s2at=-1:rtra=on_2889 on theBenchmark for (2889ds/13094Mi) % 171.77/25.08 % (236724)Instruction limit reached! % 171.77/25.08 % (236724)------------------------------ % 171.77/25.08 % (236724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.77/25.08 % (236724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.77/25.08 % (236724)CaDiCaL version: 2.1.3 % 171.77/25.08 % (236724)Termination reason: Instruction limit % 171.77/25.08 % (236724)Termination phase: Saturation % 171.77/25.08 % (236724)Time elapsed: 3.582 s % 171.77/25.08 % (236724)Peak memory usage: 100 MB % 171.77/25.08 % (236724)Instructions burned: 3553 (million) % 171.77/25.08 % (236768)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=493185609:st=2:i=12633:rtra=on:ss=axioms_2883 on theBenchmark for (2883ds/12633Mi) % 171.77/25.08 % (236728)Instruction limit reached! % 171.77/25.08 % (236728)------------------------------ % 171.77/25.08 % (236728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.77/25.08 % (236728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.77/25.08 % (236728)CaDiCaL version: 2.1.3 % 171.77/25.08 % (236728)Termination reason: Instruction limit % 171.77/25.08 % (236728)Termination phase: Saturation % 171.77/25.08 % (236728)Time elapsed: 3.656 s % 171.77/25.08 % (236728)Peak memory usage: 143 MB % 171.77/25.08 % (236728)Instructions burned: 4093 (million) % 171.77/25.08 % (236667)Instruction limit reached! % 171.77/25.08 % (236667)------------------------------ % 171.77/25.08 % (236667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.77/25.08 % (236667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.77/25.08 % (236667)CaDiCaL version: 2.1.3 % 171.77/25.08 % (236667)Termination reason: Instruction limit % 171.77/25.08 % (236667)Termination phase: Saturation % 171.77/25.08 % (236667)Time elapsed: 5.997 s % 171.77/25.08 % (236667)Peak memory usage: 128 MB % 171.77/25.08 % (236667)Instructions burned: 6401 (million) % 171.77/25.08 % (236771)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3797906743:i=1783:rtra=on:gtg=position_2881 on theBenchmark for (2881ds/1783Mi) % 171.77/25.08 % (236772)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=155147131:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2879 on theBenchmark for (2879ds/5451Mi) % 171.77/25.08 % (236771)Instruction limit reached! % 171.77/25.08 % (236771)------------------------------ % 171.77/25.08 % (236771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.77/25.08 % (236771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.77/25.08 % (236771)CaDiCaL version: 2.1.3 % 171.77/25.08 % (236771)Termination reason: Instruction limit % 171.77/25.08 % (236771)Termination phase: Saturation % 171.77/25.08 % (236771)Time elapsed: 1.845 s % 171.77/25.08 % (236771)Peak memory usage: 132 MB % 171.77/25.08 % (236771)Instructions burned: 1783 (million) % 171.77/25.08 % (236789)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=2729670759:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2860 on theBenchmark for (2860ds/4975Mi) % 171.77/25.08 % (236789)Refutation not found, incomplete strategy % 171.77/25.08 % (236789)------------------------------ % 171.77/25.08 % (236789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.44/26.13 % (236789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.44/26.13 % (236789)CaDiCaL version: 2.1.3 % 178.44/26.13 % (236789)Termination reason: Refutation not found, incomplete strategy % 178.44/26.13 % (236789)Time elapsed: 0.047 s % 178.44/26.13 % (236789)Peak memory usage: 116 MB % 178.44/26.13 % (236789)Instructions burned: 13 (million) % 178.44/26.13 % (236789)------------------------------ % 178.44/26.13 % (236789)------------------------------ % 178.44/26.13 % (236791)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=2173437495:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2853 on theBenchmark for (2853ds/2076Mi) % 178.44/26.13 % (236791)Instruction limit reached! % 178.44/26.13 % (236791)------------------------------ % 178.44/26.13 % (236791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.44/26.13 % (236791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.44/26.13 % (236791)CaDiCaL version: 2.1.3 % 178.44/26.13 % (236791)Termination reason: Instruction limit % 178.44/26.13 % (236791)Termination phase: Saturation % 178.44/26.13 % (236791)Time elapsed: 1.857 s % 178.44/26.13 % (236791)Peak memory usage: 128 MB % 178.44/26.13 % (236791)Instructions burned: 2077 (million) % 178.44/26.13 % (236795)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2870484704:i=5145:rtra=on_2832 on theBenchmark for (2832ds/5145Mi) % 178.44/26.13 % (236772)Instruction limit reached! % 178.44/26.13 % (236772)------------------------------ % 178.44/26.13 % (236772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.44/26.13 % (236772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.44/26.13 % (236772)CaDiCaL version: 2.1.3 % 178.44/26.13 % (236772)Termination reason: Instruction limit % 178.44/26.13 % (236772)Termination phase: Saturation % 178.44/26.13 % (236772)Time elapsed: 5.218 s % 178.44/26.13 % (236772)Peak memory usage: 148 MB % 178.44/26.13 % (236772)Instructions burned: 5451 (million) % 178.44/26.13 % (236798)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1033489097:i=3509:rtra=on_2825 on theBenchmark for (2825ds/3509Mi) % 178.44/26.14 % (236762)Instruction limit reached! % 178.44/26.14 % (236762)------------------------------ % 178.44/26.14 % (236762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.44/26.14 % (236762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.44/26.14 % (236762)CaDiCaL version: 2.1.3 % 178.44/26.14 % (236762)Termination reason: Instruction limit % 178.44/26.14 % (236762)Termination phase: Saturation % 178.44/26.14 % (236762)Time elapsed: 7.448 s % 178.44/26.14 % (236762)Peak memory usage: 140 MB % 178.44/26.14 % (236762)Instructions burned: 17165 (million) % 178.44/26.14 % (236800)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1703258609:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2815 on theBenchmark for (2815ds/13800Mi) % 178.44/26.14 % (236744)Instruction limit reached! % 178.44/26.14 % (236744)------------------------------ % 178.44/26.14 % (236744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.44/26.14 % (236744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.44/26.14 % (236744)CaDiCaL version: 2.1.3 % 178.44/26.14 % (236744)Termination reason: Instruction limit % 178.44/26.14 % (236744)Termination phase: Saturation % 178.44/26.14 % (236744)Time elapsed: 11.061 s % 178.44/26.14 % (236744)Peak memory usage: 202 MB % 178.44/26.14 % (236744)Instructions burned: 10544 (million) % 178.44/26.14 % (236805)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2843122126:i=1412:rtra=on:fsd=on:proc=on_2796 on theBenchmark for (2796ds/1412Mi) % 178.44/26.14 % (236805)Refutation not found, incomplete strategy % 178.44/26.14 % (236805)------------------------------ % 178.44/26.14 % (236805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.44/26.14 % (236805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.44/26.14 % (236805)CaDiCaL version: 2.1.3 % 178.44/26.14 % (236805)Termination reason: Refutation not found, incomplete strategy % 178.44/26.14 % (236805)Time elapsed: 0.046 s % 178.44/26.14 % (236805)Peak memory usage: 116 MB % 178.44/26.14 % (236805)Instructions burned: 11 (million) % 178.44/26.14 % (236805)------------------------------ % 178.44/26.14 % (236805)------------------------------ % 178.44/26.14 % (236810)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 196.02/28.32 % (236810)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4163100187:i=11747:aac=none:nm=0:rtra=on:rawr=on_2789 on theBenchmark for (2789ds/11747Mi) % 196.02/28.32 % (236798)Instruction limit reached! % 196.02/28.32 % (236798)------------------------------ % 196.02/28.32 % (236798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.02/28.32 % (236798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.02/28.32 % (236798)CaDiCaL version: 2.1.3 % 196.02/28.32 % (236798)Termination reason: Instruction limit % 196.02/28.32 % (236798)Termination phase: Saturation % 196.02/28.32 % (236798)Time elapsed: 3.598 s % 196.02/28.32 % (236798)Peak memory usage: 107 MB % 196.02/28.32 % (236798)Instructions burned: 3510 (million) % 196.02/28.32 % (236795)Instruction limit reached! % 196.02/28.32 % (236795)------------------------------ % 196.02/28.32 % (236795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.02/28.32 % (236795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.02/28.32 % (236795)CaDiCaL version: 2.1.3 % 196.02/28.32 % (236795)Termination reason: Instruction limit % 196.02/28.32 % (236795)Termination phase: Saturation % 196.02/28.32 % (236795)Time elapsed: 4.355 s % 196.02/28.32 % (236795)Peak memory usage: 95 MB % 196.02/28.32 % (236795)Instructions burned: 5145 (million) % 196.02/28.32 % (236810)Refutation not found, incomplete strategy % 196.02/28.32 % (236810)------------------------------ % 196.02/28.32 % (236810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.02/28.32 % (236810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.02/28.32 % (236810)CaDiCaL version: 2.1.3 % 196.02/28.32 % (236810)Termination reason: Refutation not found, incomplete strategy % 196.02/28.32 % (236810)Time elapsed: 0.099 s % 196.02/28.32 % (236810)Peak memory usage: 116 MB % 196.02/28.32 % (236810)Instructions burned: 66 (million) % 196.02/28.32 % (236813)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3718694268:s2a=on:i=3553:nm=0:rtra=on_2787 on theBenchmark for (2787ds/3553Mi) % 196.02/28.32 % (236814)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1649857036:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/3201Mi) % 196.02/28.32 % (236810)------------------------------ % 196.02/28.32 % (236810)------------------------------ % 196.02/28.32 % (236818)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=3182302906:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2782 on theBenchmark for (2782ds/4081Mi) % 196.02/28.32 % (236764)Instruction limit reached! % 196.02/28.32 % (236764)------------------------------ % 196.02/28.32 % (236764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.02/28.32 % (236764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.02/28.32 % (236764)CaDiCaL version: 2.1.3 % 196.02/28.32 % (236764)Termination reason: Instruction limit % 196.02/28.32 % (236764)Termination phase: Saturation % 196.02/28.32 % (236764)Time elapsed: 12.301 s % 196.02/28.32 % (236764)Peak memory usage: 135 MB % 196.02/28.32 % (236764)Instructions burned: 13094 (million) % 196.02/28.32 % (236825)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=1761751668:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2764 on theBenchmark for (2764ds/20260Mi) % 196.02/28.32 % (236814)Instruction limit reached! % 196.02/28.32 % (236814)------------------------------ % 196.02/28.32 % (236814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.02/28.32 % (236814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.02/28.32 % (236814)CaDiCaL version: 2.1.3 % 196.02/28.32 % (236814)Termination reason: Instruction limit % 196.02/28.32 % (236814)Termination phase: Saturation % 196.02/28.32 % (236814)Time elapsed: 2.709 s % 196.02/28.32 % (236814)Peak memory usage: 95 MB % 196.02/28.32 % (236814)Instructions burned: 3203 (million) % 196.02/28.32 % (236800)Instruction limit reached! % 196.02/28.32 % (236800)------------------------------ % 196.02/28.32 % (236800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.02/28.32 % (236800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.31/33.70 % (236800)CaDiCaL version: 2.1.3 % 234.31/33.70 % (236800)Termination reason: Instruction limit % 234.31/33.70 % (236800)Termination phase: Saturation % 234.31/33.70 % (236800)Time elapsed: 5.801 s % 234.31/33.70 % (236800)Peak memory usage: 138 MB % 234.31/33.70 % (236800)Instructions burned: 13801 (million) % 234.31/33.70 % (236830)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2813922704:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2757 on theBenchmark for (2757ds/58627Mi) % 234.31/33.70 % (236830)Refutation not found, incomplete strategy % 234.31/33.70 % (236830)------------------------------ % 234.31/33.70 % (236830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.31/33.70 % (236830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.31/33.70 % (236830)CaDiCaL version: 2.1.3 % 234.31/33.70 % (236830)Termination reason: Refutation not found, incomplete strategy % 234.31/33.70 % (236830)Time elapsed: 0.005 s % 234.31/33.70 % (236830)Peak memory usage: 88 MB % 234.31/33.70 % (236830)Instructions burned: 3 (million) % 234.31/33.70 % (236832)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4179784385:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2755 on theBenchmark for (2755ds/6258Mi) % 234.31/33.70 % (236832)Refutation not found, incomplete strategy % 234.31/33.70 % (236832)------------------------------ % 234.31/33.70 % (236832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.31/33.70 % (236832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.31/33.70 % (236832)CaDiCaL version: 2.1.3 % 234.31/33.70 % (236832)Termination reason: Refutation not found, incomplete strategy % 234.31/33.70 % (236832)Time elapsed: 0.025 s % 234.31/33.70 % (236832)Peak memory usage: 116 MB % 234.31/33.70 % (236832)Instructions burned: 9 (million) % 234.31/33.70 % (236832)------------------------------ % 234.31/33.70 % (236832)------------------------------ % 234.31/33.70 % (236830)------------------------------ % 234.31/33.70 % (236830)------------------------------ % 234.31/33.70 % (236837)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3203040523:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2751 on theBenchmark for (2751ds/34001Mi) % 234.31/33.70 % (236813)Instruction limit reached! % 234.31/33.70 % (236813)------------------------------ % 234.31/33.70 % (236813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.31/33.70 % (236813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.31/33.70 % (236813)CaDiCaL version: 2.1.3 % 234.31/33.70 % (236813)Termination reason: Instruction limit % 234.31/33.70 % (236813)Termination phase: Saturation % 234.31/33.70 % (236813)Time elapsed: 3.555 s % 234.31/33.70 % (236813)Peak memory usage: 99 MB % 234.31/33.70 % (236813)Instructions burned: 3553 (million) % 234.31/33.70 % (236839)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3899656556:s2a=on:i=71622:s2at=-1:rtra=on_2751 on theBenchmark for (2751ds/71622Mi) % 234.31/33.70 % (236841)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3663730690:i=24001:kws=precedence:nm=0:rtra=on_2750 on theBenchmark for (2750ds/24001Mi) % 234.31/33.70 % (236841)Refutation not found, incomplete strategy % 234.31/33.70 % (236841)------------------------------ % 234.31/33.70 % (236841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.31/33.70 % (236841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.31/33.70 % (236841)CaDiCaL version: 2.1.3 % 234.31/33.70 % (236841)Termination reason: Refutation not found, incomplete strategy % 234.31/33.70 % (236841)Time elapsed: 0.053 s % 234.31/33.70 % (236841)Peak memory usage: 116 MB % 234.31/33.70 % (236841)Instructions burned: 17 (million) % 234.31/33.70 % (236739)Instruction limit reached! % 234.31/33.70 % (236739)------------------------------ % 234.31/33.70 % (236739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.31/33.70 % (236739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.31/33.70 % (236739)CaDiCaL version: 2.1.3 % 234.31/33.70 % (236739)Termination reason: Instruction limit % 234.31/33.70 % (236739)Termination phase: Saturation % 234.31/33.70 % (236739)Time elapsed: 16.440 s % 234.31/33.70 % (236739)Peak memory usage: 138 MB % 234.31/33.70 % (236739)Instructions burned: 21173 (million) % 234.31/33.70 % (236818)Instruction limit reached! % 234.31/33.70 % (236818)------------------------------ % 234.31/33.70 % (236818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.60/37.72 % (236818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.60/37.72 % (236818)CaDiCaL version: 2.1.3 % 262.60/37.72 % (236818)Termination reason: Instruction limit % 262.60/37.72 % (236818)Termination phase: Saturation % 262.60/37.72 % (236818)Time elapsed: 3.528 s % 262.60/37.72 % (236818)Peak memory usage: 140 MB % 262.60/37.72 % (236818)Instructions burned: 4081 (million) % 262.60/37.72 % (236768)Instruction limit reached! % 262.60/37.72 % (236768)------------------------------ % 262.60/37.72 % (236768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.60/37.72 % (236768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.60/37.72 % (236768)CaDiCaL version: 2.1.3 % 262.60/37.72 % (236768)Termination reason: Instruction limit % 262.60/37.72 % (236768)Termination phase: Saturation % 262.60/37.72 % (236768)Time elapsed: 13.733 s % 262.60/37.72 % (236768)Peak memory usage: 134 MB % 262.60/37.72 % (236768)Instructions burned: 12633 (million) % 262.60/37.72 % (236846)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=293783187:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2745 on theBenchmark for (2745ds/2076Mi) % 262.60/37.72 % (236841)------------------------------ % 262.60/37.72 % (236841)------------------------------ % 262.60/37.72 % (236847)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3860190185:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2745 on theBenchmark for (2745ds/83971Mi) % 262.60/37.72 % (236848)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1291539035:i=83944:rtra=on_2744 on theBenchmark for (2744ds/83944Mi) % 262.60/37.72 % (236848)Refutation not found, incomplete strategy % 262.60/37.72 % (236848)------------------------------ % 262.60/37.72 % (236848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.60/37.72 % (236848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.60/37.72 % (236848)CaDiCaL version: 2.1.3 % 262.60/37.72 % (236848)Termination reason: Refutation not found, incomplete strategy % 262.60/37.72 % (236848)Time elapsed: 0.046 s % 262.60/37.72 % (236848)Peak memory usage: 116 MB % 262.60/37.72 % (236848)Instructions burned: 12 (million) % 262.60/37.72 % (236851)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=815806796:i=9201:rtra=on_2743 on theBenchmark for (2743ds/9201Mi) % 262.60/37.72 % (236848)------------------------------ % 262.60/37.72 % (236848)------------------------------ % 262.60/37.72 % (236856)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 262.60/37.72 % (236856)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1084331273:i=6806:aac=none:nm=0:rtra=on:rawr=on_2737 on theBenchmark for (2737ds/6806Mi) % 262.60/37.72 % (236856)Refutation not found, incomplete strategy % 262.60/37.72 % (236856)------------------------------ % 262.60/37.72 % (236856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.60/37.72 % (236856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.60/37.72 % (236856)CaDiCaL version: 2.1.3 % 262.60/37.72 % (236856)Termination reason: Refutation not found, incomplete strategy % 262.60/37.72 % (236856)Time elapsed: 0.192 s % 262.60/37.72 % (236856)Peak memory usage: 117 MB % 262.60/37.72 % (236856)Instructions burned: 179 (million) % 262.60/37.72 % (236856)------------------------------ % 262.60/37.72 % (236856)------------------------------ % 262.60/37.72 % (236862)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3003761389:s2a=on:i=3553:nm=0:rtra=on_2729 on theBenchmark for (2729ds/3553Mi) % 262.60/37.72 % (236846)Instruction limit reached! % 262.60/37.72 % (236846)------------------------------ % 262.60/37.72 % (236846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.60/37.72 % (236846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.60/37.72 % (236846)CaDiCaL version: 2.1.3 % 262.60/37.72 % (236846)Termination reason: Instruction limit % 262.60/37.72 % (236846)Termination phase: Saturation % 262.60/37.72 % (236846)Time elapsed: 1.760 s % 262.60/37.72 % (236846)Peak memory usage: 126 MB % 262.60/37.72 % (236846)Instructions burned: 2076 (million) % 262.60/37.72 % (236865)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=2845133329:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2725 on theBenchmark for (2725ds/2064Mi) % 271.59/39.05 % (236865)Instruction limit reached! % 271.59/39.05 % (236865)------------------------------ % 271.59/39.05 % (236865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.59/39.05 % (236865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.59/39.05 % (236865)CaDiCaL version: 2.1.3 % 271.59/39.05 % (236865)Termination reason: Instruction limit % 271.59/39.05 % (236865)Termination phase: Saturation % 271.59/39.05 % (236865)Time elapsed: 2.137 s % 271.59/39.05 % (236865)Peak memory usage: 144 MB % 271.59/39.05 % (236865)Instructions burned: 2064 (million) % 271.59/39.05 % (236872)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=1086002925:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2702 on theBenchmark for (2702ds/20260Mi) % 271.59/39.05 % (236862)Instruction limit reached! % 271.59/39.05 % (236862)------------------------------ % 271.59/39.05 % (236862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.59/39.05 % (236862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.59/39.05 % (236862)CaDiCaL version: 2.1.3 % 271.59/39.05 % (236862)Termination reason: Instruction limit % 271.59/39.05 % (236862)Termination phase: Saturation % 271.59/39.05 % (236862)Time elapsed: 3.622 s % 271.59/39.05 % (236862)Peak memory usage: 99 MB % 271.59/39.05 % (236862)Instructions burned: 3553 (million) % 271.59/39.05 % (236876)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4241426310:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2691 on theBenchmark for (2691ds/1244Mi) % 271.59/39.05 % (236876)Refutation not found, incomplete strategy % 271.59/39.05 % (236876)------------------------------ % 271.59/39.05 % (236876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.59/39.05 % (236876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.59/39.05 % (236876)CaDiCaL version: 2.1.3 % 271.59/39.05 % (236876)Termination reason: Refutation not found, incomplete strategy % 271.59/39.05 % (236876)Time elapsed: 0.043 s % 271.59/39.05 % (236876)Peak memory usage: 116 MB % 271.59/39.05 % (236876)Instructions burned: 9 (million) % 271.59/39.05 % (236876)------------------------------ % 271.59/39.05 % (236876)------------------------------ % 271.59/39.05 % (236880)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=189192471:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2685 on theBenchmark for (2685ds/58261Mi) % 271.59/39.05 % (236880)Refutation not found, incomplete strategy % 271.59/39.05 % (236880)------------------------------ % 271.59/39.05 % (236880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.59/39.05 % (236880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.59/39.05 % (236880)CaDiCaL version: 2.1.3 % 271.59/39.05 % (236880)Termination reason: Refutation not found, incomplete strategy % 271.59/39.05 % (236880)Time elapsed: 0.047 s % 271.59/39.05 % (236880)Peak memory usage: 116 MB % 271.59/39.05 % (236880)Instructions burned: 12 (million) % 271.59/39.05 % (236880)------------------------------ % 271.59/39.05 % (236880)------------------------------ % 271.59/39.05 % (236882)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 271.59/39.05 % (236882)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4124516259:i=6806:aac=none:nm=0:rtra=on:rawr=on_2678 on theBenchmark for (2678ds/6806Mi) % 271.59/39.05 % (236882)Refutation not found, incomplete strategy % 271.59/39.05 % (236882)------------------------------ % 271.59/39.05 % (236882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.59/39.05 % (236882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.59/39.05 % (236882)CaDiCaL version: 2.1.3 % 271.59/39.05 % (236882)Termination reason: Refutation not found, incomplete strategy % 271.59/39.05 % (236882)Time elapsed: 0.163 s % 271.59/39.05 % (236882)Peak memory usage: 117 MB % 271.59/39.05 % (236882)Instructions burned: 176 (million) % 271.59/39.05 % (236882)------------------------------ % 271.59/39.05 % (236882)------------------------------ % 271.59/39.05 % (236886)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=4161625586:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2671 on theBenchmark for (2671ds/4081Mi) % 278.00/39.95 % (236851)Instruction limit reached! % 278.00/39.95 % (236851)------------------------------ % 278.00/39.95 % (236851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.95 % (236851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.95 % (236851)CaDiCaL version: 2.1.3 % 278.00/39.95 % (236851)Termination reason: Instruction limit % 278.00/39.95 % (236851)Termination phase: Saturation % 278.00/39.95 % (236851)Time elapsed: 9.682 s % 278.00/39.95 % (236851)Peak memory usage: 127 MB % 278.00/39.95 % (236851)Instructions burned: 9202 (million) % 278.00/39.95 % (236890)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3592105334:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2644 on theBenchmark for (2644ds/1701Mi) % 278.00/39.95 % (236890)Refutation not found, incomplete strategy % 278.00/39.95 % (236890)------------------------------ % 278.00/39.95 % (236890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.95 % (236890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.95 % (236890)CaDiCaL version: 2.1.3 % 278.00/39.95 % (236890)Termination reason: Refutation not found, incomplete strategy % 278.00/39.95 % (236890)Time elapsed: 0.034 s % 278.00/39.95 % (236890)Peak memory usage: 116 MB % 278.00/39.95 % (236890)Instructions burned: 9 (million) % 278.00/39.95 % (236890)------------------------------ % 278.00/39.95 % (236890)------------------------------ % 278.00/39.95 % (236894)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=369107182:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2638 on theBenchmark for (2638ds/57001Mi) % 278.00/39.95 % (236894)Refutation not found, incomplete strategy % 278.00/39.95 % (236894)------------------------------ % 278.00/39.95 % (236894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.95 % (236894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.95 % (236894)CaDiCaL version: 2.1.3 % 278.00/39.95 % (236894)Termination reason: Refutation not found, incomplete strategy % 278.00/39.95 % (236894)Time elapsed: 0.045 s % 278.00/39.95 % (236894)Peak memory usage: 116 MB % 278.00/39.95 % (236894)Instructions burned: 12 (million) % 278.00/39.95 % (236886)Instruction limit reached! % 278.00/39.95 % (236886)------------------------------ % 278.00/39.95 % (236886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.95 % (236886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.95 % (236886)CaDiCaL version: 2.1.3 % 278.00/39.95 % (236886)Termination reason: Instruction limit % 278.00/39.95 % (236886)Termination phase: Saturation % 278.00/39.95 % (236886)Time elapsed: 3.675 s % 278.00/39.95 % (236886)Peak memory usage: 142 MB % 278.00/39.95 % (236886)Instructions burned: 4082 (million) % 278.00/39.95 % (236894)------------------------------ % 278.00/39.95 % (236894)------------------------------ % 278.00/39.95 % (236897)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2350905008:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2632 on theBenchmark for (2632ds/24Mi) % 278.00/39.95 % (236896)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 278.00/39.95 % (236896)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3617084261:i=8622:aac=none:nm=0:rtra=on:rawr=on_2632 on theBenchmark for (2632ds/8622Mi) % 278.00/39.95 % (236897)Instruction limit reached! % 278.00/39.95 % (236897)------------------------------ % 278.00/39.95 % (236897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.00/39.95 % (236897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.00/39.95 % (236897)CaDiCaL version: 2.1.3 % 278.00/39.95 % (236897)Termination reason: Instruction limit % 278.00/39.95 % (236897)Termination phase: Saturation % 278.00/39.95 % (236897)Time elapsed: 0.042 s % 278.00/39.95 % (236897)Peak memory usage: 115 MB % 278.00/39.95 % (236897)Instructions burned: 25 (million) % 278.00/39.95 % (236896)Refutation not found, incomplete strategy % 278.00/39.95 % (236896)------------------------------ % 278.00/39.95 % (236896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.77/40.77 % (236896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.77/40.77 % (236896)CaDiCaL version: 2.1.3 % 283.77/40.77 % (236896)Termination reason: Refutation not found, incomplete strategy % 283.77/40.77 % (236896)Time elapsed: 0.107 s % 283.77/40.77 % (236896)Peak memory usage: 116 MB % 283.77/40.77 % (236896)Instructions burned: 74 (million) % 283.77/40.77 % (236900)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=543377225:i=614:kws=precedence:nm=0:rtra=on_2630 on theBenchmark for (2630ds/614Mi) % 283.77/40.77 % (236900)Refutation not found, incomplete strategy % 283.77/40.77 % (236900)------------------------------ % 283.77/40.77 % (236900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.77/40.77 % (236900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.77/40.77 % (236900)CaDiCaL version: 2.1.3 % 283.77/40.77 % (236900)Termination reason: Refutation not found, incomplete strategy % 283.77/40.77 % (236900)Time elapsed: 0.081 s % 283.77/40.77 % (236900)Peak memory usage: 116 MB % 283.77/40.77 % (236900)Instructions burned: 46 (million) % 283.77/40.77 % (236896)------------------------------ % 283.77/40.77 % (236896)------------------------------ % 283.77/40.77 % (236900)------------------------------ % 283.77/40.77 % (236900)------------------------------ % 283.77/40.77 % (236904)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=318822314:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2625 on theBenchmark for (2625ds/402Mi) % 283.77/40.77 % (236905)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=756572028:s2a=on:i=14:rtra=on:inst=on_2623 on theBenchmark for (2623ds/14Mi) % 283.77/40.77 % (236905)Instruction limit reached! % 283.77/40.77 % (236905)------------------------------ % 283.77/40.77 % (236905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.77/40.77 % (236905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.77/40.77 % (236905)CaDiCaL version: 2.1.3 % 283.77/40.77 % (236905)Termination reason: Instruction limit % 283.77/40.77 % (236905)Termination phase: Saturation % 283.77/40.77 % (236905)Time elapsed: 0.015 s % 283.77/40.77 % (236905)Peak memory usage: 89 MB % 283.77/40.77 % (236905)Instructions burned: 14 (million) % 283.77/40.77 % (236908)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=150655348:i=8:rtra=on_2621 on theBenchmark for (2621ds/8Mi) % 283.77/40.77 % (236908)Instruction limit reached! % 283.77/40.77 % (236908)------------------------------ % 283.77/40.77 % (236908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.77/40.77 % (236908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.77/40.77 % (236908)CaDiCaL version: 2.1.3 % 283.77/40.77 % (236908)Termination reason: Instruction limit % 283.77/40.77 % (236908)Termination phase: Saturation % 283.77/40.77 % (236908)Time elapsed: 0.008 s % 283.77/40.77 % (236908)Peak memory usage: 89 MB % 283.77/40.77 % (236908)Instructions burned: 8 (million) % 283.77/40.77 % (236904)Instruction limit reached! % 283.77/40.77 % (236904)------------------------------ % 283.77/40.77 % (236904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.77/40.77 % (236904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.77/40.77 % (236904)CaDiCaL version: 2.1.3 % 283.77/40.77 % (236904)Termination reason: Instruction limit % 283.77/40.77 % (236904)Termination phase: Saturation % 283.77/40.77 % (236904)Time elapsed: 0.394 s % 283.77/40.77 % (236904)Peak memory usage: 119 MB % 283.77/40.77 % (236904)Instructions burned: 402 (million) % 283.77/40.77 % (236911)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3602523367:i=92:rtra=on_2619 on theBenchmark for (2619ds/92Mi) % 283.77/40.77 % (236912)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2643610612:i=66:rtra=on_2619 on theBenchmark for (2619ds/66Mi) % 283.77/40.77 % (236911)Instruction limit reached! % 283.77/40.77 % (236911)------------------------------ % 283.77/40.77 % (236911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.77/40.77 % (236911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.77/40.77 % (236911)CaDiCaL version: 2.1.3 % 283.77/40.77 % (236911)Termination reason: Instruction limit % 283.77/40.77 % (236911)Termination phase: Saturation % 283.77/40.77 % (236911)Time elapsed: 0.117 s % 283.77/40.77 % (236911)Peak memory usage: 116 MB % 283.77/40.77 % (236911)Instructions burned: 92 (million) % 283.77/40.77 % (236912)Instruction limit reached! % 283.77/40.77 % (236912)------------------------------ % 283.77/40.77 % (236912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.27 % (236912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.27 % (236912)CaDiCaL version: 2.1.3 % 287.76/41.27 % (236912)Termination reason: Instruction limit % 287.76/41.27 % (236912)Termination phase: Saturation % 287.76/41.27 % (236912)Time elapsed: 0.101 s % 287.76/41.27 % (236912)Peak memory usage: 116 MB % 287.76/41.27 % (236912)Instructions burned: 66 (million) % 287.76/41.27 % (236917)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2120422061:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2616 on theBenchmark for (2616ds/28Mi) % 287.76/41.27 % (236917)Instruction limit reached! % 287.76/41.27 % (236917)------------------------------ % 287.76/41.27 % (236917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.27 % (236917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.27 % (236917)CaDiCaL version: 2.1.3 % 287.76/41.27 % (236917)Termination reason: Instruction limit % 287.76/41.27 % (236917)Termination phase: Saturation % 287.76/41.27 % (236917)Time elapsed: 0.028 s % 287.76/41.27 % (236917)Peak memory usage: 88 MB % 287.76/41.27 % (236917)Instructions burned: 29 (million) % 287.76/41.27 % (236918)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=476039047:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2616 on theBenchmark for (2616ds/58Mi) % 287.76/41.27 % (236918)Instruction limit reached! % 287.76/41.27 % (236918)------------------------------ % 287.76/41.27 % (236918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.27 % (236918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.27 % (236918)CaDiCaL version: 2.1.3 % 287.76/41.27 % (236918)Termination reason: Instruction limit % 287.76/41.27 % (236918)Termination phase: Saturation % 287.76/41.27 % (236918)Time elapsed: 0.063 s % 287.76/41.27 % (236918)Peak memory usage: 89 MB % 287.76/41.27 % (236918)Instructions burned: 58 (million) % 287.76/41.27 % (236921)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2080057981:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2614 on theBenchmark for (2614ds/32Mi) % 287.76/41.27 % (236921)Instruction limit reached! % 287.76/41.27 % (236921)------------------------------ % 287.76/41.27 % (236921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.27 % (236921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.27 % (236921)CaDiCaL version: 2.1.3 % 287.76/41.27 % (236921)Termination reason: Instruction limit % 287.76/41.27 % (236921)Termination phase: Saturation % 287.76/41.27 % (236921)Time elapsed: 0.021 s % 287.76/41.27 % (236921)Peak memory usage: 90 MB % 287.76/41.27 % (236921)Instructions burned: 33 (million) % 287.76/41.27 % (236924)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2547946077:i=48:canc=force:rtra=on_2613 on theBenchmark for (2613ds/48Mi) % 287.76/41.27 % (236924)Instruction limit reached! % 287.76/41.27 % (236924)------------------------------ % 287.76/41.27 % (236924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.27 % (236924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.27 % (236924)CaDiCaL version: 2.1.3 % 287.76/41.27 % (236924)Termination reason: Instruction limit % 287.76/41.27 % (236924)Termination phase: Saturation % 287.76/41.27 % (236924)Time elapsed: 0.054 s % 287.76/41.27 % (236924)Peak memory usage: 90 MB % 287.76/41.27 % (236924)Instructions burned: 48 (million) % 287.76/41.27 % (236926)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=1799145743:i=54:canc=cautious:fsr=off:rtra=on_2611 on theBenchmark for (2611ds/54Mi) % 287.76/41.27 % (236926)Instruction limit reached! % 287.76/41.27 % (236926)------------------------------ % 287.76/41.27 % (236926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.76/41.27 % (236926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.76/41.27 % (236926)CaDiCaL version: 2.1.3 % 287.76/41.27 % (236926)Termination reason: Instruction limit % 287.76/41.27 % (236926)Termination phase: Saturation % 287.76/41.27 % (236926)Time elapsed: 0.049 s % 287.76/41.27 % (236926)Peak memory usage: 89 MB % 287.76/41.27 % (236926)Instructions burned: 54 (million) % 287.76/41.27 % (236929)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1501008592:i=170:gtgl=4:rtra=on:gtg=exists_sym_2610 on theBenchmark for (2610ds/170Mi) % 287.76/41.27 % (236929)Instruction limit reached! % 291.17/41.88 % (236929)------------------------------ % 291.17/41.88 % (236929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.17/41.88 % (236929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.88 % (236929)CaDiCaL version: 2.1.3 % 291.17/41.88 % (236929)Termination reason: Instruction limit % 291.17/41.88 % (236929)Termination phase: Saturation % 291.17/41.88 % (236929)Time elapsed: 0.162 s % 291.17/41.88 % (236929)Peak memory usage: 90 MB % 291.17/41.88 % (236929)Instructions burned: 170 (million) % 291.17/41.88 % (236931)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3354944093:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2609 on theBenchmark for (2609ds/4Mi) % 291.17/41.88 % (236931)Instruction limit reached! % 291.17/41.88 % (236931)------------------------------ % 291.17/41.88 % (236931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.17/41.88 % (236931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.88 % (236931)CaDiCaL version: 2.1.3 % 291.17/41.88 % (236931)Termination reason: Instruction limit % 291.17/41.88 % (236931)Termination phase: Saturation % 291.17/41.88 % (236931)Time elapsed: 0.005 s % 291.17/41.88 % (236931)Peak memory usage: 88 MB % 291.17/41.88 % (236931)Instructions burned: 4 (million) % 291.17/41.88 % (236933)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3390099899:i=362:rtra=on:ss=axioms:ev=cautious_2607 on theBenchmark for (2607ds/362Mi) % 291.17/41.88 % (236935)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4112665611:i=8:ep=RST:ins=2:rtra=on_2606 on theBenchmark for (2606ds/8Mi) % 291.17/41.88 % (236935)Instruction limit reached! % 291.17/41.88 % (236935)------------------------------ % 291.17/41.88 % (236935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.17/41.88 % (236935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.88 % (236935)CaDiCaL version: 2.1.3 % 291.17/41.88 % (236935)Termination reason: Instruction limit % 291.17/41.88 % (236935)Termination phase: Saturation % 291.17/41.88 % (236935)Time elapsed: 0.010 s % 291.17/41.88 % (236935)Peak memory usage: 89 MB % 291.17/41.88 % (236935)Instructions burned: 9 (million) % 291.17/41.88 % (236933)Refutation not found, incomplete strategy % 291.17/41.88 % (236933)------------------------------ % 291.17/41.88 % (236933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.17/41.88 % (236933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.88 % (236933)CaDiCaL version: 2.1.3 % 291.17/41.88 % (236933)Termination reason: Refutation not found, incomplete strategy % 291.17/41.88 % (236933)Time elapsed: 0.079 s % 291.17/41.88 % (236933)Peak memory usage: 91 MB % 291.17/41.88 % (236933)Instructions burned: 74 (million) % 291.17/41.88 % (236938)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4186012343:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2604 on theBenchmark for (2604ds/132Mi) % 291.17/41.88 % (236825)Instruction limit reached! % 291.17/41.88 % (236825)------------------------------ % 291.17/41.88 % (236825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.17/41.88 % (236825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.88 % (236825)CaDiCaL version: 2.1.3 % 291.17/41.88 % (236825)Termination reason: Instruction limit % 291.17/41.88 % (236825)Termination phase: Saturation % 291.17/41.88 % (236825)Time elapsed: 15.999 s % 291.17/41.88 % (236825)Peak memory usage: 143 MB % 291.17/41.88 % (236825)Instructions burned: 20260 (million) % 291.17/41.88 % (236940)lrs+10_1_thi=all:si=on:fd=off:random_seed=2853314234:i=106:rtra=on:gtg=all_2602 on theBenchmark for (2602ds/106Mi) % 291.17/41.88 % (236933)------------------------------ % 291.17/41.88 % (236933)------------------------------ % 291.17/41.88 % (236938)Instruction limit reached! % 291.17/41.88 % (236938)------------------------------ % 291.17/41.88 % (236938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.17/41.88 % (236938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.88 % (236938)CaDiCaL version: 2.1.3 % 291.17/41.88 % (236938)Termination reason: Instruction limit % 291.17/41.88 % (236938)Termination phase: Saturation % 291.17/41.88 % (236938)Time elapsed: 0.204 s % 291.17/41.88 % (236938)Peak memory usage: 135 MB % 291.17/41.88 % (236938)Instructions burned: 132 (million) % 291.17/41.88 % (236940)Instruction limit reached! % 291.17/41.88 % (236940)------------------------------ % 291.17/41.88 % (236940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.08/42.61 % (236940)CaDiCaL version: 2.1.3 % 296.08/42.61 % (236940)Termination reason: Instruction limit % 296.08/42.61 % (236940)Termination phase: Saturation % 296.08/42.61 % (236940)Time elapsed: 0.147 s % 296.08/42.61 % (236940)Peak memory usage: 117 MB % 296.08/42.61 % (236940)Instructions burned: 106 (million) % 296.08/42.61 % (236942)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2037608935:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2600 on theBenchmark for (2600ds/16Mi) % 296.08/42.61 % (236942)Instruction limit reached! % 296.08/42.61 % (236942)------------------------------ % 296.08/42.61 % (236942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.08/42.61 % (236942)CaDiCaL version: 2.1.3 % 296.08/42.61 % (236942)Termination reason: Instruction limit % 296.08/42.61 % (236942)Termination phase: Saturation % 296.08/42.61 % (236942)Time elapsed: 0.018 s % 296.08/42.61 % (236942)Peak memory usage: 88 MB % 296.08/42.61 % (236942)Instructions burned: 16 (million) % 296.08/42.61 % (236943)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4160649572:st=3:i=4:rtra=on:ss=axioms_2600 on theBenchmark for (2600ds/4Mi) % 296.08/42.61 % (236943)Instruction limit reached! % 296.08/42.61 % (236943)------------------------------ % 296.08/42.61 % (236943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.08/42.61 % (236943)CaDiCaL version: 2.1.3 % 296.08/42.61 % (236943)Termination reason: Instruction limit % 296.08/42.61 % (236943)Termination phase: Saturation % 296.08/42.61 % (236943)Time elapsed: 0.005 s % 296.08/42.61 % (236943)Peak memory usage: 89 MB % 296.08/42.61 % (236943)Instructions burned: 4 (million) % 296.08/42.61 % (236944)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3025512007:i=4:doe=on:canc=force:asg=cautious:rtra=on_2598 on theBenchmark for (2598ds/4Mi) % 296.08/42.61 % (236946)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3030454309:i=254:doe=on:rtra=on_2598 on theBenchmark for (2598ds/254Mi) % 296.08/42.61 % (236944)Instruction limit reached! % 296.08/42.61 % (236944)------------------------------ % 296.08/42.61 % (236944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.08/42.61 % (236944)CaDiCaL version: 2.1.3 % 296.08/42.61 % (236944)Termination reason: Instruction limit % 296.08/42.61 % (236944)Termination phase: Saturation % 296.08/42.61 % (236944)Time elapsed: 0.006 s % 296.08/42.61 % (236944)Peak memory usage: 89 MB % 296.08/42.61 % (236944)Instructions burned: 4 (million) % 296.08/42.61 % (236948)dis+10_1_si=on:random_seed=1008717472:i=20:ep=R:rtra=on_2597 on theBenchmark for (2597ds/20Mi) % 296.08/42.61 % (236948)Instruction limit reached! % 296.08/42.61 % (236948)------------------------------ % 296.08/42.61 % (236948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.08/42.61 % (236948)CaDiCaL version: 2.1.3 % 296.08/42.61 % (236948)Termination reason: Instruction limit % 296.08/42.61 % (236948)Termination phase: Saturation % 296.08/42.61 % (236948)Time elapsed: 0.021 s % 296.08/42.61 % (236948)Peak memory usage: 88 MB % 296.08/42.61 % (236948)Instructions burned: 20 (million) % 296.08/42.61 % (236951)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1162650976:i=52:canc=cautious:av=off:rtra=on_2596 on theBenchmark for (2596ds/52Mi) % 296.08/42.61 % (236951)Refutation not found, incomplete strategy % 296.08/42.61 % (236951)------------------------------ % 296.08/42.61 % (236951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.08/42.61 % (236951)CaDiCaL version: 2.1.3 % 296.08/42.61 % (236951)Termination reason: Refutation not found, incomplete strategy % 296.08/42.61 % (236951)Time elapsed: 0.005 s % 296.08/42.61 % (236951)Peak memory usage: 89 MB % 296.08/42.61 % (236951)Instructions burned: 3 (million) % 296.08/42.61 % (236946)Instruction limit reached! % 296.08/42.61 % (236946)------------------------------ % 296.08/42.61 % (236946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.08/42.61 % (236946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa7Terminated %------------------------------------------------------------------------------