%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW748_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n008.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:31:11 PM UTC 2026 % Result : Timeout 300.49s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW748_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.18 % Computer : n008.cluster.edu % 0.06/0.18 % Model : x86_64 x86_64 % 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.18 % Memory : 8046.5625MB % 0.06/0.18 % OS : Linux 6.8.0-71-generic % 0.06/0.18 % CPULimit : 300 % 0.06/0.18 % WCLimit : 300 % 0.06/0.18 % DateTime : Mon Sep 28 14:29:39 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.21 Running first-order theorem proving % 0.06/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.42/1.27 % (2292653)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.42/1.27 % (2292736)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=449703110:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.42/1.27 % (2292734)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=562554500:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.42/1.27 % (2292734)Instruction limit reached! % 3.42/1.27 % (2292734)------------------------------ % 3.42/1.27 % (2292734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.27 % (2292734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.27 % (2292734)CaDiCaL version: 2.1.3 % 3.42/1.27 % (2292734)Termination reason: Instruction limit % 3.42/1.27 % (2292734)Termination phase: Property scanning % 3.42/1.27 % (2292734)Time elapsed: 0.006 s % 3.42/1.27 % (2292734)Peak memory usage: 86 MB % 3.42/1.27 % (2292734)Instructions burned: 14 (million) % 3.42/1.27 % (2292738)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=760607727:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.42/1.27 % (2292737)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=30058761:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.42/1.27 % (2292740)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3451182568:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.42/1.27 % (2292740)Instruction limit reached! % 3.42/1.27 % (2292740)------------------------------ % 3.42/1.27 % (2292740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.27 % (2292740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.27 % (2292740)CaDiCaL version: 2.1.3 % 3.42/1.27 % (2292740)Termination reason: Instruction limit % 3.42/1.27 % (2292740)Termination phase: Property scanning % 3.42/1.27 % (2292740)Time elapsed: 0.003 s % 3.42/1.27 % (2292740)Peak memory usage: 85 MB % 3.42/1.27 % (2292740)Instructions burned: 7 (million) % 3.42/1.27 % (2292738)Instruction limit reached! % 3.42/1.27 % (2292738)------------------------------ % 3.42/1.27 % (2292738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.27 % (2292738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.27 % (2292738)CaDiCaL version: 2.1.3 % 3.42/1.27 % (2292738)Termination reason: Instruction limit % 3.42/1.27 % (2292738)Termination phase: Property scanning % 3.42/1.27 % (2292738)Time elapsed: 0.004 s % 3.42/1.27 % (2292738)Peak memory usage: 86 MB % 3.42/1.27 % (2292738)Instructions burned: 8 (million) % 3.42/1.27 % (2292743)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2669574774:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.42/1.27 % (2292743)Instruction limit reached! % 3.42/1.27 % (2292743)------------------------------ % 3.42/1.27 % (2292743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.27 % (2292743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.27 % (2292743)CaDiCaL version: 2.1.3 % 3.42/1.27 % (2292743)Termination reason: Instruction limit % 3.42/1.27 % (2292743)Termination phase: Naming % 3.42/1.27 % (2292743)Time elapsed: 0.015 s % 3.42/1.27 % (2292743)Peak memory usage: 87 MB % 3.42/1.27 % (2292743)Instructions burned: 34 (million) % 3.42/1.27 % (2292741)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3163103258:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.42/1.27 % (2292741)Instruction limit reached! % 3.42/1.27 % (2292741)------------------------------ % 3.42/1.27 % (2292741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.27 % (2292741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.27 % (2292741)CaDiCaL version: 2.1.3 % 3.42/1.27 % (2292741)Termination reason: Instruction limit % 3.42/1.27 % (2292741)Termination phase: Property scanning % 3.42/1.27 % (2292741)Time elapsed: 0.025 s % 3.42/1.27 % (2292741)Peak memory usage: 89 MB % 3.42/1.27 % (2292741)Instructions burned: 49 (million) % 3.42/1.27 % (2292737)Instruction limit reached! % 3.42/1.27 % (2292737)------------------------------ % 3.42/1.27 % (2292737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.27 % (2292737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.21/1.40 % (2292737)CaDiCaL version: 2.1.3 % 4.21/1.40 % (2292737)Termination reason: Instruction limit % 4.21/1.40 % (2292737)Termination phase: Saturation % 4.21/1.40 % (2292737)Time elapsed: 0.129 s % 4.21/1.40 % (2292737)Peak memory usage: 119 MB % 4.21/1.40 % (2292737)Instructions burned: 202 (million) % 4.21/1.40 % (2292770)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3850196221:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.21/1.40 % (2292770)Instruction limit reached! % 4.21/1.40 % (2292770)------------------------------ % 4.21/1.40 % (2292770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.21/1.40 % (2292770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.21/1.40 % (2292770)CaDiCaL version: 2.1.3 % 4.21/1.40 % (2292770)Termination reason: Instruction limit % 4.21/1.40 % (2292770)Termination phase: SInE selection % 4.21/1.40 % (2292770)Time elapsed: 0.007 s % 4.21/1.40 % (2292770)Peak memory usage: 86 MB % 4.21/1.40 % (2292770)Instructions burned: 16 (million) % 4.21/1.40 % (2292736)Instruction limit reached! % 4.21/1.40 % (2292736)------------------------------ % 4.21/1.40 % (2292736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.21/1.40 % (2292736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.21/1.40 % (2292736)CaDiCaL version: 2.1.3 % 4.21/1.40 % (2292736)Termination reason: Instruction limit % 4.21/1.40 % (2292736)Termination phase: Clausification % 4.21/1.40 % (2292736)Time elapsed: 0.187 s % 4.21/1.40 % (2292736)Peak memory usage: 249 MB % 4.21/1.40 % (2292736)Instructions burned: 308 (million) % 4.21/1.40 % (2292780)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3829634570:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.21/1.40 % (2292778)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=3913094631:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.21/1.40 % (2292780)Instruction limit reached! % 4.21/1.40 % (2292780)------------------------------ % 4.21/1.40 % (2292780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.21/1.40 % (2292780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.21/1.40 % (2292780)CaDiCaL version: 2.1.3 % 4.21/1.40 % (2292780)Termination reason: Instruction limit % 4.21/1.40 % (2292780)Termination phase: Unused predicate definition removal % 4.21/1.40 % (2292780)Time elapsed: 0.008 s % 4.21/1.40 % (2292780)Peak memory usage: 86 MB % 4.21/1.40 % (2292780)Instructions burned: 18 (million) % 4.21/1.40 % (2292778)Instruction limit reached! % 4.21/1.40 % (2292778)------------------------------ % 4.21/1.40 % (2292778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.21/1.40 % (2292778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.21/1.40 % (2292778)CaDiCaL version: 2.1.3 % 4.21/1.40 % (2292778)Termination reason: Instruction limit % 4.21/1.40 % (2292778)Termination phase: Preprocessing 3 % 4.21/1.40 % (2292778)Time elapsed: 0.013 s % 4.21/1.40 % (2292778)Peak memory usage: 87 MB % 4.21/1.40 % (2292778)Instructions burned: 30 (million) % 4.21/1.40 % (2292786)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1458120428:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.21/1.40 % (2292786)Instruction limit reached! % 4.21/1.40 % (2292786)------------------------------ % 4.21/1.40 % (2292786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.21/1.40 % (2292786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.21/1.40 % (2292786)CaDiCaL version: 2.1.3 % 4.21/1.40 % (2292786)Termination reason: Instruction limit % 4.21/1.40 % (2292786)Termination phase: Unused predicate definition removal % 4.21/1.40 % (2292786)Time elapsed: 0.017 s % 4.21/1.40 % (2292786)Peak memory usage: 86 MB % 4.21/1.40 % (2292786)Instructions burned: 25 (million) % 4.21/1.40 % (2292794)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=2877640775:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.21/1.40 % (2292812)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3742619673:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 4.21/1.40 % (2292808)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3861700584:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 5.50/1.51 % (2292809)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2879263202:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.50/1.51 % (2292809)Instruction limit reached! % 5.50/1.51 % (2292809)------------------------------ % 5.50/1.51 % (2292809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.50/1.51 % (2292809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.51 % (2292809)CaDiCaL version: 2.1.3 % 5.50/1.51 % (2292809)Termination reason: Instruction limit % 5.50/1.51 % (2292809)Termination phase: shuffling % 5.50/1.51 % (2292809)Time elapsed: 0.001 s % 5.50/1.51 % (2292809)Peak memory usage: 85 MB % 5.50/1.51 % (2292809)Instructions burned: 2 (million) % 5.50/1.51 % (2292812)Refutation not found, incomplete strategy % 5.50/1.51 % (2292812)------------------------------ % 5.50/1.51 % (2292812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.50/1.51 % (2292812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.51 % (2292812)CaDiCaL version: 2.1.3 % 5.50/1.51 % (2292812)Termination reason: Refutation not found, incomplete strategy % 5.50/1.51 % (2292812)Time elapsed: 0.004 s % 5.50/1.51 % (2292812)Peak memory usage: 88 MB % 5.50/1.51 % (2292812)Instructions burned: 18 (million) % 5.50/1.51 % (2292794)Instruction limit reached! % 5.50/1.51 % (2292794)------------------------------ % 5.50/1.51 % (2292794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.50/1.51 % (2292794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.51 % (2292794)CaDiCaL version: 2.1.3 % 5.50/1.51 % (2292794)Termination reason: Instruction limit % 5.50/1.51 % (2292794)Termination phase: Unused predicate definition removal % 5.50/1.51 % (2292794)Time elapsed: 0.023 s % 5.50/1.51 % (2292794)Peak memory usage: 86 MB % 5.50/1.51 % (2292794)Instructions burned: 27 (million) % 5.50/1.51 % (2292813)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2366303310:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.50/1.51 % (2292813)Instruction limit reached! % 5.50/1.51 % (2292813)------------------------------ % 5.50/1.51 % (2292813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.50/1.51 % (2292813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.51 % (2292813)CaDiCaL version: 2.1.3 % 5.50/1.51 % (2292813)Termination reason: Instruction limit % 5.50/1.51 % (2292813)Termination phase: Property scanning % 5.50/1.51 % (2292813)Time elapsed: 0.003 s % 5.50/1.51 % (2292813)Peak memory usage: 86 MB % 5.50/1.51 % (2292813)Instructions burned: 6 (million) % 5.50/1.51 % (2292808)Instruction limit reached! % 5.50/1.51 % (2292808)------------------------------ % 5.50/1.51 % (2292808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.50/1.51 % (2292808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.51 % (2292808)CaDiCaL version: 2.1.3 % 5.50/1.51 % (2292808)Termination reason: Instruction limit % 5.50/1.51 % (2292808)Termination phase: Property scanning % 5.50/1.51 % (2292808)Time elapsed: 0.039 s % 5.50/1.51 % (2292808)Peak memory usage: 89 MB % 5.50/1.51 % (2292808)Instructions burned: 85 (million) % 5.50/1.51 % (2292814)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=552784775:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.50/1.51 % (2292814)Instruction limit reached! % 5.50/1.51 % (2292814)------------------------------ % 5.50/1.51 % (2292814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.50/1.51 % (2292814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.51 % (2292814)CaDiCaL version: 2.1.3 % 5.50/1.51 % (2292814)Termination reason: Instruction limit % 5.50/1.51 % (2292814)Termination phase: Property scanning % 5.50/1.51 % (2292814)Time elapsed: 0.031 s % 5.50/1.51 % (2292814)Peak memory usage: 89 MB % 5.50/1.51 % (2292814)Instructions burned: 66 (million) % 5.50/1.51 % (2292820)lrs+10_1_thi=all:si=on:fd=off:random_seed=2469321360:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 5.50/1.51 % (2292821)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=3306503146:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 6.91/1.93 % (2292821)Instruction limit reached! % 6.91/1.93 % (2292821)------------------------------ % 6.91/1.93 % (2292821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.93 % (2292821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.93 % (2292821)CaDiCaL version: 2.1.3 % 6.91/1.93 % (2292821)Termination reason: Instruction limit % 6.91/1.93 % (2292821)Termination phase: Property scanning % 6.91/1.93 % (2292821)Time elapsed: 0.004 s % 6.91/1.93 % (2292821)Peak memory usage: 85 MB % 6.91/1.93 % (2292821)Instructions burned: 8 (million) % 6.91/1.93 % (2292812)------------------------------ % 6.91/1.93 % (2292812)------------------------------ % 6.91/1.93 % (2292820)Instruction limit reached! % 6.91/1.93 % (2292820)------------------------------ % 6.91/1.93 % (2292820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.93 % (2292820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.93 % (2292820)CaDiCaL version: 2.1.3 % 6.91/1.93 % (2292820)Termination reason: Instruction limit % 6.91/1.93 % (2292820)Termination phase: Naming % 6.91/1.93 % (2292820)Time elapsed: 0.022 s % 6.91/1.93 % (2292820)Peak memory usage: 87 MB % 6.91/1.93 % (2292820)Instructions burned: 53 (million) % 6.91/1.93 % (2292822)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=442771616:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.91/1.93 % (2292826)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3642705212:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.91/1.93 % (2292824)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3980444053:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 6.91/1.93 % (2292824)Instruction limit reached! % 6.91/1.93 % (2292824)------------------------------ % 6.91/1.93 % (2292824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.93 % (2292824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.93 % (2292824)CaDiCaL version: 2.1.3 % 6.91/1.93 % (2292824)Termination reason: Instruction limit % 6.91/1.93 % (2292824)Termination phase: Property scanning % 6.91/1.93 % (2292824)Time elapsed: 0.003 s % 6.91/1.93 % (2292824)Peak memory usage: 86 MB % 6.91/1.93 % (2292824)Instructions burned: 5 (million) % 6.91/1.93 % (2292822)Instruction limit reached! % 6.91/1.93 % (2292822)------------------------------ % 6.91/1.93 % (2292822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.93 % (2292822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.93 % (2292822)CaDiCaL version: 2.1.3 % 6.91/1.93 % (2292822)Termination reason: Instruction limit % 6.91/1.93 % (2292822)Termination phase: Property scanning % 6.91/1.93 % (2292822)Time elapsed: 0.004 s % 6.91/1.93 % (2292822)Peak memory usage: 86 MB % 6.91/1.93 % (2292822)Instructions burned: 7 (million) % 6.91/1.93 % (2292827)dis+10_1_si=on:random_seed=2325027856:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.91/1.93 % (2292827)Instruction limit reached! % 6.91/1.93 % (2292827)------------------------------ % 6.91/1.93 % (2292827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.93 % (2292827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.93 % (2292827)CaDiCaL version: 2.1.3 % 6.91/1.93 % (2292827)Termination reason: Instruction limit % 6.91/1.93 % (2292827)Termination phase: Including theory axioms % 6.91/1.93 % (2292827)Time elapsed: 0.006 s % 6.91/1.93 % (2292827)Peak memory usage: 86 MB % 6.91/1.93 % (2292827)Instructions burned: 12 (million) % 6.91/1.93 % (2292831)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1921901620:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi) % 6.91/1.93 % (2292826)Instruction limit reached! % 6.91/1.93 % (2292826)------------------------------ % 6.91/1.93 % (2292826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.91/1.93 % (2292826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.93 % (2292826)CaDiCaL version: 2.1.3 % 6.91/1.93 % (2292826)Termination reason: Instruction limit % 6.91/1.93 % (2292826)Termination phase: Saturation % 6.91/1.93 % (2292826)Time elapsed: 0.085 s % 6.91/1.93 % (2292826)Peak memory usage: 116 MB % 9.44/2.15 % (2292826)Instructions burned: 128 (million) % 9.44/2.15 % (2292831)Instruction limit reached! % 9.44/2.15 % (2292831)------------------------------ % 9.44/2.15 % (2292831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.44/2.15 % (2292831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.44/2.15 % (2292831)CaDiCaL version: 2.1.3 % 9.44/2.15 % (2292831)Termination reason: Instruction limit % 9.44/2.15 % (2292831)Termination phase: Naming % 9.44/2.15 % (2292831)Time elapsed: 0.009 s % 9.44/2.15 % (2292831)Peak memory usage: 87 MB % 9.44/2.15 % (2292831)Instructions burned: 38 (million) % 9.44/2.15 % (2292830)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2656996110:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 9.44/2.15 % (2292830)Instruction limit reached! % 9.44/2.15 % (2292830)------------------------------ % 9.44/2.15 % (2292830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.44/2.15 % (2292830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.44/2.15 % (2292830)CaDiCaL version: 2.1.3 % 9.44/2.15 % (2292830)Termination reason: Instruction limit % 9.44/2.15 % (2292830)Termination phase: Unused predicate definition removal % 9.44/2.15 % (2292830)Time elapsed: 0.013 s % 9.44/2.15 % (2292830)Peak memory usage: 86 MB % 9.44/2.15 % (2292830)Instructions burned: 28 (million) % 9.44/2.15 % (2292832)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2809340953:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 9.44/2.15 % (2292832)Instruction limit reached! % 9.44/2.15 % (2292832)------------------------------ % 9.44/2.15 % (2292832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.44/2.15 % (2292832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.44/2.15 % (2292832)CaDiCaL version: 2.1.3 % 9.44/2.15 % (2292832)Termination reason: Instruction limit % 9.44/2.15 % (2292832)Termination phase: Property scanning % 9.44/2.15 % (2292832)Time elapsed: 0.003 s % 9.44/2.15 % (2292832)Peak memory usage: 86 MB % 9.44/2.15 % (2292832)Instructions burned: 5 (million) % 9.44/2.15 % (2292837)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3303721287:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 9.44/2.15 % (2292836)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2540873106:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 9.44/2.15 % (2292836)Instruction limit reached! % 9.44/2.15 % (2292836)------------------------------ % 9.44/2.15 % (2292836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.44/2.15 % (2292836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.44/2.15 % (2292836)CaDiCaL version: 2.1.3 % 9.44/2.15 % (2292836)Termination reason: Instruction limit % 9.44/2.15 % (2292836)Termination phase: Property scanning % 9.44/2.15 % (2292836)Time elapsed: 0.004 s % 9.44/2.15 % (2292836)Peak memory usage: 86 MB % 9.44/2.15 % (2292836)Instructions burned: 9 (million) % 9.44/2.15 % (2292839)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1509880556:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 9.44/2.15 % (2292839)Instruction limit reached! % 9.44/2.15 % (2292839)------------------------------ % 9.44/2.15 % (2292839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.44/2.15 % (2292839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.44/2.15 % (2292839)CaDiCaL version: 2.1.3 % 9.44/2.15 % (2292839)Termination reason: Instruction limit % 9.44/2.15 % (2292839)Termination phase: Property scanning % 9.44/2.15 % (2292839)Time elapsed: 0.006 s % 9.44/2.15 % (2292839)Peak memory usage: 85 MB % 9.44/2.15 % (2292839)Instructions burned: 14 (million) % 9.44/2.15 % (2292842)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3393510005:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 9.44/2.15 % (2292842)Instruction limit reached! % 9.44/2.15 % (2292842)------------------------------ % 9.44/2.15 % (2292842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.44/2.15 % (2292842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.44/2.15 % (2292842)CaDiCaL version: 2.1.3 % 9.44/2.15 % (2292842)Termination reason: Instruction limit % 9.44/2.15 % (2292842)Termination phase: Preprocessing 1 % 12.10/2.48 % (2292842)Time elapsed: 0.003 s % 12.10/2.48 % (2292842)Peak memory usage: 86 MB % 12.10/2.48 % (2292842)Instructions burned: 13 (million) % 12.10/2.48 % (2292841)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=111946213:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 12.10/2.48 % (2292841)Refutation not found, incomplete strategy % 12.10/2.48 % (2292841)------------------------------ % 12.10/2.48 % (2292841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.48 % (2292841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.48 % (2292841)CaDiCaL version: 2.1.3 % 12.10/2.48 % (2292841)Termination reason: Refutation not found, incomplete strategy % 12.10/2.48 % (2292841)Time elapsed: 0.059 s % 12.10/2.48 % (2292841)Peak memory usage: 112 MB % 12.10/2.48 % (2292841)Instructions burned: 31 (million) % 12.10/2.48 % (2292846)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=1201890729:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 12.10/2.48 % (2292845)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2718801589:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 12.10/2.48 % (2292837)Instruction limit reached! % 12.10/2.48 % (2292837)------------------------------ % 12.10/2.48 % (2292837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.48 % (2292837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.48 % (2292837)CaDiCaL version: 2.1.3 % 12.10/2.48 % (2292837)Termination reason: Instruction limit % 12.10/2.48 % (2292837)Termination phase: Saturation % 12.10/2.48 % (2292837)Time elapsed: 0.201 s % 12.10/2.48 % (2292837)Peak memory usage: 97 MB % 12.10/2.48 % (2292837)Instructions burned: 370 (million) % 12.10/2.48 % (2292849)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=3041346889:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi) % 12.10/2.48 % (2292845)Instruction limit reached! % 12.10/2.48 % (2292845)------------------------------ % 12.10/2.48 % (2292845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.48 % (2292845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.48 % (2292845)CaDiCaL version: 2.1.3 % 12.10/2.48 % (2292845)Termination reason: Instruction limit % 12.10/2.48 % (2292845)Termination phase: Property scanning % 12.10/2.48 % (2292845)Time elapsed: 0.056 s % 12.10/2.48 % (2292845)Peak memory usage: 89 MB % 12.10/2.48 % (2292845)Instructions burned: 71 (million) % 12.10/2.48 % (2292846)Instruction limit reached! % 12.10/2.48 % (2292846)------------------------------ % 12.10/2.48 % (2292846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.48 % (2292846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.48 % (2292846)CaDiCaL version: 2.1.3 % 12.10/2.48 % (2292846)Termination reason: Instruction limit % 12.10/2.48 % (2292846)Termination phase: Property scanning % 12.10/2.48 % (2292846)Time elapsed: 0.059 s % 12.10/2.48 % (2292846)Peak memory usage: 89 MB % 12.10/2.48 % (2292846)Instructions burned: 75 (million) % 12.10/2.48 % (2292854)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=187027219:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 12.10/2.48 % (2292852)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=343148513:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi) % 12.10/2.48 % (2292854)Instruction limit reached! % 12.10/2.48 % (2292854)------------------------------ % 12.10/2.48 % (2292854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.48 % (2292854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.48 % (2292854)CaDiCaL version: 2.1.3 % 12.10/2.48 % (2292854)Termination reason: Instruction limit % 12.10/2.48 % (2292854)Termination phase: Saturation % 12.10/2.48 % (2292854)Time elapsed: 0.097 s % 12.10/2.48 % (2292854)Peak memory usage: 132 MB % 12.10/2.48 % (2292854)Instructions burned: 132 (million) % 12.10/2.48 % (2292865)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3365142211:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi) % 12.10/2.48 % (2292852)Instruction limit reached! % 12.66/2.70 % (2292852)------------------------------ % 12.66/2.70 % (2292852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.66/2.70 % (2292852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.66/2.70 % (2292852)CaDiCaL version: 2.1.3 % 12.66/2.70 % (2292852)Termination reason: Instruction limit % 12.66/2.70 % (2292852)Termination phase: Clausification % 12.66/2.70 % (2292852)Time elapsed: 0.164 s % 12.66/2.70 % (2292852)Peak memory usage: 131 MB % 12.66/2.70 % (2292852)Instructions burned: 130 (million) % 12.66/2.70 % (2292865)Instruction limit reached! % 12.66/2.70 % (2292865)------------------------------ % 12.66/2.70 % (2292865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.66/2.70 % (2292865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.66/2.70 % (2292865)CaDiCaL version: 2.1.3 % 12.66/2.70 % (2292865)Termination reason: Instruction limit % 12.66/2.70 % (2292865)Termination phase: Property scanning % 12.66/2.70 % (2292865)Time elapsed: 0.034 s % 12.66/2.70 % (2292865)Peak memory usage: 86 MB % 12.66/2.70 % (2292865)Instructions burned: 41 (million) % 12.66/2.70 % (2292868)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4022828588:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi) % 12.66/2.70 % (2292869)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=909354609:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 12.66/2.70 % (2292841)------------------------------ % 12.66/2.70 % (2292841)------------------------------ % 12.66/2.70 % (2292883)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3510877061:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 12.66/2.70 % (2292849)Instruction limit reached! % 12.66/2.70 % (2292849)------------------------------ % 12.66/2.70 % (2292849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.66/2.70 % (2292849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.66/2.70 % (2292849)CaDiCaL version: 2.1.3 % 12.66/2.70 % (2292849)Termination reason: Instruction limit % 12.66/2.70 % (2292849)Termination phase: Clausification % 12.66/2.70 % (2292849)Time elapsed: 0.341 s % 12.66/2.70 % (2292849)Peak memory usage: 237 MB % 12.66/2.70 % (2292849)Instructions burned: 294 (million) % 12.66/2.70 % (2292883)Instruction limit reached! % 12.66/2.70 % (2292883)------------------------------ % 12.66/2.70 % (2292883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.66/2.70 % (2292883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.66/2.70 % (2292883)CaDiCaL version: 2.1.3 % 12.66/2.70 % (2292883)Termination reason: Instruction limit % 12.66/2.70 % (2292883)Termination phase: Saturation % 12.66/2.70 % (2292883)Time elapsed: 0.047 s % 12.66/2.70 % (2292883)Peak memory usage: 116 MB % 12.66/2.70 % (2292883)Instructions burned: 134 (million) % 12.66/2.70 % (2292868)Refutation not found, incomplete strategy % 12.66/2.70 % (2292868)------------------------------ % 12.66/2.70 % (2292868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.66/2.70 % (2292868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.66/2.70 % (2292868)CaDiCaL version: 2.1.3 % 12.66/2.70 % (2292868)Termination reason: Refutation not found, incomplete strategy % 12.66/2.70 % (2292868)Time elapsed: 0.116 s % 12.66/2.70 % (2292868)Peak memory usage: 94 MB % 12.66/2.70 % (2292868)Instructions burned: 181 (million) % 12.66/2.70 % (2292890)dis+10_1_si=on:random_seed=2776317578:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi) % 12.66/2.70 % (2292889)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=3289644387:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 12.66/2.70 % (2292896)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=153786949:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi) % 12.66/2.70 % (2292889)Refutation not found, incomplete strategy % 12.66/2.70 % (2292889)------------------------------ % 12.66/2.70 % (2292889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.66/2.70 % (2292889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.66/2.70 % (2292889)CaDiCaL version: 2.1.3 % 12.66/2.70 % (2292889)Termination reason: Refutation not found, incomplete strategy % 14.64/2.94 % (2292889)Time elapsed: 0.038 s % 14.64/2.94 % (2292889)Peak memory usage: 112 MB % 14.64/2.94 % (2292889)Instructions burned: 34 (million) % 14.64/2.94 % (2292898)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2954274847:i=141:doe=on:rtra=on_2986 on theBenchmark for (2986ds/141Mi) % 14.64/2.94 % (2292898)Instruction limit reached! % 14.64/2.94 % (2292898)------------------------------ % 14.64/2.94 % (2292898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.94 % (2292898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.94 % (2292898)CaDiCaL version: 2.1.3 % 14.64/2.94 % (2292898)Termination reason: Instruction limit % 14.64/2.94 % (2292898)Termination phase: Saturation % 14.64/2.94 % (2292898)Time elapsed: 0.036 s % 14.64/2.94 % (2292898)Peak memory usage: 93 MB % 14.64/2.94 % (2292898)Instructions burned: 143 (million) % 14.64/2.94 % (2292899)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4270024460:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 14.64/2.94 % (2292899)Instruction limit reached! % 14.64/2.94 % (2292899)------------------------------ % 14.64/2.94 % (2292899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.94 % (2292899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.94 % (2292899)CaDiCaL version: 2.1.3 % 14.64/2.94 % (2292899)Termination reason: Instruction limit % 14.64/2.94 % (2292899)Termination phase: Property scanning % 14.64/2.94 % (2292899)Time elapsed: 0.031 s % 14.64/2.94 % (2292899)Peak memory usage: 88 MB % 14.64/2.94 % (2292899)Instructions burned: 66 (million) % 14.64/2.94 % (2292868)------------------------------ % 14.64/2.94 % (2292868)------------------------------ % 14.64/2.94 % (2292905)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3018516037:i=121:nm=16:rtra=on_2984 on theBenchmark for (2984ds/121Mi) % 14.64/2.94 % (2292896)Instruction limit reached! % 14.64/2.94 % (2292896)------------------------------ % 14.64/2.94 % (2292896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.94 % (2292896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.94 % (2292896)CaDiCaL version: 2.1.3 % 14.64/2.94 % (2292896)Termination reason: Instruction limit % 14.64/2.94 % (2292896)Termination phase: Saturation % 14.64/2.94 % (2292896)Time elapsed: 0.196 s % 14.64/2.94 % (2292896)Peak memory usage: 98 MB % 14.64/2.94 % (2292896)Instructions burned: 384 (million) % 14.64/2.94 % (2292869)Instruction limit reached! % 14.64/2.94 % (2292869)------------------------------ % 14.64/2.94 % (2292869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.94 % (2292869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.94 % (2292869)CaDiCaL version: 2.1.3 % 14.64/2.94 % (2292869)Termination reason: Instruction limit % 14.64/2.94 % (2292869)Termination phase: Saturation % 14.64/2.94 % (2292869)Time elapsed: 0.373 s % 14.64/2.94 % (2292869)Peak memory usage: 144 MB % 14.64/2.94 % (2292869)Instructions burned: 599 (million) % 14.64/2.94 % (2292905)Instruction limit reached! % 14.64/2.94 % (2292905)------------------------------ % 14.64/2.94 % (2292905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.94 % (2292905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.94 % (2292905)CaDiCaL version: 2.1.3 % 14.64/2.94 % (2292905)Termination reason: Instruction limit % 14.64/2.94 % (2292905)Termination phase: Saturation % 14.64/2.94 % (2292905)Time elapsed: 0.028 s % 14.64/2.94 % (2292905)Peak memory usage: 90 MB % 14.64/2.94 % (2292905)Instructions burned: 125 (million) % 14.64/2.94 % (2292889)------------------------------ % 14.64/2.94 % (2292889)------------------------------ % 14.64/2.94 % (2292907)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=564361622:s2a=on:i=128:s2at=5:ins=3:rtra=on_2983 on theBenchmark for (2983ds/128Mi) % 14.64/2.94 % (2292920)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1508140702:s2a=on:i=483:doe=on:nm=32:rtra=on_2982 on theBenchmark for (2982ds/483Mi) % 14.64/2.94 % (2292909)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=2599076777:i=39:ins=3:rtra=on_2983 on theBenchmark for (2983ds/39Mi) % 14.64/2.94 % (2292907)Instruction limit reached! % 14.64/2.94 % (2292907)------------------------------ % 14.64/2.94 % (2292907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.76/3.30 % (2292907)CaDiCaL version: 2.1.3 % 17.76/3.30 % (2292907)Termination reason: Instruction limit % 17.76/3.30 % (2292907)Termination phase: Saturation % 17.76/3.30 % (2292907)Time elapsed: 0.060 s % 17.76/3.30 % (2292907)Peak memory usage: 92 MB % 17.76/3.30 % (2292907)Instructions burned: 129 (million) % 17.76/3.30 % (2292910)dis+1010_1_to=kbo:si=on:random_seed=1346892487:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/175Mi) % 17.76/3.30 % (2292916)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=534917627:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi) % 17.76/3.30 % (2292909)Instruction limit reached! % 17.76/3.30 % (2292909)------------------------------ % 17.76/3.30 % (2292909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.76/3.30 % (2292909)CaDiCaL version: 2.1.3 % 17.76/3.30 % (2292909)Termination reason: Instruction limit % 17.76/3.30 % (2292909)Termination phase: Naming % 17.76/3.30 % (2292909)Time elapsed: 0.018 s % 17.76/3.30 % (2292909)Peak memory usage: 87 MB % 17.76/3.30 % (2292909)Instructions burned: 41 (million) % 17.76/3.30 % (2292935)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1933556677:thitd=on:i=215:nm=0:rtra=on:ev=force_2982 on theBenchmark for (2982ds/215Mi) % 17.76/3.30 % (2292920)Instruction limit reached! % 17.76/3.30 % (2292920)------------------------------ % 17.76/3.30 % (2292920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.76/3.30 % (2292920)CaDiCaL version: 2.1.3 % 17.76/3.30 % (2292920)Termination reason: Instruction limit % 17.76/3.30 % (2292920)Termination phase: Saturation % 17.76/3.30 % (2292920)Time elapsed: 0.165 s % 17.76/3.30 % (2292920)Peak memory usage: 138 MB % 17.76/3.30 % (2292920)Instructions burned: 486 (million) % 17.76/3.30 % (2292975)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1262254909:i=349:rtra=on_2981 on theBenchmark for (2981ds/349Mi) % 17.76/3.30 % (2292910)Instruction limit reached! % 17.76/3.30 % (2292910)------------------------------ % 17.76/3.30 % (2292910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.76/3.30 % (2292910)CaDiCaL version: 2.1.3 % 17.76/3.30 % (2292910)Termination reason: Instruction limit % 17.76/3.30 % (2292910)Termination phase: Clausification % 17.76/3.30 % (2292910)Time elapsed: 0.147 s % 17.76/3.30 % (2292910)Peak memory usage: 155 MB % 17.76/3.30 % (2292910)Instructions burned: 175 (million) % 17.76/3.30 % (2292979)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3368977843:st=2:i=295:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/295Mi) % 17.76/3.30 % (2292979)Refutation not found, incomplete strategy % 17.76/3.30 % (2292979)------------------------------ % 17.76/3.30 % (2292979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.76/3.30 % (2292979)CaDiCaL version: 2.1.3 % 17.76/3.30 % (2292979)Termination reason: Refutation not found, incomplete strategy % 17.76/3.30 % (2292979)Time elapsed: 0.012 s % 17.76/3.30 % (2292979)Peak memory usage: 88 MB % 17.76/3.30 % (2292979)Instructions burned: 28 (million) % 17.76/3.30 % (2292890)Instruction limit reached! % 17.76/3.30 % (2292890)------------------------------ % 17.76/3.30 % (2292890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.76/3.30 % (2292890)CaDiCaL version: 2.1.3 % 17.76/3.30 % (2292890)Termination reason: Instruction limit % 17.76/3.30 % (2292890)Termination phase: Saturation % 17.76/3.30 % (2292890)Time elapsed: 0.554 s % 17.76/3.30 % (2292890)Peak memory usage: 100 MB % 17.76/3.30 % (2292890)Instructions burned: 1001 (million) % 17.76/3.30 % (2292916)Instruction limit reached! % 17.76/3.30 % (2292916)------------------------------ % 17.76/3.30 % (2292916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.76/3.30 % (2292916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.53 % (2292916)CaDiCaL version: 2.1.3 % 18.84/3.53 % (2292916)Termination reason: Instruction limit % 18.84/3.53 % (2292916)Termination phase: Saturation % 18.84/3.53 % (2292916)Time elapsed: 0.211 s % 18.84/3.53 % (2292916)Peak memory usage: 124 MB % 18.84/3.53 % (2292916)Instructions burned: 330 (million) % 18.84/3.53 % (2292935)Instruction limit reached! % 18.84/3.53 % (2292935)------------------------------ % 18.84/3.53 % (2292935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.53 % (2292935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.53 % (2292935)CaDiCaL version: 2.1.3 % 18.84/3.53 % (2292935)Termination reason: Instruction limit % 18.84/3.53 % (2292935)Termination phase: Clausification % 18.84/3.53 % (2292935)Time elapsed: 0.197 s % 18.84/3.53 % (2292935)Peak memory usage: 184 MB % 18.84/3.53 % (2292935)Instructions burned: 215 (million) % 18.84/3.53 % (2293021)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3629358416:i=328:kws=inv_frequency:nm=20:rtra=on_2980 on theBenchmark for (2980ds/328Mi) % 18.84/3.53 % (2293030)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1193025306:i=281:gtgl=2:rtra=on:gtg=all_2980 on theBenchmark for (2980ds/281Mi) % 18.84/3.53 % (2293031)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1578412285:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/484Mi) % 18.84/3.53 % (2293031)Refutation not found, incomplete strategy % 18.84/3.53 % (2293031)------------------------------ % 18.84/3.53 % (2293031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.53 % (2293031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.53 % (2293031)CaDiCaL version: 2.1.3 % 18.84/3.53 % (2293031)Termination reason: Refutation not found, incomplete strategy % 18.84/3.53 % (2293031)Time elapsed: 0.011 s % 18.84/3.53 % (2293031)Peak memory usage: 88 MB % 18.84/3.53 % (2293031)Instructions burned: 27 (million) % 18.84/3.53 % (2292975)Instruction limit reached! % 18.84/3.53 % (2292975)------------------------------ % 18.84/3.53 % (2292975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.53 % (2292975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.53 % (2292975)CaDiCaL version: 2.1.3 % 18.84/3.53 % (2292975)Termination reason: Instruction limit % 18.84/3.53 % (2292975)Termination phase: Saturation % 18.84/3.53 % (2292975)Time elapsed: 0.214 s % 18.84/3.53 % (2292975)Peak memory usage: 126 MB % 18.84/3.53 % (2292975)Instructions burned: 349 (million) % 18.84/3.53 % (2293021)Instruction limit reached! % 18.84/3.53 % (2293021)------------------------------ % 18.84/3.53 % (2293021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.53 % (2293021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.53 % (2293021)CaDiCaL version: 2.1.3 % 18.84/3.53 % (2293021)Termination reason: Instruction limit % 18.84/3.53 % (2293021)Termination phase: Saturation % 18.84/3.53 % (2293021)Time elapsed: 0.105 s % 18.84/3.53 % (2293021)Peak memory usage: 122 MB % 18.84/3.53 % (2293021)Instructions burned: 329 (million) % 18.84/3.53 % (2293032)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=279452553:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2979 on theBenchmark for (2979ds/321Mi) % 18.84/3.53 % (2293032)Refutation not found, incomplete strategy % 18.84/3.53 % (2293032)------------------------------ % 18.84/3.53 % (2293032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.53 % (2293032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.53 % (2293032)CaDiCaL version: 2.1.3 % 18.84/3.53 % (2293032)Termination reason: Refutation not found, incomplete strategy % 18.84/3.53 % (2293032)Time elapsed: 0.037 s % 18.84/3.53 % (2293032)Peak memory usage: 112 MB % 18.84/3.53 % (2293032)Instructions burned: 31 (million) % 18.84/3.53 % (2293034)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2494956837:i=416:rtra=on:gtg=position:ss=axioms_2979 on theBenchmark for (2979ds/416Mi) % 18.84/3.53 % (2292979)------------------------------ % 18.84/3.53 % (2292979)------------------------------ % 18.84/3.53 % (2293034)Refutation not found, incomplete strategy % 18.84/3.53 % (2293034)------------------------------ % 18.84/3.53 % (2293034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.53 % (2293034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.86 % (2293034)CaDiCaL version: 2.1.3 % 21.19/3.86 % (2293034)Termination reason: Refutation not found, incomplete strategy % 21.19/3.86 % (2293034)Time elapsed: 0.037 s % 21.19/3.86 % (2293034)Peak memory usage: 112 MB % 21.19/3.86 % (2293034)Instructions burned: 31 (million) % 21.19/3.86 % (2293068)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=1847179716:avsq=on:i=276:avsqr=1,2:rtra=on_2978 on theBenchmark for (2978ds/276Mi) % 21.19/3.86 % (2293030)Instruction limit reached! % 21.19/3.86 % (2293030)------------------------------ % 21.19/3.86 % (2293030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.19/3.86 % (2293030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.86 % (2293030)CaDiCaL version: 2.1.3 % 21.19/3.86 % (2293030)Termination reason: Instruction limit % 21.19/3.86 % (2293030)Termination phase: Saturation % 21.19/3.86 % (2293030)Time elapsed: 0.170 s % 21.19/3.86 % (2293030)Peak memory usage: 121 MB % 21.19/3.86 % (2293030)Instructions burned: 283 (million) % 21.19/3.86 % (2293066)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1106179438:i=471:thf=on:kws=precedence:rtra=on_2978 on theBenchmark for (2978ds/471Mi) % 21.19/3.86 % (2293068)Instruction limit reached! % 21.19/3.86 % (2293068)------------------------------ % 21.19/3.86 % (2293068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.19/3.86 % (2293068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.86 % (2293068)CaDiCaL version: 2.1.3 % 21.19/3.86 % (2293068)Termination reason: Instruction limit % 21.19/3.86 % (2293068)Termination phase: Saturation % 21.19/3.86 % (2293068)Time elapsed: 0.095 s % 21.19/3.86 % (2293068)Peak memory usage: 135 MB % 21.19/3.86 % (2293068)Instructions burned: 277 (million) % 21.19/3.86 % (2293088)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3620077242:i=375:kws=inv_arity_squared:rtra=on_2977 on theBenchmark for (2977ds/375Mi) % 21.19/3.86 % (2293031)------------------------------ % 21.19/3.86 % (2293031)------------------------------ % 21.19/3.86 % (2293090)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3763833030:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/387Mi) % 21.19/3.86 % (2293032)------------------------------ % 21.19/3.86 % (2293032)------------------------------ % 21.19/3.86 % (2293090)Refutation not found, incomplete strategy % 21.19/3.86 % (2293090)------------------------------ % 21.19/3.86 % (2293090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.19/3.86 % (2293090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.86 % (2293090)CaDiCaL version: 2.1.3 % 21.19/3.86 % (2293090)Termination reason: Refutation not found, incomplete strategy % 21.19/3.86 % (2293090)Time elapsed: 0.038 s % 21.19/3.86 % (2293090)Peak memory usage: 112 MB % 21.19/3.86 % (2293090)Instructions burned: 34 (million) % 21.19/3.86 % (2293092)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3080267717:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2975 on theBenchmark for (2975ds/513Mi) % 21.19/3.86 % (2293034)------------------------------ % 21.19/3.86 % (2293034)------------------------------ % 21.19/3.86 % (2293094)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1010973994:i=334:rtra=on_2975 on theBenchmark for (2975ds/334Mi) % 21.19/3.86 % (2293066)Instruction limit reached! % 21.19/3.86 % (2293066)------------------------------ % 21.19/3.86 % (2293066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.19/3.86 % (2293066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.19/3.86 % (2293066)CaDiCaL version: 2.1.3 % 21.19/3.86 % (2293066)Termination reason: Instruction limit % 21.19/3.86 % (2293066)Termination phase: Saturation % 21.19/3.86 % (2293066)Time elapsed: 0.275 s % 21.19/3.86 % (2293066)Peak memory usage: 127 MB % 21.19/3.86 % (2293066)Instructions burned: 471 (million) % 21.19/3.86 % (2293096)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2418494069:i=359:rtra=on:gtg=exists_top:ss=axioms_2975 on theBenchmark for (2975ds/359Mi) % 21.19/3.86 % (2293088)Instruction limit reached! % 21.19/3.86 % (2293088)------------------------------ % 21.19/3.86 % (2293088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.17/4.33 % (2293088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.17/4.33 % (2293088)CaDiCaL version: 2.1.3 % 25.17/4.33 % (2293088)Termination reason: Instruction limit % 25.17/4.33 % (2293088)Termination phase: Saturation % 25.17/4.33 % (2293088)Time elapsed: 0.231 s % 25.17/4.33 % (2293088)Peak memory usage: 126 MB % 25.17/4.33 % (2293088)Instructions burned: 375 (million) % 25.17/4.33 % (2293096)Refutation not found, incomplete strategy % 25.17/4.33 % (2293096)------------------------------ % 25.17/4.33 % (2293096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.17/4.33 % (2293096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.17/4.33 % (2293096)CaDiCaL version: 2.1.3 % 25.17/4.33 % (2293096)Termination reason: Refutation not found, incomplete strategy % 25.17/4.33 % (2293096)Time elapsed: 0.016 s % 25.17/4.33 % (2293096)Peak memory usage: 89 MB % 25.17/4.33 % (2293096)Instructions burned: 37 (million) % 25.17/4.33 % (2293092)Instruction limit reached! % 25.17/4.33 % (2293092)------------------------------ % 25.17/4.33 % (2293092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.17/4.33 % (2293092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.17/4.33 % (2293092)CaDiCaL version: 2.1.3 % 25.17/4.33 % (2293092)Termination reason: Instruction limit % 25.17/4.33 % (2293092)Termination phase: Saturation % 25.17/4.33 % (2293092)Time elapsed: 0.155 s % 25.17/4.33 % (2293092)Peak memory usage: 99 MB % 25.17/4.33 % (2293092)Instructions burned: 515 (million) % 25.17/4.33 % (2293098)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2890427514:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2974 on theBenchmark for (2974ds/341Mi) % 25.17/4.33 % (2293090)------------------------------ % 25.17/4.33 % (2293090)------------------------------ % 25.17/4.33 % (2293100)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1403683920:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/261Mi) % 25.17/4.33 % (2293103)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1852707687:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2973 on theBenchmark for (2973ds/273Mi) % 25.17/4.33 % (2293102)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=3932153815:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/235Mi) % 25.17/4.33 % (2293094)Instruction limit reached! % 25.17/4.33 % (2293094)------------------------------ % 25.17/4.33 % (2293094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.17/4.33 % (2293094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.17/4.33 % (2293094)CaDiCaL version: 2.1.3 % 25.17/4.33 % (2293094)Termination reason: Instruction limit % 25.17/4.33 % (2293094)Termination phase: Saturation % 25.17/4.33 % (2293094)Time elapsed: 0.226 s % 25.17/4.33 % (2293094)Peak memory usage: 142 MB % 25.17/4.33 % (2293094)Instructions burned: 334 (million) % 25.17/4.33 % (2293100)Refutation not found, incomplete strategy % 25.17/4.33 % (2293100)------------------------------ % 25.17/4.33 % (2293100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.17/4.33 % (2293100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.17/4.33 % (2293100)CaDiCaL version: 2.1.3 % 25.17/4.33 % (2293100)Termination reason: Refutation not found, incomplete strategy % 25.17/4.33 % (2293100)Time elapsed: 0.034 s % 25.17/4.33 % (2293100)Peak memory usage: 112 MB % 25.17/4.33 % (2293100)Instructions burned: 24 (million) % 25.17/4.33 % (2293102)Refutation not found, incomplete strategy % 25.17/4.33 % (2293102)------------------------------ % 25.17/4.33 % (2293102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.17/4.33 % (2293102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.17/4.33 % (2293102)CaDiCaL version: 2.1.3 % 25.17/4.33 % (2293102)Termination reason: Refutation not found, incomplete strategy % 25.17/4.33 % (2293102)Time elapsed: 0.038 s % 25.17/4.33 % (2293102)Peak memory usage: 112 MB % 25.17/4.33 % (2293102)Instructions burned: 34 (million) % 25.17/4.33 % (2293103)Instruction limit reached! % 25.17/4.33 % (2293103)------------------------------ % 25.17/4.33 % (2293103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.10/4.90 % (2293103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.10/4.90 % (2293103)CaDiCaL version: 2.1.3 % 28.10/4.90 % (2293103)Termination reason: Instruction limit % 28.10/4.90 % (2293103)Termination phase: Saturation % 28.10/4.90 % (2293103)Time elapsed: 0.078 s % 28.10/4.90 % (2293103)Peak memory usage: 97 MB % 28.10/4.90 % (2293103)Instructions burned: 274 (million) % 28.10/4.90 % (2293096)------------------------------ % 28.10/4.90 % (2293096)------------------------------ % 28.10/4.90 % (2293098)Instruction limit reached! % 28.10/4.90 % (2293098)------------------------------ % 28.10/4.90 % (2293098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.10/4.90 % (2293098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.10/4.90 % (2293098)CaDiCaL version: 2.1.3 % 28.10/4.90 % (2293098)Termination reason: Instruction limit % 28.10/4.90 % (2293098)Termination phase: Saturation % 28.10/4.90 % (2293098)Time elapsed: 0.205 s % 28.10/4.90 % (2293098)Peak memory usage: 121 MB % 28.10/4.90 % (2293098)Instructions burned: 342 (million) % 28.10/4.90 % (2293105)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1555729368:i=146:doe=on:rtra=on_2972 on theBenchmark for (2972ds/146Mi) % 28.10/4.90 % (2293109)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2871244937:i=4428:doe=on:fsr=off:rtra=on_2971 on theBenchmark for (2971ds/4428Mi) % 28.10/4.90 % (2293110)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=2247171443:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi) % 28.10/4.90 % (2293105)Instruction limit reached! % 28.10/4.90 % (2293105)------------------------------ % 28.10/4.90 % (2293105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.10/4.90 % (2293105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.10/4.90 % (2293105)CaDiCaL version: 2.1.3 % 28.10/4.90 % (2293105)Termination reason: Instruction limit % 28.10/4.90 % (2293105)Termination phase: Saturation % 28.10/4.90 % (2293105)Time elapsed: 0.073 s % 28.10/4.90 % (2293105)Peak memory usage: 93 MB % 28.10/4.90 % (2293105)Instructions burned: 147 (million) % 28.10/4.90 % (2293100)------------------------------ % 28.10/4.90 % (2293100)------------------------------ % 28.10/4.90 % (2293111)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=91560890:i=1052:rtra=on_2970 on theBenchmark for (2970ds/1052Mi) % 28.10/4.90 % (2293112)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1133308243:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2970 on theBenchmark for (2970ds/655Mi) % 28.10/4.90 % (2293102)------------------------------ % 28.10/4.90 % (2293102)------------------------------ % 28.10/4.90 % (2293110)Instruction limit reached! % 28.10/4.90 % (2293110)------------------------------ % 28.10/4.90 % (2293110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.10/4.90 % (2293110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.10/4.90 % (2293110)CaDiCaL version: 2.1.3 % 28.10/4.90 % (2293110)Termination reason: Instruction limit % 28.10/4.90 % (2293110)Termination phase: Saturation % 28.10/4.90 % (2293110)Time elapsed: 0.100 s % 28.10/4.90 % (2293110)Peak memory usage: 135 MB % 28.10/4.90 % (2293110)Instructions burned: 278 (million) % 28.10/4.90 % (2293116)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=791803882:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2970 on theBenchmark for (2970ds/1054Mi) % 28.10/4.90 % (2293116)Refutation not found, incomplete strategy % 28.10/4.90 % (2293116)------------------------------ % 28.10/4.90 % (2293116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.10/4.90 % (2293116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.10/4.90 % (2293116)CaDiCaL version: 2.1.3 % 28.10/4.90 % (2293116)Termination reason: Refutation not found, incomplete strategy % 28.10/4.90 % (2293116)Time elapsed: 0.009 s % 28.10/4.90 % (2293116)Peak memory usage: 88 MB % 28.10/4.90 % (2293116)Instructions burned: 19 (million) % 28.10/4.90 % (2293119)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2925430076:i=107:rtra=on_2969 on theBenchmark for (2969ds/107Mi) % 28.10/4.90 % (2293121)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 31.49/5.15 % (2293121)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=573582141:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 31.49/5.15 % (2293120)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3397837713:s2a=on:i=450:doe=on:nm=32:rtra=on_2969 on theBenchmark for (2969ds/450Mi) % 31.49/5.15 % (2293119)Instruction limit reached! % 31.49/5.15 % (2293119)------------------------------ % 31.49/5.15 % (2293119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.49/5.15 % (2293119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.49/5.15 % (2293119)CaDiCaL version: 2.1.3 % 31.49/5.15 % (2293119)Termination reason: Instruction limit % 31.49/5.15 % (2293119)Termination phase: Saturation % 31.49/5.15 % (2293119)Time elapsed: 0.047 s % 31.49/5.15 % (2293119)Peak memory usage: 91 MB % 31.49/5.15 % (2293119)Instructions burned: 109 (million) % 31.49/5.15 % (2293116)------------------------------ % 31.49/5.15 % (2293116)------------------------------ % 31.49/5.15 % (2293126)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3331106876:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2967 on theBenchmark for (2967ds/130Mi) % 31.49/5.15 % (2293112)Instruction limit reached! % 31.49/5.15 % (2293112)------------------------------ % 31.49/5.15 % (2293112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.49/5.15 % (2293112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.49/5.15 % (2293112)CaDiCaL version: 2.1.3 % 31.49/5.15 % (2293112)Termination reason: Instruction limit % 31.49/5.15 % (2293112)Termination phase: Saturation % 31.49/5.15 % (2293112)Time elapsed: 0.370 s % 31.49/5.15 % (2293112)Peak memory usage: 98 MB % 31.49/5.15 % (2293112)Instructions burned: 655 (million) % 31.49/5.15 % (2293126)Instruction limit reached! % 31.49/5.15 % (2293126)------------------------------ % 31.49/5.15 % (2293126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.49/5.15 % (2293126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.49/5.15 % (2293126)CaDiCaL version: 2.1.3 % 31.49/5.15 % (2293126)Termination reason: Instruction limit % 31.49/5.15 % (2293126)Termination phase: Clausification % 31.49/5.15 % (2293126)Time elapsed: 0.108 s % 31.49/5.15 % (2293126)Peak memory usage: 136 MB % 31.49/5.15 % (2293126)Instructions burned: 131 (million) % 31.49/5.15 % (2293120)Instruction limit reached! % 31.49/5.15 % (2293120)------------------------------ % 31.49/5.15 % (2293120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.49/5.15 % (2293120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.49/5.15 % (2293120)CaDiCaL version: 2.1.3 % 31.49/5.15 % (2293120)Termination reason: Instruction limit % 31.49/5.15 % (2293120)Termination phase: Saturation % 31.49/5.15 % (2293120)Time elapsed: 0.281 s % 31.49/5.15 % (2293120)Peak memory usage: 138 MB % 31.49/5.15 % (2293120)Instructions burned: 450 (million) % 31.49/5.15 % (2293127)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2658189805:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi) % 31.49/5.15 % (2293129)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1633615367:i=491:doe=on:rtra=on:gtg=position_2965 on theBenchmark for (2965ds/491Mi) % 31.49/5.15 % (2293111)Instruction limit reached! % 31.49/5.15 % (2293111)------------------------------ % 31.49/5.15 % (2293111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.49/5.15 % (2293111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.49/5.15 % (2293111)CaDiCaL version: 2.1.3 % 31.49/5.15 % (2293111)Termination reason: Instruction limit % 31.49/5.15 % (2293111)Termination phase: Saturation % 31.49/5.15 % (2293111)Time elapsed: 0.599 s % 31.49/5.15 % (2293111)Peak memory usage: 99 MB % 31.49/5.15 % (2293111)Instructions burned: 1053 (million) % 31.49/5.15 % (2293129)Refutation not found, incomplete strategy % 31.49/5.15 % (2293129)------------------------------ % 31.49/5.15 % (2293129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.49/5.15 % (2293129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.49/5.15 % (2293129)CaDiCaL version: 2.1.3 % 31.49/5.15 % (2293129)Termination reason: Refutation not found, incomplete strategy % 38.08/6.09 % (2293129)Time elapsed: 0.081 s % 38.08/6.09 % (2293129)Peak memory usage: 93 MB % 38.08/6.09 % (2293129)Instructions burned: 168 (million) % 38.08/6.09 % (2293131)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3121613211:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2964 on theBenchmark for (2964ds/307Mi) % 38.08/6.09 % (2293130)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2241948088:s2a=on:i=835:s2at=2:rtra=on_2964 on theBenchmark for (2964ds/835Mi) % 38.08/6.09 % (2293127)Instruction limit reached! % 38.08/6.09 % (2293127)------------------------------ % 38.08/6.09 % (2293127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.08/6.09 % (2293127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/6.09 % (2293127)CaDiCaL version: 2.1.3 % 38.08/6.09 % (2293127)Termination reason: Instruction limit % 38.08/6.09 % (2293127)Termination phase: Saturation % 38.08/6.09 % (2293127)Time elapsed: 0.182 s % 38.08/6.09 % (2293127)Peak memory usage: 122 MB % 38.08/6.09 % (2293127)Instructions burned: 314 (million) % 38.08/6.09 % (2293131)Refutation not found, incomplete strategy % 38.08/6.09 % (2293131)------------------------------ % 38.08/6.09 % (2293131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.08/6.09 % (2293131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/6.09 % (2293131)CaDiCaL version: 2.1.3 % 38.08/6.09 % (2293131)Termination reason: Refutation not found, incomplete strategy % 38.08/6.09 % (2293131)Time elapsed: 0.108 s % 38.08/6.09 % (2293131)Peak memory usage: 93 MB % 38.08/6.09 % (2293131)Instructions burned: 207 (million) % 38.08/6.09 % (2293134)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=69821973:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi) % 38.08/6.09 % (2293121)Instruction limit reached! % 38.08/6.09 % (2293121)------------------------------ % 38.08/6.09 % (2293121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.08/6.09 % (2293121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/6.09 % (2293121)CaDiCaL version: 2.1.3 % 38.08/6.09 % (2293121)Termination reason: Instruction limit % 38.08/6.09 % (2293121)Termination phase: Clausification % 38.08/6.09 % (2293121)Time elapsed: 0.671 s % 38.08/6.09 % (2293121)Peak memory usage: 702 MB % 38.08/6.09 % (2293121)Instructions burned: 1091 (million) % 38.08/6.09 % (2293129)------------------------------ % 38.08/6.09 % (2293129)------------------------------ % 38.08/6.09 % (2293137)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=64008497:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/646Mi) % 38.08/6.09 % (2293131)------------------------------ % 38.08/6.09 % (2293131)------------------------------ % 38.08/6.09 % (2293140)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=1775101858:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2960 on theBenchmark for (2960ds/784Mi) % 38.08/6.09 % (2293141)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=174578448:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2960 on theBenchmark for (2960ds/1131Mi) % 38.08/6.09 % (2293130)Instruction limit reached! % 38.08/6.09 % (2293130)------------------------------ % 38.08/6.09 % (2293130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.08/6.09 % (2293130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/6.09 % (2293130)CaDiCaL version: 2.1.3 % 38.08/6.09 % (2293130)Termination reason: Instruction limit % 38.08/6.09 % (2293130)Termination phase: Saturation % 38.08/6.09 % (2293130)Time elapsed: 0.473 s % 38.08/6.09 % (2293130)Peak memory usage: 101 MB % 38.08/6.09 % (2293130)Instructions burned: 837 (million) % 38.08/6.09 % (2293143)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=3654399557:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/246Mi) % 38.08/6.09 % (2293140)Instruction limit reached! % 38.08/6.09 % (2293140)------------------------------ % 38.08/6.09 % (2293140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.08/6.09 % (2293140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/6.09 % (2293140)CaDiCaL version: 2.1.3 % 38.08/6.09 % (2293140)Termination reason: Instruction limit % 45.13/7.06 % (2293140)Termination phase: Saturation % 45.13/7.06 % (2293140)Time elapsed: 0.212 s % 45.13/7.06 % (2293140)Peak memory usage: 122 MB % 45.13/7.06 % (2293140)Instructions burned: 786 (million) % 45.13/7.06 % (2293143)Refutation not found, incomplete strategy % 45.13/7.06 % (2293143)------------------------------ % 45.13/7.06 % (2293143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.13/7.06 % (2293143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.13/7.06 % (2293143)CaDiCaL version: 2.1.3 % 45.13/7.06 % (2293143)Termination reason: Refutation not found, incomplete strategy % 45.13/7.06 % (2293143)Time elapsed: 0.039 s % 45.13/7.06 % (2293143)Peak memory usage: 111 MB % 45.13/7.06 % (2293143)Instructions burned: 34 (million) % 45.13/7.06 % (2293134)Instruction limit reached! % 45.13/7.06 % (2293134)------------------------------ % 45.13/7.06 % (2293134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.13/7.06 % (2293134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.13/7.06 % (2293134)CaDiCaL version: 2.1.3 % 45.13/7.06 % (2293134)Termination reason: Instruction limit % 45.13/7.06 % (2293134)Termination phase: Saturation % 45.13/7.06 % (2293134)Time elapsed: 0.434 s % 45.13/7.06 % (2293134)Peak memory usage: 126 MB % 45.13/7.06 % (2293134)Instructions burned: 777 (million) % 45.13/7.06 % (2293145)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1012411074:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2958 on theBenchmark for (2958ds/775Mi) % 45.13/7.06 % (2293137)Instruction limit reached! % 45.13/7.06 % (2293137)------------------------------ % 45.13/7.06 % (2293137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.13/7.06 % (2293137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.13/7.06 % (2293137)CaDiCaL version: 2.1.3 % 45.13/7.06 % (2293137)Termination reason: Instruction limit % 45.13/7.06 % (2293137)Termination phase: Saturation % 45.13/7.06 % (2293137)Time elapsed: 0.399 s % 45.13/7.06 % (2293137)Peak memory usage: 145 MB % 45.13/7.06 % (2293137)Instructions burned: 648 (million) % 45.13/7.06 % (2293145)Refutation not found, incomplete strategy % 45.13/7.06 % (2293145)------------------------------ % 45.13/7.06 % (2293145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.13/7.06 % (2293145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.13/7.06 % (2293145)CaDiCaL version: 2.1.3 % 45.13/7.06 % (2293145)Termination reason: Refutation not found, incomplete strategy % 45.13/7.06 % (2293145)Time elapsed: 0.014 s % 45.13/7.06 % (2293145)Peak memory usage: 88 MB % 45.13/7.06 % (2293145)Instructions burned: 31 (million) % 45.13/7.06 % (2293147)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1791330693:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 45.13/7.06 % (2293148)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=169001246:i=102:nm=16:rtra=on_2957 on theBenchmark for (2957ds/102Mi) % 45.13/7.06 % (2293147)Instruction limit reached! % 45.13/7.06 % (2293147)------------------------------ % 45.13/7.06 % (2293147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.13/7.06 % (2293147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.13/7.06 % (2293147)CaDiCaL version: 2.1.3 % 45.13/7.06 % (2293147)Termination reason: Instruction limit % 45.13/7.06 % (2293147)Termination phase: Saturation % 45.13/7.06 % (2293147)Time elapsed: 0.077 s % 45.13/7.06 % (2293147)Peak memory usage: 97 MB % 45.13/7.06 % (2293147)Instructions burned: 274 (million) % 45.13/7.06 % (2293148)Instruction limit reached! % 45.13/7.06 % (2293148)------------------------------ % 45.13/7.06 % (2293148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.13/7.06 % (2293148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.13/7.06 % (2293148)CaDiCaL version: 2.1.3 % 45.13/7.06 % (2293148)Termination reason: Instruction limit % 45.13/7.06 % (2293148)Termination phase: Property scanning % 45.13/7.06 % (2293148)Time elapsed: 0.046 s % 45.13/7.06 % (2293148)Peak memory usage: 89 MB % 45.13/7.06 % (2293148)Instructions burned: 103 (million) % 45.13/7.06 % (2293150)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=281808021:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2956 on theBenchmark for (2956ds/1094Mi) % 45.13/7.06 % (2293143)------------------------------ % 56.34/8.76 % (2293143)------------------------------ % 56.34/8.76 % (2293153)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2959300281:i=6400:doe=on:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/6400Mi) % 56.34/8.76 % (2293145)------------------------------ % 56.34/8.76 % (2293145)------------------------------ % 56.34/8.76 % (2293155)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=4008149964:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/868Mi) % 56.34/8.76 % (2293156)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=2482287100:i=1846:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/1846Mi) % 56.34/8.76 % (2293141)Instruction limit reached! % 56.34/8.76 % (2293141)------------------------------ % 56.34/8.76 % (2293141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.34/8.76 % (2293141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.34/8.76 % (2293141)CaDiCaL version: 2.1.3 % 56.34/8.76 % (2293141)Termination reason: Instruction limit % 56.34/8.76 % (2293141)Termination phase: Saturation % 56.34/8.76 % (2293141)Time elapsed: 0.609 s % 56.34/8.76 % (2293141)Peak memory usage: 126 MB % 56.34/8.76 % (2293141)Instructions burned: 1133 (million) % 56.34/8.76 % (2293156)Refutation not found, incomplete strategy % 56.34/8.76 % (2293156)------------------------------ % 56.34/8.76 % (2293156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.34/8.76 % (2293156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.34/8.76 % (2293156)CaDiCaL version: 2.1.3 % 56.34/8.76 % (2293156)Termination reason: Refutation not found, incomplete strategy % 56.34/8.76 % (2293156)Time elapsed: 0.081 s % 56.34/8.76 % (2293156)Peak memory usage: 93 MB % 56.34/8.76 % (2293156)Instructions burned: 169 (million) % 56.34/8.76 % (2293158)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3272914421:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2954 on theBenchmark for (2954ds/36816Mi) % 56.34/8.76 % (2293161)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2399729833:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2953 on theBenchmark for (2953ds/273Mi) % 56.34/8.76 % (2293156)------------------------------ % 56.34/8.76 % (2293156)------------------------------ % 56.34/8.76 % (2293161)Instruction limit reached! % 56.34/8.76 % (2293161)------------------------------ % 56.34/8.76 % (2293161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.34/8.76 % (2293161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.34/8.76 % (2293161)CaDiCaL version: 2.1.3 % 56.34/8.76 % (2293161)Termination reason: Instruction limit % 56.34/8.76 % (2293161)Termination phase: Saturation % 56.34/8.76 % (2293161)Time elapsed: 0.138 s % 56.34/8.76 % (2293161)Peak memory usage: 97 MB % 56.34/8.76 % (2293161)Instructions burned: 274 (million) % 56.34/8.76 % (2293150)Instruction limit reached! % 56.34/8.76 % (2293150)------------------------------ % 56.34/8.76 % (2293150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.34/8.76 % (2293150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.34/8.76 % (2293150)CaDiCaL version: 2.1.3 % 56.34/8.76 % (2293150)Termination reason: Instruction limit % 56.34/8.76 % (2293150)Termination phase: Saturation % 56.34/8.76 % (2293150)Time elapsed: 0.617 s % 56.34/8.76 % (2293150)Peak memory usage: 104 MB % 56.34/8.76 % (2293150)Instructions burned: 1094 (million) % 56.34/8.76 % (2293164)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=3937214507:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/863Mi) % 56.34/8.76 % (2293165)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=42970643:i=5811:kws=precedence:nm=0:rtra=on_2950 on theBenchmark for (2950ds/5811Mi) % 56.34/8.76 % (2293166)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=3679517908:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2948 on theBenchmark for (2948ds/2216Mi) % 56.34/8.76 % (2293109)Instruction limit reached! % 56.34/8.76 % (2293109)------------------------------ % 56.34/8.76 % (2293109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.80/9.36 % (2293109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.80/9.36 % (2293109)CaDiCaL version: 2.1.3 % 60.80/9.36 % (2293109)Termination reason: Instruction limit % 60.80/9.36 % (2293109)Termination phase: Saturation % 60.80/9.36 % (2293109)Time elapsed: 2.458 s % 60.80/9.36 % (2293109)Peak memory usage: 121 MB % 60.80/9.36 % (2293109)Instructions burned: 4428 (million) % 60.80/9.36 % (2293155)Instruction limit reached! % 60.80/9.36 % (2293155)------------------------------ % 60.80/9.36 % (2293155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.80/9.36 % (2293155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.80/9.36 % (2293155)CaDiCaL version: 2.1.3 % 60.80/9.36 % (2293155)Termination reason: Instruction limit % 60.80/9.36 % (2293155)Termination phase: Clausification % 60.80/9.36 % (2293155)Time elapsed: 0.863 s % 60.80/9.36 % (2293155)Peak memory usage: 548 MB % 60.80/9.36 % (2293155)Instructions burned: 868 (million) % 60.80/9.36 % (2293170)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=323090993:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2945 on theBenchmark for (2945ds/801Mi) % 60.80/9.36 % (2293171)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2814506836:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2944 on theBenchmark for (2944ds/1026Mi) % 60.80/9.36 % (2293171)Refutation not found, incomplete strategy % 60.80/9.36 % (2293171)------------------------------ % 60.80/9.36 % (2293171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.80/9.36 % (2293171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.80/9.36 % (2293171)CaDiCaL version: 2.1.3 % 60.80/9.36 % (2293171)Termination reason: Refutation not found, incomplete strategy % 60.80/9.36 % (2293171)Time elapsed: 0.009 s % 60.80/9.36 % (2293171)Peak memory usage: 88 MB % 60.80/9.36 % (2293171)Instructions burned: 19 (million) % 60.80/9.36 % (2293164)Instruction limit reached! % 60.80/9.36 % (2293164)------------------------------ % 60.80/9.36 % (2293164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.80/9.36 % (2293164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.80/9.36 % (2293164)CaDiCaL version: 2.1.3 % 60.80/9.36 % (2293164)Termination reason: Instruction limit % 60.80/9.36 % (2293164)Termination phase: Clausification % 60.80/9.36 % (2293164)Time elapsed: 0.797 s % 60.80/9.36 % (2293164)Peak memory usage: 481 MB % 60.80/9.36 % (2293164)Instructions burned: 863 (million) % 60.80/9.36 % (2293171)------------------------------ % 60.80/9.36 % (2293171)------------------------------ % 60.80/9.36 % (2293170)Instruction limit reached! % 60.80/9.36 % (2293170)------------------------------ % 60.80/9.36 % (2293170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.80/9.36 % (2293170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.80/9.36 % (2293170)CaDiCaL version: 2.1.3 % 60.80/9.36 % (2293170)Termination reason: Instruction limit % 60.80/9.36 % (2293170)Termination phase: Saturation % 60.80/9.36 % (2293170)Time elapsed: 0.473 s % 60.80/9.36 % (2293170)Peak memory usage: 99 MB % 60.80/9.36 % (2293170)Instructions burned: 802 (million) % 60.80/9.36 % (2293174)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1119527808:i=3509:rtra=on_2940 on theBenchmark for (2940ds/3509Mi) % 60.80/9.36 % (2293175)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1409153325:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2939 on theBenchmark for (2939ds/2127Mi) % 60.80/9.36 % (2293175)Refutation not found, incomplete strategy % 60.80/9.36 % (2293175)------------------------------ % 60.80/9.36 % (2293175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.80/9.36 % (2293175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.80/9.36 % (2293175)CaDiCaL version: 2.1.3 % 60.80/9.36 % (2293175)Termination reason: Refutation not found, incomplete strategy % 60.80/9.36 % (2293175)Time elapsed: 0.012 s % 60.80/9.36 % (2293175)Peak memory usage: 88 MB % 60.80/9.36 % (2293175)Instructions burned: 28 (million) % 60.80/9.36 % (2293176)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=941815767:i=1959:rtra=on:fsd=on:proc=on_2939 on theBenchmark for (2939ds/1959Mi) % 60.80/9.36 % (2293166)Instruction limit reached! % 60.80/9.36 % (2293166)------------------------------ % 60.80/9.36 % (2293166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.56/13.63 % (2293166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.56/13.63 % (2293166)CaDiCaL version: 2.1.3 % 91.56/13.63 % (2293166)Termination reason: Instruction limit % 91.56/13.63 % (2293166)Termination phase: Saturation % 91.56/13.63 % (2293166)Time elapsed: 1.138 s % 91.56/13.63 % (2293166)Peak memory usage: 128 MB % 91.56/13.63 % (2293166)Instructions burned: 2218 (million) % 91.56/13.63 % (2293175)------------------------------ % 91.56/13.63 % (2293175)------------------------------ % 91.56/13.63 % (2293153)Instruction limit reached! % 91.56/13.63 % (2293153)------------------------------ % 91.56/13.63 % (2293153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.56/13.63 % (2293153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.56/13.63 % (2293153)CaDiCaL version: 2.1.3 % 91.56/13.63 % (2293153)Termination reason: Instruction limit % 91.56/13.63 % (2293153)Termination phase: Saturation % 91.56/13.63 % (2293153)Time elapsed: 1.935 s % 91.56/13.63 % (2293153)Peak memory usage: 126 MB % 91.56/13.63 % (2293153)Instructions burned: 6402 (million) % 91.56/13.63 % (2293180)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2374551826:s2a=on:i=3553:nm=0:rtra=on_2935 on theBenchmark for (2935ds/3553Mi) % 91.56/13.63 % (2293182)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=3636900374:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2935 on theBenchmark for (2935ds/4093Mi) % 91.56/13.63 % (2293181)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3903183585:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2935 on theBenchmark for (2935ds/3201Mi) % 91.56/13.63 % (2293176)Instruction limit reached! % 91.56/13.63 % (2293176)------------------------------ % 91.56/13.63 % (2293176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.56/13.63 % (2293176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.56/13.63 % (2293176)CaDiCaL version: 2.1.3 % 91.56/13.63 % (2293176)Termination reason: Instruction limit % 91.56/13.63 % (2293176)Termination phase: Saturation % 91.56/13.63 % (2293176)Time elapsed: 1.014 s % 91.56/13.63 % (2293176)Peak memory usage: 132 MB % 91.56/13.63 % (2293176)Instructions burned: 1959 (million) % 91.56/13.63 % (2293186)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=1224476388:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2927 on theBenchmark for (2927ds/21173Mi) % 91.56/13.63 % (2293186)Refutation not found, incomplete strategy % 91.56/13.63 % (2293186)------------------------------ % 91.56/13.63 % (2293186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.56/13.63 % (2293186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.56/13.63 % (2293186)CaDiCaL version: 2.1.3 % 91.56/13.63 % (2293186)Termination reason: Refutation not found, incomplete strategy % 91.56/13.63 % (2293186)Time elapsed: 0.033 s % 91.56/13.63 % (2293186)Peak memory usage: 113 MB % 91.56/13.63 % (2293186)Instructions burned: 20 (million) % 91.56/13.63 % (2293186)------------------------------ % 91.56/13.63 % (2293186)------------------------------ % 91.56/13.63 % (2293182)Instruction limit reached! % 91.56/13.63 % (2293182)------------------------------ % 91.56/13.63 % (2293182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.56/13.63 % (2293182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.56/13.63 % (2293182)CaDiCaL version: 2.1.3 % 91.56/13.63 % (2293182)Termination reason: Instruction limit % 91.56/13.63 % (2293182)Termination phase: Saturation % 91.56/13.63 % (2293182)Time elapsed: 1.126 s % 91.56/13.63 % (2293182)Peak memory usage: 149 MB % 91.56/13.63 % (2293182)Instructions burned: 4094 (million) % 91.56/13.63 % (2293188)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=994311422:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2922 on theBenchmark for (2922ds/10544Mi) % 91.56/13.63 % (2293189)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1743914652:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2922 on theBenchmark for (2922ds/1262Mi) % 91.56/13.63 % (2293181)Instruction limit reached! % 91.56/13.63 % (2293181)------------------------------ % 91.56/13.63 % (2293181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.56/13.63 % (2293181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.52/15.89 % (2293181)CaDiCaL version: 2.1.3 % 106.52/15.89 % (2293181)Termination reason: Instruction limit % 106.52/15.89 % (2293181)Termination phase: Saturation % 106.52/15.89 % (2293181)Time elapsed: 1.481 s % 106.52/15.89 % (2293181)Peak memory usage: 101 MB % 106.52/15.89 % (2293181)Instructions burned: 3202 (million) % 106.52/15.89 % (2293189)Instruction limit reached! % 106.52/15.89 % (2293189)------------------------------ % 106.52/15.89 % (2293189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.52/15.89 % (2293189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.52/15.89 % (2293189)CaDiCaL version: 2.1.3 % 106.52/15.89 % (2293189)Termination reason: Instruction limit % 106.52/15.89 % (2293189)Termination phase: Saturation % 106.52/15.89 % (2293189)Time elapsed: 0.362 s % 106.52/15.89 % (2293189)Peak memory usage: 128 MB % 106.52/15.89 % (2293189)Instructions burned: 1264 (million) % 106.52/15.89 % (2293192)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2674067314:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2918 on theBenchmark for (2918ds/775Mi) % 106.52/15.89 % (2293192)Refutation not found, incomplete strategy % 106.52/15.89 % (2293192)------------------------------ % 106.52/15.89 % (2293192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.52/15.89 % (2293192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.52/15.89 % (2293192)CaDiCaL version: 2.1.3 % 106.52/15.89 % (2293192)Termination reason: Refutation not found, incomplete strategy % 106.52/15.89 % (2293192)Time elapsed: 0.013 s % 106.52/15.89 % (2293192)Peak memory usage: 88 MB % 106.52/15.89 % (2293192)Instructions burned: 31 (million) % 106.52/15.89 % (2293193)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3436444501:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2917 on theBenchmark for (2917ds/270Mi) % 106.52/15.89 % (2293193)Instruction limit reached! % 106.52/15.89 % (2293193)------------------------------ % 106.52/15.89 % (2293193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.52/15.89 % (2293193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.52/15.89 % (2293193)CaDiCaL version: 2.1.3 % 106.52/15.89 % (2293193)Termination reason: Instruction limit % 106.52/15.89 % (2293193)Termination phase: Saturation % 106.52/15.89 % (2293193)Time elapsed: 0.075 s % 106.52/15.89 % (2293193)Peak memory usage: 97 MB % 106.52/15.89 % (2293193)Instructions burned: 271 (million) % 106.52/15.89 % (2293174)Instruction limit reached! % 106.52/15.89 % (2293174)------------------------------ % 106.52/15.89 % (2293174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.52/15.89 % (2293174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.52/15.89 % (2293174)CaDiCaL version: 2.1.3 % 106.52/15.89 % (2293174)Termination reason: Instruction limit % 106.52/15.89 % (2293174)Termination phase: Saturation % 106.52/15.89 % (2293174)Time elapsed: 2.325 s % 106.52/15.89 % (2293174)Peak memory usage: 113 MB % 106.52/15.89 % (2293174)Instructions burned: 3510 (million) % 106.52/15.89 % (2293192)------------------------------ % 106.52/15.89 % (2293192)------------------------------ % 106.52/15.89 % (2293196)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2632742577:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2915 on theBenchmark for (2915ds/17165Mi) % 106.52/15.89 % (2293197)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2933625778:s2a=on:i=13094:s2at=-1:rtra=on_2915 on theBenchmark for (2915ds/13094Mi) % 106.52/15.89 % (2293180)Instruction limit reached! % 106.52/15.89 % (2293180)------------------------------ % 106.52/15.89 % (2293180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.52/15.89 % (2293180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.52/15.89 % (2293180)CaDiCaL version: 2.1.3 % 106.52/15.89 % (2293180)Termination reason: Instruction limit % 106.52/15.89 % (2293180)Termination phase: NewCNF % 106.52/15.89 % (2293180)Time elapsed: 2.104 s % 106.52/15.89 % (2293180)Peak memory usage: 429 MB % 106.52/15.89 % (2293180)Instructions burned: 3553 (million) % 106.52/15.89 % (2293198)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3836803795:st=2:i=12633:rtra=on:ss=axioms_2914 on theBenchmark for (2914ds/12633Mi) % 106.52/15.89 % (2293198)Refutation not found, incomplete strategy % 106.52/15.89 % (2293198)------------------------------ % 106.52/15.89 % (2293198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.32/18.11 % (2293198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.32/18.11 % (2293198)CaDiCaL version: 2.1.3 % 123.32/18.11 % (2293198)Termination reason: Refutation not found, incomplete strategy % 123.32/18.11 % (2293198)Time elapsed: 0.011 s % 123.32/18.11 % (2293198)Peak memory usage: 88 MB % 123.32/18.11 % (2293198)Instructions burned: 25 (million) % 123.32/18.11 % (2293202)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3472466075:i=1783:rtra=on:gtg=position_2912 on theBenchmark for (2912ds/1783Mi) % 123.32/18.11 % (2293198)------------------------------ % 123.32/18.11 % (2293198)------------------------------ % 123.32/18.11 % (2293204)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=2319450393:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2910 on theBenchmark for (2910ds/5451Mi) % 123.32/18.11 % (2293202)Instruction limit reached! % 123.32/18.11 % (2293202)------------------------------ % 123.32/18.11 % (2293202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.32/18.11 % (2293202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.32/18.11 % (2293202)CaDiCaL version: 2.1.3 % 123.32/18.11 % (2293202)Termination reason: Instruction limit % 123.32/18.11 % (2293202)Termination phase: Saturation % 123.32/18.11 % (2293202)Time elapsed: 0.915 s % 123.32/18.11 % (2293202)Peak memory usage: 127 MB % 123.32/18.11 % (2293202)Instructions burned: 1783 (million) % 123.32/18.11 % (2293206)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=930055970:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2901 on theBenchmark for (2901ds/4975Mi) % 123.32/18.11 % (2293165)Instruction limit reached! % 123.32/18.11 % (2293165)------------------------------ % 123.32/18.11 % (2293165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.32/18.11 % (2293165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.32/18.11 % (2293165)CaDiCaL version: 2.1.3 % 123.32/18.11 % (2293165)Termination reason: Instruction limit % 123.32/18.11 % (2293165)Termination phase: Clausification % 123.32/18.11 % (2293165)Time elapsed: 6.185 s % 123.32/18.11 % (2293165)Peak memory usage: 3405 MB % 123.32/18.11 % (2293165)Instructions burned: 5814 (million) % 123.32/18.11 % (2293208)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=646717876:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2882 on theBenchmark for (2882ds/2076Mi) % 123.32/18.11 % (2293196)Instruction limit reached! % 123.32/18.11 % (2293196)------------------------------ % 123.32/18.11 % (2293196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.32/18.11 % (2293196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.32/18.11 % (2293196)CaDiCaL version: 2.1.3 % 123.32/18.11 % (2293196)Termination reason: Instruction limit % 123.32/18.11 % (2293196)Termination phase: Saturation % 123.32/18.11 % (2293196)Time elapsed: 3.662 s % 123.32/18.11 % (2293196)Peak memory usage: 143 MB % 123.32/18.11 % (2293196)Instructions burned: 17167 (million) % 123.32/18.11 % (2293210)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2171960017:i=5145:rtra=on_2877 on theBenchmark for (2877ds/5145Mi) % 123.32/18.11 % (2293188)Instruction limit reached! % 123.32/18.11 % (2293188)------------------------------ % 123.32/18.11 % (2293188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.32/18.11 % (2293188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.32/18.11 % (2293188)CaDiCaL version: 2.1.3 % 123.32/18.11 % (2293188)Termination reason: Instruction limit % 123.32/18.11 % (2293188)Termination phase: Saturation % 123.32/18.11 % (2293188)Time elapsed: 4.905 s % 123.32/18.11 % (2293188)Peak memory usage: 142 MB % 123.32/18.11 % (2293188)Instructions burned: 10544 (million) % 123.32/18.11 % (2293212)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2866889252:i=3509:rtra=on_2872 on theBenchmark for (2872ds/3509Mi) % 123.32/18.11 % (2293208)Instruction limit reached! % 123.32/18.11 % (2293208)------------------------------ % 123.32/18.11 % (2293208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.32/18.11 % (2293208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.32/18.11 % (2293208)CaDiCaL version: 2.1.3 % 123.32/18.11 % (2293208)Termination reason: Instruction limit % 196.39/28.42 % (2293208)Termination phase: Saturation % 196.39/28.42 % (2293208)Time elapsed: 1.049 s % 196.39/28.42 % (2293208)Peak memory usage: 128 MB % 196.39/28.42 % (2293208)Instructions burned: 2077 (million) % 196.39/28.42 % (2293214)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1923915515:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2870 on theBenchmark for (2870ds/13800Mi) % 196.39/28.42 % (2293214)Refutation not found, incomplete strategy % 196.39/28.42 % (2293214)------------------------------ % 196.39/28.42 % (2293214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.39/28.42 % (2293214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.39/28.42 % (2293214)CaDiCaL version: 2.1.3 % 196.39/28.42 % (2293214)Termination reason: Refutation not found, incomplete strategy % 196.39/28.42 % (2293214)Time elapsed: 0.012 s % 196.39/28.42 % (2293214)Peak memory usage: 88 MB % 196.39/28.42 % (2293214)Instructions burned: 28 (million) % 196.39/28.42 % (2293214)------------------------------ % 196.39/28.42 % (2293214)------------------------------ % 196.39/28.42 % (2293216)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1088007487:i=1412:rtra=on:fsd=on:proc=on_2866 on theBenchmark for (2866ds/1412Mi) % 196.39/28.42 % (2293210)Instruction limit reached! % 196.39/28.42 % (2293210)------------------------------ % 196.39/28.42 % (2293210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.39/28.42 % (2293210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.39/28.42 % (2293210)CaDiCaL version: 2.1.3 % 196.39/28.42 % (2293210)Termination reason: Instruction limit % 196.39/28.42 % (2293210)Termination phase: Saturation % 196.39/28.42 % (2293210)Time elapsed: 1.481 s % 196.39/28.42 % (2293210)Peak memory usage: 113 MB % 196.39/28.42 % (2293210)Instructions burned: 5145 (million) % 196.39/28.42 % (2293326)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 % 196.39/28.42 % (2293326)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3463694653:i=11747:aac=none:nm=0:rtra=on:rawr=on_2861 on theBenchmark for (2861ds/11747Mi) % 196.39/28.42 % (2293216)Instruction limit reached! % 196.39/28.42 % (2293216)------------------------------ % 196.39/28.42 % (2293216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.39/28.42 % (2293216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.39/28.42 % (2293216)CaDiCaL version: 2.1.3 % 196.39/28.42 % (2293216)Termination reason: Instruction limit % 196.39/28.42 % (2293216)Termination phase: Saturation % 196.39/28.42 % (2293216)Time elapsed: 0.775 s % 196.39/28.42 % (2293216)Peak memory usage: 132 MB % 196.39/28.42 % (2293216)Instructions burned: 1414 (million) % 196.39/28.42 % (2293361)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1324886080:s2a=on:i=3553:nm=0:rtra=on_2856 on theBenchmark for (2856ds/3553Mi) % 196.39/28.42 % (2293204)Instruction limit reached! % 196.39/28.42 % (2293204)------------------------------ % 196.39/28.42 % (2293204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.39/28.42 % (2293204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.39/28.42 % (2293204)CaDiCaL version: 2.1.3 % 196.39/28.42 % (2293204)Termination reason: Instruction limit % 196.39/28.42 % (2293204)Termination phase: Clausification % 196.39/28.42 % (2293204)Time elapsed: 5.564 s % 196.39/28.42 % (2293204)Peak memory usage: 3030 MB % 196.39/28.42 % (2293204)Instructions burned: 5451 (million) % 196.39/28.42 % (2293206)Instruction limit reached! % 196.39/28.42 % (2293206)------------------------------ % 196.39/28.42 % (2293206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.39/28.42 % (2293206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.39/28.42 % (2293206)CaDiCaL version: 2.1.3 % 196.39/28.42 % (2293206)Termination reason: Instruction limit % 196.39/28.42 % (2293206)Termination phase: Clausification % 196.39/28.42 % (2293206)Time elapsed: 5.202 s % 196.39/28.42 % (2293206)Peak memory usage: 2870 MB % 196.39/28.42 % (2293206)Instructions burned: 4975 (million) % 196.39/28.42 % (2293212)Instruction limit reached! % 196.39/28.42 % (2293212)------------------------------ % 196.39/28.42 % (2293212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.39/28.42 % (2293212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.39/28.42 % (2293212)CaDiCaL version: 2.1.3 % 196.39/28.42 % (2293212)Termination reason: Instruction limit % 255.37/36.86 % (2293212)Termination phase: Saturation % 255.37/36.86 % (2293212)Time elapsed: 2.287 s % 255.37/36.86 % (2293212)Peak memory usage: 113 MB % 255.37/36.86 % (2293212)Instructions burned: 3510 (million) % 255.37/36.86 % (2293478)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2986345065:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2849 on theBenchmark for (2849ds/3201Mi) % 255.37/36.86 % (2293485)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=3059035760:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2847 on theBenchmark for (2847ds/4081Mi) % 255.37/36.86 % (2293197)Instruction limit reached! % 255.37/36.86 % (2293197)------------------------------ % 255.37/36.86 % (2293197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.37/36.86 % (2293197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.37/36.86 % (2293197)CaDiCaL version: 2.1.3 % 255.37/36.86 % (2293197)Termination reason: Instruction limit % 255.37/36.86 % (2293197)Termination phase: Saturation % 255.37/36.86 % (2293197)Time elapsed: 6.893 s % 255.37/36.86 % (2293197)Peak memory usage: 118 MB % 255.37/36.86 % (2293197)Instructions burned: 13096 (million) % 255.37/36.86 % (2293488)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=3757314703:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2844 on theBenchmark for (2844ds/20260Mi) % 255.37/36.86 % (2293489)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3238640290:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2844 on theBenchmark for (2844ds/58627Mi) % 255.37/36.86 % (2293488)Refutation not found, incomplete strategy % 255.37/36.86 % (2293488)------------------------------ % 255.37/36.86 % (2293488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.37/36.86 % (2293488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.37/36.86 % (2293488)CaDiCaL version: 2.1.3 % 255.37/36.86 % (2293488)Termination reason: Refutation not found, incomplete strategy % 255.37/36.86 % (2293488)Time elapsed: 0.033 s % 255.37/36.86 % (2293488)Peak memory usage: 113 MB % 255.37/36.86 % (2293488)Instructions burned: 20 (million) % 255.37/36.86 % (2293488)------------------------------ % 255.37/36.86 % (2293488)------------------------------ % 255.37/36.86 % (2293493)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=319041642:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/6258Mi) % 255.37/36.86 % (2293361)Instruction limit reached! % 255.37/36.86 % (2293361)------------------------------ % 255.37/36.86 % (2293361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.37/36.86 % (2293361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.37/36.86 % (2293361)CaDiCaL version: 2.1.3 % 255.37/36.86 % (2293361)Termination reason: Instruction limit % 255.37/36.86 % (2293361)Termination phase: NewCNF % 255.37/36.86 % (2293361)Time elapsed: 2.174 s % 255.37/36.86 % (2293361)Peak memory usage: 418 MB % 255.37/36.86 % (2293361)Instructions burned: 3554 (million) % 255.37/36.86 % (2293478)Instruction limit reached! % 255.37/36.86 % (2293478)------------------------------ % 255.37/36.86 % (2293478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.37/36.86 % (2293478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.37/36.86 % (2293478)CaDiCaL version: 2.1.3 % 255.37/36.86 % (2293478)Termination reason: Instruction limit % 255.37/36.86 % (2293478)Termination phase: Saturation % 255.37/36.86 % (2293478)Time elapsed: 1.479 s % 255.37/36.86 % (2293478)Peak memory usage: 101 MB % 255.37/36.86 % (2293478)Instructions burned: 3203 (million) % 255.37/36.86 % (2293495)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2487424229:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2832 on theBenchmark for (2832ds/34001Mi) % 255.37/36.86 % (2293496)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1070123662:s2a=on:i=71622:s2at=-1:rtra=on_2832 on theBenchmark for (2832ds/71622Mi) % 255.37/36.86 % (2293485)Instruction limit reached! % 255.37/36.86 % (2293485)------------------------------ % 255.37/36.86 % (2293485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.37/36.86 % (2293485)Linked with Z3 4.14.0.0 3c47Terminated %------------------------------------------------------------------------------