%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW830_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:54 PM UTC 2026 % Result : Timeout 300.54s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW830_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.19 % Computer : n009.cluster.edu % 0.12/0.19 % Model : x86_64 x86_64 % 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.19 % Memory : 8046.5625MB % 0.12/0.19 % OS : Linux 6.8.0-71-generic % 0.12/0.19 % CPULimit : 300 % 0.12/0.19 % WCLimit : 300 % 0.12/0.19 % DateTime : Mon Sep 28 14:30:52 UTC 2026 % 0.12/0.19 % CPUTime : % 0.12/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.23 Running first-order theorem proving % 0.12/0.23 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 % 3.87/1.52 % (3069995)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.87/1.52 % (3070057)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4090316272:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.87/1.52 % (3070057)Instruction limit reached! % 3.87/1.52 % (3070057)------------------------------ % 3.87/1.52 % (3070057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.52 % (3070057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.52 % (3070057)CaDiCaL version: 2.1.3 % 3.87/1.52 % (3070057)Termination reason: Instruction limit % 3.87/1.52 % (3070057)Termination phase: Property scanning % 3.87/1.52 % (3070057)Time elapsed: 0.003 s % 3.87/1.52 % (3070057)Peak memory usage: 85 MB % 3.87/1.52 % (3070057)Instructions burned: 12 (million) % 3.87/1.52 % (3070062)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=362029062:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.87/1.52 % (3070061)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3570649379:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.87/1.52 % (3070058)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4048408869:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.87/1.52 % (3070059)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1732287764:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.87/1.52 % (3070063)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2107660445:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.87/1.52 % (3070060)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2469956593:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.87/1.52 % (3070061)Instruction limit reached! % 3.87/1.52 % (3070061)------------------------------ % 3.87/1.52 % (3070061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.52 % (3070061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.52 % (3070061)CaDiCaL version: 2.1.3 % 3.87/1.52 % (3070061)Termination reason: Instruction limit % 3.87/1.52 % (3070061)Termination phase: Property scanning % 3.87/1.52 % (3070061)Time elapsed: 0.003 s % 3.87/1.52 % (3070061)Peak memory usage: 85 MB % 3.87/1.52 % (3070061)Instructions burned: 5 (million) % 3.87/1.52 % (3070060)Instruction limit reached! % 3.87/1.52 % (3070060)------------------------------ % 3.87/1.52 % (3070060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.52 % (3070060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.52 % (3070060)CaDiCaL version: 2.1.3 % 3.87/1.52 % (3070060)Termination reason: Instruction limit % 3.87/1.52 % (3070060)Termination phase: Property scanning % 3.87/1.52 % (3070060)Time elapsed: 0.005 s % 3.87/1.52 % (3070060)Peak memory usage: 85 MB % 3.87/1.52 % (3070060)Instructions burned: 9 (million) % 3.87/1.52 % (3070063)Instruction limit reached! % 3.87/1.52 % (3070063)------------------------------ % 3.87/1.52 % (3070063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.52 % (3070063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.52 % (3070063)CaDiCaL version: 2.1.3 % 3.87/1.52 % (3070063)Termination reason: Instruction limit % 3.87/1.52 % (3070063)Termination phase: Preprocessing 3 % 3.87/1.52 % (3070063)Time elapsed: 0.018 s % 3.87/1.52 % (3070063)Peak memory usage: 87 MB % 3.87/1.52 % (3070063)Instructions burned: 34 (million) % 3.87/1.52 % (3070062)Instruction limit reached! % 3.87/1.52 % (3070062)------------------------------ % 3.87/1.52 % (3070062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.87/1.52 % (3070062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/1.52 % (3070062)CaDiCaL version: 2.1.3 % 3.87/1.52 % (3070062)Termination reason: Instruction limit % 3.87/1.52 % (3070062)Termination phase: Property scanning % 3.87/1.52 % (3070062)Time elapsed: 0.024 s % 3.87/1.52 % (3070062)Peak memory usage: 87 MB % 3.87/1.52 % (3070062)Instructions burned: 48 (million) % 3.87/1.52 % (3070066)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4130906017:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 3.87/1.52 % (3070066)Refutation not found, incomplete strategy % 4.91/1.70 % (3070066)------------------------------ % 4.91/1.70 % (3070066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.91/1.70 % (3070066)CaDiCaL version: 2.1.3 % 4.91/1.70 % (3070066)Termination reason: Refutation not found, incomplete strategy % 4.91/1.70 % (3070066)Time elapsed: 0.004 s % 4.91/1.70 % (3070066)Peak memory usage: 88 MB % 4.91/1.70 % (3070066)Instructions burned: 15 (million) % 4.91/1.70 % (3070059)Instruction limit reached! % 4.91/1.70 % (3070059)------------------------------ % 4.91/1.70 % (3070059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.91/1.70 % (3070059)CaDiCaL version: 2.1.3 % 4.91/1.70 % (3070059)Termination reason: Instruction limit % 4.91/1.70 % (3070059)Termination phase: Saturation % 4.91/1.70 % (3070059)Time elapsed: 0.141 s % 4.91/1.70 % (3070059)Peak memory usage: 118 MB % 4.91/1.70 % (3070059)Instructions burned: 202 (million) % 4.91/1.70 % (3070074)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2681475345:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 4.91/1.70 % (3070073)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=4203780308:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 4.91/1.70 % (3070074)Instruction limit reached! % 4.91/1.70 % (3070074)------------------------------ % 4.91/1.70 % (3070074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.91/1.70 % (3070074)CaDiCaL version: 2.1.3 % 4.91/1.70 % (3070074)Termination reason: Instruction limit % 4.91/1.70 % (3070074)Termination phase: Preprocessing 3 % 4.91/1.70 % (3070074)Time elapsed: 0.010 s % 4.91/1.70 % (3070074)Peak memory usage: 86 MB % 4.91/1.70 % (3070074)Instructions burned: 17 (million) % 4.91/1.70 % (3070073)Instruction limit reached! % 4.91/1.70 % (3070073)------------------------------ % 4.91/1.70 % (3070073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.91/1.70 % (3070073)CaDiCaL version: 2.1.3 % 4.91/1.70 % (3070073)Termination reason: Instruction limit % 4.91/1.70 % (3070073)Termination phase: Preprocessing 3 % 4.91/1.70 % (3070073)Time elapsed: 0.016 s % 4.91/1.70 % (3070073)Peak memory usage: 86 MB % 4.91/1.70 % (3070073)Instructions burned: 30 (million) % 4.91/1.70 % (3070075)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2066163883:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.91/1.70 % (3070076)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=2261092445:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.91/1.70 % (3070075)Instruction limit reached! % 4.91/1.70 % (3070075)------------------------------ % 4.91/1.70 % (3070075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.91/1.70 % (3070075)CaDiCaL version: 2.1.3 % 4.91/1.70 % (3070075)Termination reason: Instruction limit % 4.91/1.70 % (3070075)Termination phase: Naming % 4.91/1.70 % (3070075)Time elapsed: 0.012 s % 4.91/1.70 % (3070075)Peak memory usage: 86 MB % 4.91/1.70 % (3070075)Instructions burned: 24 (million) % 4.91/1.70 % (3070076)Instruction limit reached! % 4.91/1.70 % (3070076)------------------------------ % 4.91/1.70 % (3070076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.91/1.70 % (3070076)CaDiCaL version: 2.1.3 % 4.91/1.70 % (3070076)Termination reason: Instruction limit % 4.91/1.70 % (3070076)Termination phase: Preprocessing 3 % 4.91/1.70 % (3070076)Time elapsed: 0.014 s % 4.91/1.70 % (3070076)Peak memory usage: 87 MB % 4.91/1.70 % (3070076)Instructions burned: 27 (million) % 4.91/1.70 % (3070058)Instruction limit reached! % 4.91/1.70 % (3070058)------------------------------ % 4.91/1.70 % (3070058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.91/1.70 % (3070058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.86 % (3070058)CaDiCaL version: 2.1.3 % 6.15/1.86 % (3070058)Termination reason: Instruction limit % 6.15/1.86 % (3070058)Termination phase: Saturation % 6.15/1.86 % (3070058)Time elapsed: 0.200 s % 6.15/1.86 % (3070058)Peak memory usage: 119 MB % 6.15/1.86 % (3070058)Instructions burned: 307 (million) % 6.15/1.86 % (3070066)------------------------------ % 6.15/1.86 % (3070066)------------------------------ % 6.15/1.86 % (3070102)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4202695421:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.15/1.86 % (3070115)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1218258631:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 6.15/1.86 % (3070115)Instruction limit reached! % 6.15/1.86 % (3070115)------------------------------ % 6.15/1.86 % (3070115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.86 % (3070115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.86 % (3070115)CaDiCaL version: 2.1.3 % 6.15/1.86 % (3070115)Termination reason: Instruction limit % 6.15/1.86 % (3070115)Termination phase: Property scanning % 6.15/1.86 % (3070115)Time elapsed: 0.002 s % 6.15/1.86 % (3070115)Peak memory usage: 85 MB % 6.15/1.86 % (3070115)Instructions burned: 2 (million) % 6.15/1.86 % (3070126)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4290348598:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 6.15/1.86 % (3070126)Instruction limit reached! % 6.15/1.86 % (3070126)------------------------------ % 6.15/1.86 % (3070126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.86 % (3070126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.86 % (3070126)CaDiCaL version: 2.1.3 % 6.15/1.86 % (3070126)Termination reason: Instruction limit % 6.15/1.86 % (3070126)Termination phase: Property scanning % 6.15/1.86 % (3070126)Time elapsed: 0.003 s % 6.15/1.86 % (3070126)Peak memory usage: 85 MB % 6.15/1.86 % (3070126)Instructions burned: 5 (million) % 6.15/1.86 % (3070120)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2063586349:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 6.15/1.86 % (3070102)Instruction limit reached! % 6.15/1.86 % (3070102)------------------------------ % 6.15/1.86 % (3070102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.86 % (3070102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.86 % (3070102)CaDiCaL version: 2.1.3 % 6.15/1.86 % (3070102)Termination reason: Instruction limit % 6.15/1.86 % (3070102)Termination phase: Saturation % 6.15/1.86 % (3070102)Time elapsed: 0.042 s % 6.15/1.86 % (3070102)Peak memory usage: 89 MB % 6.15/1.86 % (3070102)Instructions burned: 85 (million) % 6.15/1.86 % (3070120)Refutation not found, incomplete strategy % 6.15/1.86 % (3070120)------------------------------ % 6.15/1.86 % (3070120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.86 % (3070120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.86 % (3070120)CaDiCaL version: 2.1.3 % 6.15/1.86 % (3070120)Termination reason: Refutation not found, incomplete strategy % 6.15/1.86 % (3070120)Time elapsed: 0.009 s % 6.15/1.86 % (3070120)Peak memory usage: 88 MB % 6.15/1.86 % (3070120)Instructions burned: 14 (million) % 6.15/1.86 % (3070130)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=513994090:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 6.15/1.86 % (3070134)lrs+10_1_thi=all:si=on:fd=off:random_seed=437731152:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.15/1.86 % (3070155)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=826408270:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 6.15/1.86 % (3070155)Instruction limit reached! % 6.15/1.86 % (3070155)------------------------------ % 6.15/1.86 % (3070155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.15/1.86 % (3070155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.15/1.86 % (3070155)CaDiCaL version: 2.1.3 % 6.15/1.86 % (3070155)Termination reason: Instruction limit % 6.15/1.86 % (3070155)Termination phase: shuffling % 6.15/1.86 % (3070155)Time elapsed: 0.002 s % 6.82/2.03 % (3070155)Peak memory usage: 85 MB % 6.82/2.03 % (3070155)Instructions burned: 8 (million) % 6.82/2.03 % (3070134)Instruction limit reached! % 6.82/2.03 % (3070134)------------------------------ % 6.82/2.03 % (3070134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.82/2.03 % (3070134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.82/2.03 % (3070134)CaDiCaL version: 2.1.3 % 6.82/2.03 % (3070134)Termination reason: Instruction limit % 6.82/2.03 % (3070134)Termination phase: Property scanning % 6.82/2.03 % (3070134)Time elapsed: 0.027 s % 6.82/2.03 % (3070134)Peak memory usage: 87 MB % 6.82/2.03 % (3070134)Instructions burned: 54 (million) % 6.82/2.03 % (3070130)Instruction limit reached! % 6.82/2.03 % (3070130)------------------------------ % 6.82/2.03 % (3070130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.82/2.03 % (3070130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.82/2.03 % (3070130)CaDiCaL version: 2.1.3 % 6.82/2.03 % (3070130)Termination reason: Instruction limit % 6.82/2.03 % (3070130)Termination phase: Saturation % 6.82/2.03 % (3070130)Time elapsed: 0.041 s % 6.82/2.03 % (3070130)Peak memory usage: 97 MB % 6.82/2.03 % (3070130)Instructions burned: 66 (million) % 6.82/2.03 % (3070176)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=604441966:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 6.82/2.03 % (3070176)Instruction limit reached! % 6.82/2.03 % (3070176)------------------------------ % 6.82/2.03 % (3070176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.82/2.03 % (3070176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.82/2.03 % (3070176)CaDiCaL version: 2.1.3 % 6.82/2.03 % (3070176)Termination reason: Instruction limit % 6.82/2.03 % (3070176)Termination phase: Property scanning % 6.82/2.03 % (3070176)Time elapsed: 0.002 s % 6.82/2.03 % (3070176)Peak memory usage: 85 MB % 6.82/2.03 % (3070176)Instructions burned: 2 (million) % 6.82/2.03 % (3070185)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1674053798:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 6.82/2.03 % (3070185)Instruction limit reached! % 6.82/2.03 % (3070185)------------------------------ % 6.82/2.03 % (3070185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.82/2.03 % (3070185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.82/2.03 % (3070185)CaDiCaL version: 2.1.3 % 6.82/2.03 % (3070185)Termination reason: Instruction limit % 6.82/2.03 % (3070185)Termination phase: Property scanning % 6.82/2.03 % (3070185)Time elapsed: 0.002 s % 6.82/2.03 % (3070185)Peak memory usage: 85 MB % 6.82/2.03 % (3070185)Instructions burned: 2 (million) % 6.82/2.03 % (3070196)dis+10_1_si=on:random_seed=570923622:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 6.82/2.03 % (3070196)Instruction limit reached! % 6.82/2.03 % (3070196)------------------------------ % 6.82/2.03 % (3070196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.82/2.03 % (3070196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.82/2.03 % (3070196)CaDiCaL version: 2.1.3 % 6.82/2.03 % (3070196)Termination reason: Instruction limit % 6.82/2.03 % (3070196)Termination phase: Property scanning % 6.82/2.03 % (3070196)Time elapsed: 0.003 s % 6.82/2.03 % (3070196)Peak memory usage: 85 MB % 6.82/2.03 % (3070196)Instructions burned: 12 (million) % 6.82/2.03 % (3070189)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2324951500:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.82/2.03 % (3070205)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3640790232:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 6.82/2.03 % (3070206)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2211749319: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_2993 on theBenchmark for (2993ds/35Mi) % 6.82/2.03 % (3070205)Instruction limit reached! % 6.82/2.03 % (3070205)------------------------------ % 6.82/2.03 % (3070205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.82/2.03 % (3070205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.82/2.03 % (3070205)CaDiCaL version: 2.1.3 % 6.82/2.03 % (3070205)Termination reason: Instruction limit % 6.82/2.03 % (3070205)Termination phase: Preprocessing 3 % 8.84/2.25 % (3070205)Time elapsed: 0.014 s % 8.84/2.25 % (3070205)Peak memory usage: 87 MB % 8.84/2.25 % (3070205)Instructions burned: 27 (million) % 8.84/2.25 % (3070213)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2553285480:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi) % 8.84/2.25 % (3070189)Instruction limit reached! % 8.84/2.25 % (3070189)------------------------------ % 8.84/2.25 % (3070189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.84/2.25 % (3070189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.84/2.25 % (3070189)CaDiCaL version: 2.1.3 % 8.84/2.25 % (3070189)Termination reason: Instruction limit % 8.84/2.25 % (3070189)Termination phase: Saturation % 8.84/2.25 % (3070189)Time elapsed: 0.098 s % 8.84/2.25 % (3070189)Peak memory usage: 118 MB % 8.84/2.25 % (3070189)Instructions burned: 128 (million) % 8.84/2.25 % (3070206)Instruction limit reached! % 8.84/2.25 % (3070206)------------------------------ % 8.84/2.25 % (3070206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.84/2.25 % (3070206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.84/2.25 % (3070206)CaDiCaL version: 2.1.3 % 8.84/2.25 % (3070206)Termination reason: Instruction limit % 8.84/2.25 % (3070206)Termination phase: Preprocessing 3 % 8.84/2.25 % (3070206)Time elapsed: 0.020 s % 8.84/2.25 % (3070206)Peak memory usage: 87 MB % 8.84/2.25 % (3070206)Instructions burned: 35 (million) % 8.84/2.25 % (3070208)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4188245915:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 8.84/2.25 % (3070208)Instruction limit reached! % 8.84/2.25 % (3070208)------------------------------ % 8.84/2.25 % (3070208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.84/2.25 % (3070208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.84/2.25 % (3070208)CaDiCaL version: 2.1.3 % 8.84/2.25 % (3070208)Termination reason: Instruction limit % 8.84/2.25 % (3070208)Termination phase: Property scanning % 8.84/2.25 % (3070208)Time elapsed: 0.002 s % 8.84/2.25 % (3070208)Peak memory usage: 85 MB % 8.84/2.25 % (3070208)Instructions burned: 2 (million) % 8.84/2.25 % (3070120)------------------------------ % 8.84/2.25 % (3070120)------------------------------ % 8.84/2.25 % (3070212)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=37654390:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 8.84/2.25 % (3070212)Instruction limit reached! % 8.84/2.25 % (3070212)------------------------------ % 8.84/2.25 % (3070212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.84/2.25 % (3070212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.84/2.25 % (3070212)CaDiCaL version: 2.1.3 % 8.84/2.25 % (3070212)Termination reason: Instruction limit % 8.84/2.25 % (3070212)Termination phase: Property scanning % 8.84/2.25 % (3070212)Time elapsed: 0.005 s % 8.84/2.25 % (3070212)Peak memory usage: 85 MB % 8.84/2.25 % (3070212)Instructions burned: 10 (million) % 8.84/2.25 % (3070213)Instruction limit reached! % 8.84/2.25 % (3070213)------------------------------ % 8.84/2.25 % (3070213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.84/2.25 % (3070213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.84/2.25 % (3070213)CaDiCaL version: 2.1.3 % 8.84/2.25 % (3070213)Termination reason: Instruction limit % 8.84/2.25 % (3070213)Termination phase: Saturation % 8.84/2.25 % (3070213)Time elapsed: 0.112 s % 8.84/2.25 % (3070213)Peak memory usage: 92 MB % 8.84/2.25 % (3070213)Instructions burned: 373 (million) % 8.84/2.25 % (3070224)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=652790165:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 8.84/2.25 % (3070224)Instruction limit reached! % 8.84/2.25 % (3070224)------------------------------ % 8.84/2.25 % (3070224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.84/2.25 % (3070224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.84/2.25 % (3070224)CaDiCaL version: 2.1.3 % 8.84/2.25 % (3070224)Termination reason: Instruction limit % 8.84/2.25 % (3070224)Termination phase: Property scanning % 8.84/2.25 % (3070224)Time elapsed: 0.006 s % 8.84/2.25 % (3070224)Peak memory usage: 85 MB % 8.84/2.25 % (3070224)Instructions burned: 13 (million) % 8.84/2.25 % (3070237)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3291454146:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi) % 10.75/2.54 % (3070241)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=470961739:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi) % 10.75/2.54 % (3070239)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3153665576:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.75/2.54 % (3070239)Instruction limit reached! % 10.75/2.54 % (3070239)------------------------------ % 10.75/2.54 % (3070239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.75/2.54 % (3070239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.75/2.54 % (3070239)CaDiCaL version: 2.1.3 % 10.75/2.54 % (3070239)Termination reason: Instruction limit % 10.75/2.54 % (3070239)Termination phase: Preprocessing 1 % 10.75/2.54 % (3070239)Time elapsed: 0.006 s % 10.75/2.54 % (3070239)Peak memory usage: 85 MB % 10.75/2.54 % (3070239)Instructions burned: 11 (million) % 10.75/2.54 % (3070241)Instruction limit reached! % 10.75/2.54 % (3070241)------------------------------ % 10.75/2.54 % (3070241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.75/2.54 % (3070241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.75/2.54 % (3070241)CaDiCaL version: 2.1.3 % 10.75/2.54 % (3070241)Termination reason: Instruction limit % 10.75/2.54 % (3070241)Termination phase: Saturation % 10.75/2.54 % (3070241)Time elapsed: 0.034 s % 10.75/2.54 % (3070241)Peak memory usage: 88 MB % 10.75/2.54 % (3070241)Instructions burned: 72 (million) % 10.75/2.54 % (3070265)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=1038939765:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi) % 10.75/2.54 % (3070264)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=515484431:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi) % 10.75/2.54 % (3070237)Refutation not found, incomplete strategy % 10.75/2.54 % (3070237)------------------------------ % 10.75/2.54 % (3070237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.75/2.54 % (3070237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.75/2.54 % (3070237)CaDiCaL version: 2.1.3 % 10.75/2.54 % (3070237)Termination reason: Refutation not found, incomplete strategy % 10.75/2.54 % (3070237)Time elapsed: 0.037 s % 10.75/2.54 % (3070237)Peak memory usage: 111 MB % 10.75/2.54 % (3070237)Instructions burned: 26 (million) % 10.75/2.54 % (3070264)Instruction limit reached! % 10.75/2.54 % (3070264)------------------------------ % 10.75/2.54 % (3070264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.75/2.54 % (3070264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.75/2.54 % (3070264)CaDiCaL version: 2.1.3 % 10.75/2.54 % (3070264)Termination reason: Instruction limit % 10.75/2.54 % (3070264)Termination phase: Saturation % 10.75/2.54 % (3070264)Time elapsed: 0.038 s % 10.75/2.54 % (3070264)Peak memory usage: 90 MB % 10.75/2.54 % (3070264)Instructions burned: 75 (million) % 10.75/2.54 % (3070272)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1627114995:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi) % 10.75/2.54 % (3070272)Instruction limit reached! % 10.75/2.54 % (3070272)------------------------------ % 10.75/2.54 % (3070272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.75/2.54 % (3070272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.75/2.54 % (3070272)CaDiCaL version: 2.1.3 % 10.75/2.54 % (3070272)Termination reason: Instruction limit % 10.75/2.54 % (3070272)Termination phase: Saturation % 10.75/2.54 % (3070272)Time elapsed: 0.054 s % 10.75/2.54 % (3070272)Peak memory usage: 118 MB % 10.75/2.54 % (3070272)Instructions burned: 132 (million) % 10.75/2.54 % (3070277)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3709510381:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 10.75/2.54 % (3070278)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=15300089:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 10.75/2.54 % (3070278)Instruction limit reached! % 10.75/2.54 % (3070278)------------------------------ % 12.26/2.86 % (3070278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.26/2.86 % (3070278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.26/2.86 % (3070278)CaDiCaL version: 2.1.3 % 12.26/2.86 % (3070278)Termination reason: Instruction limit % 12.26/2.86 % (3070278)Termination phase: Preprocessing 2 % 12.26/2.86 % (3070278)Time elapsed: 0.018 s % 12.26/2.86 % (3070278)Peak memory usage: 86 MB % 12.26/2.86 % (3070278)Instructions burned: 40 (million) % 12.26/2.86 % (3070281)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1595109411:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 12.26/2.86 % (3070277)Instruction limit reached! % 12.26/2.86 % (3070277)------------------------------ % 12.26/2.86 % (3070277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.26/2.86 % (3070277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.26/2.86 % (3070277)CaDiCaL version: 2.1.3 % 12.26/2.86 % (3070277)Termination reason: Instruction limit % 12.26/2.86 % (3070277)Termination phase: Saturation % 12.26/2.86 % (3070277)Time elapsed: 0.069 s % 12.26/2.86 % (3070277)Peak memory usage: 135 MB % 12.26/2.86 % (3070277)Instructions burned: 132 (million) % 12.26/2.86 % (3070265)Instruction limit reached! % 12.26/2.86 % (3070265)------------------------------ % 12.26/2.86 % (3070265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.26/2.86 % (3070265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.26/2.86 % (3070265)CaDiCaL version: 2.1.3 % 12.26/2.86 % (3070265)Termination reason: Instruction limit % 12.26/2.86 % (3070265)Termination phase: Saturation % 12.26/2.86 % (3070265)Time elapsed: 0.178 s % 12.26/2.86 % (3070265)Peak memory usage: 92 MB % 12.26/2.86 % (3070265)Instructions burned: 296 (million) % 12.26/2.86 % (3070283)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1313354957:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 12.26/2.86 % (3070237)------------------------------ % 12.26/2.86 % (3070237)------------------------------ % 12.26/2.86 % (3070284)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1497366179:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 12.26/2.86 % (3070287)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=2536670525:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi) % 12.26/2.86 % (3070290)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2495961642:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 12.26/2.86 % (3070281)Instruction limit reached! % 12.26/2.86 % (3070281)------------------------------ % 12.26/2.86 % (3070281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.26/2.86 % (3070281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.26/2.86 % (3070281)CaDiCaL version: 2.1.3 % 12.26/2.86 % (3070281)Termination reason: Instruction limit % 12.26/2.86 % (3070281)Termination phase: Saturation % 12.26/2.86 % (3070281)Time elapsed: 0.143 s % 12.26/2.86 % (3070281)Peak memory usage: 91 MB % 12.26/2.86 % (3070281)Instructions burned: 307 (million) % 12.26/2.86 % (3070287)Refutation not found, incomplete strategy % 12.26/2.86 % (3070287)------------------------------ % 12.26/2.86 % (3070287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.26/2.86 % (3070287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.26/2.86 % (3070287)CaDiCaL version: 2.1.3 % 12.26/2.86 % (3070287)Termination reason: Refutation not found, incomplete strategy % 12.26/2.86 % (3070287)Time elapsed: 0.038 s % 12.26/2.86 % (3070287)Peak memory usage: 112 MB % 12.26/2.86 % (3070287)Instructions burned: 28 (million) % 12.26/2.86 % (3070289)dis+10_1_si=on:random_seed=2791673766:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi) % 12.26/2.86 % (3070284)Instruction limit reached! % 12.26/2.86 % (3070284)------------------------------ % 12.26/2.86 % (3070284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.26/2.86 % (3070284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.26/2.86 % (3070284)CaDiCaL version: 2.1.3 % 12.26/2.86 % (3070284)Termination reason: Instruction limit % 12.26/2.86 % (3070284)Termination phase: Saturation % 15.33/3.05 % (3070284)Time elapsed: 0.094 s % 15.33/3.05 % (3070284)Peak memory usage: 118 MB % 15.33/3.05 % (3070284)Instructions burned: 131 (million) % 15.33/3.05 % (3070290)Instruction limit reached! % 15.33/3.05 % (3070290)------------------------------ % 15.33/3.05 % (3070290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.33/3.05 % (3070290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.33/3.05 % (3070290)CaDiCaL version: 2.1.3 % 15.33/3.05 % (3070290)Termination reason: Instruction limit % 15.33/3.05 % (3070290)Termination phase: Saturation % 15.33/3.05 % (3070290)Time elapsed: 0.118 s % 15.33/3.05 % (3070290)Peak memory usage: 97 MB % 15.33/3.05 % (3070290)Instructions burned: 384 (million) % 15.33/3.05 % (3070293)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4013373630:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi) % 15.33/3.05 % (3070296)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3074652768:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 15.33/3.05 % (3070296)Instruction limit reached! % 15.33/3.05 % (3070296)------------------------------ % 15.33/3.05 % (3070296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.33/3.05 % (3070296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.33/3.05 % (3070296)CaDiCaL version: 2.1.3 % 15.33/3.05 % (3070296)Termination reason: Instruction limit % 15.33/3.05 % (3070296)Termination phase: Saturation % 15.33/3.05 % (3070296)Time elapsed: 0.035 s % 15.33/3.05 % (3070296)Peak memory usage: 90 MB % 15.33/3.05 % (3070296)Instructions burned: 66 (million) % 15.33/3.05 % (3070293)Instruction limit reached! % 15.33/3.05 % (3070293)------------------------------ % 15.33/3.05 % (3070293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.33/3.05 % (3070293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.33/3.05 % (3070293)CaDiCaL version: 2.1.3 % 15.33/3.05 % (3070293)Termination reason: Instruction limit % 15.33/3.05 % (3070293)Termination phase: Saturation % 15.33/3.05 % (3070293)Time elapsed: 0.082 s % 15.33/3.05 % (3070293)Peak memory usage: 91 MB % 15.33/3.05 % (3070293)Instructions burned: 141 (million) % 15.33/3.05 % (3070298)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1613046643:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi) % 15.33/3.05 % (3070299)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=428973769:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi) % 15.33/3.05 % (3070287)------------------------------ % 15.33/3.05 % (3070287)------------------------------ % 15.33/3.05 % (3070298)Instruction limit reached! % 15.33/3.05 % (3070298)------------------------------ % 15.33/3.05 % (3070298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.33/3.05 % (3070298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.33/3.05 % (3070298)CaDiCaL version: 2.1.3 % 15.33/3.05 % (3070298)Termination reason: Instruction limit % 15.33/3.05 % (3070298)Termination phase: Saturation % 15.33/3.05 % (3070298)Time elapsed: 0.068 s % 15.33/3.05 % (3070298)Peak memory usage: 90 MB % 15.33/3.05 % (3070298)Instructions burned: 122 (million) % 15.33/3.05 % (3070299)Refutation not found, incomplete strategy % 15.33/3.05 % (3070299)------------------------------ % 15.33/3.05 % (3070299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.33/3.05 % (3070299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.33/3.05 % (3070299)CaDiCaL version: 2.1.3 % 15.33/3.05 % (3070299)Termination reason: Refutation not found, incomplete strategy % 15.33/3.05 % (3070299)Time elapsed: 0.048 s % 15.33/3.05 % (3070299)Peak memory usage: 115 MB % 15.33/3.05 % (3070299)Instructions burned: 109 (million) % 15.33/3.05 % (3070302)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=3443905245:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi) % 15.33/3.05 % (3070283)Instruction limit reached! % 15.33/3.05 % (3070283)------------------------------ % 15.33/3.05 % (3070283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.33/3.05 % (3070283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.33/3.05 % (3070283)CaDiCaL version: 2.1.3 % 15.33/3.05 % (3070283)Termination reason: Instruction limit % 15.33/3.05 % (3070283)Termination phase: Saturation % 15.33/3.05 % (3070283)Time elapsed: 0.441 s % 16.87/3.45 % (3070283)Peak memory usage: 140 MB % 16.87/3.45 % (3070283)Instructions burned: 599 (million) % 16.87/3.45 % (3070302)Instruction limit reached! % 16.87/3.45 % (3070302)------------------------------ % 16.87/3.45 % (3070302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.45 % (3070302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.45 % (3070302)CaDiCaL version: 2.1.3 % 16.87/3.45 % (3070302)Termination reason: Instruction limit % 16.87/3.45 % (3070302)Termination phase: Property scanning % 16.87/3.45 % (3070302)Time elapsed: 0.021 s % 16.87/3.45 % (3070302)Peak memory usage: 87 MB % 16.87/3.45 % (3070302)Instructions burned: 40 (million) % 16.87/3.45 % (3070304)dis+1010_1_to=kbo:si=on:random_seed=1794264662:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi) % 16.87/3.45 % (3070299)------------------------------ % 16.87/3.45 % (3070299)------------------------------ % 16.87/3.45 % (3070306)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2122007860:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi) % 16.87/3.45 % (3070307)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=266843975:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 16.87/3.45 % (3070304)Instruction limit reached! % 16.87/3.45 % (3070304)------------------------------ % 16.87/3.45 % (3070304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.45 % (3070304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.45 % (3070304)CaDiCaL version: 2.1.3 % 16.87/3.45 % (3070304)Termination reason: Instruction limit % 16.87/3.45 % (3070304)Termination phase: Saturation % 16.87/3.45 % (3070304)Time elapsed: 0.103 s % 16.87/3.45 % (3070304)Peak memory usage: 91 MB % 16.87/3.45 % (3070304)Instructions burned: 175 (million) % 16.87/3.45 % (3070311)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2170594609:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi) % 16.87/3.45 % (3070309)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2340009885:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi) % 16.87/3.45 % (3070314)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3987690782:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi) % 16.87/3.45 % (3070314)Refutation not found, incomplete strategy % 16.87/3.45 % (3070314)------------------------------ % 16.87/3.45 % (3070314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.45 % (3070314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.45 % (3070314)CaDiCaL version: 2.1.3 % 16.87/3.45 % (3070314)Termination reason: Refutation not found, incomplete strategy % 16.87/3.45 % (3070314)Time elapsed: 0.006 s % 16.87/3.45 % (3070314)Peak memory usage: 88 MB % 16.87/3.45 % (3070314)Instructions burned: 23 (million) % 16.87/3.45 % (3070289)Instruction limit reached! % 16.87/3.45 % (3070289)------------------------------ % 16.87/3.45 % (3070289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.45 % (3070289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.45 % (3070289)CaDiCaL version: 2.1.3 % 16.87/3.45 % (3070289)Termination reason: Instruction limit % 16.87/3.45 % (3070289)Termination phase: Saturation % 16.87/3.45 % (3070289)Time elapsed: 0.548 s % 16.87/3.45 % (3070289)Peak memory usage: 95 MB % 16.87/3.45 % (3070289)Instructions burned: 1001 (million) % 16.87/3.45 % (3070315)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3888156374:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 16.87/3.45 % (3070306)Instruction limit reached! % 16.87/3.45 % (3070306)------------------------------ % 16.87/3.45 % (3070306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.87/3.45 % (3070306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.87/3.45 % (3070306)CaDiCaL version: 2.1.3 % 16.87/3.45 % (3070306)Termination reason: Instruction limit % 16.87/3.45 % (3070306)Termination phase: Saturation % 16.87/3.45 % (3070306)Time elapsed: 0.215 s % 16.87/3.45 % (3070306)Peak memory usage: 119 MB % 16.87/3.45 % (3070306)Instructions burned: 329 (million) % 16.87/3.45 % (3070309)Instruction limit reached! % 18.02/3.68 % (3070309)------------------------------ % 18.02/3.68 % (3070309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.02/3.68 % (3070309)CaDiCaL version: 2.1.3 % 18.02/3.68 % (3070309)Termination reason: Instruction limit % 18.02/3.68 % (3070309)Termination phase: Saturation % 18.02/3.68 % (3070309)Time elapsed: 0.161 s % 18.02/3.68 % (3070309)Peak memory usage: 139 MB % 18.02/3.68 % (3070309)Instructions burned: 216 (million) % 18.02/3.68 % (3070314)------------------------------ % 18.02/3.68 % (3070314)------------------------------ % 18.02/3.68 % (3070319)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=730989072:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi) % 18.02/3.68 % (3070311)Instruction limit reached! % 18.02/3.68 % (3070311)------------------------------ % 18.02/3.68 % (3070311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.02/3.68 % (3070311)CaDiCaL version: 2.1.3 % 18.02/3.68 % (3070311)Termination reason: Instruction limit % 18.02/3.68 % (3070311)Termination phase: Saturation % 18.02/3.68 % (3070311)Time elapsed: 0.231 s % 18.02/3.68 % (3070311)Peak memory usage: 120 MB % 18.02/3.68 % (3070311)Instructions burned: 350 (million) % 18.02/3.68 % (3070307)Instruction limit reached! % 18.02/3.68 % (3070307)------------------------------ % 18.02/3.68 % (3070307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.02/3.68 % (3070307)CaDiCaL version: 2.1.3 % 18.02/3.68 % (3070307)Termination reason: Instruction limit % 18.02/3.68 % (3070307)Termination phase: Saturation % 18.02/3.68 % (3070307)Time elapsed: 0.340 s % 18.02/3.68 % (3070307)Peak memory usage: 137 MB % 18.02/3.68 % (3070307)Instructions burned: 483 (million) % 18.02/3.68 % (3070321)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2569671501:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/484Mi) % 18.02/3.68 % (3070321)Refutation not found, incomplete strategy % 18.02/3.68 % (3070321)------------------------------ % 18.02/3.68 % (3070321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.02/3.68 % (3070321)CaDiCaL version: 2.1.3 % 18.02/3.68 % (3070321)Termination reason: Refutation not found, incomplete strategy % 18.02/3.68 % (3070321)Time elapsed: 0.011 s % 18.02/3.68 % (3070321)Peak memory usage: 88 MB % 18.02/3.68 % (3070321)Instructions burned: 22 (million) % 18.02/3.68 % (3070323)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2922898372:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 18.02/3.68 % (3070322)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2378903978:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi) % 18.02/3.68 % (3070323)Refutation not found, incomplete strategy % 18.02/3.68 % (3070323)------------------------------ % 18.02/3.68 % (3070323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.02/3.68 % (3070323)CaDiCaL version: 2.1.3 % 18.02/3.68 % (3070323)Termination reason: Refutation not found, incomplete strategy % 18.02/3.68 % (3070323)Time elapsed: 0.021 s % 18.02/3.68 % (3070323)Peak memory usage: 112 MB % 18.02/3.68 % (3070323)Instructions burned: 26 (million) % 18.02/3.68 % (3070315)Instruction limit reached! % 18.02/3.68 % (3070315)------------------------------ % 18.02/3.68 % (3070315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.02/3.68 % (3070315)CaDiCaL version: 2.1.3 % 18.02/3.68 % (3070315)Termination reason: Instruction limit % 18.02/3.68 % (3070315)Termination phase: Saturation % 18.02/3.68 % (3070315)Time elapsed: 0.222 s % 18.02/3.68 % (3070315)Peak memory usage: 119 MB % 18.02/3.68 % (3070315)Instructions burned: 328 (million) % 18.02/3.68 % (3070322)Refutation not found, incomplete strategy % 18.02/3.68 % (3070322)------------------------------ % 18.02/3.68 % (3070322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.02/3.68 % (3070322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/4.06 % (3070322)CaDiCaL version: 2.1.3 % 22.03/4.06 % (3070322)Termination reason: Refutation not found, incomplete strategy % 22.03/4.06 % (3070322)Time elapsed: 0.037 s % 22.03/4.06 % (3070322)Peak memory usage: 112 MB % 22.03/4.06 % (3070322)Instructions burned: 27 (million) % 22.03/4.06 % (3070325)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=110757102:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi) % 22.03/4.06 % (3070319)Instruction limit reached! % 22.03/4.06 % (3070319)------------------------------ % 22.03/4.06 % (3070319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.03/4.06 % (3070319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/4.06 % (3070319)CaDiCaL version: 2.1.3 % 22.03/4.06 % (3070319)Termination reason: Instruction limit % 22.03/4.06 % (3070319)Termination phase: Saturation % 22.03/4.06 % (3070319)Time elapsed: 0.166 s % 22.03/4.06 % (3070319)Peak memory usage: 118 MB % 22.03/4.06 % (3070319)Instructions burned: 282 (million) % 22.03/4.06 % (3070326)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=3027499962:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 22.03/4.06 % (3070323)------------------------------ % 22.03/4.06 % (3070323)------------------------------ % 22.03/4.06 % (3070330)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4016642441:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi) % 22.03/4.06 % (3070321)------------------------------ % 22.03/4.06 % (3070321)------------------------------ % 22.03/4.06 % (3070332)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=435947774:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi) % 22.03/4.06 % (3070332)Refutation not found, incomplete strategy % 22.03/4.06 % (3070332)------------------------------ % 22.03/4.06 % (3070332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.03/4.06 % (3070332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/4.06 % (3070332)CaDiCaL version: 2.1.3 % 22.03/4.06 % (3070332)Termination reason: Refutation not found, incomplete strategy % 22.03/4.06 % (3070332)Time elapsed: 0.038 s % 22.03/4.06 % (3070332)Peak memory usage: 112 MB % 22.03/4.06 % (3070332)Instructions burned: 29 (million) % 22.03/4.06 % (3070322)------------------------------ % 22.03/4.06 % (3070322)------------------------------ % 22.03/4.06 % (3070334)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=4048594376:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 22.03/4.06 % (3070326)Instruction limit reached! % 22.03/4.06 % (3070326)------------------------------ % 22.03/4.06 % (3070326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.03/4.06 % (3070326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/4.06 % (3070326)CaDiCaL version: 2.1.3 % 22.03/4.06 % (3070326)Termination reason: Instruction limit % 22.03/4.06 % (3070326)Termination phase: Saturation % 22.03/4.06 % (3070326)Time elapsed: 0.224 s % 22.03/4.06 % (3070326)Peak memory usage: 136 MB % 22.03/4.06 % (3070326)Instructions burned: 277 (million) % 22.03/4.06 % (3070325)Instruction limit reached! % 22.03/4.06 % (3070325)------------------------------ % 22.03/4.06 % (3070325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.03/4.06 % (3070325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/4.06 % (3070325)CaDiCaL version: 2.1.3 % 22.03/4.06 % (3070325)Termination reason: Instruction limit % 22.03/4.06 % (3070325)Termination phase: Saturation % 22.03/4.06 % (3070325)Time elapsed: 0.305 s % 22.03/4.06 % (3070325)Peak memory usage: 121 MB % 22.03/4.06 % (3070325)Instructions burned: 472 (million) % 22.03/4.06 % (3070336)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1941778098:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi) % 22.03/4.06 % (3070330)Instruction limit reached! % 22.03/4.06 % (3070330)------------------------------ % 22.03/4.06 % (3070330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.03/4.06 % (3070330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.03/4.06 % (3070330)CaDiCaL version: 2.1.3 % 24.28/4.47 % (3070330)Termination reason: Instruction limit % 24.28/4.47 % (3070330)Termination phase: Saturation % 24.28/4.47 % (3070330)Time elapsed: 0.238 s % 24.28/4.47 % (3070330)Peak memory usage: 120 MB % 24.28/4.47 % (3070330)Instructions burned: 375 (million) % 24.28/4.47 % (3070339)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=153028885:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi) % 24.28/4.47 % (3070334)Instruction limit reached! % 24.28/4.47 % (3070334)------------------------------ % 24.28/4.47 % (3070334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.47 % (3070334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.47 % (3070334)CaDiCaL version: 2.1.3 % 24.28/4.47 % (3070334)Termination reason: Instruction limit % 24.28/4.47 % (3070334)Termination phase: Saturation % 24.28/4.47 % (3070334)Time elapsed: 0.173 s % 24.28/4.47 % (3070334)Peak memory usage: 94 MB % 24.28/4.47 % (3070334)Instructions burned: 514 (million) % 24.28/4.47 % (3070340)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2911449864:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi) % 24.28/4.47 % (3070332)------------------------------ % 24.28/4.47 % (3070332)------------------------------ % 24.28/4.47 % (3070342)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2267394580:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi) % 24.28/4.47 % (3070342)Refutation not found, incomplete strategy % 24.28/4.47 % (3070342)------------------------------ % 24.28/4.47 % (3070342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.47 % (3070342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.47 % (3070342)CaDiCaL version: 2.1.3 % 24.28/4.47 % (3070342)Termination reason: Refutation not found, incomplete strategy % 24.28/4.47 % (3070342)Time elapsed: 0.034 s % 24.28/4.47 % (3070342)Peak memory usage: 111 MB % 24.28/4.47 % (3070342)Instructions burned: 19 (million) % 24.28/4.47 % (3070345)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1001461503:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi) % 24.28/4.47 % (3070343)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=2095412975:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi) % 24.28/4.47 % (3070343)Refutation not found, incomplete strategy % 24.28/4.47 % (3070343)------------------------------ % 24.28/4.47 % (3070343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.47 % (3070343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.47 % (3070343)CaDiCaL version: 2.1.3 % 24.28/4.47 % (3070343)Termination reason: Refutation not found, incomplete strategy % 24.28/4.47 % (3070343)Time elapsed: 0.038 s % 24.28/4.47 % (3070343)Peak memory usage: 112 MB % 24.28/4.47 % (3070343)Instructions burned: 28 (million) % 24.28/4.47 % (3070336)Instruction limit reached! % 24.28/4.47 % (3070336)------------------------------ % 24.28/4.47 % (3070336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.47 % (3070336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.47 % (3070336)CaDiCaL version: 2.1.3 % 24.28/4.47 % (3070336)Termination reason: Instruction limit % 24.28/4.47 % (3070336)Termination phase: Saturation % 24.28/4.47 % (3070336)Time elapsed: 0.250 s % 24.28/4.47 % (3070336)Peak memory usage: 137 MB % 24.28/4.47 % (3070336)Instructions burned: 335 (million) % 24.28/4.47 % (3070339)Instruction limit reached! % 24.28/4.47 % (3070339)------------------------------ % 24.28/4.47 % (3070339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.47 % (3070339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.47 % (3070339)CaDiCaL version: 2.1.3 % 24.28/4.47 % (3070339)Termination reason: Instruction limit % 24.28/4.47 % (3070339)Termination phase: Saturation % 24.28/4.47 % (3070339)Time elapsed: 0.201 s % 24.28/4.47 % (3070339)Peak memory usage: 93 MB % 24.28/4.47 % (3070339)Instructions burned: 359 (million) % 24.28/4.47 % (3070345)Instruction limit reached! % 24.28/4.47 % (3070345)------------------------------ % 24.28/4.47 % (3070345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.47 % (3070345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/5.01 % (3070345)CaDiCaL version: 2.1.3 % 27.23/5.01 % (3070345)Termination reason: Instruction limit % 27.23/5.01 % (3070345)Termination phase: Saturation % 27.23/5.01 % (3070345)Time elapsed: 0.090 s % 27.23/5.01 % (3070345)Peak memory usage: 92 MB % 27.23/5.01 % (3070345)Instructions burned: 273 (million) % 27.23/5.01 % (3070347)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=278255173:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi) % 27.23/5.01 % (3070340)Instruction limit reached! % 27.23/5.01 % (3070340)------------------------------ % 27.23/5.01 % (3070340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/5.01 % (3070340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/5.01 % (3070340)CaDiCaL version: 2.1.3 % 27.23/5.01 % (3070340)Termination reason: Instruction limit % 27.23/5.01 % (3070340)Termination phase: Saturation % 27.23/5.01 % (3070340)Time elapsed: 0.220 s % 27.23/5.01 % (3070340)Peak memory usage: 123 MB % 27.23/5.01 % (3070340)Instructions burned: 342 (million) % 27.23/5.01 % (3070347)Instruction limit reached! % 27.23/5.01 % (3070347)------------------------------ % 27.23/5.01 % (3070347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/5.01 % (3070347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/5.01 % (3070347)CaDiCaL version: 2.1.3 % 27.23/5.01 % (3070347)Termination reason: Instruction limit % 27.23/5.01 % (3070347)Termination phase: Saturation % 27.23/5.01 % (3070347)Time elapsed: 0.084 s % 27.23/5.01 % (3070347)Peak memory usage: 91 MB % 27.23/5.01 % (3070347)Instructions burned: 147 (million) % 27.23/5.01 % (3070351)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1298102027:i=4428:doe=on:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/4428Mi) % 27.23/5.01 % (3070352)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=716607769:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi) % 27.23/5.01 % (3070342)------------------------------ % 27.23/5.01 % (3070342)------------------------------ % 27.23/5.01 % (3070353)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=978230298:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi) % 27.23/5.01 % (3070343)------------------------------ % 27.23/5.01 % (3070343)------------------------------ % 27.23/5.01 % (3070355)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3243183023:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2971 on theBenchmark for (2971ds/655Mi) % 27.23/5.01 % (3070356)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=283009583:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi) % 27.23/5.01 % (3070356)Refutation not found, incomplete strategy % 27.23/5.01 % (3070356)------------------------------ % 27.23/5.01 % (3070356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/5.01 % (3070356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/5.01 % (3070356)CaDiCaL version: 2.1.3 % 27.23/5.01 % (3070356)Termination reason: Refutation not found, incomplete strategy % 27.23/5.01 % (3070356)Time elapsed: 0.004 s % 27.23/5.01 % (3070356)Peak memory usage: 88 MB % 27.23/5.01 % (3070356)Instructions burned: 15 (million) % 27.23/5.01 % (3070360)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3703557427:i=107:rtra=on_2970 on theBenchmark for (2970ds/107Mi) % 27.23/5.01 % (3070352)Instruction limit reached! % 27.23/5.01 % (3070352)------------------------------ % 27.23/5.01 % (3070352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/5.01 % (3070352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/5.01 % (3070352)CaDiCaL version: 2.1.3 % 27.23/5.01 % (3070352)Termination reason: Instruction limit % 27.23/5.01 % (3070352)Termination phase: Saturation % 27.23/5.01 % (3070352)Time elapsed: 0.212 s % 27.23/5.01 % (3070352)Peak memory usage: 136 MB % 27.23/5.01 % (3070352)Instructions burned: 277 (million) % 27.23/5.01 % (3070356)------------------------------ % 27.23/5.01 % (3070356)------------------------------ % 27.23/5.01 % (3070361)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=387085988:s2a=on:i=450:doe=on:nm=32:rtra=on_2970 on theBenchmark for (2970ds/450Mi) % 31.36/5.35 % (3070360)Refutation not found, incomplete strategy % 31.36/5.35 % (3070360)------------------------------ % 31.36/5.35 % (3070360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.36/5.35 % (3070360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.36/5.35 % (3070360)CaDiCaL version: 2.1.3 % 31.36/5.35 % (3070360)Termination reason: Refutation not found, incomplete strategy % 31.36/5.35 % (3070360)Time elapsed: 0.076 s % 31.36/5.35 % (3070360)Peak memory usage: 115 MB % 31.36/5.35 % (3070360)Instructions burned: 101 (million) % 31.36/5.35 % (3070365)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 % 31.36/5.35 % (3070367)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1972254051:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2968 on theBenchmark for (2968ds/130Mi) % 31.36/5.35 % (3070365)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3873215501:i=1090:aac=none:nm=0:rtra=on:rawr=on_2968 on theBenchmark for (2968ds/1090Mi) % 31.36/5.35 % (3070367)Instruction limit reached! % 31.36/5.35 % (3070367)------------------------------ % 31.36/5.35 % (3070367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.36/5.35 % (3070367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.36/5.35 % (3070367)CaDiCaL version: 2.1.3 % 31.36/5.35 % (3070367)Termination reason: Instruction limit % 31.36/5.35 % (3070367)Termination phase: Saturation % 31.36/5.35 % (3070367)Time elapsed: 0.051 s % 31.36/5.35 % (3070367)Peak memory usage: 118 MB % 31.36/5.35 % (3070367)Instructions burned: 130 (million) % 31.36/5.35 % (3070355)Instruction limit reached! % 31.36/5.35 % (3070355)------------------------------ % 31.36/5.35 % (3070355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.36/5.35 % (3070355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.36/5.35 % (3070355)CaDiCaL version: 2.1.3 % 31.36/5.35 % (3070355)Termination reason: Instruction limit % 31.36/5.35 % (3070355)Termination phase: Saturation % 31.36/5.35 % (3070355)Time elapsed: 0.371 s % 31.36/5.35 % (3070355)Peak memory usage: 94 MB % 31.36/5.35 % (3070355)Instructions burned: 656 (million) % 31.36/5.35 % (3070360)------------------------------ % 31.36/5.35 % (3070360)------------------------------ % 31.36/5.35 % (3070370)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=772891568:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi) % 31.36/5.35 % (3070361)Instruction limit reached! % 31.36/5.35 % (3070361)------------------------------ % 31.36/5.35 % (3070361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.36/5.35 % (3070361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.36/5.35 % (3070361)CaDiCaL version: 2.1.3 % 31.36/5.35 % (3070361)Termination reason: Instruction limit % 31.36/5.35 % (3070361)Termination phase: Saturation % 31.36/5.35 % (3070361)Time elapsed: 0.318 s % 31.36/5.35 % (3070361)Peak memory usage: 136 MB % 31.36/5.35 % (3070361)Instructions burned: 451 (million) % 31.36/5.35 % (3070353)Instruction limit reached! % 31.36/5.35 % (3070353)------------------------------ % 31.36/5.35 % (3070353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.36/5.35 % (3070353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.36/5.35 % (3070353)CaDiCaL version: 2.1.3 % 31.36/5.35 % (3070353)Termination reason: Instruction limit % 31.36/5.35 % (3070353)Termination phase: Saturation % 31.36/5.35 % (3070353)Time elapsed: 0.568 s % 31.36/5.35 % (3070353)Peak memory usage: 98 MB % 31.36/5.35 % (3070353)Instructions burned: 1053 (million) % 31.36/5.35 % (3070371)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2303193721:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi) % 31.36/5.35 % (3070370)Instruction limit reached! % 31.36/5.35 % (3070370)------------------------------ % 31.36/5.35 % (3070370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.36/5.35 % (3070370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.36/5.35 % (3070370)CaDiCaL version: 2.1.3 % 31.36/5.35 % (3070370)Termination reason: Instruction limit % 31.36/5.35 % (3070370)Termination phase: Saturation % 31.36/5.35 % (3070370)Time elapsed: 0.116 s % 31.36/5.35 % (3070370)Peak memory usage: 119 MB % 32.71/5.93 % (3070370)Instructions burned: 313 (million) % 32.71/5.93 % (3070371)Refutation not found, incomplete strategy % 32.71/5.93 % (3070371)------------------------------ % 32.71/5.93 % (3070371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.71/5.93 % (3070371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.71/5.93 % (3070371)CaDiCaL version: 2.1.3 % 32.71/5.93 % (3070371)Termination reason: Refutation not found, incomplete strategy % 32.71/5.93 % (3070371)Time elapsed: 0.054 s % 32.71/5.93 % (3070371)Peak memory usage: 91 MB % 32.71/5.93 % (3070371)Instructions burned: 103 (million) % 32.71/5.93 % (3070372)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3186143522:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi) % 32.71/5.93 % (3070374)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=4182233015:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi) % 32.71/5.93 % (3070376)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2669062247:i=776:doe=on:rtra=on_2964 on theBenchmark for (2964ds/776Mi) % 32.71/5.93 % (3070377)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1566822763:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/646Mi) % 32.71/5.93 % (3070374)Refutation not found, incomplete strategy % 32.71/5.93 % (3070374)------------------------------ % 32.71/5.93 % (3070374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.71/5.93 % (3070374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.71/5.93 % (3070374)CaDiCaL version: 2.1.3 % 32.71/5.93 % (3070374)Termination reason: Refutation not found, incomplete strategy % 32.71/5.93 % (3070374)Time elapsed: 0.072 s % 32.71/5.93 % (3070374)Peak memory usage: 91 MB % 32.71/5.93 % (3070374)Instructions burned: 127 (million) % 32.71/5.93 % (3070371)------------------------------ % 32.71/5.93 % (3070371)------------------------------ % 32.71/5.93 % (3070377)Instruction limit reached! % 32.71/5.93 % (3070377)------------------------------ % 32.71/5.93 % (3070377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.71/5.93 % (3070377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.71/5.93 % (3070377)CaDiCaL version: 2.1.3 % 32.71/5.93 % (3070377)Termination reason: Instruction limit % 32.71/5.93 % (3070377)Termination phase: Saturation % 32.71/5.93 % (3070377)Time elapsed: 0.251 s % 32.71/5.93 % (3070377)Peak memory usage: 141 MB % 32.71/5.93 % (3070377)Instructions burned: 648 (million) % 32.71/5.93 % (3070365)Instruction limit reached! % 32.71/5.93 % (3070365)------------------------------ % 32.71/5.93 % (3070365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.71/5.93 % (3070365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.71/5.93 % (3070365)CaDiCaL version: 2.1.3 % 32.71/5.93 % (3070365)Termination reason: Instruction limit % 32.71/5.93 % (3070365)Termination phase: Saturation % 32.71/5.93 % (3070365)Time elapsed: 0.665 s % 32.71/5.93 % (3070365)Peak memory usage: 125 MB % 32.71/5.93 % (3070365)Instructions burned: 1090 (million) % 32.71/5.93 % (3070374)------------------------------ % 32.71/5.93 % (3070374)------------------------------ % 32.71/5.93 % (3070382)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=3573235123:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2961 on theBenchmark for (2961ds/784Mi) % 32.71/5.93 % (3070383)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=727773873:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2960 on theBenchmark for (2960ds/1131Mi) % 32.71/5.93 % (3070372)Instruction limit reached! % 32.71/5.93 % (3070372)------------------------------ % 32.71/5.93 % (3070372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.71/5.93 % (3070372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.71/5.93 % (3070372)CaDiCaL version: 2.1.3 % 32.71/5.93 % (3070372)Termination reason: Instruction limit % 32.71/5.93 % (3070372)Termination phase: Saturation % 32.71/5.93 % (3070372)Time elapsed: 0.476 s % 32.71/5.93 % (3070372)Peak memory usage: 97 MB % 32.71/5.93 % (3070372)Instructions burned: 835 (million) % 32.71/5.93 % (3070384)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=2123862796:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi) % 39.73/6.69 % (3070385)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3813376575:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi) % 39.73/6.69 % (3070376)Instruction limit reached! % 39.73/6.69 % (3070376)------------------------------ % 39.73/6.69 % (3070376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.73/6.69 % (3070376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.73/6.69 % (3070376)CaDiCaL version: 2.1.3 % 39.73/6.69 % (3070376)Termination reason: Instruction limit % 39.73/6.69 % (3070376)Termination phase: Saturation % 39.73/6.69 % (3070376)Time elapsed: 0.470 s % 39.73/6.69 % (3070376)Peak memory usage: 124 MB % 39.73/6.69 % (3070376)Instructions burned: 777 (million) % 39.73/6.69 % (3070385)Refutation not found, incomplete strategy % 39.73/6.69 % (3070385)------------------------------ % 39.73/6.69 % (3070385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.73/6.69 % (3070385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.73/6.69 % (3070385)CaDiCaL version: 2.1.3 % 39.73/6.69 % (3070385)Termination reason: Refutation not found, incomplete strategy % 39.73/6.69 % (3070385)Time elapsed: 0.013 s % 39.73/6.69 % (3070385)Peak memory usage: 88 MB % 39.73/6.69 % (3070385)Instructions burned: 25 (million) % 39.73/6.69 % (3070384)Refutation not found, incomplete strategy % 39.73/6.69 % (3070384)------------------------------ % 39.73/6.69 % (3070384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.73/6.69 % (3070384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.73/6.69 % (3070384)CaDiCaL version: 2.1.3 % 39.73/6.69 % (3070384)Termination reason: Refutation not found, incomplete strategy % 39.73/6.69 % (3070384)Time elapsed: 0.038 s % 39.73/6.69 % (3070384)Peak memory usage: 112 MB % 39.73/6.69 % (3070384)Instructions burned: 28 (million) % 39.73/6.69 % (3070388)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=835670103:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 39.73/6.69 % (3070391)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1751387131:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi) % 39.73/6.69 % (3070391)Instruction limit reached! % 39.73/6.69 % (3070391)------------------------------ % 39.73/6.69 % (3070391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.73/6.69 % (3070391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.73/6.69 % (3070391)CaDiCaL version: 2.1.3 % 39.73/6.69 % (3070391)Termination reason: Instruction limit % 39.73/6.69 % (3070391)Termination phase: Saturation % 39.73/6.69 % (3070391)Time elapsed: 0.054 s % 39.73/6.69 % (3070391)Peak memory usage: 90 MB % 39.73/6.69 % (3070391)Instructions burned: 103 (million) % 39.73/6.69 % (3070388)Instruction limit reached! % 39.73/6.69 % (3070388)------------------------------ % 39.73/6.69 % (3070388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.73/6.69 % (3070388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.73/6.69 % (3070388)CaDiCaL version: 2.1.3 % 39.73/6.69 % (3070388)Termination reason: Instruction limit % 39.73/6.69 % (3070388)Termination phase: Saturation % 39.73/6.69 % (3070388)Time elapsed: 0.165 s % 39.73/6.69 % (3070388)Peak memory usage: 92 MB % 39.73/6.69 % (3070388)Instructions burned: 274 (million) % 39.73/6.69 % (3070385)------------------------------ % 39.73/6.69 % (3070385)------------------------------ % 39.73/6.69 % (3070384)------------------------------ % 39.73/6.69 % (3070384)------------------------------ % 39.73/6.69 % (3070382)Instruction limit reached! % 39.73/6.69 % (3070382)------------------------------ % 39.73/6.69 % (3070382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.73/6.69 % (3070382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.73/6.69 % (3070382)CaDiCaL version: 2.1.3 % 39.73/6.69 % (3070382)Termination reason: Instruction limit % 39.73/6.69 % (3070382)Termination phase: Saturation % 39.73/6.69 % (3070382)Time elapsed: 0.470 s % 39.73/6.69 % (3070382)Peak memory usage: 121 MB % 39.73/6.69 % (3070382)Instructions burned: 785 (million) % 39.73/6.69 % (3070383)Instruction limit reached! % 39.73/6.69 % (3070383)------------------------------ % 39.73/6.69 % (3070383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.90/8.27 % (3070383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.90/8.27 % (3070383)CaDiCaL version: 2.1.3 % 51.90/8.27 % (3070383)Termination reason: Instruction limit % 51.90/8.27 % (3070383)Termination phase: Saturation % 51.90/8.27 % (3070383)Time elapsed: 0.389 s % 51.90/8.27 % (3070383)Peak memory usage: 133 MB % 51.90/8.27 % (3070383)Instructions burned: 1132 (million) % 51.90/8.27 % (3070394)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=238906466:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2956 on theBenchmark for (2956ds/1094Mi) % 51.90/8.27 % (3070395)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2806302015:i=6400:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/6400Mi) % 51.90/8.27 % (3070396)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=2220775259:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/868Mi) % 51.90/8.27 % (3070397)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=875343561:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi) % 51.90/8.27 % (3070399)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3984224502:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi) % 51.90/8.27 % (3070398)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3292071329:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi) % 51.90/8.27 % (3070397)Refutation not found, incomplete strategy % 51.90/8.27 % (3070397)------------------------------ % 51.90/8.27 % (3070397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.90/8.27 % (3070397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.90/8.27 % (3070397)CaDiCaL version: 2.1.3 % 51.90/8.27 % (3070397)Termination reason: Refutation not found, incomplete strategy % 51.90/8.27 % (3070397)Time elapsed: 0.051 s % 51.90/8.27 % (3070397)Peak memory usage: 91 MB % 51.90/8.27 % (3070397)Instructions burned: 97 (million) % 51.90/8.27 % (3070399)Instruction limit reached! % 51.90/8.27 % (3070399)------------------------------ % 51.90/8.27 % (3070399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.90/8.27 % (3070399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.90/8.27 % (3070399)CaDiCaL version: 2.1.3 % 51.90/8.27 % (3070399)Termination reason: Instruction limit % 51.90/8.27 % (3070399)Termination phase: Saturation % 51.90/8.27 % (3070399)Time elapsed: 0.090 s % 51.90/8.27 % (3070399)Peak memory usage: 92 MB % 51.90/8.27 % (3070399)Instructions burned: 274 (million) % 51.90/8.27 % (3070406)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=2918040986:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/863Mi) % 51.90/8.27 % (3070397)------------------------------ % 51.90/8.27 % (3070397)------------------------------ % 51.90/8.27 % (3070351)Instruction limit reached! % 51.90/8.27 % (3070351)------------------------------ % 51.90/8.27 % (3070351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.90/8.27 % (3070351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.90/8.27 % (3070351)CaDiCaL version: 2.1.3 % 51.90/8.27 % (3070351)Termination reason: Instruction limit % 51.90/8.27 % (3070351)Termination phase: Saturation % 51.90/8.27 % (3070351)Time elapsed: 2.065 s % 51.90/8.27 % (3070351)Peak memory usage: 108 MB % 51.90/8.27 % (3070351)Instructions burned: 4428 (million) % 51.90/8.27 % (3070408)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3469500546:i=5811:kws=precedence:nm=0:rtra=on_2951 on theBenchmark for (2951ds/5811Mi) % 51.90/8.27 % (3070396)Instruction limit reached! % 51.90/8.27 % (3070396)------------------------------ % 51.90/8.27 % (3070396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.90/8.27 % (3070396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.90/8.27 % (3070396)CaDiCaL version: 2.1.3 % 51.90/8.27 % (3070396)Termination reason: Instruction limit % 51.90/8.27 % (3070396)Termination phase: Saturation % 51.90/8.27 % (3070396)Time elapsed: 0.493 s % 59.69/9.51 % (3070396)Peak memory usage: 122 MB % 59.69/9.51 % (3070396)Instructions burned: 869 (million) % 59.69/9.51 % (3070406)Instruction limit reached! % 59.69/9.51 % (3070406)------------------------------ % 59.69/9.51 % (3070406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.69/9.51 % (3070406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.69/9.51 % (3070406)CaDiCaL version: 2.1.3 % 59.69/9.51 % (3070406)Termination reason: Instruction limit % 59.69/9.51 % (3070406)Termination phase: Saturation % 59.69/9.51 % (3070406)Time elapsed: 0.264 s % 59.69/9.51 % (3070406)Peak memory usage: 122 MB % 59.69/9.51 % (3070406)Instructions burned: 863 (million) % 59.69/9.51 % (3070394)Instruction limit reached! % 59.69/9.51 % (3070394)------------------------------ % 59.69/9.51 % (3070394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.69/9.51 % (3070394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.69/9.51 % (3070394)CaDiCaL version: 2.1.3 % 59.69/9.51 % (3070394)Termination reason: Instruction limit % 59.69/9.51 % (3070394)Termination phase: Saturation % 59.69/9.51 % (3070394)Time elapsed: 0.609 s % 59.69/9.51 % (3070394)Peak memory usage: 96 MB % 59.69/9.51 % (3070394)Instructions burned: 1094 (million) % 59.69/9.51 % (3070409)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=2563732626:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2950 on theBenchmark for (2950ds/2216Mi) % 59.69/9.51 % (3070411)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=79057702:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2949 on theBenchmark for (2949ds/801Mi) % 59.69/9.51 % (3070412)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2425959936:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2949 on theBenchmark for (2949ds/1026Mi) % 59.69/9.51 % (3070412)Refutation not found, incomplete strategy % 59.69/9.51 % (3070412)------------------------------ % 59.69/9.51 % (3070412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.69/9.51 % (3070412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.69/9.51 % (3070412)CaDiCaL version: 2.1.3 % 59.69/9.51 % (3070412)Termination reason: Refutation not found, incomplete strategy % 59.69/9.51 % (3070412)Time elapsed: 0.008 s % 59.69/9.51 % (3070412)Peak memory usage: 87 MB % 59.69/9.51 % (3070412)Instructions burned: 15 (million) % 59.69/9.51 % (3070414)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3827040894:i=3509:rtra=on_2948 on theBenchmark for (2948ds/3509Mi) % 59.69/9.51 % (3070411)Instruction limit reached! % 59.69/9.51 % (3070411)------------------------------ % 59.69/9.51 % (3070411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.69/9.51 % (3070411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.69/9.51 % (3070411)CaDiCaL version: 2.1.3 % 59.69/9.51 % (3070411)Termination reason: Instruction limit % 59.69/9.51 % (3070411)Termination phase: Saturation % 59.69/9.51 % (3070411)Time elapsed: 0.243 s % 59.69/9.51 % (3070411)Peak memory usage: 95 MB % 59.69/9.51 % (3070411)Instructions burned: 804 (million) % 59.69/9.51 % (3070412)------------------------------ % 59.69/9.51 % (3070412)------------------------------ % 59.69/9.51 % (3070418)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3256900462:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2946 on theBenchmark for (2946ds/2127Mi) % 59.69/9.51 % (3070418)Refutation not found, incomplete strategy % 59.69/9.51 % (3070418)------------------------------ % 59.69/9.51 % (3070418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.69/9.51 % (3070418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.69/9.51 % (3070418)CaDiCaL version: 2.1.3 % 59.69/9.51 % (3070418)Termination reason: Refutation not found, incomplete strategy % 59.69/9.51 % (3070418)Time elapsed: 0.006 s % 59.69/9.51 % (3070418)Peak memory usage: 88 MB % 59.69/9.51 % (3070418)Instructions burned: 23 (million) % 59.69/9.51 % (3070419)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3204690257:i=1959:rtra=on:fsd=on:proc=on_2945 on theBenchmark for (2945ds/1959Mi) % 59.69/9.51 % (3070418)------------------------------ % 59.69/9.51 % (3070418)------------------------------ % 59.69/9.51 % (3070422)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2570762398:s2a=on:i=3553:nm=0:rtra=on_2943 on theBenchmark for (2943ds/3553Mi) % 99.52/15.04 % (3070409)Instruction limit reached! % 99.52/15.04 % (3070409)------------------------------ % 99.52/15.04 % (3070409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.04 % (3070409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.04 % (3070409)CaDiCaL version: 2.1.3 % 99.52/15.04 % (3070409)Termination reason: Instruction limit % 99.52/15.04 % (3070409)Termination phase: Saturation % 99.52/15.04 % (3070409)Time elapsed: 1.244 s % 99.52/15.04 % (3070409)Peak memory usage: 134 MB % 99.52/15.04 % (3070409)Instructions burned: 2216 (million) % 99.52/15.04 % (3070540)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1860901572:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2936 on theBenchmark for (2936ds/3201Mi) % 99.52/15.04 % (3070419)Instruction limit reached! % 99.52/15.04 % (3070419)------------------------------ % 99.52/15.04 % (3070419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.04 % (3070419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.04 % (3070419)CaDiCaL version: 2.1.3 % 99.52/15.04 % (3070419)Termination reason: Instruction limit % 99.52/15.04 % (3070419)Termination phase: Saturation % 99.52/15.04 % (3070419)Time elapsed: 1.167 s % 99.52/15.04 % (3070419)Peak memory usage: 140 MB % 99.52/15.04 % (3070419)Instructions burned: 1959 (million) % 99.52/15.04 % (3070551)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=3127702998:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2932 on theBenchmark for (2932ds/4093Mi) % 99.52/15.04 % (3070422)Instruction limit reached! % 99.52/15.04 % (3070422)------------------------------ % 99.52/15.04 % (3070422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.04 % (3070422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.04 % (3070422)CaDiCaL version: 2.1.3 % 99.52/15.04 % (3070422)Termination reason: Instruction limit % 99.52/15.04 % (3070422)Termination phase: Saturation % 99.52/15.04 % (3070422)Time elapsed: 1.172 s % 99.52/15.04 % (3070422)Peak memory usage: 118 MB % 99.52/15.04 % (3070422)Instructions burned: 3554 (million) % 99.52/15.04 % (3070608)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=3375738896:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 99.52/15.04 % (3070608)Refutation not found, incomplete strategy % 99.52/15.04 % (3070608)------------------------------ % 99.52/15.04 % (3070608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.04 % (3070608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.04 % (3070608)CaDiCaL version: 2.1.3 % 99.52/15.04 % (3070608)Termination reason: Refutation not found, incomplete strategy % 99.52/15.04 % (3070608)Time elapsed: 0.020 s % 99.52/15.04 % (3070608)Peak memory usage: 113 MB % 99.52/15.04 % (3070608)Instructions burned: 17 (million) % 99.52/15.04 % (3070608)------------------------------ % 99.52/15.04 % (3070608)------------------------------ % 99.52/15.04 % (3070395)Instruction limit reached! % 99.52/15.04 % (3070395)------------------------------ % 99.52/15.04 % (3070395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.04 % (3070395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.04 % (3070395)CaDiCaL version: 2.1.3 % 99.52/15.04 % (3070395)Termination reason: Instruction limit % 99.52/15.04 % (3070395)Termination phase: Saturation % 99.52/15.04 % (3070395)Time elapsed: 2.756 s % 99.52/15.04 % (3070395)Peak memory usage: 109 MB % 99.52/15.04 % (3070395)Instructions burned: 6403 (million) % 99.52/15.04 % (3070414)Instruction limit reached! % 99.52/15.04 % (3070414)------------------------------ % 99.52/15.04 % (3070414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.04 % (3070414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.04 % (3070414)CaDiCaL version: 2.1.3 % 99.52/15.04 % (3070414)Termination reason: Instruction limit % 99.52/15.04 % (3070414)Termination phase: Saturation % 99.52/15.04 % (3070414)Time elapsed: 1.995 s % 99.52/15.04 % (3070414)Peak memory usage: 114 MB % 99.52/15.04 % (3070414)Instructions burned: 3510 (million) % 99.52/15.04 % (3070667)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=22520120:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2927 on theBenchmark for (2927ds/10544Mi) % 114.72/17.09 % (3070673)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3910700219:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2927 on theBenchmark for (2927ds/1262Mi) % 114.72/17.09 % (3070678)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=438870818:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2927 on theBenchmark for (2927ds/775Mi) % 114.72/17.09 % (3070678)Refutation not found, incomplete strategy % 114.72/17.09 % (3070678)------------------------------ % 114.72/17.09 % (3070678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.72/17.09 % (3070678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.72/17.09 % (3070678)CaDiCaL version: 2.1.3 % 114.72/17.09 % (3070678)Termination reason: Refutation not found, incomplete strategy % 114.72/17.09 % (3070678)Time elapsed: 0.013 s % 114.72/17.09 % (3070678)Peak memory usage: 88 MB % 114.72/17.09 % (3070678)Instructions burned: 25 (million) % 114.72/17.09 % (3070678)------------------------------ % 114.72/17.09 % (3070678)------------------------------ % 114.72/17.09 % (3070682)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1580330910:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/270Mi) % 114.72/17.09 % (3070682)Instruction limit reached! % 114.72/17.09 % (3070682)------------------------------ % 114.72/17.09 % (3070682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.72/17.09 % (3070682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.72/17.09 % (3070682)CaDiCaL version: 2.1.3 % 114.72/17.09 % (3070682)Termination reason: Instruction limit % 114.72/17.09 % (3070682)Termination phase: Saturation % 114.72/17.09 % (3070682)Time elapsed: 0.229 s % 114.72/17.09 % (3070682)Peak memory usage: 92 MB % 114.72/17.09 % (3070682)Instructions burned: 270 (million) % 114.72/17.09 % (3070540)Instruction limit reached! % 114.72/17.09 % (3070540)------------------------------ % 114.72/17.09 % (3070540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.72/17.09 % (3070540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.72/17.09 % (3070540)CaDiCaL version: 2.1.3 % 114.72/17.09 % (3070540)Termination reason: Instruction limit % 114.72/17.09 % (3070540)Termination phase: Saturation % 114.72/17.09 % (3070540)Time elapsed: 1.584 s % 114.72/17.09 % (3070540)Peak memory usage: 100 MB % 114.72/17.09 % (3070540)Instructions burned: 3201 (million) % 114.72/17.09 % (3070408)Instruction limit reached! % 114.72/17.09 % (3070408)------------------------------ % 114.72/17.09 % (3070408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.72/17.09 % (3070408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.72/17.09 % (3070408)CaDiCaL version: 2.1.3 % 114.72/17.09 % (3070408)Termination reason: Instruction limit % 114.72/17.09 % (3070408)Termination phase: Saturation % 114.72/17.09 % (3070408)Time elapsed: 3.307 s % 114.72/17.09 % (3070408)Peak memory usage: 141 MB % 114.72/17.09 % (3070408)Instructions burned: 5812 (million) % 114.72/17.09 % (3070673)Instruction limit reached! % 114.72/17.09 % (3070673)------------------------------ % 114.72/17.09 % (3070673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.72/17.09 % (3070673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.72/17.09 % (3070673)CaDiCaL version: 2.1.3 % 114.72/17.09 % (3070673)Termination reason: Instruction limit % 114.72/17.09 % (3070673)Termination phase: Saturation % 114.72/17.09 % (3070673)Time elapsed: 0.912 s % 114.72/17.09 % (3070673)Peak memory usage: 126 MB % 114.72/17.09 % (3070673)Instructions burned: 1263 (million) % 114.72/17.09 % (3070696)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3919101394:s2a=on:i=13094:s2at=-1:rtra=on_2919 on theBenchmark for (2919ds/13094Mi) % 114.72/17.09 % (3070695)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1403465626:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2919 on theBenchmark for (2919ds/17165Mi) % 114.72/17.09 % (3070707)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1632960976:st=2:i=12633:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/12633Mi) % 114.72/17.09 % (3070707)Refutation not found, incomplete strategy % 114.72/17.09 % (3070707)------------------------------ % 114.72/17.09 % (3070707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.24/22.06 % (3070707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.24/22.06 % (3070707)CaDiCaL version: 2.1.3 % 150.24/22.06 % (3070707)Termination reason: Refutation not found, incomplete strategy % 150.24/22.06 % (3070707)Time elapsed: 0.019 s % 150.24/22.06 % (3070707)Peak memory usage: 88 MB % 150.24/22.06 % (3070707)Instructions burned: 22 (million) % 150.24/22.06 % (3070709)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2079569537:i=1783:rtra=on:gtg=position_2916 on theBenchmark for (2916ds/1783Mi) % 150.24/22.06 % (3070707)------------------------------ % 150.24/22.06 % (3070707)------------------------------ % 150.24/22.06 % (3070743)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=516312696:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2910 on theBenchmark for (2910ds/5451Mi) % 150.24/22.06 % (3070709)Instruction limit reached! % 150.24/22.06 % (3070709)------------------------------ % 150.24/22.06 % (3070709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.24/22.06 % (3070709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.24/22.06 % (3070709)CaDiCaL version: 2.1.3 % 150.24/22.06 % (3070709)Termination reason: Instruction limit % 150.24/22.06 % (3070709)Termination phase: Saturation % 150.24/22.06 % (3070709)Time elapsed: 1.612 s % 150.24/22.06 % (3070709)Peak memory usage: 128 MB % 150.24/22.06 % (3070709)Instructions burned: 1786 (million) % 150.24/22.06 % (3070551)Instruction limit reached! % 150.24/22.06 % (3070551)------------------------------ % 150.24/22.06 % (3070551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.24/22.06 % (3070551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.24/22.06 % (3070551)CaDiCaL version: 2.1.3 % 150.24/22.06 % (3070551)Termination reason: Instruction limit % 150.24/22.06 % (3070551)Termination phase: Saturation % 150.24/22.06 % (3070551)Time elapsed: 3.351 s % 150.24/22.06 % (3070551)Peak memory usage: 166 MB % 150.24/22.06 % (3070551)Instructions burned: 4095 (million) % 150.24/22.06 % (3070788)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=3539816310:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2897 on theBenchmark for (2897ds/4975Mi) % 150.24/22.06 % (3070789)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=1672059031:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2897 on theBenchmark for (2897ds/2076Mi) % 150.24/22.06 % (3070667)Instruction limit reached! % 150.24/22.06 % (3070667)------------------------------ % 150.24/22.06 % (3070667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.24/22.06 % (3070667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.24/22.06 % (3070667)CaDiCaL version: 2.1.3 % 150.24/22.06 % (3070667)Termination reason: Instruction limit % 150.24/22.06 % (3070667)Termination phase: Saturation % 150.24/22.06 % (3070667)Time elapsed: 4.794 s % 150.24/22.06 % (3070667)Peak memory usage: 238 MB % 150.24/22.06 % (3070667)Instructions burned: 10547 (million) % 150.24/22.06 % (3070789)Instruction limit reached! % 150.24/22.06 % (3070789)------------------------------ % 150.24/22.06 % (3070789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.24/22.06 % (3070789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.24/22.06 % (3070789)CaDiCaL version: 2.1.3 % 150.24/22.06 % (3070789)Termination reason: Instruction limit % 150.24/22.06 % (3070789)Termination phase: Saturation % 150.24/22.06 % (3070789)Time elapsed: 1.843 s % 150.24/22.06 % (3070789)Peak memory usage: 134 MB % 150.24/22.06 % (3070789)Instructions burned: 2076 (million) % 150.24/22.06 % (3070840)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2346883374:i=5145:rtra=on_2878 on theBenchmark for (2878ds/5145Mi) % 150.24/22.06 % (3070845)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1246460242:i=3509:rtra=on_2875 on theBenchmark for (2875ds/3509Mi) % 150.24/22.06 % (3070743)Instruction limit reached! % 150.24/22.06 % (3070743)------------------------------ % 150.24/22.06 % (3070743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.24/22.06 % (3070743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.24/22.06 % (3070743)CaDiCaL version: 2.1.3 % 150.24/22.06 % (3070743)Termination reason: Instruction limit % 150.24/22.06 % (3070743)Termination phase: Saturation % 150.24/22.06 % (3070743)Time elapsed: 4.908 s % 260.90/37.65 % (3070743)Peak memory usage: 142 MB % 260.90/37.65 % (3070743)Instructions burned: 5451 (million) % 260.90/37.65 % (3070879)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1234184378:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2858 on theBenchmark for (2858ds/13800Mi) % 260.90/37.65 % (3070879)Refutation not found, incomplete strategy % 260.90/37.65 % (3070879)------------------------------ % 260.90/37.65 % (3070879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.90/37.65 % (3070879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.90/37.65 % (3070879)CaDiCaL version: 2.1.3 % 260.90/37.65 % (3070879)Termination reason: Refutation not found, incomplete strategy % 260.90/37.65 % (3070879)Time elapsed: 0.017 s % 260.90/37.65 % (3070879)Peak memory usage: 88 MB % 260.90/37.65 % (3070879)Instructions burned: 23 (million) % 260.90/37.65 % (3070788)Instruction limit reached! % 260.90/37.65 % (3070788)------------------------------ % 260.90/37.65 % (3070788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.90/37.65 % (3070788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.90/37.65 % (3070788)CaDiCaL version: 2.1.3 % 260.90/37.65 % (3070788)Termination reason: Instruction limit % 260.90/37.65 % (3070788)Termination phase: Saturation % 260.90/37.65 % (3070788)Time elapsed: 4.042 s % 260.90/37.65 % (3070788)Peak memory usage: 140 MB % 260.90/37.65 % (3070788)Instructions burned: 4975 (million) % 260.90/37.65 % (3070840)Instruction limit reached! % 260.90/37.65 % (3070840)------------------------------ % 260.90/37.65 % (3070840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.90/37.65 % (3070840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.90/37.65 % (3070840)CaDiCaL version: 2.1.3 % 260.90/37.65 % (3070840)Termination reason: Instruction limit % 260.90/37.65 % (3070840)Termination phase: Saturation % 260.90/37.65 % (3070840)Time elapsed: 2.342 s % 260.90/37.65 % (3070840)Peak memory usage: 122 MB % 260.90/37.65 % (3070840)Instructions burned: 5145 (million) % 260.90/37.65 % (3070888)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=758779504:i=1412:rtra=on:fsd=on:proc=on_2854 on theBenchmark for (2854ds/1412Mi) % 260.90/37.65 % (3070879)------------------------------ % 260.90/37.65 % (3070879)------------------------------ % 260.90/37.65 % (3070890)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 % 260.90/37.65 % (3070890)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2980552453:i=11747:aac=none:nm=0:rtra=on:rawr=on_2852 on theBenchmark for (2852ds/11747Mi) % 260.90/37.65 % (3070893)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3505790797:s2a=on:i=3553:nm=0:rtra=on_2851 on theBenchmark for (2851ds/3553Mi) % 260.90/37.65 % (3070888)Instruction limit reached! % 260.90/37.65 % (3070888)------------------------------ % 260.90/37.65 % (3070888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.90/37.65 % (3070888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.90/37.65 % (3070888)CaDiCaL version: 2.1.3 % 260.90/37.65 % (3070888)Termination reason: Instruction limit % 260.90/37.65 % (3070888)Termination phase: Saturation % 260.90/37.65 % (3070888)Time elapsed: 0.756 s % 260.90/37.65 % (3070888)Peak memory usage: 136 MB % 260.90/37.65 % (3070888)Instructions burned: 1413 (million) % 260.90/37.65 % (3070909)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2248017650:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2844 on theBenchmark for (2844ds/3201Mi) % 260.90/37.65 % (3070845)Instruction limit reached! % 260.90/37.65 % (3070845)------------------------------ % 260.90/37.65 % (3070845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.90/37.65 % (3070845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.90/37.65 % (3070845)CaDiCaL version: 2.1.3 % 260.90/37.65 % (3070845)Termination reason: Instruction limit % 260.90/37.65 % (3070845)Termination phase: Saturation % 260.90/37.65 % (3070845)Time elapsed: 3.190 s % 260.90/37.65 % (3070845)Peak memory usage: 114 MB % 260.90/37.65 % (3070845)Instructions burned: 3510 (million) % 260.90/37.65 % (3070913)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=3444887072:thitd=on:cond=on:i=4Terminated %------------------------------------------------------------------------------