%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX149_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n002.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:45:58 PM UTC 2026 % Result : Timeout 300.66s 43.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX149_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n002.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 15:07:22 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 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 % 3.85/1.38 % (425752)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.85/1.38 % (425794)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3047153046:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.85/1.38 % (425794)Instruction limit reached! % 3.85/1.38 % (425794)------------------------------ % 3.85/1.38 % (425794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.85/1.38 % (425794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.38 % (425794)CaDiCaL version: 2.1.3 % 3.85/1.38 % (425794)Termination reason: Instruction limit % 3.85/1.38 % (425794)Termination phase: Saturation % 3.85/1.38 % (425794)Time elapsed: 0.009 s % 3.85/1.38 % (425794)Peak memory usage: 86 MB % 3.85/1.38 % (425794)Instructions burned: 47 (million) % 3.85/1.38 % (425789)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=556770141:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.85/1.38 % (425795)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=486896705:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.85/1.38 % (425789)Instruction limit reached! % 3.85/1.38 % (425789)------------------------------ % 3.85/1.38 % (425789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.85/1.38 % (425789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.38 % (425789)CaDiCaL version: 2.1.3 % 3.85/1.38 % (425789)Termination reason: Instruction limit % 3.85/1.38 % (425789)Termination phase: Property scanning % 3.85/1.38 % (425789)Time elapsed: 0.003 s % 3.85/1.38 % (425789)Peak memory usage: 85 MB % 3.85/1.38 % (425789)Instructions burned: 13 (million) % 3.85/1.38 % (425793)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2593843982:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.85/1.38 % (425790)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3943418115:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.85/1.38 % (425791)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2541782645:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.85/1.38 % (425792)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=745588262:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.85/1.38 % (425793)Instruction limit reached! % 3.85/1.38 % (425793)------------------------------ % 3.85/1.38 % (425793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.85/1.38 % (425793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.38 % (425793)CaDiCaL version: 2.1.3 % 3.85/1.38 % (425793)Termination reason: Instruction limit % 3.85/1.38 % (425793)Termination phase: Property scanning % 3.85/1.38 % (425793)Time elapsed: 0.004 s % 3.85/1.38 % (425793)Peak memory usage: 85 MB % 3.85/1.38 % (425793)Instructions burned: 4 (million) % 3.85/1.38 % (425795)Instruction limit reached! % 3.85/1.38 % (425795)------------------------------ % 3.85/1.38 % (425795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.85/1.38 % (425795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.38 % (425795)CaDiCaL version: 2.1.3 % 3.85/1.38 % (425795)Termination reason: Instruction limit % 3.85/1.38 % (425795)Termination phase: Property scanning % 3.85/1.38 % (425795)Time elapsed: 0.028 s % 3.85/1.38 % (425795)Peak memory usage: 86 MB % 3.85/1.38 % (425795)Instructions burned: 34 (million) % 3.85/1.38 % (425792)Instruction limit reached! % 3.85/1.38 % (425792)------------------------------ % 3.85/1.38 % (425792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.85/1.38 % (425792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.85/1.38 % (425792)CaDiCaL version: 2.1.3 % 3.85/1.38 % (425792)Termination reason: Instruction limit % 3.85/1.38 % (425792)Termination phase: Property scanning % 3.85/1.38 % (425792)Time elapsed: 0.006 s % 3.85/1.38 % (425792)Peak memory usage: 85 MB % 3.85/1.38 % (425792)Instructions burned: 7 (million) % 3.85/1.38 % (425810)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=951175463:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 3.85/1.38 % (425810)Instruction limit reached! % 3.85/1.38 % (425810)------------------------------ % 5.04/1.61 % (425810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.04/1.61 % (425810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.04/1.61 % (425810)CaDiCaL version: 2.1.3 % 5.04/1.61 % (425810)Termination reason: Instruction limit % 5.04/1.61 % (425810)Termination phase: Property scanning % 5.04/1.61 % (425810)Time elapsed: 0.007 s % 5.04/1.61 % (425810)Peak memory usage: 86 MB % 5.04/1.61 % (425810)Instructions burned: 31 (million) % 5.04/1.61 % (425803)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3475457411:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.04/1.61 % (425803)Instruction limit reached! % 5.04/1.61 % (425803)------------------------------ % 5.04/1.61 % (425803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.04/1.61 % (425803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.04/1.61 % (425803)CaDiCaL version: 2.1.3 % 5.04/1.61 % (425803)Termination reason: Instruction limit % 5.04/1.61 % (425803)Termination phase: Property scanning % 5.04/1.61 % (425803)Time elapsed: 0.010 s % 5.04/1.61 % (425803)Peak memory usage: 85 MB % 5.04/1.61 % (425803)Instructions burned: 14 (million) % 5.04/1.61 % (425791)Instruction limit reached! % 5.04/1.61 % (425791)------------------------------ % 5.04/1.61 % (425791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.04/1.61 % (425791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.04/1.61 % (425791)CaDiCaL version: 2.1.3 % 5.04/1.61 % (425791)Termination reason: Instruction limit % 5.04/1.61 % (425791)Termination phase: Saturation % 5.04/1.61 % (425791)Time elapsed: 0.169 s % 5.04/1.61 % (425791)Peak memory usage: 118 MB % 5.04/1.61 % (425791)Instructions burned: 202 (million) % 5.04/1.61 % (425824)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3466891311:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 5.04/1.61 % (425824)Instruction limit reached! % 5.04/1.61 % (425824)------------------------------ % 5.04/1.61 % (425824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.04/1.61 % (425824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.04/1.61 % (425824)CaDiCaL version: 2.1.3 % 5.04/1.61 % (425824)Termination reason: Instruction limit % 5.04/1.61 % (425824)Termination phase: Property scanning % 5.04/1.61 % (425824)Time elapsed: 0.020 s % 5.04/1.61 % (425824)Peak memory usage: 87 MB % 5.04/1.61 % (425824)Instructions burned: 88 (million) % 5.04/1.61 % (425819)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=3537573420:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 5.04/1.61 % (425818)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1098045996:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 5.04/1.61 % (425819)Instruction limit reached! % 5.04/1.61 % (425819)------------------------------ % 5.04/1.61 % (425819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.04/1.61 % (425819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.04/1.61 % (425819)CaDiCaL version: 2.1.3 % 5.04/1.61 % (425819)Termination reason: Instruction limit % 5.04/1.61 % (425819)Termination phase: Property scanning % 5.04/1.61 % (425819)Time elapsed: 0.024 s % 5.04/1.61 % (425819)Peak memory usage: 86 MB % 5.04/1.61 % (425819)Instructions burned: 27 (million) % 5.04/1.61 % (425790)Instruction limit reached! % 5.04/1.61 % (425790)------------------------------ % 5.04/1.61 % (425790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.04/1.61 % (425790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.04/1.61 % (425790)CaDiCaL version: 2.1.3 % 5.04/1.61 % (425790)Termination reason: Instruction limit % 5.04/1.61 % (425790)Termination phase: Saturation % 5.04/1.61 % (425790)Time elapsed: 0.237 s % 5.04/1.61 % (425790)Peak memory usage: 116 MB % 5.04/1.61 % (425790)Instructions burned: 308 (million) % 5.04/1.61 % (425817)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2301025753:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 5.04/1.61 % (425818)Instruction limit reached! % 5.04/1.61 % (425818)------------------------------ % 5.04/1.61 % (425818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.88/1.83 % (425818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.88/1.83 % (425818)CaDiCaL version: 2.1.3 % 6.88/1.83 % (425818)Termination reason: Instruction limit % 6.88/1.83 % (425818)Termination phase: Property scanning % 6.88/1.83 % (425818)Time elapsed: 0.021 s % 6.88/1.83 % (425818)Peak memory usage: 86 MB % 6.88/1.83 % (425818)Instructions burned: 25 (million) % 6.88/1.83 % (425817)Instruction limit reached! % 6.88/1.83 % (425817)------------------------------ % 6.88/1.83 % (425817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.88/1.83 % (425817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.88/1.83 % (425817)CaDiCaL version: 2.1.3 % 6.88/1.83 % (425817)Termination reason: Instruction limit % 6.88/1.83 % (425817)Termination phase: Including theory axioms % 6.88/1.83 % (425817)Time elapsed: 0.013 s % 6.88/1.83 % (425817)Peak memory usage: 86 MB % 6.88/1.83 % (425817)Instructions burned: 16 (million) % 6.88/1.83 % (425834)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1230777827:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 6.88/1.83 % (425834)Instruction limit reached! % 6.88/1.83 % (425834)------------------------------ % 6.88/1.83 % (425834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.88/1.83 % (425834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.88/1.83 % (425834)CaDiCaL version: 2.1.3 % 6.88/1.83 % (425834)Termination reason: Instruction limit % 6.88/1.83 % (425834)Termination phase: Property scanning % 6.88/1.83 % (425834)Time elapsed: 0.002 s % 6.88/1.83 % (425834)Peak memory usage: 85 MB % 6.88/1.83 % (425834)Instructions burned: 4 (million) % 6.88/1.83 % (425830)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2598174049:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 6.88/1.83 % (425827)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3013248244:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 6.88/1.83 % (425827)Instruction limit reached! % 6.88/1.83 % (425827)------------------------------ % 6.88/1.83 % (425827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.88/1.83 % (425827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.88/1.83 % (425827)CaDiCaL version: 2.1.3 % 6.88/1.83 % (425827)Termination reason: Instruction limit % 6.88/1.83 % (425827)Termination phase: shuffling % 6.88/1.83 % (425827)Time elapsed: 0.002 s % 6.88/1.83 % (425827)Peak memory usage: 85 MB % 6.88/1.83 % (425827)Instructions burned: 2 (million) % 6.88/1.83 % (425838)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1137964685:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 6.88/1.83 % (425830)Refutation not found, incomplete strategy % 6.88/1.83 % (425830)------------------------------ % 6.88/1.83 % (425830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.88/1.83 % (425830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.88/1.83 % (425830)CaDiCaL version: 2.1.3 % 6.88/1.83 % (425830)Termination reason: Refutation not found, incomplete strategy % 6.88/1.83 % (425830)Time elapsed: 0.028 s % 6.88/1.83 % (425830)Peak memory usage: 88 MB % 6.88/1.83 % (425830)Instructions burned: 47 (million) % 6.88/1.83 % (425838)Instruction limit reached! % 6.88/1.83 % (425838)------------------------------ % 6.88/1.83 % (425838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.88/1.83 % (425838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.88/1.83 % (425838)CaDiCaL version: 2.1.3 % 6.88/1.83 % (425838)Termination reason: Instruction limit % 6.88/1.83 % (425838)Termination phase: Saturation % 6.88/1.83 % (425838)Time elapsed: 0.027 s % 6.88/1.83 % (425838)Peak memory usage: 87 MB % 6.88/1.83 % (425838)Instructions burned: 69 (million) % 6.88/1.83 % (425839)lrs+10_1_thi=all:si=on:fd=off:random_seed=650114700:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.88/1.83 % (425841)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=3134750224:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 6.88/1.83 % (425841)Instruction limit reached! % 6.88/1.83 % (425841)------------------------------ % 6.88/1.83 % (425841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.01/2.11 % (425841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.01/2.11 % (425841)CaDiCaL version: 2.1.3 % 10.01/2.11 % (425841)Termination reason: Instruction limit % 10.01/2.11 % (425841)Termination phase: Property scanning % 10.01/2.11 % (425841)Time elapsed: 0.008 s % 10.01/2.11 % (425841)Peak memory usage: 85 MB % 10.01/2.11 % (425841)Instructions burned: 9 (million) % 10.01/2.11 % (425842)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3535577669:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 10.01/2.11 % (425842)Instruction limit reached! % 10.01/2.11 % (425842)------------------------------ % 10.01/2.11 % (425842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.01/2.11 % (425842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.01/2.11 % (425842)CaDiCaL version: 2.1.3 % 10.01/2.11 % (425842)Termination reason: Instruction limit % 10.01/2.11 % (425842)Termination phase: Property scanning % 10.01/2.11 % (425842)Time elapsed: 0.004 s % 10.01/2.11 % (425842)Peak memory usage: 85 MB % 10.01/2.11 % (425842)Instructions burned: 4 (million) % 10.01/2.11 % (425839)Instruction limit reached! % 10.01/2.11 % (425839)------------------------------ % 10.01/2.11 % (425839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.01/2.11 % (425839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.01/2.11 % (425839)CaDiCaL version: 2.1.3 % 10.01/2.11 % (425839)Termination reason: Instruction limit % 10.01/2.11 % (425839)Termination phase: Property scanning % 10.01/2.11 % (425839)Time elapsed: 0.040 s % 10.01/2.11 % (425839)Peak memory usage: 86 MB % 10.01/2.11 % (425839)Instructions burned: 54 (million) % 10.01/2.11 % (425856)dis+10_1_si=on:random_seed=836132948:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 10.01/2.11 % (425856)Instruction limit reached! % 10.01/2.11 % (425856)------------------------------ % 10.01/2.11 % (425856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.01/2.11 % (425856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.01/2.11 % (425856)CaDiCaL version: 2.1.3 % 10.01/2.11 % (425856)Termination reason: Instruction limit % 10.01/2.11 % (425856)Termination phase: Property scanning % 10.01/2.11 % (425856)Time elapsed: 0.006 s % 10.01/2.11 % (425856)Peak memory usage: 85 MB % 10.01/2.11 % (425856)Instructions burned: 12 (million) % 10.01/2.11 % (425850)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1143572407:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 10.01/2.11 % (425850)Instruction limit reached! % 10.01/2.11 % (425850)------------------------------ % 10.01/2.11 % (425850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.01/2.11 % (425850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.01/2.11 % (425850)CaDiCaL version: 2.1.3 % 10.01/2.11 % (425850)Termination reason: Instruction limit % 10.01/2.11 % (425850)Termination phase: Property scanning % 10.01/2.11 % (425850)Time elapsed: 0.002 s % 10.01/2.11 % (425850)Peak memory usage: 85 MB % 10.01/2.11 % (425850)Instructions burned: 2 (million) % 10.01/2.11 % (425855)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=106027382:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi) % 10.01/2.11 % (425865)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1637753310: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) % 10.01/2.11 % (425866)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2984163419:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi) % 10.01/2.11 % (425864)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3653952058:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi) % 10.01/2.11 % (425866)Instruction limit reached! % 10.01/2.11 % (425866)------------------------------ % 10.01/2.11 % (425866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.01/2.11 % (425866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.01/2.11 % (425866)CaDiCaL version: 2.1.3 % 10.01/2.11 % (425866)Termination reason: Instruction limit % 10.01/2.11 % (425866)Termination phase: Property scanning % 10.01/2.11 % (425866)Time elapsed: 0.002 s % 10.01/2.11 % (425866)Peak memory usage: 85 MB % 10.01/2.11 % (425866)Instructions burned: 2 (million) % 11.87/2.51 % (425865)Instruction limit reached! % 11.87/2.51 % (425865)------------------------------ % 11.87/2.51 % (425865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.87/2.51 % (425865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.51 % (425865)CaDiCaL version: 2.1.3 % 11.87/2.51 % (425865)Termination reason: Instruction limit % 11.87/2.51 % (425865)Termination phase: Property scanning % 11.87/2.51 % (425865)Time elapsed: 0.016 s % 11.87/2.51 % (425865)Peak memory usage: 86 MB % 11.87/2.51 % (425865)Instructions burned: 37 (million) % 11.87/2.51 % (425855)Instruction limit reached! % 11.87/2.51 % (425855)------------------------------ % 11.87/2.51 % (425855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.87/2.51 % (425855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.51 % (425855)CaDiCaL version: 2.1.3 % 11.87/2.51 % (425855)Termination reason: Instruction limit % 11.87/2.51 % (425855)Termination phase: Saturation % 11.87/2.51 % (425855)Time elapsed: 0.123 s % 11.87/2.51 % (425855)Peak memory usage: 113 MB % 11.87/2.51 % (425855)Instructions burned: 128 (million) % 11.87/2.51 % (425864)Instruction limit reached! % 11.87/2.51 % (425864)------------------------------ % 11.87/2.51 % (425864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.87/2.51 % (425864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.51 % (425864)CaDiCaL version: 2.1.3 % 11.87/2.51 % (425864)Termination reason: Instruction limit % 11.87/2.51 % (425864)Termination phase: Property scanning % 11.87/2.51 % (425864)Time elapsed: 0.021 s % 11.87/2.51 % (425864)Peak memory usage: 86 MB % 11.87/2.51 % (425864)Instructions burned: 27 (million) % 11.87/2.51 % (425872)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3399787443:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 11.87/2.51 % (425872)Refutation not found, incomplete strategy % 11.87/2.51 % (425872)------------------------------ % 11.87/2.51 % (425872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.87/2.51 % (425872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.51 % (425872)CaDiCaL version: 2.1.3 % 11.87/2.51 % (425872)Termination reason: Refutation not found, incomplete strategy % 11.87/2.51 % (425872)Time elapsed: 0.034 s % 11.87/2.51 % (425872)Peak memory usage: 89 MB % 11.87/2.51 % (425872)Instructions burned: 104 (million) % 11.87/2.51 % (425869)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1147126169:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 11.87/2.51 % (425869)Instruction limit reached! % 11.87/2.51 % (425869)------------------------------ % 11.87/2.51 % (425869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.87/2.51 % (425869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.51 % (425869)CaDiCaL version: 2.1.3 % 11.87/2.51 % (425869)Termination reason: Instruction limit % 11.87/2.51 % (425869)Termination phase: Property scanning % 11.87/2.51 % (425869)Time elapsed: 0.006 s % 11.87/2.51 % (425869)Peak memory usage: 85 MB % 11.87/2.51 % (425869)Instructions burned: 8 (million) % 11.87/2.51 % (425830)------------------------------ % 11.87/2.51 % (425830)------------------------------ % 11.87/2.51 % (425884)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1551267503:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi) % 11.87/2.51 % (425883)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1110352918:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 11.87/2.51 % (425886)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2892860237:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 11.87/2.51 % (425886)Instruction limit reached! % 11.87/2.51 % (425886)------------------------------ % 11.87/2.51 % (425886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.87/2.51 % (425886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.51 % (425886)CaDiCaL version: 2.1.3 % 11.87/2.51 % (425886)Termination reason: Instruction limit % 11.87/2.51 % (425886)Termination phase: Property scanning % 11.87/2.51 % (425886)Time elapsed: 0.009 s % 11.87/2.51 % (425886)Peak memory usage: 85 MB % 11.87/2.51 % (425886)Instructions burned: 11 (million) % 11.87/2.51 % (425883)Instruction limit reached! % 11.87/2.51 % (425883)------------------------------ % 13.47/2.81 % (425883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.47/2.81 % (425883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.47/2.81 % (425883)CaDiCaL version: 2.1.3 % 13.47/2.81 % (425883)Termination reason: Instruction limit % 13.47/2.81 % (425883)Termination phase: shuffling % 13.47/2.81 % (425883)Time elapsed: 0.010 s % 13.47/2.81 % (425883)Peak memory usage: 85 MB % 13.47/2.81 % (425883)Instructions burned: 15 (million) % 13.47/2.81 % (425893)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=3962379745:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi) % 13.47/2.81 % (425888)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4086414673:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi) % 13.47/2.81 % (425872)------------------------------ % 13.47/2.81 % (425872)------------------------------ % 13.47/2.81 % (425892)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=663898894:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 13.47/2.81 % (425884)Refutation not found, incomplete strategy % 13.47/2.81 % (425884)------------------------------ % 13.47/2.81 % (425884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.47/2.81 % (425884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.47/2.81 % (425884)CaDiCaL version: 2.1.3 % 13.47/2.81 % (425884)Termination reason: Refutation not found, incomplete strategy % 13.47/2.81 % (425884)Time elapsed: 0.074 s % 13.47/2.81 % (425884)Peak memory usage: 112 MB % 13.47/2.81 % (425884)Instructions burned: 66 (million) % 13.47/2.81 % (425888)Instruction limit reached! % 13.47/2.81 % (425888)------------------------------ % 13.47/2.81 % (425888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.47/2.81 % (425888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.47/2.81 % (425888)CaDiCaL version: 2.1.3 % 13.47/2.81 % (425888)Termination reason: Instruction limit % 13.47/2.81 % (425888)Termination phase: Saturation % 13.47/2.81 % (425888)Time elapsed: 0.075 s % 13.47/2.81 % (425888)Peak memory usage: 112 MB % 13.47/2.81 % (425888)Instructions burned: 71 (million) % 13.47/2.81 % (425892)Instruction limit reached! % 13.47/2.81 % (425892)------------------------------ % 13.47/2.81 % (425892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.47/2.81 % (425892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.47/2.81 % (425892)CaDiCaL version: 2.1.3 % 13.47/2.81 % (425892)Termination reason: Instruction limit % 13.47/2.81 % (425892)Termination phase: Saturation % 13.47/2.81 % (425892)Time elapsed: 0.047 s % 13.47/2.81 % (425892)Peak memory usage: 86 MB % 13.47/2.81 % (425892)Instructions burned: 76 (million) % 13.47/2.81 % (425893)Instruction limit reached! % 13.47/2.81 % (425893)------------------------------ % 13.47/2.81 % (425893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.47/2.81 % (425893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.47/2.81 % (425893)CaDiCaL version: 2.1.3 % 13.47/2.81 % (425893)Termination reason: Instruction limit % 13.47/2.81 % (425893)Termination phase: Saturation % 13.47/2.81 % (425893)Time elapsed: 0.149 s % 13.47/2.81 % (425893)Peak memory usage: 91 MB % 13.47/2.81 % (425893)Instructions burned: 295 (million) % 13.47/2.81 % (425903)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1396647688:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 13.47/2.81 % (425901)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2764334055:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 13.47/2.81 % (425909)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=737917992:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi) % 13.47/2.81 % (425903)Instruction limit reached! % 13.47/2.81 % (425903)------------------------------ % 13.47/2.81 % (425903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.47/2.81 % (425903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.47/2.81 % (425903)CaDiCaL version: 2.1.3 % 13.47/2.81 % (425903)Termination reason: Instruction limit % 13.47/2.81 % (425903)Termination phase: Saturation % 14.35/3.14 % (425903)Time elapsed: 0.099 s % 14.35/3.14 % (425903)Peak memory usage: 130 MB % 14.35/3.14 % (425903)Instructions burned: 133 (million) % 14.35/3.14 % (425909)Instruction limit reached! % 14.35/3.14 % (425909)------------------------------ % 14.35/3.14 % (425909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/3.14 % (425909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/3.14 % (425909)CaDiCaL version: 2.1.3 % 14.35/3.14 % (425909)Termination reason: Instruction limit % 14.35/3.14 % (425909)Termination phase: Property scanning % 14.35/3.14 % (425909)Time elapsed: 0.031 s % 14.35/3.14 % (425909)Peak memory usage: 86 MB % 14.35/3.14 % (425909)Instructions burned: 42 (million) % 14.35/3.14 % (425913)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2013983813:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi) % 14.35/3.14 % (425901)Instruction limit reached! % 14.35/3.14 % (425901)------------------------------ % 14.35/3.14 % (425901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/3.14 % (425901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/3.14 % (425901)CaDiCaL version: 2.1.3 % 14.35/3.14 % (425901)Termination reason: Instruction limit % 14.35/3.14 % (425901)Termination phase: Property scanning % 14.35/3.14 % (425901)Time elapsed: 0.096 s % 14.35/3.14 % (425901)Peak memory usage: 88 MB % 14.35/3.14 % (425901)Instructions burned: 131 (million) % 14.35/3.14 % (425912)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1096096075:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi) % 14.35/3.14 % (425917)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3613637321:i=131:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 14.35/3.14 % (425912)Refutation not found, incomplete strategy % 14.35/3.14 % (425912)------------------------------ % 14.35/3.14 % (425912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/3.14 % (425912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/3.14 % (425912)CaDiCaL version: 2.1.3 % 14.35/3.14 % (425912)Termination reason: Refutation not found, incomplete strategy % 14.35/3.14 % (425912)Time elapsed: 0.100 s % 14.35/3.14 % (425912)Peak memory usage: 89 MB % 14.35/3.14 % (425912)Instructions burned: 138 (million) % 14.35/3.14 % (425923)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=421405141:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2985 on theBenchmark for (2985ds/259Mi) % 14.35/3.14 % (425884)------------------------------ % 14.35/3.14 % (425884)------------------------------ % 14.35/3.14 % (425927)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=734881726:i=383:fsr=off:rtra=on:ev=force_2985 on theBenchmark for (2985ds/383Mi) % 14.35/3.14 % (425923)Refutation not found, incomplete strategy % 14.35/3.14 % (425923)------------------------------ % 14.35/3.14 % (425923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/3.14 % (425923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/3.14 % (425923)CaDiCaL version: 2.1.3 % 14.35/3.14 % (425923)Termination reason: Refutation not found, incomplete strategy % 14.35/3.14 % (425923)Time elapsed: 0.039 s % 14.35/3.14 % (425923)Peak memory usage: 112 MB % 14.35/3.14 % (425923)Instructions burned: 69 (million) % 14.35/3.14 % (425917)Instruction limit reached! % 14.35/3.14 % (425917)------------------------------ % 14.35/3.14 % (425917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.35/3.14 % (425917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.35/3.14 % (425917)CaDiCaL version: 2.1.3 % 14.35/3.14 % (425917)Termination reason: Instruction limit % 14.35/3.14 % (425917)Termination phase: Saturation % 14.35/3.14 % (425917)Time elapsed: 0.127 s % 14.35/3.14 % (425917)Peak memory usage: 113 MB % 14.35/3.14 % (425917)Instructions burned: 131 (million) % 14.35/3.14 % (425925)dis+10_1_si=on:random_seed=3565258365:s2a=on:i=1000:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/1000Mi) % 14.35/3.14 % (425923)------------------------------ % 14.35/3.14 % (425923)------------------------------ % 14.35/3.14 % (425934)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2064963085:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi) % 14.35/3.14 % (425936)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1690777423:i=65:nm=16:rtra=on_2983 on theBenchmark for (2983ds/65Mi) % 18.76/3.48 % (425927)Instruction limit reached! % 18.76/3.48 % (425927)------------------------------ % 18.76/3.48 % (425927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.76/3.48 % (425927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/3.48 % (425927)CaDiCaL version: 2.1.3 % 18.76/3.48 % (425927)Termination reason: Instruction limit % 18.76/3.48 % (425927)Termination phase: Saturation % 18.76/3.48 % (425927)Time elapsed: 0.243 s % 18.76/3.48 % (425927)Peak memory usage: 91 MB % 18.76/3.48 % (425927)Instructions burned: 384 (million) % 18.76/3.48 % (425936)Instruction limit reached! % 18.76/3.48 % (425936)------------------------------ % 18.76/3.48 % (425936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.76/3.48 % (425936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/3.48 % (425936)CaDiCaL version: 2.1.3 % 18.76/3.48 % (425936)Termination reason: Instruction limit % 18.76/3.48 % (425936)Termination phase: Saturation % 18.76/3.48 % (425936)Time elapsed: 0.042 s % 18.76/3.48 % (425936)Peak memory usage: 88 MB % 18.76/3.48 % (425936)Instructions burned: 65 (million) % 18.76/3.48 % (425945)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3704358873:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi) % 18.76/3.48 % (425934)Instruction limit reached! % 18.76/3.48 % (425934)------------------------------ % 18.76/3.48 % (425934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.76/3.48 % (425934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/3.48 % (425934)CaDiCaL version: 2.1.3 % 18.76/3.48 % (425934)Termination reason: Instruction limit % 18.76/3.48 % (425934)Termination phase: Saturation % 18.76/3.48 % (425934)Time elapsed: 0.104 s % 18.76/3.48 % (425934)Peak memory usage: 89 MB % 18.76/3.48 % (425934)Instructions burned: 142 (million) % 18.76/3.48 % (425945)Instruction limit reached! % 18.76/3.48 % (425945)------------------------------ % 18.76/3.48 % (425945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.76/3.48 % (425945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/3.48 % (425945)CaDiCaL version: 2.1.3 % 18.76/3.48 % (425945)Termination reason: Instruction limit % 18.76/3.48 % (425945)Termination phase: Saturation % 18.76/3.48 % (425945)Time elapsed: 0.028 s % 18.76/3.48 % (425945)Peak memory usage: 90 MB % 18.76/3.48 % (425945)Instructions burned: 122 (million) % 18.76/3.48 % (425912)------------------------------ % 18.76/3.48 % (425912)------------------------------ % 18.76/3.48 % (425913)Instruction limit reached! % 18.76/3.48 % (425913)------------------------------ % 18.76/3.48 % (425913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.76/3.48 % (425913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/3.48 % (425913)CaDiCaL version: 2.1.3 % 18.76/3.48 % (425913)Termination reason: Instruction limit % 18.76/3.48 % (425913)Termination phase: Saturation % 18.76/3.48 % (425913)Time elapsed: 0.509 s % 18.76/3.48 % (425913)Peak memory usage: 138 MB % 18.76/3.48 % (425913)Instructions burned: 598 (million) % 18.76/3.48 % (425955)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=295055221:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/329Mi) % 18.76/3.48 % (425948)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=3218117018:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi) % 18.76/3.48 % (425949)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=2830990334:i=39:ins=3:rtra=on_2980 on theBenchmark for (2980ds/39Mi) % 18.76/3.48 % (425949)Instruction limit reached! % 18.76/3.48 % (425949)------------------------------ % 18.76/3.48 % (425949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.76/3.48 % (425949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/3.48 % (425949)CaDiCaL version: 2.1.3 % 18.76/3.48 % (425949)Termination reason: Instruction limit % 18.76/3.48 % (425949)Termination phase: Property scanning % 18.76/3.48 % (425949)Time elapsed: 0.017 s % 18.76/3.48 % (425949)Peak memory usage: 86 MB % 18.76/3.48 % (425949)Instructions burned: 42 (million) % 18.76/3.48 % (425953)dis+1010_1_to=kbo:si=on:random_seed=3058620922:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2980 on theBenchmark for (2980ds/175Mi) % 21.88/3.95 % (425948)Instruction limit reached! % 21.88/3.95 % (425948)------------------------------ % 21.88/3.95 % (425948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.88/3.95 % (425948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.95 % (425948)CaDiCaL version: 2.1.3 % 21.88/3.95 % (425948)Termination reason: Instruction limit % 21.88/3.95 % (425948)Termination phase: Saturation % 21.88/3.95 % (425948)Time elapsed: 0.098 s % 21.88/3.95 % (425948)Peak memory usage: 90 MB % 21.88/3.95 % (425948)Instructions burned: 128 (million) % 21.88/3.95 % (425958)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1857792310:s2a=on:i=483:doe=on:nm=32:rtra=on_2980 on theBenchmark for (2980ds/483Mi) % 21.88/3.95 % (425955)Instruction limit reached! % 21.88/3.95 % (425955)------------------------------ % 21.88/3.95 % (425955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.88/3.95 % (425955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.95 % (425955)CaDiCaL version: 2.1.3 % 21.88/3.95 % (425955)Termination reason: Instruction limit % 21.88/3.95 % (425955)Termination phase: Saturation % 21.88/3.95 % (425955)Time elapsed: 0.127 s % 21.88/3.95 % (425955)Peak memory usage: 118 MB % 21.88/3.95 % (425955)Instructions burned: 330 (million) % 21.88/3.95 % (425959)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=495029034:thitd=on:i=215:nm=0:rtra=on:ev=force_2980 on theBenchmark for (2980ds/215Mi) % 21.88/3.95 % (425966)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3898601252:i=349:rtra=on_2978 on theBenchmark for (2978ds/349Mi) % 21.88/3.95 % (425953)Instruction limit reached! % 21.88/3.95 % (425953)------------------------------ % 21.88/3.95 % (425953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.88/3.95 % (425953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.95 % (425953)CaDiCaL version: 2.1.3 % 21.88/3.95 % (425953)Termination reason: Instruction limit % 21.88/3.95 % (425953)Termination phase: Saturation % 21.88/3.95 % (425953)Time elapsed: 0.126 s % 21.88/3.95 % (425953)Peak memory usage: 91 MB % 21.88/3.95 % (425953)Instructions burned: 175 (million) % 21.88/3.95 % (425973)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2029307995:i=328:kws=inv_frequency:nm=20:rtra=on_2977 on theBenchmark for (2977ds/328Mi) % 21.88/3.95 % (425959)Instruction limit reached! % 21.88/3.95 % (425959)------------------------------ % 21.88/3.95 % (425959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.88/3.95 % (425959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.95 % (425959)CaDiCaL version: 2.1.3 % 21.88/3.95 % (425959)Termination reason: Instruction limit % 21.88/3.95 % (425959)Termination phase: Saturation % 21.88/3.95 % (425959)Time elapsed: 0.190 s % 21.88/3.95 % (425959)Peak memory usage: 131 MB % 21.88/3.95 % (425959)Instructions burned: 216 (million) % 21.88/3.95 % (425925)Instruction limit reached! % 21.88/3.95 % (425925)------------------------------ % 21.88/3.95 % (425925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.88/3.95 % (425925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.95 % (425925)CaDiCaL version: 2.1.3 % 21.88/3.95 % (425925)Termination reason: Instruction limit % 21.88/3.95 % (425925)Termination phase: Saturation % 21.88/3.95 % (425925)Time elapsed: 0.723 s % 21.88/3.95 % (425925)Peak memory usage: 92 MB % 21.88/3.95 % (425925)Instructions burned: 1000 (million) % 21.88/3.95 % (425971)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2991517045:st=2:i=295:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/295Mi) % 21.88/3.95 % (425971)Refutation not found, incomplete strategy % 21.88/3.95 % (425971)------------------------------ % 21.88/3.95 % (425971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.88/3.95 % (425971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.88/3.95 % (425971)CaDiCaL version: 2.1.3 % 21.88/3.95 % (425971)Termination reason: Refutation not found, incomplete strategy % 21.88/3.95 % (425971)Time elapsed: 0.044 s % 21.88/3.95 % (425971)Peak memory usage: 88 MB % 21.88/3.95 % (425971)Instructions burned: 63 (million) % 21.88/3.95 % (425979)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1126779880:i=281:gtgl=2:rtra=on:gtg=all_2977 on theBenchmark for (2977ds/281Mi) % 25.02/4.29 % (425966)Instruction limit reached! % 25.02/4.29 % (425966)------------------------------ % 25.02/4.29 % (425966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425966)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425966)Termination reason: Instruction limit % 25.02/4.29 % (425966)Termination phase: Saturation % 25.02/4.29 % (425966)Time elapsed: 0.253 s % 25.02/4.29 % (425966)Peak memory usage: 117 MB % 25.02/4.29 % (425966)Instructions burned: 349 (million) % 25.02/4.29 % (425981)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1980831389:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/484Mi) % 25.02/4.29 % (425981)Refutation not found, incomplete strategy % 25.02/4.29 % (425981)------------------------------ % 25.02/4.29 % (425981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425981)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425981)Termination reason: Refutation not found, incomplete strategy % 25.02/4.29 % (425981)Time elapsed: 0.012 s % 25.02/4.29 % (425981)Peak memory usage: 88 MB % 25.02/4.29 % (425981)Instructions burned: 61 (million) % 25.02/4.29 % (425958)Instruction limit reached! % 25.02/4.29 % (425958)------------------------------ % 25.02/4.29 % (425958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425958)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425958)Termination reason: Instruction limit % 25.02/4.29 % (425958)Termination phase: Saturation % 25.02/4.29 % (425958)Time elapsed: 0.417 s % 25.02/4.29 % (425958)Peak memory usage: 137 MB % 25.02/4.29 % (425958)Instructions burned: 484 (million) % 25.02/4.29 % (425973)Instruction limit reached! % 25.02/4.29 % (425973)------------------------------ % 25.02/4.29 % (425973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425973)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425973)Termination reason: Instruction limit % 25.02/4.29 % (425973)Termination phase: Saturation % 25.02/4.29 % (425973)Time elapsed: 0.251 s % 25.02/4.29 % (425973)Peak memory usage: 115 MB % 25.02/4.29 % (425973)Instructions burned: 329 (million) % 25.02/4.29 % (425984)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3151115415:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2975 on theBenchmark for (2975ds/321Mi) % 25.02/4.29 % (425979)Instruction limit reached! % 25.02/4.29 % (425979)------------------------------ % 25.02/4.29 % (425979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425979)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425979)Termination reason: Instruction limit % 25.02/4.29 % (425979)Termination phase: Saturation % 25.02/4.29 % (425979)Time elapsed: 0.224 s % 25.02/4.29 % (425979)Peak memory usage: 113 MB % 25.02/4.29 % (425979)Instructions burned: 283 (million) % 25.02/4.29 % (425984)Refutation not found, incomplete strategy % 25.02/4.29 % (425984)------------------------------ % 25.02/4.29 % (425984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425984)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425984)Termination reason: Refutation not found, incomplete strategy % 25.02/4.29 % (425984)Time elapsed: 0.068 s % 25.02/4.29 % (425984)Peak memory usage: 112 MB % 25.02/4.29 % (425984)Instructions burned: 66 (million) % 25.02/4.29 % (425992)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3860899927:i=416:rtra=on:gtg=position:ss=axioms_2974 on theBenchmark for (2974ds/416Mi) % 25.02/4.29 % (425981)------------------------------ % 25.02/4.29 % (425981)------------------------------ % 25.02/4.29 % (425992)Refutation not found, incomplete strategy % 25.02/4.29 % (425992)------------------------------ % 25.02/4.29 % (425992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.02/4.29 % (425992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/4.29 % (425992)CaDiCaL version: 2.1.3 % 25.02/4.29 % (425992)Termination reason: Refutation not found, incomplete strategy % 26.40/4.73 % (425992)Time elapsed: 0.075 s % 26.40/4.73 % (425992)Peak memory usage: 112 MB % 26.40/4.73 % (425992)Instructions burned: 65 (million) % 26.40/4.73 % (425994)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=3166687749:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi) % 26.40/4.73 % (425971)------------------------------ % 26.40/4.73 % (425971)------------------------------ % 26.40/4.73 % (425993)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2425046529:i=471:thf=on:kws=precedence:rtra=on_2973 on theBenchmark for (2973ds/471Mi) % 26.40/4.73 % (426000)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1896878970:i=375:kws=inv_arity_squared:rtra=on_2972 on theBenchmark for (2972ds/375Mi) % 26.40/4.73 % (426003)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=895367499:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/387Mi) % 26.40/4.73 % (426003)Refutation not found, incomplete strategy % 26.40/4.73 % (426003)------------------------------ % 26.40/4.73 % (426003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.40/4.73 % (426003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.40/4.73 % (426003)CaDiCaL version: 2.1.3 % 26.40/4.73 % (426003)Termination reason: Refutation not found, incomplete strategy % 26.40/4.73 % (426003)Time elapsed: 0.031 s % 26.40/4.73 % (426003)Peak memory usage: 112 MB % 26.40/4.73 % (426003)Instructions burned: 70 (million) % 26.40/4.73 % (425994)Instruction limit reached! % 26.40/4.73 % (425994)------------------------------ % 26.40/4.73 % (425994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.40/4.73 % (425994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.40/4.73 % (425994)CaDiCaL version: 2.1.3 % 26.40/4.73 % (425994)Termination reason: Instruction limit % 26.40/4.73 % (425994)Termination phase: Saturation % 26.40/4.73 % (425994)Time elapsed: 0.238 s % 26.40/4.73 % (425994)Peak memory usage: 131 MB % 26.40/4.73 % (425994)Instructions burned: 276 (million) % 26.40/4.73 % (426007)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2336203975:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2971 on theBenchmark for (2971ds/513Mi) % 26.40/4.73 % (425984)------------------------------ % 26.40/4.73 % (425984)------------------------------ % 26.40/4.73 % (426003)------------------------------ % 26.40/4.73 % (426003)------------------------------ % 26.40/4.73 % (426000)Instruction limit reached! % 26.40/4.73 % (426000)------------------------------ % 26.40/4.73 % (426000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.40/4.73 % (426000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.40/4.73 % (426000)CaDiCaL version: 2.1.3 % 26.40/4.73 % (426000)Termination reason: Instruction limit % 26.40/4.73 % (426000)Termination phase: Saturation % 26.40/4.73 % (426000)Time elapsed: 0.306 s % 26.40/4.73 % (426000)Peak memory usage: 117 MB % 26.40/4.73 % (426000)Instructions burned: 375 (million) % 26.40/4.73 % (425992)------------------------------ % 26.40/4.73 % (425992)------------------------------ % 26.40/4.73 % (425993)Instruction limit reached! % 26.40/4.73 % (425993)------------------------------ % 26.40/4.73 % (425993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.40/4.73 % (425993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.40/4.73 % (425993)CaDiCaL version: 2.1.3 % 26.40/4.73 % (425993)Termination reason: Instruction limit % 26.40/4.73 % (425993)Termination phase: Saturation % 26.40/4.73 % (425993)Time elapsed: 0.355 s % 26.40/4.73 % (425993)Peak memory usage: 113 MB % 26.40/4.73 % (425993)Instructions burned: 471 (million) % 26.40/4.73 % (426020)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2109780432:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2968 on theBenchmark for (2968ds/341Mi) % 26.40/4.73 % (426017)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3305796100:i=334:rtra=on_2969 on theBenchmark for (2969ds/334Mi) % 26.40/4.73 % (426018)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=139758535:i=359:rtra=on:gtg=exists_top:ss=axioms_2969 on theBenchmark for (2969ds/359Mi) % 32.20/5.26 % (426018)Refutation not found, incomplete strategy % 32.20/5.26 % (426018)------------------------------ % 32.20/5.26 % (426018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.20/5.26 % (426018)CaDiCaL version: 2.1.3 % 32.20/5.26 % (426018)Termination reason: Refutation not found, incomplete strategy % 32.20/5.26 % (426018)Time elapsed: 0.056 s % 32.20/5.26 % (426018)Peak memory usage: 89 MB % 32.20/5.26 % (426018)Instructions burned: 76 (million) % 32.20/5.26 % (426021)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3324548601:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/261Mi) % 32.20/5.26 % (426022)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=3002094730:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2968 on theBenchmark for (2968ds/235Mi) % 32.20/5.26 % (426025)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3737070643:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2968 on theBenchmark for (2968ds/273Mi) % 32.20/5.26 % (426020)Instruction limit reached! % 32.20/5.26 % (426020)------------------------------ % 32.20/5.26 % (426020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.20/5.26 % (426020)CaDiCaL version: 2.1.3 % 32.20/5.26 % (426020)Termination reason: Instruction limit % 32.20/5.26 % (426020)Termination phase: Saturation % 32.20/5.26 % (426020)Time elapsed: 0.149 s % 32.20/5.26 % (426020)Peak memory usage: 118 MB % 32.20/5.26 % (426020)Instructions burned: 342 (million) % 32.20/5.26 % (426021)Refutation not found, incomplete strategy % 32.20/5.26 % (426021)------------------------------ % 32.20/5.26 % (426021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.20/5.26 % (426021)CaDiCaL version: 2.1.3 % 32.20/5.26 % (426021)Termination reason: Refutation not found, incomplete strategy % 32.20/5.26 % (426021)Time elapsed: 0.065 s % 32.20/5.26 % (426021)Peak memory usage: 112 MB % 32.20/5.26 % (426021)Instructions burned: 60 (million) % 32.20/5.26 % (426007)Instruction limit reached! % 32.20/5.26 % (426007)------------------------------ % 32.20/5.26 % (426007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.20/5.26 % (426007)CaDiCaL version: 2.1.3 % 32.20/5.26 % (426007)Termination reason: Instruction limit % 32.20/5.26 % (426007)Termination phase: Saturation % 32.20/5.26 % (426007)Time elapsed: 0.369 s % 32.20/5.26 % (426007)Peak memory usage: 90 MB % 32.20/5.26 % (426007)Instructions burned: 513 (million) % 32.20/5.26 % (426022)Refutation not found, incomplete strategy % 32.20/5.26 % (426022)------------------------------ % 32.20/5.26 % (426022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.20/5.26 % (426022)CaDiCaL version: 2.1.3 % 32.20/5.26 % (426022)Termination reason: Refutation not found, incomplete strategy % 32.20/5.26 % (426022)Time elapsed: 0.080 s % 32.20/5.26 % (426022)Peak memory usage: 112 MB % 32.20/5.26 % (426022)Instructions burned: 68 (million) % 32.20/5.26 % (426017)Instruction limit reached! % 32.20/5.26 % (426017)------------------------------ % 32.20/5.26 % (426017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.20/5.26 % (426017)CaDiCaL version: 2.1.3 % 32.20/5.26 % (426017)Termination reason: Instruction limit % 32.20/5.26 % (426017)Termination phase: Saturation % 32.20/5.26 % (426017)Time elapsed: 0.275 s % 32.20/5.26 % (426017)Peak memory usage: 134 MB % 32.20/5.26 % (426017)Instructions burned: 334 (million) % 32.20/5.26 % (426039)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2377544839:i=146:doe=on:rtra=on_2965 on theBenchmark for (2965ds/146Mi) % 32.20/5.26 % (426025)Instruction limit reached! % 32.20/5.26 % (426025)------------------------------ % 32.20/5.26 % (426025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.20/5.26 % (426025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.04/5.95 % (426025)CaDiCaL version: 2.1.3 % 35.04/5.95 % (426025)Termination reason: Instruction limit % 35.04/5.95 % (426025)Termination phase: Saturation % 35.04/5.95 % (426025)Time elapsed: 0.210 s % 35.04/5.95 % (426025)Peak memory usage: 91 MB % 35.04/5.95 % (426025)Instructions burned: 273 (million) % 35.04/5.95 % (426039)Instruction limit reached! % 35.04/5.95 % (426039)------------------------------ % 35.04/5.95 % (426039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.04/5.95 % (426039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.04/5.95 % (426039)CaDiCaL version: 2.1.3 % 35.04/5.95 % (426039)Termination reason: Instruction limit % 35.04/5.95 % (426039)Termination phase: Saturation % 35.04/5.95 % (426039)Time elapsed: 0.048 s % 35.04/5.95 % (426039)Peak memory usage: 90 MB % 35.04/5.95 % (426039)Instructions burned: 152 (million) % 35.04/5.95 % (426040)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1295143944:i=4428:doe=on:fsr=off:rtra=on_2965 on theBenchmark for (2965ds/4428Mi) % 35.04/5.95 % (426018)------------------------------ % 35.04/5.95 % (426018)------------------------------ % 35.04/5.95 % (426044)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=343974907:avsq=on:i=276:avsqr=1,2:rtra=on_2964 on theBenchmark for (2964ds/276Mi) % 35.04/5.95 % (426022)------------------------------ % 35.04/5.95 % (426022)------------------------------ % 35.04/5.95 % (426048)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1994001739:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2963 on theBenchmark for (2963ds/655Mi) % 35.04/5.95 % (426021)------------------------------ % 35.04/5.95 % (426021)------------------------------ % 35.04/5.95 % (426047)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3181812575:i=1052:rtra=on_2963 on theBenchmark for (2963ds/1052Mi) % 35.04/5.95 % (426059)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=704371412:i=107:rtra=on_2962 on theBenchmark for (2962ds/107Mi) % 35.04/5.95 % (426051)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3709079896:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2962 on theBenchmark for (2962ds/1054Mi) % 35.04/5.95 % (426044)Instruction limit reached! % 35.04/5.95 % (426044)------------------------------ % 35.04/5.95 % (426044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.04/5.95 % (426044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.04/5.95 % (426044)CaDiCaL version: 2.1.3 % 35.04/5.95 % (426044)Termination reason: Instruction limit % 35.04/5.95 % (426044)Termination phase: Saturation % 35.04/5.95 % (426044)Time elapsed: 0.223 s % 35.04/5.95 % (426044)Peak memory usage: 131 MB % 35.04/5.95 % (426044)Instructions burned: 276 (million) % 35.04/5.95 % (426051)Refutation not found, incomplete strategy % 35.04/5.95 % (426051)------------------------------ % 35.04/5.95 % (426051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.04/5.95 % (426051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.04/5.95 % (426051)CaDiCaL version: 2.1.3 % 35.04/5.95 % (426051)Termination reason: Refutation not found, incomplete strategy % 35.04/5.95 % (426051)Time elapsed: 0.032 s % 35.04/5.95 % (426051)Peak memory usage: 88 MB % 35.04/5.95 % (426051)Instructions burned: 48 (million) % 35.04/5.95 % (426059)Instruction limit reached! % 35.04/5.95 % (426059)------------------------------ % 35.04/5.95 % (426059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.04/5.95 % (426059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.04/5.95 % (426059)CaDiCaL version: 2.1.3 % 35.04/5.95 % (426059)Termination reason: Instruction limit % 35.04/5.95 % (426059)Termination phase: Saturation % 35.04/5.95 % (426059)Time elapsed: 0.052 s % 35.04/5.95 % (426059)Peak memory usage: 89 MB % 35.04/5.95 % (426059)Instructions burned: 107 (million) % 35.04/5.95 % (426060)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2148946711:s2a=on:i=450:doe=on:nm=32:rtra=on_2961 on theBenchmark for (2961ds/450Mi) % 35.04/5.95 % (426048)Instruction limit reached! % 35.04/5.95 % (426048)------------------------------ % 35.04/5.95 % (426048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.04/5.95 % (426048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.64/6.59 % (426048)CaDiCaL version: 2.1.3 % 40.64/6.59 % (426048)Termination reason: Instruction limit % 40.64/6.59 % (426048)Termination phase: Saturation % 40.64/6.59 % (426048)Time elapsed: 0.288 s % 40.64/6.59 % (426048)Peak memory usage: 101 MB % 40.64/6.59 % (426048)Instructions burned: 657 (million) % 40.64/6.59 % (426068)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 % 40.64/6.59 % (426068)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=955277967:i=1090:aac=none:nm=0:rtra=on:rawr=on_2960 on theBenchmark for (2960ds/1090Mi) % 40.64/6.59 % (426069)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1339700503:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2960 on theBenchmark for (2960ds/130Mi) % 40.64/6.59 % (426072)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2832512230:i=312:kws=inv_frequency:nm=20:rtra=on_2959 on theBenchmark for (2959ds/312Mi) % 40.64/6.59 % (426069)Instruction limit reached! % 40.64/6.59 % (426069)------------------------------ % 40.64/6.59 % (426069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.64/6.59 % (426069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.64/6.59 % (426069)CaDiCaL version: 2.1.3 % 40.64/6.59 % (426069)Termination reason: Instruction limit % 40.64/6.59 % (426069)Termination phase: Property scanning % 40.64/6.59 % (426069)Time elapsed: 0.094 s % 40.64/6.59 % (426069)Peak memory usage: 88 MB % 40.64/6.59 % (426069)Instructions burned: 130 (million) % 40.64/6.59 % (426051)------------------------------ % 40.64/6.59 % (426051)------------------------------ % 40.64/6.59 % (426047)Instruction limit reached! % 40.64/6.59 % (426047)------------------------------ % 40.64/6.59 % (426047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.64/6.59 % (426047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.64/6.59 % (426047)CaDiCaL version: 2.1.3 % 40.64/6.59 % (426047)Termination reason: Instruction limit % 40.64/6.59 % (426047)Termination phase: Saturation % 40.64/6.59 % (426047)Time elapsed: 0.523 s % 40.64/6.59 % (426047)Peak memory usage: 91 MB % 40.64/6.59 % (426047)Instructions burned: 1053 (million) % 40.64/6.59 % (426072)Instruction limit reached! % 40.64/6.59 % (426072)------------------------------ % 40.64/6.59 % (426072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.64/6.59 % (426072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.64/6.59 % (426072)CaDiCaL version: 2.1.3 % 40.64/6.59 % (426072)Termination reason: Instruction limit % 40.64/6.59 % (426072)Termination phase: Saturation % 40.64/6.59 % (426072)Time elapsed: 0.134 s % 40.64/6.59 % (426072)Peak memory usage: 113 MB % 40.64/6.59 % (426072)Instructions burned: 313 (million) % 40.64/6.59 % (426060)Instruction limit reached! % 40.64/6.59 % (426060)------------------------------ % 40.64/6.59 % (426060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.64/6.59 % (426060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.64/6.59 % (426060)CaDiCaL version: 2.1.3 % 40.64/6.59 % (426060)Termination reason: Instruction limit % 40.64/6.59 % (426060)Termination phase: Saturation % 40.64/6.59 % (426060)Time elapsed: 0.398 s % 40.64/6.59 % (426060)Peak memory usage: 135 MB % 40.64/6.59 % (426060)Instructions burned: 451 (million) % 40.64/6.59 % (426080)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3147030473:i=491:doe=on:rtra=on:gtg=position_2957 on theBenchmark for (2957ds/491Mi) % 40.64/6.59 % (426084)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=882992172:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2956 on theBenchmark for (2956ds/307Mi) % 40.64/6.59 % (426087)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2708572725:i=776:doe=on:rtra=on_2956 on theBenchmark for (2956ds/776Mi) % 40.64/6.59 % (426083)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2683144997:s2a=on:i=835:s2at=2:rtra=on_2956 on theBenchmark for (2956ds/835Mi) % 40.64/6.59 % (426084)Refutation not found, incomplete strategy % 40.64/6.59 % (426084)------------------------------ % 40.64/6.59 % (426084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.64/6.59 % (426084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.68/7.39 % (426084)CaDiCaL version: 2.1.3 % 46.68/7.39 % (426084)Termination reason: Refutation not found, incomplete strategy % 46.68/7.39 % (426084)Time elapsed: 0.084 s % 46.68/7.39 % (426084)Peak memory usage: 96 MB % 46.68/7.39 % (426084)Instructions burned: 242 (million) % 46.68/7.39 % (426080)Refutation not found, incomplete strategy % 46.68/7.39 % (426080)------------------------------ % 46.68/7.39 % (426080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.68/7.39 % (426080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.68/7.39 % (426080)CaDiCaL version: 2.1.3 % 46.68/7.39 % (426080)Termination reason: Refutation not found, incomplete strategy % 46.68/7.39 % (426080)Time elapsed: 0.110 s % 46.68/7.39 % (426080)Peak memory usage: 91 MB % 46.68/7.39 % (426080)Instructions burned: 176 (million) % 46.68/7.39 % (426088)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1466985779:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/646Mi) % 46.68/7.39 % (426084)------------------------------ % 46.68/7.39 % (426084)------------------------------ % 46.68/7.39 % (426068)Instruction limit reached! % 46.68/7.39 % (426068)------------------------------ % 46.68/7.39 % (426068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.68/7.39 % (426068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.68/7.39 % (426068)CaDiCaL version: 2.1.3 % 46.68/7.39 % (426068)Termination reason: Instruction limit % 46.68/7.39 % (426068)Termination phase: Saturation % 46.68/7.39 % (426068)Time elapsed: 0.779 s % 46.68/7.39 % (426068)Peak memory usage: 120 MB % 46.68/7.39 % (426068)Instructions burned: 1091 (million) % 46.68/7.39 % (426100)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=2584464083:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2951 on theBenchmark for (2951ds/784Mi) % 46.68/7.39 % (426080)------------------------------ % 46.68/7.39 % (426080)------------------------------ % 46.68/7.39 % (426087)Instruction limit reached! % 46.68/7.39 % (426087)------------------------------ % 46.68/7.39 % (426087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.68/7.39 % (426087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.68/7.39 % (426087)CaDiCaL version: 2.1.3 % 46.68/7.39 % (426087)Termination reason: Instruction limit % 46.68/7.39 % (426087)Termination phase: Saturation % 46.68/7.39 % (426087)Time elapsed: 0.565 s % 46.68/7.39 % (426087)Peak memory usage: 114 MB % 46.68/7.39 % (426087)Instructions burned: 776 (million) % 46.68/7.39 % (426083)Instruction limit reached! % 46.68/7.39 % (426083)------------------------------ % 46.68/7.39 % (426083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.68/7.39 % (426083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.68/7.39 % (426083)CaDiCaL version: 2.1.3 % 46.68/7.39 % (426083)Termination reason: Instruction limit % 46.68/7.39 % (426083)Termination phase: Saturation % 46.68/7.39 % (426083)Time elapsed: 0.553 s % 46.68/7.39 % (426083)Peak memory usage: 90 MB % 46.68/7.39 % (426083)Instructions burned: 835 (million) % 46.68/7.39 % (426103)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=2910534169:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2950 on theBenchmark for (2950ds/1131Mi) % 46.68/7.39 % (426105)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=1441810958:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2949 on theBenchmark for (2949ds/246Mi) % 46.68/7.39 % (426088)Instruction limit reached! % 46.68/7.39 % (426088)------------------------------ % 46.68/7.39 % (426088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.68/7.39 % (426088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.68/7.39 % (426088)CaDiCaL version: 2.1.3 % 46.68/7.39 % (426088)Termination reason: Instruction limit % 46.68/7.39 % (426088)Termination phase: Saturation % 46.68/7.39 % (426088)Time elapsed: 0.565 s % 46.68/7.39 % (426088)Peak memory usage: 138 MB % 46.68/7.39 % (426088)Instructions burned: 647 (million) % 46.68/7.39 % (426105)Refutation not found, incomplete strategy % 46.68/7.39 % (426105)------------------------------ % 46.68/7.39 % (426105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.68/7.39 % (426105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.80/8.83 % (426105)CaDiCaL version: 2.1.3 % 56.80/8.83 % (426105)Termination reason: Refutation not found, incomplete strategy % 56.80/8.83 % (426105)Time elapsed: 0.062 s % 56.80/8.83 % (426105)Peak memory usage: 112 MB % 56.80/8.83 % (426105)Instructions burned: 69 (million) % 56.80/8.83 % (426100)Instruction limit reached! % 56.80/8.83 % (426100)------------------------------ % 56.80/8.83 % (426100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.80/8.83 % (426100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.80/8.83 % (426100)CaDiCaL version: 2.1.3 % 56.80/8.83 % (426100)Termination reason: Instruction limit % 56.80/8.83 % (426100)Termination phase: Saturation % 56.80/8.83 % (426100)Time elapsed: 0.305 s % 56.80/8.83 % (426100)Peak memory usage: 113 MB % 56.80/8.83 % (426100)Instructions burned: 786 (million) % 56.80/8.83 % (426108)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2528865699:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2948 on theBenchmark for (2948ds/775Mi) % 56.80/8.83 % (426109)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1545409914:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2948 on theBenchmark for (2948ds/273Mi) % 56.80/8.83 % (426108)Refutation not found, incomplete strategy % 56.80/8.83 % (426108)------------------------------ % 56.80/8.83 % (426108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.80/8.83 % (426108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.80/8.83 % (426108)CaDiCaL version: 2.1.3 % 56.80/8.83 % (426108)Termination reason: Refutation not found, incomplete strategy % 56.80/8.83 % (426108)Time elapsed: 0.045 s % 56.80/8.83 % (426108)Peak memory usage: 88 MB % 56.80/8.83 % (426108)Instructions burned: 66 (million) % 56.80/8.83 % (426116)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2323268131:i=102:nm=16:rtra=on_2947 on theBenchmark for (2947ds/102Mi) % 56.80/8.83 % (426116)Instruction limit reached! % 56.80/8.83 % (426116)------------------------------ % 56.80/8.83 % (426116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.80/8.83 % (426116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.80/8.83 % (426116)CaDiCaL version: 2.1.3 % 56.80/8.83 % (426116)Termination reason: Instruction limit % 56.80/8.83 % (426116)Termination phase: Saturation % 56.80/8.83 % (426116)Time elapsed: 0.022 s % 56.80/8.83 % (426116)Peak memory usage: 88 MB % 56.80/8.83 % (426116)Instructions burned: 104 (million) % 56.80/8.83 % (426117)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2601712158:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2946 on theBenchmark for (2946ds/1094Mi) % 56.80/8.83 % (426124)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1490090236:i=6400:doe=on:fsr=off:rtra=on_2945 on theBenchmark for (2945ds/6400Mi) % 56.80/8.83 % (426109)Instruction limit reached! % 56.80/8.83 % (426109)------------------------------ % 56.80/8.83 % (426109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.80/8.83 % (426109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.80/8.83 % (426109)CaDiCaL version: 2.1.3 % 56.80/8.83 % (426109)Termination reason: Instruction limit % 56.80/8.83 % (426109)Termination phase: Saturation % 56.80/8.83 % (426109)Time elapsed: 0.208 s % 56.80/8.83 % (426109)Peak memory usage: 92 MB % 56.80/8.83 % (426109)Instructions burned: 274 (million) % 56.80/8.83 % (426105)------------------------------ % 56.80/8.83 % (426105)------------------------------ % 56.80/8.83 % (426108)------------------------------ % 56.80/8.83 % (426108)------------------------------ % 56.80/8.83 % (426128)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=3364595265:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2944 on theBenchmark for (2944ds/868Mi) % 56.80/8.83 % (426131)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=1678242945:i=1846:canc=cautious:fsr=off:rtra=on_2943 on theBenchmark for (2943ds/1846Mi) % 56.80/8.83 % (426131)Refutation not found, incomplete strategy % 56.80/8.83 % (426131)------------------------------ % 56.80/8.83 % (426131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.80/8.83 % (426131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.53/10.54 % (426131)CaDiCaL version: 2.1.3 % 69.53/10.54 % (426131)Termination reason: Refutation not found, incomplete strategy % 69.53/10.54 % (426131)Time elapsed: 0.045 s % 69.53/10.54 % (426131)Peak memory usage: 89 MB % 69.53/10.54 % (426131)Instructions burned: 115 (million) % 69.53/10.54 % (426103)Instruction limit reached! % 69.53/10.54 % (426103)------------------------------ % 69.53/10.54 % (426103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.53/10.54 % (426103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.53/10.54 % (426103)CaDiCaL version: 2.1.3 % 69.53/10.54 % (426103)Termination reason: Instruction limit % 69.53/10.54 % (426103)Termination phase: Saturation % 69.53/10.54 % (426103)Time elapsed: 0.782 s % 69.53/10.54 % (426103)Peak memory usage: 117 MB % 69.53/10.54 % (426103)Instructions burned: 1131 (million) % 69.53/10.54 % (426136)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2117155636:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2942 on theBenchmark for (2942ds/36816Mi) % 69.53/10.54 % (426117)Instruction limit reached! % 69.53/10.54 % (426117)------------------------------ % 69.53/10.54 % (426117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.53/10.54 % (426117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.53/10.54 % (426117)CaDiCaL version: 2.1.3 % 69.53/10.54 % (426117)Termination reason: Instruction limit % 69.53/10.54 % (426117)Termination phase: Saturation % 69.53/10.54 % (426117)Time elapsed: 0.689 s % 69.53/10.54 % (426117)Peak memory usage: 92 MB % 69.53/10.54 % (426117)Instructions burned: 1094 (million) % 69.53/10.54 % (426142)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3040218940:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2940 on theBenchmark for (2940ds/273Mi) % 69.53/10.54 % (426131)------------------------------ % 69.53/10.54 % (426131)------------------------------ % 69.53/10.54 % (426148)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=805208441:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2938 on theBenchmark for (2938ds/863Mi) % 69.53/10.54 % (426142)Instruction limit reached! % 69.53/10.54 % (426142)------------------------------ % 69.53/10.54 % (426142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.53/10.54 % (426142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.53/10.54 % (426142)CaDiCaL version: 2.1.3 % 69.53/10.54 % (426142)Termination reason: Instruction limit % 69.53/10.54 % (426142)Termination phase: Saturation % 69.53/10.54 % (426142)Time elapsed: 0.212 s % 69.53/10.54 % (426142)Peak memory usage: 91 MB % 69.53/10.54 % (426142)Instructions burned: 274 (million) % 69.53/10.54 % (426128)Instruction limit reached! % 69.53/10.54 % (426128)------------------------------ % 69.53/10.54 % (426128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.53/10.54 % (426128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.53/10.54 % (426128)CaDiCaL version: 2.1.3 % 69.53/10.54 % (426128)Termination reason: Instruction limit % 69.53/10.54 % (426128)Termination phase: Saturation % 69.53/10.54 % (426128)Time elapsed: 0.726 s % 69.53/10.54 % (426128)Peak memory usage: 137 MB % 69.53/10.54 % (426128)Instructions burned: 868 (million) % 69.53/10.54 % (426150)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1332346030:i=5811:kws=precedence:nm=0:rtra=on_2936 on theBenchmark for (2936ds/5811Mi) % 69.53/10.54 % (426040)Instruction limit reached! % 69.53/10.54 % (426040)------------------------------ % 69.53/10.54 % (426040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.53/10.54 % (426040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.53/10.54 % (426040)CaDiCaL version: 2.1.3 % 69.53/10.54 % (426040)Termination reason: Instruction limit % 69.53/10.54 % (426040)Termination phase: Saturation % 69.53/10.54 % (426040)Time elapsed: 2.963 s % 69.53/10.54 % (426040)Peak memory usage: 92 MB % 69.53/10.54 % (426040)Instructions burned: 4428 (million) % 69.53/10.54 % (426152)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=3029154131:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2935 on theBenchmark for (2935ds/2216Mi) % 69.53/10.54 % (426154)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1001569871:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2934 on theBenchmark for (2934ds/801Mi) % 78.07/11.90 % (426158)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=496081261:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2933 on theBenchmark for (2933ds/1026Mi) % 78.07/11.90 % (426158)Refutation not found, incomplete strategy % 78.07/11.90 % (426158)------------------------------ % 78.07/11.90 % (426158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.07/11.90 % (426158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.07/11.90 % (426158)CaDiCaL version: 2.1.3 % 78.07/11.90 % (426158)Termination reason: Refutation not found, incomplete strategy % 78.07/11.90 % (426158)Time elapsed: 0.029 s % 78.07/11.90 % (426158)Peak memory usage: 88 MB % 78.07/11.90 % (426158)Instructions burned: 48 (million) % 78.07/11.90 % (426148)Instruction limit reached! % 78.07/11.90 % (426148)------------------------------ % 78.07/11.90 % (426148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.07/11.90 % (426148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.07/11.90 % (426148)CaDiCaL version: 2.1.3 % 78.07/11.90 % (426148)Termination reason: Instruction limit % 78.07/11.90 % (426148)Termination phase: Saturation % 78.07/11.90 % (426148)Time elapsed: 0.737 s % 78.07/11.90 % (426148)Peak memory usage: 137 MB % 78.07/11.90 % (426148)Instructions burned: 863 (million) % 78.07/11.90 % (426158)------------------------------ % 78.07/11.90 % (426158)------------------------------ % 78.07/11.90 % (426170)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4202964873:i=3509:rtra=on_2928 on theBenchmark for (2928ds/3509Mi) % 78.07/11.90 % (426154)Instruction limit reached! % 78.07/11.90 % (426154)------------------------------ % 78.07/11.90 % (426154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.07/11.90 % (426154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.07/11.90 % (426154)CaDiCaL version: 2.1.3 % 78.07/11.90 % (426154)Termination reason: Instruction limit % 78.07/11.90 % (426154)Termination phase: Saturation % 78.07/11.90 % (426154)Time elapsed: 0.693 s % 78.07/11.90 % (426154)Peak memory usage: 101 MB % 78.07/11.90 % (426154)Instructions burned: 802 (million) % 78.07/11.90 % (426171)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3749962283:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2927 on theBenchmark for (2927ds/2127Mi) % 78.07/11.90 % (426171)Refutation not found, incomplete strategy % 78.07/11.90 % (426171)------------------------------ % 78.07/11.90 % (426171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.07/11.90 % (426171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.07/11.90 % (426171)CaDiCaL version: 2.1.3 % 78.07/11.90 % (426171)Termination reason: Refutation not found, incomplete strategy % 78.07/11.90 % (426171)Time elapsed: 0.042 s % 78.07/11.90 % (426171)Peak memory usage: 88 MB % 78.07/11.90 % (426171)Instructions burned: 63 (million) % 78.07/11.90 % (426173)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=57364117:i=1959:rtra=on:fsd=on:proc=on_2925 on theBenchmark for (2925ds/1959Mi) % 78.07/11.90 % (426124)Instruction limit reached! % 78.07/11.90 % (426124)------------------------------ % 78.07/11.90 % (426124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.07/11.90 % (426124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.07/11.90 % (426124)CaDiCaL version: 2.1.3 % 78.07/11.90 % (426124)Termination reason: Instruction limit % 78.07/11.90 % (426124)Termination phase: Saturation % 78.07/11.90 % (426124)Time elapsed: 2.234 s % 78.07/11.90 % (426124)Peak memory usage: 93 MB % 78.07/11.90 % (426124)Instructions burned: 6402 (million) % 78.07/11.90 % (426179)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3635770786:s2a=on:i=3553:nm=0:rtra=on_2922 on theBenchmark for (2922ds/3553Mi) % 78.07/11.90 % (426171)------------------------------ % 78.07/11.90 % (426171)------------------------------ % 78.07/11.90 % (426152)Instruction limit reached! % 78.07/11.90 % (426152)------------------------------ % 78.07/11.90 % (426152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.07/11.90 % (426152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.07/11.90 % (426152)CaDiCaL version: 2.1.3 % 78.07/11.90 % (426152)Termination reason: Instruction limit % 78.07/11.90 % (426152)Termination phase: Saturation % 78.07/11.90 % (426152)Time elapsed: 1.419 s % 78.07/11.90 % (426152)Peak memory usage: 122 MB % 78.07/11.90 % (426152)Instructions burned: 2216 (million) % 78.07/11.90 % (426183)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1966710869:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2920 on theBenchmark for (2920ds/3201Mi) % 107.48/15.97 % (426185)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=387375244:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2919 on theBenchmark for (2919ds/4093Mi) % 107.48/15.97 % (426183)Refutation not found, incomplete strategy % 107.48/15.97 % (426183)------------------------------ % 107.48/15.97 % (426183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.48/15.97 % (426183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.48/15.97 % (426183)CaDiCaL version: 2.1.3 % 107.48/15.97 % (426183)Termination reason: Refutation not found, incomplete strategy % 107.48/15.97 % (426183)Time elapsed: 0.331 s % 107.48/15.97 % (426183)Peak memory usage: 93 MB % 107.48/15.97 % (426183)Instructions burned: 437 (million) % 107.48/15.97 % (426183)------------------------------ % 107.48/15.97 % (426183)------------------------------ % 107.48/15.97 % (426193)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=4078153730:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2912 on theBenchmark for (2912ds/21173Mi) % 107.48/15.97 % (426193)Refutation not found, incomplete strategy % 107.48/15.97 % (426193)------------------------------ % 107.48/15.97 % (426193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.48/15.97 % (426193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.48/15.97 % (426193)CaDiCaL version: 2.1.3 % 107.48/15.97 % (426193)Termination reason: Refutation not found, incomplete strategy % 107.48/15.97 % (426193)Time elapsed: 0.053 s % 107.48/15.97 % (426193)Peak memory usage: 113 MB % 107.48/15.97 % (426193)Instructions burned: 24 (million) % 107.48/15.97 % (426179)Instruction limit reached! % 107.48/15.97 % (426179)------------------------------ % 107.48/15.97 % (426179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.48/15.97 % (426179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.48/15.97 % (426179)CaDiCaL version: 2.1.3 % 107.48/15.97 % (426179)Termination reason: Instruction limit % 107.48/15.97 % (426179)Termination phase: Saturation % 107.48/15.97 % (426179)Time elapsed: 1.217 s % 107.48/15.97 % (426179)Peak memory usage: 92 MB % 107.48/15.97 % (426179)Instructions burned: 3556 (million) % 107.48/15.97 % (426173)Instruction limit reached! % 107.48/15.97 % (426173)------------------------------ % 107.48/15.97 % (426173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.48/15.97 % (426173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.48/15.97 % (426173)CaDiCaL version: 2.1.3 % 107.48/15.97 % (426173)Termination reason: Instruction limit % 107.48/15.97 % (426173)Termination phase: Saturation % 107.48/15.97 % (426173)Time elapsed: 1.504 s % 107.48/15.97 % (426173)Peak memory usage: 121 MB % 107.48/15.97 % (426173)Instructions burned: 1959 (million) % 107.48/15.97 % (426197)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4207099042:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2908 on theBenchmark for (2908ds/10544Mi) % 107.48/15.97 % (426193)------------------------------ % 107.48/15.97 % (426193)------------------------------ % 107.48/15.97 % (426199)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=732319355:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2908 on theBenchmark for (2908ds/1262Mi) % 107.48/15.97 % (426202)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3241930482:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2906 on theBenchmark for (2906ds/775Mi) % 107.48/15.97 % (426202)Refutation not found, incomplete strategy % 107.48/15.97 % (426202)------------------------------ % 107.48/15.97 % (426202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.48/15.97 % (426202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.48/15.97 % (426202)CaDiCaL version: 2.1.3 % 107.48/15.97 % (426202)Termination reason: Refutation not found, incomplete strategy % 107.48/15.97 % (426202)Time elapsed: 0.046 s % 107.48/15.97 % (426202)Peak memory usage: 88 MB % 107.48/15.97 % (426202)Instructions burned: 66 (million) % 107.48/15.97 % (426170)Instruction limit reached! % 107.48/15.97 % (426170)------------------------------ % 107.48/15.97 % (426170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.86/18.65 % (426170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.86/18.65 % (426170)CaDiCaL version: 2.1.3 % 126.86/18.65 % (426170)Termination reason: Instruction limit % 126.86/18.65 % (426170)Termination phase: Saturation % 126.86/18.65 % (426170)Time elapsed: 2.504 s % 126.86/18.65 % (426170)Peak memory usage: 91 MB % 126.86/18.65 % (426170)Instructions burned: 3510 (million) % 126.86/18.65 % (426202)------------------------------ % 126.86/18.65 % (426202)------------------------------ % 126.86/18.65 % (426208)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=614290349:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2901 on theBenchmark for (2901ds/270Mi) % 126.86/18.65 % (426209)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1277538802:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2899 on theBenchmark for (2899ds/17165Mi) % 126.86/18.65 % (426208)Instruction limit reached! % 126.86/18.65 % (426208)------------------------------ % 126.86/18.65 % (426208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.86/18.65 % (426208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.86/18.65 % (426208)CaDiCaL version: 2.1.3 % 126.86/18.65 % (426208)Termination reason: Instruction limit % 126.86/18.65 % (426208)Termination phase: Saturation % 126.86/18.65 % (426208)Time elapsed: 0.205 s % 126.86/18.65 % (426208)Peak memory usage: 91 MB % 126.86/18.65 % (426208)Instructions burned: 271 (million) % 126.86/18.65 % (426199)Instruction limit reached! % 126.86/18.65 % (426199)------------------------------ % 126.86/18.65 % (426199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.86/18.65 % (426199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.86/18.65 % (426199)CaDiCaL version: 2.1.3 % 126.86/18.65 % (426199)Termination reason: Instruction limit % 126.86/18.65 % (426199)Termination phase: Saturation % 126.86/18.65 % (426199)Time elapsed: 0.974 s % 126.86/18.65 % (426199)Peak memory usage: 121 MB % 126.86/18.65 % (426199)Instructions burned: 1263 (million) % 126.86/18.65 % (426213)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3344031988:s2a=on:i=13094:s2at=-1:rtra=on_2896 on theBenchmark for (2896ds/13094Mi) % 126.86/18.65 % (426214)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2720406347:st=2:i=12633:rtra=on:ss=axioms_2896 on theBenchmark for (2896ds/12633Mi) % 126.86/18.65 % (426214)Refutation not found, incomplete strategy % 126.86/18.65 % (426214)------------------------------ % 126.86/18.65 % (426214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.86/18.65 % (426214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.86/18.65 % (426214)CaDiCaL version: 2.1.3 % 126.86/18.65 % (426214)Termination reason: Refutation not found, incomplete strategy % 126.86/18.65 % (426214)Time elapsed: 0.029 s % 126.86/18.65 % (426214)Peak memory usage: 88 MB % 126.86/18.65 % (426214)Instructions burned: 35 (million) % 126.86/18.65 % (426150)Instruction limit reached! % 126.86/18.65 % (426150)------------------------------ % 126.86/18.65 % (426150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.86/18.65 % (426150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.86/18.65 % (426150)CaDiCaL version: 2.1.3 % 126.86/18.65 % (426150)Termination reason: Instruction limit % 126.86/18.65 % (426150)Termination phase: Saturation % 126.86/18.65 % (426150)Time elapsed: 4.049 s % 126.86/18.65 % (426150)Peak memory usage: 121 MB % 126.86/18.65 % (426150)Instructions burned: 5811 (million) % 126.86/18.65 % (426218)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3640084831:i=1783:rtra=on:gtg=position_2894 on theBenchmark for (2894ds/1783Mi) % 126.86/18.65 % (426214)------------------------------ % 126.86/18.65 % (426214)------------------------------ % 126.86/18.65 % (426221)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=3285983315:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2890 on theBenchmark for (2890ds/5451Mi) % 126.86/18.65 % (426185)Instruction limit reached! % 126.86/18.65 % (426185)------------------------------ % 126.86/18.65 % (426185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.86/18.65 % (426185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.86/18.65 % (426185)CaDiCaL version: 2.1.3 % 126.86/18.65 % (426185)Termination reason: Instruction limit % 168.35/24.44 % (426185)Termination phase: Saturation % 168.35/24.44 % (426185)Time elapsed: 2.954 s % 168.35/24.44 % (426185)Peak memory usage: 139 MB % 168.35/24.44 % (426185)Instructions burned: 4097 (million) % 168.35/24.44 % (426229)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=591682482:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2887 on theBenchmark for (2887ds/4975Mi) % 168.35/24.44 % (426218)Instruction limit reached! % 168.35/24.44 % (426218)------------------------------ % 168.35/24.44 % (426218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.35/24.44 % (426218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.35/24.44 % (426218)CaDiCaL version: 2.1.3 % 168.35/24.44 % (426218)Termination reason: Instruction limit % 168.35/24.44 % (426218)Termination phase: Saturation % 168.35/24.44 % (426218)Time elapsed: 1.254 s % 168.35/24.44 % (426218)Peak memory usage: 121 MB % 168.35/24.44 % (426218)Instructions burned: 1784 (million) % 168.35/24.44 % (426238)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=510290105:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2879 on theBenchmark for (2879ds/2076Mi) % 168.35/24.45 % (426238)Instruction limit reached! % 168.35/24.45 % (426238)------------------------------ % 168.35/24.45 % (426238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.35/24.45 % (426238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.35/24.45 % (426238)CaDiCaL version: 2.1.3 % 168.35/24.45 % (426238)Termination reason: Instruction limit % 168.35/24.45 % (426238)Termination phase: Saturation % 168.35/24.45 % (426238)Time elapsed: 1.498 s % 168.35/24.45 % (426238)Peak memory usage: 122 MB % 168.35/24.45 % (426238)Instructions burned: 2076 (million) % 168.35/24.45 % (426197)Instruction limit reached! % 168.35/24.45 % (426197)------------------------------ % 168.35/24.45 % (426197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.35/24.45 % (426197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.35/24.45 % (426197)CaDiCaL version: 2.1.3 % 168.35/24.45 % (426197)Termination reason: Instruction limit % 168.35/24.45 % (426197)Termination phase: Saturation % 168.35/24.45 % (426197)Time elapsed: 4.645 s % 168.35/24.45 % (426197)Peak memory usage: 173 MB % 168.35/24.45 % (426197)Instructions burned: 10546 (million) % 168.35/24.45 % (426242)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=31759208:i=5145:rtra=on_2861 on theBenchmark for (2861ds/5145Mi) % 168.35/24.45 % (426243)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1767592079:i=3509:rtra=on_2860 on theBenchmark for (2860ds/3509Mi) % 168.35/24.45 % (426221)Instruction limit reached! % 168.35/24.45 % (426221)------------------------------ % 168.35/24.45 % (426221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.35/24.45 % (426221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.35/24.45 % (426221)CaDiCaL version: 2.1.3 % 168.35/24.45 % (426221)Termination reason: Instruction limit % 168.35/24.45 % (426221)Termination phase: Saturation % 168.35/24.45 % (426221)Time elapsed: 3.651 s % 168.35/24.45 % (426221)Peak memory usage: 123 MB % 168.35/24.45 % (426221)Instructions burned: 5452 (million) % 168.35/24.45 % (426250)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3095498501:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2851 on theBenchmark for (2851ds/13800Mi) % 168.35/24.45 % (426250)Refutation not found, incomplete strategy % 168.35/24.45 % (426250)------------------------------ % 168.35/24.45 % (426250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.35/24.45 % (426250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.35/24.45 % (426250)CaDiCaL version: 2.1.3 % 168.35/24.45 % (426250)Termination reason: Refutation not found, incomplete strategy % 168.35/24.45 % (426250)Time elapsed: 0.042 s % 168.35/24.45 % (426250)Peak memory usage: 88 MB % 168.35/24.45 % (426250)Instructions burned: 63 (million) % 168.35/24.45 % (426243)Instruction limit reached! % 168.35/24.45 % (426243)------------------------------ % 168.35/24.45 % (426243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.35/24.45 % (426243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.35/24.45 % (426243)CaDiCaL version: 2.1.3 % 168.35/24.45 % (426243)Termination reason: Instruction limit % 168.35/24.45 % (426243)Termination phase: Saturation % 168.35/24.45 % (426243)Time elapsed: 1.247 s % 240.20/34.60 % (426243)Peak memory usage: 91 MB % 240.20/34.60 % (426243)Instructions burned: 3509 (million) % 240.20/34.60 % (426250)------------------------------ % 240.20/34.60 % (426250)------------------------------ % 240.20/34.60 % (426252)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=129570500:i=1412:rtra=on:fsd=on:proc=on_2846 on theBenchmark for (2846ds/1412Mi) % 240.20/34.60 % (426229)Instruction limit reached! % 240.20/34.60 % (426229)------------------------------ % 240.20/34.60 % (426229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.20/34.60 % (426229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.20/34.60 % (426229)CaDiCaL version: 2.1.3 % 240.20/34.60 % (426229)Termination reason: Instruction limit % 240.20/34.60 % (426229)Termination phase: Saturation % 240.20/34.60 % (426229)Time elapsed: 4.066 s % 240.20/34.60 % (426229)Peak memory usage: 164 MB % 240.20/34.60 % (426229)Instructions burned: 4976 (million) % 240.20/34.60 % (426253)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 % 240.20/34.60 % (426253)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3143049218:i=11747:aac=none:nm=0:rtra=on:rawr=on_2845 on theBenchmark for (2845ds/11747Mi) % 240.20/34.60 % (426255)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4117910878:s2a=on:i=3553:nm=0:rtra=on_2844 on theBenchmark for (2844ds/3553Mi) % 240.20/34.60 % (426252)Instruction limit reached! % 240.20/34.60 % (426252)------------------------------ % 240.20/34.60 % (426252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.20/34.60 % (426252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.20/34.60 % (426252)CaDiCaL version: 2.1.3 % 240.20/34.60 % (426252)Termination reason: Instruction limit % 240.20/34.60 % (426252)Termination phase: Saturation % 240.20/34.60 % (426252)Time elapsed: 0.588 s % 240.20/34.60 % (426252)Peak memory usage: 121 MB % 240.20/34.60 % (426252)Instructions burned: 1412 (million) % 240.20/34.60 % (426260)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1635617507:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/3201Mi) % 240.20/34.60 % (426260)Refutation not found, incomplete strategy % 240.20/34.60 % (426260)------------------------------ % 240.20/34.60 % (426260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.20/34.60 % (426260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.20/34.60 % (426260)CaDiCaL version: 2.1.3 % 240.20/34.60 % (426260)Termination reason: Refutation not found, incomplete strategy % 240.20/34.60 % (426260)Time elapsed: 0.189 s % 240.20/34.60 % (426260)Peak memory usage: 93 MB % 240.20/34.60 % (426260)Instructions burned: 498 (million) % 240.20/34.60 % (426260)------------------------------ % 240.20/34.60 % (426260)------------------------------ % 240.20/34.60 % (426267)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=3121685931:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2833 on theBenchmark for (2833ds/4081Mi) % 240.20/34.60 % (426242)Instruction limit reached! % 240.20/34.60 % (426242)------------------------------ % 240.20/34.60 % (426242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.20/34.60 % (426242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.20/34.60 % (426242)CaDiCaL version: 2.1.3 % 240.20/34.60 % (426242)Termination reason: Instruction limit % 240.20/34.60 % (426242)Termination phase: Saturation % 240.20/34.60 % (426242)Time elapsed: 3.679 s % 240.20/34.60 % (426242)Peak memory usage: 97 MB % 240.20/34.60 % (426242)Instructions burned: 5145 (million) % 240.20/34.60 % (426274)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=2853938224:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2822 on theBenchmark for (2822ds/20260Mi) % 240.20/34.60 % (426274)Refutation not found, incomplete strategy % 240.20/34.60 % (426274)------------------------------ % 240.20/34.60 % (426274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.20/34.60 % (426274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.20/34.60 % (426274)CaDiCaL version: 2.1.3 % 275.75/39.56 % (426274)Termination reason: Refutation not found, incomplete strategy % 275.75/39.56 % (426274)Time elapsed: 0.052 s % 275.75/39.56 % (426274)Peak memory usage: 113 MB % 275.75/39.56 % (426274)Instructions burned: 24 (million) % 275.75/39.56 % (426255)Instruction limit reached! % 275.75/39.56 % (426255)------------------------------ % 275.75/39.56 % (426255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.75/39.56 % (426255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.75/39.56 % (426255)CaDiCaL version: 2.1.3 % 275.75/39.56 % (426255)Termination reason: Instruction limit % 275.75/39.56 % (426255)Termination phase: Saturation % 275.75/39.56 % (426255)Time elapsed: 2.426 s % 275.75/39.56 % (426255)Peak memory usage: 93 MB % 275.75/39.56 % (426255)Instructions burned: 3553 (million) % 275.75/39.56 % (426267)Instruction limit reached! % 275.75/39.56 % (426267)------------------------------ % 275.75/39.56 % (426267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.75/39.56 % (426267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.75/39.56 % (426267)CaDiCaL version: 2.1.3 % 275.75/39.56 % (426267)Termination reason: Instruction limit % 275.75/39.56 % (426267)Termination phase: Saturation % 275.75/39.56 % (426267)Time elapsed: 1.569 s % 275.75/39.56 % (426267)Peak memory usage: 134 MB % 275.75/39.56 % (426267)Instructions burned: 4083 (million) % 275.75/39.56 % (426274)------------------------------ % 275.75/39.56 % (426274)------------------------------ % 275.75/39.56 % (426277)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1802459362:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2817 on theBenchmark for (2817ds/58627Mi) % 275.75/39.56 % (426278)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=837581688:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/6258Mi) % 275.75/39.56 % (426279)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3091956196:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2816 on theBenchmark for (2816ds/34001Mi) % 275.75/39.56 % (426213)Instruction limit reached! % 275.75/39.56 % (426213)------------------------------ % 275.75/39.56 % (426213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.75/39.56 % (426213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.75/39.56 % (426213)CaDiCaL version: 2.1.3 % 275.75/39.56 % (426213)Termination reason: Instruction limit % 275.75/39.56 % (426213)Termination phase: Saturation % 275.75/39.56 % (426213)Time elapsed: 9.456 s % 275.75/39.56 % (426213)Peak memory usage: 121 MB % 275.75/39.56 % (426213)Instructions burned: 13094 (million) % 275.75/39.56 % (426288)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4192181830:s2a=on:i=71622:s2at=-1:rtra=on_2799 on theBenchmark for (2799ds/71622Mi) % 275.75/39.56 % (426278)Instruction limit reached! % 275.75/39.56 % (426278)------------------------------ % 275.75/39.56 % (426278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.75/39.56 % (426278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.75/39.56 % (426278)CaDiCaL version: 2.1.3 % 275.75/39.56 % (426278)Termination reason: Instruction limit % 275.75/39.56 % (426278)Termination phase: Saturation % 275.75/39.56 % (426278)Time elapsed: 2.502 s % 275.75/39.56 % (426278)Peak memory usage: 123 MB % 275.75/39.56 % (426278)Instructions burned: 6259 (million) % 275.75/39.56 % (426294)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3345983229:i=24001:kws=precedence:nm=0:rtra=on_2789 on theBenchmark for (2789ds/24001Mi) % 275.75/39.56 % (426209)Instruction limit reached! % 275.75/39.56 % (426209)------------------------------ % 275.75/39.56 % (426209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.75/39.56 % (426209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.75/39.56 % (426209)CaDiCaL version: 2.1.3 % 275.75/39.56 % (426209)Termination reason: Instruction limit % 275.75/39.56 % (426209)Termination phase: Saturation % 275.75/39.56 % (426209)Time elapsed: 11.796 s % 275.75/39.56 % (426209)Peak memory usage: 97 MB % 275.75/39.56 % (426209)Instructions burned: 17165 (million) % 275.75/39.56 % (426298)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=3699040015:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2779 on theBenchmark for (2779ds/2076Mi) % 275.75/39.56 % (426298)Instruction limit reached! % 275.75/39.56 % (426298)------------------------------ % 300.66/43.04 Terminated %------------------------------------------------------------------------------