%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC463_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n015.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:59 PM UTC 2026 % Result : Timeout 288.35s 41.52s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC463_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.20 % Computer : n015.cluster.edu % 0.07/0.20 % Model : x86_64 x86_64 % 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.20 % Memory : 8046.5625MB % 0.07/0.20 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 09:42:47 UTC 2026 % 0.07/0.21 % CPUTime : % 0.07/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.24 Running first-order theorem proving % 0.07/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.22/1.60 % (2506002)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.22/1.60 % (2506040)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2607447588:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.22/1.60 % (2506046)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3472939581:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.22/1.60 % (2506037)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=99095518:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.22/1.60 % (2506038)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=73647288:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.22/1.60 % (2506046)Instruction limit reached! % 5.22/1.60 % (2506046)------------------------------ % 5.22/1.60 % (2506046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.22/1.60 % (2506046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.22/1.60 % (2506046)CaDiCaL version: 2.1.3 % 5.22/1.60 % (2506046)Termination reason: Instruction limit % 5.22/1.60 % (2506046)Termination phase: Saturation % 5.22/1.60 % (2506046)Time elapsed: 0.048 s % 5.22/1.60 % (2506046)Peak memory usage: 116 MB % 5.22/1.60 % (2506046)Instructions burned: 33 (million) % 5.22/1.60 % (2506037)Instruction limit reached! % 5.22/1.60 % (2506037)------------------------------ % 5.22/1.60 % (2506037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.22/1.60 % (2506037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.22/1.60 % (2506037)CaDiCaL version: 2.1.3 % 5.22/1.60 % (2506037)Termination reason: Instruction limit % 5.22/1.60 % (2506037)Termination phase: Saturation % 5.22/1.60 % (2506037)Time elapsed: 0.041 s % 5.22/1.60 % (2506037)Peak memory usage: 115 MB % 5.22/1.60 % (2506037)Instructions burned: 13 (million) % 5.22/1.60 % (2506040)Instruction limit reached! % 5.22/1.60 % (2506040)------------------------------ % 5.22/1.60 % (2506040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.22/1.60 % (2506040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.22/1.60 % (2506040)CaDiCaL version: 2.1.3 % 5.22/1.60 % (2506040)Termination reason: Instruction limit % 5.22/1.60 % (2506040)Termination phase: Saturation % 5.22/1.60 % (2506040)Time elapsed: 0.112 s % 5.22/1.60 % (2506040)Peak memory usage: 118 MB % 5.22/1.60 % (2506040)Instructions burned: 203 (million) % 5.22/1.60 % (2506041)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2044346445:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.22/1.60 % (2506043)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4036819799:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.22/1.60 % (2506041)Instruction limit reached! % 5.22/1.60 % (2506041)------------------------------ % 5.22/1.60 % (2506041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.22/1.60 % (2506041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.22/1.60 % (2506041)CaDiCaL version: 2.1.3 % 5.22/1.60 % (2506041)Termination reason: Instruction limit % 5.22/1.60 % (2506041)Termination phase: Saturation % 5.22/1.60 % (2506041)Time elapsed: 0.009 s % 5.22/1.60 % (2506041)Peak memory usage: 88 MB % 5.22/1.60 % (2506041)Instructions burned: 7 (million) % 5.22/1.60 % (2506043)Instruction limit reached! % 5.22/1.60 % (2506043)------------------------------ % 5.22/1.60 % (2506043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.22/1.60 % (2506043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.22/1.60 % (2506043)CaDiCaL version: 2.1.3 % 5.22/1.60 % (2506043)Termination reason: Instruction limit % 5.22/1.60 % (2506043)Termination phase: Saturation % 5.22/1.60 % (2506043)Time elapsed: 0.008 s % 5.22/1.60 % (2506043)Peak memory usage: 89 MB % 5.22/1.60 % (2506043)Instructions burned: 7 (million) % 5.22/1.60 % (2506045)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2520372699:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.22/1.60 % (2506045)Instruction limit reached! % 5.22/1.60 % (2506045)------------------------------ % 5.22/1.60 % (2506045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.22/1.60 % (2506045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.93 % (2506045)CaDiCaL version: 2.1.3 % 7.27/1.93 % (2506045)Termination reason: Instruction limit % 7.27/1.93 % (2506045)Termination phase: Saturation % 7.27/1.93 % (2506045)Time elapsed: 0.078 s % 7.27/1.93 % (2506045)Peak memory usage: 115 MB % 7.27/1.93 % (2506045)Instructions burned: 47 (million) % 7.27/1.93 % (2506061)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=261759515:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 7.27/1.93 % (2506067)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=3785967356:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 7.27/1.93 % (2506061)Instruction limit reached! % 7.27/1.93 % (2506061)------------------------------ % 7.27/1.93 % (2506061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.27/1.93 % (2506061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.93 % (2506061)CaDiCaL version: 2.1.3 % 7.27/1.93 % (2506061)Termination reason: Instruction limit % 7.27/1.93 % (2506061)Termination phase: Saturation % 7.27/1.93 % (2506061)Time elapsed: 0.008 s % 7.27/1.93 % (2506061)Peak memory usage: 88 MB % 7.27/1.93 % (2506061)Instructions burned: 15 (million) % 7.27/1.93 % (2506067)Instruction limit reached! % 7.27/1.93 % (2506067)------------------------------ % 7.27/1.93 % (2506067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.27/1.93 % (2506067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.93 % (2506067)CaDiCaL version: 2.1.3 % 7.27/1.93 % (2506067)Termination reason: Instruction limit % 7.27/1.93 % (2506067)Termination phase: Saturation % 7.27/1.93 % (2506067)Time elapsed: 0.024 s % 7.27/1.93 % (2506067)Peak memory usage: 89 MB % 7.27/1.93 % (2506067)Instructions burned: 29 (million) % 7.27/1.93 % (2506038)Instruction limit reached! % 7.27/1.93 % (2506038)------------------------------ % 7.27/1.93 % (2506038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.27/1.93 % (2506038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.93 % (2506038)CaDiCaL version: 2.1.3 % 7.27/1.93 % (2506038)Termination reason: Instruction limit % 7.27/1.93 % (2506038)Termination phase: Saturation % 7.27/1.93 % (2506038)Time elapsed: 0.302 s % 7.27/1.93 % (2506038)Peak memory usage: 117 MB % 7.27/1.93 % (2506038)Instructions burned: 308 (million) % 7.27/1.93 % (2506071)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1635933946:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 7.27/1.93 % (2506068)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2855153883:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 7.27/1.93 % (2506071)Instruction limit reached! % 7.27/1.93 % (2506071)------------------------------ % 7.27/1.93 % (2506071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.27/1.93 % (2506071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.93 % (2506071)CaDiCaL version: 2.1.3 % 7.27/1.93 % (2506071)Termination reason: Instruction limit % 7.27/1.93 % (2506071)Termination phase: Saturation % 7.27/1.93 % (2506071)Time elapsed: 0.021 s % 7.27/1.93 % (2506071)Peak memory usage: 89 MB % 7.27/1.93 % (2506071)Instructions burned: 25 (million) % 7.27/1.93 % (2506072)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=2087922507:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 7.27/1.93 % (2506068)Instruction limit reached! % 7.27/1.93 % (2506068)------------------------------ % 7.27/1.93 % (2506068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.27/1.93 % (2506068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.93 % (2506068)CaDiCaL version: 2.1.3 % 7.27/1.93 % (2506068)Termination reason: Instruction limit % 7.27/1.93 % (2506068)Termination phase: Saturation % 7.27/1.93 % (2506068)Time elapsed: 0.016 s % 7.27/1.93 % (2506068)Peak memory usage: 90 MB % 7.27/1.93 % (2506068)Instructions burned: 16 (million) % 7.27/1.93 % (2506072)Instruction limit reached! % 7.27/1.93 % (2506072)------------------------------ % 7.27/1.93 % (2506072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.27/1.93 % (2506072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.20 % (2506072)CaDiCaL version: 2.1.3 % 10.28/2.20 % (2506072)Termination reason: Instruction limit % 10.28/2.20 % (2506072)Termination phase: Saturation % 10.28/2.20 % (2506072)Time elapsed: 0.025 s % 10.28/2.20 % (2506072)Peak memory usage: 89 MB % 10.28/2.20 % (2506072)Instructions burned: 28 (million) % 10.28/2.20 % (2506076)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4076637513:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 10.28/2.20 % (2506083)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=733898632:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 10.28/2.20 % (2506083)Instruction limit reached! % 10.28/2.20 % (2506083)------------------------------ % 10.28/2.20 % (2506083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.20 % (2506083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.20 % (2506083)CaDiCaL version: 2.1.3 % 10.28/2.20 % (2506083)Termination reason: Instruction limit % 10.28/2.20 % (2506083)Termination phase: Saturation % 10.28/2.20 % (2506083)Time elapsed: 0.002 s % 10.28/2.20 % (2506083)Peak memory usage: 88 MB % 10.28/2.20 % (2506083)Instructions burned: 2 (million) % 10.28/2.20 % (2506093)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3759533378:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 10.28/2.20 % (2506076)Instruction limit reached! % 10.28/2.20 % (2506076)------------------------------ % 10.28/2.20 % (2506076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.20 % (2506076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.20 % (2506076)CaDiCaL version: 2.1.3 % 10.28/2.20 % (2506076)Termination reason: Instruction limit % 10.28/2.20 % (2506076)Termination phase: Saturation % 10.28/2.20 % (2506076)Time elapsed: 0.074 s % 10.28/2.20 % (2506076)Peak memory usage: 89 MB % 10.28/2.20 % (2506076)Instructions burned: 85 (million) % 10.28/2.20 % (2506085)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2863603654:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 10.28/2.20 % (2506085)Refutation not found, incomplete strategy % 10.28/2.20 % (2506085)------------------------------ % 10.28/2.20 % (2506085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.20 % (2506085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.20 % (2506085)CaDiCaL version: 2.1.3 % 10.28/2.20 % (2506085)Termination reason: Refutation not found, incomplete strategy % 10.28/2.20 % (2506085)Time elapsed: 0.005 s % 10.28/2.20 % (2506085)Peak memory usage: 89 MB % 10.28/2.20 % (2506085)Instructions burned: 2 (million) % 10.28/2.20 % (2506089)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4275737916:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 10.28/2.20 % (2506089)Instruction limit reached! % 10.28/2.20 % (2506089)------------------------------ % 10.28/2.20 % (2506089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.20 % (2506089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.20 % (2506089)CaDiCaL version: 2.1.3 % 10.28/2.20 % (2506089)Termination reason: Instruction limit % 10.28/2.20 % (2506089)Termination phase: Saturation % 10.28/2.20 % (2506089)Time elapsed: 0.006 s % 10.28/2.20 % (2506089)Peak memory usage: 88 MB % 10.28/2.20 % (2506089)Instructions burned: 4 (million) % 10.28/2.20 % (2506093)Instruction limit reached! % 10.28/2.20 % (2506093)------------------------------ % 10.28/2.20 % (2506093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.20 % (2506093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.20 % (2506093)CaDiCaL version: 2.1.3 % 10.28/2.20 % (2506093)Termination reason: Instruction limit % 10.28/2.20 % (2506093)Termination phase: Saturation % 10.28/2.20 % (2506093)Time elapsed: 0.114 s % 10.28/2.20 % (2506093)Peak memory usage: 133 MB % 10.28/2.20 % (2506093)Instructions burned: 66 (million) % 10.28/2.20 % (2506095)lrs+10_1_thi=all:si=on:fd=off:random_seed=1335494141:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 10.28/2.20 % (2506098)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=1947095554:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 10.28/2.20 % (2506098)Instruction limit reached! % 11.76/2.51 % (2506098)------------------------------ % 11.76/2.51 % (2506098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.76/2.51 % (2506098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.76/2.51 % (2506098)CaDiCaL version: 2.1.3 % 11.76/2.51 % (2506098)Termination reason: Instruction limit % 11.76/2.51 % (2506098)Termination phase: Saturation % 11.76/2.51 % (2506098)Time elapsed: 0.011 s % 11.76/2.51 % (2506098)Peak memory usage: 88 MB % 11.76/2.51 % (2506098)Instructions burned: 8 (million) % 11.76/2.51 % (2506104)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=337773647:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 11.76/2.51 % (2506095)Instruction limit reached! % 11.76/2.51 % (2506095)------------------------------ % 11.76/2.51 % (2506095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.76/2.51 % (2506095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.76/2.51 % (2506095)CaDiCaL version: 2.1.3 % 11.76/2.51 % (2506095)Termination reason: Instruction limit % 11.76/2.51 % (2506095)Termination phase: Saturation % 11.76/2.51 % (2506095)Time elapsed: 0.101 s % 11.76/2.51 % (2506095)Peak memory usage: 116 MB % 11.76/2.51 % (2506095)Instructions burned: 53 (million) % 11.76/2.51 % (2506104)Instruction limit reached! % 11.76/2.51 % (2506104)------------------------------ % 11.76/2.51 % (2506104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.76/2.51 % (2506104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.76/2.51 % (2506104)CaDiCaL version: 2.1.3 % 11.76/2.51 % (2506104)Termination reason: Instruction limit % 11.76/2.51 % (2506104)Termination phase: Saturation % 11.76/2.51 % (2506104)Time elapsed: 0.004 s % 11.76/2.51 % (2506104)Peak memory usage: 88 MB % 11.76/2.51 % (2506104)Instructions burned: 2 (million) % 11.76/2.51 % (2506085)------------------------------ % 11.76/2.51 % (2506085)------------------------------ % 11.76/2.51 % (2506108)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=738580802:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 11.76/2.51 % (2506108)Instruction limit reached! % 11.76/2.51 % (2506108)------------------------------ % 11.76/2.51 % (2506108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.76/2.51 % (2506108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.76/2.51 % (2506108)CaDiCaL version: 2.1.3 % 11.76/2.51 % (2506108)Termination reason: Instruction limit % 11.76/2.51 % (2506108)Termination phase: Saturation % 11.76/2.51 % (2506108)Time elapsed: 0.003 s % 11.76/2.51 % (2506108)Peak memory usage: 88 MB % 11.76/2.51 % (2506108)Instructions burned: 2 (million) % 11.76/2.51 % (2506114)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1968473123:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 11.76/2.51 % (2506119)dis+10_1_si=on:random_seed=3897838235:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 11.76/2.51 % (2506119)Instruction limit reached! % 11.76/2.51 % (2506119)------------------------------ % 11.76/2.51 % (2506119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.76/2.51 % (2506119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.76/2.51 % (2506119)CaDiCaL version: 2.1.3 % 11.76/2.51 % (2506119)Termination reason: Instruction limit % 11.76/2.51 % (2506119)Termination phase: Saturation % 11.76/2.51 % (2506119)Time elapsed: 0.012 s % 11.76/2.51 % (2506119)Peak memory usage: 88 MB % 11.76/2.51 % (2506119)Instructions burned: 10 (million) % 11.76/2.51 % (2506121)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3639687109:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 11.76/2.51 % (2506121)Refutation not found, incomplete strategy % 11.76/2.51 % (2506121)------------------------------ % 11.76/2.51 % (2506121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.76/2.51 % (2506121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.76/2.51 % (2506121)CaDiCaL version: 2.1.3 % 11.76/2.51 % (2506121)Termination reason: Refutation not found, incomplete strategy % 11.76/2.51 % (2506121)Time elapsed: 0.005 s % 11.76/2.51 % (2506121)Peak memory usage: 89 MB % 11.76/2.51 % (2506121)Instructions burned: 3 (million) % 11.76/2.51 % (2506131)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3010040277:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 11.76/2.51 % (2506126)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=261067196:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 13.40/2.97 % (2506125)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3781867072: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_2990 on theBenchmark for (2990ds/35Mi) % 13.40/2.97 % (2506126)Instruction limit reached! % 13.40/2.97 % (2506126)------------------------------ % 13.40/2.97 % (2506126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.97 % (2506126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.97 % (2506126)CaDiCaL version: 2.1.3 % 13.40/2.97 % (2506126)Termination reason: Instruction limit % 13.40/2.97 % (2506126)Termination phase: Saturation % 13.40/2.97 % (2506126)Time elapsed: 0.003 s % 13.40/2.97 % (2506126)Peak memory usage: 89 MB % 13.40/2.97 % (2506126)Instructions burned: 3 (million) % 13.40/2.97 % (2506127)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4144148911:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 13.40/2.97 % (2506114)Instruction limit reached! % 13.40/2.97 % (2506114)------------------------------ % 13.40/2.97 % (2506114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.97 % (2506114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.97 % (2506114)CaDiCaL version: 2.1.3 % 13.40/2.97 % (2506114)Termination reason: Instruction limit % 13.40/2.97 % (2506114)Termination phase: Saturation % 13.40/2.97 % (2506114)Time elapsed: 0.168 s % 13.40/2.97 % (2506114)Peak memory usage: 116 MB % 13.40/2.97 % (2506114)Instructions burned: 128 (million) % 13.40/2.97 % (2506127)Instruction limit reached! % 13.40/2.97 % (2506127)------------------------------ % 13.40/2.97 % (2506127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.97 % (2506127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.97 % (2506127)CaDiCaL version: 2.1.3 % 13.40/2.97 % (2506127)Termination reason: Instruction limit % 13.40/2.97 % (2506127)Termination phase: Saturation % 13.40/2.97 % (2506127)Time elapsed: 0.010 s % 13.40/2.97 % (2506127)Peak memory usage: 88 MB % 13.40/2.97 % (2506127)Instructions burned: 9 (million) % 13.40/2.97 % (2506125)Instruction limit reached! % 13.40/2.97 % (2506125)------------------------------ % 13.40/2.97 % (2506125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.97 % (2506125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.97 % (2506125)CaDiCaL version: 2.1.3 % 13.40/2.97 % (2506125)Termination reason: Instruction limit % 13.40/2.97 % (2506125)Termination phase: Saturation % 13.40/2.97 % (2506125)Time elapsed: 0.038 s % 13.40/2.97 % (2506125)Peak memory usage: 89 MB % 13.40/2.97 % (2506125)Instructions burned: 35 (million) % 13.40/2.97 % (2506131)Instruction limit reached! % 13.40/2.97 % (2506131)------------------------------ % 13.40/2.97 % (2506131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.97 % (2506131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.97 % (2506131)CaDiCaL version: 2.1.3 % 13.40/2.97 % (2506131)Termination reason: Instruction limit % 13.40/2.97 % (2506131)Termination phase: Saturation % 13.40/2.97 % (2506131)Time elapsed: 0.157 s % 13.40/2.97 % (2506131)Peak memory usage: 91 MB % 13.40/2.97 % (2506131)Instructions burned: 373 (million) % 13.40/2.97 % (2506139)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=726643977:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi) % 13.40/2.97 % (2506145)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3283102894:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 13.40/2.97 % (2506139)Instruction limit reached! % 13.40/2.97 % (2506139)------------------------------ % 13.40/2.97 % (2506139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.97 % (2506139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.97 % (2506139)CaDiCaL version: 2.1.3 % 13.40/2.97 % (2506139)Termination reason: Instruction limit % 13.40/2.97 % (2506139)Termination phase: Saturation % 13.40/2.97 % (2506139)Time elapsed: 0.047 s % 13.40/2.97 % (2506139)Peak memory usage: 116 MB % 13.40/2.97 % (2506139)Instructions burned: 13 (million) % 13.40/2.97 % (2506146)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2452267129:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 17.21/3.37 % (2506145)Refutation not found, incomplete strategy % 17.21/3.37 % (2506145)------------------------------ % 17.21/3.37 % (2506145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.21/3.37 % (2506145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.21/3.37 % (2506145)CaDiCaL version: 2.1.3 % 17.21/3.37 % (2506145)Termination reason: Refutation not found, incomplete strategy % 17.21/3.37 % (2506145)Time elapsed: 0.039 s % 17.21/3.37 % (2506145)Peak memory usage: 115 MB % 17.21/3.37 % (2506145)Instructions burned: 7 (million) % 17.21/3.37 % (2506146)Instruction limit reached! % 17.21/3.37 % (2506146)------------------------------ % 17.21/3.37 % (2506146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.21/3.37 % (2506146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.21/3.37 % (2506146)CaDiCaL version: 2.1.3 % 17.21/3.37 % (2506146)Termination reason: Instruction limit % 17.21/3.37 % (2506146)Termination phase: Saturation % 17.21/3.37 % (2506146)Time elapsed: 0.009 s % 17.21/3.37 % (2506146)Peak memory usage: 88 MB % 17.21/3.37 % (2506146)Instructions burned: 10 (million) % 17.21/3.37 % (2506147)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=397835250:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 17.21/3.37 % (2506149)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=3231725641:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 17.21/3.37 % (2506121)------------------------------ % 17.21/3.37 % (2506121)------------------------------ % 17.21/3.37 % (2506154)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=2396681460:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi) % 17.21/3.37 % (2506149)Instruction limit reached! % 17.21/3.37 % (2506149)------------------------------ % 17.21/3.37 % (2506149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.21/3.37 % (2506149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.21/3.37 % (2506149)CaDiCaL version: 2.1.3 % 17.21/3.37 % (2506149)Termination reason: Instruction limit % 17.21/3.37 % (2506149)Termination phase: Saturation % 17.21/3.37 % (2506149)Time elapsed: 0.074 s % 17.21/3.37 % (2506149)Peak memory usage: 90 MB % 17.21/3.37 % (2506149)Instructions burned: 75 (million) % 17.21/3.37 % (2506147)Instruction limit reached! % 17.21/3.37 % (2506147)------------------------------ % 17.21/3.37 % (2506147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.21/3.37 % (2506147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.21/3.37 % (2506147)CaDiCaL version: 2.1.3 % 17.21/3.37 % (2506147)Termination reason: Instruction limit % 17.21/3.37 % (2506147)Termination phase: Saturation % 17.21/3.37 % (2506147)Time elapsed: 0.138 s % 17.21/3.37 % (2506147)Peak memory usage: 133 MB % 17.21/3.37 % (2506147)Instructions burned: 71 (million) % 17.21/3.37 % (2506162)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2440476000:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 17.21/3.37 % (2506154)Instruction limit reached! % 17.21/3.37 % (2506154)------------------------------ % 17.21/3.37 % (2506154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.21/3.37 % (2506154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.21/3.37 % (2506154)CaDiCaL version: 2.1.3 % 17.21/3.37 % (2506154)Termination reason: Instruction limit % 17.21/3.37 % (2506154)Termination phase: Saturation % 17.21/3.37 % (2506154)Time elapsed: 0.148 s % 17.21/3.37 % (2506154)Peak memory usage: 90 MB % 17.21/3.37 % (2506154)Instructions burned: 296 (million) % 17.21/3.37 % (2506161)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3979774661:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi) % 17.21/3.37 % (2506162)Instruction limit reached! % 17.21/3.37 % (2506162)------------------------------ % 17.21/3.37 % (2506162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.21/3.37 % (2506162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.21/3.37 % (2506162)CaDiCaL version: 2.1.3 % 17.21/3.37 % (2506162)Termination reason: Instruction limit % 19.89/3.86 % (2506162)Termination phase: Saturation % 19.89/3.86 % (2506162)Time elapsed: 0.124 s % 19.89/3.86 % (2506162)Peak memory usage: 133 MB % 19.89/3.86 % (2506162)Instructions burned: 133 (million) % 19.89/3.86 % (2506167)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3145205602:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 19.89/3.86 % (2506145)------------------------------ % 19.89/3.86 % (2506145)------------------------------ % 19.89/3.86 % (2506173)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2660718344:i=307:rtra=on:gtg=exists_top_2983 on theBenchmark for (2983ds/307Mi) % 19.89/3.86 % (2506161)Instruction limit reached! % 19.89/3.86 % (2506161)------------------------------ % 19.89/3.86 % (2506161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.89/3.86 % (2506161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.89/3.86 % (2506161)CaDiCaL version: 2.1.3 % 19.89/3.86 % (2506161)Termination reason: Instruction limit % 19.89/3.86 % (2506161)Termination phase: Saturation % 19.89/3.86 % (2506161)Time elapsed: 0.149 s % 19.89/3.86 % (2506161)Peak memory usage: 116 MB % 19.89/3.86 % (2506161)Instructions burned: 131 (million) % 19.89/3.86 % (2506174)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1814329379:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 19.89/3.86 % (2506178)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2253065267:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 19.89/3.86 % (2506167)Instruction limit reached! % 19.89/3.86 % (2506167)------------------------------ % 19.89/3.86 % (2506167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.89/3.86 % (2506167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.89/3.86 % (2506167)CaDiCaL version: 2.1.3 % 19.89/3.86 % (2506167)Termination reason: Instruction limit % 19.89/3.86 % (2506167)Termination phase: Saturation % 19.89/3.86 % (2506167)Time elapsed: 0.103 s % 19.89/3.86 % (2506167)Peak memory usage: 134 MB % 19.89/3.86 % (2506167)Instructions burned: 40 (million) % 19.89/3.86 % (2506184)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=1273398973:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 19.89/3.86 % (2506178)Instruction limit reached! % 19.89/3.86 % (2506178)------------------------------ % 19.89/3.86 % (2506178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.89/3.86 % (2506178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.89/3.86 % (2506178)CaDiCaL version: 2.1.3 % 19.89/3.86 % (2506178)Termination reason: Instruction limit % 19.89/3.86 % (2506178)Termination phase: Saturation % 19.89/3.86 % (2506178)Time elapsed: 0.094 s % 19.89/3.86 % (2506178)Peak memory usage: 117 MB % 19.89/3.86 % (2506178)Instructions burned: 132 (million) % 19.89/3.86 % (2506187)dis+10_1_si=on:random_seed=2325300259:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 19.89/3.86 % (2506173)Instruction limit reached! % 19.89/3.86 % (2506173)------------------------------ % 19.89/3.86 % (2506173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.89/3.86 % (2506173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.89/3.86 % (2506173)CaDiCaL version: 2.1.3 % 19.89/3.86 % (2506173)Termination reason: Instruction limit % 19.89/3.86 % (2506173)Termination phase: Saturation % 19.89/3.86 % (2506173)Time elapsed: 0.288 s % 19.89/3.86 % (2506173)Peak memory usage: 92 MB % 19.89/3.86 % (2506173)Instructions burned: 307 (million) % 19.89/3.86 % (2506191)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2129211598:i=383:fsr=off:rtra=on:ev=force_2980 on theBenchmark for (2980ds/383Mi) % 19.89/3.86 % (2506184)Instruction limit reached! % 19.89/3.86 % (2506184)------------------------------ % 19.89/3.86 % (2506184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.89/3.86 % (2506184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.89/3.86 % (2506184)CaDiCaL version: 2.1.3 % 19.89/3.86 % (2506184)Termination reason: Instruction limit % 19.89/3.86 % (2506184)Termination phase: Saturation % 19.89/3.86 % (2506184)Time elapsed: 0.228 s % 19.89/3.86 % (2506184)Peak memory usage: 116 MB % 19.89/3.86 % (2506184)Instructions burned: 260 (million) % 24.55/4.36 % (2506196)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3009300356:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 24.55/4.36 % (2506174)Instruction limit reached! % 24.55/4.36 % (2506174)------------------------------ % 24.55/4.36 % (2506174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.55/4.36 % (2506174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.55/4.36 % (2506174)CaDiCaL version: 2.1.3 % 24.55/4.36 % (2506174)Termination reason: Instruction limit % 24.55/4.36 % (2506174)Termination phase: Saturation % 24.55/4.36 % (2506174)Time elapsed: 0.373 s % 24.55/4.36 % (2506174)Peak memory usage: 137 MB % 24.55/4.36 % (2506174)Instructions burned: 599 (million) % 24.55/4.36 % (2506199)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3394954842:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 24.55/4.36 % (2506199)Refutation not found, incomplete strategy % 24.55/4.36 % (2506199)------------------------------ % 24.55/4.36 % (2506199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.55/4.36 % (2506199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.55/4.36 % (2506199)CaDiCaL version: 2.1.3 % 24.55/4.36 % (2506199)Termination reason: Refutation not found, incomplete strategy % 24.55/4.36 % (2506199)Time elapsed: 0.043 s % 24.55/4.36 % (2506199)Peak memory usage: 115 MB % 24.55/4.36 % (2506199)Instructions burned: 8 (million) % 24.55/4.36 % (2506196)Instruction limit reached! % 24.55/4.36 % (2506196)------------------------------ % 24.55/4.36 % (2506196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.55/4.36 % (2506196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.55/4.36 % (2506196)CaDiCaL version: 2.1.3 % 24.55/4.36 % (2506196)Termination reason: Instruction limit % 24.55/4.36 % (2506196)Termination phase: Saturation % 24.55/4.36 % (2506196)Time elapsed: 0.152 s % 24.55/4.36 % (2506196)Peak memory usage: 90 MB % 24.55/4.36 % (2506196)Instructions burned: 141 (million) % 24.55/4.36 % (2506205)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4216328672:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 24.55/4.36 % (2506212)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=2713591196:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 24.55/4.36 % (2506209)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=2140684821:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 24.55/4.36 % (2506212)Instruction limit reached! % 24.55/4.36 % (2506212)------------------------------ % 24.55/4.36 % (2506212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.55/4.36 % (2506212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.55/4.36 % (2506212)CaDiCaL version: 2.1.3 % 24.55/4.36 % (2506212)Termination reason: Instruction limit % 24.55/4.36 % (2506212)Termination phase: Saturation % 24.55/4.36 % (2506212)Time elapsed: 0.032 s % 24.55/4.36 % (2506212)Peak memory usage: 116 MB % 24.55/4.36 % (2506212)Instructions burned: 39 (million) % 24.55/4.36 % (2506191)Instruction limit reached! % 24.55/4.36 % (2506191)------------------------------ % 24.55/4.36 % (2506191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.55/4.36 % (2506191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.55/4.36 % (2506191)CaDiCaL version: 2.1.3 % 24.55/4.36 % (2506191)Termination reason: Instruction limit % 24.55/4.36 % (2506191)Termination phase: Saturation % 24.55/4.36 % (2506191)Time elapsed: 0.360 s % 24.55/4.36 % (2506191)Peak memory usage: 92 MB % 24.55/4.36 % (2506191)Instructions burned: 383 (million) % 24.55/4.36 % (2506205)Instruction limit reached! % 24.55/4.36 % (2506205)------------------------------ % 24.55/4.36 % (2506205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.55/4.36 % (2506205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.55/4.36 % (2506205)CaDiCaL version: 2.1.3 % 24.55/4.36 % (2506205)Termination reason: Instruction limit % 24.55/4.36 % (2506205)Termination phase: Saturation % 24.55/4.36 % (2506205)Time elapsed: 0.109 s % 24.55/4.36 % (2506205)Peak memory usage: 89 MB % 24.55/4.36 % (2506205)Instructions burned: 121 (million) % 24.55/4.36 % (2506209)Instruction limit reached! % 24.55/4.36 % (2506209)------------------------------ % 24.55/4.36 % (2506209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.85 % (2506209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.85 % (2506209)CaDiCaL version: 2.1.3 % 27.31/4.85 % (2506209)Termination reason: Instruction limit % 27.31/4.85 % (2506209)Termination phase: Saturation % 27.31/4.85 % (2506209)Time elapsed: 0.162 s % 27.31/4.85 % (2506209)Peak memory usage: 117 MB % 27.31/4.85 % (2506209)Instructions burned: 129 (million) % 27.31/4.85 % (2506222)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3478167187:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 27.31/4.85 % (2506215)dis+1010_1_to=kbo:si=on:random_seed=1500746307:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 27.31/4.85 % (2506199)------------------------------ % 27.31/4.85 % (2506199)------------------------------ % 27.31/4.85 % (2506222)Instruction limit reached! % 27.31/4.85 % (2506222)------------------------------ % 27.31/4.85 % (2506222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.85 % (2506222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.85 % (2506222)CaDiCaL version: 2.1.3 % 27.31/4.85 % (2506222)Termination reason: Instruction limit % 27.31/4.85 % (2506222)Termination phase: Saturation % 27.31/4.85 % (2506222)Time elapsed: 0.175 s % 27.31/4.85 % (2506222)Peak memory usage: 118 MB % 27.31/4.85 % (2506222)Instructions burned: 329 (million) % 27.31/4.85 % (2506224)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=78393438:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 27.31/4.85 % (2506225)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1431178716:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 27.31/4.85 % (2506215)Instruction limit reached! % 27.31/4.85 % (2506215)------------------------------ % 27.31/4.85 % (2506215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.85 % (2506215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.85 % (2506215)CaDiCaL version: 2.1.3 % 27.31/4.85 % (2506215)Termination reason: Instruction limit % 27.31/4.85 % (2506215)Termination phase: Saturation % 27.31/4.85 % (2506215)Time elapsed: 0.206 s % 27.31/4.85 % (2506215)Peak memory usage: 91 MB % 27.31/4.85 % (2506215)Instructions burned: 175 (million) % 27.31/4.85 % (2506229)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2685343805:i=349:rtra=on_2973 on theBenchmark for (2973ds/349Mi) % 27.31/4.85 % (2506229)Refutation not found, incomplete strategy % 27.31/4.85 % (2506229)------------------------------ % 27.31/4.85 % (2506229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.85 % (2506229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.85 % (2506229)CaDiCaL version: 2.1.3 % 27.31/4.85 % (2506229)Termination reason: Refutation not found, incomplete strategy % 27.31/4.85 % (2506229)Time elapsed: 0.043 s % 27.31/4.85 % (2506229)Peak memory usage: 116 MB % 27.31/4.85 % (2506229)Instructions burned: 9 (million) % 27.31/4.85 % (2506235)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=546041107:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 27.31/4.85 % (2506240)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=317286961:i=328:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/328Mi) % 27.31/4.85 % (2506225)Instruction limit reached! % 27.31/4.85 % (2506225)------------------------------ % 27.31/4.85 % (2506225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.85 % (2506225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.85 % (2506225)CaDiCaL version: 2.1.3 % 27.31/4.85 % (2506225)Termination reason: Instruction limit % 27.31/4.85 % (2506225)Termination phase: Saturation % 27.31/4.85 % (2506225)Time elapsed: 0.254 s % 27.31/4.85 % (2506225)Peak memory usage: 135 MB % 27.31/4.85 % (2506225)Instructions burned: 216 (million) % 27.31/4.85 % (2506187)Instruction limit reached! % 27.31/4.85 % (2506187)------------------------------ % 27.31/4.85 % (2506187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.85 % (2506187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.72/5.23 % (2506187)CaDiCaL version: 2.1.3 % 31.72/5.23 % (2506187)Termination reason: Instruction limit % 31.72/5.23 % (2506187)Termination phase: Saturation % 31.72/5.23 % (2506187)Time elapsed: 0.966 s % 31.72/5.23 % (2506187)Peak memory usage: 93 MB % 31.72/5.23 % (2506187)Instructions burned: 1000 (million) % 31.72/5.23 % (2506242)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2794479705:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi) % 31.72/5.23 % (2506240)Instruction limit reached! % 31.72/5.23 % (2506240)------------------------------ % 31.72/5.23 % (2506240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.72/5.23 % (2506240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.72/5.23 % (2506240)CaDiCaL version: 2.1.3 % 31.72/5.23 % (2506240)Termination reason: Instruction limit % 31.72/5.23 % (2506240)Termination phase: Saturation % 31.72/5.23 % (2506240)Time elapsed: 0.184 s % 31.72/5.23 % (2506240)Peak memory usage: 118 MB % 31.72/5.23 % (2506240)Instructions burned: 330 (million) % 31.72/5.23 % (2506235)Instruction limit reached! % 31.72/5.23 % (2506235)------------------------------ % 31.72/5.23 % (2506235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.72/5.23 % (2506235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.72/5.23 % (2506235)CaDiCaL version: 2.1.3 % 31.72/5.23 % (2506235)Termination reason: Instruction limit % 31.72/5.23 % (2506235)Termination phase: Saturation % 31.72/5.23 % (2506235)Time elapsed: 0.269 s % 31.72/5.23 % (2506235)Peak memory usage: 90 MB % 31.72/5.23 % (2506235)Instructions burned: 295 (million) % 31.72/5.23 % (2506229)------------------------------ % 31.72/5.23 % (2506229)------------------------------ % 31.72/5.23 % (2506255)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2274363118:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi) % 31.72/5.23 % (2506253)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3163575394:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/484Mi) % 31.72/5.23 % (2506224)Instruction limit reached! % 31.72/5.23 % (2506224)------------------------------ % 31.72/5.23 % (2506224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.72/5.23 % (2506224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.72/5.23 % (2506224)CaDiCaL version: 2.1.3 % 31.72/5.23 % (2506224)Termination reason: Instruction limit % 31.72/5.23 % (2506224)Termination phase: Saturation % 31.72/5.23 % (2506224)Time elapsed: 0.562 s % 31.72/5.23 % (2506224)Peak memory usage: 135 MB % 31.72/5.23 % (2506224)Instructions burned: 485 (million) % 31.72/5.23 % (2506242)Instruction limit reached! % 31.72/5.23 % (2506242)------------------------------ % 31.72/5.23 % (2506242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.72/5.23 % (2506242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.72/5.23 % (2506242)CaDiCaL version: 2.1.3 % 31.72/5.23 % (2506242)Termination reason: Instruction limit % 31.72/5.23 % (2506242)Termination phase: Saturation % 31.72/5.23 % (2506242)Time elapsed: 0.289 s % 31.72/5.23 % (2506242)Peak memory usage: 117 MB % 31.72/5.23 % (2506242)Instructions burned: 281 (million) % 31.72/5.23 % (2506258)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=700800169:i=416:rtra=on:gtg=position:ss=axioms_2967 on theBenchmark for (2967ds/416Mi) % 31.72/5.23 % (2506258)Refutation not found, incomplete strategy % 31.72/5.23 % (2506258)------------------------------ % 31.72/5.23 % (2506258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.72/5.23 % (2506258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.72/5.23 % (2506258)CaDiCaL version: 2.1.3 % 31.72/5.23 % (2506258)Termination reason: Refutation not found, incomplete strategy % 31.72/5.23 % (2506258)Time elapsed: 0.025 s % 31.72/5.23 % (2506258)Peak memory usage: 116 MB % 31.72/5.23 % (2506258)Instructions burned: 7 (million) % 31.72/5.23 % (2506260)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2957351749:i=471:thf=on:kws=precedence:rtra=on_2966 on theBenchmark for (2966ds/471Mi) % 31.72/5.23 % (2506267)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3615064197:i=375:kws=inv_arity_squared:rtra=on_2965 on theBenchmark for (2965ds/375Mi) % 31.72/5.23 % (2506264)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=4041636165:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 32.45/5.80 % (2506255)Instruction limit reached! % 32.45/5.80 % (2506255)------------------------------ % 32.45/5.80 % (2506255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.45/5.80 % (2506255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.45/5.80 % (2506255)CaDiCaL version: 2.1.3 % 32.45/5.80 % (2506255)Termination reason: Instruction limit % 32.45/5.80 % (2506255)Termination phase: Saturation % 32.45/5.80 % (2506255)Time elapsed: 0.277 s % 32.45/5.80 % (2506255)Peak memory usage: 113 MB % 32.45/5.80 % (2506255)Instructions burned: 321 (million) % 32.45/5.80 % (2506258)------------------------------ % 32.45/5.80 % (2506258)------------------------------ % 32.45/5.80 % (2506268)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3008340556:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi) % 32.45/5.80 % (2506253)Instruction limit reached! % 32.45/5.80 % (2506253)------------------------------ % 32.45/5.80 % (2506253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.45/5.80 % (2506253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.45/5.80 % (2506253)CaDiCaL version: 2.1.3 % 32.45/5.80 % (2506253)Termination reason: Instruction limit % 32.45/5.80 % (2506253)Termination phase: Saturation % 32.45/5.80 % (2506253)Time elapsed: 0.444 s % 32.45/5.80 % (2506253)Peak memory usage: 92 MB % 32.45/5.80 % (2506253)Instructions burned: 484 (million) % 32.45/5.80 % (2506264)Instruction limit reached! % 32.45/5.80 % (2506264)------------------------------ % 32.45/5.80 % (2506264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.45/5.80 % (2506264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.45/5.80 % (2506264)CaDiCaL version: 2.1.3 % 32.45/5.80 % (2506264)Termination reason: Instruction limit % 32.45/5.80 % (2506264)Termination phase: Saturation % 32.45/5.80 % (2506264)Time elapsed: 0.270 s % 32.45/5.80 % (2506264)Peak memory usage: 135 MB % 32.45/5.80 % (2506264)Instructions burned: 277 (million) % 32.45/5.80 % (2506278)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2130723834:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2963 on theBenchmark for (2963ds/513Mi) % 32.45/5.80 % (2506286)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2988295624:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi) % 32.45/5.80 % (2506267)Instruction limit reached! % 32.45/5.80 % (2506267)------------------------------ % 32.45/5.80 % (2506267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.45/5.80 % (2506267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.45/5.80 % (2506267)CaDiCaL version: 2.1.3 % 32.45/5.80 % (2506267)Termination reason: Instruction limit % 32.45/5.80 % (2506267)Termination phase: Saturation % 32.45/5.80 % (2506267)Time elapsed: 0.380 s % 32.45/5.80 % (2506267)Peak memory usage: 118 MB % 32.45/5.80 % (2506267)Instructions burned: 375 (million) % 32.45/5.80 % (2506260)Instruction limit reached! % 32.45/5.80 % (2506260)------------------------------ % 32.45/5.80 % (2506260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.45/5.80 % (2506260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.45/5.80 % (2506260)CaDiCaL version: 2.1.3 % 32.45/5.80 % (2506260)Termination reason: Instruction limit % 32.45/5.80 % (2506260)Termination phase: Saturation % 32.45/5.80 % (2506260)Time elapsed: 0.460 s % 32.45/5.80 % (2506260)Peak memory usage: 119 MB % 32.45/5.80 % (2506260)Instructions burned: 472 (million) % 32.45/5.80 % (2506293)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2498943488:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 32.45/5.80 % (2506292)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3151703049:i=359:rtra=on:gtg=exists_top:ss=axioms_2961 on theBenchmark for (2961ds/359Mi) % 32.45/5.80 % (2506292)Refutation not found, incomplete strategy % 32.45/5.80 % (2506292)------------------------------ % 32.45/5.80 % (2506292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.45/5.80 % (2506292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506292)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506292)Termination reason: Refutation not found, incomplete strategy % 39.82/6.61 % (2506292)Time elapsed: 0.004 s % 39.82/6.61 % (2506292)Peak memory usage: 89 MB % 39.82/6.61 % (2506292)Instructions burned: 2 (million) % 39.82/6.61 % (2506286)Instruction limit reached! % 39.82/6.61 % (2506286)------------------------------ % 39.82/6.61 % (2506286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.82/6.61 % (2506286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506286)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506286)Termination reason: Instruction limit % 39.82/6.61 % (2506286)Termination phase: Saturation % 39.82/6.61 % (2506286)Time elapsed: 0.157 s % 39.82/6.61 % (2506286)Peak memory usage: 134 MB % 39.82/6.61 % (2506286)Instructions burned: 334 (million) % 39.82/6.61 % (2506268)Instruction limit reached! % 39.82/6.61 % (2506268)------------------------------ % 39.82/6.61 % (2506268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.82/6.61 % (2506268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506268)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506268)Termination reason: Instruction limit % 39.82/6.61 % (2506268)Termination phase: Saturation % 39.82/6.61 % (2506268)Time elapsed: 0.439 s % 39.82/6.61 % (2506268)Peak memory usage: 119 MB % 39.82/6.61 % (2506268)Instructions burned: 387 (million) % 39.82/6.61 % (2506302)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1375521442:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.82/6.61 % (2506298)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=1911237806:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/235Mi) % 39.82/6.61 % (2506297)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3368642217:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 39.82/6.61 % (2506297)Refutation not found, incomplete strategy % 39.82/6.61 % (2506297)------------------------------ % 39.82/6.61 % (2506297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.82/6.61 % (2506297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506297)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506297)Termination reason: Refutation not found, incomplete strategy % 39.82/6.61 % (2506297)Time elapsed: 0.043 s % 39.82/6.61 % (2506297)Peak memory usage: 115 MB % 39.82/6.61 % (2506297)Instructions burned: 7 (million) % 39.82/6.61 % (2506302)Instruction limit reached! % 39.82/6.61 % (2506302)------------------------------ % 39.82/6.61 % (2506302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.82/6.61 % (2506302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506302)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506302)Termination reason: Instruction limit % 39.82/6.61 % (2506302)Termination phase: Saturation % 39.82/6.61 % (2506302)Time elapsed: 0.107 s % 39.82/6.61 % (2506302)Peak memory usage: 91 MB % 39.82/6.61 % (2506302)Instructions burned: 275 (million) % 39.82/6.61 % (2506293)Instruction limit reached! % 39.82/6.61 % (2506293)------------------------------ % 39.82/6.61 % (2506293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.82/6.61 % (2506293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506293)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506293)Termination reason: Instruction limit % 39.82/6.61 % (2506293)Termination phase: Saturation % 39.82/6.61 % (2506293)Time elapsed: 0.330 s % 39.82/6.61 % (2506293)Peak memory usage: 118 MB % 39.82/6.61 % (2506293)Instructions burned: 341 (million) % 39.82/6.61 % (2506304)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1692663662:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi) % 39.82/6.61 % (2506278)Instruction limit reached! % 39.82/6.61 % (2506278)------------------------------ % 39.82/6.61 % (2506278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.82/6.61 % (2506278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.82/6.61 % (2506278)CaDiCaL version: 2.1.3 % 39.82/6.61 % (2506278)Termination reason: Instruction limit % 39.82/6.61 % (2506278)Termination phase: Saturation % 39.82/6.61 % (2506278)Time elapsed: 0.543 s % 39.82/6.61 % (2506278)Peak memory usage: 94 MB % 47.36/7.55 % (2506278)Instructions burned: 513 (million) % 47.36/7.55 % (2506292)------------------------------ % 47.36/7.55 % (2506292)------------------------------ % 47.36/7.55 % (2506298)Instruction limit reached! % 47.36/7.55 % (2506298)------------------------------ % 47.36/7.55 % (2506298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.36/7.55 % (2506298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.36/7.55 % (2506298)CaDiCaL version: 2.1.3 % 47.36/7.55 % (2506298)Termination reason: Instruction limit % 47.36/7.55 % (2506298)Termination phase: Saturation % 47.36/7.55 % (2506298)Time elapsed: 0.254 s % 47.36/7.55 % (2506298)Peak memory usage: 116 MB % 47.36/7.55 % (2506298)Instructions burned: 235 (million) % 47.36/7.55 % (2506313)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3256201880:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi) % 47.36/7.55 % (2506304)Instruction limit reached! % 47.36/7.55 % (2506304)------------------------------ % 47.36/7.55 % (2506304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.36/7.55 % (2506304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.36/7.55 % (2506304)CaDiCaL version: 2.1.3 % 47.36/7.55 % (2506304)Termination reason: Instruction limit % 47.36/7.55 % (2506304)Termination phase: Saturation % 47.36/7.55 % (2506304)Time elapsed: 0.151 s % 47.36/7.55 % (2506304)Peak memory usage: 90 MB % 47.36/7.55 % (2506304)Instructions burned: 146 (million) % 47.36/7.55 % (2506314)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=707632113:avsq=on:i=276:avsqr=1,2:rtra=on_2955 on theBenchmark for (2955ds/276Mi) % 47.36/7.55 % (2506297)------------------------------ % 47.36/7.55 % (2506297)------------------------------ % 47.36/7.55 % (2506319)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4233085988:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 47.36/7.55 % (2506320)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=774097451:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/655Mi) % 47.36/7.55 % (2506320)Refutation not found, incomplete strategy % 47.36/7.55 % (2506320)------------------------------ % 47.36/7.55 % (2506320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.36/7.55 % (2506320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.36/7.55 % (2506320)CaDiCaL version: 2.1.3 % 47.36/7.55 % (2506320)Termination reason: Refutation not found, incomplete strategy % 47.36/7.55 % (2506320)Time elapsed: 0.011 s % 47.36/7.55 % (2506320)Peak memory usage: 89 MB % 47.36/7.55 % (2506320)Instructions burned: 8 (million) % 47.36/7.55 % (2506321)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2528253000:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1054Mi) % 47.36/7.55 % (2506321)Refutation not found, incomplete strategy % 47.36/7.55 % (2506321)------------------------------ % 47.36/7.55 % (2506321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.36/7.55 % (2506321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.36/7.55 % (2506321)CaDiCaL version: 2.1.3 % 47.36/7.55 % (2506321)Termination reason: Refutation not found, incomplete strategy % 47.36/7.55 % (2506321)Time elapsed: 0.015 s % 47.36/7.55 % (2506321)Peak memory usage: 89 MB % 47.36/7.55 % (2506321)Instructions burned: 11 (million) % 47.36/7.55 % (2506324)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=4131312220:i=107:rtra=on_2953 on theBenchmark for (2953ds/107Mi) % 47.36/7.55 % (2506324)Refutation not found, incomplete strategy % 47.36/7.55 % (2506324)------------------------------ % 47.36/7.55 % (2506324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.36/7.55 % (2506324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.36/7.55 % (2506324)CaDiCaL version: 2.1.3 % 47.36/7.55 % (2506324)Termination reason: Refutation not found, incomplete strategy % 47.36/7.55 % (2506324)Time elapsed: 0.043 s % 47.36/7.55 % (2506324)Peak memory usage: 116 MB % 47.36/7.55 % (2506324)Instructions burned: 8 (million) % 47.36/7.55 % (2506328)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1809350962:s2a=on:i=450:doe=on:nm=32:rtra=on_2952 on theBenchmark for (2952ds/450Mi) % 47.36/7.55 % (2506314)Instruction limit reached! % 52.96/8.21 % (2506314)------------------------------ % 52.96/8.21 % (2506314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.21 % (2506314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.21 % (2506314)CaDiCaL version: 2.1.3 % 52.96/8.21 % (2506314)Termination reason: Instruction limit % 52.96/8.21 % (2506314)Termination phase: Saturation % 52.96/8.21 % (2506314)Time elapsed: 0.368 s % 52.96/8.21 % (2506314)Peak memory usage: 134 MB % 52.96/8.21 % (2506314)Instructions burned: 276 (million) % 52.96/8.21 % (2506320)------------------------------ % 52.96/8.21 % (2506320)------------------------------ % 52.96/8.21 % (2506321)------------------------------ % 52.96/8.21 % (2506321)------------------------------ % 52.96/8.21 % (2506324)------------------------------ % 52.96/8.21 % (2506324)------------------------------ % 52.96/8.21 % (2506343)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 % 52.96/8.21 % (2506343)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2881485001:i=1090:aac=none:nm=0:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/1090Mi) % 52.96/8.21 % (2506344)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2698838920:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2948 on theBenchmark for (2948ds/130Mi) % 52.96/8.21 % (2506346)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3625444133:i=312:kws=inv_frequency:nm=20:rtra=on_2947 on theBenchmark for (2947ds/312Mi) % 52.96/8.21 % (2506328)Instruction limit reached! % 52.96/8.21 % (2506328)------------------------------ % 52.96/8.21 % (2506328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.21 % (2506328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.21 % (2506328)CaDiCaL version: 2.1.3 % 52.96/8.21 % (2506328)Termination reason: Instruction limit % 52.96/8.21 % (2506328)Termination phase: Saturation % 52.96/8.21 % (2506328)Time elapsed: 0.512 s % 52.96/8.21 % (2506328)Peak memory usage: 135 MB % 52.96/8.21 % (2506328)Instructions burned: 450 (million) % 52.96/8.21 % (2506348)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2262120551:i=491:doe=on:rtra=on:gtg=position_2947 on theBenchmark for (2947ds/491Mi) % 52.96/8.21 % (2506344)Instruction limit reached! % 52.96/8.21 % (2506344)------------------------------ % 52.96/8.21 % (2506344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.21 % (2506344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.21 % (2506344)CaDiCaL version: 2.1.3 % 52.96/8.21 % (2506344)Termination reason: Instruction limit % 52.96/8.21 % (2506344)Termination phase: Saturation % 52.96/8.21 % (2506344)Time elapsed: 0.131 s % 52.96/8.21 % (2506344)Peak memory usage: 116 MB % 52.96/8.21 % (2506344)Instructions burned: 130 (million) % 52.96/8.21 % (2506319)Instruction limit reached! % 52.96/8.21 % (2506319)------------------------------ % 52.96/8.21 % (2506319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.21 % (2506319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.21 % (2506319)CaDiCaL version: 2.1.3 % 52.96/8.21 % (2506319)Termination reason: Instruction limit % 52.96/8.21 % (2506319)Termination phase: Saturation % 52.96/8.21 % (2506319)Time elapsed: 0.939 s % 52.96/8.21 % (2506319)Peak memory usage: 91 MB % 52.96/8.21 % (2506319)Instructions burned: 1053 (million) % 52.96/8.21 % (2506357)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3943625320:s2a=on:i=835:s2at=2:rtra=on_2944 on theBenchmark for (2944ds/835Mi) % 52.96/8.21 % (2506346)Instruction limit reached! % 52.96/8.21 % (2506346)------------------------------ % 52.96/8.21 % (2506346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.21 % (2506346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.21 % (2506346)CaDiCaL version: 2.1.3 % 52.96/8.21 % (2506346)Termination reason: Instruction limit % 52.96/8.21 % (2506346)Termination phase: Saturation % 52.96/8.21 % (2506346)Time elapsed: 0.342 s % 52.96/8.21 % (2506346)Peak memory usage: 118 MB % 52.96/8.21 % (2506346)Instructions burned: 313 (million) % 52.96/8.21 % (2506359)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1890813449:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2944 on theBenchmark for (2944ds/307Mi) % 55.12/8.92 % (2506363)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1863291290:i=776:doe=on:rtra=on_2942 on theBenchmark for (2942ds/776Mi) % 55.12/8.92 % (2506348)Instruction limit reached! % 55.12/8.92 % (2506348)------------------------------ % 55.12/8.92 % (2506348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.12/8.92 % (2506348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.12/8.92 % (2506348)CaDiCaL version: 2.1.3 % 55.12/8.92 % (2506348)Termination reason: Instruction limit % 55.12/8.92 % (2506348)Termination phase: Saturation % 55.12/8.92 % (2506348)Time elapsed: 0.494 s % 55.12/8.92 % (2506348)Peak memory usage: 92 MB % 55.12/8.92 % (2506348)Instructions burned: 491 (million) % 55.12/8.92 % (2506367)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1970746798:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2941 on theBenchmark for (2941ds/646Mi) % 55.12/8.92 % (2506359)Instruction limit reached! % 55.12/8.92 % (2506359)------------------------------ % 55.12/8.92 % (2506359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.12/8.92 % (2506359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.12/8.92 % (2506359)CaDiCaL version: 2.1.3 % 55.12/8.92 % (2506359)Termination reason: Instruction limit % 55.12/8.92 % (2506359)Termination phase: Saturation % 55.12/8.92 % (2506359)Time elapsed: 0.312 s % 55.12/8.92 % (2506359)Peak memory usage: 92 MB % 55.12/8.92 % (2506359)Instructions burned: 307 (million) % 55.12/8.92 % (2506343)Instruction limit reached! % 55.12/8.92 % (2506343)------------------------------ % 55.12/8.92 % (2506343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.12/8.92 % (2506343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.12/8.92 % (2506343)CaDiCaL version: 2.1.3 % 55.12/8.92 % (2506343)Termination reason: Instruction limit % 55.12/8.92 % (2506343)Termination phase: Saturation % 55.12/8.92 % (2506343)Time elapsed: 0.936 s % 55.12/8.92 % (2506343)Peak memory usage: 123 MB % 55.12/8.92 % (2506343)Instructions burned: 1092 (million) % 55.12/8.92 % (2506371)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=1286470318:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2939 on theBenchmark for (2939ds/784Mi) % 55.12/8.92 % (2506375)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=3314853606:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi) % 55.12/8.92 % (2506357)Instruction limit reached! % 55.12/8.92 % (2506357)------------------------------ % 55.12/8.92 % (2506357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.12/8.92 % (2506357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.12/8.92 % (2506357)CaDiCaL version: 2.1.3 % 55.12/8.92 % (2506357)Termination reason: Instruction limit % 55.12/8.92 % (2506357)Termination phase: Saturation % 55.12/8.92 % (2506357)Time elapsed: 0.694 s % 55.12/8.92 % (2506357)Peak memory usage: 93 MB % 55.12/8.92 % (2506357)Instructions burned: 836 (million) % 55.12/8.92 % (2506380)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=69250794:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2936 on theBenchmark for (2936ds/246Mi) % 55.12/8.92 % (2506363)Instruction limit reached! % 55.12/8.92 % (2506363)------------------------------ % 55.12/8.92 % (2506363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.12/8.92 % (2506363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.12/8.92 % (2506363)CaDiCaL version: 2.1.3 % 55.12/8.92 % (2506363)Termination reason: Instruction limit % 55.12/8.92 % (2506363)Termination phase: Saturation % 55.12/8.92 % (2506363)Time elapsed: 0.716 s % 55.12/8.92 % (2506363)Peak memory usage: 121 MB % 55.12/8.92 % (2506363)Instructions burned: 777 (million) % 55.12/8.92 % (2506313)Instruction limit reached! % 55.12/8.92 % (2506313)------------------------------ % 55.12/8.92 % (2506313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.12/8.92 % (2506313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.12/8.92 % (2506313)CaDiCaL version: 2.1.3 % 55.12/8.92 % (2506313)Termination reason: Instruction limit % 55.12/8.92 % (2506313)Termination phase: Saturation % 66.74/10.19 % (2506313)Time elapsed: 2.208 s % 66.74/10.19 % (2506313)Peak memory usage: 113 MB % 66.74/10.19 % (2506313)Instructions burned: 4428 (million) % 66.74/10.19 % (2506386)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=119542321:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/775Mi) % 66.74/10.19 % (2506380)Instruction limit reached! % 66.74/10.19 % (2506380)------------------------------ % 66.74/10.19 % (2506380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.74/10.19 % (2506380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.74/10.19 % (2506380)CaDiCaL version: 2.1.3 % 66.74/10.19 % (2506380)Termination reason: Instruction limit % 66.74/10.19 % (2506380)Termination phase: Saturation % 66.74/10.19 % (2506380)Time elapsed: 0.257 s % 66.74/10.19 % (2506380)Peak memory usage: 116 MB % 66.74/10.19 % (2506380)Instructions burned: 246 (million) % 66.74/10.19 % (2506367)Instruction limit reached! % 66.74/10.19 % (2506367)------------------------------ % 66.74/10.19 % (2506367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.74/10.19 % (2506367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.74/10.19 % (2506367)CaDiCaL version: 2.1.3 % 66.74/10.19 % (2506367)Termination reason: Instruction limit % 66.74/10.19 % (2506367)Termination phase: Saturation % 66.74/10.19 % (2506367)Time elapsed: 0.741 s % 66.74/10.19 % (2506367)Peak memory usage: 137 MB % 66.74/10.19 % (2506367)Instructions burned: 647 (million) % 66.74/10.19 % (2506390)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3282328260:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2932 on theBenchmark for (2932ds/273Mi) % 66.74/10.19 % (2506391)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1041998168:i=102:nm=16:rtra=on_2931 on theBenchmark for (2931ds/102Mi) % 66.74/10.19 % (2506391)Instruction limit reached! % 66.74/10.19 % (2506391)------------------------------ % 66.74/10.19 % (2506391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.74/10.19 % (2506391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.74/10.19 % (2506391)CaDiCaL version: 2.1.3 % 66.74/10.19 % (2506391)Termination reason: Instruction limit % 66.74/10.19 % (2506391)Termination phase: Saturation % 66.74/10.19 % (2506391)Time elapsed: 0.052 s % 66.74/10.19 % (2506391)Peak memory usage: 89 MB % 66.74/10.19 % (2506391)Instructions burned: 103 (million) % 66.74/10.19 % (2506393)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2232599957:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 66.74/10.19 % (2506371)Instruction limit reached! % 66.74/10.19 % (2506371)------------------------------ % 66.74/10.19 % (2506371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.74/10.19 % (2506371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.74/10.19 % (2506371)CaDiCaL version: 2.1.3 % 66.74/10.19 % (2506371)Termination reason: Instruction limit % 66.74/10.19 % (2506371)Termination phase: Saturation % 66.74/10.19 % (2506371)Time elapsed: 0.831 s % 66.74/10.19 % (2506371)Peak memory usage: 121 MB % 66.74/10.19 % (2506371)Instructions burned: 784 (million) % 66.74/10.19 % (2506396)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=400928340:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 66.74/10.19 % (2506390)Instruction limit reached! % 66.74/10.19 % (2506390)------------------------------ % 66.74/10.19 % (2506390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.74/10.19 % (2506390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.74/10.19 % (2506390)CaDiCaL version: 2.1.3 % 66.74/10.19 % (2506390)Termination reason: Instruction limit % 66.74/10.19 % (2506390)Termination phase: Saturation % 66.74/10.19 % (2506390)Time elapsed: 0.239 s % 66.74/10.19 % (2506390)Peak memory usage: 91 MB % 66.74/10.19 % (2506390)Instructions burned: 273 (million) % 66.74/10.19 % (2506400)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=1288468934:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi) % 66.74/10.19 % (2506403)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=112489941:i=1846:canc=cautious:fsr=off:rtra=on_2928 on theBenchmark for (2928ds/1846Mi) % 77.44/11.70 % (2506406)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3276765527:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2927 on theBenchmark for (2927ds/36816Mi) % 77.44/11.70 % (2506406)Refutation not found, incomplete strategy % 77.44/11.70 % (2506406)------------------------------ % 77.44/11.70 % (2506406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.44/11.70 % (2506406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.44/11.70 % (2506406)CaDiCaL version: 2.1.3 % 77.44/11.70 % (2506406)Termination reason: Refutation not found, incomplete strategy % 77.44/11.70 % (2506406)Time elapsed: 0.004 s % 77.44/11.70 % (2506406)Peak memory usage: 88 MB % 77.44/11.70 % (2506406)Instructions burned: 3 (million) % 77.44/11.70 % (2506386)Instruction limit reached! % 77.44/11.70 % (2506386)------------------------------ % 77.44/11.70 % (2506386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.44/11.70 % (2506386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.44/11.70 % (2506386)CaDiCaL version: 2.1.3 % 77.44/11.70 % (2506386)Termination reason: Instruction limit % 77.44/11.70 % (2506386)Termination phase: Saturation % 77.44/11.70 % (2506386)Time elapsed: 0.788 s % 77.44/11.70 % (2506386)Peak memory usage: 94 MB % 77.44/11.70 % (2506386)Instructions burned: 775 (million) % 77.44/11.70 % (2506375)Instruction limit reached! % 77.44/11.70 % (2506375)------------------------------ % 77.44/11.70 % (2506375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.44/11.70 % (2506375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.44/11.70 % (2506375)CaDiCaL version: 2.1.3 % 77.44/11.70 % (2506375)Termination reason: Instruction limit % 77.44/11.70 % (2506375)Termination phase: Saturation % 77.44/11.70 % (2506375)Time elapsed: 1.186 s % 77.44/11.70 % (2506375)Peak memory usage: 122 MB % 77.44/11.70 % (2506375)Instructions burned: 1131 (million) % 77.44/11.70 % (2506400)Instruction limit reached! % 77.44/11.70 % (2506400)------------------------------ % 77.44/11.70 % (2506400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.44/11.70 % (2506400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.44/11.70 % (2506400)CaDiCaL version: 2.1.3 % 77.44/11.70 % (2506400)Termination reason: Instruction limit % 77.44/11.70 % (2506400)Termination phase: Saturation % 77.44/11.70 % (2506400)Time elapsed: 0.458 s % 77.44/11.70 % (2506400)Peak memory usage: 118 MB % 77.44/11.70 % (2506400)Instructions burned: 868 (million) % 77.44/11.70 % (2506417)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1805556735:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/273Mi) % 77.44/11.70 % (2506406)------------------------------ % 77.44/11.70 % (2506406)------------------------------ % 77.44/11.70 % (2506418)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=2083824722:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2922 on theBenchmark for (2922ds/863Mi) % 77.44/11.70 % (2506420)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2060941945:i=5811:kws=precedence:nm=0:rtra=on_2922 on theBenchmark for (2922ds/5811Mi) % 77.44/11.70 % (2506393)Instruction limit reached! % 77.44/11.70 % (2506393)------------------------------ % 77.44/11.70 % (2506393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.44/11.70 % (2506393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.44/11.70 % (2506393)CaDiCaL version: 2.1.3 % 77.44/11.70 % (2506393)Termination reason: Instruction limit % 77.44/11.70 % (2506393)Termination phase: Saturation % 77.44/11.70 % (2506393)Time elapsed: 0.993 s % 77.44/11.70 % (2506393)Peak memory usage: 91 MB % 77.44/11.70 % (2506393)Instructions burned: 1095 (million) % 77.44/11.70 % (2506420)Refutation not found, incomplete strategy % 77.44/11.70 % (2506420)------------------------------ % 77.44/11.70 % (2506420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.44/11.70 % (2506420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.44/11.70 % (2506420)CaDiCaL version: 2.1.3 % 77.44/11.70 % (2506420)Termination reason: Refutation not found, incomplete strategy % 77.44/11.70 % (2506420)Time elapsed: 0.194 s % 77.44/11.70 % (2506420)Peak memory usage: 118 MB % 77.44/11.70 % (2506420)Instructions burned: 370 (million) % 77.44/11.70 % (2506417)Instruction limit reached! % 77.44/11.70 % (2506417)------------------------------ % 77.44/11.70 % (2506417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.60/14.22 % (2506417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.60/14.22 % (2506417)CaDiCaL version: 2.1.3 % 95.60/14.22 % (2506417)Termination reason: Instruction limit % 95.60/14.22 % (2506417)Termination phase: Saturation % 95.60/14.22 % (2506417)Time elapsed: 0.289 s % 95.60/14.22 % (2506417)Peak memory usage: 91 MB % 95.60/14.22 % (2506417)Instructions burned: 273 (million) % 95.60/14.22 % (2506423)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=3818858384:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2920 on theBenchmark for (2920ds/2216Mi) % 95.60/14.22 % (2506420)------------------------------ % 95.60/14.22 % (2506420)------------------------------ % 95.60/14.22 % (2506427)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2828251920:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2918 on theBenchmark for (2918ds/801Mi) % 95.60/14.22 % (2506427)Refutation not found, incomplete strategy % 95.60/14.22 % (2506427)------------------------------ % 95.60/14.22 % (2506427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.60/14.22 % (2506427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.60/14.22 % (2506427)CaDiCaL version: 2.1.3 % 95.60/14.22 % (2506427)Termination reason: Refutation not found, incomplete strategy % 95.60/14.22 % (2506427)Time elapsed: 0.011 s % 95.60/14.22 % (2506427)Peak memory usage: 89 MB % 95.60/14.22 % (2506427)Instructions burned: 8 (million) % 95.60/14.22 % (2506428)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=789348008:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2918 on theBenchmark for (2918ds/1026Mi) % 95.60/14.22 % (2506428)Refutation not found, incomplete strategy % 95.60/14.22 % (2506428)------------------------------ % 95.60/14.22 % (2506428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.60/14.22 % (2506428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.60/14.22 % (2506428)CaDiCaL version: 2.1.3 % 95.60/14.22 % (2506428)Termination reason: Refutation not found, incomplete strategy % 95.60/14.22 % (2506428)Time elapsed: 0.016 s % 95.60/14.22 % (2506428)Peak memory usage: 89 MB % 95.60/14.22 % (2506428)Instructions burned: 11 (million) % 95.60/14.22 % (2506430)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3066341290:i=3509:rtra=on_2915 on theBenchmark for (2915ds/3509Mi) % 95.60/14.22 % (2506418)Instruction limit reached! % 95.60/14.22 % (2506418)------------------------------ % 95.60/14.22 % (2506418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.60/14.22 % (2506418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.60/14.22 % (2506418)CaDiCaL version: 2.1.3 % 95.60/14.22 % (2506418)Termination reason: Instruction limit % 95.60/14.22 % (2506418)Termination phase: Saturation % 95.60/14.22 % (2506418)Time elapsed: 0.765 s % 95.60/14.22 % (2506418)Peak memory usage: 118 MB % 95.60/14.22 % (2506418)Instructions burned: 863 (million) % 95.60/14.22 % (2506427)------------------------------ % 95.60/14.22 % (2506427)------------------------------ % 95.60/14.22 % (2506428)------------------------------ % 95.60/14.22 % (2506428)------------------------------ % 95.60/14.22 % (2506437)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3973343280:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2912 on theBenchmark for (2912ds/2127Mi) % 95.60/14.22 % (2506439)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2290374093:i=1959:rtra=on:fsd=on:proc=on_2911 on theBenchmark for (2911ds/1959Mi) % 95.60/14.22 % (2506403)Instruction limit reached! % 95.60/14.22 % (2506403)------------------------------ % 95.60/14.22 % (2506403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.60/14.22 % (2506403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.60/14.22 % (2506403)CaDiCaL version: 2.1.3 % 95.60/14.22 % (2506403)Termination reason: Instruction limit % 95.60/14.22 % (2506403)Termination phase: Saturation % 95.60/14.22 % (2506403)Time elapsed: 1.671 s % 95.60/14.22 % (2506403)Peak memory usage: 96 MB % 95.60/14.22 % (2506403)Instructions burned: 1846 (million) % 95.60/14.22 % (2506440)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4253058014:s2a=on:i=3553:nm=0:rtra=on_2911 on theBenchmark for (2911ds/3553Mi) % 95.60/14.22 % (2506443)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1769555216:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2908 on theBenchmark for (2908ds/3201Mi) % 131.79/19.34 % (2506443)Refutation not found, incomplete strategy % 131.79/19.34 % (2506443)------------------------------ % 131.79/19.34 % (2506443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.79/19.34 % (2506443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.79/19.34 % (2506443)CaDiCaL version: 2.1.3 % 131.79/19.34 % (2506443)Termination reason: Refutation not found, incomplete strategy % 131.79/19.34 % (2506443)Time elapsed: 0.029 s % 131.79/19.34 % (2506443)Peak memory usage: 90 MB % 131.79/19.34 % (2506443)Instructions burned: 27 (million) % 131.79/19.34 % (2506443)------------------------------ % 131.79/19.34 % (2506443)------------------------------ % 131.79/19.34 % (2506423)Instruction limit reached! % 131.79/19.34 % (2506423)------------------------------ % 131.79/19.34 % (2506423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.79/19.34 % (2506423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.79/19.34 % (2506423)CaDiCaL version: 2.1.3 % 131.79/19.35 % (2506423)Termination reason: Instruction limit % 131.79/19.35 % (2506423)Termination phase: Saturation % 131.79/19.35 % (2506423)Time elapsed: 1.828 s % 131.79/19.35 % (2506423)Peak memory usage: 125 MB % 131.79/19.35 % (2506423)Instructions burned: 2216 (million) % 131.79/19.35 % (2506430)Instruction limit reached! % 131.79/19.35 % (2506430)------------------------------ % 131.79/19.35 % (2506430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.79/19.35 % (2506430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.79/19.35 % (2506430)CaDiCaL version: 2.1.3 % 131.79/19.35 % (2506430)Termination reason: Instruction limit % 131.79/19.35 % (2506430)Termination phase: Saturation % 131.79/19.35 % (2506430)Time elapsed: 1.498 s % 131.79/19.35 % (2506430)Peak memory usage: 98 MB % 131.79/19.35 % (2506430)Instructions burned: 3511 (million) % 131.79/19.35 % (2506451)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=3841988648:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2901 on theBenchmark for (2901ds/4093Mi) % 131.79/19.35 % (2506454)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3880845656:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2898 on theBenchmark for (2898ds/10544Mi) % 131.79/19.35 % (2506453)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=645209747:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2899 on theBenchmark for (2899ds/21173Mi) % 131.79/19.35 % (2506453)Refutation not found, incomplete strategy % 131.79/19.35 % (2506453)------------------------------ % 131.79/19.35 % (2506453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.79/19.35 % (2506453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.79/19.35 % (2506453)CaDiCaL version: 2.1.3 % 131.79/19.35 % (2506453)Termination reason: Refutation not found, incomplete strategy % 131.79/19.35 % (2506453)Time elapsed: 0.080 s % 131.79/19.35 % (2506453)Peak memory usage: 115 MB % 131.79/19.35 % (2506453)Instructions burned: 107 (million) % 131.79/19.35 % (2506437)Instruction limit reached! % 131.79/19.35 % (2506437)------------------------------ % 131.79/19.35 % (2506437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.79/19.35 % (2506437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.79/19.35 % (2506437)CaDiCaL version: 2.1.3 % 131.79/19.35 % (2506437)Termination reason: Instruction limit % 131.79/19.35 % (2506437)Termination phase: Saturation % 131.79/19.35 % (2506437)Time elapsed: 1.702 s % 131.79/19.35 % (2506437)Peak memory usage: 99 MB % 131.79/19.35 % (2506437)Instructions burned: 2127 (million) % 131.79/19.35 % (2506453)------------------------------ % 131.79/19.35 % (2506453)------------------------------ % 131.79/19.35 % (2506439)Instruction limit reached! % 131.79/19.35 % (2506439)------------------------------ % 131.79/19.35 % (2506439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.79/19.35 % (2506439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.79/19.35 % (2506439)CaDiCaL version: 2.1.3 % 131.79/19.35 % (2506439)Termination reason: Instruction limit % 131.79/19.35 % (2506439)Termination phase: Saturation % 131.79/19.35 % (2506439)Time elapsed: 1.834 s % 131.79/19.35 % (2506439)Peak memory usage: 120 MB % 141.26/22.05 % (2506439)Instructions burned: 1960 (million) % 141.26/22.05 % (2506462)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4231635756:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2893 on theBenchmark for (2893ds/1262Mi) % 141.26/22.05 % (2506462)Refutation not found, incomplete strategy % 141.26/22.05 % (2506462)------------------------------ % 141.26/22.05 % (2506462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.26/22.05 % (2506462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.26/22.05 % (2506462)CaDiCaL version: 2.1.3 % 141.26/22.05 % (2506462)Termination reason: Refutation not found, incomplete strategy % 141.26/22.05 % (2506462)Time elapsed: 0.043 s % 141.26/22.05 % (2506462)Peak memory usage: 116 MB % 141.26/22.05 % (2506462)Instructions burned: 9 (million) % 141.26/22.05 % (2506463)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3683216455:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2891 on theBenchmark for (2891ds/775Mi) % 141.26/22.05 % (2506466)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3663650223:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2890 on theBenchmark for (2890ds/270Mi) % 141.26/22.05 % (2506462)------------------------------ % 141.26/22.05 % (2506462)------------------------------ % 141.26/22.05 % (2506466)Instruction limit reached! % 141.26/22.05 % (2506466)------------------------------ % 141.26/22.05 % (2506466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.26/22.05 % (2506466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.26/22.05 % (2506466)CaDiCaL version: 2.1.3 % 141.26/22.05 % (2506466)Termination reason: Instruction limit % 141.26/22.05 % (2506466)Termination phase: Saturation % 141.26/22.05 % (2506466)Time elapsed: 0.296 s % 141.26/22.05 % (2506466)Peak memory usage: 91 MB % 141.26/22.05 % (2506466)Instructions burned: 270 (million) % 141.26/22.05 % (2506470)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2047294444:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2885 on theBenchmark for (2885ds/17165Mi) % 141.26/22.05 % (2506472)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2302860971:s2a=on:i=13094:s2at=-1:rtra=on_2884 on theBenchmark for (2884ds/13094Mi) % 141.26/22.05 % (2506463)Instruction limit reached! % 141.26/22.05 % (2506463)------------------------------ % 141.26/22.05 % (2506463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.26/22.05 % (2506463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.26/22.05 % (2506463)CaDiCaL version: 2.1.3 % 141.26/22.05 % (2506463)Termination reason: Instruction limit % 141.26/22.05 % (2506463)Termination phase: Saturation % 141.26/22.05 % (2506463)Time elapsed: 0.831 s % 141.26/22.05 % (2506463)Peak memory usage: 94 MB % 141.26/22.05 % (2506463)Instructions burned: 775 (million) % 141.26/22.05 % (2506476)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2505363864:st=2:i=12633:rtra=on:ss=axioms_2880 on theBenchmark for (2880ds/12633Mi) % 141.26/22.05 % (2506440)Instruction limit reached! % 141.26/22.05 % (2506440)------------------------------ % 141.26/22.05 % (2506440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.26/22.05 % (2506440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.26/22.05 % (2506440)CaDiCaL version: 2.1.3 % 141.26/22.05 % (2506440)Termination reason: Instruction limit % 141.26/22.05 % (2506440)Termination phase: Saturation % 141.26/22.05 % (2506440)Time elapsed: 3.772 s % 141.26/22.05 % (2506440)Peak memory usage: 106 MB % 141.26/22.05 % (2506440)Instructions burned: 3554 (million) % 141.26/22.05 % (2506396)Instruction limit reached! % 141.26/22.05 % (2506396)------------------------------ % 141.26/22.05 % (2506396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.26/22.05 % (2506396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.26/22.05 % (2506396)CaDiCaL version: 2.1.3 % 141.26/22.05 % (2506396)Termination reason: Instruction limit % 141.26/22.05 % (2506396)Termination phase: Saturation % 141.26/22.05 % (2506396)Time elapsed: 5.964 s % 141.26/22.05 % (2506396)Peak memory usage: 123 MB % 141.26/22.05 % (2506396)Instructions burned: 6400 (million) % 141.26/22.05 % (2506480)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2731597272:i=1783:rtra=on:gtg=position_2870 on theBenchmark for (2870ds/1783Mi) % 141.26/22.05 % (2506481)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=1075307976:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2868 on theBenchmark for (2868ds/5451Mi) % 175.12/25.49 % (2506451)Instruction limit reached! % 175.12/25.49 % (2506451)------------------------------ % 175.12/25.49 % (2506451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.12/25.49 % (2506451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.12/25.49 % (2506451)CaDiCaL version: 2.1.3 % 175.12/25.49 % (2506451)Termination reason: Instruction limit % 175.12/25.49 % (2506451)Termination phase: Saturation % 175.12/25.49 % (2506451)Time elapsed: 4.065 s % 175.12/25.49 % (2506451)Peak memory usage: 160 MB % 175.12/25.49 % (2506451)Instructions burned: 4093 (million) % 175.12/25.49 % (2506487)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=3297207011:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2857 on theBenchmark for (2857ds/4975Mi) % 175.12/25.49 % (2506480)Instruction limit reached! % 175.12/25.49 % (2506480)------------------------------ % 175.12/25.49 % (2506480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.12/25.49 % (2506480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.12/25.49 % (2506480)CaDiCaL version: 2.1.3 % 175.12/25.49 % (2506480)Termination reason: Instruction limit % 175.12/25.49 % (2506480)Termination phase: Saturation % 175.12/25.49 % (2506480)Time elapsed: 1.766 s % 175.12/25.49 % (2506480)Peak memory usage: 126 MB % 175.12/25.49 % (2506480)Instructions burned: 1783 (million) % 175.12/25.49 % (2506490)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=2570191218:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2849 on theBenchmark for (2849ds/2076Mi) % 175.12/25.49 % (2506454)Instruction limit reached! % 175.12/25.49 % (2506454)------------------------------ % 175.12/25.49 % (2506454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.12/25.49 % (2506454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.12/25.49 % (2506454)CaDiCaL version: 2.1.3 % 175.12/25.49 % (2506454)Termination reason: Instruction limit % 175.12/25.49 % (2506454)Termination phase: Saturation % 175.12/25.49 % (2506454)Time elapsed: 5.863 s % 175.12/25.49 % (2506454)Peak memory usage: 190 MB % 175.12/25.49 % (2506454)Instructions burned: 10545 (million) % 175.12/25.49 % (2506493)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=996996496:i=5145:rtra=on_2838 on theBenchmark for (2838ds/5145Mi) % 175.12/25.49 % (2506490)Instruction limit reached! % 175.12/25.49 % (2506490)------------------------------ % 175.12/25.49 % (2506490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.12/25.49 % (2506490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.12/25.49 % (2506490)CaDiCaL version: 2.1.3 % 175.12/25.49 % (2506490)Termination reason: Instruction limit % 175.12/25.49 % (2506490)Termination phase: Saturation % 175.12/25.49 % (2506490)Time elapsed: 1.928 s % 175.12/25.49 % (2506490)Peak memory usage: 125 MB % 175.12/25.49 % (2506490)Instructions burned: 2076 (million) % 175.12/25.49 % (2506497)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=518699132:i=3509:rtra=on_2828 on theBenchmark for (2828ds/3509Mi) % 175.12/25.49 % (2506493)Instruction limit reached! % 175.12/25.49 % (2506493)------------------------------ % 175.12/25.49 % (2506493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.12/25.49 % (2506493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.12/25.49 % (2506493)CaDiCaL version: 2.1.3 % 175.12/25.49 % (2506493)Termination reason: Instruction limit % 175.12/25.49 % (2506493)Termination phase: Saturation % 175.12/25.49 % (2506493)Time elapsed: 2.120 s % 175.12/25.49 % (2506493)Peak memory usage: 98 MB % 175.12/25.49 % (2506493)Instructions burned: 5145 (million) % 175.12/25.49 % (2506481)Instruction limit reached! % 175.12/25.49 % (2506481)------------------------------ % 175.12/25.49 % (2506481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.12/25.49 % (2506481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.12/25.49 % (2506481)CaDiCaL version: 2.1.3 % 175.12/25.49 % (2506481)Termination reason: Instruction limit % 175.12/25.49 % (2506481)Termination phase: Saturation % 175.12/25.49 % (2506481)Time elapsed: 5.127 s % 175.12/25.49 % (2506481)Peak memory usage: 146 MB % 175.12/25.49 % (2506481)Instructions burned: 5451 (million) % 192.77/27.95 % (2506502)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1097690371:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2814 on theBenchmark for (2814ds/13800Mi) % 192.77/27.95 % (2506487)Instruction limit reached! % 192.77/27.95 % (2506487)------------------------------ % 192.77/27.95 % (2506487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.77/27.95 % (2506487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.77/27.95 % (2506487)CaDiCaL version: 2.1.3 % 192.77/27.95 % (2506487)Termination reason: Instruction limit % 192.77/27.95 % (2506487)Termination phase: Saturation % 192.77/27.95 % (2506487)Time elapsed: 4.381 s % 192.77/27.95 % (2506487)Peak memory usage: 126 MB % 192.77/27.95 % (2506487)Instructions burned: 4975 (million) % 192.77/27.95 % (2506503)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3047727004:i=1412:rtra=on:fsd=on:proc=on_2813 on theBenchmark for (2813ds/1412Mi) % 192.77/27.95 % (2506506)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 % 192.77/27.95 % (2506506)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=422376007:i=11747:aac=none:nm=0:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/11747Mi) % 192.77/27.95 % (2506497)Instruction limit reached! % 192.77/27.95 % (2506497)------------------------------ % 192.77/27.95 % (2506497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.77/27.95 % (2506497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.77/27.95 % (2506497)CaDiCaL version: 2.1.3 % 192.77/27.95 % (2506497)Termination reason: Instruction limit % 192.77/27.95 % (2506497)Termination phase: Saturation % 192.77/27.95 % (2506497)Time elapsed: 2.525 s % 192.77/27.95 % (2506497)Peak memory usage: 97 MB % 192.77/27.95 % (2506497)Instructions burned: 3512 (million) % 192.77/27.95 % (2506503)Instruction limit reached! % 192.77/27.95 % (2506503)------------------------------ % 192.77/27.95 % (2506503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.77/27.95 % (2506503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.77/27.95 % (2506503)CaDiCaL version: 2.1.3 % 192.77/27.95 % (2506503)Termination reason: Instruction limit % 192.77/27.95 % (2506503)Termination phase: Saturation % 192.77/27.95 % (2506503)Time elapsed: 1.352 s % 192.77/27.95 % (2506503)Peak memory usage: 120 MB % 192.77/27.95 % (2506503)Instructions burned: 1413 (million) % 192.77/27.95 % (2506518)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3420873583:s2a=on:i=3553:nm=0:rtra=on_2799 on theBenchmark for (2799ds/3553Mi) % 192.77/27.95 % (2506521)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3288458543:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/3201Mi) % 192.77/27.95 % (2506521)Refutation not found, incomplete strategy % 192.77/27.95 % (2506521)------------------------------ % 192.77/27.95 % (2506521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.77/27.95 % (2506521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.77/27.95 % (2506521)CaDiCaL version: 2.1.3 % 192.77/27.95 % (2506521)Termination reason: Refutation not found, incomplete strategy % 192.77/27.95 % (2506521)Time elapsed: 0.031 s % 192.77/27.95 % (2506521)Peak memory usage: 90 MB % 192.77/27.95 % (2506521)Instructions burned: 30 (million) % 192.77/27.95 % (2506521)------------------------------ % 192.77/27.95 % (2506521)------------------------------ % 192.77/27.95 % (2506476)Instruction limit reached! % 192.77/27.95 % (2506476)------------------------------ % 192.77/27.95 % (2506476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.77/27.95 % (2506476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.77/27.95 % (2506476)CaDiCaL version: 2.1.3 % 192.77/27.95 % (2506476)Termination reason: Instruction limit % 192.77/27.95 % (2506476)Termination phase: Saturation % 192.77/27.95 % (2506476)Time elapsed: 9.045 s % 192.77/27.95 % (2506476)Peak memory usage: 108 MB % 192.77/27.95 % (2506476)Instructions burned: 12633 (million) % 192.77/27.95 % (2506524)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=2518701676:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2789 on theBenchmark for (2789ds/4081Mi) % 221.90/32.03 % (2506472)Instruction limit reached! % 221.90/32.03 % (2506472)------------------------------ % 221.90/32.03 % (2506472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.90/32.03 % (2506472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/32.03 % (2506472)CaDiCaL version: 2.1.3 % 221.90/32.03 % (2506472)Termination reason: Instruction limit % 221.90/32.03 % (2506472)Termination phase: Saturation % 221.90/32.03 % (2506472)Time elapsed: 9.564 s % 221.90/32.03 % (2506472)Peak memory usage: 95 MB % 221.90/32.03 % (2506472)Instructions burned: 13094 (million) % 221.90/32.03 % (2506525)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=2674341860:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2787 on theBenchmark for (2787ds/20260Mi) % 221.90/32.03 % (2506525)Refutation not found, incomplete strategy % 221.90/32.03 % (2506525)------------------------------ % 221.90/32.03 % (2506525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.90/32.03 % (2506525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/32.03 % (2506525)CaDiCaL version: 2.1.3 % 221.90/32.03 % (2506525)Termination reason: Refutation not found, incomplete strategy % 221.90/32.03 % (2506525)Time elapsed: 0.109 s % 221.90/32.03 % (2506525)Peak memory usage: 115 MB % 221.90/32.03 % (2506525)Instructions burned: 85 (million) % 221.90/32.03 % (2506527)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1660291509:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2785 on theBenchmark for (2785ds/58627Mi) % 221.90/32.03 % (2506527)Refutation not found, incomplete strategy % 221.90/32.03 % (2506527)------------------------------ % 221.90/32.03 % (2506527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.90/32.03 % (2506527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/32.03 % (2506527)CaDiCaL version: 2.1.3 % 221.90/32.03 % (2506527)Termination reason: Refutation not found, incomplete strategy % 221.90/32.03 % (2506527)Time elapsed: 0.005 s % 221.90/32.03 % (2506527)Peak memory usage: 88 MB % 221.90/32.03 % (2506527)Instructions burned: 3 (million) % 221.90/32.03 % (2506525)------------------------------ % 221.90/32.03 % (2506525)------------------------------ % 221.90/32.03 % (2506527)------------------------------ % 221.90/32.03 % (2506527)------------------------------ % 221.90/32.03 % (2506532)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1531539618:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2779 on theBenchmark for (2779ds/6258Mi) % 221.90/32.03 % (2506532)Refutation not found, incomplete strategy % 221.90/32.03 % (2506532)------------------------------ % 221.90/32.03 % (2506532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.90/32.03 % (2506532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/32.03 % (2506532)CaDiCaL version: 2.1.3 % 221.90/32.03 % (2506532)Termination reason: Refutation not found, incomplete strategy % 221.90/32.03 % (2506532)Time elapsed: 0.043 s % 221.90/32.03 % (2506532)Peak memory usage: 116 MB % 221.90/32.03 % (2506532)Instructions burned: 9 (million) % 221.90/32.03 % (2506534)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=521897998:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2778 on theBenchmark for (2778ds/34001Mi) % 221.90/32.03 % (2506532)------------------------------ % 221.90/32.03 % (2506532)------------------------------ % 221.90/32.03 % (2506542)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1195863170:s2a=on:i=71622:s2at=-1:rtra=on_2772 on theBenchmark for (2772ds/71622Mi) % 221.90/32.03 % (2506518)Instruction limit reached! % 221.90/32.03 % (2506518)------------------------------ % 221.90/32.03 % (2506518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.90/32.03 % (2506518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/32.03 % (2506518)CaDiCaL version: 2.1.3 % 221.90/32.03 % (2506518)Termination reason: Instruction limit % 221.90/32.03 % (2506518)Termination phase: Saturation % 221.90/32.03 % (2506518)Time elapsed: 3.949 s % 221.90/32.03 % (2506518)Peak memory usage: 101 MB % 221.90/32.03 % (2506518)Instructions burned: 3553 (million) % 221.90/32.03 % (2506545)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3477516181:i=24001:kws=precedence:nm=0:rtra=on_2756 on theBenchmark for (2756ds/24001Mi) % 221.90/32.03 % (2506502)Instruction limit reached! % 221.90/32.03 % (2506502)------------------------------ % 255.30/36.85 % (2506502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.30/36.85 % (2506502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.30/36.85 % (2506502)CaDiCaL version: 2.1.3 % 255.30/36.85 % (2506502)Termination reason: Instruction limit % 255.30/36.85 % (2506502)Termination phase: Saturation % 255.30/36.85 % (2506502)Time elapsed: 5.970 s % 255.30/36.85 % (2506502)Peak memory usage: 138 MB % 255.30/36.85 % (2506502)Instructions burned: 13803 (million) % 255.30/36.85 % (2506550)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=2977852337:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2752 on theBenchmark for (2752ds/2076Mi) % 255.30/36.85 % (2506545)Refutation not found, incomplete strategy % 255.30/36.85 % (2506545)------------------------------ % 255.30/36.85 % (2506545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.30/36.85 % (2506545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.30/36.85 % (2506545)CaDiCaL version: 2.1.3 % 255.30/36.85 % (2506545)Termination reason: Refutation not found, incomplete strategy % 255.30/36.85 % (2506545)Time elapsed: 0.388 s % 255.30/36.85 % (2506545)Peak memory usage: 118 MB % 255.30/36.85 % (2506545)Instructions burned: 393 (million) % 255.30/36.85 % (2506545)------------------------------ % 255.30/36.85 % (2506545)------------------------------ % 255.30/36.85 % (2506524)Instruction limit reached! % 255.30/36.85 % (2506524)------------------------------ % 255.30/36.85 % (2506524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.30/36.85 % (2506524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.30/36.85 % (2506524)CaDiCaL version: 2.1.3 % 255.30/36.85 % (2506524)Termination reason: Instruction limit % 255.30/36.85 % (2506524)Termination phase: Saturation % 255.30/36.85 % (2506524)Time elapsed: 4.198 s % 255.30/36.85 % (2506524)Peak memory usage: 161 MB % 255.30/36.85 % (2506524)Instructions burned: 4081 (million) % 255.30/36.85 % (2506554)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=4266128736:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2745 on theBenchmark for (2745ds/83971Mi) % 255.30/36.85 % (2506555)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=4169916260:i=83944:rtra=on_2744 on theBenchmark for (2744ds/83944Mi) % 255.30/36.85 % (2506555)Refutation not found, incomplete strategy % 255.30/36.85 % (2506555)------------------------------ % 255.30/36.85 % (2506555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.30/36.85 % (2506555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.30/36.85 % (2506555)CaDiCaL version: 2.1.3 % 255.30/36.85 % (2506555)Termination reason: Refutation not found, incomplete strategy % 255.30/36.85 % (2506555)Time elapsed: 0.042 s % 255.30/36.85 % (2506555)Peak memory usage: 116 MB % 255.30/36.85 % (2506555)Instructions burned: 11 (million) % 255.30/36.85 % (2506550)Instruction limit reached! % 255.30/36.85 % (2506550)------------------------------ % 255.30/36.85 % (2506550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.30/36.85 % (2506550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.30/36.85 % (2506550)CaDiCaL version: 2.1.3 % 255.30/36.85 % (2506550)Termination reason: Instruction limit % 255.30/36.85 % (2506550)Termination phase: Saturation % 255.30/36.85 % (2506550)Time elapsed: 1.018 s % 255.30/36.85 % (2506550)Peak memory usage: 124 MB % 255.30/36.85 % (2506550)Instructions burned: 2077 (million) % 255.30/36.85 % (2506555)------------------------------ % 255.30/36.85 % (2506555)------------------------------ % 255.30/36.85 % (2506559)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1453049169:i=9201:rtra=on_2739 on theBenchmark for (2739ds/9201Mi) % 255.30/36.85 % (2506560)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 % 255.30/36.85 % (2506560)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2815360359:i=6806:aac=none:nm=0:rtra=on:rawr=on_2739 on theBenchmark for (2739ds/6806Mi) % 255.30/36.85 % (2506470)Instruction limit reached! % 255.30/36.85 % (2506470)------------------------------ % 255.30/36.85 % (2506470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.30/36.85 % (2506470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.96/39.17 % (2506470)CaDiCaL version: 2.1.3 % 271.96/39.17 % (2506470)Termination reason: Instruction limit % 271.96/39.17 % (2506470)Termination phase: Saturation % 271.96/39.17 % (2506470)Time elapsed: 15.502 s % 271.96/39.17 % (2506470)Peak memory usage: 170 MB % 271.96/39.17 % (2506470)Instructions burned: 17167 (million) % 271.96/39.17 % (2506568)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=797974898:s2a=on:i=3553:nm=0:rtra=on_2727 on theBenchmark for (2727ds/3553Mi) % 271.96/39.17 % (2506506)Instruction limit reached! % 271.96/39.17 % (2506506)------------------------------ % 271.96/39.17 % (2506506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.96/39.17 % (2506506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.96/39.17 % (2506506)CaDiCaL version: 2.1.3 % 271.96/39.17 % (2506506)Termination reason: Instruction limit % 271.96/39.17 % (2506506)Termination phase: Saturation % 271.96/39.17 % (2506506)Time elapsed: 9.684 s % 271.96/39.17 % (2506506)Peak memory usage: 172 MB % 271.96/39.17 % (2506506)Instructions burned: 11748 (million) % 271.96/39.17 % (2506573)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=897818491:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2710 on theBenchmark for (2710ds/2064Mi) % 271.96/39.17 % (2506560)Instruction limit reached! % 271.96/39.17 % (2506560)------------------------------ % 271.96/39.17 % (2506560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.96/39.17 % (2506560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.96/39.17 % (2506560)CaDiCaL version: 2.1.3 % 271.96/39.17 % (2506560)Termination reason: Instruction limit % 271.96/39.17 % (2506560)Termination phase: Saturation % 271.96/39.17 % (2506560)Time elapsed: 2.979 s % 271.96/39.17 % (2506560)Peak memory usage: 147 MB % 271.96/39.17 % (2506560)Instructions burned: 6808 (million) % 271.96/39.17 % (2506576)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=3705849246:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2706 on theBenchmark for (2706ds/20260Mi) % 271.96/39.17 % (2506576)Refutation not found, incomplete strategy % 271.96/39.17 % (2506576)------------------------------ % 271.96/39.17 % (2506576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.96/39.17 % (2506576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.96/39.17 % (2506576)CaDiCaL version: 2.1.3 % 271.96/39.17 % (2506576)Termination reason: Refutation not found, incomplete strategy % 271.96/39.17 % (2506576)Time elapsed: 0.042 s % 271.96/39.17 % (2506576)Peak memory usage: 115 MB % 271.96/39.17 % (2506576)Instructions burned: 85 (million) % 271.96/39.17 % (2506576)------------------------------ % 271.96/39.17 % (2506576)------------------------------ % 271.96/39.17 % (2506578)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2374600963:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2702 on theBenchmark for (2702ds/1244Mi) % 271.96/39.17 % (2506578)Refutation not found, incomplete strategy % 271.96/39.17 % (2506578)------------------------------ % 271.96/39.17 % (2506578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.96/39.17 % (2506578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.96/39.17 % (2506578)CaDiCaL version: 2.1.3 % 271.96/39.17 % (2506578)Termination reason: Refutation not found, incomplete strategy % 271.96/39.17 % (2506578)Time elapsed: 0.026 s % 271.96/39.17 % (2506578)Peak memory usage: 116 MB % 271.96/39.17 % (2506578)Instructions burned: 9 (million) % 271.96/39.17 % (2506578)------------------------------ % 271.96/39.17 % (2506578)------------------------------ % 271.96/39.17 % (2506580)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=1435171069:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2698 on theBenchmark for (2698ds/58261Mi) % 271.96/39.17 % (2506568)Instruction limit reached! % 271.96/39.17 % (2506568)------------------------------ % 271.96/39.17 % (2506568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.96/39.17 % (2506568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.96/39.17 % (2506568)CaDiCaL version: 2.1.3 % 271.96/39.17 % (2506568)Termination reason: Instruction limit % 271.96/39.17 % (2506568)Termination phase: Saturation % 271.96/39.17 % (2506568)Time elapsed: 3.766 s % 271.96/39.17 % (2506568)Peak memory usage: 106 MB % 279.02/40.20 % (2506568)Instructions burned: 3553 (million) % 279.02/40.20 % (2506573)Instruction limit reached! % 279.02/40.20 % (2506573)------------------------------ % 279.02/40.20 % (2506573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.02/40.20 % (2506573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/40.20 % (2506573)CaDiCaL version: 2.1.3 % 279.02/40.20 % (2506573)Termination reason: Instruction limit % 279.02/40.20 % (2506573)Termination phase: Saturation % 279.02/40.20 % (2506573)Time elapsed: 2.178 s % 279.02/40.20 % (2506573)Peak memory usage: 148 MB % 279.02/40.20 % (2506573)Instructions burned: 2065 (million) % 279.02/40.20 % (2506583)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 % 279.02/40.20 % (2506583)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2363072171:i=6806:aac=none:nm=0:rtra=on:rawr=on_2687 on theBenchmark for (2687ds/6806Mi) % 279.02/40.20 % (2506585)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=3798068054:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2685 on theBenchmark for (2685ds/4081Mi) % 279.02/40.20 % (2506559)Instruction limit reached! % 279.02/40.20 % (2506559)------------------------------ % 279.02/40.20 % (2506559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.02/40.20 % (2506559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/40.20 % (2506559)CaDiCaL version: 2.1.3 % 279.02/40.20 % (2506559)Termination reason: Instruction limit % 279.02/40.20 % (2506559)Termination phase: Saturation % 279.02/40.20 % (2506559)Time elapsed: 8.367 s % 279.02/40.20 % (2506559)Peak memory usage: 112 MB % 279.02/40.20 % (2506559)Instructions burned: 9201 (million) % 279.02/40.20 % (2506596)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1172117442:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2653 on theBenchmark for (2653ds/1701Mi) % 279.02/40.20 % (2506596)Refutation not found, incomplete strategy % 279.02/40.20 % (2506596)------------------------------ % 279.02/40.20 % (2506596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.02/40.20 % (2506596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/40.20 % (2506596)CaDiCaL version: 2.1.3 % 279.02/40.20 % (2506596)Termination reason: Refutation not found, incomplete strategy % 279.02/40.20 % (2506596)Time elapsed: 0.044 s % 279.02/40.20 % (2506596)Peak memory usage: 116 MB % 279.02/40.20 % (2506596)Instructions burned: 9 (million) % 279.02/40.20 % (2506596)------------------------------ % 279.02/40.20 % (2506596)------------------------------ % 279.02/40.20 % (2506598)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=1050045644:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2645 on theBenchmark for (2645ds/57001Mi) % 279.02/40.20 % (2506598)Refutation not found, incomplete strategy % 279.02/40.20 % (2506598)------------------------------ % 279.02/40.20 % (2506598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.02/40.20 % (2506598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/40.20 % (2506598)CaDiCaL version: 2.1.3 % 279.02/40.20 % (2506598)Termination reason: Refutation not found, incomplete strategy % 279.02/40.20 % (2506598)Time elapsed: 0.062 s % 279.02/40.20 % (2506598)Peak memory usage: 116 MB % 279.02/40.20 % (2506598)Instructions burned: 26 (million) % 279.02/40.20 % (2506585)Instruction limit reached! % 279.02/40.20 % (2506585)------------------------------ % 279.02/40.20 % (2506585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.02/40.20 % (2506585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/40.20 % (2506585)CaDiCaL version: 2.1.3 % 279.02/40.20 % (2506585)Termination reason: Instruction limit % 279.02/40.20 % (2506585)Termination phase: Saturation % 279.02/40.20 % (2506585)Time elapsed: 4.133 s % 279.02/40.20 % (2506585)Peak memory usage: 162 MB % 279.02/40.20 % (2506585)Instructions burned: 4081 (million) % 279.02/40.20 % (2506598)------------------------------ % 279.02/40.20 % (2506598)------------------------------ % 279.02/40.20 % (2506601)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 % 288.35/41.52 % (2506601)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=461121529:i=8622:aac=none:nm=0:rtra=on:rawr=on_2641 on theBenchmark for (2641ds/8622Mi) % 288.35/41.52 % (2506604)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2771332251:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2638 on theBenchmark for (2638ds/24Mi) % 288.35/41.52 % (2506604)Instruction limit reached! % 288.35/41.52 % (2506604)------------------------------ % 288.35/41.52 % (2506604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.52 % (2506604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.52 % (2506604)CaDiCaL version: 2.1.3 % 288.35/41.52 % (2506604)Termination reason: Instruction limit % 288.35/41.52 % (2506604)Termination phase: Saturation % 288.35/41.52 % (2506604)Time elapsed: 0.064 s % 288.35/41.52 % (2506604)Peak memory usage: 116 MB % 288.35/41.52 % (2506604)Instructions burned: 24 (million) % 288.35/41.52 % (2506583)Instruction limit reached! % 288.35/41.52 % (2506583)------------------------------ % 288.35/41.52 % (2506583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.52 % (2506583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.52 % (2506583)CaDiCaL version: 2.1.3 % 288.35/41.52 % (2506583)Termination reason: Instruction limit % 288.35/41.52 % (2506583)Termination phase: Saturation % 288.35/41.52 % (2506583)Time elapsed: 5.719 s % 288.35/41.52 % (2506583)Peak memory usage: 144 MB % 288.35/41.52 % (2506583)Instructions burned: 6807 (million) % 288.35/41.52 % (2506616)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2241520733:i=614:kws=precedence:nm=0:rtra=on_2628 on theBenchmark for (2628ds/614Mi) % 288.35/41.52 % (2506617)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3603482336:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2626 on theBenchmark for (2626ds/402Mi) % 288.35/41.52 % (2506616)Refutation not found, incomplete strategy % 288.35/41.52 % (2506616)------------------------------ % 288.35/41.52 % (2506616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.52 % (2506616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.52 % (2506616)CaDiCaL version: 2.1.3 % 288.35/41.52 % (2506616)Termination reason: Refutation not found, incomplete strategy % 288.35/41.52 % (2506616)Time elapsed: 0.356 s % 288.35/41.52 % (2506616)Peak memory usage: 118 MB % 288.35/41.52 % (2506616)Instructions burned: 381 (million) % 288.35/41.52 % (2506617)Instruction limit reached! % 288.35/41.52 % (2506617)------------------------------ % 288.35/41.52 % (2506617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.52 % (2506617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.52 % (2506617)CaDiCaL version: 2.1.3 % 288.35/41.52 % (2506617)Termination reason: Instruction limit % 288.35/41.52 % (2506617)Termination phase: Saturation % 288.35/41.52 % (2506617)Time elapsed: 0.392 s % 288.35/41.52 % (2506617)Peak memory usage: 119 MB % 288.35/41.52 % (2506617)Instructions burned: 402 (million) % 288.35/41.52 % (2506616)------------------------------ % 288.35/41.52 % (2506616)------------------------------ % 288.35/41.52 % (2506631)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1975717731:s2a=on:i=14:rtra=on:inst=on_2619 on theBenchmark for (2619ds/14Mi) % 288.35/41.52 % (2506631)Instruction limit reached! % 288.35/41.52 % (2506631)------------------------------ % 288.35/41.52 % (2506631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.52 % (2506631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.52 % (2506631)CaDiCaL version: 2.1.3 % 288.35/41.52 % (2506631)Termination reason: Instruction limit % 288.35/41.52 % (2506631)Termination phase: Saturation % 288.35/41.52 % (2506631)Time elapsed: 0.016 s % 288.35/41.52 % (2506631)Peak memory usage: 88 MB % 288.35/41.52 % (2506631)Instructions burned: 15 (million) % 288.35/41.52 % (2506632)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3003546996:i=8:rtra=on_2618 on theBenchmark for (2618ds/8Mi) % 288.35/41.52 % (2506632)Instruction limit reached! % 288.35/41.52 % (2506632)------------------------------ % 288.35/41.52 % (2506632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.52 % (2506632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.53/42.72 % (2506632)CaDiCaL version: 2.1.3 % 296.53/42.72 % (2506632)Termination reason: Instruction limit % 296.53/42.72 % (2506632)Termination phase: Saturation % 296.53/42.72 % (2506632)Time elapsed: 0.009 s % 296.53/42.72 % (2506632)Peak memory usage: 89 MB % 296.53/42.72 % (2506632)Instructions burned: 8 (million) % 296.53/42.72 % (2506637)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=596682051:i=92:rtra=on_2616 on theBenchmark for (2616ds/92Mi) % 296.53/42.72 % (2506637)Instruction limit reached! % 296.53/42.72 % (2506637)------------------------------ % 296.53/42.72 % (2506637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.53/42.72 % (2506637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.53/42.72 % (2506637)CaDiCaL version: 2.1.3 % 296.53/42.72 % (2506637)Termination reason: Instruction limit % 296.53/42.72 % (2506637)Termination phase: Saturation % 296.53/42.72 % (2506637)Time elapsed: 0.118 s % 296.53/42.72 % (2506637)Peak memory usage: 116 MB % 296.53/42.72 % (2506637)Instructions burned: 92 (million) % 296.53/42.72 % (2506640)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1383599077:i=66:rtra=on_2615 on theBenchmark for (2615ds/66Mi) % 296.53/42.72 % (2506640)Instruction limit reached! % 296.53/42.72 % (2506640)------------------------------ % 296.53/42.72 % (2506640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.53/42.72 % (2506640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.53/42.72 % (2506640)CaDiCaL version: 2.1.3 % 296.53/42.72 % (2506640)Termination reason: Instruction limit % 296.53/42.72 % (2506640)Termination phase: Saturation % 296.53/42.72 % (2506640)Time elapsed: 0.103 s % 296.53/42.72 % (2506640)Peak memory usage: 116 MB % 296.53/42.72 % (2506640)Instructions burned: 66 (million) % 296.53/42.72 % (2506648)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=323082769:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2613 on theBenchmark for (2613ds/28Mi) % 296.53/42.72 % (2506648)Instruction limit reached! % 296.53/42.72 % (2506648)------------------------------ % 296.53/42.72 % (2506648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.53/42.72 % (2506648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.53/42.72 % (2506648)CaDiCaL version: 2.1.3 % 296.53/42.72 % (2506648)Termination reason: Instruction limit % 296.53/42.72 % (2506648)Termination phase: Saturation % 296.53/42.72 % (2506648)Time elapsed: 0.027 s % 296.53/42.72 % (2506648)Peak memory usage: 88 MB % 296.53/42.72 % (2506648)Instructions burned: 29 (million) % 296.53/42.72 % (2506654)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=3775545134:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2611 on theBenchmark for (2611ds/58Mi) % 296.53/42.72 % (2506654)Instruction limit reached! % 296.53/42.72 % (2506654)------------------------------ % 296.53/42.72 % (2506654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.53/42.72 % (2506654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.53/42.72 % (2506654)CaDiCaL version: 2.1.3 % 296.53/42.72 % (2506654)Termination reason: Instruction limit % 296.53/42.72 % (2506654)Termination phase: Saturation % 296.53/42.72 % (2506654)Time elapsed: 0.046 s % 296.53/42.72 % (2506654)Peak memory usage: 89 MB % 296.53/42.72 % (2506654)Instructions burned: 61 (million) % 296.53/42.72 % (2506659)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1625398015:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2609 on theBenchmark for (2609ds/32Mi) % 296.53/42.72 % (2506659)Refutation not found, incomplete strategy % 296.53/42.72 % (2506659)------------------------------ % 296.53/42.72 % (2506659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.53/42.72 % (2506659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.53/42.72 % (2506659)CaDiCaL version: 2.1.3 % 296.53/42.72 % (2506659)Termination reason: Refutation not found, incomplete strategy % 296.53/42.72 % (2506659)Time elapsed: 0.028 s % 296.53/42.72 % (2506659)Peak memory usage: 90 MB % 296.53/42.72 % (2506659)Instructions burned: 28 (million) % 296.53/42.72 % (2506663)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2340501509:i=48:canc=force:rtra=on_2608 on theBenchmark for (2608ds/48Mi) % 296.53/42.72 % (2506663)Instruction limit reached! % 296.53/42.72 % (2506663)------------------------------ % 296.53/42.72 % (2506663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.53/42.72 % (2506663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506663)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506663)Termination reason: Instruction limit % 300.24/43.16 % (2506663)Termination phase: Saturation % 300.24/43.16 % (2506663)Time elapsed: 0.048 s % 300.24/43.16 % (2506663)Peak memory usage: 89 MB % 300.24/43.16 % (2506663)Instructions burned: 48 (million) % 300.24/43.16 % (2506659)------------------------------ % 300.24/43.16 % (2506659)------------------------------ % 300.24/43.16 % (2506671)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=3217144324:i=54:canc=cautious:fsr=off:rtra=on_2605 on theBenchmark for (2605ds/54Mi) % 300.24/43.16 % (2506671)Instruction limit reached! % 300.24/43.16 % (2506671)------------------------------ % 300.24/43.16 % (2506671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506671)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506671)Termination reason: Instruction limit % 300.24/43.16 % (2506671)Termination phase: Saturation % 300.24/43.16 % (2506671)Time elapsed: 0.050 s % 300.24/43.16 % (2506671)Peak memory usage: 89 MB % 300.24/43.16 % (2506671)Instructions burned: 54 (million) % 300.24/43.16 % (2506677)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2688164487:i=170:gtgl=4:rtra=on:gtg=exists_sym_2603 on theBenchmark for (2603ds/170Mi) % 300.24/43.16 % (2506684)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1705365407:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2601 on theBenchmark for (2601ds/4Mi) % 300.24/43.16 % (2506684)Instruction limit reached! % 300.24/43.16 % (2506684)------------------------------ % 300.24/43.16 % (2506684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506684)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506684)Termination reason: Instruction limit % 300.24/43.16 % (2506684)Termination phase: Saturation % 300.24/43.16 % (2506684)Time elapsed: 0.005 s % 300.24/43.16 % (2506684)Peak memory usage: 88 MB % 300.24/43.16 % (2506684)Instructions burned: 4 (million) % 300.24/43.16 % (2506677)Instruction limit reached! % 300.24/43.16 % (2506677)------------------------------ % 300.24/43.16 % (2506677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506677)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506677)Termination reason: Instruction limit % 300.24/43.16 % (2506677)Termination phase: Saturation % 300.24/43.16 % (2506677)Time elapsed: 0.155 s % 300.24/43.16 % (2506677)Peak memory usage: 90 MB % 300.24/43.16 % (2506677)Instructions burned: 170 (million) % 300.24/43.16 % (2506694)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2511515418:i=362:rtra=on:ss=axioms:ev=cautious_2598 on theBenchmark for (2598ds/362Mi) % 300.24/43.16 % (2506695)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1131158513:i=8:ep=RST:ins=2:rtra=on_2598 on theBenchmark for (2598ds/8Mi) % 300.24/43.16 % (2506694)Refutation not found, incomplete strategy % 300.24/43.16 % (2506694)------------------------------ % 300.24/43.16 % (2506694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506694)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506694)Termination reason: Refutation not found, incomplete strategy % 300.24/43.16 % (2506694)Time elapsed: 0.004 s % 300.24/43.16 % (2506694)Peak memory usage: 89 MB % 300.24/43.16 % (2506694)Instructions burned: 2 (million) % 300.24/43.16 % (2506695)Instruction limit reached! % 300.24/43.16 % (2506695)------------------------------ % 300.24/43.16 % (2506695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506695)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506695)Termination reason: Instruction limit % 300.24/43.16 % (2506695)Termination phase: Saturation % 300.24/43.16 % (2506695)Time elapsed: 0.011 s % 300.24/43.16 % (2506695)Peak memory usage: 89 MB % 300.24/43.16 % (2506695)Instructions burned: 8 (million) % 300.24/43.16 % (2506702)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=61483190:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2596 on theBenchmark for (2596ds/132Mi) % 300.24/43.16 % (2506694)------------------------------ % 300.24/43.16 % (2506694)------------------------------ % 300.24/43.16 % (2506702)Instruction limit reached! % 300.24/43.16 % (2506702)------------------------------ % 300.24/43.16 % (2506702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506702)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506702)Termination reason: Instruction limit % 300.24/43.16 % (2506702)Termination phase: Saturation % 300.24/43.16 % (2506702)Time elapsed: 0.203 s % 300.24/43.16 % (2506702)Peak memory usage: 134 MB % 300.24/43.16 % (2506702)Instructions burned: 133 (million) % 300.24/43.16 % (2506710)lrs+10_1_thi=all:si=on:fd=off:random_seed=4151416803:i=106:rtra=on:gtg=all_2592 on theBenchmark for (2592ds/106Mi) % 300.24/43.16 % (2506715)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=3466013577:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2590 on theBenchmark for (2590ds/16Mi) % 300.24/43.16 % (2506715)Instruction limit reached! % 300.24/43.16 % (2506715)------------------------------ % 300.24/43.16 % (2506715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506715)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506715)Termination reason: Instruction limit % 300.24/43.16 % (2506715)Termination phase: Saturation % 300.24/43.16 % (2506715)Time elapsed: 0.018 s % 300.24/43.16 % (2506715)Peak memory usage: 88 MB % 300.24/43.16 % (2506715)Instructions burned: 16 (million) % 300.24/43.16 % (2506710)Instruction limit reached! % 300.24/43.16 % (2506710)------------------------------ % 300.24/43.16 % (2506710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506710)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506710)Termination reason: Instruction limit % 300.24/43.16 % (2506710)Termination phase: Saturation % 300.24/43.16 % (2506710)Time elapsed: 0.158 s % 300.24/43.16 % (2506710)Peak memory usage: 116 MB % 300.24/43.16 % (2506710)Instructions burned: 106 (million) % 300.24/43.16 % (2506724)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3048974952:i=4:doe=on:canc=force:asg=cautious:rtra=on_2587 on theBenchmark for (2587ds/4Mi) % 300.24/43.16 % (2506724)Instruction limit reached! % 300.24/43.16 % (2506724)------------------------------ % 300.24/43.16 % (2506724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506724)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506724)Termination reason: Instruction limit % 300.24/43.16 % (2506724)Termination phase: Saturation % 300.24/43.16 % (2506724)Time elapsed: 0.006 s % 300.24/43.16 % (2506724)Peak memory usage: 89 MB % 300.24/43.16 % (2506724)Instructions burned: 4 (million) % 300.24/43.16 % (2506722)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3097820206:st=3:i=4:rtra=on:ss=axioms_2588 on theBenchmark for (2588ds/4Mi) % 300.24/43.16 % (2506722)Instruction limit reached! % 300.24/43.16 % (2506722)------------------------------ % 300.24/43.16 % (2506722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506722)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506722)Termination reason: Instruction limit % 300.24/43.16 % (2506722)Termination phase: Saturation % 300.24/43.16 % (2506722)Time elapsed: 0.005 s % 300.24/43.16 % (2506722)Peak memory usage: 88 MB % 300.24/43.16 % (2506722)Instructions burned: 4 (million) % 300.24/43.16 % (2506728)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1701939227:i=254:doe=on:rtra=on_2585 on theBenchmark for (2585ds/254Mi) % 300.24/43.16 % (2506731)dis+10_1_si=on:random_seed=3886946520:i=20:ep=R:rtra=on_2584 on theBenchmark for (2584ds/20Mi) % 300.24/43.16 % (2506731)Instruction limit reached! % 300.24/43.16 % (2506731)------------------------------ % 300.24/43.16 % (2506731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.16 % (2506731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.16 % (2506731)CaDiCaL version: 2.1.3 % 300.24/43.16 % (2506731)Termination reason: Instruction limit % 300.24/43.16 % (2506731)Termination phase: Saturation % 300.24/43.16 % (2506731)Time elapsed: 0.021 s % 300.24/43.16 % (2506731)Peak memory usage: 88 MB % 300.24/43.16 % (2506731)Instructions burned: 20 (million) % 300.24/43.16 % % 300.24/43.17 Terminated %------------------------------------------------------------------------------