%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC455_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 : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:03:59 PM UTC 2026 % Result : Timeout 288.35s 41.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC455_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.21 % Computer : n015.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 09:42:47 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.25 Running first-order theorem proving % 0.09/0.25 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.06/1.14 % (2505960)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.06/1.14 % (2506012)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=656925587:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.06/1.14 % (2506011)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=85134109:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.06/1.14 % (2506007)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=157817305:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.06/1.14 % (2506009)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3303592323:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.06/1.14 % (2506008)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3256358624:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.06/1.14 % (2506011)Instruction limit reached! % 4.06/1.14 % (2506011)------------------------------ % 4.06/1.14 % (2506011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.06/1.14 % (2506011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/1.14 % (2506011)CaDiCaL version: 2.1.3 % 4.06/1.14 % (2506011)Termination reason: Instruction limit % 4.06/1.14 % (2506011)Termination phase: Saturation % 4.06/1.14 % (2506011)Time elapsed: 0.003 s % 4.06/1.14 % (2506011)Peak memory usage: 89 MB % 4.06/1.14 % (2506011)Instructions burned: 4 (million) % 4.06/1.14 % (2506012)Refutation not found, incomplete strategy % 4.06/1.14 % (2506012)------------------------------ % 4.06/1.14 % (2506012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.06/1.14 % (2506012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/1.14 % (2506012)CaDiCaL version: 2.1.3 % 4.06/1.14 % (2506012)Termination reason: Refutation not found, incomplete strategy % 4.06/1.14 % (2506012)Time elapsed: 0.018 s % 4.06/1.14 % (2506012)Peak memory usage: 116 MB % 4.06/1.14 % (2506012)Instructions burned: 7 (million) % 4.06/1.14 % (2506010)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2629878521:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.06/1.14 % (2506010)Instruction limit reached! % 4.06/1.14 % (2506010)------------------------------ % 4.06/1.14 % (2506010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.06/1.14 % (2506010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/1.14 % (2506010)CaDiCaL version: 2.1.3 % 4.06/1.14 % (2506010)Termination reason: Instruction limit % 4.06/1.14 % (2506010)Termination phase: Saturation % 4.06/1.14 % (2506010)Time elapsed: 0.005 s % 4.06/1.14 % (2506010)Peak memory usage: 88 MB % 4.06/1.14 % (2506010)Instructions burned: 8 (million) % 4.06/1.14 % (2506007)Instruction limit reached! % 4.06/1.14 % (2506007)------------------------------ % 4.06/1.14 % (2506007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.06/1.14 % (2506007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/1.14 % (2506007)CaDiCaL version: 2.1.3 % 4.06/1.14 % (2506007)Termination reason: Instruction limit % 4.06/1.14 % (2506007)Termination phase: Saturation % 4.06/1.14 % (2506007)Time elapsed: 0.034 s % 4.06/1.14 % (2506007)Peak memory usage: 116 MB % 4.06/1.14 % (2506007)Instructions burned: 18 (million) % 4.06/1.14 % (2506008)Refutation not found, incomplete strategy % 4.06/1.14 % (2506008)------------------------------ % 4.06/1.14 % (2506008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.06/1.14 % (2506008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/1.14 % (2506008)CaDiCaL version: 2.1.3 % 4.06/1.14 % (2506008)Termination reason: Refutation not found, incomplete strategy % 4.06/1.14 % (2506008)Time elapsed: 0.056 s % 4.06/1.14 % (2506008)Peak memory usage: 116 MB % 4.06/1.14 % (2506008)Instructions burned: 47 (million) % 4.06/1.14 % (2506013)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3909518637:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.06/1.14 % (2506013)Instruction limit reached! % 4.06/1.14 % (2506013)------------------------------ % 4.06/1.14 % (2506013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.06/1.14 % (2506013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.15/1.35 % (2506013)CaDiCaL version: 2.1.3 % 5.15/1.35 % (2506013)Termination reason: Instruction limit % 5.15/1.35 % (2506013)Termination phase: Saturation % 5.15/1.35 % (2506013)Time elapsed: 0.064 s % 5.15/1.35 % (2506013)Peak memory usage: 117 MB % 5.15/1.35 % (2506013)Instructions burned: 33 (million) % 5.15/1.35 % (2506019)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2978451708:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 5.15/1.35 % (2506019)Refutation not found, incomplete strategy % 5.15/1.35 % (2506019)------------------------------ % 5.15/1.35 % (2506019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.15/1.35 % (2506019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.15/1.35 % (2506019)CaDiCaL version: 2.1.3 % 5.15/1.35 % (2506019)Termination reason: Refutation not found, incomplete strategy % 5.15/1.35 % (2506019)Time elapsed: 0.001 s % 5.15/1.35 % (2506019)Peak memory usage: 89 MB % 5.15/1.35 % (2506019)Instructions burned: 1 (million) % 5.15/1.35 % (2506021)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=3930587298:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 5.15/1.35 % (2506012)------------------------------ % 5.15/1.35 % (2506012)------------------------------ % 5.15/1.35 % (2506009)Instruction limit reached! % 5.15/1.35 % (2506009)------------------------------ % 5.15/1.35 % (2506009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.15/1.35 % (2506009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.15/1.35 % (2506009)CaDiCaL version: 2.1.3 % 5.15/1.35 % (2506009)Termination reason: Instruction limit % 5.15/1.35 % (2506009)Termination phase: Saturation % 5.15/1.35 % (2506009)Time elapsed: 0.167 s % 5.15/1.35 % (2506009)Peak memory usage: 117 MB % 5.15/1.35 % (2506009)Instructions burned: 201 (million) % 5.15/1.35 % (2506021)Instruction limit reached! % 5.15/1.35 % (2506021)------------------------------ % 5.15/1.35 % (2506021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.15/1.35 % (2506021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.15/1.35 % (2506021)CaDiCaL version: 2.1.3 % 5.15/1.35 % (2506021)Termination reason: Instruction limit % 5.15/1.35 % (2506021)Termination phase: Saturation % 5.15/1.35 % (2506021)Time elapsed: 0.018 s % 5.15/1.35 % (2506021)Peak memory usage: 88 MB % 5.15/1.35 % (2506021)Instructions burned: 29 (million) % 5.15/1.35 % (2506022)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2919041856:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 5.15/1.35 % (2506022)Instruction limit reached! % 5.15/1.35 % (2506022)------------------------------ % 5.15/1.35 % (2506022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.15/1.35 % (2506022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.15/1.35 % (2506022)CaDiCaL version: 2.1.3 % 5.15/1.35 % (2506022)Termination reason: Instruction limit % 5.15/1.35 % (2506022)Termination phase: Saturation % 5.15/1.35 % (2506022)Time elapsed: 0.009 s % 5.15/1.35 % (2506022)Peak memory usage: 90 MB % 5.15/1.35 % (2506022)Instructions burned: 16 (million) % 5.15/1.35 % (2506027)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=1399223517:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 5.15/1.35 % (2506027)Instruction limit reached! % 5.15/1.35 % (2506027)------------------------------ % 5.15/1.35 % (2506027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.15/1.35 % (2506027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.15/1.35 % (2506027)CaDiCaL version: 2.1.3 % 5.15/1.35 % (2506027)Termination reason: Instruction limit % 5.15/1.35 % (2506027)Termination phase: Saturation % 5.15/1.35 % (2506027)Time elapsed: 0.008 s % 5.15/1.35 % (2506027)Peak memory usage: 89 MB % 5.15/1.35 % (2506027)Instructions burned: 31 (million) % 5.15/1.35 % (2506025)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=638166217:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 5.15/1.35 % (2506025)Instruction limit reached! % 5.15/1.35 % (2506025)------------------------------ % 5.15/1.35 % (2506025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.06/1.61 % (2506025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.61 % (2506025)CaDiCaL version: 2.1.3 % 7.06/1.61 % (2506025)Termination reason: Instruction limit % 7.06/1.61 % (2506025)Termination phase: Saturation % 7.06/1.61 % (2506025)Time elapsed: 0.018 s % 7.06/1.61 % (2506025)Peak memory usage: 89 MB % 7.06/1.61 % (2506025)Instructions burned: 25 (million) % 7.06/1.61 % (2506029)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3649866904:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 7.06/1.61 % (2506029)Instruction limit reached! % 7.06/1.61 % (2506029)------------------------------ % 7.06/1.61 % (2506029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.06/1.61 % (2506029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.61 % (2506029)CaDiCaL version: 2.1.3 % 7.06/1.61 % (2506029)Termination reason: Instruction limit % 7.06/1.61 % (2506029)Termination phase: Saturation % 7.06/1.61 % (2506029)Time elapsed: 0.003 s % 7.06/1.61 % (2506029)Peak memory usage: 89 MB % 7.06/1.61 % (2506029)Instructions burned: 3 (million) % 7.06/1.61 % (2506028)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3044939694:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 7.06/1.61 % (2506008)------------------------------ % 7.06/1.61 % (2506008)------------------------------ % 7.06/1.61 % (2506031)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1911522907:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 7.06/1.61 % (2506031)Refutation not found, incomplete strategy % 7.06/1.61 % (2506031)------------------------------ % 7.06/1.61 % (2506031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.06/1.61 % (2506031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.61 % (2506031)CaDiCaL version: 2.1.3 % 7.06/1.61 % (2506031)Termination reason: Refutation not found, incomplete strategy % 7.06/1.61 % (2506031)Time elapsed: 0.007 s % 7.06/1.61 % (2506031)Peak memory usage: 89 MB % 7.06/1.61 % (2506031)Instructions burned: 5 (million) % 7.06/1.61 % (2506028)Instruction limit reached! % 7.06/1.61 % (2506028)------------------------------ % 7.06/1.61 % (2506028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.06/1.61 % (2506028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.61 % (2506028)CaDiCaL version: 2.1.3 % 7.06/1.61 % (2506028)Termination reason: Instruction limit % 7.06/1.61 % (2506028)Termination phase: Saturation % 7.06/1.61 % (2506028)Time elapsed: 0.085 s % 7.06/1.61 % (2506028)Peak memory usage: 89 MB % 7.06/1.61 % (2506028)Instructions burned: 85 (million) % 7.06/1.61 % (2506019)------------------------------ % 7.06/1.61 % (2506019)------------------------------ % 7.06/1.61 % (2506033)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3006808878:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 7.06/1.61 % (2506033)Instruction limit reached! % 7.06/1.61 % (2506033)------------------------------ % 7.06/1.61 % (2506033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.06/1.61 % (2506033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.61 % (2506033)CaDiCaL version: 2.1.3 % 7.06/1.61 % (2506033)Termination reason: Instruction limit % 7.06/1.61 % (2506033)Termination phase: Saturation % 7.06/1.61 % (2506033)Time elapsed: 0.004 s % 7.06/1.61 % (2506033)Peak memory usage: 89 MB % 7.06/1.61 % (2506033)Instructions burned: 8 (million) % 7.06/1.61 % (2506036)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1638840528:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 7.06/1.61 % (2506047)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=2472605148:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 7.06/1.61 % (2506044)lrs+10_1_thi=all:si=on:fd=off:random_seed=1602442279:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 7.06/1.61 % (2506047)Instruction limit reached! % 7.06/1.61 % (2506047)------------------------------ % 7.06/1.61 % (2506047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.06/1.61 % (2506047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.61 % (2506047)CaDiCaL version: 2.1.3 % 7.06/1.61 % (2506047)Termination reason: Instruction limit % 7.89/1.88 % (2506047)Termination phase: Saturation % 7.89/1.88 % (2506047)Time elapsed: 0.008 s % 7.89/1.88 % (2506047)Peak memory usage: 88 MB % 7.89/1.88 % (2506047)Instructions burned: 8 (million) % 7.89/1.88 % (2506050)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=566203830:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 7.89/1.88 % (2506050)Instruction limit reached! % 7.89/1.88 % (2506050)------------------------------ % 7.89/1.88 % (2506050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.89/1.88 % (2506050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.89/1.88 % (2506050)CaDiCaL version: 2.1.3 % 7.89/1.88 % (2506050)Termination reason: Instruction limit % 7.89/1.88 % (2506050)Termination phase: Saturation % 7.89/1.88 % (2506050)Time elapsed: 0.002 s % 7.89/1.88 % (2506050)Peak memory usage: 89 MB % 7.89/1.88 % (2506050)Instructions burned: 3 (million) % 7.89/1.88 % (2506051)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3112248933:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 7.89/1.88 % (2506051)Instruction limit reached! % 7.89/1.88 % (2506051)------------------------------ % 7.89/1.88 % (2506051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.89/1.88 % (2506051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.89/1.88 % (2506051)CaDiCaL version: 2.1.3 % 7.89/1.88 % (2506051)Termination reason: Instruction limit % 7.89/1.88 % (2506051)Termination phase: Saturation % 7.89/1.88 % (2506051)Time elapsed: 0.006 s % 7.89/1.88 % (2506051)Peak memory usage: 89 MB % 7.89/1.88 % (2506051)Instructions burned: 5 (million) % 7.89/1.88 % (2506044)Instruction limit reached! % 7.89/1.88 % (2506044)------------------------------ % 7.89/1.88 % (2506044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.89/1.88 % (2506044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.89/1.88 % (2506044)CaDiCaL version: 2.1.3 % 7.89/1.88 % (2506044)Termination reason: Instruction limit % 7.89/1.88 % (2506044)Termination phase: Saturation % 7.89/1.88 % (2506044)Time elapsed: 0.075 s % 7.89/1.88 % (2506044)Peak memory usage: 116 MB % 7.89/1.88 % (2506044)Instructions burned: 53 (million) % 7.89/1.88 % (2506052)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=577310832:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 7.89/1.88 % (2506036)Instruction limit reached! % 7.89/1.88 % (2506036)------------------------------ % 7.89/1.88 % (2506036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.89/1.88 % (2506036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.89/1.88 % (2506036)CaDiCaL version: 2.1.3 % 7.89/1.88 % (2506036)Termination reason: Instruction limit % 7.89/1.88 % (2506036)Termination phase: Saturation % 7.89/1.88 % (2506036)Time elapsed: 0.133 s % 7.89/1.88 % (2506036)Peak memory usage: 134 MB % 7.89/1.88 % (2506036)Instructions burned: 66 (million) % 7.89/1.88 % (2506066)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3242219425:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 7.89/1.88 % (2506066)Refutation not found, incomplete strategy % 7.89/1.88 % (2506066)------------------------------ % 7.89/1.88 % (2506066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.89/1.88 % (2506066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.89/1.88 % (2506066)CaDiCaL version: 2.1.3 % 7.89/1.88 % (2506066)Termination reason: Refutation not found, incomplete strategy % 7.89/1.88 % (2506066)Time elapsed: 0.002 s % 7.89/1.88 % (2506066)Peak memory usage: 89 MB % 7.89/1.88 % (2506066)Instructions burned: 2 (million) % 7.89/1.88 % (2506031)------------------------------ % 7.89/1.88 % (2506031)------------------------------ % 7.89/1.88 % (2506052)Instruction limit reached! % 7.89/1.88 % (2506052)------------------------------ % 7.89/1.88 % (2506052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.89/1.88 % (2506052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.89/1.88 % (2506052)CaDiCaL version: 2.1.3 % 7.89/1.88 % (2506052)Termination reason: Instruction limit % 7.89/1.88 % (2506052)Termination phase: Saturation % 7.89/1.88 % (2506052)Time elapsed: 0.101 s % 7.89/1.88 % (2506052)Peak memory usage: 116 MB % 7.89/1.88 % (2506052)Instructions burned: 128 (million) % 7.89/1.88 % (2506060)dis+10_1_si=on:random_seed=2007436042:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 11.79/2.26 % (2506060)Instruction limit reached! % 11.79/2.26 % (2506060)------------------------------ % 11.79/2.26 % (2506060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.79/2.26 % (2506060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.79/2.26 % (2506060)CaDiCaL version: 2.1.3 % 11.79/2.26 % (2506060)Termination reason: Instruction limit % 11.79/2.26 % (2506060)Termination phase: Saturation % 11.79/2.26 % (2506060)Time elapsed: 0.010 s % 11.79/2.26 % (2506060)Peak memory usage: 88 MB % 11.79/2.26 % (2506060)Instructions burned: 11 (million) % 11.79/2.26 % (2506069)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=802482862: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_2992 on theBenchmark for (2992ds/35Mi) % 11.79/2.26 % (2506073)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3965294012:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi) % 11.79/2.26 % (2506073)Instruction limit reached! % 11.79/2.26 % (2506073)------------------------------ % 11.79/2.26 % (2506073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.79/2.26 % (2506073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.79/2.26 % (2506073)CaDiCaL version: 2.1.3 % 11.79/2.26 % (2506073)Termination reason: Instruction limit % 11.79/2.26 % (2506073)Termination phase: Saturation % 11.79/2.26 % (2506073)Time elapsed: 0.004 s % 11.79/2.26 % (2506073)Peak memory usage: 89 MB % 11.79/2.26 % (2506073)Instructions burned: 3 (million) % 11.79/2.26 % (2506069)Instruction limit reached! % 11.79/2.26 % (2506069)------------------------------ % 11.79/2.26 % (2506069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.79/2.26 % (2506069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.79/2.26 % (2506069)CaDiCaL version: 2.1.3 % 11.79/2.26 % (2506069)Termination reason: Instruction limit % 11.79/2.26 % (2506069)Termination phase: Saturation % 11.79/2.26 % (2506069)Time elapsed: 0.038 s % 11.79/2.26 % (2506069)Peak memory usage: 89 MB % 11.79/2.26 % (2506069)Instructions burned: 35 (million) % 11.79/2.26 % (2506075)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1321993271:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 11.79/2.26 % (2506075)Instruction limit reached! % 11.79/2.26 % (2506075)------------------------------ % 11.79/2.26 % (2506075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.79/2.26 % (2506080)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2457091664:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 11.79/2.26 % (2506075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.79/2.26 % (2506075)CaDiCaL version: 2.1.3 % 11.79/2.26 % (2506075)Termination reason: Instruction limit % 11.79/2.26 % (2506075)Termination phase: Saturation % 11.79/2.26 % (2506075)Time elapsed: 0.010 s % 11.79/2.26 % (2506075)Peak memory usage: 89 MB % 11.79/2.26 % (2506075)Instructions burned: 8 (million) % 11.79/2.26 % (2506066)------------------------------ % 11.79/2.26 % (2506066)------------------------------ % 11.79/2.26 % (2506082)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1637418575:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi) % 11.79/2.26 % (2506084)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2240620679:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi) % 11.79/2.26 % (2506082)Instruction limit reached! % 11.79/2.26 % (2506082)------------------------------ % 11.79/2.26 % (2506082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.79/2.26 % (2506082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.79/2.26 % (2506082)CaDiCaL version: 2.1.3 % 11.79/2.26 % (2506082)Termination reason: Instruction limit % 11.79/2.26 % (2506082)Termination phase: Saturation % 11.79/2.26 % (2506082)Time elapsed: 0.035 s % 11.79/2.26 % (2506082)Peak memory usage: 116 MB % 11.79/2.26 % (2506082)Instructions burned: 13 (million) % 11.79/2.26 % (2506084)Refutation not found, incomplete strategy % 11.79/2.26 % (2506084)------------------------------ % 11.79/2.26 % (2506084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.79/2.26 % (2506084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.78/2.65 % (2506084)CaDiCaL version: 2.1.3 % 12.78/2.65 % (2506084)Termination reason: Refutation not found, incomplete strategy % 12.78/2.65 % (2506084)Time elapsed: 0.039 s % 12.78/2.65 % (2506084)Peak memory usage: 116 MB % 12.78/2.65 % (2506084)Instructions burned: 7 (million) % 12.78/2.65 % (2506101)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=204412490:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi) % 12.78/2.65 % (2506090)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=867784848:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 12.78/2.65 % (2506092)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=895886164:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi) % 12.78/2.65 % (2506090)Refutation not found, incomplete strategy % 12.78/2.65 % (2506090)------------------------------ % 12.78/2.65 % (2506090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.78/2.65 % (2506090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.78/2.65 % (2506090)CaDiCaL version: 2.1.3 % 12.78/2.65 % (2506090)Termination reason: Refutation not found, incomplete strategy % 12.78/2.65 % (2506090)Time elapsed: 0.002 s % 12.78/2.65 % (2506090)Peak memory usage: 88 MB % 12.78/2.65 % (2506090)Instructions burned: 1 (million) % 12.78/2.65 % (2506099)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=478281139:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 12.78/2.65 % (2506092)Refutation not found, incomplete strategy % 12.78/2.65 % (2506092)------------------------------ % 12.78/2.65 % (2506092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.78/2.65 % (2506092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.78/2.65 % (2506092)CaDiCaL version: 2.1.3 % 12.78/2.65 % (2506092)Termination reason: Refutation not found, incomplete strategy % 12.78/2.65 % (2506092)Time elapsed: 0.073 s % 12.78/2.65 % (2506092)Peak memory usage: 132 MB % 12.78/2.65 % (2506092)Instructions burned: 12 (million) % 12.78/2.65 % (2506080)Instruction limit reached! % 12.78/2.65 % (2506080)------------------------------ % 12.78/2.65 % (2506080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.78/2.65 % (2506080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.78/2.65 % (2506080)CaDiCaL version: 2.1.3 % 12.78/2.65 % (2506080)Termination reason: Instruction limit % 12.78/2.65 % (2506080)Termination phase: Saturation % 12.78/2.65 % (2506080)Time elapsed: 0.230 s % 12.78/2.65 % (2506080)Peak memory usage: 89 MB % 12.78/2.65 % (2506080)Instructions burned: 372 (million) % 12.78/2.65 % (2506101)Instruction limit reached! % 12.78/2.65 % (2506101)------------------------------ % 12.78/2.65 % (2506101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.78/2.65 % (2506101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.78/2.65 % (2506101)CaDiCaL version: 2.1.3 % 12.78/2.65 % (2506101)Termination reason: Instruction limit % 12.78/2.65 % (2506101)Termination phase: Saturation % 12.78/2.65 % (2506101)Time elapsed: 0.093 s % 12.78/2.65 % (2506101)Peak memory usage: 88 MB % 12.78/2.65 % (2506101)Instructions burned: 296 (million) % 12.78/2.65 % (2506099)Instruction limit reached! % 12.78/2.65 % (2506099)------------------------------ % 12.78/2.65 % (2506099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.78/2.65 % (2506099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.78/2.65 % (2506099)CaDiCaL version: 2.1.3 % 12.78/2.65 % (2506099)Termination reason: Instruction limit % 12.78/2.65 % (2506099)Termination phase: Saturation % 12.78/2.65 % (2506099)Time elapsed: 0.054 s % 12.78/2.65 % (2506099)Peak memory usage: 89 MB % 12.78/2.65 % (2506099)Instructions burned: 76 (million) % 12.78/2.65 % (2506106)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=832868066:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 12.78/2.65 % (2506106)Refutation not found, incomplete strategy % 12.78/2.65 % (2506106)------------------------------ % 12.78/2.65 % (2506106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.78/2.65 % (2506106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.10 % (2506106)CaDiCaL version: 2.1.3 % 18.17/3.10 % (2506106)Termination reason: Refutation not found, incomplete strategy % 18.17/3.10 % (2506106)Time elapsed: 0.072 s % 18.17/3.10 % (2506106)Peak memory usage: 118 MB % 18.17/3.10 % (2506106)Instructions burned: 40 (million) % 18.17/3.10 % (2506117)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2639475482:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi) % 18.17/3.10 % (2506117)Instruction limit reached! % 18.17/3.10 % (2506117)------------------------------ % 18.17/3.10 % (2506117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.10 % (2506117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.10 % (2506117)CaDiCaL version: 2.1.3 % 18.17/3.10 % (2506117)Termination reason: Instruction limit % 18.17/3.10 % (2506117)Termination phase: Saturation % 18.17/3.10 % (2506117)Time elapsed: 0.041 s % 18.17/3.10 % (2506117)Peak memory usage: 133 MB % 18.17/3.10 % (2506117)Instructions burned: 43 (million) % 18.17/3.10 % (2506116)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4132937648:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 18.17/3.10 % (2506084)------------------------------ % 18.17/3.10 % (2506084)------------------------------ % 18.17/3.10 % (2506122)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4186545978:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi) % 18.17/3.10 % (2506090)------------------------------ % 18.17/3.10 % (2506090)------------------------------ % 18.17/3.10 % (2506116)Refutation not found, incomplete strategy % 18.17/3.10 % (2506116)------------------------------ % 18.17/3.10 % (2506116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.10 % (2506116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.10 % (2506116)CaDiCaL version: 2.1.3 % 18.17/3.10 % (2506116)Termination reason: Refutation not found, incomplete strategy % 18.17/3.10 % (2506116)Time elapsed: 0.070 s % 18.17/3.10 % (2506116)Peak memory usage: 133 MB % 18.17/3.10 % (2506116)Instructions burned: 12 (million) % 18.17/3.10 % (2506092)------------------------------ % 18.17/3.10 % (2506092)------------------------------ % 18.17/3.10 % (2506135)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1105049705:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi) % 18.17/3.10 % (2506132)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2963125905:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi) % 18.17/3.10 % (2506137)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=1795298226:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi) % 18.17/3.10 % (2506132)Refutation not found, incomplete strategy % 18.17/3.10 % (2506132)------------------------------ % 18.17/3.10 % (2506132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.10 % (2506132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.10 % (2506132)CaDiCaL version: 2.1.3 % 18.17/3.10 % (2506132)Termination reason: Refutation not found, incomplete strategy % 18.17/3.10 % (2506132)Time elapsed: 0.076 s % 18.17/3.10 % (2506132)Peak memory usage: 133 MB % 18.17/3.10 % (2506132)Instructions burned: 13 (million) % 18.17/3.10 % (2506135)Instruction limit reached! % 18.17/3.10 % (2506135)------------------------------ % 18.17/3.10 % (2506135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.10 % (2506135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.10 % (2506135)CaDiCaL version: 2.1.3 % 18.17/3.10 % (2506135)Termination reason: Instruction limit % 18.17/3.10 % (2506135)Termination phase: Saturation % 18.17/3.10 % (2506135)Time elapsed: 0.086 s % 18.17/3.10 % (2506135)Peak memory usage: 118 MB % 18.17/3.10 % (2506135)Instructions burned: 132 (million) % 18.17/3.10 % (2506138)dis+10_1_si=on:random_seed=554643187:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi) % 18.17/3.10 % (2506106)------------------------------ % 18.17/3.10 % (2506106)------------------------------ % 18.17/3.10 % (2506122)Instruction limit reached! % 18.17/3.10 % (2506122)------------------------------ % 18.17/3.10 % (2506122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.10 % (2506122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.30/3.57 % (2506122)CaDiCaL version: 2.1.3 % 20.30/3.57 % (2506122)Termination reason: Instruction limit % 20.30/3.57 % (2506122)Termination phase: Saturation % 20.30/3.57 % (2506122)Time elapsed: 0.269 s % 20.30/3.57 % (2506122)Peak memory usage: 92 MB % 20.30/3.57 % (2506122)Instructions burned: 307 (million) % 20.30/3.57 % (2506116)------------------------------ % 20.30/3.57 % (2506116)------------------------------ % 20.30/3.57 % (2506155)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3497545278:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi) % 20.30/3.57 % (2506152)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1099276656:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 20.30/3.57 % (2506152)Refutation not found, incomplete strategy % 20.30/3.57 % (2506152)------------------------------ % 20.30/3.57 % (2506152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.30/3.57 % (2506152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.30/3.57 % (2506152)CaDiCaL version: 2.1.3 % 20.30/3.57 % (2506152)Termination reason: Refutation not found, incomplete strategy % 20.30/3.57 % (2506152)Time elapsed: 0.006 s % 20.30/3.57 % (2506152)Peak memory usage: 89 MB % 20.30/3.57 % (2506152)Instructions burned: 4 (million) % 20.30/3.57 % (2506137)Instruction limit reached! % 20.30/3.57 % (2506137)------------------------------ % 20.30/3.57 % (2506137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.30/3.57 % (2506137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.30/3.57 % (2506137)CaDiCaL version: 2.1.3 % 20.30/3.57 % (2506137)Termination reason: Instruction limit % 20.30/3.57 % (2506137)Termination phase: Saturation % 20.30/3.57 % (2506137)Time elapsed: 0.226 s % 20.30/3.57 % (2506137)Peak memory usage: 116 MB % 20.30/3.57 % (2506137)Instructions burned: 259 (million) % 20.30/3.57 % (2506159)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=454962003:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi) % 20.30/3.57 % (2506155)Instruction limit reached! % 20.30/3.57 % (2506155)------------------------------ % 20.30/3.57 % (2506155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.30/3.57 % (2506155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.30/3.57 % (2506155)CaDiCaL version: 2.1.3 % 20.30/3.57 % (2506155)Termination reason: Instruction limit % 20.30/3.57 % (2506155)Termination phase: Saturation % 20.30/3.57 % (2506155)Time elapsed: 0.068 s % 20.30/3.57 % (2506155)Peak memory usage: 90 MB % 20.30/3.57 % (2506155)Instructions burned: 141 (million) % 20.30/3.57 % (2506156)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2442045809:i=65:nm=16:rtra=on_2982 on theBenchmark for (2982ds/65Mi) % 20.30/3.57 % (2506156)Refutation not found, incomplete strategy % 20.30/3.57 % (2506156)------------------------------ % 20.30/3.57 % (2506156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.30/3.57 % (2506156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.30/3.57 % (2506156)CaDiCaL version: 2.1.3 % 20.30/3.57 % (2506156)Termination reason: Refutation not found, incomplete strategy % 20.30/3.57 % (2506156)Time elapsed: 0.038 s % 20.30/3.57 % (2506156)Peak memory usage: 115 MB % 20.30/3.57 % (2506156)Instructions burned: 6 (million) % 20.30/3.57 % (2506159)Instruction limit reached! % 20.30/3.57 % (2506159)------------------------------ % 20.30/3.57 % (2506159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.30/3.57 % (2506159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.30/3.57 % (2506159)CaDiCaL version: 2.1.3 % 20.30/3.57 % (2506159)Termination reason: Instruction limit % 20.30/3.57 % (2506159)Termination phase: Saturation % 20.30/3.57 % (2506159)Time elapsed: 0.057 s % 20.30/3.57 % (2506159)Peak memory usage: 88 MB % 20.30/3.57 % (2506159)Instructions burned: 121 (million) % 20.30/3.57 % (2506132)------------------------------ % 20.30/3.57 % (2506132)------------------------------ % 20.30/3.57 % (2506172)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=2306284804:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi) % 20.30/3.57 % (2506168)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=3680498089:s2a=on:i=128:s2at=5:ins=3:rtra=on_2980 on theBenchmark for (2980ds/128Mi) % 21.95/3.95 % (2506172)Instruction limit reached! % 21.95/3.95 % (2506172)------------------------------ % 21.95/3.95 % (2506172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.95/3.95 % (2506172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.95 % (2506172)CaDiCaL version: 2.1.3 % 21.95/3.95 % (2506172)Termination reason: Instruction limit % 21.95/3.95 % (2506172)Termination phase: Saturation % 21.95/3.95 % (2506172)Time elapsed: 0.039 s % 21.95/3.95 % (2506172)Peak memory usage: 116 MB % 21.95/3.95 % (2506172)Instructions burned: 41 (million) % 21.95/3.95 % (2506175)dis+1010_1_to=kbo:si=on:random_seed=1471374259:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi) % 21.95/3.95 % (2506168)Instruction limit reached! % 21.95/3.95 % (2506168)------------------------------ % 21.95/3.95 % (2506168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.95/3.95 % (2506168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.95 % (2506168)CaDiCaL version: 2.1.3 % 21.95/3.95 % (2506168)Termination reason: Instruction limit % 21.95/3.95 % (2506168)Termination phase: Saturation % 21.95/3.95 % (2506168)Time elapsed: 0.145 s % 21.95/3.95 % (2506168)Peak memory usage: 117 MB % 21.95/3.95 % (2506168)Instructions burned: 128 (million) % 21.95/3.95 % (2506152)------------------------------ % 21.95/3.95 % (2506152)------------------------------ % 21.95/3.95 % (2506177)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1351714326:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/329Mi) % 21.95/3.95 % (2506175)Instruction limit reached! % 21.95/3.95 % (2506175)------------------------------ % 21.95/3.95 % (2506175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.95/3.95 % (2506175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.95 % (2506175)CaDiCaL version: 2.1.3 % 21.95/3.95 % (2506175)Termination reason: Instruction limit % 21.95/3.95 % (2506175)Termination phase: Saturation % 21.95/3.95 % (2506175)Time elapsed: 0.140 s % 21.95/3.95 % (2506175)Peak memory usage: 91 MB % 21.95/3.95 % (2506175)Instructions burned: 175 (million) % 21.95/3.95 % (2506183)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3234461359:s2a=on:i=483:doe=on:nm=32:rtra=on_2977 on theBenchmark for (2977ds/483Mi) % 21.95/3.95 % (2506183)Refutation not found, incomplete strategy % 21.95/3.95 % (2506183)------------------------------ % 21.95/3.95 % (2506183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.95/3.95 % (2506183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.95 % (2506183)CaDiCaL version: 2.1.3 % 21.95/3.95 % (2506183)Termination reason: Refutation not found, incomplete strategy % 21.95/3.95 % (2506183)Time elapsed: 0.046 s % 21.95/3.95 % (2506183)Peak memory usage: 132 MB % 21.95/3.95 % (2506183)Instructions burned: 12 (million) % 21.95/3.95 % (2506156)------------------------------ % 21.95/3.95 % (2506156)------------------------------ % 21.95/3.95 % (2506192)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4076461054:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi) % 21.95/3.95 % (2506190)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=180910193:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi) % 21.95/3.95 % (2506195)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3927925525:st=2:i=295:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/295Mi) % 21.95/3.95 % (2506198)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3742136954:i=328:kws=inv_frequency:nm=20:rtra=on_2975 on theBenchmark for (2975ds/328Mi) % 21.95/3.95 % (2506192)Refutation not found, incomplete strategy % 21.95/3.95 % (2506192)------------------------------ % 21.95/3.95 % (2506192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.95/3.95 % (2506192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.95 % (2506192)CaDiCaL version: 2.1.3 % 21.95/3.95 % (2506192)Termination reason: Refutation not found, incomplete strategy % 21.95/3.95 % (2506192)Time elapsed: 0.039 s % 21.95/3.95 % (2506192)Peak memory usage: 116 MB % 21.95/3.95 % (2506192)Instructions burned: 7 (million) % 21.95/3.95 % (2506183)------------------------------ % 21.95/3.95 % (2506183)------------------------------ % 26.53/4.39 % (2506190)Refutation not found, incomplete strategy % 26.53/4.39 % (2506190)------------------------------ % 26.53/4.39 % (2506190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.53/4.39 % (2506190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.53/4.39 % (2506190)CaDiCaL version: 2.1.3 % 26.53/4.39 % (2506190)Termination reason: Refutation not found, incomplete strategy % 26.53/4.39 % (2506190)Time elapsed: 0.112 s % 26.53/4.39 % (2506190)Peak memory usage: 135 MB % 26.53/4.39 % (2506190)Instructions burned: 45 (million) % 26.53/4.39 % (2506138)Instruction limit reached! % 26.53/4.39 % (2506138)------------------------------ % 26.53/4.39 % (2506138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.53/4.39 % (2506138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.53/4.39 % (2506138)CaDiCaL version: 2.1.3 % 26.53/4.39 % (2506138)Termination reason: Instruction limit % 26.53/4.39 % (2506138)Termination phase: Saturation % 26.53/4.39 % (2506138)Time elapsed: 0.914 s % 26.53/4.39 % (2506138)Peak memory usage: 94 MB % 26.53/4.39 % (2506138)Instructions burned: 1000 (million) % 26.53/4.39 % (2506177)Instruction limit reached! % 26.53/4.39 % (2506177)------------------------------ % 26.53/4.39 % (2506177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.53/4.39 % (2506177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.53/4.39 % (2506177)CaDiCaL version: 2.1.3 % 26.53/4.39 % (2506177)Termination reason: Instruction limit % 26.53/4.39 % (2506177)Termination phase: Saturation % 26.53/4.39 % (2506177)Time elapsed: 0.389 s % 26.53/4.39 % (2506177)Peak memory usage: 118 MB % 26.53/4.39 % (2506177)Instructions burned: 329 (million) % 26.53/4.39 % (2506207)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1364477469:i=281:gtgl=2:rtra=on:gtg=all_2973 on theBenchmark for (2973ds/281Mi) % 26.53/4.39 % (2506195)Instruction limit reached! % 26.53/4.39 % (2506195)------------------------------ % 26.53/4.39 % (2506195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.53/4.39 % (2506195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.53/4.39 % (2506195)CaDiCaL version: 2.1.3 % 26.53/4.39 % (2506195)Termination reason: Instruction limit % 26.53/4.39 % (2506195)Termination phase: Saturation % 26.53/4.39 % (2506195)Time elapsed: 0.259 s % 26.53/4.39 % (2506195)Peak memory usage: 90 MB % 26.53/4.39 % (2506195)Instructions burned: 295 (million) % 26.53/4.39 % (2506198)Instruction limit reached! % 26.53/4.39 % (2506198)------------------------------ % 26.53/4.39 % (2506198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.53/4.39 % (2506198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.53/4.39 % (2506198)CaDiCaL version: 2.1.3 % 26.53/4.39 % (2506198)Termination reason: Instruction limit % 26.53/4.39 % (2506198)Termination phase: Saturation % 26.53/4.39 % (2506198)Time elapsed: 0.318 s % 26.53/4.39 % (2506198)Peak memory usage: 119 MB % 26.53/4.39 % (2506198)Instructions burned: 329 (million) % 26.53/4.39 % (2506210)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=950933191:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi) % 26.53/4.39 % (2506213)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2478721097:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2972 on theBenchmark for (2972ds/321Mi) % 26.53/4.39 % (2506192)------------------------------ % 26.53/4.39 % (2506192)------------------------------ % 26.53/4.39 % (2506207)Instruction limit reached! % 26.53/4.39 % (2506207)------------------------------ % 26.53/4.39 % (2506207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.53/4.39 % (2506207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.53/4.39 % (2506207)CaDiCaL version: 2.1.3 % 26.53/4.39 % (2506207)Termination reason: Instruction limit % 26.53/4.39 % (2506207)Termination phase: Saturation % 26.53/4.39 % (2506207)Time elapsed: 0.199 s % 26.53/4.39 % (2506207)Peak memory usage: 118 MB % 26.53/4.39 % (2506207)Instructions burned: 282 (million) % 26.53/4.39 % (2506216)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2830372498:i=416:rtra=on:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/416Mi) % 26.53/4.39 % (2506190)------------------------------ % 26.53/4.39 % (2506190)------------------------------ % 26.53/4.39 % (2506216)Refutation not found, incomplete strategy % 26.53/4.39 % (2506216)------------------------------ % 26.53/4.39 % (2506216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.50/4.74 % (2506216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.50/4.74 % (2506216)CaDiCaL version: 2.1.3 % 28.50/4.74 % (2506216)Termination reason: Refutation not found, incomplete strategy % 28.50/4.74 % (2506216)Time elapsed: 0.040 s % 28.50/4.74 % (2506216)Peak memory usage: 116 MB % 28.50/4.74 % (2506216)Instructions burned: 7 (million) % 28.50/4.74 % (2506220)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2574663415:i=471:thf=on:kws=precedence:rtra=on_2971 on theBenchmark for (2971ds/471Mi) % 28.50/4.74 % (2506220)Refutation not found, incomplete strategy % 28.50/4.74 % (2506220)------------------------------ % 28.50/4.74 % (2506220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.50/4.74 % (2506220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.50/4.74 % (2506220)CaDiCaL version: 2.1.3 % 28.50/4.74 % (2506220)Termination reason: Refutation not found, incomplete strategy % 28.50/4.74 % (2506220)Time elapsed: 0.044 s % 28.50/4.74 % (2506220)Peak memory usage: 116 MB % 28.50/4.74 % (2506220)Instructions burned: 9 (million) % 28.50/4.74 % (2506227)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2311779386:i=375:kws=inv_arity_squared:rtra=on_2970 on theBenchmark for (2970ds/375Mi) % 28.50/4.74 % (2506227)Refutation not found, incomplete strategy % 28.50/4.74 % (2506227)------------------------------ % 28.50/4.74 % (2506227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.50/4.74 % (2506227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.50/4.74 % (2506227)CaDiCaL version: 2.1.3 % 28.50/4.74 % (2506227)Termination reason: Refutation not found, incomplete strategy % 28.50/4.74 % (2506227)Time elapsed: 0.024 s % 28.50/4.74 % (2506227)Peak memory usage: 115 MB % 28.50/4.74 % (2506227)Instructions burned: 7 (million) % 28.50/4.74 % (2506226)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=2598610497:avsq=on:i=276:avsqr=1,2:rtra=on_2970 on theBenchmark for (2970ds/276Mi) % 28.50/4.74 % (2506213)Instruction limit reached! % 28.50/4.74 % (2506213)------------------------------ % 28.50/4.74 % (2506213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.50/4.74 % (2506213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.50/4.74 % (2506213)CaDiCaL version: 2.1.3 % 28.50/4.74 % (2506213)Termination reason: Instruction limit % 28.50/4.74 % (2506213)Termination phase: Saturation % 28.50/4.74 % (2506213)Time elapsed: 0.298 s % 28.50/4.74 % (2506213)Peak memory usage: 115 MB % 28.50/4.74 % (2506213)Instructions burned: 321 (million) % 28.50/4.74 % (2506232)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=726748334:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi) % 28.50/4.74 % (2506210)Instruction limit reached! % 28.50/4.74 % (2506210)------------------------------ % 28.50/4.74 % (2506210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.50/4.74 % (2506210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.50/4.74 % (2506210)CaDiCaL version: 2.1.3 % 28.50/4.74 % (2506210)Termination reason: Instruction limit % 28.50/4.74 % (2506210)Termination phase: Saturation % 28.50/4.74 % (2506210)Time elapsed: 0.393 s % 28.50/4.74 % (2506210)Peak memory usage: 90 MB % 28.50/4.74 % (2506210)Instructions burned: 484 (million) % 28.50/4.74 % (2506227)------------------------------ % 28.50/4.74 % (2506227)------------------------------ % 28.50/4.74 % (2506216)------------------------------ % 28.50/4.74 % (2506216)------------------------------ % 28.50/4.74 % (2506226)Instruction limit reached! % 28.50/4.74 % (2506226)------------------------------ % 28.50/4.74 % (2506226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.50/4.74 % (2506226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.50/4.74 % (2506226)CaDiCaL version: 2.1.3 % 28.50/4.74 % (2506226)Termination reason: Instruction limit % 28.50/4.74 % (2506226)Termination phase: Saturation % 28.50/4.74 % (2506226)Time elapsed: 0.251 s % 28.50/4.74 % (2506226)Peak memory usage: 133 MB % 28.50/4.74 % (2506226)Instructions burned: 276 (million) % 28.50/4.74 % (2506237)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3466084426:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2967 on theBenchmark for (2967ds/513Mi) % 32.85/5.19 % (2506220)------------------------------ % 32.85/5.19 % (2506220)------------------------------ % 32.85/5.19 % (2506243)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=871427092:i=334:rtra=on_2966 on theBenchmark for (2966ds/334Mi) % 32.85/5.19 % (2506245)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=654857292:i=359:rtra=on:gtg=exists_top:ss=axioms_2966 on theBenchmark for (2966ds/359Mi) % 32.85/5.19 % (2506245)Refutation not found, incomplete strategy % 32.85/5.19 % (2506245)------------------------------ % 32.85/5.19 % (2506245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.85/5.19 % (2506245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.85/5.19 % (2506245)CaDiCaL version: 2.1.3 % 32.85/5.19 % (2506245)Termination reason: Refutation not found, incomplete strategy % 32.85/5.19 % (2506245)Time elapsed: 0.003 s % 32.85/5.19 % (2506245)Peak memory usage: 89 MB % 32.85/5.19 % (2506245)Instructions burned: 3 (million) % 32.85/5.19 % (2506243)Refutation not found, incomplete strategy % 32.85/5.19 % (2506243)------------------------------ % 32.85/5.19 % (2506243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.85/5.19 % (2506243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.85/5.19 % (2506243)CaDiCaL version: 2.1.3 % 32.85/5.19 % (2506243)Termination reason: Refutation not found, incomplete strategy % 32.85/5.19 % (2506243)Time elapsed: 0.076 s % 32.85/5.19 % (2506243)Peak memory usage: 132 MB % 32.85/5.19 % (2506243)Instructions burned: 12 (million) % 32.85/5.19 % (2506249)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1177659430:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/261Mi) % 32.85/5.19 % (2506248)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3073389000:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2965 on theBenchmark for (2965ds/341Mi) % 32.85/5.19 % (2506249)Refutation not found, incomplete strategy % 32.85/5.19 % (2506249)------------------------------ % 32.85/5.19 % (2506249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.85/5.19 % (2506249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.85/5.19 % (2506249)CaDiCaL version: 2.1.3 % 32.85/5.19 % (2506249)Termination reason: Refutation not found, incomplete strategy % 32.85/5.19 % (2506249)Time elapsed: 0.049 s % 32.85/5.19 % (2506249)Peak memory usage: 117 MB % 32.85/5.19 % (2506249)Instructions burned: 27 (million) % 32.85/5.19 % (2506248)Refutation not found, incomplete strategy % 32.85/5.19 % (2506248)------------------------------ % 32.85/5.19 % (2506248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.85/5.19 % (2506248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.85/5.19 % (2506248)CaDiCaL version: 2.1.3 % 32.85/5.19 % (2506248)Termination reason: Refutation not found, incomplete strategy % 32.85/5.19 % (2506248)Time elapsed: 0.038 s % 32.85/5.19 % (2506248)Peak memory usage: 113 MB % 32.85/5.19 % (2506248)Instructions burned: 6 (million) % 32.85/5.19 % (2506252)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=3936844488:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/235Mi) % 32.85/5.19 % (2506245)------------------------------ % 32.85/5.19 % (2506245)------------------------------ % 32.85/5.19 % (2506232)Instruction limit reached! % 32.85/5.19 % (2506232)------------------------------ % 32.85/5.19 % (2506232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.85/5.19 % (2506232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.85/5.19 % (2506232)CaDiCaL version: 2.1.3 % 32.85/5.19 % (2506232)Termination reason: Instruction limit % 32.85/5.19 % (2506232)Termination phase: Saturation % 32.85/5.19 % (2506232)Time elapsed: 0.480 s % 32.85/5.19 % (2506232)Peak memory usage: 120 MB % 32.85/5.19 % (2506232)Instructions burned: 389 (million) % 32.85/5.19 % (2506262)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3066335902:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 32.85/5.19 % (2506243)------------------------------ % 35.70/5.80 % (2506243)------------------------------ % 35.70/5.80 % (2506252)Instruction limit reached! % 35.70/5.80 % (2506252)------------------------------ % 35.70/5.80 % (2506252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.70/5.80 % (2506252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.70/5.80 % (2506252)CaDiCaL version: 2.1.3 % 35.70/5.80 % (2506252)Termination reason: Instruction limit % 35.70/5.80 % (2506252)Termination phase: Saturation % 35.70/5.80 % (2506252)Time elapsed: 0.206 s % 35.70/5.80 % (2506252)Peak memory usage: 116 MB % 35.70/5.80 % (2506252)Instructions burned: 235 (million) % 35.70/5.80 % (2506237)Instruction limit reached! % 35.70/5.80 % (2506237)------------------------------ % 35.70/5.80 % (2506237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.70/5.80 % (2506237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.70/5.80 % (2506237)CaDiCaL version: 2.1.3 % 35.70/5.80 % (2506237)Termination reason: Instruction limit % 35.70/5.80 % (2506237)Termination phase: Saturation % 35.70/5.80 % (2506237)Time elapsed: 0.487 s % 35.70/5.80 % (2506237)Peak memory usage: 93 MB % 35.70/5.80 % (2506237)Instructions burned: 513 (million) % 35.70/5.80 % (2506265)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1080368610:i=146:doe=on:rtra=on_2962 on theBenchmark for (2962ds/146Mi) % 35.70/5.80 % (2506262)Instruction limit reached! % 35.70/5.80 % (2506262)------------------------------ % 35.70/5.80 % (2506262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.70/5.80 % (2506262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.70/5.80 % (2506262)CaDiCaL version: 2.1.3 % 35.70/5.80 % (2506262)Termination reason: Instruction limit % 35.70/5.80 % (2506262)Termination phase: Saturation % 35.70/5.80 % (2506262)Time elapsed: 0.150 s % 35.70/5.80 % (2506262)Peak memory usage: 91 MB % 35.70/5.80 % (2506262)Instructions burned: 274 (million) % 35.70/5.80 % (2506249)------------------------------ % 35.70/5.80 % (2506249)------------------------------ % 35.70/5.80 % (2506248)------------------------------ % 35.70/5.80 % (2506248)------------------------------ % 35.70/5.80 % (2506265)Instruction limit reached! % 35.70/5.80 % (2506265)------------------------------ % 35.70/5.80 % (2506265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.70/5.80 % (2506265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.70/5.80 % (2506265)CaDiCaL version: 2.1.3 % 35.70/5.80 % (2506265)Termination reason: Instruction limit % 35.70/5.80 % (2506265)Termination phase: Saturation % 35.70/5.80 % (2506265)Time elapsed: 0.154 s % 35.70/5.80 % (2506265)Peak memory usage: 90 MB % 35.70/5.80 % (2506265)Instructions burned: 146 (million) % 35.70/5.80 % (2506272)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=1279350657:avsq=on:i=276:avsqr=1,2:rtra=on_2960 on theBenchmark for (2960ds/276Mi) % 35.70/5.80 % (2506271)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4291376722:i=4428:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/4428Mi) % 35.70/5.80 % (2506274)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2786291590:i=1052:rtra=on_2960 on theBenchmark for (2960ds/1052Mi) % 35.70/5.80 % (2506281)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2140200835:i=107:rtra=on_2958 on theBenchmark for (2958ds/107Mi) % 35.70/5.80 % (2506280)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=491794563:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2959 on theBenchmark for (2959ds/1054Mi) % 35.70/5.80 % (2506280)Refutation not found, incomplete strategy % 35.70/5.80 % (2506280)------------------------------ % 35.70/5.80 % (2506280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.70/5.80 % (2506280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.70/5.80 % (2506280)CaDiCaL version: 2.1.3 % 35.70/5.80 % (2506280)Termination reason: Refutation not found, incomplete strategy % 35.70/5.80 % (2506280)Time elapsed: 0.004 s % 35.70/5.80 % (2506280)Peak memory usage: 89 MB % 35.70/5.80 % (2506280)Instructions burned: 2 (million) % 35.70/5.80 % (2506281)Refutation not found, incomplete strategy % 35.70/5.80 % (2506281)------------------------------ % 35.70/5.80 % (2506281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.70/5.80 % (2506281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.59 % (2506281)CaDiCaL version: 2.1.3 % 42.19/6.59 % (2506281)Termination reason: Refutation not found, incomplete strategy % 42.19/6.59 % (2506281)Time elapsed: 0.022 s % 42.19/6.59 % (2506281)Peak memory usage: 116 MB % 42.19/6.59 % (2506281)Instructions burned: 8 (million) % 42.19/6.59 % (2506279)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1051473341:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2959 on theBenchmark for (2959ds/655Mi) % 42.19/6.59 % (2506282)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1963844461:s2a=on:i=450:doe=on:nm=32:rtra=on_2958 on theBenchmark for (2958ds/450Mi) % 42.19/6.59 % (2506279)Refutation not found, incomplete strategy % 42.19/6.59 % (2506279)------------------------------ % 42.19/6.59 % (2506279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.19/6.59 % (2506279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.59 % (2506279)CaDiCaL version: 2.1.3 % 42.19/6.59 % (2506279)Termination reason: Refutation not found, incomplete strategy % 42.19/6.59 % (2506279)Time elapsed: 0.006 s % 42.19/6.59 % (2506279)Peak memory usage: 89 MB % 42.19/6.59 % (2506279)Instructions burned: 4 (million) % 42.19/6.59 % (2506282)Refutation not found, incomplete strategy % 42.19/6.59 % (2506282)------------------------------ % 42.19/6.59 % (2506282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.19/6.59 % (2506282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.59 % (2506282)CaDiCaL version: 2.1.3 % 42.19/6.59 % (2506282)Termination reason: Refutation not found, incomplete strategy % 42.19/6.59 % (2506282)Time elapsed: 0.068 s % 42.19/6.59 % (2506282)Peak memory usage: 132 MB % 42.19/6.59 % (2506282)Instructions burned: 12 (million) % 42.19/6.59 % (2506272)Instruction limit reached! % 42.19/6.59 % (2506272)------------------------------ % 42.19/6.59 % (2506272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.19/6.59 % (2506272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.59 % (2506272)CaDiCaL version: 2.1.3 % 42.19/6.59 % (2506272)Termination reason: Instruction limit % 42.19/6.59 % (2506272)Termination phase: Saturation % 42.19/6.59 % (2506272)Time elapsed: 0.248 s % 42.19/6.59 % (2506272)Peak memory usage: 133 MB % 42.19/6.59 % (2506272)Instructions burned: 276 (million) % 42.19/6.59 % (2506281)------------------------------ % 42.19/6.59 % (2506281)------------------------------ % 42.19/6.59 % (2506280)------------------------------ % 42.19/6.59 % (2506280)------------------------------ % 42.19/6.59 % (2506279)------------------------------ % 42.19/6.59 % (2506279)------------------------------ % 42.19/6.59 % (2506296)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 42.19/6.59 % (2506296)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1302934930:i=1090:aac=none:nm=0:rtra=on:rawr=on_2955 on theBenchmark for (2955ds/1090Mi) % 42.19/6.59 % (2506299)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2659467054:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2955 on theBenchmark for (2955ds/130Mi) % 42.19/6.59 % (2506296)Refutation not found, incomplete strategy % 42.19/6.59 % (2506296)------------------------------ % 42.19/6.59 % (2506296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.19/6.59 % (2506296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.59 % (2506296)CaDiCaL version: 2.1.3 % 42.19/6.59 % (2506296)Termination reason: Refutation not found, incomplete strategy % 42.19/6.59 % (2506296)Time elapsed: 0.041 s % 42.19/6.59 % (2506296)Peak memory usage: 116 MB % 42.19/6.59 % (2506296)Instructions burned: 7 (million) % 42.19/6.59 % (2506299)Refutation not found, incomplete strategy % 42.19/6.59 % (2506299)------------------------------ % 42.19/6.59 % (2506299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.19/6.59 % (2506299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.19/6.59 % (2506299)CaDiCaL version: 2.1.3 % 42.19/6.59 % (2506299)Termination reason: Refutation not found, incomplete strategy % 42.19/6.59 % (2506299)Time elapsed: 0.065 s % 42.19/6.59 % (2506299)Peak memory usage: 117 MB % 42.19/6.59 % (2506299)Instructions burned: 34 (million) % 45.47/7.18 % (2506282)------------------------------ % 45.47/7.18 % (2506282)------------------------------ % 45.47/7.18 % (2506303)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=464947912:i=312:kws=inv_frequency:nm=20:rtra=on_2954 on theBenchmark for (2954ds/312Mi) % 45.47/7.18 % (2506306)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=911337155:i=491:doe=on:rtra=on:gtg=position_2953 on theBenchmark for (2953ds/491Mi) % 45.47/7.18 % (2506306)Refutation not found, incomplete strategy % 45.47/7.18 % (2506306)------------------------------ % 45.47/7.18 % (2506306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.18 % (2506306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.18 % (2506306)CaDiCaL version: 2.1.3 % 45.47/7.18 % (2506306)Termination reason: Refutation not found, incomplete strategy % 45.47/7.18 % (2506306)Time elapsed: 0.004 s % 45.47/7.18 % (2506306)Peak memory usage: 89 MB % 45.47/7.18 % (2506306)Instructions burned: 2 (million) % 45.47/7.18 % (2506274)Instruction limit reached! % 45.47/7.18 % (2506274)------------------------------ % 45.47/7.18 % (2506274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.18 % (2506274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.18 % (2506274)CaDiCaL version: 2.1.3 % 45.47/7.18 % (2506274)Termination reason: Instruction limit % 45.47/7.18 % (2506274)Termination phase: Saturation % 45.47/7.18 % (2506274)Time elapsed: 0.691 s % 45.47/7.18 % (2506274)Peak memory usage: 89 MB % 45.47/7.18 % (2506274)Instructions burned: 1053 (million) % 45.47/7.18 % (2506311)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2071769274:s2a=on:i=835:s2at=2:rtra=on_2952 on theBenchmark for (2952ds/835Mi) % 45.47/7.18 % (2506296)------------------------------ % 45.47/7.18 % (2506296)------------------------------ % 45.47/7.18 % (2506299)------------------------------ % 45.47/7.18 % (2506299)------------------------------ % 45.47/7.18 % (2506316)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=630542044:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2951 on theBenchmark for (2951ds/307Mi) % 45.47/7.18 % (2506316)Refutation not found, incomplete strategy % 45.47/7.18 % (2506316)------------------------------ % 45.47/7.18 % (2506316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.18 % (2506316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.18 % (2506316)CaDiCaL version: 2.1.3 % 45.47/7.18 % (2506316)Termination reason: Refutation not found, incomplete strategy % 45.47/7.18 % (2506316)Time elapsed: 0.006 s % 45.47/7.18 % (2506316)Peak memory usage: 89 MB % 45.47/7.18 % (2506316)Instructions burned: 5 (million) % 45.47/7.18 % (2506303)Instruction limit reached! % 45.47/7.18 % (2506303)------------------------------ % 45.47/7.18 % (2506303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.18 % (2506303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.18 % (2506303)CaDiCaL version: 2.1.3 % 45.47/7.18 % (2506303)Termination reason: Instruction limit % 45.47/7.18 % (2506303)Termination phase: Saturation % 45.47/7.18 % (2506303)Time elapsed: 0.332 s % 45.47/7.18 % (2506303)Peak memory usage: 119 MB % 45.47/7.18 % (2506303)Instructions burned: 312 (million) % 45.47/7.18 % (2506306)------------------------------ % 45.47/7.18 % (2506306)------------------------------ % 45.47/7.18 % (2506325)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=359482027:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2949 on theBenchmark for (2949ds/646Mi) % 45.47/7.18 % (2506323)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2795007272:i=776:doe=on:rtra=on_2949 on theBenchmark for (2949ds/776Mi) % 45.47/7.18 % (2506325)Refutation not found, incomplete strategy % 45.47/7.18 % (2506325)------------------------------ % 45.47/7.18 % (2506325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.18 % (2506325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.18 % (2506325)CaDiCaL version: 2.1.3 % 45.47/7.18 % (2506325)Termination reason: Refutation not found, incomplete strategy % 45.47/7.18 % (2506325)Time elapsed: 0.069 s % 45.47/7.18 % (2506325)Peak memory usage: 133 MB % 45.47/7.18 % (2506325)Instructions burned: 13 (million) % 45.47/7.18 % (2506311)Instruction limit reached! % 45.47/7.18 % (2506311)------------------------------ % 45.47/7.18 % (2506311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.26/8.09 % (2506311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.26/8.09 % (2506311)CaDiCaL version: 2.1.3 % 53.26/8.09 % (2506311)Termination reason: Instruction limit % 53.26/8.09 % (2506311)Termination phase: Saturation % 53.26/8.09 % (2506311)Time elapsed: 0.415 s % 53.26/8.09 % (2506311)Peak memory usage: 94 MB % 53.26/8.09 % (2506311)Instructions burned: 836 (million) % 53.26/8.09 % (2506329)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=447360889:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2948 on theBenchmark for (2948ds/784Mi) % 53.26/8.09 % (2506316)------------------------------ % 53.26/8.09 % (2506316)------------------------------ % 53.26/8.09 % (2506334)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=2420853016:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2947 on theBenchmark for (2947ds/1131Mi) % 53.26/8.09 % (2506337)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=3875115035:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2946 on theBenchmark for (2946ds/246Mi) % 53.26/8.09 % (2506337)Instruction limit reached! % 53.26/8.09 % (2506337)------------------------------ % 53.26/8.09 % (2506337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.26/8.09 % (2506337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.26/8.09 % (2506337)CaDiCaL version: 2.1.3 % 53.26/8.09 % (2506337)Termination reason: Instruction limit % 53.26/8.09 % (2506337)Termination phase: Saturation % 53.26/8.09 % (2506337)Time elapsed: 0.132 s % 53.26/8.09 % (2506337)Peak memory usage: 116 MB % 53.26/8.09 % (2506337)Instructions burned: 247 (million) % 53.26/8.09 % (2506340)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=459150437:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2945 on theBenchmark for (2945ds/775Mi) % 53.26/8.09 % (2506325)------------------------------ % 53.26/8.09 % (2506325)------------------------------ % 53.26/8.09 % (2506345)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3438391556:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2943 on theBenchmark for (2943ds/273Mi) % 53.26/8.09 % (2506323)Instruction limit reached! % 53.26/8.09 % (2506323)------------------------------ % 53.26/8.09 % (2506323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.26/8.09 % (2506323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.26/8.09 % (2506323)CaDiCaL version: 2.1.3 % 53.26/8.09 % (2506323)Termination reason: Instruction limit % 53.26/8.09 % (2506323)Termination phase: Saturation % 53.26/8.09 % (2506323)Time elapsed: 0.645 s % 53.26/8.09 % (2506323)Peak memory usage: 121 MB % 53.26/8.09 % (2506323)Instructions burned: 776 (million) % 53.26/8.09 % (2506349)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1397765270:i=102:nm=16:rtra=on_2942 on theBenchmark for (2942ds/102Mi) % 53.26/8.09 % (2506345)Instruction limit reached! % 53.26/8.09 % (2506345)------------------------------ % 53.26/8.09 % (2506345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.26/8.09 % (2506345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.26/8.09 % (2506345)CaDiCaL version: 2.1.3 % 53.26/8.09 % (2506345)Termination reason: Instruction limit % 53.26/8.09 % (2506345)Termination phase: Saturation % 53.26/8.09 % (2506345)Time elapsed: 0.156 s % 53.26/8.09 % (2506345)Peak memory usage: 92 MB % 53.26/8.09 % (2506345)Instructions burned: 273 (million) % 53.26/8.09 % (2506349)Instruction limit reached! % 53.26/8.09 % (2506349)------------------------------ % 53.26/8.09 % (2506349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.26/8.09 % (2506349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.26/8.09 % (2506349)CaDiCaL version: 2.1.3 % 53.26/8.09 % (2506349)Termination reason: Instruction limit % 53.26/8.09 % (2506349)Termination phase: Saturation % 53.26/8.09 % (2506349)Time elapsed: 0.079 s % 53.26/8.09 % (2506349)Peak memory usage: 88 MB % 53.26/8.09 % (2506349)Instructions burned: 103 (million) % 53.26/8.09 % (2506356)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3001775036:i=6400:doe=on:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/6400Mi) % 63.58/9.59 % (2506353)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=4139534243:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2940 on theBenchmark for (2940ds/1094Mi) % 63.58/9.59 % (2506353)Refutation not found, incomplete strategy % 63.58/9.59 % (2506353)------------------------------ % 63.58/9.59 % (2506353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.59 % (2506353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.59 % (2506353)CaDiCaL version: 2.1.3 % 63.58/9.59 % (2506353)Termination reason: Refutation not found, incomplete strategy % 63.58/9.59 % (2506353)Time elapsed: 0.002 s % 63.58/9.59 % (2506353)Peak memory usage: 88 MB % 63.58/9.59 % (2506329)Instruction limit reached! % 63.58/9.59 % (2506329)------------------------------ % 63.58/9.59 % (2506329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.59 % (2506329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.59 % (2506329)CaDiCaL version: 2.1.3 % 63.58/9.59 % (2506329)Termination reason: Instruction limit % 63.58/9.59 % (2506329)Termination phase: Saturation % 63.58/9.59 % (2506329)Time elapsed: 0.832 s % 63.58/9.59 % (2506329)Peak memory usage: 122 MB % 63.58/9.59 % (2506329)Instructions burned: 784 (million) % 63.58/9.59 % (2506360)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=1109493397:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2939 on theBenchmark for (2939ds/868Mi) % 63.58/9.59 % (2506360)Refutation not found, incomplete strategy % 63.58/9.59 % (2506360)------------------------------ % 63.58/9.59 % (2506360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.59 % (2506360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.59 % (2506360)CaDiCaL version: 2.1.3 % 63.58/9.59 % (2506360)Termination reason: Refutation not found, incomplete strategy % 63.58/9.59 % (2506360)Time elapsed: 0.098 s % 63.58/9.59 % (2506360)Peak memory usage: 118 MB % 63.58/9.59 % (2506360)Instructions burned: 58 (million) % 63.58/9.59 % (2506364)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=2418834313:i=1846:canc=cautious:fsr=off:rtra=on_2937 on theBenchmark for (2937ds/1846Mi) % 63.58/9.59 % (2506340)Instruction limit reached! % 63.58/9.59 % (2506340)------------------------------ % 63.58/9.59 % (2506340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.59 % (2506340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.59 % (2506340)CaDiCaL version: 2.1.3 % 63.58/9.59 % (2506340)Termination reason: Instruction limit % 63.58/9.59 % (2506340)Termination phase: Saturation % 63.58/9.59 % (2506340)Time elapsed: 0.792 s % 63.58/9.59 % (2506340)Peak memory usage: 95 MB % 63.58/9.59 % (2506340)Instructions burned: 775 (million) % 63.58/9.59 % (2506353)------------------------------ % 63.58/9.59 % (2506353)------------------------------ % 63.58/9.59 % (2506334)Instruction limit reached! % 63.58/9.59 % (2506334)------------------------------ % 63.58/9.59 % (2506334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.59 % (2506334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.59 % (2506334)CaDiCaL version: 2.1.3 % 63.58/9.59 % (2506334)Termination reason: Instruction limit % 63.58/9.59 % (2506334)Termination phase: Saturation % 63.58/9.59 % (2506334)Time elapsed: 1.173 s % 63.58/9.59 % (2506334)Peak memory usage: 125 MB % 63.58/9.59 % (2506334)Instructions burned: 1131 (million) % 63.58/9.59 % (2506373)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1858931161:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi) % 63.58/9.59 % (2506372)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1252612440:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2935 on theBenchmark for (2935ds/36816Mi) % 63.58/9.59 % (2506372)Refutation not found, incomplete strategy % 63.58/9.59 % (2506372)------------------------------ % 63.58/9.59 % (2506372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.59 % (2506372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.59 % (2506372)CaDiCaL version: 2.1.3 % 63.58/9.59 % (2506360)------------------------------ % 63.58/9.59 % (2506360)------------------------------ % 63.58/9.59 % (2506372)Termination reason: Refutation not found, incomplete strategy % 78.96/11.86 % (2506372)Time elapsed: 0.002 s % 78.96/11.86 % (2506372)Peak memory usage: 88 MB % 78.96/11.86 % (2506372)Instructions burned: 1 (million) % 78.96/11.86 % (2506376)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=2467530629:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2933 on theBenchmark for (2933ds/863Mi) % 78.96/11.86 % (2506373)Instruction limit reached! % 78.96/11.86 % (2506373)------------------------------ % 78.96/11.86 % (2506373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.96/11.86 % (2506373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.96/11.86 % (2506373)CaDiCaL version: 2.1.3 % 78.96/11.86 % (2506373)Termination reason: Instruction limit % 78.96/11.86 % (2506373)Termination phase: Saturation % 78.96/11.86 % (2506373)Time elapsed: 0.217 s % 78.96/11.86 % (2506373)Peak memory usage: 91 MB % 78.96/11.86 % (2506373)Instructions burned: 274 (million) % 78.96/11.86 % (2506379)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=294818469:i=5811:kws=precedence:nm=0:rtra=on_2932 on theBenchmark for (2932ds/5811Mi) % 78.96/11.86 % (2506376)Refutation not found, incomplete strategy % 78.96/11.86 % (2506376)------------------------------ % 78.96/11.86 % (2506376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.96/11.86 % (2506376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.96/11.86 % (2506376)CaDiCaL version: 2.1.3 % 78.96/11.86 % (2506376)Termination reason: Refutation not found, incomplete strategy % 78.96/11.86 % (2506376)Time elapsed: 0.094 s % 78.96/11.86 % (2506376)Peak memory usage: 117 MB % 78.96/11.86 % (2506376)Instructions burned: 54 (million) % 78.96/11.86 % (2506379)Refutation not found, incomplete strategy % 78.96/11.86 % (2506379)------------------------------ % 78.96/11.86 % (2506379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.96/11.86 % (2506379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.96/11.86 % (2506379)CaDiCaL version: 2.1.3 % 78.96/11.86 % (2506379)Termination reason: Refutation not found, incomplete strategy % 78.96/11.86 % (2506379)Time elapsed: 0.078 s % 78.96/11.86 % (2506379)Peak memory usage: 117 MB % 78.96/11.86 % (2506379)Instructions burned: 50 (million) % 78.96/11.86 % (2506372)------------------------------ % 78.96/11.86 % (2506372)------------------------------ % 78.96/11.86 % (2506383)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=3348748531:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2931 on theBenchmark for (2931ds/2216Mi) % 78.96/11.86 % (2506376)------------------------------ % 78.96/11.86 % (2506376)------------------------------ % 78.96/11.86 % (2506388)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2104784233:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/801Mi) % 78.96/11.86 % (2506388)Refutation not found, incomplete strategy % 78.96/11.86 % (2506388)------------------------------ % 78.96/11.86 % (2506388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.96/11.86 % (2506388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.96/11.86 % (2506388)CaDiCaL version: 2.1.3 % 78.96/11.86 % (2506388)Termination reason: Refutation not found, incomplete strategy % 78.96/11.86 % (2506388)Time elapsed: 0.007 s % 78.96/11.86 % (2506388)Peak memory usage: 89 MB % 78.96/11.86 % (2506388)Instructions burned: 5 (million) % 78.96/11.86 % (2506379)------------------------------ % 78.96/11.86 % (2506379)------------------------------ % 78.96/11.86 % (2506394)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1240462638:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2926 on theBenchmark for (2926ds/1026Mi) % 78.96/11.86 % (2506394)Refutation not found, incomplete strategy % 78.96/11.86 % (2506394)------------------------------ % 78.96/11.86 % (2506394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.96/11.86 % (2506394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.96/11.86 % (2506394)CaDiCaL version: 2.1.3 % 78.96/11.86 % (2506394)Termination reason: Refutation not found, incomplete strategy % 78.96/11.86 % (2506394)Time elapsed: 0.004 s % 78.96/11.86 % (2506394)Peak memory usage: 89 MB % 78.96/11.86 % (2506394)Instructions burned: 2 (million) % 78.96/11.86 % (2506397)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2807987774:i=3509:rtra=on_2925 on theBenchmark for (2925ds/3509Mi) % 117.19/17.07 % (2506364)Instruction limit reached! % 117.19/17.07 % (2506364)------------------------------ % 117.19/17.07 % (2506364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.19/17.07 % (2506364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.19/17.07 % (2506364)CaDiCaL version: 2.1.3 % 117.19/17.07 % (2506364)Termination reason: Instruction limit % 117.19/17.07 % (2506364)Termination phase: Saturation % 117.19/17.07 % (2506364)Time elapsed: 1.264 s % 117.19/17.07 % (2506364)Peak memory usage: 99 MB % 117.19/17.07 % (2506364)Instructions burned: 1846 (million) % 117.19/17.07 % (2506388)------------------------------ % 117.19/17.07 % (2506388)------------------------------ % 117.19/17.07 % (2506271)Instruction limit reached! % 117.19/17.07 % (2506271)------------------------------ % 117.19/17.07 % (2506271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.19/17.07 % (2506271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.19/17.07 % (2506271)CaDiCaL version: 2.1.3 % 117.19/17.07 % (2506271)Termination reason: Instruction limit % 117.19/17.07 % (2506271)Termination phase: Saturation % 117.19/17.07 % (2506271)Time elapsed: 3.603 s % 117.19/17.07 % (2506271)Peak memory usage: 104 MB % 117.19/17.07 % (2506271)Instructions burned: 4428 (million) % 117.19/17.07 % (2506407)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=699143537:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2923 on theBenchmark for (2923ds/2127Mi) % 117.19/17.07 % (2506409)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2700286351:i=1959:rtra=on:fsd=on:proc=on_2922 on theBenchmark for (2922ds/1959Mi) % 117.19/17.07 % (2506394)------------------------------ % 117.19/17.07 % (2506394)------------------------------ % 117.19/17.07 % (2506410)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2062919925:s2a=on:i=3553:nm=0:rtra=on_2922 on theBenchmark for (2922ds/3553Mi) % 117.19/17.07 % (2506409)Refutation not found, incomplete strategy % 117.19/17.07 % (2506409)------------------------------ % 117.19/17.07 % (2506409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.19/17.07 % (2506409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.19/17.07 % (2506409)CaDiCaL version: 2.1.3 % 117.19/17.07 % (2506409)Termination reason: Refutation not found, incomplete strategy % 117.19/17.07 % (2506409)Time elapsed: 0.041 s % 117.19/17.07 % (2506409)Peak memory usage: 116 MB % 117.19/17.07 % (2506409)Instructions burned: 7 (million) % 117.19/17.07 % (2506416)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1303047442:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2920 on theBenchmark for (2920ds/3201Mi) % 117.19/17.07 % (2506409)------------------------------ % 117.19/17.07 % (2506409)------------------------------ % 117.19/17.07 % (2506424)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=4259495728:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2916 on theBenchmark for (2916ds/4093Mi) % 117.19/17.07 % (2506356)Instruction limit reached! % 117.19/17.07 % (2506356)------------------------------ % 117.19/17.07 % (2506356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.19/17.07 % (2506356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.19/17.07 % (2506356)CaDiCaL version: 2.1.3 % 117.19/17.07 % (2506356)Termination reason: Instruction limit % 117.19/17.07 % (2506356)Termination phase: Saturation % 117.19/17.07 % (2506356)Time elapsed: 2.844 s % 117.19/17.07 % (2506356)Peak memory usage: 111 MB % 117.19/17.07 % (2506356)Instructions burned: 6402 (million) % 117.19/17.07 % (2506383)Instruction limit reached! % 117.19/17.07 % (2506383)------------------------------ % 117.19/17.07 % (2506383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.19/17.07 % (2506383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.19/17.07 % (2506383)CaDiCaL version: 2.1.3 % 117.19/17.07 % (2506383)Termination reason: Instruction limit % 117.19/17.07 % (2506383)Termination phase: Saturation % 117.19/17.07 % (2506383)Time elapsed: 1.941 s % 117.19/17.07 % (2506383)Peak memory usage: 130 MB % 117.19/17.07 % (2506383)Instructions burned: 2217 (million) % 117.19/17.07 % (2506433)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=1171569281:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2910 on theBenchmark for (2910ds/21173Mi) % 141.37/20.51 % (2506435)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=370931395:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2909 on theBenchmark for (2909ds/10544Mi) % 141.37/20.51 % (2506416)Refutation not found, incomplete strategy % 141.37/20.51 % (2506416)------------------------------ % 141.37/20.51 % (2506416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.37/20.51 % (2506416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.37/20.51 % (2506416)CaDiCaL version: 2.1.3 % 141.37/20.51 % (2506416)Termination reason: Refutation not found, incomplete strategy % 141.37/20.51 % (2506416)Time elapsed: 1.288 s % 141.37/20.51 % (2506416)Peak memory usage: 94 MB % 141.37/20.51 % (2506416)Instructions burned: 1732 (million) % 141.37/20.51 % (2506407)Instruction limit reached! % 141.37/20.51 % (2506407)------------------------------ % 141.37/20.51 % (2506407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.37/20.51 % (2506407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.37/20.51 % (2506407)CaDiCaL version: 2.1.3 % 141.37/20.51 % (2506407)Termination reason: Instruction limit % 141.37/20.51 % (2506407)Termination phase: Saturation % 141.37/20.51 % (2506407)Time elapsed: 1.679 s % 141.37/20.51 % (2506407)Peak memory usage: 101 MB % 141.37/20.51 % (2506407)Instructions burned: 2128 (million) % 141.37/20.51 % (2506444)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2250277778:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2904 on theBenchmark for (2904ds/1262Mi) % 141.37/20.51 % (2506444)Refutation not found, incomplete strategy % 141.37/20.51 % (2506444)------------------------------ % 141.37/20.51 % (2506444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.37/20.51 % (2506444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.37/20.51 % (2506444)CaDiCaL version: 2.1.3 % 141.37/20.51 % (2506444)Termination reason: Refutation not found, incomplete strategy % 141.37/20.51 % (2506444)Time elapsed: 0.041 s % 141.37/20.51 % (2506444)Peak memory usage: 116 MB % 141.37/20.51 % (2506444)Instructions burned: 7 (million) % 141.37/20.51 % (2506416)------------------------------ % 141.37/20.51 % (2506416)------------------------------ % 141.37/20.51 % (2506447)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1914234199:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2901 on theBenchmark for (2901ds/775Mi) % 141.37/20.51 % (2506444)------------------------------ % 141.37/20.51 % (2506444)------------------------------ % 141.37/20.51 % (2506450)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3184971259:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2898 on theBenchmark for (2898ds/270Mi) % 141.37/20.51 % (2506450)Instruction limit reached! % 141.37/20.51 % (2506450)------------------------------ % 141.37/20.51 % (2506450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.37/20.51 % (2506450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.37/20.51 % (2506450)CaDiCaL version: 2.1.3 % 141.37/20.51 % (2506450)Termination reason: Instruction limit % 141.37/20.51 % (2506450)Termination phase: Saturation % 141.37/20.51 % (2506450)Time elapsed: 0.264 s % 141.37/20.51 % (2506450)Peak memory usage: 92 MB % 141.37/20.51 % (2506450)Instructions burned: 271 (million) % 141.37/20.51 % (2506456)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=410492938:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2893 on theBenchmark for (2893ds/17165Mi) % 141.37/20.51 % (2506447)Instruction limit reached! % 141.37/20.51 % (2506447)------------------------------ % 141.37/20.51 % (2506447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.37/20.51 % (2506447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.37/20.51 % (2506447)CaDiCaL version: 2.1.3 % 141.37/20.51 % (2506447)Termination reason: Instruction limit % 141.37/20.51 % (2506447)Termination phase: Saturation % 141.37/20.51 % (2506447)Time elapsed: 0.829 s % 141.37/20.51 % (2506447)Peak memory usage: 96 MB % 141.37/20.51 % (2506447)Instructions burned: 776 (million) % 141.37/20.51 % (2506460)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3661998746:s2a=on:i=13094:s2at=-1:rtra=on_2890 on theBenchmark for (2890ds/13094Mi) % 141.37/20.51 % (2506397)Instruction limit reached! % 141.37/20.51 % (2506397)------------------------------ % 160.54/23.19 % (2506397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.54/23.19 % (2506397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.54/23.19 % (2506397)CaDiCaL version: 2.1.3 % 160.54/23.19 % (2506397)Termination reason: Instruction limit % 160.54/23.19 % (2506397)Termination phase: Saturation % 160.54/23.19 % (2506397)Time elapsed: 3.770 s % 160.54/23.19 % (2506397)Peak memory usage: 105 MB % 160.54/23.19 % (2506397)Instructions burned: 3509 (million) % 160.54/23.19 % (2506465)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=813917623:st=2:i=12633:rtra=on:ss=axioms_2886 on theBenchmark for (2886ds/12633Mi) % 160.54/23.19 % (2506410)Instruction limit reached! % 160.54/23.19 % (2506410)------------------------------ % 160.54/23.19 % (2506410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.54/23.19 % (2506410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.54/23.19 % (2506410)CaDiCaL version: 2.1.3 % 160.54/23.19 % (2506410)Termination reason: Instruction limit % 160.54/23.19 % (2506410)Termination phase: Saturation % 160.54/23.19 % (2506410)Time elapsed: 4.018 s % 160.54/23.19 % (2506410)Peak memory usage: 104 MB % 160.54/23.19 % (2506410)Instructions burned: 3553 (million) % 160.54/23.19 % (2506471)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2799857636:i=1783:rtra=on:gtg=position_2880 on theBenchmark for (2880ds/1783Mi) % 160.54/23.19 % (2506424)Instruction limit reached! % 160.54/23.19 % (2506424)------------------------------ % 160.54/23.19 % (2506424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.54/23.19 % (2506424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.54/23.19 % (2506424)CaDiCaL version: 2.1.3 % 160.54/23.19 % (2506424)Termination reason: Instruction limit % 160.54/23.19 % (2506424)Termination phase: Saturation % 160.54/23.19 % (2506424)Time elapsed: 4.230 s % 160.54/23.19 % (2506424)Peak memory usage: 165 MB % 160.54/23.19 % (2506424)Instructions burned: 4093 (million) % 160.54/23.19 % (2506478)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=171570899:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2871 on theBenchmark for (2871ds/5451Mi) % 160.54/23.19 % (2506471)Instruction limit reached! % 160.54/23.19 % (2506471)------------------------------ % 160.54/23.19 % (2506471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.54/23.19 % (2506471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.54/23.19 % (2506471)CaDiCaL version: 2.1.3 % 160.54/23.19 % (2506471)Termination reason: Instruction limit % 160.54/23.19 % (2506471)Termination phase: Saturation % 160.54/23.19 % (2506471)Time elapsed: 1.694 s % 160.54/23.19 % (2506471)Peak memory usage: 123 MB % 160.54/23.19 % (2506471)Instructions burned: 1783 (million) % 160.54/23.19 % (2506483)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=932528135:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2861 on theBenchmark for (2861ds/4975Mi) % 160.54/23.19 % (2506483)Refutation not found, incomplete strategy % 160.54/23.19 % (2506483)------------------------------ % 160.54/23.19 % (2506483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.54/23.19 % (2506483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.54/23.19 % (2506483)CaDiCaL version: 2.1.3 % 160.54/23.19 % (2506483)Termination reason: Refutation not found, incomplete strategy % 160.54/23.19 % (2506483)Time elapsed: 0.099 s % 160.54/23.19 % (2506483)Peak memory usage: 117 MB % 160.54/23.19 % (2506483)Instructions burned: 58 (million) % 160.54/23.19 % (2506483)------------------------------ % 160.54/23.19 % (2506483)------------------------------ % 160.54/23.19 % (2506486)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=1378214785:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2854 on theBenchmark for (2854ds/2076Mi) % 160.54/23.19 % (2506486)Instruction limit reached! % 160.54/23.19 % (2506486)------------------------------ % 160.54/23.19 % (2506486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.54/23.19 % (2506486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.54/23.19 % (2506486)CaDiCaL version: 2.1.3 % 160.54/23.19 % (2506486)Termination reason: Instruction limit % 160.54/23.19 % (2506486)Termination phase: Saturation % 160.54/23.19 % (2506486)Time elapsed: 1.818 s % 160.54/23.19 % (2506486)Peak memory usage: 129 MB % 187.30/27.06 % (2506486)Instructions burned: 2077 (million) % 187.30/27.06 % (2506492)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=169603827:i=5145:rtra=on_2833 on theBenchmark for (2833ds/5145Mi) % 187.30/27.06 % (2506433)Instruction limit reached! % 187.30/27.06 % (2506433)------------------------------ % 187.30/27.06 % (2506433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.30/27.06 % (2506433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.30/27.06 % (2506433)CaDiCaL version: 2.1.3 % 187.30/27.06 % (2506433)Termination reason: Instruction limit % 187.30/27.06 % (2506433)Termination phase: Saturation % 187.30/27.06 % (2506433)Time elapsed: 8.445 s % 187.30/27.06 % (2506433)Peak memory usage: 136 MB % 187.30/27.06 % (2506433)Instructions burned: 21175 (million) % 187.30/27.06 % (2506496)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3205071654:i=3509:rtra=on_2824 on theBenchmark for (2824ds/3509Mi) % 187.30/27.06 % (2506478)Instruction limit reached! % 187.30/27.06 % (2506478)------------------------------ % 187.30/27.06 % (2506478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.30/27.06 % (2506478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.30/27.06 % (2506478)CaDiCaL version: 2.1.3 % 187.30/27.06 % (2506478)Termination reason: Instruction limit % 187.30/27.06 % (2506478)Termination phase: Saturation % 187.30/27.06 % (2506478)Time elapsed: 5.145 s % 187.30/27.06 % (2506478)Peak memory usage: 133 MB % 187.30/27.06 % (2506478)Instructions burned: 5451 (million) % 187.30/27.06 % (2506500)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1062302594:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2818 on theBenchmark for (2818ds/13800Mi) % 187.30/27.06 % (2506460)Instruction limit reached! % 187.30/27.06 % (2506460)------------------------------ % 187.30/27.06 % (2506460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.30/27.06 % (2506460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.30/27.06 % (2506460)CaDiCaL version: 2.1.3 % 187.30/27.06 % (2506460)Termination reason: Instruction limit % 187.30/27.06 % (2506460)Termination phase: Saturation % 187.30/27.06 % (2506460)Time elapsed: 7.994 s % 187.30/27.06 % (2506460)Peak memory usage: 91 MB % 187.30/27.06 % (2506460)Instructions burned: 13094 (million) % 187.30/27.06 % (2506504)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1664226034:i=1412:rtra=on:fsd=on:proc=on_2808 on theBenchmark for (2808ds/1412Mi) % 187.30/27.06 % (2506504)Refutation not found, incomplete strategy % 187.30/27.06 % (2506504)------------------------------ % 187.30/27.06 % (2506504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.30/27.06 % (2506504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.30/27.06 % (2506504)CaDiCaL version: 2.1.3 % 187.30/27.06 % (2506504)Termination reason: Refutation not found, incomplete strategy % 187.30/27.06 % (2506504)Time elapsed: 0.042 s % 187.30/27.06 % (2506504)Peak memory usage: 116 MB % 187.30/27.06 % (2506504)Instructions burned: 7 (million) % 187.30/27.06 % (2506504)------------------------------ % 187.30/27.06 % (2506504)------------------------------ % 187.30/27.06 % (2506496)Instruction limit reached! % 187.30/27.06 % (2506496)------------------------------ % 187.30/27.06 % (2506496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.30/27.06 % (2506496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.30/27.06 % (2506496)CaDiCaL version: 2.1.3 % 187.30/27.06 % (2506496)Termination reason: Instruction limit % 187.30/27.06 % (2506496)Termination phase: Saturation % 187.30/27.06 % (2506496)Time elapsed: 2.066 s % 187.30/27.06 % (2506496)Peak memory usage: 106 MB % 187.30/27.06 % (2506496)Instructions burned: 3509 (million) % 187.30/27.06 % (2506510)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 % 187.30/27.06 % (2506510)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3117500248:i=11747:aac=none:nm=0:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/11747Mi) % 187.30/27.06 % (2506511)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3985353748:s2a=on:i=3553:nm=0:rtra=on_2801 on theBenchmark for (2801ds/3553Mi) % 187.30/27.06 % (2506510)Refutation not found, incomplete strategy % 187.30/27.06 % (2506510)------------------------------ % 187.30/27.06 % (2506510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.19 % (2506510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.19 % (2506510)CaDiCaL version: 2.1.3 % 224.57/32.19 % (2506510)Termination reason: Refutation not found, incomplete strategy % 224.57/32.19 % (2506510)Time elapsed: 0.042 s % 224.57/32.19 % (2506510)Peak memory usage: 116 MB % 224.57/32.19 % (2506510)Instructions burned: 7 (million) % 224.57/32.19 % (2506435)Instruction limit reached! % 224.57/32.19 % (2506435)------------------------------ % 224.57/32.19 % (2506435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.19 % (2506435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.19 % (2506435)CaDiCaL version: 2.1.3 % 224.57/32.19 % (2506435)Termination reason: Instruction limit % 224.57/32.19 % (2506435)Termination phase: Saturation % 224.57/32.19 % (2506435)Time elapsed: 11.026 s % 224.57/32.19 % (2506435)Peak memory usage: 198 MB % 224.57/32.19 % (2506435)Instructions burned: 10545 (million) % 224.57/32.19 % (2506492)Instruction limit reached! % 224.57/32.19 % (2506492)------------------------------ % 224.57/32.19 % (2506492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.19 % (2506492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.19 % (2506492)CaDiCaL version: 2.1.3 % 224.57/32.19 % (2506492)Termination reason: Instruction limit % 224.57/32.19 % (2506492)Termination phase: Saturation % 224.57/32.19 % (2506492)Time elapsed: 3.585 s % 224.57/32.19 % (2506492)Peak memory usage: 91 MB % 224.57/32.19 % (2506492)Instructions burned: 5145 (million) % 224.57/32.19 % (2506510)------------------------------ % 224.57/32.19 % (2506510)------------------------------ % 224.57/32.19 % (2506514)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2057422266:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/3201Mi) % 224.57/32.19 % (2506516)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=3917030221:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2795 on theBenchmark for (2795ds/20260Mi) % 224.57/32.19 % (2506515)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=846880092:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2795 on theBenchmark for (2795ds/4081Mi) % 224.57/32.19 % (2506511)Instruction limit reached! % 224.57/32.19 % (2506511)------------------------------ % 224.57/32.19 % (2506511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.19 % (2506511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.19 % (2506511)CaDiCaL version: 2.1.3 % 224.57/32.19 % (2506511)Termination reason: Instruction limit % 224.57/32.19 % (2506511)Termination phase: Saturation % 224.57/32.19 % (2506511)Time elapsed: 2.153 s % 224.57/32.19 % (2506511)Peak memory usage: 106 MB % 224.57/32.19 % (2506511)Instructions burned: 3553 (million) % 224.57/32.19 % (2506530)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=638375407:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2778 on theBenchmark for (2778ds/58627Mi) % 224.57/32.19 % (2506530)Refutation not found, incomplete strategy % 224.57/32.19 % (2506530)------------------------------ % 224.57/32.19 % (2506530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.19 % (2506530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.19 % (2506530)CaDiCaL version: 2.1.3 % 224.57/32.19 % (2506530)Termination reason: Refutation not found, incomplete strategy % 224.57/32.19 % (2506530)Time elapsed: 0.001 s % 224.57/32.19 % (2506530)Peak memory usage: 89 MB % 224.57/32.19 % (2506530)Instructions burned: 1 (million) % 224.57/32.19 % (2506530)------------------------------ % 224.57/32.19 % (2506530)------------------------------ % 224.57/32.19 % (2506514)Refutation not found, incomplete strategy % 224.57/32.19 % (2506514)------------------------------ % 224.57/32.19 % (2506514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.57/32.19 % (2506514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.57/32.19 % (2506514)CaDiCaL version: 2.1.3 % 224.57/32.19 % (2506514)Termination reason: Refutation not found, incomplete strategy % 224.57/32.19 % (2506514)Time elapsed: 2.103 s % 224.57/32.19 % (2506514)Peak memory usage: 94 MB % 224.57/32.19 % (2506514)Instructions burned: 2655 (million) % 224.57/32.19 % (2506533)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2301436623:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/6258Mi) % 256.82/36.79 % (2506533)Refutation not found, incomplete strategy % 256.82/36.79 % (2506533)------------------------------ % 256.82/36.79 % (2506533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.82/36.79 % (2506533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.82/36.79 % (2506533)CaDiCaL version: 2.1.3 % 256.82/36.79 % (2506533)Termination reason: Refutation not found, incomplete strategy % 256.82/36.79 % (2506533)Time elapsed: 0.024 s % 256.82/36.79 % (2506533)Peak memory usage: 116 MB % 256.82/36.79 % (2506533)Instructions burned: 7 (million) % 256.82/36.79 % (2506514)------------------------------ % 256.82/36.79 % (2506514)------------------------------ % 256.82/36.79 % (2506533)------------------------------ % 256.82/36.79 % (2506533)------------------------------ % 256.82/36.79 % (2506538)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=4129156388:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2770 on theBenchmark for (2770ds/34001Mi) % 256.82/36.79 % (2506539)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1195438544:s2a=on:i=71622:s2at=-1:rtra=on_2770 on theBenchmark for (2770ds/71622Mi) % 256.82/36.79 % (2506515)Instruction limit reached! % 256.82/36.79 % (2506515)------------------------------ % 256.82/36.79 % (2506515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.82/36.79 % (2506515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.82/36.79 % (2506515)CaDiCaL version: 2.1.3 % 256.82/36.79 % (2506515)Termination reason: Instruction limit % 256.82/36.79 % (2506515)Termination phase: Saturation % 256.82/36.79 % (2506515)Time elapsed: 4.072 s % 256.82/36.79 % (2506515)Peak memory usage: 149 MB % 256.82/36.79 % (2506515)Instructions burned: 4081 (million) % 256.82/36.79 % (2506465)Instruction limit reached! % 256.82/36.79 % (2506465)------------------------------ % 256.82/36.79 % (2506465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.82/36.79 % (2506465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.82/36.79 % (2506465)CaDiCaL version: 2.1.3 % 256.82/36.79 % (2506465)Termination reason: Instruction limit % 256.82/36.79 % (2506465)Termination phase: Saturation % 256.82/36.79 % (2506465)Time elapsed: 13.106 s % 256.82/36.79 % (2506465)Peak memory usage: 137 MB % 256.82/36.79 % (2506465)Instructions burned: 12634 (million) % 256.82/36.79 % (2506544)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2592702134:i=24001:kws=precedence:nm=0:rtra=on_2752 on theBenchmark for (2752ds/24001Mi) % 256.82/36.79 % (2506546)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=3628010641:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2752 on theBenchmark for (2752ds/2076Mi) % 256.82/36.79 % (2506544)Refutation not found, incomplete strategy % 256.82/36.79 % (2506544)------------------------------ % 256.82/36.79 % (2506544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.82/36.79 % (2506544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.82/36.79 % (2506544)CaDiCaL version: 2.1.3 % 256.82/36.79 % (2506544)Termination reason: Refutation not found, incomplete strategy % 256.82/36.79 % (2506544)Time elapsed: 0.086 s % 256.82/36.79 % (2506544)Peak memory usage: 117 MB % 256.82/36.79 % (2506544)Instructions burned: 47 (million) % 256.82/36.79 % (2506544)------------------------------ % 256.82/36.79 % (2506544)------------------------------ % 256.82/36.79 % (2506552)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1025029354:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2745 on theBenchmark for (2745ds/83971Mi) % 256.82/36.79 % (2506546)Instruction limit reached! % 256.82/36.79 % (2506546)------------------------------ % 256.82/36.79 % (2506546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.82/36.79 % (2506546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.82/36.79 % (2506546)CaDiCaL version: 2.1.3 % 256.82/36.79 % (2506546)Termination reason: Instruction limit % 256.82/36.79 % (2506546)Termination phase: Saturation % 256.82/36.79 % (2506546)Time elapsed: 1.449 s % 256.82/36.79 % (2506546)Peak memory usage: 129 MB % 256.82/36.79 % (2506546)Instructions burned: 2078 (million) % 256.82/36.79 % (2506558)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=343451205:i=83944:rtra=on_2735 on theBenchmark for (2735ds/83944Mi) % 265.23/38.00 % (2506558)Refutation not found, incomplete strategy % 265.23/38.00 % (2506558)------------------------------ % 265.23/38.00 % (2506558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.23/38.00 % (2506558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.23/38.00 % (2506558)CaDiCaL version: 2.1.3 % 265.23/38.00 % (2506558)Termination reason: Refutation not found, incomplete strategy % 265.23/38.00 % (2506558)Time elapsed: 0.037 s % 265.23/38.00 % (2506558)Peak memory usage: 116 MB % 265.23/38.00 % (2506558)Instructions burned: 8 (million) % 265.23/38.00 % (2506456)Instruction limit reached! % 265.23/38.00 % (2506456)------------------------------ % 265.23/38.00 % (2506456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.23/38.00 % (2506456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.23/38.00 % (2506456)CaDiCaL version: 2.1.3 % 265.23/38.00 % (2506456)Termination reason: Instruction limit % 265.23/38.00 % (2506456)Termination phase: Saturation % 265.23/38.00 % (2506456)Time elapsed: 15.830 s % 265.23/38.00 % (2506456)Peak memory usage: 162 MB % 265.23/38.00 % (2506456)Instructions burned: 17165 (million) % 265.23/38.00 % (2506564)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3158961666:i=9201:rtra=on_2732 on theBenchmark for (2732ds/9201Mi) % 265.23/38.00 % (2506558)------------------------------ % 265.23/38.00 % (2506558)------------------------------ % 265.23/38.00 % (2506566)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 % 265.23/38.00 % (2506566)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3096880787:i=6806:aac=none:nm=0:rtra=on:rawr=on_2729 on theBenchmark for (2729ds/6806Mi) % 265.23/38.00 % (2506566)Refutation not found, incomplete strategy % 265.23/38.00 % (2506566)------------------------------ % 265.23/38.00 % (2506566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.23/38.00 % (2506566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.23/38.00 % (2506566)CaDiCaL version: 2.1.3 % 265.23/38.00 % (2506566)Termination reason: Refutation not found, incomplete strategy % 265.23/38.00 % (2506566)Time elapsed: 0.041 s % 265.23/38.00 % (2506566)Peak memory usage: 116 MB % 265.23/38.00 % (2506566)Instructions burned: 7 (million) % 265.23/38.00 % (2506566)------------------------------ % 265.23/38.00 % (2506566)------------------------------ % 265.23/38.00 % (2506569)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2077650906:s2a=on:i=3553:nm=0:rtra=on_2723 on theBenchmark for (2723ds/3553Mi) % 265.23/38.00 % (2506500)Instruction limit reached! % 265.23/38.00 % (2506500)------------------------------ % 265.23/38.00 % (2506500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.23/38.00 % (2506500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.23/38.00 % (2506500)CaDiCaL version: 2.1.3 % 265.23/38.00 % (2506500)Termination reason: Instruction limit % 265.23/38.00 % (2506500)Termination phase: Saturation % 265.23/38.00 % (2506500)Time elapsed: 10.943 s % 265.23/38.00 % (2506500)Peak memory usage: 134 MB % 265.23/38.00 % (2506500)Instructions burned: 13800 (million) % 265.23/38.00 % (2506572)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=2562108881:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2706 on theBenchmark for (2706ds/2064Mi) % 265.23/38.00 % (2506572)Instruction limit reached! % 265.23/38.00 % (2506572)------------------------------ % 265.23/38.00 % (2506572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.23/38.00 % (2506572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.23/38.00 % (2506572)CaDiCaL version: 2.1.3 % 265.23/38.00 % (2506572)Termination reason: Instruction limit % 265.23/38.00 % (2506572)Termination phase: Saturation % 265.23/38.00 % (2506572)Time elapsed: 2.097 s % 265.23/38.00 % (2506572)Peak memory usage: 145 MB % 265.23/38.00 % (2506572)Instructions burned: 2064 (million) % 265.23/38.00 % (2506569)Instruction limit reached! % 265.23/38.00 % (2506569)------------------------------ % 265.23/38.00 % (2506569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.23/38.00 % (2506569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/38.84 % (2506569)CaDiCaL version: 2.1.3 % 271.10/38.84 % (2506569)Termination reason: Instruction limit % 271.10/38.84 % (2506569)Termination phase: Saturation % 271.10/38.84 % (2506569)Time elapsed: 3.824 s % 271.10/38.84 % (2506569)Peak memory usage: 104 MB % 271.10/38.84 % (2506569)Instructions burned: 3553 (million) % 271.10/38.84 % (2506582)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=4213073169:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2683 on theBenchmark for (2683ds/20260Mi) % 271.10/38.84 % (2506584)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3117106038:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2682 on theBenchmark for (2682ds/1244Mi) % 271.10/38.84 % (2506584)Refutation not found, incomplete strategy % 271.10/38.84 % (2506584)------------------------------ % 271.10/38.84 % (2506584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/38.84 % (2506584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/38.84 % (2506584)CaDiCaL version: 2.1.3 % 271.10/38.84 % (2506584)Termination reason: Refutation not found, incomplete strategy % 271.10/38.84 % (2506584)Time elapsed: 0.030 s % 271.10/38.84 % (2506584)Peak memory usage: 116 MB % 271.10/38.84 % (2506584)Instructions burned: 7 (million) % 271.10/38.84 % (2506584)------------------------------ % 271.10/38.84 % (2506584)------------------------------ % 271.10/38.84 % (2506590)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=2483739079:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2676 on theBenchmark for (2676ds/58261Mi) % 271.10/38.84 % (2506590)Refutation not found, incomplete strategy % 271.10/38.84 % (2506590)------------------------------ % 271.10/38.84 % (2506590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/38.84 % (2506590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/38.84 % (2506590)CaDiCaL version: 2.1.3 % 271.10/38.84 % (2506590)Termination reason: Refutation not found, incomplete strategy % 271.10/38.84 % (2506590)Time elapsed: 0.090 s % 271.10/38.84 % (2506590)Peak memory usage: 117 MB % 271.10/38.84 % (2506590)Instructions burned: 51 (million) % 271.10/38.85 % (2506590)------------------------------ % 271.10/38.85 % (2506590)------------------------------ % 271.10/38.85 % (2506592)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 271.10/38.85 % (2506592)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3073524232:i=6806:aac=none:nm=0:rtra=on:rawr=on_2669 on theBenchmark for (2669ds/6806Mi) % 271.10/38.85 % (2506592)Refutation not found, incomplete strategy % 271.10/38.85 % (2506592)------------------------------ % 271.10/38.85 % (2506592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/38.85 % (2506592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/38.85 % (2506592)CaDiCaL version: 2.1.3 % 271.10/38.85 % (2506592)Termination reason: Refutation not found, incomplete strategy % 271.10/38.85 % (2506592)Time elapsed: 0.041 s % 271.10/38.85 % (2506592)Peak memory usage: 115 MB % 271.10/38.85 % (2506592)Instructions burned: 7 (million) % 271.10/38.85 % (2506592)------------------------------ % 271.10/38.85 % (2506592)------------------------------ % 271.10/38.85 % (2506594)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=2015500966:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2663 on theBenchmark for (2663ds/4081Mi) % 271.10/38.85 % (2506516)Instruction limit reached! % 271.10/38.85 % (2506516)------------------------------ % 271.10/38.85 % (2506516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.10/38.85 % (2506516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.10/38.85 % (2506516)CaDiCaL version: 2.1.3 % 271.10/38.85 % (2506516)Termination reason: Instruction limit % 271.10/38.85 % (2506516)Termination phase: Saturation % 271.10/38.85 % (2506516)Time elapsed: 15.396 s % 271.10/38.85 % (2506516)Peak memory usage: 134 MB % 271.10/38.85 % (2506516)Instructions burned: 20261 (million) % 271.10/38.85 % (2506599)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1682790584:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2639 on theBenchmark for (2639ds/1701Mi) % 276.96/39.60 % (2506599)Refutation not found, incomplete strategy % 276.96/39.60 % (2506599)------------------------------ % 276.96/39.60 % (2506599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.96/39.60 % (2506599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.60 % (2506599)CaDiCaL version: 2.1.3 % 276.96/39.60 % (2506599)Termination reason: Refutation not found, incomplete strategy % 276.96/39.60 % (2506599)Time elapsed: 0.041 s % 276.96/39.60 % (2506599)Peak memory usage: 116 MB % 276.96/39.60 % (2506599)Instructions burned: 7 (million) % 276.96/39.60 % (2506564)Instruction limit reached! % 276.96/39.60 % (2506564)------------------------------ % 276.96/39.60 % (2506564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.96/39.60 % (2506564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.60 % (2506564)CaDiCaL version: 2.1.3 % 276.96/39.60 % (2506564)Termination reason: Instruction limit % 276.96/39.60 % (2506564)Termination phase: Saturation % 276.96/39.60 % (2506564)Time elapsed: 9.688 s % 276.96/39.60 % (2506564)Peak memory usage: 123 MB % 276.96/39.60 % (2506564)Instructions burned: 9201 (million) % 276.96/39.60 % (2506599)------------------------------ % 276.96/39.60 % (2506599)------------------------------ % 276.96/39.60 % (2506605)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=2328079562:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2633 on theBenchmark for (2633ds/57001Mi) % 276.96/39.60 % (2506606)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 % 276.96/39.60 % (2506606)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4211062720:i=8622:aac=none:nm=0:rtra=on:rawr=on_2633 on theBenchmark for (2633ds/8622Mi) % 276.96/39.60 % (2506605)Refutation not found, incomplete strategy % 276.96/39.60 % (2506605)------------------------------ % 276.96/39.60 % (2506605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.96/39.60 % (2506605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.60 % (2506605)CaDiCaL version: 2.1.3 % 276.96/39.60 % (2506605)Termination reason: Refutation not found, incomplete strategy % 276.96/39.60 % (2506605)Time elapsed: 0.063 s % 276.96/39.60 % (2506605)Peak memory usage: 117 MB % 276.96/39.60 % (2506605)Instructions burned: 52 (million) % 276.96/39.60 % (2506606)Refutation not found, incomplete strategy % 276.96/39.60 % (2506606)------------------------------ % 276.96/39.60 % (2506606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.96/39.60 % (2506606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.60 % (2506606)CaDiCaL version: 2.1.3 % 276.96/39.60 % (2506606)Termination reason: Refutation not found, incomplete strategy % 276.96/39.60 % (2506606)Time elapsed: 0.041 s % 276.96/39.60 % (2506606)Peak memory usage: 115 MB % 276.96/39.60 % (2506606)Instructions burned: 7 (million) % 276.96/39.60 % (2506605)------------------------------ % 276.96/39.60 % (2506605)------------------------------ % 276.96/39.60 % (2506609)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2165335306:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2628 on theBenchmark for (2628ds/24Mi) % 276.96/39.60 % (2506606)------------------------------ % 276.96/39.60 % (2506606)------------------------------ % 276.96/39.60 % (2506609)Instruction limit reached! % 276.96/39.60 % (2506609)------------------------------ % 276.96/39.60 % (2506609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.96/39.60 % (2506609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.60 % (2506609)CaDiCaL version: 2.1.3 % 276.96/39.60 % (2506609)Termination reason: Instruction limit % 276.96/39.60 % (2506609)Termination phase: Saturation % 276.96/39.60 % (2506609)Time elapsed: 0.039 s % 276.96/39.60 % (2506609)Peak memory usage: 116 MB % 276.96/39.60 % (2506609)Instructions burned: 25 (million) % 276.96/39.60 % (2506611)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=734751556:i=614:kws=precedence:nm=0:rtra=on_2626 on theBenchmark for (2626ds/614Mi) % 276.96/39.60 % (2506612)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3303011409:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2626 on theBenchmark for (2626ds/402Mi) % 281.56/40.24 % (2506611)Refutation not found, incomplete strategy % 281.56/40.24 % (2506611)------------------------------ % 281.56/40.24 % (2506611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.56/40.24 % (2506611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.24 % (2506611)CaDiCaL version: 2.1.3 % 281.56/40.24 % (2506611)Termination reason: Refutation not found, incomplete strategy % 281.56/40.24 % (2506611)Time elapsed: 0.093 s % 281.56/40.24 % (2506611)Peak memory usage: 118 MB % 281.56/40.24 % (2506611)Instructions burned: 57 (million) % 281.56/40.24 % (2506594)Instruction limit reached! % 281.56/40.24 % (2506594)------------------------------ % 281.56/40.24 % (2506594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.56/40.24 % (2506594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.24 % (2506594)CaDiCaL version: 2.1.3 % 281.56/40.24 % (2506594)Termination reason: Instruction limit % 281.56/40.24 % (2506594)Termination phase: Saturation % 281.56/40.24 % (2506594)Time elapsed: 3.900 s % 281.56/40.24 % (2506594)Peak memory usage: 148 MB % 281.56/40.24 % (2506594)Instructions burned: 4082 (million) % 281.56/40.24 % (2506611)------------------------------ % 281.56/40.24 % (2506611)------------------------------ % 281.56/40.24 % (2506612)Instruction limit reached! % 281.56/40.24 % (2506612)------------------------------ % 281.56/40.24 % (2506612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.56/40.24 % (2506612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.24 % (2506612)CaDiCaL version: 2.1.3 % 281.56/40.24 % (2506612)Termination reason: Instruction limit % 281.56/40.24 % (2506612)Termination phase: Saturation % 281.56/40.24 % (2506612)Time elapsed: 0.482 s % 281.56/40.24 % (2506612)Peak memory usage: 119 MB % 281.56/40.24 % (2506612)Instructions burned: 403 (million) % 281.56/40.24 % (2506619)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=991907875:s2a=on:i=14:rtra=on:inst=on_2621 on theBenchmark for (2621ds/14Mi) % 281.56/40.24 % (2506619)Instruction limit reached! % 281.56/40.24 % (2506619)------------------------------ % 281.56/40.24 % (2506619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.56/40.24 % (2506619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.24 % (2506619)CaDiCaL version: 2.1.3 % 281.56/40.24 % (2506619)Termination reason: Instruction limit % 281.56/40.24 % (2506619)Termination phase: Saturation % 281.56/40.24 % (2506619)Time elapsed: 0.013 s % 281.56/40.24 % (2506619)Peak memory usage: 88 MB % 281.56/40.24 % (2506619)Instructions burned: 14 (million) % 281.56/40.24 % (2506620)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2398365994:i=8:rtra=on_2620 on theBenchmark for (2620ds/8Mi) % 281.56/40.24 % (2506620)Instruction limit reached! % 281.56/40.24 % (2506620)------------------------------ % 281.56/40.24 % (2506620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.56/40.24 % (2506620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.24 % (2506620)CaDiCaL version: 2.1.3 % 281.56/40.24 % (2506620)Termination reason: Instruction limit % 281.56/40.24 % (2506620)Termination phase: Saturation % 281.56/40.24 % (2506620)Time elapsed: 0.010 s % 281.56/40.24 % (2506620)Peak memory usage: 89 MB % 281.56/40.24 % (2506620)Instructions burned: 9 (million) % 281.56/40.24 % (2506621)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=700420652:i=92:rtra=on_2619 on theBenchmark for (2619ds/92Mi) % 281.56/40.24 % (2506621)Refutation not found, incomplete strategy % 281.56/40.24 % (2506621)------------------------------ % 281.56/40.24 % (2506621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.56/40.24 % (2506621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.24 % (2506621)CaDiCaL version: 2.1.3 % 281.56/40.24 % (2506621)Termination reason: Refutation not found, incomplete strategy % 281.56/40.24 % (2506621)Time elapsed: 0.042 s % 281.56/40.24 % (2506621)Peak memory usage: 116 MB % 281.56/40.24 % (2506621)Instructions burned: 7 (million) % 281.56/40.24 % (2506624)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2412806332:i=66:rtra=on_2619 on theBenchmark for (2619ds/66Mi) % 281.56/40.24 % (2506626)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2916915055:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2618 on theBenchmark for (2618ds/28Mi) % 281.56/40.24 % (2506626)Refutation not found, incomplete strategy % 281.56/40.24 % (2506626)------------------------------ % 281.56/40.24 % (2506626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.97/40.71 % (2506626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.97/40.71 % (2506626)CaDiCaL version: 2.1.3 % 284.97/40.71 % (2506626)Termination reason: Refutation not found, incomplete strategy % 284.97/40.71 % (2506626)Time elapsed: 0.002 s % 284.97/40.71 % (2506626)Peak memory usage: 88 MB % 284.97/40.71 % (2506626)Instructions burned: 1 (million) % 284.97/40.71 % (2506624)Instruction limit reached! % 284.97/40.71 % (2506624)------------------------------ % 284.97/40.71 % (2506624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.97/40.71 % (2506624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.97/40.71 % (2506624)CaDiCaL version: 2.1.3 % 284.97/40.71 % (2506624)Termination reason: Instruction limit % 284.97/40.71 % (2506624)Termination phase: Saturation % 284.97/40.71 % (2506624)Time elapsed: 0.104 s % 284.97/40.71 % (2506624)Peak memory usage: 117 MB % 284.97/40.71 % (2506624)Instructions burned: 66 (million) % 284.97/40.71 % (2506630)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=1484720283:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2616 on theBenchmark for (2616ds/58Mi) % 284.97/40.71 % (2506630)Instruction limit reached! % 284.97/40.71 % (2506630)------------------------------ % 284.97/40.71 % (2506630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.97/40.71 % (2506630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.97/40.71 % (2506630)CaDiCaL version: 2.1.3 % 284.97/40.71 % (2506630)Termination reason: Instruction limit % 284.97/40.71 % (2506630)Termination phase: Saturation % 284.97/40.71 % (2506630)Time elapsed: 0.044 s % 284.97/40.71 % (2506630)Peak memory usage: 88 MB % 284.97/40.71 % (2506630)Instructions burned: 58 (million) % 284.97/40.71 % (2506621)------------------------------ % 284.97/40.71 % (2506621)------------------------------ % 284.97/40.71 % (2506626)------------------------------ % 284.97/40.71 % (2506626)------------------------------ % 284.97/40.71 % (2506634)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2947704864:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2613 on theBenchmark for (2613ds/32Mi) % 284.97/40.71 % (2506635)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4037394335:i=48:canc=force:rtra=on_2613 on theBenchmark for (2613ds/48Mi) % 284.97/40.71 % (2506634)Instruction limit reached! % 284.97/40.71 % (2506634)------------------------------ % 284.97/40.71 % (2506634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.97/40.71 % (2506634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.97/40.71 % (2506634)CaDiCaL version: 2.1.3 % 284.97/40.71 % (2506634)Termination reason: Instruction limit % 284.97/40.71 % (2506634)Termination phase: Saturation % 284.97/40.71 % (2506634)Time elapsed: 0.030 s % 284.97/40.71 % (2506634)Peak memory usage: 90 MB % 284.97/40.71 % (2506634)Instructions burned: 33 (million) % 284.97/40.71 % (2506635)Instruction limit reached! % 284.97/40.71 % (2506635)------------------------------ % 284.97/40.71 % (2506635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.97/40.71 % (2506635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.97/40.71 % (2506635)CaDiCaL version: 2.1.3 % 284.97/40.71 % (2506635)Termination reason: Instruction limit % 284.97/40.71 % (2506635)Termination phase: Saturation % 284.97/40.71 % (2506635)Time elapsed: 0.052 s % 284.97/40.71 % (2506635)Peak memory usage: 89 MB % 284.97/40.71 % (2506635)Instructions burned: 48 (million) % 284.97/40.71 % (2506638)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=515666259:i=54:canc=cautious:fsr=off:rtra=on_2612 on theBenchmark for (2612ds/54Mi) % 284.97/40.71 % (2506638)Instruction limit reached! % 284.97/40.71 % (2506638)------------------------------ % 284.97/40.71 % (2506638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.97/40.71 % (2506638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.97/40.71 % (2506638)CaDiCaL version: 2.1.3 % 284.97/40.71 % (2506638)Termination reason: Instruction limit % 284.97/40.71 % (2506638)Termination phase: Saturation % 284.97/40.71 % (2506638)Time elapsed: 0.038 s % 284.97/40.71 % (2506638)Peak memory usage: 90 MB % 284.97/40.71 % (2506638)Instructions burned: 55 (million) % 284.97/40.71 % (2506643)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1309218914:i=170:gtgl=4:rtra=on:gtg=exists_sym_2610 on theBenchmark for (2610ds/170Mi) % 288.35/41.16 % (2506644)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2994142866:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2610 on theBenchmark for (2610ds/4Mi) % 288.35/41.16 % (2506644)Instruction limit reached! % 288.35/41.16 % (2506644)------------------------------ % 288.35/41.16 % (2506644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.16 % (2506644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.16 % (2506644)CaDiCaL version: 2.1.3 % 288.35/41.16 % (2506644)Termination reason: Instruction limit % 288.35/41.16 % (2506644)Termination phase: Saturation % 288.35/41.16 % (2506644)Time elapsed: 0.006 s % 288.35/41.16 % (2506644)Peak memory usage: 88 MB % 288.35/41.16 % (2506644)Instructions burned: 5 (million) % 288.35/41.16 % (2506647)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1870138646:i=362:rtra=on:ss=axioms:ev=cautious_2610 on theBenchmark for (2610ds/362Mi) % 288.35/41.16 % (2506647)Refutation not found, incomplete strategy % 288.35/41.16 % (2506647)------------------------------ % 288.35/41.16 % (2506647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.16 % (2506647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.16 % (2506647)CaDiCaL version: 2.1.3 % 288.35/41.16 % (2506647)Termination reason: Refutation not found, incomplete strategy % 288.35/41.16 % (2506647)Time elapsed: 0.008 s % 288.35/41.16 % (2506647)Peak memory usage: 89 MB % 288.35/41.16 % (2506647)Instructions burned: 5 (million) % 288.35/41.16 % (2506643)Instruction limit reached! % 288.35/41.16 % (2506643)------------------------------ % 288.35/41.16 % (2506643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.16 % (2506643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.16 % (2506643)CaDiCaL version: 2.1.3 % 288.35/41.16 % (2506643)Termination reason: Instruction limit % 288.35/41.16 % (2506643)Termination phase: Saturation % 288.35/41.16 % (2506643)Time elapsed: 0.180 s % 288.35/41.16 % (2506643)Peak memory usage: 90 MB % 288.35/41.16 % (2506643)Instructions burned: 170 (million) % 288.35/41.16 % (2506652)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1249512411:i=8:ep=RST:ins=2:rtra=on_2608 on theBenchmark for (2608ds/8Mi) % 288.35/41.16 % (2506652)Instruction limit reached! % 288.35/41.16 % (2506652)------------------------------ % 288.35/41.16 % (2506652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.16 % (2506652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.16 % (2506652)CaDiCaL version: 2.1.3 % 288.35/41.16 % (2506652)Termination reason: Instruction limit % 288.35/41.16 % (2506652)Termination phase: Saturation % 288.35/41.16 % (2506652)Time elapsed: 0.011 s % 288.35/41.16 % (2506652)Peak memory usage: 89 MB % 288.35/41.16 % (2506652)Instructions burned: 9 (million) % 288.35/41.16 % (2506655)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=344310735:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2606 on theBenchmark for (2606ds/132Mi) % 288.35/41.16 % (2506647)------------------------------ % 288.35/41.16 % (2506647)------------------------------ % 288.35/41.16 % (2506658)lrs+10_1_thi=all:si=on:fd=off:random_seed=1904931221:i=106:rtra=on:gtg=all_2605 on theBenchmark for (2605ds/106Mi) % 288.35/41.16 % (2506655)Instruction limit reached! % 288.35/41.16 % (2506655)------------------------------ % 288.35/41.16 % (2506655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.16 % (2506655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.16 % (2506655)CaDiCaL version: 2.1.3 % 288.35/41.16 % (2506655)Termination reason: Instruction limit % 288.35/41.16 % (2506655)Termination phase: Saturation % 288.35/41.16 % (2506655)Time elapsed: 0.163 s % 288.35/41.16 % (2506655)Peak memory usage: 135 MB % 288.35/41.16 % (2506655)Instructions burned: 132 (million) % 288.35/41.16 % (2506662)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=3167520068:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2604 on theBenchmark for (2604ds/16Mi) % 288.35/41.16 % (2506658)Instruction limit reached! % 288.35/41.16 % (2506658)------------------------------ % 288.35/41.16 % (2506658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.16 % (2506658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.16 % (2506658)CaDiCaL version: 2.1.3 % 288.35/41.16 % (2506658)Termination reason: Instruction limit % 292.77/41.97 % (2506658)Termination phase: Saturation % 292.77/41.97 % (2506658)Time elapsed: 0.136 s % 292.77/41.97 % (2506658)Peak memory usage: 113 MB % 292.77/41.97 % (2506658)Instructions burned: 106 (million) % 292.77/41.97 % (2506662)Instruction limit reached! % 292.77/41.97 % (2506662)------------------------------ % 292.77/41.97 % (2506662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.77/41.97 % (2506662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.77/41.97 % (2506662)CaDiCaL version: 2.1.3 % 292.77/41.97 % (2506662)Termination reason: Instruction limit % 292.77/41.97 % (2506662)Termination phase: Saturation % 292.77/41.97 % (2506662)Time elapsed: 0.018 s % 292.77/41.97 % (2506662)Peak memory usage: 88 MB % 292.77/41.97 % (2506662)Instructions burned: 17 (million) % 292.77/41.97 % (2506666)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3932346654:st=3:i=4:rtra=on:ss=axioms_2602 on theBenchmark for (2602ds/4Mi) % 292.77/41.97 % (2506666)Instruction limit reached! % 292.77/41.97 % (2506666)------------------------------ % 292.77/41.97 % (2506666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.77/41.97 % (2506666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.77/41.97 % (2506666)CaDiCaL version: 2.1.3 % 292.77/41.97 % (2506666)Termination reason: Instruction limit % 292.77/41.97 % (2506666)Termination phase: Saturation % 292.77/41.97 % (2506666)Time elapsed: 0.007 s % 292.77/41.97 % (2506666)Peak memory usage: 89 MB % 292.77/41.97 % (2506666)Instructions burned: 5 (million) % 292.77/41.97 % (2506668)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2556057838:i=4:doe=on:canc=force:asg=cautious:rtra=on_2602 on theBenchmark for (2602ds/4Mi) % 292.77/41.97 % (2506668)Instruction limit reached! % 292.77/41.97 % (2506668)------------------------------ % 292.77/41.97 % (2506668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.77/41.97 % (2506668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.77/41.97 % (2506668)CaDiCaL version: 2.1.3 % 292.77/41.97 % (2506668)Termination reason: Instruction limit % 292.77/41.97 % (2506668)Termination phase: Saturation % 292.77/41.97 % (2506668)Time elapsed: 0.006 s % 292.77/41.97 % (2506668)Peak memory usage: 89 MB % 292.77/41.97 % (2506668)Instructions burned: 4 (million) % 292.77/41.97 % (2506669)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1817182301:i=254:doe=on:rtra=on_2602 on theBenchmark for (2602ds/254Mi) % 292.77/41.97 % (2506673)dis+10_1_si=on:random_seed=4024036568:i=20:ep=R:rtra=on_2600 on theBenchmark for (2600ds/20Mi) % 292.77/41.97 % (2506673)Instruction limit reached! % 292.77/41.97 % (2506673)------------------------------ % 292.77/41.97 % (2506673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.77/41.97 % (2506673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.77/41.97 % (2506673)CaDiCaL version: 2.1.3 % 292.77/41.97 % (2506673)Termination reason: Instruction limit % 292.77/41.97 % (2506673)Termination phase: Saturation % 292.77/41.97 % (2506673)Time elapsed: 0.017 s % 292.77/41.97 % (2506673)Peak memory usage: 88 MB % 292.77/41.97 % (2506673)Instructions burned: 20 (million) % 292.77/41.97 % (2506538)Instruction limit reached! % 292.77/41.97 % (2506538)------------------------------ % 292.77/41.97 % (2506538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.77/41.97 % (2506538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.77/41.97 % (2506538)CaDiCaL version: 2.1.3 % 292.77/41.97 % (2506538)Termination reason: Instruction limit % 292.77/41.97 % (2506538)Termination phase: Saturation % 292.77/41.97 % (2506538)Time elapsed: 17.053 s % 292.77/41.97 % (2506538)Peak memory usage: 264 MB % 292.77/41.97 % (2506538)Instructions burned: 34002 (million) % 292.77/41.97 % (2506669)Instruction limit reached! % 292.77/41.97 % (2506669)------------------------------ % 292.77/41.97 % (2506669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.77/41.97 % (2506669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.77/41.97 % (2506669)CaDiCaL version: 2.1.3 % 292.77/41.97 % (2506669)Termination reason: Instruction limit % 292.77/41.97 % (2506669)Termination phase: Saturation % 292.77/41.97 % (2506669)Time elapsed: 0.208 s % 292.77/41.97 % (2506669)Peak memory usage: 118 MB % 292.77/41.97 % (2506669)Instructions burned: 254 (million) % 292.77/41.97 % (2506676)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1292715702:i=52:canc=cautious:av=off:rtra=on_2600 on theBenchmark for (2600ds/52Mi) % 292.77/41.97 % (2506676)Refutation not found, incomplete strategy % 297.00/42.56 % (2506676)------------------------------ % 297.00/42.56 % (2506676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.00/42.56 % (2506676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.00/42.56 % (2506676)CaDiCaL version: 2.1.3 % 297.00/42.56 % (2506676)Termination reason: Refutation not found, incomplete strategy % 297.00/42.56 % (2506676)Time elapsed: 0.004 s % 297.00/42.56 % (2506676)Peak memory usage: 89 MB % 297.00/42.56 % (2506676)Instructions burned: 2 (million) % 297.00/42.56 % (2506682)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1795889330:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2597 on theBenchmark for (2597ds/16Mi) % 297.00/42.56 % (2506679)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3806574883:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2598 on theBenchmark for (2598ds/70Mi) % 297.00/42.56 % (2506681)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3522383330:i=4:fsr=off:rtra=on:inst=on_2598 on theBenchmark for (2598ds/4Mi) % 297.00/42.56 % (2506682)Instruction limit reached! % 297.00/42.56 % (2506682)------------------------------ % 297.00/42.56 % (2506682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.00/42.56 % (2506682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.00/42.56 % (2506682)CaDiCaL version: 2.1.3 % 297.00/42.56 % (2506682)Termination reason: Instruction limit % 297.00/42.56 % (2506682)Termination phase: Saturation % 297.00/42.56 % (2506682)Time elapsed: 0.009 s % 297.00/42.56 % (2506682)Peak memory usage: 89 MB % 297.00/42.56 % (2506682)Instructions burned: 16 (million) % 297.00/42.56 % (2506681)Instruction limit reached! % 297.00/42.56 % (2506681)------------------------------ % 297.00/42.56 % (2506681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.00/42.56 % (2506681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.00/42.56 % (2506681)CaDiCaL version: 2.1.3 % 297.00/42.56 % (2506681)Termination reason: Instruction limit % 297.00/42.56 % (2506681)Termination phase: Saturation % 297.00/42.56 % (2506681)Time elapsed: 0.005 s % 297.00/42.56 % (2506681)Peak memory usage: 88 MB % 297.00/42.56 % (2506681)Instructions burned: 4 (million) % 297.00/42.56 % (2506679)Instruction limit reached! % 297.00/42.56 % (2506679)------------------------------ % 297.00/42.56 % (2506679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.00/42.56 % (2506679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.00/42.56 % (2506679)CaDiCaL version: 2.1.3 % 297.00/42.56 % (2506679)Termination reason: Instruction limit % 297.00/42.56 % (2506679)Termination phase: Saturation % 297.00/42.56 % (2506679)Time elapsed: 0.068 s % 297.00/42.56 % (2506679)Peak memory usage: 90 MB % 297.00/42.56 % (2506679)Instructions burned: 70 (million) % 297.00/42.56 % (2506689)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=917778496:i=740:ep=RS:fsr=off:rtra=on_2596 on theBenchmark for (2596ds/740Mi) % 297.00/42.56 % (2506690)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1733650039:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2596 on theBenchmark for (2596ds/26Mi) % 297.00/42.56 % (2506676)------------------------------ % 297.00/42.56 % (2506676)------------------------------ % 297.00/42.56 % (2506691)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=574748641:i=452:rtra=on:gtg=position:ss=axioms_2595 on theBenchmark for (2595ds/452Mi) % 297.00/42.56 % (2506690)Instruction limit reached! % 297.00/42.56 % (2506690)------------------------------ % 297.00/42.56 % (2506690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.00/42.56 % (2506690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.00/42.56 % (2506690)CaDiCaL version: 2.1.3 % 297.00/42.56 % (2506690)Termination reason: Instruction limit % 297.00/42.56 % (2506690)Termination phase: Saturation % 297.00/42.56 % (2506690)Time elapsed: 0.053 s % 297.00/42.56 % (2506690)Peak memory usage: 116 MB % 297.00/42.56 % (2506690)Instructions burned: 26 (million) % 297.00/42.56 % (2506691)Refutation not found, incomplete strategy % 297.00/42.56 % (2506691)------------------------------ % 297.00/42.56 % (2506691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.00/42.56 % (2506691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.00/42.56 % (2506691)CaDiTerminated %------------------------------------------------------------------------------