%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC427_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:03:56 PM UTC 2026 % Result : Timeout 291.99s 42.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWC427_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.12/0.27 % Computer : n006.cluster.edu % 0.12/0.27 % Model : x86_64 x86_64 % 0.12/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.27 % Memory : 8046.5625MB % 0.12/0.27 % OS : Linux 6.8.0-71-generic % 0.12/0.27 % CPULimit : 300 % 0.12/0.27 % WCLimit : 300 % 0.12/0.27 % DateTime : Mon Sep 28 09:36:10 UTC 2026 % 0.12/0.27 % CPUTime : % 0.12/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.29/0.31 Running first-order theorem proving % 0.29/0.31 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.14/1.91 % (3840179)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 6.14/1.91 % (3840184)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2564757080:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 6.14/1.91 % (3840184)Instruction limit reached! % 6.14/1.91 % (3840184)------------------------------ % 6.14/1.91 % (3840184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.14/1.91 % (3840184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.14/1.91 % (3840184)CaDiCaL version: 2.1.3 % 6.14/1.91 % (3840184)Termination reason: Instruction limit % 6.14/1.91 % (3840184)Termination phase: Saturation % 6.14/1.91 % (3840184)Time elapsed: 0.026 s % 6.14/1.91 % (3840184)Peak memory usage: 115 MB % 6.14/1.91 % (3840184)Instructions burned: 13 (million) % 6.14/1.91 % (3840190)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1461007244:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 6.14/1.91 % (3840189)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2362688100:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 6.14/1.91 % (3840188)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=833796007:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 6.14/1.91 % (3840185)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2012727272:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 6.14/1.91 % (3840186)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1691855995:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 6.14/1.91 % (3840187)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=547495944:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 6.14/1.91 % (3840188)Instruction limit reached! % 6.14/1.91 % (3840188)------------------------------ % 6.14/1.91 % (3840188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.14/1.91 % (3840188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.14/1.91 % (3840188)CaDiCaL version: 2.1.3 % 6.14/1.91 % (3840188)Termination reason: Instruction limit % 6.14/1.91 % (3840188)Termination phase: Saturation % 6.14/1.91 % (3840188)Time elapsed: 0.005 s % 6.14/1.91 % (3840188)Peak memory usage: 88 MB % 6.14/1.91 % (3840188)Instructions burned: 4 (million) % 6.14/1.91 % (3840187)Instruction limit reached! % 6.14/1.91 % (3840187)------------------------------ % 6.14/1.91 % (3840187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.14/1.91 % (3840187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.14/1.91 % (3840187)CaDiCaL version: 2.1.3 % 6.14/1.91 % (3840187)Termination reason: Instruction limit % 6.14/1.91 % (3840187)Termination phase: Saturation % 6.14/1.91 % (3840187)Time elapsed: 0.008 s % 6.14/1.91 % (3840187)Peak memory usage: 88 MB % 6.14/1.91 % (3840187)Instructions burned: 7 (million) % 6.14/1.91 % (3840190)Instruction limit reached! % 6.14/1.91 % (3840190)------------------------------ % 6.14/1.91 % (3840190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.14/1.91 % (3840190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.14/1.91 % (3840190)CaDiCaL version: 2.1.3 % 6.14/1.91 % (3840190)Termination reason: Instruction limit % 6.14/1.91 % (3840190)Termination phase: Saturation % 6.14/1.91 % (3840190)Time elapsed: 0.037 s % 6.14/1.91 % (3840190)Peak memory usage: 116 MB % 6.14/1.91 % (3840190)Instructions burned: 34 (million) % 6.14/1.91 % (3840189)Instruction limit reached! % 6.14/1.91 % (3840189)------------------------------ % 6.14/1.91 % (3840189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.14/1.91 % (3840189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.14/1.91 % (3840189)CaDiCaL version: 2.1.3 % 6.14/1.91 % (3840189)Termination reason: Instruction limit % 6.14/1.91 % (3840189)Termination phase: Saturation % 6.14/1.91 % (3840189)Time elapsed: 0.075 s % 6.14/1.91 % (3840189)Peak memory usage: 115 MB % 6.14/1.91 % (3840189)Instructions burned: 47 (million) % 6.14/1.91 % (3840185)Refutation not found, incomplete strategy % 6.14/1.91 % (3840185)------------------------------ % 6.14/1.91 % (3840185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.14/1.91 % (3840185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.06/2.18 % (3840185)CaDiCaL version: 2.1.3 % 9.06/2.18 % (3840185)Termination reason: Refutation not found, incomplete strategy % 9.06/2.18 % (3840185)Time elapsed: 0.078 s % 9.06/2.18 % (3840185)Peak memory usage: 116 MB % 9.06/2.18 % (3840185)Instructions burned: 46 (million) % 9.06/2.18 % (3840192)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3609284315:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 9.06/2.18 % (3840192)Instruction limit reached! % 9.06/2.18 % (3840192)------------------------------ % 9.06/2.18 % (3840192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.06/2.18 % (3840192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.06/2.18 % (3840192)CaDiCaL version: 2.1.3 % 9.06/2.18 % (3840192)Termination reason: Instruction limit % 9.06/2.18 % (3840192)Termination phase: Saturation % 9.06/2.18 % (3840192)Time elapsed: 0.015 s % 9.06/2.18 % (3840192)Peak memory usage: 88 MB % 9.06/2.18 % (3840192)Instructions burned: 14 (million) % 9.06/2.18 % (3840201)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=526335362:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 9.06/2.18 % (3840199)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=3786057941:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 9.06/2.18 % (3840201)Instruction limit reached! % 9.06/2.18 % (3840201)------------------------------ % 9.06/2.18 % (3840201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.06/2.18 % (3840201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.06/2.18 % (3840201)CaDiCaL version: 2.1.3 % 9.06/2.18 % (3840201)Termination reason: Instruction limit % 9.06/2.18 % (3840201)Termination phase: Saturation % 9.06/2.18 % (3840201)Time elapsed: 0.016 s % 9.06/2.18 % (3840201)Peak memory usage: 89 MB % 9.06/2.18 % (3840201)Instructions burned: 26 (million) % 9.06/2.18 % (3840202)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=1270994214:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 9.06/2.18 % (3840186)Instruction limit reached! % 9.06/2.18 % (3840186)------------------------------ % 9.06/2.18 % (3840186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.06/2.18 % (3840186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.06/2.18 % (3840186)CaDiCaL version: 2.1.3 % 9.06/2.18 % (3840186)Termination reason: Instruction limit % 9.06/2.18 % (3840186)Termination phase: Saturation % 9.06/2.18 % (3840186)Time elapsed: 0.270 s % 9.06/2.18 % (3840186)Peak memory usage: 117 MB % 9.06/2.18 % (3840186)Instructions burned: 201 (million) % 9.06/2.18 % (3840199)Instruction limit reached! % 9.06/2.18 % (3840199)------------------------------ % 9.06/2.18 % (3840199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.06/2.18 % (3840199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.06/2.18 % (3840199)CaDiCaL version: 2.1.3 % 9.06/2.18 % (3840199)Termination reason: Instruction limit % 9.06/2.18 % (3840199)Termination phase: Saturation % 9.06/2.18 % (3840199)Time elapsed: 0.033 s % 9.06/2.18 % (3840199)Peak memory usage: 89 MB % 9.06/2.18 % (3840199)Instructions burned: 31 (million) % 9.06/2.18 % (3840202)Instruction limit reached! % 9.06/2.18 % (3840202)------------------------------ % 9.06/2.18 % (3840202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.06/2.18 % (3840202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.06/2.18 % (3840202)CaDiCaL version: 2.1.3 % 9.06/2.18 % (3840202)Termination reason: Instruction limit % 9.06/2.18 % (3840202)Termination phase: Saturation % 9.06/2.18 % (3840202)Time elapsed: 0.017 s % 9.06/2.18 % (3840202)Peak memory usage: 89 MB % 9.06/2.18 % (3840202)Instructions burned: 32 (million) % 9.06/2.18 % (3840200)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1611787606:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 9.06/2.18 % (3840200)Instruction limit reached! % 9.06/2.18 % (3840200)------------------------------ % 9.06/2.18 % (3840200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.06/2.18 % (3840200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.84/2.41 % (3840200)CaDiCaL version: 2.1.3 % 9.84/2.41 % (3840200)Termination reason: Instruction limit % 9.84/2.41 % (3840200)Termination phase: Saturation % 9.84/2.41 % (3840200)Time elapsed: 0.018 s % 9.84/2.41 % (3840200)Peak memory usage: 90 MB % 9.84/2.41 % (3840200)Instructions burned: 16 (million) % 9.84/2.41 % (3840204)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1109488338:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 9.84/2.41 % (3840212)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3656498863:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 9.84/2.41 % (3840185)------------------------------ % 9.84/2.41 % (3840185)------------------------------ % 9.84/2.41 % (3840207)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3795673834:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 9.84/2.41 % (3840207)Instruction limit reached! % 9.84/2.41 % (3840207)------------------------------ % 9.84/2.41 % (3840207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.84/2.41 % (3840207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.84/2.41 % (3840207)CaDiCaL version: 2.1.3 % 9.84/2.41 % (3840207)Termination reason: Instruction limit % 9.84/2.41 % (3840207)Termination phase: Saturation % 9.84/2.41 % (3840207)Time elapsed: 0.004 s % 9.84/2.41 % (3840207)Peak memory usage: 88 MB % 9.84/2.41 % (3840207)Instructions burned: 2 (million) % 9.84/2.41 % (3840213)lrs+10_1_thi=all:si=on:fd=off:random_seed=602425096:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 9.84/2.41 % (3840209)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2129560948:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.84/2.41 % (3840210)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=209971634:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.84/2.41 % (3840210)Instruction limit reached! % 9.84/2.41 % (3840210)------------------------------ % 9.84/2.41 % (3840210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.84/2.41 % (3840210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.84/2.41 % (3840210)CaDiCaL version: 2.1.3 % 9.84/2.41 % (3840210)Termination reason: Instruction limit % 9.84/2.41 % (3840210)Termination phase: Saturation % 9.84/2.41 % (3840210)Time elapsed: 0.006 s % 9.84/2.41 % (3840210)Peak memory usage: 88 MB % 9.84/2.41 % (3840210)Instructions burned: 4 (million) % 9.84/2.41 % (3840204)Instruction limit reached! % 9.84/2.41 % (3840204)------------------------------ % 9.84/2.41 % (3840204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.84/2.41 % (3840204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.84/2.41 % (3840204)CaDiCaL version: 2.1.3 % 9.84/2.41 % (3840204)Termination reason: Instruction limit % 9.84/2.41 % (3840204)Termination phase: Saturation % 9.84/2.41 % (3840204)Time elapsed: 0.078 s % 9.84/2.41 % (3840204)Peak memory usage: 89 MB % 9.84/2.41 % (3840204)Instructions burned: 85 (million) % 9.84/2.41 % (3840212)Instruction limit reached! % 9.84/2.41 % (3840212)------------------------------ % 9.84/2.41 % (3840212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.84/2.41 % (3840212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.84/2.41 % (3840212)CaDiCaL version: 2.1.3 % 9.84/2.41 % (3840212)Termination reason: Instruction limit % 9.84/2.41 % (3840212)Termination phase: Saturation % 9.84/2.41 % (3840212)Time elapsed: 0.076 s % 9.84/2.41 % (3840212)Peak memory usage: 134 MB % 9.84/2.41 % (3840212)Instructions burned: 68 (million) % 9.84/2.41 % (3840213)Instruction limit reached! % 9.84/2.41 % (3840213)------------------------------ % 9.84/2.41 % (3840213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.84/2.41 % (3840213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.84/2.41 % (3840213)CaDiCaL version: 2.1.3 % 9.84/2.41 % (3840213)Termination reason: Instruction limit % 9.84/2.41 % (3840213)Termination phase: Saturation % 9.84/2.41 % (3840213)Time elapsed: 0.062 s % 9.84/2.41 % (3840213)Peak memory usage: 116 MB % 9.84/2.41 % (3840213)Instructions burned: 53 (million) % 9.84/2.41 % (3840209)Instruction limit reached! % 9.84/2.41 % (3840209)------------------------------ % 9.84/2.41 % (3840209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.51/2.78 % (3840209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.51/2.78 % (3840209)CaDiCaL version: 2.1.3 % 11.51/2.78 % (3840209)Termination reason: Instruction limit % 11.51/2.78 % (3840209)Termination phase: Saturation % 11.51/2.78 % (3840209)Time elapsed: 0.177 s % 11.51/2.78 % (3840209)Peak memory usage: 90 MB % 11.51/2.78 % (3840209)Instructions burned: 182 (million) % 11.51/2.78 % (3840225)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3920066409:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 11.51/2.78 % (3840224)dis+10_1_si=on:random_seed=3373394352:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 11.51/2.78 % (3840225)Refutation not found, incomplete strategy % 11.51/2.78 % (3840225)------------------------------ % 11.51/2.78 % (3840225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.51/2.78 % (3840225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.51/2.78 % (3840225)CaDiCaL version: 2.1.3 % 11.51/2.78 % (3840225)Termination reason: Refutation not found, incomplete strategy % 11.51/2.78 % (3840225)Time elapsed: 0.002 s % 11.51/2.78 % (3840225)Peak memory usage: 89 MB % 11.51/2.78 % (3840225)Instructions burned: 2 (million) % 11.51/2.78 % (3840219)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2493096665:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 11.51/2.78 % (3840218)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=2775111440:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 11.51/2.78 % (3840222)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3843356291:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 11.51/2.78 % (3840222)Instruction limit reached! % 11.51/2.78 % (3840222)------------------------------ % 11.51/2.78 % (3840222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.51/2.78 % (3840222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.51/2.78 % (3840222)CaDiCaL version: 2.1.3 % 11.51/2.78 % (3840222)Termination reason: Instruction limit % 11.51/2.78 % (3840222)Termination phase: Saturation % 11.51/2.78 % (3840222)Time elapsed: 0.003 s % 11.51/2.78 % (3840222)Peak memory usage: 88 MB % 11.51/2.78 % (3840222)Instructions burned: 2 (million) % 11.51/2.78 % (3840219)Instruction limit reached! % 11.51/2.78 % (3840219)------------------------------ % 11.51/2.78 % (3840219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.51/2.78 % (3840219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.51/2.78 % (3840219)CaDiCaL version: 2.1.3 % 11.51/2.78 % (3840219)Termination reason: Instruction limit % 11.51/2.78 % (3840219)Termination phase: Saturation % 11.51/2.78 % (3840219)Time elapsed: 0.003 s % 11.51/2.78 % (3840219)Peak memory usage: 89 MB % 11.51/2.78 % (3840219)Instructions burned: 2 (million) % 11.51/2.78 % (3840224)Instruction limit reached! % 11.51/2.78 % (3840224)------------------------------ % 11.51/2.78 % (3840224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.51/2.78 % (3840224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.51/2.78 % (3840224)CaDiCaL version: 2.1.3 % 11.51/2.78 % (3840224)Termination reason: Instruction limit % 11.51/2.78 % (3840224)Termination phase: Saturation % 11.51/2.78 % (3840224)Time elapsed: 0.010 s % 11.51/2.78 % (3840224)Peak memory usage: 88 MB % 11.51/2.78 % (3840224)Instructions burned: 11 (million) % 11.51/2.78 % (3840218)Instruction limit reached! % 11.51/2.78 % (3840218)------------------------------ % 11.51/2.78 % (3840218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.51/2.78 % (3840218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.51/2.78 % (3840218)CaDiCaL version: 2.1.3 % 11.51/2.78 % (3840218)Termination reason: Instruction limit % 11.51/2.78 % (3840218)Termination phase: Saturation % 11.51/2.78 % (3840218)Time elapsed: 0.010 s % 11.51/2.78 % (3840218)Peak memory usage: 88 MB % 11.51/2.78 % (3840218)Instructions burned: 8 (million) % 11.51/2.78 % (3840223)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2025099108:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 11.51/2.78 % (3840225)------------------------------ % 11.51/2.78 % (3840225)------------------------------ % 11.51/2.78 % (3840226)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=26998618:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 16.06/3.19 % (3840223)Instruction limit reached! % 16.06/3.19 % (3840223)------------------------------ % 16.06/3.19 % (3840223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.06/3.19 % (3840223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.06/3.19 % (3840223)CaDiCaL version: 2.1.3 % 16.06/3.19 % (3840223)Termination reason: Instruction limit % 16.06/3.19 % (3840223)Termination phase: Saturation % 16.06/3.19 % (3840223)Time elapsed: 0.159 s % 16.06/3.19 % (3840223)Peak memory usage: 116 MB % 16.06/3.19 % (3840223)Instructions burned: 128 (million) % 16.06/3.19 % (3840233)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1724937466:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 16.06/3.19 % (3840235)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1787513619:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 16.06/3.19 % (3840234)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=141227170:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 16.06/3.19 % (3840232)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2306235311:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 16.06/3.19 % (3840232)Instruction limit reached! % 16.06/3.19 % (3840232)------------------------------ % 16.06/3.19 % (3840232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.06/3.19 % (3840232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.06/3.19 % (3840232)CaDiCaL version: 2.1.3 % 16.06/3.19 % (3840232)Termination reason: Instruction limit % 16.06/3.19 % (3840232)Termination phase: Saturation % 16.06/3.19 % (3840232)Time elapsed: 0.004 s % 16.06/3.19 % (3840232)Peak memory usage: 88 MB % 16.06/3.19 % (3840232)Instructions burned: 2 (million) % 16.06/3.19 % (3840226)Instruction limit reached! % 16.06/3.19 % (3840226)------------------------------ % 16.06/3.19 % (3840226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.06/3.19 % (3840226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.06/3.19 % (3840226)CaDiCaL version: 2.1.3 % 16.06/3.19 % (3840226)Termination reason: Instruction limit % 16.06/3.19 % (3840226)Termination phase: Saturation % 16.06/3.19 % (3840226)Time elapsed: 0.044 s % 16.06/3.19 % (3840226)Peak memory usage: 89 MB % 16.06/3.19 % (3840226)Instructions burned: 35 (million) % 16.06/3.19 % (3840233)Instruction limit reached! % 16.06/3.19 % (3840233)------------------------------ % 16.06/3.19 % (3840233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.06/3.19 % (3840233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.06/3.19 % (3840233)CaDiCaL version: 2.1.3 % 16.06/3.19 % (3840233)Termination reason: Instruction limit % 16.06/3.19 % (3840233)Termination phase: Saturation % 16.06/3.19 % (3840233)Time elapsed: 0.012 s % 16.06/3.19 % (3840233)Peak memory usage: 88 MB % 16.06/3.19 % (3840233)Instructions burned: 10 (million) % 16.06/3.19 % (3840235)Instruction limit reached! % 16.06/3.19 % (3840235)------------------------------ % 16.06/3.19 % (3840235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.06/3.19 % (3840235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.06/3.19 % (3840235)CaDiCaL version: 2.1.3 % 16.06/3.19 % (3840235)Termination reason: Instruction limit % 16.06/3.19 % (3840235)Termination phase: Saturation % 16.06/3.19 % (3840235)Time elapsed: 0.046 s % 16.06/3.19 % (3840235)Peak memory usage: 116 MB % 16.06/3.19 % (3840235)Instructions burned: 13 (million) % 16.06/3.19 % (3840237)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=372102046:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi) % 16.06/3.19 % (3840237)Refutation not found, incomplete strategy % 16.06/3.19 % (3840237)------------------------------ % 16.06/3.19 % (3840237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.06/3.19 % (3840237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.06/3.19 % (3840237)CaDiCaL version: 2.1.3 % 16.06/3.19 % (3840237)Termination reason: Refutation not found, incomplete strategy % 16.06/3.19 % (3840237)Time elapsed: 0.024 s % 16.06/3.19 % (3840237)Peak memory usage: 116 MB % 18.31/3.62 % (3840237)Instructions burned: 7 (million) % 18.31/3.62 % (3840244)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1595542657:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 18.31/3.62 % (3840243)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=50964926:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 18.31/3.62 % (3840246)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=2767058960:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 18.31/3.62 % (3840245)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=758978872:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 18.31/3.62 % (3840243)Instruction limit reached! % 18.31/3.62 % (3840243)------------------------------ % 18.31/3.62 % (3840243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.62 % (3840243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.62 % (3840243)CaDiCaL version: 2.1.3 % 18.31/3.62 % (3840243)Termination reason: Instruction limit % 18.31/3.62 % (3840243)Termination phase: Saturation % 18.31/3.62 % (3840243)Time elapsed: 0.012 s % 18.31/3.62 % (3840243)Peak memory usage: 88 MB % 18.31/3.62 % (3840243)Instructions burned: 11 (million) % 18.31/3.62 % (3840234)Instruction limit reached! % 18.31/3.62 % (3840234)------------------------------ % 18.31/3.62 % (3840234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.62 % (3840234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.62 % (3840234)CaDiCaL version: 2.1.3 % 18.31/3.62 % (3840234)Termination reason: Instruction limit % 18.31/3.62 % (3840234)Termination phase: Saturation % 18.31/3.62 % (3840234)Time elapsed: 0.326 s % 18.31/3.62 % (3840234)Peak memory usage: 91 MB % 18.31/3.62 % (3840234)Instructions burned: 371 (million) % 18.31/3.62 % (3840247)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1458315058:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 18.31/3.62 % (3840245)Instruction limit reached! % 18.31/3.62 % (3840245)------------------------------ % 18.31/3.62 % (3840245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.62 % (3840245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.62 % (3840245)CaDiCaL version: 2.1.3 % 18.31/3.62 % (3840245)Termination reason: Instruction limit % 18.31/3.62 % (3840245)Termination phase: Saturation % 18.31/3.62 % (3840245)Time elapsed: 0.061 s % 18.31/3.62 % (3840245)Peak memory usage: 89 MB % 18.31/3.62 % (3840245)Instructions burned: 76 (million) % 18.31/3.62 % (3840244)Instruction limit reached! % 18.31/3.62 % (3840244)------------------------------ % 18.31/3.62 % (3840244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.62 % (3840244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.62 % (3840244)CaDiCaL version: 2.1.3 % 18.31/3.62 % (3840244)Termination reason: Instruction limit % 18.31/3.62 % (3840244)Termination phase: Saturation % 18.31/3.62 % (3840244)Time elapsed: 0.132 s % 18.31/3.62 % (3840244)Peak memory usage: 132 MB % 18.31/3.62 % (3840244)Instructions burned: 71 (million) % 18.31/3.62 % (3840237)------------------------------ % 18.31/3.62 % (3840237)------------------------------ % 18.31/3.62 % (3840247)Instruction limit reached! % 18.31/3.62 % (3840247)------------------------------ % 18.31/3.62 % (3840247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.62 % (3840247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.62 % (3840247)CaDiCaL version: 2.1.3 % 18.31/3.62 % (3840247)Termination reason: Instruction limit % 18.31/3.62 % (3840247)Termination phase: Saturation % 18.31/3.62 % (3840247)Time elapsed: 0.149 s % 18.31/3.62 % (3840247)Peak memory usage: 116 MB % 18.31/3.62 % (3840247)Instructions burned: 131 (million) % 18.31/3.62 % (3840253)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=791325223:i=131:rtra=on_2984 on theBenchmark for (2984ds/131Mi) % 18.31/3.62 % (3840246)Instruction limit reached! % 18.31/3.62 % (3840246)------------------------------ % 18.31/3.62 % (3840246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.62 % (3840246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/4.12 % (3840246)CaDiCaL version: 2.1.3 % 21.96/4.12 % (3840246)Termination reason: Instruction limit % 21.96/4.12 % (3840246)Termination phase: Saturation % 21.96/4.12 % (3840246)Time elapsed: 0.290 s % 21.96/4.12 % (3840246)Peak memory usage: 89 MB % 21.96/4.12 % (3840246)Instructions burned: 295 (million) % 21.96/4.12 % (3840255)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1661248592:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 21.96/4.12 % (3840256)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1454457:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 21.96/4.12 % (3840258)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=988968122:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 21.96/4.12 % (3840257)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=40983500:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 21.96/4.12 % (3840255)Instruction limit reached! % 21.96/4.12 % (3840255)------------------------------ % 21.96/4.12 % (3840255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/4.12 % (3840255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/4.12 % (3840255)CaDiCaL version: 2.1.3 % 21.96/4.12 % (3840255)Termination reason: Instruction limit % 21.96/4.12 % (3840255)Termination phase: Saturation % 21.96/4.12 % (3840255)Time elapsed: 0.104 s % 21.96/4.12 % (3840255)Peak memory usage: 133 MB % 21.96/4.12 % (3840255)Instructions burned: 40 (million) % 21.96/4.12 % (3840258)Instruction limit reached! % 21.96/4.12 % (3840258)------------------------------ % 21.96/4.12 % (3840258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/4.12 % (3840258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/4.12 % (3840258)CaDiCaL version: 2.1.3 % 21.96/4.12 % (3840258)Termination reason: Instruction limit % 21.96/4.12 % (3840258)Termination phase: Saturation % 21.96/4.12 % (3840258)Time elapsed: 0.081 s % 21.96/4.12 % (3840258)Peak memory usage: 118 MB % 21.96/4.12 % (3840258)Instructions burned: 132 (million) % 21.96/4.12 % (3840253)Instruction limit reached! % 21.96/4.12 % (3840253)------------------------------ % 21.96/4.12 % (3840253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/4.12 % (3840253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/4.12 % (3840253)CaDiCaL version: 2.1.3 % 21.96/4.12 % (3840253)Termination reason: Instruction limit % 21.96/4.12 % (3840253)Termination phase: Saturation % 21.96/4.12 % (3840253)Time elapsed: 0.165 s % 21.96/4.12 % (3840253)Peak memory usage: 132 MB % 21.96/4.12 % (3840253)Instructions burned: 131 (million) % 21.96/4.12 % (3840259)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=2504418419:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 21.96/4.12 % (3840261)dis+10_1_si=on:random_seed=1353224935:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 21.96/4.12 % (3840256)Instruction limit reached! % 21.96/4.12 % (3840256)------------------------------ % 21.96/4.12 % (3840256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/4.12 % (3840256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/4.12 % (3840256)CaDiCaL version: 2.1.3 % 21.96/4.12 % (3840256)Termination reason: Instruction limit % 21.96/4.12 % (3840256)Termination phase: Saturation % 21.96/4.12 % (3840256)Time elapsed: 0.261 s % 21.96/4.12 % (3840256)Peak memory usage: 91 MB % 21.96/4.12 % (3840256)Instructions burned: 308 (million) % 21.96/4.12 % (3840268)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3282088066:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 21.96/4.12 % (3840267)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2678709705:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 21.96/4.12 % (3840266)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2140341277:i=383:fsr=off:rtra=on:ev=force_2980 on theBenchmark for (2980ds/383Mi) % 21.96/4.12 % (3840268)Refutation not found, incomplete strategy % 21.96/4.12 % (3840268)------------------------------ % 21.96/4.12 % (3840268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840268)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840268)Termination reason: Refutation not found, incomplete strategy % 23.88/4.63 % (3840268)Time elapsed: 0.023 s % 23.88/4.63 % (3840268)Peak memory usage: 116 MB % 23.88/4.63 % (3840268)Instructions burned: 7 (million) % 23.88/4.63 % (3840259)Instruction limit reached! % 23.88/4.63 % (3840259)------------------------------ % 23.88/4.63 % (3840259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840259)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840259)Termination reason: Instruction limit % 23.88/4.63 % (3840259)Termination phase: Saturation % 23.88/4.63 % (3840259)Time elapsed: 0.255 s % 23.88/4.63 % (3840259)Peak memory usage: 116 MB % 23.88/4.63 % (3840259)Instructions burned: 260 (million) % 23.88/4.63 % (3840267)Instruction limit reached! % 23.88/4.63 % (3840267)------------------------------ % 23.88/4.63 % (3840267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840267)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840267)Termination reason: Instruction limit % 23.88/4.63 % (3840267)Termination phase: Saturation % 23.88/4.63 % (3840267)Time elapsed: 0.139 s % 23.88/4.63 % (3840267)Peak memory usage: 90 MB % 23.88/4.63 % (3840267)Instructions burned: 142 (million) % 23.88/4.63 % (3840271)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2771261252:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 23.88/4.63 % (3840268)------------------------------ % 23.88/4.63 % (3840268)------------------------------ % 23.88/4.63 % (3840271)Instruction limit reached! % 23.88/4.63 % (3840271)------------------------------ % 23.88/4.63 % (3840271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840271)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840271)Termination reason: Instruction limit % 23.88/4.63 % (3840271)Termination phase: Saturation % 23.88/4.63 % (3840271)Time elapsed: 0.109 s % 23.88/4.63 % (3840271)Peak memory usage: 89 MB % 23.88/4.63 % (3840271)Instructions burned: 121 (million) % 23.88/4.63 % (3840266)Instruction limit reached! % 23.88/4.63 % (3840266)------------------------------ % 23.88/4.63 % (3840266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840266)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840266)Termination reason: Instruction limit % 23.88/4.63 % (3840266)Termination phase: Saturation % 23.88/4.63 % (3840266)Time elapsed: 0.331 s % 23.88/4.63 % (3840266)Peak memory usage: 91 MB % 23.88/4.63 % (3840266)Instructions burned: 383 (million) % 23.88/4.63 % (3840275)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=3891729980:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 23.88/4.63 % (3840276)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=4193967871:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi) % 23.88/4.63 % (3840278)dis+1010_1_to=kbo:si=on:random_seed=3731351312:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 23.88/4.63 % (3840276)Instruction limit reached! % 23.88/4.63 % (3840276)------------------------------ % 23.88/4.63 % (3840276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840276)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840276)Termination reason: Instruction limit % 23.88/4.63 % (3840276)Termination phase: Saturation % 23.88/4.63 % (3840276)Time elapsed: 0.067 s % 23.88/4.63 % (3840276)Peak memory usage: 116 MB % 23.88/4.63 % (3840276)Instructions burned: 39 (million) % 23.88/4.63 % (3840257)Instruction limit reached! % 23.88/4.63 % (3840257)------------------------------ % 23.88/4.63 % (3840257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.63 % (3840257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.63 % (3840257)CaDiCaL version: 2.1.3 % 23.88/4.63 % (3840257)Termination reason: Instruction limit % 23.88/4.63 % (3840257)Termination phase: Saturation % 30.19/5.15 % (3840257)Time elapsed: 0.713 s % 30.19/5.15 % (3840257)Peak memory usage: 136 MB % 30.19/5.15 % (3840257)Instructions burned: 598 (million) % 30.19/5.15 % (3840275)Instruction limit reached! % 30.19/5.15 % (3840275)------------------------------ % 30.19/5.15 % (3840275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.19/5.15 % (3840275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.19/5.15 % (3840275)CaDiCaL version: 2.1.3 % 30.19/5.15 % (3840275)Termination reason: Instruction limit % 30.19/5.15 % (3840275)Termination phase: Saturation % 30.19/5.15 % (3840275)Time elapsed: 0.161 s % 30.19/5.15 % (3840275)Peak memory usage: 117 MB % 30.19/5.15 % (3840275)Instructions burned: 128 (million) % 30.19/5.15 % (3840279)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1425044835:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/329Mi) % 30.19/5.15 % (3840278)Instruction limit reached! % 30.19/5.15 % (3840278)------------------------------ % 30.19/5.15 % (3840278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.19/5.15 % (3840278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.19/5.15 % (3840278)CaDiCaL version: 2.1.3 % 30.19/5.15 % (3840278)Termination reason: Instruction limit % 30.19/5.15 % (3840278)Termination phase: Saturation % 30.19/5.15 % (3840278)Time elapsed: 0.099 s % 30.19/5.15 % (3840278)Peak memory usage: 91 MB % 30.19/5.15 % (3840278)Instructions burned: 176 (million) % 30.19/5.15 % (3840280)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1740594815:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 30.19/5.15 % (3840284)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2010815756:thitd=on:i=215:nm=0:rtra=on:ev=force_2973 on theBenchmark for (2973ds/215Mi) % 30.19/5.15 % (3840285)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=763651122:i=349:rtra=on_2973 on theBenchmark for (2973ds/349Mi) % 30.19/5.15 % (3840288)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2442307570:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi) % 30.19/5.15 % (3840286)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=360144382:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 30.19/5.15 % (3840285)Refutation not found, incomplete strategy % 30.19/5.15 % (3840285)------------------------------ % 30.19/5.15 % (3840285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.19/5.15 % (3840285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.19/5.15 % (3840285)CaDiCaL version: 2.1.3 % 30.19/5.15 % (3840285)Termination reason: Refutation not found, incomplete strategy % 30.19/5.15 % (3840285)Time elapsed: 0.040 s % 30.19/5.15 % (3840285)Peak memory usage: 116 MB % 30.19/5.15 % (3840285)Instructions burned: 8 (million) % 30.19/5.15 % (3840261)Instruction limit reached! % 30.19/5.15 % (3840261)------------------------------ % 30.19/5.15 % (3840261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.19/5.15 % (3840261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.19/5.15 % (3840261)CaDiCaL version: 2.1.3 % 30.19/5.15 % (3840261)Termination reason: Instruction limit % 30.19/5.15 % (3840261)Termination phase: Saturation % 30.19/5.15 % (3840261)Time elapsed: 0.951 s % 30.19/5.15 % (3840261)Peak memory usage: 94 MB % 30.19/5.15 % (3840261)Instructions burned: 1000 (million) % 30.19/5.15 % (3840279)Instruction limit reached! % 30.19/5.15 % (3840279)------------------------------ % 30.19/5.15 % (3840279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.19/5.15 % (3840279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.19/5.15 % (3840279)CaDiCaL version: 2.1.3 % 30.19/5.15 % (3840279)Termination reason: Instruction limit % 30.19/5.15 % (3840279)Termination phase: Saturation % 30.19/5.15 % (3840279)Time elapsed: 0.347 s % 30.19/5.15 % (3840279)Peak memory usage: 118 MB % 30.19/5.15 % (3840279)Instructions burned: 329 (million) % 30.19/5.15 % (3840288)Instruction limit reached! % 30.19/5.15 % (3840288)------------------------------ % 30.19/5.15 % (3840288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.19/5.15 % (3840288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.27/5.54 % (3840288)CaDiCaL version: 2.1.3 % 32.27/5.54 % (3840288)Termination reason: Instruction limit % 32.27/5.54 % (3840288)Termination phase: Saturation % 32.27/5.54 % (3840288)Time elapsed: 0.180 s % 32.27/5.54 % (3840288)Peak memory usage: 118 MB % 32.27/5.54 % (3840288)Instructions burned: 330 (million) % 32.27/5.54 % (3840284)Instruction limit reached! % 32.27/5.54 % (3840284)------------------------------ % 32.27/5.54 % (3840284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.27/5.54 % (3840284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.27/5.54 % (3840284)CaDiCaL version: 2.1.3 % 32.27/5.54 % (3840284)Termination reason: Instruction limit % 32.27/5.54 % (3840284)Termination phase: Saturation % 32.27/5.54 % (3840284)Time elapsed: 0.272 s % 32.27/5.54 % (3840284)Peak memory usage: 135 MB % 32.27/5.54 % (3840284)Instructions burned: 215 (million) % 32.27/5.54 % (3840286)Instruction limit reached! % 32.27/5.54 % (3840286)------------------------------ % 32.27/5.54 % (3840286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.27/5.54 % (3840286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.27/5.54 % (3840286)CaDiCaL version: 2.1.3 % 32.27/5.54 % (3840286)Termination reason: Instruction limit % 32.27/5.54 % (3840286)Termination phase: Saturation % 32.27/5.54 % (3840286)Time elapsed: 0.274 s % 32.27/5.54 % (3840286)Peak memory usage: 90 MB % 32.27/5.54 % (3840286)Instructions burned: 296 (million) % 32.27/5.54 % (3840294)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=324472334:i=281:gtgl=2:rtra=on:gtg=all_2969 on theBenchmark for (2969ds/281Mi) % 32.27/5.54 % (3840295)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=337761134:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/484Mi) % 32.27/5.54 % (3840296)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1189330023:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi) % 32.27/5.54 % (3840285)------------------------------ % 32.27/5.54 % (3840285)------------------------------ % 32.27/5.54 % (3840280)Instruction limit reached! % 32.27/5.54 % (3840280)------------------------------ % 32.27/5.54 % (3840280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.27/5.54 % (3840280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.27/5.54 % (3840280)CaDiCaL version: 2.1.3 % 32.27/5.54 % (3840280)Termination reason: Instruction limit % 32.27/5.54 % (3840280)Termination phase: Saturation % 32.27/5.54 % (3840280)Time elapsed: 0.568 s % 32.27/5.54 % (3840280)Peak memory usage: 135 MB % 32.27/5.54 % (3840280)Instructions burned: 483 (million) % 32.27/5.54 % (3840297)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4056125695:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi) % 32.27/5.54 % (3840297)Refutation not found, incomplete strategy % 32.27/5.54 % (3840297)------------------------------ % 32.27/5.54 % (3840297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.27/5.54 % (3840297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.27/5.54 % (3840297)CaDiCaL version: 2.1.3 % 32.27/5.54 % (3840297)Termination reason: Refutation not found, incomplete strategy % 32.27/5.54 % (3840297)Time elapsed: 0.042 s % 32.27/5.54 % (3840297)Peak memory usage: 116 MB % 32.27/5.54 % (3840297)Instructions burned: 7 (million) % 32.27/5.54 % (3840296)Instruction limit reached! % 32.27/5.54 % (3840296)------------------------------ % 32.27/5.54 % (3840296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.27/5.54 % (3840296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.27/5.54 % (3840296)CaDiCaL version: 2.1.3 % 32.27/5.54 % (3840296)Termination reason: Instruction limit % 32.27/5.54 % (3840296)Termination phase: Saturation % 32.27/5.54 % (3840296)Time elapsed: 0.171 s % 32.27/5.54 % (3840296)Peak memory usage: 118 MB % 32.27/5.54 % (3840296)Instructions burned: 321 (million) % 32.27/5.54 % (3840298)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=622535435:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 32.27/5.54 % (3840302)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=1618623734:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 32.27/5.54 % (3840294)Instruction limit reached! % 32.27/5.54 % (3840294)------------------------------ % 36.61/6.13 % (3840294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.61/6.13 % (3840294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/6.13 % (3840294)CaDiCaL version: 2.1.3 % 36.61/6.13 % (3840294)Termination reason: Instruction limit % 36.61/6.13 % (3840294)Termination phase: Saturation % 36.61/6.13 % (3840294)Time elapsed: 0.320 s % 36.61/6.13 % (3840294)Peak memory usage: 118 MB % 36.61/6.13 % (3840294)Instructions burned: 282 (million) % 36.61/6.13 % (3840303)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2071031710:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 36.61/6.13 % (3840305)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2143102106:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/387Mi) % 36.61/6.13 % (3840295)Instruction limit reached! % 36.61/6.13 % (3840295)------------------------------ % 36.61/6.13 % (3840295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.61/6.13 % (3840295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/6.13 % (3840295)CaDiCaL version: 2.1.3 % 36.61/6.13 % (3840295)Termination reason: Instruction limit % 36.61/6.13 % (3840295)Termination phase: Saturation % 36.61/6.13 % (3840295)Time elapsed: 0.463 s % 36.61/6.13 % (3840295)Peak memory usage: 92 MB % 36.61/6.13 % (3840295)Instructions burned: 484 (million) % 36.61/6.13 % (3840303)Refutation not found, incomplete strategy % 36.61/6.13 % (3840303)------------------------------ % 36.61/6.13 % (3840303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.61/6.13 % (3840303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/6.13 % (3840303)CaDiCaL version: 2.1.3 % 36.61/6.13 % (3840303)Termination reason: Refutation not found, incomplete strategy % 36.61/6.13 % (3840303)Time elapsed: 0.132 s % 36.61/6.13 % (3840303)Peak memory usage: 117 MB % 36.61/6.13 % (3840303)Instructions burned: 105 (million) % 36.61/6.13 % (3840297)------------------------------ % 36.61/6.13 % (3840297)------------------------------ % 36.61/6.13 % (3840298)Instruction limit reached! % 36.61/6.13 % (3840298)------------------------------ % 36.61/6.13 % (3840298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.61/6.13 % (3840298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/6.13 % (3840298)CaDiCaL version: 2.1.3 % 36.61/6.13 % (3840298)Termination reason: Instruction limit % 36.61/6.13 % (3840298)Termination phase: Saturation % 36.61/6.13 % (3840298)Time elapsed: 0.431 s % 36.61/6.13 % (3840298)Peak memory usage: 119 MB % 36.61/6.13 % (3840298)Instructions burned: 471 (million) % 36.61/6.13 % (3840308)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1367902905:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2963 on theBenchmark for (2963ds/513Mi) % 36.61/6.13 % (3840302)Instruction limit reached! % 36.61/6.13 % (3840302)------------------------------ % 36.61/6.13 % (3840302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.61/6.13 % (3840302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/6.13 % (3840302)CaDiCaL version: 2.1.3 % 36.61/6.13 % (3840302)Termination reason: Instruction limit % 36.61/6.13 % (3840302)Termination phase: Saturation % 36.61/6.13 % (3840302)Time elapsed: 0.362 s % 36.61/6.13 % (3840302)Peak memory usage: 135 MB % 36.61/6.13 % (3840302)Instructions burned: 277 (million) % 36.61/6.13 % (3840305)Instruction limit reached! % 36.61/6.13 % (3840305)------------------------------ % 36.61/6.13 % (3840305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.61/6.13 % (3840305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/6.13 % (3840305)CaDiCaL version: 2.1.3 % 36.61/6.13 % (3840305)Termination reason: Instruction limit % 36.61/6.13 % (3840305)Termination phase: Saturation % 36.61/6.13 % (3840305)Time elapsed: 0.248 s % 36.61/6.13 % (3840305)Peak memory usage: 119 MB % 36.61/6.13 % (3840305)Instructions burned: 389 (million) % 36.61/6.13 % (3840311)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=414705764:i=334:rtra=on_2961 on theBenchmark for (2961ds/334Mi) % 36.61/6.13 % (3840312)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=554173849:i=359:rtra=on:gtg=exists_top:ss=axioms_2960 on theBenchmark for (2960ds/359Mi) % 40.02/6.86 % (3840312)Refutation not found, incomplete strategy % 40.02/6.86 % (3840312)------------------------------ % 40.02/6.86 % (3840312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.02/6.86 % (3840312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.02/6.86 % (3840312)CaDiCaL version: 2.1.3 % 40.02/6.86 % (3840312)Termination reason: Refutation not found, incomplete strategy % 40.02/6.86 % (3840312)Time elapsed: 0.005 s % 40.02/6.86 % (3840312)Peak memory usage: 89 MB % 40.02/6.86 % (3840312)Instructions burned: 3 (million) % 40.02/6.86 % (3840303)------------------------------ % 40.02/6.86 % (3840303)------------------------------ % 40.02/6.86 % (3840315)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=580588488:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi) % 40.02/6.86 % (3840314)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2263255100:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 40.02/6.86 % (3840315)Refutation not found, incomplete strategy % 40.02/6.86 % (3840315)------------------------------ % 40.02/6.86 % (3840315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.02/6.86 % (3840315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.02/6.86 % (3840315)CaDiCaL version: 2.1.3 % 40.02/6.86 % (3840315)Termination reason: Refutation not found, incomplete strategy % 40.02/6.86 % (3840315)Time elapsed: 0.024 s % 40.02/6.86 % (3840315)Peak memory usage: 115 MB % 40.02/6.86 % (3840315)Instructions burned: 6 (million) % 40.02/6.86 % (3840316)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=995181251:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/235Mi) % 40.02/6.86 % (3840311)Instruction limit reached! % 40.02/6.86 % (3840311)------------------------------ % 40.02/6.86 % (3840311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.02/6.86 % (3840311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.02/6.86 % (3840311)CaDiCaL version: 2.1.3 % 40.02/6.86 % (3840311)Termination reason: Instruction limit % 40.02/6.86 % (3840311)Termination phase: Saturation % 40.02/6.86 % (3840311)Time elapsed: 0.340 s % 40.02/6.86 % (3840311)Peak memory usage: 133 MB % 40.02/6.86 % (3840311)Instructions burned: 334 (million) % 40.02/6.86 % (3840315)------------------------------ % 40.02/6.86 % (3840315)------------------------------ % 40.02/6.86 % (3840321)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3993223416:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 40.02/6.86 % (3840316)Instruction limit reached! % 40.02/6.86 % (3840316)------------------------------ % 40.02/6.86 % (3840316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.02/6.86 % (3840316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.02/6.86 % (3840316)CaDiCaL version: 2.1.3 % 40.02/6.86 % (3840316)Termination reason: Instruction limit % 40.02/6.86 % (3840316)Termination phase: Saturation % 40.02/6.86 % (3840316)Time elapsed: 0.229 s % 40.02/6.86 % (3840316)Peak memory usage: 116 MB % 40.02/6.86 % (3840316)Instructions burned: 236 (million) % 40.02/6.86 % (3840308)Instruction limit reached! % 40.02/6.86 % (3840308)------------------------------ % 40.02/6.86 % (3840308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.02/6.86 % (3840308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.02/6.86 % (3840308)CaDiCaL version: 2.1.3 % 40.02/6.86 % (3840308)Termination reason: Instruction limit % 40.02/6.86 % (3840308)Termination phase: Saturation % 40.02/6.86 % (3840308)Time elapsed: 0.555 s % 40.02/6.86 % (3840308)Peak memory usage: 93 MB % 40.02/6.86 % (3840308)Instructions burned: 514 (million) % 40.02/6.86 % (3840312)------------------------------ % 40.02/6.86 % (3840312)------------------------------ % 40.02/6.86 % (3840314)Instruction limit reached! % 40.02/6.86 % (3840314)------------------------------ % 40.02/6.86 % (3840314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.02/6.86 % (3840314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.02/6.86 % (3840314)CaDiCaL version: 2.1.3 % 40.02/6.86 % (3840314)Termination reason: Instruction limit % 40.02/6.86 % (3840314)Termination phase: Saturation % 46.21/7.69 % (3840314)Time elapsed: 0.356 s % 46.21/7.69 % (3840314)Peak memory usage: 118 MB % 46.21/7.69 % (3840314)Instructions burned: 341 (million) % 46.21/7.69 % (3840324)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2211062799:i=4428:doe=on:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/4428Mi) % 46.21/7.69 % (3840323)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1146848390:i=146:doe=on:rtra=on_2955 on theBenchmark for (2955ds/146Mi) % 46.21/7.69 % (3840327)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2119590847:i=1052:rtra=on_2954 on theBenchmark for (2954ds/1052Mi) % 46.21/7.69 % (3840326)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=3595830171:avsq=on:i=276:avsqr=1,2:rtra=on_2954 on theBenchmark for (2954ds/276Mi) % 46.21/7.69 % (3840321)Instruction limit reached! % 46.21/7.69 % (3840321)------------------------------ % 46.21/7.69 % (3840321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.21/7.69 % (3840321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.21/7.69 % (3840321)CaDiCaL version: 2.1.3 % 46.21/7.69 % (3840321)Termination reason: Instruction limit % 46.21/7.69 % (3840321)Termination phase: Saturation % 46.21/7.69 % (3840321)Time elapsed: 0.301 s % 46.21/7.69 % (3840321)Peak memory usage: 92 MB % 46.21/7.69 % (3840321)Instructions burned: 273 (million) % 46.21/7.69 % (3840323)Instruction limit reached! % 46.21/7.69 % (3840323)------------------------------ % 46.21/7.69 % (3840323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.21/7.69 % (3840323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.21/7.69 % (3840323)CaDiCaL version: 2.1.3 % 46.21/7.69 % (3840323)Termination reason: Instruction limit % 46.21/7.69 % (3840323)Termination phase: Saturation % 46.21/7.69 % (3840323)Time elapsed: 0.151 s % 46.21/7.69 % (3840323)Peak memory usage: 90 MB % 46.21/7.69 % (3840323)Instructions burned: 147 (million) % 46.21/7.69 % (3840329)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2771491826:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1054Mi) % 46.21/7.69 % (3840328)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3164240981:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/655Mi) % 46.21/7.69 % (3840329)Refutation not found, incomplete strategy % 46.21/7.69 % (3840329)------------------------------ % 46.21/7.69 % (3840329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.21/7.69 % (3840329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.21/7.69 % (3840329)CaDiCaL version: 2.1.3 % 46.21/7.69 % (3840329)Termination reason: Refutation not found, incomplete strategy % 46.21/7.69 % (3840329)Time elapsed: 0.008 s % 46.21/7.69 % (3840329)Peak memory usage: 89 MB % 46.21/7.69 % (3840329)Instructions burned: 6 (million) % 46.21/7.69 % (3840334)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=4243798604:i=107:rtra=on_2951 on theBenchmark for (2951ds/107Mi) % 46.21/7.69 % (3840335)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1328484172:s2a=on:i=450:doe=on:nm=32:rtra=on_2951 on theBenchmark for (2951ds/450Mi) % 46.21/7.69 % (3840334)Refutation not found, incomplete strategy % 46.21/7.69 % (3840334)------------------------------ % 46.21/7.69 % (3840334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.21/7.69 % (3840334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.21/7.69 % (3840334)CaDiCaL version: 2.1.3 % 46.21/7.69 % (3840334)Termination reason: Refutation not found, incomplete strategy % 46.21/7.69 % (3840334)Time elapsed: 0.042 s % 46.21/7.69 % (3840334)Peak memory usage: 116 MB % 46.21/7.69 % (3840334)Instructions burned: 8 (million) % 46.21/7.69 % (3840326)Instruction limit reached! % 46.21/7.69 % (3840326)------------------------------ % 46.21/7.69 % (3840326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.21/7.69 % (3840326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.21/7.69 % (3840326)CaDiCaL version: 2.1.3 % 46.21/7.69 % (3840326)Termination reason: Instruction limit % 46.21/7.69 % (3840326)Termination phase: Saturation % 46.21/7.69 % (3840326)Time elapsed: 0.370 s % 46.21/7.69 % (3840326)Peak memory usage: 135 MB % 52.06/8.30 % (3840326)Instructions burned: 277 (million) % 52.06/8.30 % (3840329)------------------------------ % 52.06/8.30 % (3840329)------------------------------ % 52.06/8.30 % (3840340)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 52.06/8.30 % (3840340)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3759307097:i=1090:aac=none:nm=0:rtra=on:rawr=on_2948 on theBenchmark for (2948ds/1090Mi) % 52.06/8.30 % (3840328)Instruction limit reached! % 52.06/8.30 % (3840328)------------------------------ % 52.06/8.30 % (3840328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.06/8.30 % (3840328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.06/8.30 % (3840328)CaDiCaL version: 2.1.3 % 52.06/8.30 % (3840328)Termination reason: Instruction limit % 52.06/8.30 % (3840328)Termination phase: Saturation % 52.06/8.30 % (3840328)Time elapsed: 0.559 s % 52.06/8.30 % (3840328)Peak memory usage: 91 MB % 52.06/8.30 % (3840328)Instructions burned: 656 (million) % 52.06/8.30 % (3840334)------------------------------ % 52.06/8.30 % (3840334)------------------------------ % 52.06/8.30 % (3840341)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2949659453:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2947 on theBenchmark for (2947ds/130Mi) % 52.06/8.30 % (3840327)Instruction limit reached! % 52.06/8.30 % (3840327)------------------------------ % 52.06/8.30 % (3840327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.06/8.30 % (3840327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.06/8.30 % (3840327)CaDiCaL version: 2.1.3 % 52.06/8.30 % (3840327)Termination reason: Instruction limit % 52.06/8.30 % (3840327)Termination phase: Saturation % 52.06/8.30 % (3840327)Time elapsed: 0.903 s % 52.06/8.30 % (3840327)Peak memory usage: 91 MB % 52.06/8.30 % (3840327)Instructions burned: 1052 (million) % 52.06/8.30 % (3840343)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=733458556:i=312:kws=inv_frequency:nm=20:rtra=on_2945 on theBenchmark for (2945ds/312Mi) % 52.06/8.30 % (3840335)Instruction limit reached! % 52.06/8.30 % (3840335)------------------------------ % 52.06/8.30 % (3840335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.06/8.30 % (3840335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.06/8.30 % (3840335)CaDiCaL version: 2.1.3 % 52.06/8.30 % (3840335)Termination reason: Instruction limit % 52.06/8.30 % (3840335)Termination phase: Saturation % 52.06/8.30 % (3840335)Time elapsed: 0.515 s % 52.06/8.30 % (3840335)Peak memory usage: 135 MB % 52.06/8.30 % (3840335)Instructions burned: 450 (million) % 52.06/8.30 % (3840341)Instruction limit reached! % 52.06/8.30 % (3840341)------------------------------ % 52.06/8.30 % (3840341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.06/8.30 % (3840341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.06/8.30 % (3840341)CaDiCaL version: 2.1.3 % 52.06/8.30 % (3840341)Termination reason: Instruction limit % 52.06/8.30 % (3840341)Termination phase: Saturation % 52.06/8.30 % (3840341)Time elapsed: 0.145 s % 52.06/8.30 % (3840341)Peak memory usage: 116 MB % 52.06/8.30 % (3840341)Instructions burned: 131 (million) % 52.06/8.30 % (3840345)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1864866377:i=491:doe=on:rtra=on:gtg=position_2944 on theBenchmark for (2944ds/491Mi) % 52.06/8.30 % (3840345)Refutation not found, incomplete strategy % 52.06/8.30 % (3840345)------------------------------ % 52.06/8.30 % (3840345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.06/8.30 % (3840345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.06/8.30 % (3840345)CaDiCaL version: 2.1.3 % 52.06/8.30 % (3840345)Termination reason: Refutation not found, incomplete strategy % 52.06/8.30 % (3840345)Time elapsed: 0.005 s % 52.06/8.30 % (3840345)Peak memory usage: 89 MB % 52.06/8.30 % (3840345)Instructions burned: 3 (million) % 52.06/8.30 % (3840346)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3043340973:s2a=on:i=835:s2at=2:rtra=on_2943 on theBenchmark for (2943ds/835Mi) % 52.06/8.30 % (3840348)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3908062591:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2943 on theBenchmark for (2943ds/307Mi) % 57.77/9.13 % (3840343)Instruction limit reached! % 57.77/9.13 % (3840343)------------------------------ % 57.77/9.13 % (3840343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.77/9.13 % (3840343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.77/9.13 % (3840343)CaDiCaL version: 2.1.3 % 57.77/9.13 % (3840343)Termination reason: Instruction limit % 57.77/9.13 % (3840343)Termination phase: Saturation % 57.77/9.13 % (3840343)Time elapsed: 0.316 s % 57.77/9.13 % (3840343)Peak memory usage: 118 MB % 57.77/9.13 % (3840343)Instructions burned: 312 (million) % 57.77/9.13 % (3840349)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3655530916:i=776:doe=on:rtra=on_2943 on theBenchmark for (2943ds/776Mi) % 57.77/9.13 % (3840340)Instruction limit reached! % 57.77/9.13 % (3840340)------------------------------ % 57.77/9.13 % (3840340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.77/9.13 % (3840340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.77/9.13 % (3840340)CaDiCaL version: 2.1.3 % 57.77/9.13 % (3840340)Termination reason: Instruction limit % 57.77/9.13 % (3840340)Termination phase: Saturation % 57.77/9.13 % (3840340)Time elapsed: 0.736 s % 57.77/9.13 % (3840340)Peak memory usage: 122 MB % 57.77/9.13 % (3840340)Instructions burned: 1090 (million) % 57.77/9.13 % (3840345)------------------------------ % 57.77/9.13 % (3840345)------------------------------ % 57.77/9.13 % (3840354)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=754717870:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 57.77/9.13 % (3840348)Instruction limit reached! % 57.77/9.13 % (3840348)------------------------------ % 57.77/9.13 % (3840348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.77/9.13 % (3840348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.77/9.13 % (3840348)CaDiCaL version: 2.1.3 % 57.77/9.13 % (3840348)Termination reason: Instruction limit % 57.77/9.13 % (3840348)Termination phase: Saturation % 57.77/9.13 % (3840348)Time elapsed: 0.339 s % 57.77/9.13 % (3840348)Peak memory usage: 93 MB % 57.77/9.13 % (3840348)Instructions burned: 307 (million) % 57.77/9.13 % (3840355)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=3104476728:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2938 on theBenchmark for (2938ds/784Mi) % 57.77/9.13 % (3840358)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=723358758:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi) % 57.77/9.13 % (3840357)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=52143508:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2937 on theBenchmark for (2937ds/1131Mi) % 57.77/9.13 % (3840349)Instruction limit reached! % 57.77/9.13 % (3840349)------------------------------ % 57.77/9.13 % (3840349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.77/9.13 % (3840349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.77/9.13 % (3840349)CaDiCaL version: 2.1.3 % 57.77/9.13 % (3840349)Termination reason: Instruction limit % 57.77/9.13 % (3840349)Termination phase: Saturation % 57.77/9.13 % (3840349)Time elapsed: 0.728 s % 57.77/9.13 % (3840349)Peak memory usage: 123 MB % 57.77/9.13 % (3840349)Instructions burned: 777 (million) % 57.77/9.13 % (3840358)Instruction limit reached! % 57.77/9.13 % (3840358)------------------------------ % 57.77/9.13 % (3840358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.77/9.13 % (3840358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.77/9.13 % (3840358)CaDiCaL version: 2.1.3 % 57.77/9.13 % (3840358)Termination reason: Instruction limit % 57.77/9.13 % (3840358)Termination phase: Saturation % 57.77/9.13 % (3840358)Time elapsed: 0.246 s % 57.77/9.13 % (3840358)Peak memory usage: 116 MB % 57.77/9.13 % (3840358)Instructions burned: 246 (million) % 57.77/9.13 % (3840324)Instruction limit reached! % 57.77/9.13 % (3840324)------------------------------ % 57.77/9.13 % (3840324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.77/9.13 % (3840324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.77/9.13 % (3840324)CaDiCaL version: 2.1.3 % 57.77/9.13 % (3840324)Termination reason: Instruction limit % 64.86/10.14 % (3840324)Termination phase: Saturation % 64.86/10.14 % (3840324)Time elapsed: 2.060 s % 64.86/10.14 % (3840324)Peak memory usage: 112 MB % 64.86/10.14 % (3840324)Instructions burned: 4430 (million) % 64.86/10.14 % (3840346)Instruction limit reached! % 64.86/10.14 % (3840346)------------------------------ % 64.86/10.14 % (3840346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.86/10.14 % (3840346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.86/10.14 % (3840346)CaDiCaL version: 2.1.3 % 64.86/10.14 % (3840346)Termination reason: Instruction limit % 64.86/10.14 % (3840346)Termination phase: Saturation % 64.86/10.14 % (3840346)Time elapsed: 0.871 s % 64.86/10.14 % (3840346)Peak memory usage: 94 MB % 64.86/10.14 % (3840346)Instructions burned: 835 (million) % 64.86/10.14 % (3840362)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2949284736:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2933 on theBenchmark for (2933ds/775Mi) % 64.86/10.14 % (3840354)Instruction limit reached! % 64.86/10.14 % (3840354)------------------------------ % 64.86/10.14 % (3840354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.86/10.14 % (3840354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.86/10.14 % (3840354)CaDiCaL version: 2.1.3 % 64.86/10.14 % (3840354)Termination reason: Instruction limit % 64.86/10.14 % (3840354)Termination phase: Saturation % 64.86/10.14 % (3840354)Time elapsed: 0.763 s % 64.86/10.14 % (3840354)Peak memory usage: 136 MB % 64.86/10.14 % (3840354)Instructions burned: 646 (million) % 64.86/10.14 % (3840363)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2488230840:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2932 on theBenchmark for (2932ds/273Mi) % 64.86/10.14 % (3840364)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2935562903:i=102:nm=16:rtra=on_2932 on theBenchmark for (2932ds/102Mi) % 64.86/10.14 % (3840365)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=540478082:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2932 on theBenchmark for (2932ds/1094Mi) % 64.86/10.14 % (3840364)Instruction limit reached! % 64.86/10.14 % (3840364)------------------------------ % 64.86/10.14 % (3840364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.86/10.14 % (3840364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.86/10.14 % (3840364)CaDiCaL version: 2.1.3 % 64.86/10.14 % (3840364)Termination reason: Instruction limit % 64.86/10.14 % (3840364)Termination phase: Saturation % 64.86/10.14 % (3840364)Time elapsed: 0.090 s % 64.86/10.14 % (3840364)Peak memory usage: 89 MB % 64.86/10.14 % (3840364)Instructions burned: 102 (million) % 64.86/10.14 % (3840355)Instruction limit reached! % 64.86/10.14 % (3840355)------------------------------ % 64.86/10.14 % (3840355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.86/10.14 % (3840355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.86/10.14 % (3840355)CaDiCaL version: 2.1.3 % 64.86/10.14 % (3840355)Termination reason: Instruction limit % 64.86/10.14 % (3840355)Termination phase: Saturation % 64.86/10.14 % (3840355)Time elapsed: 0.810 s % 64.86/10.14 % (3840355)Peak memory usage: 121 MB % 64.86/10.14 % (3840355)Instructions burned: 784 (million) % 64.86/10.14 % (3840367)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3904376609:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 64.86/10.14 % (3840363)Instruction limit reached! % 64.86/10.14 % (3840363)------------------------------ % 64.86/10.14 % (3840363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.86/10.14 % (3840363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.86/10.14 % (3840363)CaDiCaL version: 2.1.3 % 64.86/10.14 % (3840363)Termination reason: Instruction limit % 64.86/10.14 % (3840363)Termination phase: Saturation % 64.86/10.14 % (3840363)Time elapsed: 0.276 s % 64.86/10.14 % (3840363)Peak memory usage: 91 MB % 64.86/10.14 % (3840363)Instructions burned: 273 (million) % 64.86/10.14 % (3840362)Instruction limit reached! % 64.86/10.14 % (3840362)------------------------------ % 64.86/10.14 % (3840362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.86/10.14 % (3840362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.86/10.14 % (3840362)CaDiCaL version: 2.1.3 % 64.86/10.14 % (3840362)Termination reason: Instruction limit % 64.86/10.14 % (3840362)Termination phase: Saturation % 77.04/12.06 % (3840362)Time elapsed: 0.421 s % 77.04/12.06 % (3840362)Peak memory usage: 95 MB % 77.04/12.06 % (3840362)Instructions burned: 778 (million) % 77.04/12.06 % (3840371)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=1396410547:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2928 on theBenchmark for (2928ds/868Mi) % 77.04/12.06 % (3840372)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=2374678293:i=1846:canc=cautious:fsr=off:rtra=on_2927 on theBenchmark for (2927ds/1846Mi) % 77.04/12.06 % (3840375)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=122038388:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2926 on theBenchmark for (2926ds/273Mi) % 77.04/12.06 % (3840374)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1986223367:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2927 on theBenchmark for (2927ds/36816Mi) % 77.04/12.06 % (3840374)Refutation not found, incomplete strategy % 77.04/12.06 % (3840374)------------------------------ % 77.04/12.06 % (3840374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.04/12.06 % (3840374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.04/12.06 % (3840374)CaDiCaL version: 2.1.3 % 77.04/12.06 % (3840374)Termination reason: Refutation not found, incomplete strategy % 77.04/12.06 % (3840374)Time elapsed: 0.004 s % 77.04/12.06 % (3840374)Peak memory usage: 88 MB % 77.04/12.06 % (3840374)Instructions burned: 2 (million) % 77.04/12.06 % (3840357)Instruction limit reached! % 77.04/12.06 % (3840357)------------------------------ % 77.04/12.06 % (3840357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.04/12.06 % (3840357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.04/12.06 % (3840357)CaDiCaL version: 2.1.3 % 77.04/12.06 % (3840357)Termination reason: Instruction limit % 77.04/12.06 % (3840357)Termination phase: Saturation % 77.04/12.06 % (3840357)Time elapsed: 1.171 s % 77.04/12.06 % (3840357)Peak memory usage: 124 MB % 77.04/12.06 % (3840357)Instructions burned: 1131 (million) % 77.04/12.06 % (3840375)Instruction limit reached! % 77.04/12.06 % (3840375)------------------------------ % 77.04/12.06 % (3840375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.04/12.06 % (3840375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.04/12.06 % (3840375)CaDiCaL version: 2.1.3 % 77.04/12.06 % (3840375)Termination reason: Instruction limit % 77.04/12.06 % (3840375)Termination phase: Saturation % 77.04/12.06 % (3840375)Time elapsed: 0.148 s % 77.04/12.06 % (3840375)Peak memory usage: 91 MB % 77.04/12.06 % (3840375)Instructions burned: 275 (million) % 77.04/12.06 % (3840381)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1188419708:i=5811:kws=precedence:nm=0:rtra=on_2922 on theBenchmark for (2922ds/5811Mi) % 77.04/12.06 % (3840380)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=1135772002:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2923 on theBenchmark for (2923ds/863Mi) % 77.04/12.06 % (3840365)Instruction limit reached! % 77.04/12.06 % (3840365)------------------------------ % 77.04/12.06 % (3840365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.04/12.06 % (3840365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.04/12.06 % (3840365)CaDiCaL version: 2.1.3 % 77.04/12.06 % (3840365)Termination reason: Instruction limit % 77.04/12.06 % (3840365)Termination phase: Saturation % 77.04/12.06 % (3840365)Time elapsed: 0.913 s % 77.04/12.06 % (3840365)Peak memory usage: 91 MB % 77.04/12.06 % (3840365)Instructions burned: 1095 (million) % 77.04/12.06 % (3840374)------------------------------ % 77.04/12.06 % (3840374)------------------------------ % 77.04/12.06 % (3840381)Refutation not found, incomplete strategy % 77.04/12.06 % (3840381)------------------------------ % 77.04/12.06 % (3840381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.04/12.06 % (3840381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.04/12.06 % (3840381)CaDiCaL version: 2.1.3 % 77.04/12.06 % (3840381)Termination reason: Refutation not found, incomplete strategy % 77.04/12.06 % (3840381)Time elapsed: 0.038 s % 77.04/12.06 % (3840381)Peak memory usage: 116 MB % 77.04/12.06 % (3840381)Instructions burned: 39 (million) % 77.04/12.06 % (3840371)Instruction limit reached! % 102.56/15.43 % (3840371)------------------------------ % 102.56/15.43 % (3840371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.56/15.43 % (3840371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.56/15.43 % (3840371)CaDiCaL version: 2.1.3 % 102.56/15.43 % (3840371)Termination reason: Instruction limit % 102.56/15.43 % (3840371)Termination phase: Saturation % 102.56/15.43 % (3840371)Time elapsed: 0.759 s % 102.56/15.43 % (3840371)Peak memory usage: 117 MB % 102.56/15.43 % (3840371)Instructions burned: 868 (million) % 102.56/15.43 % (3840381)------------------------------ % 102.56/15.43 % (3840381)------------------------------ % 102.56/15.43 % (3840384)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=3073850480:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2920 on theBenchmark for (2920ds/2216Mi) % 102.56/15.43 % (3840385)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3076240449:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2920 on theBenchmark for (2920ds/801Mi) % 102.56/15.43 % (3840387)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=730005556:i=3509:rtra=on_2917 on theBenchmark for (2917ds/3509Mi) % 102.56/15.43 % (3840386)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2509208950:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2918 on theBenchmark for (2918ds/1026Mi) % 102.56/15.43 % (3840386)Refutation not found, incomplete strategy % 102.56/15.43 % (3840386)------------------------------ % 102.56/15.43 % (3840386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.56/15.43 % (3840386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.56/15.43 % (3840386)CaDiCaL version: 2.1.3 % 102.56/15.43 % (3840386)Termination reason: Refutation not found, incomplete strategy % 102.56/15.43 % (3840386)Time elapsed: 0.008 s % 102.56/15.43 % (3840386)Peak memory usage: 89 MB % 102.56/15.43 % (3840386)Instructions burned: 6 (million) % 102.56/15.43 % (3840380)Instruction limit reached! % 102.56/15.43 % (3840380)------------------------------ % 102.56/15.43 % (3840380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.56/15.43 % (3840380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.56/15.43 % (3840380)CaDiCaL version: 2.1.3 % 102.56/15.43 % (3840380)Termination reason: Instruction limit % 102.56/15.43 % (3840380)Termination phase: Saturation % 102.56/15.43 % (3840380)Time elapsed: 0.798 s % 102.56/15.43 % (3840380)Peak memory usage: 117 MB % 102.56/15.43 % (3840380)Instructions burned: 863 (million) % 102.56/15.43 % (3840386)------------------------------ % 102.56/15.43 % (3840386)------------------------------ % 102.56/15.43 % (3840385)Instruction limit reached! % 102.56/15.43 % (3840385)------------------------------ % 102.56/15.43 % (3840385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.56/15.43 % (3840385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.56/15.43 % (3840385)CaDiCaL version: 2.1.3 % 102.56/15.43 % (3840385)Termination reason: Instruction limit % 102.56/15.43 % (3840385)Termination phase: Saturation % 102.56/15.43 % (3840385)Time elapsed: 0.663 s % 102.56/15.43 % (3840385)Peak memory usage: 91 MB % 102.56/15.43 % (3840385)Instructions burned: 801 (million) % 102.56/15.43 % (3840392)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1745704569:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2912 on theBenchmark for (2912ds/2127Mi) % 102.56/15.43 % (3840393)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1035949750:i=1959:rtra=on:fsd=on:proc=on_2911 on theBenchmark for (2911ds/1959Mi) % 102.56/15.43 % (3840372)Instruction limit reached! % 102.56/15.43 % (3840372)------------------------------ % 102.56/15.43 % (3840372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.56/15.43 % (3840372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.56/15.43 % (3840372)CaDiCaL version: 2.1.3 % 102.56/15.43 % (3840372)Termination reason: Instruction limit % 102.56/15.43 % (3840372)Termination phase: Saturation % 102.56/15.43 % (3840372)Time elapsed: 1.659 s % 102.56/15.43 % (3840372)Peak memory usage: 96 MB % 102.56/15.43 % (3840372)Instructions burned: 1847 (million) % 102.56/15.43 % (3840393)Refutation not found, incomplete strategy % 102.56/15.43 % (3840393)------------------------------ % 102.56/15.43 % (3840393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.56/15.43 % (3840393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.24/23.00 % (3840393)CaDiCaL version: 2.1.3 % 156.24/23.00 % (3840393)Termination reason: Refutation not found, incomplete strategy % 156.24/23.00 % (3840393)Time elapsed: 0.045 s % 156.24/23.00 % (3840393)Peak memory usage: 116 MB % 156.24/23.00 % (3840393)Instructions burned: 9 (million) % 156.24/23.00 % (3840394)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4005231213:s2a=on:i=3553:nm=0:rtra=on_2910 on theBenchmark for (2910ds/3553Mi) % 156.24/23.00 % (3840397)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1786720535:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2908 on theBenchmark for (2908ds/3201Mi) % 156.24/23.00 % (3840393)------------------------------ % 156.24/23.00 % (3840393)------------------------------ % 156.24/23.00 % (3840387)Instruction limit reached! % 156.24/23.00 % (3840387)------------------------------ % 156.24/23.00 % (3840387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.24/23.00 % (3840387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.24/23.00 % (3840387)CaDiCaL version: 2.1.3 % 156.24/23.00 % (3840387)Termination reason: Instruction limit % 156.24/23.00 % (3840387)Termination phase: Saturation % 156.24/23.00 % (3840387)Time elapsed: 1.355 s % 156.24/23.00 % (3840387)Peak memory usage: 104 MB % 156.24/23.00 % (3840387)Instructions burned: 3510 (million) % 156.24/23.00 % (3840400)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=2010224149:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2904 on theBenchmark for (2904ds/4093Mi) % 156.24/23.00 % (3840401)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=2962092786:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2902 on theBenchmark for (2902ds/21173Mi) % 156.24/23.00 % (3840384)Instruction limit reached! % 156.24/23.00 % (3840384)------------------------------ % 156.24/23.00 % (3840384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.24/23.00 % (3840384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.24/23.00 % (3840384)CaDiCaL version: 2.1.3 % 156.24/23.00 % (3840384)Termination reason: Instruction limit % 156.24/23.00 % (3840384)Termination phase: Saturation % 156.24/23.00 % (3840384)Time elapsed: 1.935 s % 156.24/23.00 % (3840384)Peak memory usage: 126 MB % 156.24/23.00 % (3840384)Instructions burned: 2217 (million) % 156.24/23.00 % (3840404)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1751271758:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2898 on theBenchmark for (2898ds/10544Mi) % 156.24/23.00 % (3840392)Instruction limit reached! % 156.24/23.00 % (3840392)------------------------------ % 156.24/23.00 % (3840392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.24/23.00 % (3840392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.24/23.00 % (3840392)CaDiCaL version: 2.1.3 % 156.24/23.00 % (3840392)Termination reason: Instruction limit % 156.24/23.00 % (3840392)Termination phase: Saturation % 156.24/23.00 % (3840392)Time elapsed: 1.717 s % 156.24/23.00 % (3840392)Peak memory usage: 101 MB % 156.24/23.00 % (3840392)Instructions burned: 2127 (million) % 156.24/23.00 % (3840397)Refutation not found, incomplete strategy % 156.24/23.00 % (3840397)------------------------------ % 156.24/23.00 % (3840397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.24/23.00 % (3840397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.24/23.00 % (3840397)CaDiCaL version: 2.1.3 % 156.24/23.00 % (3840397)Termination reason: Refutation not found, incomplete strategy % 156.24/23.00 % (3840397)Time elapsed: 1.443 s % 156.24/23.00 % (3840397)Peak memory usage: 94 MB % 156.24/23.00 % (3840397)Instructions burned: 1873 (million) % 156.24/23.00 % (3840408)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3530535302:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/1262Mi) % 156.24/23.00 % (3840408)Refutation not found, incomplete strategy % 156.24/23.00 % (3840408)------------------------------ % 156.24/23.00 % (3840408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.24/23.00 % (3840408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.24/23.00 % (3840408)CaDiCaL version: 2.1.3 % 156.24/23.00 % (3840408)Termination reason: Refutation not found, incomplete strategy % 176.58/25.80 % (3840408)Time elapsed: 0.042 s % 176.58/25.80 % (3840408)Peak memory usage: 116 MB % 176.58/25.80 % (3840408)Instructions burned: 8 (million) % 176.58/25.80 % (3840397)------------------------------ % 176.58/25.80 % (3840397)------------------------------ % 176.58/25.80 % (3840408)------------------------------ % 176.58/25.80 % (3840408)------------------------------ % 176.58/25.80 % (3840410)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3621935558:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2886 on theBenchmark for (2886ds/775Mi) % 176.58/25.80 % (3840411)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2077672200:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2884 on theBenchmark for (2884ds/270Mi) % 176.58/25.80 % (3840411)Instruction limit reached! % 176.58/25.80 % (3840411)------------------------------ % 176.58/25.80 % (3840411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.58/25.80 % (3840411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.58/25.80 % (3840411)CaDiCaL version: 2.1.3 % 176.58/25.80 % (3840411)Termination reason: Instruction limit % 176.58/25.80 % (3840411)Termination phase: Saturation % 176.58/25.80 % (3840411)Time elapsed: 0.289 s % 176.58/25.80 % (3840411)Peak memory usage: 91 MB % 176.58/25.80 % (3840411)Instructions burned: 270 (million) % 176.58/25.80 % (3840414)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2359511405:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2879 on theBenchmark for (2879ds/17165Mi) % 176.58/25.80 % (3840410)Instruction limit reached! % 176.58/25.80 % (3840410)------------------------------ % 176.58/25.80 % (3840410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.58/25.80 % (3840410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.58/25.80 % (3840410)CaDiCaL version: 2.1.3 % 176.58/25.80 % (3840410)Termination reason: Instruction limit % 176.58/25.80 % (3840410)Termination phase: Saturation % 176.58/25.80 % (3840410)Time elapsed: 0.770 s % 176.58/25.80 % (3840410)Peak memory usage: 96 MB % 176.58/25.80 % (3840410)Instructions burned: 775 (million) % 176.58/25.80 % (3840394)Instruction limit reached! % 176.58/25.80 % (3840394)------------------------------ % 176.58/25.80 % (3840394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.58/25.80 % (3840394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.58/25.80 % (3840394)CaDiCaL version: 2.1.3 % 176.58/25.80 % (3840394)Termination reason: Instruction limit % 176.58/25.80 % (3840394)Termination phase: Saturation % 176.58/25.80 % (3840394)Time elapsed: 3.372 s % 176.58/25.80 % (3840394)Peak memory usage: 99 MB % 176.58/25.80 % (3840394)Instructions burned: 3553 (million) % 176.58/25.80 % (3840416)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3402017316:s2a=on:i=13094:s2at=-1:rtra=on_2875 on theBenchmark for (2875ds/13094Mi) % 176.58/25.80 % (3840417)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=472335829:st=2:i=12633:rtra=on:ss=axioms_2874 on theBenchmark for (2874ds/12633Mi) % 176.58/25.80 % (3840367)Instruction limit reached! % 176.58/25.80 % (3840367)------------------------------ % 176.58/25.80 % (3840367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.58/25.80 % (3840367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.58/25.80 % (3840367)CaDiCaL version: 2.1.3 % 176.58/25.80 % (3840367)Termination reason: Instruction limit % 176.58/25.80 % (3840367)Termination phase: Saturation % 176.58/25.80 % (3840367)Time elapsed: 5.759 s % 176.58/25.80 % (3840367)Peak memory usage: 119 MB % 176.58/25.80 % (3840367)Instructions burned: 6401 (million) % 176.58/25.80 % (3840420)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3888533100:i=1783:rtra=on:gtg=position_2869 on theBenchmark for (2869ds/1783Mi) % 176.58/25.80 % (3840400)Instruction limit reached! % 176.58/25.80 % (3840400)------------------------------ % 176.58/25.80 % (3840400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.58/25.80 % (3840400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.58/25.80 % (3840400)CaDiCaL version: 2.1.3 % 176.58/25.80 % (3840400)Termination reason: Instruction limit % 176.58/25.80 % (3840400)Termination phase: Saturation % 176.58/25.80 % (3840400)Time elapsed: 4.275 s % 176.58/25.80 % (3840400)Peak memory usage: 158 MB % 176.58/25.80 % (3840400)Instructions burned: 4093 (million) % 176.58/25.80 % (3840424)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=1505570201:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2858 on theBenchmark for (2858ds/5451Mi) % 192.82/28.09 % (3840420)Instruction limit reached! % 192.82/28.09 % (3840420)------------------------------ % 192.82/28.09 % (3840420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.82/28.09 % (3840420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.82/28.09 % (3840420)CaDiCaL version: 2.1.3 % 192.82/28.09 % (3840420)Termination reason: Instruction limit % 192.82/28.09 % (3840420)Termination phase: Saturation % 192.82/28.09 % (3840420)Time elapsed: 1.876 s % 192.82/28.09 % (3840420)Peak memory usage: 126 MB % 192.82/28.09 % (3840420)Instructions burned: 1784 (million) % 192.82/28.09 % (3840426)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=632097571:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2847 on theBenchmark for (2847ds/4975Mi) % 192.82/28.09 % (3840401)Instruction limit reached! % 192.82/28.09 % (3840401)------------------------------ % 192.82/28.09 % (3840401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.82/28.09 % (3840401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.82/28.09 % (3840401)CaDiCaL version: 2.1.3 % 192.82/28.09 % (3840401)Termination reason: Instruction limit % 192.82/28.09 % (3840401)Termination phase: Saturation % 192.82/28.09 % (3840401)Time elapsed: 8.751 s % 192.82/28.09 % (3840401)Peak memory usage: 138 MB % 192.82/28.09 % (3840401)Instructions burned: 21173 (million) % 192.82/28.09 % (3840428)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=2570579511:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2812 on theBenchmark for (2812ds/2076Mi) % 192.82/28.09 % (3840426)Instruction limit reached! % 192.82/28.09 % (3840426)------------------------------ % 192.82/28.09 % (3840426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.82/28.09 % (3840426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.82/28.09 % (3840426)CaDiCaL version: 2.1.3 % 192.82/28.09 % (3840426)Termination reason: Instruction limit % 192.82/28.09 % (3840426)Termination phase: Saturation % 192.82/28.09 % (3840426)Time elapsed: 3.700 s % 192.82/28.09 % (3840426)Peak memory usage: 120 MB % 192.82/28.09 % (3840426)Instructions burned: 4976 (million) % 192.82/28.09 % (3840430)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4126859303:i=5145:rtra=on_2807 on theBenchmark for (2807ds/5145Mi) % 192.82/28.09 % (3840424)Instruction limit reached! % 192.82/28.09 % (3840424)------------------------------ % 192.82/28.09 % (3840424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.82/28.09 % (3840424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.82/28.09 % (3840424)CaDiCaL version: 2.1.3 % 192.82/28.09 % (3840424)Termination reason: Instruction limit % 192.82/28.09 % (3840424)Termination phase: Saturation % 192.82/28.09 % (3840424)Time elapsed: 5.138 s % 192.82/28.09 % (3840424)Peak memory usage: 146 MB % 192.82/28.09 % (3840424)Instructions burned: 5451 (million) % 192.82/28.09 % (3840432)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2014064759:i=3509:rtra=on_2803 on theBenchmark for (2803ds/3509Mi) % 192.82/28.09 % (3840428)Instruction limit reached! % 192.82/28.09 % (3840428)------------------------------ % 192.82/28.09 % (3840428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.82/28.09 % (3840428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.82/28.09 % (3840428)CaDiCaL version: 2.1.3 % 192.82/28.09 % (3840428)Termination reason: Instruction limit % 192.82/28.09 % (3840428)Termination phase: Saturation % 192.82/28.09 % (3840428)Time elapsed: 0.986 s % 192.82/28.09 % (3840428)Peak memory usage: 126 MB % 192.82/28.09 % (3840428)Instructions burned: 2076 (million) % 192.82/28.09 % (3840434)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1027458926:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2799 on theBenchmark for (2799ds/13800Mi) % 192.82/28.09 % (3840404)Instruction limit reached! % 192.82/28.09 % (3840404)------------------------------ % 192.82/28.09 % (3840404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.82/28.09 % (3840404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.82/28.09 % (3840404)CaDiCaL version: 2.1.3 % 192.82/28.09 % (3840404)Termination reason: Instruction limit % 204.26/29.79 % (3840404)Termination phase: Saturation % 204.26/29.79 % (3840404)Time elapsed: 11.551 s % 204.26/29.79 % (3840404)Peak memory usage: 200 MB % 204.26/29.79 % (3840404)Instructions burned: 10544 (million) % 204.26/29.79 % (3840440)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=367850038:i=1412:rtra=on:fsd=on:proc=on_2779 on theBenchmark for (2779ds/1412Mi) % 204.26/29.79 % (3840440)Refutation not found, incomplete strategy % 204.26/29.79 % (3840440)------------------------------ % 204.26/29.79 % (3840440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.26/29.79 % (3840440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.26/29.79 % (3840440)CaDiCaL version: 2.1.3 % 204.26/29.79 % (3840440)Termination reason: Refutation not found, incomplete strategy % 204.26/29.79 % (3840440)Time elapsed: 0.045 s % 204.26/29.79 % (3840440)Peak memory usage: 116 MB % 204.26/29.79 % (3840440)Instructions burned: 9 (million) % 204.26/29.79 % (3840417)Instruction limit reached! % 204.26/29.79 % (3840417)------------------------------ % 204.26/29.79 % (3840417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.26/29.79 % (3840417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.26/29.79 % (3840417)CaDiCaL version: 2.1.3 % 204.26/29.79 % (3840417)Termination reason: Instruction limit % 204.26/29.79 % (3840417)Termination phase: Saturation % 204.26/29.79 % (3840417)Time elapsed: 9.666 s % 204.26/29.79 % (3840417)Peak memory usage: 140 MB % 204.26/29.79 % (3840417)Instructions burned: 12633 (million) % 204.26/29.79 % (3840440)------------------------------ % 204.26/29.79 % (3840440)------------------------------ % 204.26/29.79 % (3840442)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 % 204.26/29.79 % (3840442)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1074283633:i=11747:aac=none:nm=0:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/11747Mi) % 204.26/29.79 % (3840443)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3841285419:s2a=on:i=3553:nm=0:rtra=on_2771 on theBenchmark for (2771ds/3553Mi) % 204.26/29.79 % (3840432)Instruction limit reached! % 204.26/29.79 % (3840432)------------------------------ % 204.26/29.79 % (3840432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.26/29.79 % (3840432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.26/29.79 % (3840432)CaDiCaL version: 2.1.3 % 204.26/29.79 % (3840432)Termination reason: Instruction limit % 204.26/29.79 % (3840432)Termination phase: Saturation % 204.26/29.79 % (3840432)Time elapsed: 3.282 s % 204.26/29.79 % (3840432)Peak memory usage: 102 MB % 204.26/29.79 % (3840432)Instructions burned: 3509 (million) % 204.26/29.79 % (3840446)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2552552674:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/3201Mi) % 204.26/29.79 % (3840430)Instruction limit reached! % 204.26/29.79 % (3840430)------------------------------ % 204.26/29.79 % (3840430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.26/29.79 % (3840430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.26/29.79 % (3840430)CaDiCaL version: 2.1.3 % 204.26/29.79 % (3840430)Termination reason: Instruction limit % 204.26/29.79 % (3840430)Termination phase: Saturation % 204.26/29.79 % (3840430)Time elapsed: 4.029 s % 204.26/29.79 % (3840430)Peak memory usage: 95 MB % 204.26/29.79 % (3840430)Instructions burned: 5146 (million) % 204.26/29.79 % (3840448)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=216887919:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2763 on theBenchmark for (2763ds/4081Mi) % 204.26/29.79 % (3840416)Instruction limit reached! % 204.26/29.79 % (3840416)------------------------------ % 204.26/29.79 % (3840416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.26/29.79 % (3840416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.26/29.79 % (3840416)CaDiCaL version: 2.1.3 % 204.26/29.79 % (3840416)Termination reason: Instruction limit % 204.26/29.79 % (3840416)Termination phase: Saturation % 204.26/29.79 % (3840416)Time elapsed: 11.820 s % 204.26/29.79 % (3840416)Peak memory usage: 127 MB % 204.26/29.79 % (3840416)Instructions burned: 13095 (million) % 233.27/33.87 % (3840450)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=1926355640:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2754 on theBenchmark for (2754ds/20260Mi) % 233.27/33.87 % (3840446)Refutation not found, incomplete strategy % 233.27/33.87 % (3840446)------------------------------ % 233.27/33.87 % (3840446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.27/33.87 % (3840446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.27/33.87 % (3840446)CaDiCaL version: 2.1.3 % 233.27/33.87 % (3840446)Termination reason: Refutation not found, incomplete strategy % 233.27/33.87 % (3840446)Time elapsed: 2.084 s % 233.27/33.87 % (3840446)Peak memory usage: 94 MB % 233.27/33.87 % (3840446)Instructions burned: 2657 (million) % 233.27/33.87 % (3840446)------------------------------ % 233.27/33.87 % (3840446)------------------------------ % 233.27/33.87 % (3840456)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1041139587:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2740 on theBenchmark for (2740ds/58627Mi) % 233.27/33.87 % (3840456)Refutation not found, incomplete strategy % 233.27/33.87 % (3840456)------------------------------ % 233.27/33.87 % (3840456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.27/33.87 % (3840456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.27/33.87 % (3840456)CaDiCaL version: 2.1.3 % 233.27/33.87 % (3840456)Termination reason: Refutation not found, incomplete strategy % 233.27/33.87 % (3840456)Time elapsed: 0.004 s % 233.27/33.87 % (3840456)Peak memory usage: 88 MB % 233.27/33.87 % (3840456)Instructions burned: 2 (million) % 233.27/33.87 % (3840434)Instruction limit reached! % 233.27/33.87 % (3840434)------------------------------ % 233.27/33.87 % (3840434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.27/33.87 % (3840434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.27/33.87 % (3840434)CaDiCaL version: 2.1.3 % 233.27/33.87 % (3840434)Termination reason: Instruction limit % 233.27/33.87 % (3840434)Termination phase: Saturation % 233.27/33.87 % (3840434)Time elapsed: 6.187 s % 233.27/33.87 % (3840434)Peak memory usage: 139 MB % 233.27/33.87 % (3840434)Instructions burned: 13801 (million) % 233.27/33.87 % (3840443)Instruction limit reached! % 233.27/33.87 % (3840443)------------------------------ % 233.27/33.87 % (3840443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.27/33.87 % (3840443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.27/33.87 % (3840443)CaDiCaL version: 2.1.3 % 233.27/33.87 % (3840443)Termination reason: Instruction limit % 233.27/33.87 % (3840443)Termination phase: Saturation % 233.27/33.87 % (3840443)Time elapsed: 3.427 s % 233.27/33.87 % (3840443)Peak memory usage: 99 MB % 233.27/33.87 % (3840443)Instructions burned: 3553 (million) % 233.27/33.87 % (3840458)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1281782011:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2735 on theBenchmark for (2735ds/6258Mi) % 233.27/33.87 % (3840458)Refutation not found, incomplete strategy % 233.27/33.87 % (3840458)------------------------------ % 233.27/33.87 % (3840458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.27/33.87 % (3840458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.27/33.87 % (3840458)CaDiCaL version: 2.1.3 % 233.27/33.87 % (3840458)Termination reason: Refutation not found, incomplete strategy % 233.27/33.87 % (3840458)Time elapsed: 0.022 s % 233.27/33.87 % (3840458)Peak memory usage: 116 MB % 233.27/33.87 % (3840458)Instructions burned: 8 (million) % 233.27/33.87 % (3840456)------------------------------ % 233.27/33.87 % (3840456)------------------------------ % 233.27/33.87 % (3840459)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=485757889:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2734 on theBenchmark for (2734ds/34001Mi) % 233.27/33.87 % (3840463)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=766357814:s2a=on:i=71622:s2at=-1:rtra=on_2733 on theBenchmark for (2733ds/71622Mi) % 233.27/33.87 % (3840458)------------------------------ % 233.27/33.87 % (3840458)------------------------------ % 233.27/33.87 % (3840466)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1272339106:i=24001:kws=precedence:nm=0:rtra=on_2731 on theBenchmark for (2731ds/24001Mi) % 233.27/33.87 % (3840466)Refutation not found, incomplete strategy % 282.69/40.76 % (3840466)------------------------------ % 282.69/40.76 % (3840466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.69/40.76 % (3840466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.69/40.76 % (3840466)CaDiCaL version: 2.1.3 % 282.69/40.76 % (3840466)Termination reason: Refutation not found, incomplete strategy % 282.69/40.76 % (3840466)Time elapsed: 0.078 s % 282.69/40.76 % (3840466)Peak memory usage: 116 MB % 282.69/40.76 % (3840466)Instructions burned: 87 (million) % 282.69/40.76 % (3840414)Instruction limit reached! % 282.69/40.76 % (3840414)------------------------------ % 282.69/40.76 % (3840414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.69/40.76 % (3840414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.69/40.76 % (3840414)CaDiCaL version: 2.1.3 % 282.69/40.76 % (3840414)Termination reason: Instruction limit % 282.69/40.76 % (3840414)Termination phase: Saturation % 282.69/40.76 % (3840414)Time elapsed: 14.801 s % 282.69/40.76 % (3840414)Peak memory usage: 154 MB % 282.69/40.76 % (3840414)Instructions burned: 17165 (million) % 282.69/40.76 % (3840487)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=769662757:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2728 on theBenchmark for (2728ds/2076Mi) % 282.69/40.76 % (3840466)------------------------------ % 282.69/40.76 % (3840466)------------------------------ % 282.69/40.76 % (3840448)Instruction limit reached! % 282.69/40.76 % (3840448)------------------------------ % 282.69/40.76 % (3840448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.69/40.76 % (3840448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.69/40.76 % (3840448)CaDiCaL version: 2.1.3 % 282.69/40.76 % (3840448)Termination reason: Instruction limit % 282.69/40.76 % (3840448)Termination phase: Saturation % 282.69/40.76 % (3840448)Time elapsed: 3.514 s % 282.69/40.76 % (3840448)Peak memory usage: 152 MB % 282.69/40.76 % (3840448)Instructions burned: 4081 (million) % 282.69/40.76 % (3840560)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=97694804:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2726 on theBenchmark for (2726ds/83971Mi) % 282.69/40.76 % (3840577)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1005940359:i=83944:rtra=on_2725 on theBenchmark for (2725ds/83944Mi) % 282.69/40.76 % (3840577)Refutation not found, incomplete strategy % 282.69/40.76 % (3840577)------------------------------ % 282.69/40.76 % (3840577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.69/40.76 % (3840577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.69/40.76 % (3840577)CaDiCaL version: 2.1.3 % 282.69/40.76 % (3840577)Termination reason: Refutation not found, incomplete strategy % 282.69/40.76 % (3840577)Time elapsed: 0.030 s % 282.69/40.76 % (3840577)Peak memory usage: 116 MB % 282.69/40.76 % (3840577)Instructions burned: 10 (million) % 282.69/40.76 % (3840577)------------------------------ % 282.69/40.76 % (3840577)------------------------------ % 282.69/40.76 % (3840627)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1284110298:i=9201:rtra=on_2721 on theBenchmark for (2721ds/9201Mi) % 282.69/40.76 % (3840487)Instruction limit reached! % 282.69/40.76 % (3840487)------------------------------ % 282.69/40.76 % (3840487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.69/40.76 % (3840487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.69/40.76 % (3840487)CaDiCaL version: 2.1.3 % 282.69/40.76 % (3840487)Termination reason: Instruction limit % 282.69/40.76 % (3840487)Termination phase: Saturation % 282.69/40.76 % (3840487)Time elapsed: 1.065 s % 282.69/40.76 % (3840487)Peak memory usage: 126 MB % 282.69/40.76 % (3840487)Instructions burned: 2076 (million) % 282.69/40.76 % (3840629)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 % 282.69/40.76 % (3840629)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1350855941:i=6806:aac=none:nm=0:rtra=on:rawr=on_2715 on theBenchmark for (2715ds/6806Mi) % 282.69/40.76 % (3840442)Instruction limit reached! % 282.69/40.76 % (3840442)------------------------------ % 282.69/40.76 % (3840442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.69/40.76 % (3840442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.99/42.08 % (3840442)CaDiCaL version: 2.1.3 % 291.99/42.08 % (3840442)Termination reason: Instruction limit % 291.99/42.08 % (3840442)Termination phase: Saturation % 291.99/42.08 % (3840442)Time elapsed: 5.942 s % 291.99/42.08 % (3840442)Peak memory usage: 194 MB % 291.99/42.08 % (3840442)Instructions burned: 11748 (million) % 291.99/42.08 % (3840631)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3371132963:s2a=on:i=3553:nm=0:rtra=on_2711 on theBenchmark for (2711ds/3553Mi) % 291.99/42.08 % (3840631)Instruction limit reached! % 291.99/42.08 % (3840631)------------------------------ % 291.99/42.08 % (3840631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.99/42.08 % (3840631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.99/42.08 % (3840631)CaDiCaL version: 2.1.3 % 291.99/42.08 % (3840631)Termination reason: Instruction limit % 291.99/42.08 % (3840631)Termination phase: Saturation % 291.99/42.08 % (3840631)Time elapsed: 2.084 s % 291.99/42.08 % (3840631)Peak memory usage: 99 MB % 291.99/42.08 % (3840631)Instructions burned: 3553 (million) % 291.99/42.08 % (3840629)Instruction limit reached! % 291.99/42.08 % (3840629)------------------------------ % 291.99/42.08 % (3840629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.99/42.08 % (3840629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.99/42.08 % (3840629)CaDiCaL version: 2.1.3 % 291.99/42.08 % (3840629)Termination reason: Instruction limit % 291.99/42.08 % (3840629)Termination phase: Saturation % 291.99/42.08 % (3840629)Time elapsed: 2.634 s % 291.99/42.08 % (3840629)Peak memory usage: 129 MB % 291.99/42.08 % (3840629)Instructions burned: 6807 (million) % 291.99/42.08 % (3840633)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=2734243887:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2689 on theBenchmark for (2689ds/2064Mi) % 291.99/42.08 % (3840634)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=3030493215:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2687 on theBenchmark for (2687ds/20260Mi) % 291.99/42.08 % (3840627)Instruction limit reached! % 291.99/42.08 % (3840627)------------------------------ % 291.99/42.08 % (3840627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.99/42.08 % (3840627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.99/42.08 % (3840627)CaDiCaL version: 2.1.3 % 291.99/42.08 % (3840627)Termination reason: Instruction limit % 291.99/42.08 % (3840627)Termination phase: Saturation % 291.99/42.08 % (3840627)Time elapsed: 4.279 s % 291.99/42.08 % (3840627)Peak memory usage: 115 MB % 291.99/42.08 % (3840627)Instructions burned: 9201 (million) % 291.99/42.08 % (3840637)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2298354149:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2677 on theBenchmark for (2677ds/1244Mi) % 291.99/42.08 % (3840637)Refutation not found, incomplete strategy % 291.99/42.08 % (3840637)------------------------------ % 291.99/42.08 % (3840637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.99/42.08 % (3840637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.99/42.08 % (3840637)CaDiCaL version: 2.1.3 % 291.99/42.08 % (3840637)Termination reason: Refutation not found, incomplete strategy % 291.99/42.08 % (3840637)Time elapsed: 0.029 s % 291.99/42.08 % (3840637)Peak memory usage: 116 MB % 291.99/42.08 % (3840637)Instructions burned: 8 (million) % 291.99/42.08 % (3840633)Instruction limit reached! % 291.99/42.08 % (3840633)------------------------------ % 291.99/42.08 % (3840633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.99/42.08 % (3840633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.99/42.08 % (3840633)CaDiCaL version: 2.1.3 % 291.99/42.08 % (3840633)Termination reason: Instruction limit % 291.99/42.08 % (3840633)Termination phase: Saturation % 291.99/42.08 % (3840633)Time elapsed: 1.246 s % 291.99/42.08 % (3840633)Peak memory usage: 144 MB % 291.99/42.08 % (3840633)Instructions burned: 2065 (million) % 291.99/42.08 % (3840639)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=2505806894:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2675 on theBenchmark for (2675ds/58261Mi) % 291.99/42.08 % (3840637)------------------------------ % 291.99/42.08 % (3840637)------------------------------ % 291.99/42.08 % (3840641)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 % 296.64/42.73 % (3840641)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1818727654:i=6806:aac=none:nm=0:rtra=on:rawr=on_2672 on theBenchmark for (2672ds/6806Mi) % 296.64/42.73 % (3840450)Instruction limit reached! % 296.64/42.73 % (3840450)------------------------------ % 296.64/42.73 % (3840450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.64/42.73 % (3840450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.64/42.73 % (3840450)CaDiCaL version: 2.1.3 % 296.64/42.73 % (3840450)Termination reason: Instruction limit % 296.64/42.73 % (3840450)Termination phase: Saturation % 296.64/42.73 % (3840450)Time elapsed: 9.935 s % 296.64/42.73 % (3840450)Peak memory usage: 154 MB % 296.64/42.73 % (3840450)Instructions burned: 20261 (million) % 296.64/42.73 % (3840643)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=3120990898:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2652 on theBenchmark for (2652ds/4081Mi) % 296.64/42.73 % (3840641)Instruction limit reached! % 296.64/42.73 % (3840641)------------------------------ % 296.64/42.73 % (3840641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.64/42.73 % (3840641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.64/42.73 % (3840641)CaDiCaL version: 2.1.3 % 296.64/42.73 % (3840641)Termination reason: Instruction limit % 296.64/42.73 % (3840641)Termination phase: Saturation % 296.64/42.73 % (3840641)Time elapsed: 2.654 s % 296.64/42.73 % (3840641)Peak memory usage: 139 MB % 296.64/42.73 % (3840641)Instructions burned: 6806 (million) % 296.64/42.73 % (3840645)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1691175759:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2644 on theBenchmark for (2644ds/1701Mi) % 296.64/42.73 % (3840645)Refutation not found, incomplete strategy % 296.64/42.73 % (3840645)------------------------------ % 296.64/42.73 % (3840645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.64/42.73 % (3840645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.64/42.73 % (3840645)CaDiCaL version: 2.1.3 % 296.64/42.73 % (3840645)Termination reason: Refutation not found, incomplete strategy % 296.64/42.73 % (3840645)Time elapsed: 0.029 s % 296.64/42.73 % (3840645)Peak memory usage: 116 MB % 296.64/42.73 % (3840645)Instructions burned: 8 (million) % 296.64/42.73 % (3840645)------------------------------ % 296.64/42.73 % (3840645)------------------------------ % 296.64/42.73 % (3840647)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=2580335034:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2640 on theBenchmark for (2640ds/57001Mi) % 296.64/42.73 % (3840643)Instruction limit reached! % 296.64/42.73 % (3840643)------------------------------ % 296.64/42.73 % (3840643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.64/42.73 % (3840643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.64/42.73 % (3840643)CaDiCaL version: 2.1.3 % 296.64/42.73 % (3840643)Termination reason: Instruction limit % 296.64/42.73 % (3840643)Termination phase: Saturation % 296.64/42.73 % (3840643)Time elapsed: 2.458 s % 296.64/42.73 % (3840643)Peak memory usage: 151 MB % 296.64/42.73 % (3840643)Instructions burned: 4082 (million) % 296.64/42.73 % (3840649)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 % 296.64/42.73 % (3840649)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1787886734:i=8622:aac=none:nm=0:rtra=on:rawr=on_2625 on theBenchmark for (2625ds/8622Mi) % 296.64/42.73 % (3840634)Instruction limit reached! % 296.64/42.73 % (3840634)------------------------------ % 296.64/42.73 % (3840634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.64/42.73 % (3840634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.64/42.73 % (3840634)CaDiCaL version: 2.1.3 % 296.64/42.73 % (3840634)Termination reason: Instruction limit % 296.64/42.73 % (3840634)Termination phase: Saturation % 296.64/42.73 % (3840634)Time elapsed: 8.408 s % 300.42/43.23 % (3840634)Peak memory usage: 137 MB % 300.42/43.23 % (3840634)Instructions burned: 20263 (million) % 300.42/43.23 % (3840651)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=35278834:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2602 on theBenchmark for (2602ds/24Mi) % 300.42/43.23 % (3840651)Instruction limit reached! % 300.42/43.23 % (3840651)------------------------------ % 300.42/43.23 % (3840651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.42/43.23 % (3840651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/43.23 % (3840651)CaDiCaL version: 2.1.3 % 300.42/43.23 % (3840651)Termination reason: Instruction limit % 300.42/43.23 % (3840651)Termination phase: Saturation % 300.42/43.23 % (3840651)Time elapsed: 0.037 s % 300.42/43.23 % (3840651)Peak memory usage: 115 MB % 300.42/43.23 % (3840651)Instructions burned: 24 (million) % 300.42/43.23 % (3840653)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3981694136:i=614:kws=precedence:nm=0:rtra=on_2600 on theBenchmark for (2600ds/614Mi) % 300.42/43.23 % (3840653)Refutation not found, incomplete strategy % 300.42/43.23 % (3840653)------------------------------ % 300.42/43.23 % (3840653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.42/43.23 % (3840653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/43.23 % (3840653)CaDiCaL version: 2.1.3 % 300.42/43.23 % (3840653)Termination reason: Refutation not found, incomplete strategy % 300.42/43.23 % (3840653)Time elapsed: 0.049 s % 300.42/43.23 % (3840653)Peak memory usage: 116 MB % 300.42/43.23 % (3840653)Instructions burned: 40 (million) % 300.42/43.23 % (3840653)------------------------------ % 300.42/43.23 % (3840653)------------------------------ % 300.42/43.23 % (3840655)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2219384520:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2595 on theBenchmark for (2595ds/402Mi) % 300.42/43.23 % (3840655)Instruction limit reached! % 300.42/43.23 % (3840655)------------------------------ % 300.42/43.23 % (3840655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.42/43.23 % (3840655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/43.23 % (3840655)CaDiCaL version: 2.1.3 % 300.42/43.23 % (3840655)Termination reason: Instruction limit % 300.42/43.23 % (3840655)Termination phase: Saturation % 300.42/43.23 % (3840655)Time elapsed: 0.249 s % 300.42/43.23 % (3840655)Peak memory usage: 118 MB % 300.42/43.23 % (3840655)Instructions burned: 403 (million) % 300.42/43.23 % (3840649)Instruction limit reached! % 300.42/43.23 % (3840649)------------------------------ % 300.42/43.23 % (3840649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.42/43.23 % (3840649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/43.23 % (3840649)CaDiCaL version: 2.1.3 % 300.42/43.23 % (3840649)Termination reason: Instruction limit % 300.42/43.23 % (3840649)Termination phase: Saturation % 300.42/43.23 % (3840649)Time elapsed: 3.343 s % 300.42/43.23 % (3840649)Peak memory usage: 124 MB % 300.42/43.23 % (3840649)Instructions burned: 8625 (million) % 300.42/43.23 % (3840657)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2226343582:s2a=on:i=14:rtra=on:inst=on_2591 on theBenchmark for (2591ds/14Mi) % 300.42/43.23 % (3840657)Instruction limit reached! % 300.42/43.23 % (3840657)------------------------------ % 300.42/43.23 % (3840657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.42/43.23 % (3840657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/43.23 % (3840657)CaDiCaL version: 2.1.3 % 300.42/43.23 % (3840657)Termination reason: Instruction limit % 300.42/43.23 % (3840657)Termination phase: Saturation % 300.42/43.23 % (3840657)Time elapsed: 0.013 s % 300.42/43.23 % (3840657)Peak memory usage: 89 MB % 300.42/43.23 % (3840657)Instructions burned: 18 (million) % 300.42/43.23 % (3840658)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1009148696:i=8:rtra=on_2590 on theBenchmark for (2590ds/8Mi) % 300.42/43.23 % (3840658)Instruction limit reached! % 300.42/43.23 % (3840658)------------------------------ % 300.42/43.23 % (3840658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.42/43.23 % (3840658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.42/43.23 % (3840658)CaDiCaL version: 2.1.3 % 300.42/43.23 % (3840658)Termination reason: Instruction limit % 300.42/43.23 % (3840658)Termination phase: Saturation % 300.42/43.23 % (3 % 300.42/43.23 Terminated %------------------------------------------------------------------------------