%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX147_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:58 PM UTC 2026 % Result : Timeout 285.89s 41.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX147_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.26 % Computer : n002.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 15:05:52 UTC 2026 % 0.10/0.26 % CPUTime : % 0.10/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.26/0.32 Running first-order theorem proving % 0.26/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.75/1.75 % (424361)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.75/1.75 % (424374)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=34287833:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.75/1.75 % (424376)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2748810388:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.75/1.75 % (424374)Instruction limit reached! % 4.75/1.75 % (424374)------------------------------ % 4.75/1.75 % (424374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.75/1.75 % (424374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.75/1.75 % (424374)CaDiCaL version: 2.1.3 % 4.75/1.75 % (424374)Termination reason: Instruction limit % 4.75/1.75 % (424374)Termination phase: Property scanning % 4.75/1.75 % (424374)Time elapsed: 0.004 s % 4.75/1.75 % (424374)Peak memory usage: 85 MB % 4.75/1.75 % (424374)Instructions burned: 9 (million) % 4.75/1.75 % (424376)Instruction limit reached! % 4.75/1.75 % (424376)------------------------------ % 4.75/1.75 % (424376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.75/1.75 % (424376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.75/1.75 % (424376)CaDiCaL version: 2.1.3 % 4.75/1.75 % (424376)Termination reason: Instruction limit % 4.75/1.75 % (424376)Termination phase: Saturation % 4.75/1.75 % (424376)Time elapsed: 0.028 s % 4.75/1.75 % (424376)Peak memory usage: 87 MB % 4.75/1.75 % (424376)Instructions burned: 47 (million) % 4.75/1.75 % (424373)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2809305833:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.75/1.75 % (424372)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3225666070:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.75/1.75 % (424371)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1055133667:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.75/1.75 % (424375)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=213440930:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.75/1.75 % (424377)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1149544510:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.75/1.75 % (424375)Instruction limit reached! % 4.75/1.75 % (424375)------------------------------ % 4.75/1.75 % (424375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.75/1.75 % (424375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.75/1.75 % (424375)CaDiCaL version: 2.1.3 % 4.75/1.75 % (424375)Termination reason: Instruction limit % 4.75/1.75 % (424375)Termination phase: Property scanning % 4.75/1.75 % (424375)Time elapsed: 0.004 s % 4.75/1.75 % (424375)Peak memory usage: 85 MB % 4.75/1.75 % (424375)Instructions burned: 4 (million) % 4.75/1.75 % (424371)Instruction limit reached! % 4.75/1.75 % (424371)------------------------------ % 4.75/1.75 % (424371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.75/1.75 % (424371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.75/1.75 % (424371)CaDiCaL version: 2.1.3 % 4.75/1.75 % (424371)Termination reason: Instruction limit % 4.75/1.75 % (424371)Termination phase: shuffling % 4.75/1.75 % (424371)Time elapsed: 0.012 s % 4.75/1.75 % (424371)Peak memory usage: 85 MB % 4.75/1.75 % (424371)Instructions burned: 14 (million) % 4.75/1.75 % (424377)Instruction limit reached! % 4.75/1.75 % (424377)------------------------------ % 4.75/1.75 % (424377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.75/1.75 % (424377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.75/1.75 % (424377)CaDiCaL version: 2.1.3 % 4.75/1.75 % (424377)Termination reason: Instruction limit % 4.75/1.75 % (424377)Termination phase: Property scanning % 4.75/1.75 % (424377)Time elapsed: 0.027 s % 4.75/1.75 % (424377)Peak memory usage: 86 MB % 4.75/1.75 % (424377)Instructions burned: 33 (million) % 4.75/1.75 % (424381)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3856092180:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 4.75/1.75 % (424381)Instruction limit reached! % 4.75/1.75 % (424381)------------------------------ % 4.75/1.75 % (424381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424381)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424381)Termination reason: Instruction limit % 6.24/2.02 % (424381)Termination phase: Property scanning % 6.24/2.02 % (424381)Time elapsed: 0.006 s % 6.24/2.02 % (424381)Peak memory usage: 85 MB % 6.24/2.02 % (424381)Instructions burned: 14 (million) % 6.24/2.02 % (424373)Instruction limit reached! % 6.24/2.02 % (424373)------------------------------ % 6.24/2.02 % (424373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424373)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424373)Termination reason: Instruction limit % 6.24/2.02 % (424373)Termination phase: Saturation % 6.24/2.02 % (424373)Time elapsed: 0.189 s % 6.24/2.02 % (424373)Peak memory usage: 117 MB % 6.24/2.02 % (424373)Instructions burned: 202 (million) % 6.24/2.02 % (424382)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=2510893135:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.24/2.02 % (424382)Instruction limit reached! % 6.24/2.02 % (424382)------------------------------ % 6.24/2.02 % (424382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424382)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424382)Termination reason: Instruction limit % 6.24/2.02 % (424382)Termination phase: Property scanning % 6.24/2.02 % (424382)Time elapsed: 0.025 s % 6.24/2.02 % (424382)Peak memory usage: 86 MB % 6.24/2.02 % (424382)Instructions burned: 29 (million) % 6.24/2.02 % (424389)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2301274107:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 6.24/2.02 % (424390)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2979017896:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 6.24/2.02 % (424372)Instruction limit reached! % 6.24/2.02 % (424372)------------------------------ % 6.24/2.02 % (424372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424372)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424372)Termination reason: Instruction limit % 6.24/2.02 % (424372)Termination phase: Saturation % 6.24/2.02 % (424372)Time elapsed: 0.270 s % 6.24/2.02 % (424372)Peak memory usage: 116 MB % 6.24/2.02 % (424372)Instructions burned: 308 (million) % 6.24/2.02 % (424389)Instruction limit reached! % 6.24/2.02 % (424389)------------------------------ % 6.24/2.02 % (424389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424389)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424389)Termination reason: Instruction limit % 6.24/2.02 % (424389)Termination phase: Property scanning % 6.24/2.02 % (424389)Time elapsed: 0.013 s % 6.24/2.02 % (424389)Peak memory usage: 85 MB % 6.24/2.02 % (424389)Instructions burned: 16 (million) % 6.24/2.02 % (424390)Instruction limit reached! % 6.24/2.02 % (424390)------------------------------ % 6.24/2.02 % (424390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424390)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424390)Termination reason: Instruction limit % 6.24/2.02 % (424390)Termination phase: Property scanning % 6.24/2.02 % (424390)Time elapsed: 0.022 s % 6.24/2.02 % (424390)Peak memory usage: 85 MB % 6.24/2.02 % (424390)Instructions burned: 27 (million) % 6.24/2.02 % (424392)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=1862381515:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.24/2.02 % (424392)Instruction limit reached! % 6.24/2.02 % (424392)------------------------------ % 6.24/2.02 % (424392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.24/2.02 % (424392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.24/2.02 % (424392)CaDiCaL version: 2.1.3 % 6.24/2.02 % (424392)Termination reason: Instruction limit % 8.96/2.27 % (424392)Termination phase: Property scanning % 8.96/2.27 % (424392)Time elapsed: 0.012 s % 8.96/2.27 % (424392)Peak memory usage: 86 MB % 8.96/2.27 % (424392)Instructions burned: 29 (million) % 8.96/2.27 % (424394)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3970123751:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 8.96/2.27 % (424394)Instruction limit reached! % 8.96/2.27 % (424394)------------------------------ % 8.96/2.27 % (424394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.96/2.27 % (424394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.96/2.27 % (424394)CaDiCaL version: 2.1.3 % 8.96/2.27 % (424394)Termination reason: Instruction limit % 8.96/2.27 % (424394)Termination phase: Property scanning % 8.96/2.27 % (424394)Time elapsed: 0.034 s % 8.96/2.27 % (424394)Peak memory usage: 87 MB % 8.96/2.27 % (424394)Instructions burned: 87 (million) % 8.96/2.27 % (424397)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=39271258:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 8.96/2.27 % (424395)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=679872590:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 8.96/2.27 % (424395)Instruction limit reached! % 8.96/2.27 % (424395)------------------------------ % 8.96/2.27 % (424395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.96/2.27 % (424395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.96/2.27 % (424395)CaDiCaL version: 2.1.3 % 8.96/2.27 % (424395)Termination reason: Instruction limit % 8.96/2.27 % (424395)Termination phase: Property scanning % 8.96/2.27 % (424395)Time elapsed: 0.003 s % 8.96/2.27 % (424395)Peak memory usage: 85 MB % 8.96/2.27 % (424395)Instructions burned: 2 (million) % 8.96/2.27 % (424397)Refutation not found, incomplete strategy % 8.96/2.27 % (424397)------------------------------ % 8.96/2.27 % (424397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.96/2.27 % (424397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.96/2.27 % (424397)CaDiCaL version: 2.1.3 % 8.96/2.27 % (424397)Termination reason: Refutation not found, incomplete strategy % 8.96/2.27 % (424397)Time elapsed: 0.018 s % 8.96/2.27 % (424397)Peak memory usage: 88 MB % 8.96/2.27 % (424397)Instructions burned: 47 (million) % 8.96/2.27 % (424402)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=288906463:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 8.96/2.27 % (424401)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3789731377:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 8.96/2.27 % (424403)lrs+10_1_thi=all:si=on:fd=off:random_seed=3916237853:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 8.96/2.27 % (424401)Instruction limit reached! % 8.96/2.27 % (424401)------------------------------ % 8.96/2.27 % (424401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.96/2.27 % (424401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.96/2.27 % (424401)CaDiCaL version: 2.1.3 % 8.96/2.27 % (424401)Termination reason: Instruction limit % 8.96/2.27 % (424401)Termination phase: Property scanning % 8.96/2.27 % (424401)Time elapsed: 0.004 s % 8.96/2.27 % (424401)Peak memory usage: 85 MB % 8.96/2.27 % (424401)Instructions burned: 4 (million) % 8.96/2.27 % (424408)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2114457427:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 8.96/2.27 % (424408)Instruction limit reached! % 8.96/2.27 % (424408)------------------------------ % 8.96/2.27 % (424408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.96/2.27 % (424408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.96/2.27 % (424408)CaDiCaL version: 2.1.3 % 8.96/2.27 % (424408)Termination reason: Instruction limit % 8.96/2.27 % (424408)Termination phase: Property scanning % 8.96/2.27 % (424408)Time elapsed: 0.001 s % 8.96/2.27 % (424408)Peak memory usage: 85 MB % 8.96/2.27 % (424408)Instructions burned: 2 (million) % 8.96/2.27 % (424407)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=2715018115:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 10.74/2.53 % (424407)Instruction limit reached! % 10.74/2.53 % (424407)------------------------------ % 10.74/2.53 % (424407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.53 % (424407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.53 % (424407)CaDiCaL version: 2.1.3 % 10.74/2.53 % (424407)Termination reason: Instruction limit % 10.74/2.53 % (424407)Termination phase: Property scanning % 10.74/2.53 % (424407)Time elapsed: 0.007 s % 10.74/2.53 % (424407)Peak memory usage: 85 MB % 10.74/2.53 % (424407)Instructions burned: 8 (million) % 10.74/2.53 % (424403)Instruction limit reached! % 10.74/2.53 % (424403)------------------------------ % 10.74/2.53 % (424403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.53 % (424403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.53 % (424403)CaDiCaL version: 2.1.3 % 10.74/2.53 % (424403)Termination reason: Instruction limit % 10.74/2.53 % (424403)Termination phase: Property scanning % 10.74/2.53 % (424403)Time elapsed: 0.042 s % 10.74/2.53 % (424403)Peak memory usage: 86 MB % 10.74/2.53 % (424403)Instructions burned: 54 (million) % 10.74/2.53 % (424402)Instruction limit reached! % 10.74/2.53 % (424402)------------------------------ % 10.74/2.53 % (424402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.53 % (424402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.53 % (424402)CaDiCaL version: 2.1.3 % 10.74/2.53 % (424402)Termination reason: Instruction limit % 10.74/2.53 % (424402)Termination phase: Saturation % 10.74/2.53 % (424402)Time elapsed: 0.050 s % 10.74/2.53 % (424402)Peak memory usage: 86 MB % 10.74/2.53 % (424402)Instructions burned: 67 (million) % 10.74/2.53 % (424411)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3776254830:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 10.74/2.53 % (424411)Instruction limit reached! % 10.74/2.53 % (424411)------------------------------ % 10.74/2.53 % (424411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.53 % (424411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.53 % (424411)CaDiCaL version: 2.1.3 % 10.74/2.53 % (424411)Termination reason: Instruction limit % 10.74/2.53 % (424411)Termination phase: shuffling % 10.74/2.53 % (424411)Time elapsed: 0.002 s % 10.74/2.53 % (424411)Peak memory usage: 85 MB % 10.74/2.53 % (424411)Instructions burned: 2 (million) % 10.74/2.53 % (424419)dis+10_1_si=on:random_seed=2282047430:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.74/2.53 % (424419)Instruction limit reached! % 10.74/2.53 % (424419)------------------------------ % 10.74/2.53 % (424419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.53 % (424419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.53 % (424419)CaDiCaL version: 2.1.3 % 10.74/2.53 % (424419)Termination reason: Instruction limit % 10.74/2.53 % (424419)Termination phase: Property scanning % 10.74/2.53 % (424419)Time elapsed: 0.005 s % 10.74/2.53 % (424419)Peak memory usage: 85 MB % 10.74/2.53 % (424419)Instructions burned: 11 (million) % 10.74/2.53 % (424397)------------------------------ % 10.74/2.53 % (424397)------------------------------ % 10.74/2.53 % (424423)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4208824623:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 10.74/2.53 % (424416)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1172222349:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 10.74/2.53 % (424423)Instruction limit reached! % 10.74/2.53 % (424423)------------------------------ % 10.74/2.53 % (424423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.74/2.53 % (424423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.74/2.53 % (424423)CaDiCaL version: 2.1.3 % 10.74/2.53 % (424423)Termination reason: Instruction limit % 10.74/2.53 % (424423)Termination phase: shuffling % 10.74/2.53 % (424423)Time elapsed: 0.002 s % 10.74/2.53 % (424423)Peak memory usage: 85 MB % 10.74/2.53 % (424423)Instructions burned: 2 (million) % 10.74/2.53 % (424420)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4211043252:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 10.74/2.53 % (424422)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3522932996: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_2991 on theBenchmark for (2991ds/35Mi) % 15.24/3.06 % (424420)Instruction limit reached! % 15.24/3.06 % (424420)------------------------------ % 15.24/3.06 % (424420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.24/3.06 % (424420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.24/3.06 % (424420)CaDiCaL version: 2.1.3 % 15.24/3.06 % (424420)Termination reason: Instruction limit % 15.24/3.06 % (424420)Termination phase: Property scanning % 15.24/3.06 % (424420)Time elapsed: 0.022 s % 15.24/3.06 % (424420)Peak memory usage: 86 MB % 15.24/3.06 % (424420)Instructions burned: 26 (million) % 15.24/3.06 % (424422)Instruction limit reached! % 15.24/3.06 % (424422)------------------------------ % 15.24/3.06 % (424422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.24/3.06 % (424422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.24/3.06 % (424422)CaDiCaL version: 2.1.3 % 15.24/3.06 % (424422)Termination reason: Instruction limit % 15.24/3.06 % (424422)Termination phase: Property scanning % 15.24/3.06 % (424422)Time elapsed: 0.030 s % 15.24/3.06 % (424422)Peak memory usage: 86 MB % 15.24/3.06 % (424422)Instructions burned: 36 (million) % 15.24/3.06 % (424427)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3243592541:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 15.24/3.06 % (424416)Instruction limit reached! % 15.24/3.06 % (424416)------------------------------ % 15.24/3.06 % (424416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.24/3.06 % (424416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.24/3.06 % (424416)CaDiCaL version: 2.1.3 % 15.24/3.06 % (424416)Termination reason: Instruction limit % 15.24/3.06 % (424416)Termination phase: Saturation % 15.24/3.06 % (424416)Time elapsed: 0.128 s % 15.24/3.06 % (424416)Peak memory usage: 113 MB % 15.24/3.06 % (424416)Instructions burned: 127 (million) % 15.24/3.06 % (424425)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=381781346:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 15.24/3.06 % (424425)Instruction limit reached! % 15.24/3.06 % (424425)------------------------------ % 15.24/3.06 % (424425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.24/3.06 % (424425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.24/3.06 % (424425)CaDiCaL version: 2.1.3 % 15.24/3.06 % (424425)Termination reason: Instruction limit % 15.24/3.06 % (424425)Termination phase: Property scanning % 15.24/3.06 % (424425)Time elapsed: 0.007 s % 15.24/3.06 % (424425)Peak memory usage: 85 MB % 15.24/3.06 % (424425)Instructions burned: 8 (million) % 15.24/3.06 % (424427)Refutation not found, incomplete strategy % 15.24/3.06 % (424427)------------------------------ % 15.24/3.06 % (424427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.24/3.06 % (424427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.24/3.06 % (424427)CaDiCaL version: 2.1.3 % 15.24/3.06 % (424427)Termination reason: Refutation not found, incomplete strategy % 15.24/3.06 % (424427)Time elapsed: 0.041 s % 15.24/3.06 % (424427)Peak memory usage: 89 MB % 15.24/3.06 % (424427)Instructions burned: 105 (million) % 15.24/3.06 % (424431)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3853314418:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 15.24/3.06 % (424432)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3687883929:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 15.24/3.06 % (424431)Instruction limit reached! % 15.24/3.06 % (424431)------------------------------ % 15.24/3.06 % (424431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.24/3.06 % (424431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.24/3.06 % (424431)CaDiCaL version: 2.1.3 % 15.24/3.06 % (424431)Termination reason: Instruction limit % 15.24/3.06 % (424431)Termination phase: shuffling % 15.24/3.06 % (424431)Time elapsed: 0.012 s % 15.24/3.06 % (424431)Peak memory usage: 85 MB % 15.24/3.06 % (424431)Instructions burned: 14 (million) % 15.24/3.06 % (424435)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=250254329:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 15.24/3.06 % (424440)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=3646128150:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 16.42/3.31 % (424432)Refutation not found, incomplete strategy % 16.42/3.31 % (424432)------------------------------ % 16.42/3.31 % (424432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.42/3.31 % (424432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.42/3.31 % (424432)CaDiCaL version: 2.1.3 % 16.42/3.31 % (424432)Termination reason: Refutation not found, incomplete strategy % 16.42/3.31 % (424432)Time elapsed: 0.077 s % 16.42/3.31 % (424432)Peak memory usage: 112 MB % 16.42/3.31 % (424432)Instructions burned: 65 (million) % 16.42/3.31 % (424435)Instruction limit reached! % 16.42/3.31 % (424435)------------------------------ % 16.42/3.31 % (424435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.42/3.31 % (424435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.42/3.31 % (424435)CaDiCaL version: 2.1.3 % 16.42/3.31 % (424435)Termination reason: Instruction limit % 16.42/3.31 % (424435)Termination phase: Property scanning % 16.42/3.31 % (424435)Time elapsed: 0.009 s % 16.42/3.31 % (424435)Peak memory usage: 85 MB % 16.42/3.31 % (424435)Instructions burned: 10 (million) % 16.42/3.31 % (424436)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3725128062:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 16.42/3.31 % (424439)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=3747661017:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi) % 16.42/3.31 % (424427)------------------------------ % 16.42/3.31 % (424427)------------------------------ % 16.42/3.31 % (424436)Instruction limit reached! % 16.42/3.31 % (424436)------------------------------ % 16.42/3.31 % (424436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.42/3.31 % (424436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.42/3.31 % (424436)CaDiCaL version: 2.1.3 % 16.42/3.31 % (424436)Termination reason: Instruction limit % 16.42/3.31 % (424436)Termination phase: Saturation % 16.42/3.31 % (424436)Time elapsed: 0.080 s % 16.42/3.31 % (424436)Peak memory usage: 113 MB % 16.42/3.31 % (424436)Instructions burned: 71 (million) % 16.42/3.31 % (424439)Instruction limit reached! % 16.42/3.31 % (424439)------------------------------ % 16.42/3.31 % (424439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.42/3.31 % (424439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.42/3.31 % (424439)CaDiCaL version: 2.1.3 % 16.42/3.31 % (424439)Termination reason: Instruction limit % 16.42/3.31 % (424439)Termination phase: Saturation % 16.42/3.31 % (424439)Time elapsed: 0.050 s % 16.42/3.31 % (424439)Peak memory usage: 86 MB % 16.42/3.31 % (424439)Instructions burned: 75 (million) % 16.42/3.31 % (424443)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2639996677:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 16.42/3.31 % (424440)Instruction limit reached! % 16.42/3.31 % (424440)------------------------------ % 16.42/3.31 % (424440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.42/3.31 % (424440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.42/3.31 % (424440)CaDiCaL version: 2.1.3 % 16.42/3.31 % (424440)Termination reason: Instruction limit % 16.42/3.31 % (424440)Termination phase: Saturation % 16.42/3.31 % (424440)Time elapsed: 0.204 s % 16.42/3.31 % (424440)Peak memory usage: 90 MB % 16.42/3.31 % (424440)Instructions burned: 295 (million) % 16.42/3.31 % (424446)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=514270106:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 16.42/3.31 % (424443)Instruction limit reached! % 16.42/3.31 % (424443)------------------------------ % 16.42/3.31 % (424443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.42/3.31 % (424443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.42/3.31 % (424443)CaDiCaL version: 2.1.3 % 16.42/3.31 % (424443)Termination reason: Instruction limit % 16.42/3.31 % (424443)Termination phase: Property scanning % 16.42/3.31 % (424443)Time elapsed: 0.084 s % 16.42/3.31 % (424443)Peak memory usage: 88 MB % 16.42/3.31 % (424443)Instructions burned: 130 (million) % 16.42/3.31 % (424450)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=305300014:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 17.78/3.71 % (424450)Instruction limit reached! % 17.78/3.71 % (424450)------------------------------ % 17.78/3.71 % (424450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.71 % (424450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.71 % (424450)CaDiCaL version: 2.1.3 % 17.78/3.71 % (424450)Termination reason: Instruction limit % 17.78/3.71 % (424450)Termination phase: Property scanning % 17.78/3.71 % (424450)Time elapsed: 0.017 s % 17.78/3.71 % (424450)Peak memory usage: 86 MB % 17.78/3.71 % (424450)Instructions burned: 41 (million) % 17.78/3.71 % (424451)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=26356532:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi) % 17.78/3.71 % (424451)Refutation not found, incomplete strategy % 17.78/3.71 % (424451)------------------------------ % 17.78/3.71 % (424451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.71 % (424451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.71 % (424451)CaDiCaL version: 2.1.3 % 17.78/3.71 % (424451)Termination reason: Refutation not found, incomplete strategy % 17.78/3.71 % (424451)Time elapsed: 0.060 s % 17.78/3.71 % (424451)Peak memory usage: 90 MB % 17.78/3.71 % (424451)Instructions burned: 138 (million) % 17.78/3.71 % (424452)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3921017878:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi) % 17.78/3.71 % (424432)------------------------------ % 17.78/3.71 % (424432)------------------------------ % 17.78/3.71 % (424446)Instruction limit reached! % 17.78/3.71 % (424446)------------------------------ % 17.78/3.71 % (424446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.71 % (424446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.71 % (424446)CaDiCaL version: 2.1.3 % 17.78/3.71 % (424446)Termination reason: Instruction limit % 17.78/3.71 % (424446)Termination phase: Saturation % 17.78/3.71 % (424446)Time elapsed: 0.154 s % 17.78/3.71 % (424446)Peak memory usage: 130 MB % 17.78/3.71 % (424446)Instructions burned: 131 (million) % 17.78/3.72 % (424454)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2775176152:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi) % 17.78/3.72 % (424459)dis+10_1_si=on:random_seed=1259644108:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi) % 17.78/3.72 % (424458)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=1772563186:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 17.78/3.72 % (424454)Instruction limit reached! % 17.78/3.72 % (424454)------------------------------ % 17.78/3.72 % (424454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.72 % (424454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.72 % (424454)CaDiCaL version: 2.1.3 % 17.78/3.72 % (424454)Termination reason: Instruction limit % 17.78/3.72 % (424454)Termination phase: Saturation % 17.78/3.72 % (424454)Time elapsed: 0.125 s % 17.78/3.72 % (424454)Peak memory usage: 113 MB % 17.78/3.72 % (424454)Instructions burned: 132 (million) % 17.78/3.72 % (424458)Refutation not found, incomplete strategy % 17.78/3.72 % (424458)------------------------------ % 17.78/3.72 % (424458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.72 % (424458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.72 % (424458)CaDiCaL version: 2.1.3 % 17.78/3.72 % (424458)Termination reason: Refutation not found, incomplete strategy % 17.78/3.72 % (424458)Time elapsed: 0.073 s % 17.78/3.72 % (424458)Peak memory usage: 112 MB % 17.78/3.72 % (424458)Instructions burned: 68 (million) % 17.78/3.72 % (424451)------------------------------ % 17.78/3.72 % (424451)------------------------------ % 17.78/3.72 % (424463)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3277996368:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 17.78/3.72 % (424464)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=371010467:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi) % 17.78/3.72 % (424464)Instruction limit reached! % 17.78/3.72 % (424464)------------------------------ % 22.24/4.05 % (424464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424464)CaDiCaL version: 2.1.3 % 22.24/4.05 % (424464)Termination reason: Instruction limit % 22.24/4.05 % (424464)Termination phase: Saturation % 22.24/4.05 % (424464)Time elapsed: 0.106 s % 22.24/4.05 % (424464)Peak memory usage: 90 MB % 22.24/4.05 % (424464)Instructions burned: 142 (million) % 22.24/4.05 % (424459)Instruction limit reached! % 22.24/4.05 % (424459)------------------------------ % 22.24/4.05 % (424459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424459)CaDiCaL version: 2.1.3 % 22.24/4.05 % (424459)Termination reason: Instruction limit % 22.24/4.05 % (424459)Termination phase: Saturation % 22.24/4.05 % (424459)Time elapsed: 0.363 s % 22.24/4.05 % (424459)Peak memory usage: 92 MB % 22.24/4.05 % (424459)Instructions burned: 1000 (million) % 22.24/4.05 % (424469)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=370768195:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 22.24/4.05 % (424469)Instruction limit reached! % 22.24/4.05 % (424469)------------------------------ % 22.24/4.05 % (424469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424469)CaDiCaL version: 2.1.3 % 22.24/4.05 % (424469)Termination reason: Instruction limit % 22.24/4.05 % (424469)Termination phase: Saturation % 22.24/4.05 % (424469)Time elapsed: 0.049 s % 22.24/4.05 % (424469)Peak memory usage: 88 MB % 22.24/4.05 % (424469)Instructions burned: 65 (million) % 22.24/4.05 % (424471)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1110480686:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 22.24/4.05 % (424452)Instruction limit reached! % 22.24/4.05 % (424452)------------------------------ % 22.24/4.05 % (424452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424452)CaDiCaL version: 2.1.3 % 22.24/4.05 % (424452)Termination reason: Instruction limit % 22.24/4.05 % (424452)Termination phase: Saturation % 22.24/4.05 % (424452)Time elapsed: 0.537 s % 22.24/4.05 % (424452)Peak memory usage: 138 MB % 22.24/4.05 % (424452)Instructions burned: 599 (million) % 22.24/4.05 % (424463)Instruction limit reached! % 22.24/4.05 % (424463)------------------------------ % 22.24/4.05 % (424463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424463)CaDiCaL version: 2.1.3 % 22.24/4.05 % (424463)Termination reason: Instruction limit % 22.24/4.05 % (424463)Termination phase: Saturation % 22.24/4.05 % (424463)Time elapsed: 0.285 s % 22.24/4.05 % (424463)Peak memory usage: 91 MB % 22.24/4.05 % (424463)Instructions burned: 383 (million) % 22.24/4.05 % (424458)------------------------------ % 22.24/4.05 % (424458)------------------------------ % 22.24/4.05 % (424471)Instruction limit reached! % 22.24/4.05 % (424471)------------------------------ % 22.24/4.05 % (424471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424471)CaDiCaL version: 2.1.3 % 22.24/4.05 % (424471)Termination reason: Instruction limit % 22.24/4.05 % (424471)Termination phase: Saturation % 22.24/4.05 % (424471)Time elapsed: 0.092 s % 22.24/4.05 % (424471)Peak memory usage: 90 MB % 22.24/4.05 % (424471)Instructions burned: 122 (million) % 22.24/4.05 % (424475)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=1711140371:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 22.24/4.05 % (424476)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=1012489244:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi) % 22.24/4.05 % (424476)Instruction limit reached! % 22.24/4.05 % (424476)------------------------------ % 22.24/4.05 % (424476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.24/4.05 % (424476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.24/4.05 % (424476)CaDiCaL version: 2.1.3 % 24.88/4.58 % (424476)Termination reason: Instruction limit % 24.88/4.58 % (424476)Termination phase: Property scanning % 24.88/4.58 % (424476)Time elapsed: 0.017 s % 24.88/4.58 % (424476)Peak memory usage: 86 MB % 24.88/4.58 % (424476)Instructions burned: 41 (million) % 24.88/4.58 % (424475)Instruction limit reached! % 24.88/4.58 % (424475)------------------------------ % 24.88/4.58 % (424475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.88/4.58 % (424475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.88/4.58 % (424475)CaDiCaL version: 2.1.3 % 24.88/4.58 % (424475)Termination reason: Instruction limit % 24.88/4.58 % (424475)Termination phase: Saturation % 24.88/4.58 % (424475)Time elapsed: 0.098 s % 24.88/4.58 % (424475)Peak memory usage: 90 MB % 24.88/4.58 % (424475)Instructions burned: 128 (million) % 24.88/4.58 % (424479)dis+1010_1_to=kbo:si=on:random_seed=2937919800:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi) % 24.88/4.58 % (424480)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=185385879:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/329Mi) % 24.88/4.58 % (424481)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1471854336:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 24.88/4.58 % (424482)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3045046644:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi) % 24.88/4.58 % (424483)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1201321673:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi) % 24.88/4.58 % (424486)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1705656064:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi) % 24.88/4.58 % (424479)Instruction limit reached! % 24.88/4.58 % (424479)------------------------------ % 24.88/4.58 % (424479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.88/4.58 % (424479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.88/4.58 % (424479)CaDiCaL version: 2.1.3 % 24.88/4.58 % (424479)Termination reason: Instruction limit % 24.88/4.58 % (424479)Termination phase: Saturation % 24.88/4.58 % (424479)Time elapsed: 0.138 s % 24.88/4.58 % (424479)Peak memory usage: 91 MB % 24.88/4.58 % (424479)Instructions burned: 176 (million) % 24.88/4.58 % (424486)Refutation not found, incomplete strategy % 24.88/4.58 % (424486)------------------------------ % 24.88/4.58 % (424486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.88/4.58 % (424486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.88/4.58 % (424486)CaDiCaL version: 2.1.3 % 24.88/4.58 % (424486)Termination reason: Refutation not found, incomplete strategy % 24.88/4.58 % (424486)Time elapsed: 0.022 s % 24.88/4.58 % (424486)Peak memory usage: 88 MB % 24.88/4.58 % (424486)Instructions burned: 63 (million) % 24.88/4.58 % (424488)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1645174420:i=328:kws=inv_frequency:nm=20:rtra=on_2975 on theBenchmark for (2975ds/328Mi) % 24.88/4.58 % (424480)Instruction limit reached! % 24.88/4.58 % (424480)------------------------------ % 24.88/4.58 % (424480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.88/4.58 % (424480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.88/4.58 % (424480)CaDiCaL version: 2.1.3 % 24.88/4.58 % (424480)Termination reason: Instruction limit % 24.88/4.58 % (424480)Termination phase: Saturation % 24.88/4.58 % (424480)Time elapsed: 0.277 s % 24.88/4.58 % (424480)Peak memory usage: 118 MB % 24.88/4.58 % (424480)Instructions burned: 330 (million) % 24.88/4.58 % (424482)Instruction limit reached! % 24.88/4.58 % (424482)------------------------------ % 24.88/4.58 % (424482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.88/4.58 % (424482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.88/4.58 % (424482)CaDiCaL version: 2.1.3 % 24.88/4.58 % (424482)Termination reason: Instruction limit % 24.88/4.58 % (424482)Termination phase: Saturation % 24.88/4.58 % (424482)Time elapsed: 0.200 s % 24.88/4.58 % (424482)Peak memory usage: 131 MB % 24.88/4.58 % (424482)Instructions burned: 219 (million) % 24.88/4.58 % (424495)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2028204310:i=281:gtgl=2:rtra=on:gtg=all_2973 on theBenchmark for (2973ds/281Mi) % 25.98/4.95 % (424486)------------------------------ % 25.98/4.95 % (424486)------------------------------ % 25.98/4.95 % (424483)Instruction limit reached! % 25.98/4.95 % (424483)------------------------------ % 25.98/4.95 % (424483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.98/4.95 % (424483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.98/4.95 % (424483)CaDiCaL version: 2.1.3 % 25.98/4.95 % (424483)Termination reason: Instruction limit % 25.98/4.95 % (424483)Termination phase: Saturation % 25.98/4.95 % (424483)Time elapsed: 0.298 s % 25.98/4.95 % (424483)Peak memory usage: 117 MB % 25.98/4.95 % (424483)Instructions burned: 349 (million) % 25.98/4.95 % (424481)Instruction limit reached! % 25.98/4.95 % (424481)------------------------------ % 25.98/4.95 % (424481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.98/4.95 % (424481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.98/4.95 % (424481)CaDiCaL version: 2.1.3 % 25.98/4.95 % (424481)Termination reason: Instruction limit % 25.98/4.95 % (424481)Termination phase: Saturation % 25.98/4.95 % (424481)Time elapsed: 0.434 s % 25.98/4.95 % (424481)Peak memory usage: 136 MB % 25.98/4.95 % (424481)Instructions burned: 483 (million) % 25.98/4.95 % (424488)Instruction limit reached! % 25.98/4.95 % (424488)------------------------------ % 25.98/4.95 % (424488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.98/4.95 % (424488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.98/4.95 % (424488)CaDiCaL version: 2.1.3 % 25.98/4.95 % (424488)Termination reason: Instruction limit % 25.98/4.95 % (424488)Termination phase: Saturation % 25.98/4.95 % (424488)Time elapsed: 0.278 s % 25.98/4.95 % (424488)Peak memory usage: 115 MB % 25.98/4.95 % (424488)Instructions burned: 328 (million) % 25.98/4.95 % (424495)Instruction limit reached! % 25.98/4.95 % (424495)------------------------------ % 25.98/4.95 % (424495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.98/4.95 % (424495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.98/4.95 % (424495)CaDiCaL version: 2.1.3 % 25.98/4.95 % (424495)Termination reason: Instruction limit % 25.98/4.95 % (424495)Termination phase: Saturation % 25.98/4.95 % (424495)Time elapsed: 0.212 s % 25.98/4.95 % (424495)Peak memory usage: 113 MB % 25.98/4.95 % (424495)Instructions burned: 281 (million) % 25.98/4.95 % (424499)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=355509064:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi) % 25.98/4.95 % (424500)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3718450742:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi) % 25.98/4.95 % (424503)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1129972778:i=471:thf=on:kws=precedence:rtra=on_2971 on theBenchmark for (2971ds/471Mi) % 25.98/4.95 % (424502)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=158960569:i=416:rtra=on:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/416Mi) % 25.98/4.95 % (424499)Refutation not found, incomplete strategy % 25.98/4.95 % (424499)------------------------------ % 25.98/4.95 % (424499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.98/4.95 % (424499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.98/4.95 % (424499)CaDiCaL version: 2.1.3 % 25.98/4.95 % (424499)Termination reason: Refutation not found, incomplete strategy % 25.98/4.95 % (424499)Time elapsed: 0.042 s % 25.98/4.95 % (424499)Peak memory usage: 88 MB % 25.98/4.95 % (424499)Instructions burned: 61 (million) % 25.98/4.95 % (424500)Refutation not found, incomplete strategy % 25.98/4.95 % (424500)------------------------------ % 25.98/4.95 % (424500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.98/4.95 % (424500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.98/4.95 % (424500)CaDiCaL version: 2.1.3 % 25.98/4.95 % (424500)Termination reason: Refutation not found, incomplete strategy % 25.98/4.95 % (424500)Time elapsed: 0.075 s % 25.98/4.95 % (424500)Peak memory usage: 112 MB % 25.98/4.95 % (424500)Instructions burned: 66 (million) % 25.98/4.95 % (424502)Refutation not found, incomplete strategy % 25.98/4.95 % (424502)------------------------------ % 25.98/4.95 % (424502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.84/5.73 % (424502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.84/5.73 % (424502)CaDiCaL version: 2.1.3 % 31.84/5.73 % (424502)Termination reason: Refutation not found, incomplete strategy % 31.84/5.73 % (424502)Time elapsed: 0.077 s % 31.84/5.73 % (424502)Peak memory usage: 112 MB % 31.84/5.73 % (424502)Instructions burned: 65 (million) % 31.84/5.73 % (424505)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=3005833102:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 31.84/5.73 % (424503)Instruction limit reached! % 31.84/5.73 % (424503)------------------------------ % 31.84/5.73 % (424503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.84/5.73 % (424503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.84/5.73 % (424503)CaDiCaL version: 2.1.3 % 31.84/5.73 % (424503)Termination reason: Instruction limit % 31.84/5.73 % (424503)Termination phase: Saturation % 31.84/5.73 % (424503)Time elapsed: 0.197 s % 31.84/5.73 % (424503)Peak memory usage: 113 MB % 31.84/5.73 % (424503)Instructions burned: 472 (million) % 31.84/5.73 % (424506)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4002436702:i=375:kws=inv_arity_squared:rtra=on_2969 on theBenchmark for (2969ds/375Mi) % 31.84/5.73 % (424508)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4050057469:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi) % 31.84/5.73 % (424508)Refutation not found, incomplete strategy % 31.84/5.73 % (424508)------------------------------ % 31.84/5.73 % (424508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.84/5.73 % (424508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.84/5.73 % (424508)CaDiCaL version: 2.1.3 % 31.84/5.73 % (424508)Termination reason: Refutation not found, incomplete strategy % 31.84/5.73 % (424508)Time elapsed: 0.080 s % 31.84/5.73 % (424508)Peak memory usage: 112 MB % 31.84/5.73 % (424508)Instructions burned: 70 (million) % 31.84/5.73 % (424505)Instruction limit reached! % 31.84/5.73 % (424505)------------------------------ % 31.84/5.73 % (424505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.84/5.73 % (424505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.84/5.73 % (424505)CaDiCaL version: 2.1.3 % 31.84/5.73 % (424505)Termination reason: Instruction limit % 31.84/5.73 % (424505)Termination phase: Saturation % 31.84/5.73 % (424505)Time elapsed: 0.190 s % 31.84/5.73 % (424505)Peak memory usage: 131 MB % 31.84/5.73 % (424505)Instructions burned: 278 (million) % 31.84/5.73 % (424499)------------------------------ % 31.84/5.73 % (424499)------------------------------ % 31.84/5.73 % (424514)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2068788253:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2967 on theBenchmark for (2967ds/513Mi) % 31.84/5.73 % (424500)------------------------------ % 31.84/5.73 % (424500)------------------------------ % 31.84/5.73 % (424502)------------------------------ % 31.84/5.73 % (424502)------------------------------ % 31.84/5.73 % (424506)Instruction limit reached! % 31.84/5.73 % (424506)------------------------------ % 31.84/5.73 % (424506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.84/5.73 % (424506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.84/5.73 % (424506)CaDiCaL version: 2.1.3 % 31.84/5.73 % (424506)Termination reason: Instruction limit % 31.84/5.73 % (424506)Termination phase: Saturation % 31.84/5.73 % (424506)Time elapsed: 0.320 s % 31.84/5.73 % (424506)Peak memory usage: 117 MB % 31.84/5.73 % (424506)Instructions burned: 376 (million) % 31.84/5.73 % (424519)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1787648380:i=334:rtra=on_2965 on theBenchmark for (2965ds/334Mi) % 31.84/5.73 % (424514)Instruction limit reached! % 31.84/5.73 % (424514)------------------------------ % 31.84/5.73 % (424514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.84/5.73 % (424514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.84/5.73 % (424514)CaDiCaL version: 2.1.3 % 31.84/5.73 % (424514)Termination reason: Instruction limit % 31.84/5.73 % (424514)Termination phase: Saturation % 31.84/5.73 % (424514)Time elapsed: 0.194 s % 31.84/5.73 % (424514)Peak memory usage: 92 MB % 31.84/5.73 % (424514)Instructions burned: 515 (million) % 37.43/6.28 % (424521)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=140069794:i=359:rtra=on:gtg=exists_top:ss=axioms_2965 on theBenchmark for (2965ds/359Mi) % 37.43/6.28 % (424522)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1484797246:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2964 on theBenchmark for (2964ds/341Mi) % 37.43/6.28 % (424521)Refutation not found, incomplete strategy % 37.43/6.28 % (424521)------------------------------ % 37.43/6.28 % (424521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.43/6.28 % (424521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.43/6.28 % (424521)CaDiCaL version: 2.1.3 % 37.43/6.28 % (424521)Termination reason: Refutation not found, incomplete strategy % 37.43/6.28 % (424521)Time elapsed: 0.054 s % 37.43/6.28 % (424521)Peak memory usage: 89 MB % 37.43/6.28 % (424521)Instructions burned: 76 (million) % 37.43/6.28 % (424508)------------------------------ % 37.43/6.28 % (424508)------------------------------ % 37.43/6.28 % (424523)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=273309625:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/261Mi) % 37.43/6.28 % (424519)Instruction limit reached! % 37.43/6.28 % (424519)------------------------------ % 37.43/6.28 % (424519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.43/6.28 % (424519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.43/6.28 % (424519)CaDiCaL version: 2.1.3 % 37.43/6.28 % (424519)Termination reason: Instruction limit % 37.43/6.28 % (424519)Termination phase: Saturation % 37.43/6.28 % (424519)Time elapsed: 0.236 s % 37.43/6.28 % (424519)Peak memory usage: 133 MB % 37.43/6.28 % (424519)Instructions burned: 334 (million) % 37.43/6.28 % (424524)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=3940873927:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/235Mi) % 37.43/6.28 % (424523)Refutation not found, incomplete strategy % 37.43/6.28 % (424523)------------------------------ % 37.43/6.28 % (424523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.43/6.28 % (424523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.43/6.28 % (424523)CaDiCaL version: 2.1.3 % 37.43/6.28 % (424523)Termination reason: Refutation not found, incomplete strategy % 37.43/6.28 % (424523)Time elapsed: 0.071 s % 37.43/6.28 % (424523)Peak memory usage: 112 MB % 37.43/6.28 % (424523)Instructions burned: 59 (million) % 37.43/6.28 % (424528)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3877939037:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2963 on theBenchmark for (2963ds/273Mi) % 37.43/6.28 % (424524)Refutation not found, incomplete strategy % 37.43/6.28 % (424524)------------------------------ % 37.43/6.28 % (424524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.43/6.28 % (424524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.43/6.28 % (424524)CaDiCaL version: 2.1.3 % 37.43/6.28 % (424524)Termination reason: Refutation not found, incomplete strategy % 37.43/6.28 % (424524)Time elapsed: 0.081 s % 37.43/6.28 % (424524)Peak memory usage: 112 MB % 37.43/6.28 % (424524)Instructions burned: 69 (million) % 37.43/6.28 % (424531)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3082282533:i=146:doe=on:rtra=on_2962 on theBenchmark for (2962ds/146Mi) % 37.43/6.28 % (424522)Instruction limit reached! % 37.43/6.28 % (424522)------------------------------ % 37.43/6.28 % (424522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.43/6.28 % (424522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.43/6.28 % (424522)CaDiCaL version: 2.1.3 % 37.43/6.28 % (424522)Termination reason: Instruction limit % 37.43/6.28 % (424522)Termination phase: Saturation % 37.43/6.28 % (424522)Time elapsed: 0.251 s % 37.43/6.28 % (424522)Peak memory usage: 119 MB % 37.43/6.28 % (424522)Instructions burned: 341 (million) % 37.43/6.28 % (424531)Instruction limit reached! % 37.43/6.28 % (424531)------------------------------ % 37.43/6.28 % (424531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.43/6.28 % (424531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.52/6.96 % (424531)CaDiCaL version: 2.1.3 % 40.52/6.96 % (424531)Termination reason: Instruction limit % 40.52/6.96 % (424531)Termination phase: Saturation % 40.52/6.96 % (424531)Time elapsed: 0.058 s % 40.52/6.96 % (424531)Peak memory usage: 90 MB % 40.52/6.96 % (424531)Instructions burned: 147 (million) % 40.52/6.96 % (424536)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=803638489:i=4428:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/4428Mi) % 40.52/6.96 % (424528)Instruction limit reached! % 40.52/6.96 % (424528)------------------------------ % 40.52/6.96 % (424528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.52/6.96 % (424528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.52/6.96 % (424528)CaDiCaL version: 2.1.3 % 40.52/6.96 % (424528)Termination reason: Instruction limit % 40.52/6.96 % (424528)Termination phase: Saturation % 40.52/6.96 % (424528)Time elapsed: 0.209 s % 40.52/6.96 % (424528)Peak memory usage: 91 MB % 40.52/6.96 % (424528)Instructions burned: 273 (million) % 40.52/6.96 % (424521)------------------------------ % 40.52/6.96 % (424521)------------------------------ % 40.52/6.96 % (424539)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=649812648:avsq=on:i=276:avsqr=1,2:rtra=on_2959 on theBenchmark for (2959ds/276Mi) % 40.52/6.96 % (424523)------------------------------ % 40.52/6.96 % (424523)------------------------------ % 40.52/6.96 % (424540)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1846778551:i=1052:rtra=on_2959 on theBenchmark for (2959ds/1052Mi) % 40.52/6.96 % (424524)------------------------------ % 40.52/6.96 % (424524)------------------------------ % 40.52/6.96 % (424544)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3181458536:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/655Mi) % 40.52/6.96 % (424545)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1232216282:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2958 on theBenchmark for (2958ds/1054Mi) % 40.52/6.96 % (424545)Refutation not found, incomplete strategy % 40.52/6.96 % (424545)------------------------------ % 40.52/6.96 % (424545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.52/6.96 % (424545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.52/6.96 % (424545)CaDiCaL version: 2.1.3 % 40.52/6.96 % (424545)Termination reason: Refutation not found, incomplete strategy % 40.52/6.96 % (424545)Time elapsed: 0.031 s % 40.52/6.96 % (424545)Peak memory usage: 88 MB % 40.52/6.96 % (424545)Instructions burned: 48 (million) % 40.52/6.96 % (424539)Instruction limit reached! % 40.52/6.96 % (424539)------------------------------ % 40.52/6.96 % (424539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.52/6.96 % (424539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.52/6.96 % (424539)CaDiCaL version: 2.1.3 % 40.52/6.96 % (424539)Termination reason: Instruction limit % 40.52/6.96 % (424539)Termination phase: Saturation % 40.52/6.96 % (424539)Time elapsed: 0.263 s % 40.52/6.96 % (424539)Peak memory usage: 131 MB % 40.52/6.96 % (424539)Instructions burned: 276 (million) % 40.52/6.96 % (424550)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1955257333:s2a=on:i=450:doe=on:nm=32:rtra=on_2956 on theBenchmark for (2956ds/450Mi) % 40.52/6.96 % (424548)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3407181400:i=107:rtra=on_2957 on theBenchmark for (2957ds/107Mi) % 40.52/6.96 % (424548)Instruction limit reached! % 40.52/6.96 % (424548)------------------------------ % 40.52/6.96 % (424548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.52/6.96 % (424548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.52/6.96 % (424548)CaDiCaL version: 2.1.3 % 40.52/6.96 % (424548)Termination reason: Instruction limit % 40.52/6.96 % (424548)Termination phase: Saturation % 40.52/6.96 % (424548)Time elapsed: 0.081 s % 40.52/6.96 % (424548)Peak memory usage: 89 MB % 40.52/6.96 % (424548)Instructions burned: 108 (million) % 40.52/6.96 % (424554)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 40.52/6.96 % (424554)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=528192272:i=1090:aac=none:nm=0:rtra=on:rawr=on_2954 on theBenchmark for (2954ds/1090Mi) % 45.17/7.42 % (424545)------------------------------ % 45.17/7.42 % (424545)------------------------------ % 45.17/7.42 % (424558)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2157156140:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2953 on theBenchmark for (2953ds/130Mi) % 45.17/7.42 % (424550)Instruction limit reached! % 45.17/7.42 % (424550)------------------------------ % 45.17/7.42 % (424550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.17/7.42 % (424550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/7.42 % (424550)CaDiCaL version: 2.1.3 % 45.17/7.42 % (424550)Termination reason: Instruction limit % 45.17/7.42 % (424550)Termination phase: Saturation % 45.17/7.42 % (424550)Time elapsed: 0.368 s % 45.17/7.42 % (424550)Peak memory usage: 135 MB % 45.17/7.42 % (424550)Instructions burned: 450 (million) % 45.17/7.42 % (424544)Instruction limit reached! % 45.17/7.42 % (424544)------------------------------ % 45.17/7.42 % (424544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.17/7.42 % (424544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/7.42 % (424544)CaDiCaL version: 2.1.3 % 45.17/7.42 % (424544)Termination reason: Instruction limit % 45.17/7.42 % (424544)Termination phase: Saturation % 45.17/7.42 % (424544)Time elapsed: 0.568 s % 45.17/7.42 % (424544)Peak memory usage: 101 MB % 45.17/7.42 % (424544)Instructions burned: 655 (million) % 45.17/7.42 % (424558)Instruction limit reached! % 45.17/7.42 % (424558)------------------------------ % 45.17/7.42 % (424558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.17/7.42 % (424558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/7.42 % (424558)CaDiCaL version: 2.1.3 % 45.17/7.42 % (424558)Termination reason: Instruction limit % 45.17/7.42 % (424558)Termination phase: Property scanning % 45.17/7.42 % (424558)Time elapsed: 0.096 s % 45.17/7.42 % (424558)Peak memory usage: 88 MB % 45.17/7.42 % (424558)Instructions burned: 131 (million) % 45.17/7.42 % (424540)Instruction limit reached! % 45.17/7.42 % (424540)------------------------------ % 45.17/7.42 % (424540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.17/7.42 % (424540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/7.42 % (424540)CaDiCaL version: 2.1.3 % 45.17/7.42 % (424540)Termination reason: Instruction limit % 45.17/7.42 % (424540)Termination phase: Saturation % 45.17/7.42 % (424540)Time elapsed: 0.699 s % 45.17/7.42 % (424540)Peak memory usage: 91 MB % 45.17/7.42 % (424540)Instructions burned: 1052 (million) % 45.17/7.42 % (424564)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=762183600:i=312:kws=inv_frequency:nm=20:rtra=on_2951 on theBenchmark for (2951ds/312Mi) % 45.17/7.42 % (424567)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=4057506116:i=491:doe=on:rtra=on:gtg=position_2950 on theBenchmark for (2950ds/491Mi) % 45.17/7.42 % (424569)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1484840821:s2a=on:i=835:s2at=2:rtra=on_2950 on theBenchmark for (2950ds/835Mi) % 45.17/7.42 % (424572)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=534503660:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2949 on theBenchmark for (2949ds/307Mi) % 45.17/7.42 % (424573)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2706491504:i=776:doe=on:rtra=on_2949 on theBenchmark for (2949ds/776Mi) % 45.17/7.42 % (424567)Refutation not found, incomplete strategy % 45.17/7.42 % (424567)------------------------------ % 45.17/7.42 % (424567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.17/7.42 % (424567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/7.42 % (424567)CaDiCaL version: 2.1.3 % 45.17/7.42 % (424567)Termination reason: Refutation not found, incomplete strategy % 45.17/7.42 % (424567)Time elapsed: 0.135 s % 45.17/7.42 % (424567)Peak memory usage: 91 MB % 45.17/7.42 % (424567)Instructions burned: 177 (million) % 45.17/7.42 % (424564)Instruction limit reached! % 45.17/7.42 % (424564)------------------------------ % 45.17/7.42 % (424564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.17/7.42 % (424564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/7.42 % (424564)CaDiCaL version: 2.1.3 % 45.17/7.42 % (424564)Termination reason: Instruction limit % 51.09/8.19 % (424564)Termination phase: Saturation % 51.09/8.19 % (424564)Time elapsed: 0.266 s % 51.09/8.19 % (424564)Peak memory usage: 113 MB % 51.09/8.19 % (424564)Instructions burned: 312 (million) % 51.09/8.19 % (424572)Refutation not found, incomplete strategy % 51.09/8.19 % (424572)------------------------------ % 51.09/8.19 % (424572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.09/8.19 % (424572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.09/8.19 % (424572)CaDiCaL version: 2.1.3 % 51.09/8.19 % (424572)Termination reason: Refutation not found, incomplete strategy % 51.09/8.19 % (424572)Time elapsed: 0.180 s % 51.09/8.19 % (424572)Peak memory usage: 95 MB % 51.09/8.19 % (424572)Instructions burned: 242 (million) % 51.09/8.19 % (424582)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=18218957:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2946 on theBenchmark for (2946ds/646Mi) % 51.09/8.19 % (424554)Instruction limit reached! % 51.09/8.19 % (424554)------------------------------ % 51.09/8.19 % (424554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.09/8.19 % (424554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.09/8.19 % (424554)CaDiCaL version: 2.1.3 % 51.09/8.19 % (424554)Termination reason: Instruction limit % 51.09/8.19 % (424554)Termination phase: Saturation % 51.09/8.19 % (424554)Time elapsed: 0.849 s % 51.09/8.19 % (424554)Peak memory usage: 120 MB % 51.09/8.19 % (424554)Instructions burned: 1091 (million) % 51.09/8.19 % (424536)Instruction limit reached! % 51.09/8.19 % (424536)------------------------------ % 51.09/8.19 % (424536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.09/8.19 % (424536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.09/8.19 % (424536)CaDiCaL version: 2.1.3 % 51.09/8.19 % (424536)Termination reason: Instruction limit % 51.09/8.19 % (424536)Termination phase: Saturation % 51.09/8.19 % (424536)Time elapsed: 1.556 s % 51.09/8.19 % (424536)Peak memory usage: 92 MB % 51.09/8.19 % (424536)Instructions burned: 4428 (million) % 51.09/8.19 % (424567)------------------------------ % 51.09/8.19 % (424567)------------------------------ % 51.09/8.19 % (424569)Instruction limit reached! % 51.09/8.19 % (424569)------------------------------ % 51.09/8.19 % (424569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.09/8.19 % (424569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.09/8.19 % (424569)CaDiCaL version: 2.1.3 % 51.09/8.19 % (424569)Termination reason: Instruction limit % 51.09/8.19 % (424569)Termination phase: Saturation % 51.09/8.19 % (424569)Time elapsed: 0.547 s % 51.09/8.19 % (424569)Peak memory usage: 90 MB % 51.09/8.19 % (424569)Instructions burned: 836 (million) % 51.09/8.19 % (424573)Instruction limit reached! % 51.09/8.19 % (424573)------------------------------ % 51.09/8.19 % (424573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.09/8.19 % (424573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.09/8.19 % (424573)CaDiCaL version: 2.1.3 % 51.09/8.19 % (424573)Termination reason: Instruction limit % 51.09/8.19 % (424573)Termination phase: Saturation % 51.09/8.19 % (424573)Time elapsed: 0.563 s % 51.09/8.19 % (424573)Peak memory usage: 114 MB % 51.09/8.19 % (424573)Instructions burned: 777 (million) % 51.09/8.19 % (424572)------------------------------ % 51.09/8.19 % (424572)------------------------------ % 51.09/8.19 % (424589)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=1442082240:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2943 on theBenchmark for (2943ds/1131Mi) % 51.09/8.19 % (424588)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=3707247479:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2943 on theBenchmark for (2943ds/784Mi) % 51.09/8.19 % (424590)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=408095955:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2942 on theBenchmark for (2942ds/246Mi) % 51.09/8.19 % (424591)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2634489432:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2942 on theBenchmark for (2942ds/775Mi) % 51.09/8.19 % (424590)Refutation not found, incomplete strategy % 51.09/8.19 % (424590)------------------------------ % 51.09/8.19 % (424590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424590)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424590)Termination reason: Refutation not found, incomplete strategy % 62.87/10.03 % (424590)Time elapsed: 0.080 s % 62.87/10.03 % (424590)Peak memory usage: 112 MB % 62.87/10.03 % (424590)Instructions burned: 68 (million) % 62.87/10.03 % (424591)Refutation not found, incomplete strategy % 62.87/10.03 % (424591)------------------------------ % 62.87/10.03 % (424591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424591)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424591)Termination reason: Refutation not found, incomplete strategy % 62.87/10.03 % (424591)Time elapsed: 0.039 s % 62.87/10.03 % (424591)Peak memory usage: 88 MB % 62.87/10.03 % (424591)Instructions burned: 67 (million) % 62.87/10.03 % (424592)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1045884591:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2941 on theBenchmark for (2941ds/273Mi) % 62.87/10.03 % (424595)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=264772933:i=102:nm=16:rtra=on_2941 on theBenchmark for (2941ds/102Mi) % 62.87/10.03 % (424595)Instruction limit reached! % 62.87/10.03 % (424595)------------------------------ % 62.87/10.03 % (424595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424582)Instruction limit reached! % 62.87/10.03 % (424582)------------------------------ % 62.87/10.03 % (424582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424582)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424582)Termination reason: Instruction limit % 62.87/10.03 % (424582)Termination phase: Saturation % 62.87/10.03 % (424595)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424582)Time elapsed: 0.581 s % 62.87/10.03 % (424582)Peak memory usage: 138 MB % 62.87/10.03 % (424595)Termination reason: Instruction limit % 62.87/10.03 % (424595)Termination phase: Saturation % 62.87/10.03 % (424595)Time elapsed: 0.077 s % 62.87/10.03 % (424582)Instructions burned: 646 (million) % 62.87/10.03 % (424595)Peak memory usage: 88 MB % 62.87/10.03 % (424595)Instructions burned: 104 (million) % 62.87/10.03 % (424592)Instruction limit reached! % 62.87/10.03 % (424592)------------------------------ % 62.87/10.03 % (424592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424592)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424592)Termination reason: Instruction limit % 62.87/10.03 % (424592)Termination phase: Saturation % 62.87/10.03 % (424592)Time elapsed: 0.210 s % 62.87/10.03 % (424592)Peak memory usage: 91 MB % 62.87/10.03 % (424592)Instructions burned: 273 (million) % 62.87/10.03 % (424589)Instruction limit reached! % 62.87/10.03 % (424589)------------------------------ % 62.87/10.03 % (424589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424589)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424589)Termination reason: Instruction limit % 62.87/10.03 % (424589)Termination phase: Saturation % 62.87/10.03 % (424589)Time elapsed: 0.473 s % 62.87/10.03 % (424589)Peak memory usage: 119 MB % 62.87/10.03 % (424589)Instructions burned: 1133 (million) % 62.87/10.03 % (424590)------------------------------ % 62.87/10.03 % (424590)------------------------------ % 62.87/10.03 % (424591)------------------------------ % 62.87/10.03 % (424591)------------------------------ % 62.87/10.03 % (424604)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2558484049:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2937 on theBenchmark for (2937ds/1094Mi) % 62.87/10.03 % (424588)Instruction limit reached! % 62.87/10.03 % (424588)------------------------------ % 62.87/10.03 % (424588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.87/10.03 % (424588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.87/10.03 % (424588)CaDiCaL version: 2.1.3 % 62.87/10.03 % (424588)Termination reason: Instruction limit % 62.87/10.03 % (424588)Termination phase: Saturation % 62.87/10.03 % (424588)Time elapsed: 0.589 s % 76.99/12.02 % (424588)Peak memory usage: 113 MB % 76.99/12.02 % (424588)Instructions burned: 785 (million) % 76.99/12.02 % (424605)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3517478809:i=6400:doe=on:fsr=off:rtra=on_2937 on theBenchmark for (2937ds/6400Mi) % 76.99/12.02 % (424608)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=1007505460:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2936 on theBenchmark for (2936ds/868Mi) % 76.99/12.02 % (424609)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=2124077339:i=1846:canc=cautious:fsr=off:rtra=on_2936 on theBenchmark for (2936ds/1846Mi) % 76.99/12.02 % (424609)Refutation not found, incomplete strategy % 76.99/12.02 % (424609)------------------------------ % 76.99/12.02 % (424609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.99/12.02 % (424609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.99/12.02 % (424609)CaDiCaL version: 2.1.3 % 76.99/12.02 % (424609)Termination reason: Refutation not found, incomplete strategy % 76.99/12.02 % (424609)Time elapsed: 0.044 s % 76.99/12.02 % (424609)Peak memory usage: 89 MB % 76.99/12.02 % (424609)Instructions burned: 115 (million) % 76.99/12.02 % (424612)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3369239468:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi) % 76.99/12.02 % (424611)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4242541913:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2935 on theBenchmark for (2935ds/36816Mi) % 76.99/12.02 % (424616)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=1671791877:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2934 on theBenchmark for (2934ds/863Mi) % 76.99/12.02 % (424609)------------------------------ % 76.99/12.02 % (424609)------------------------------ % 76.99/12.02 % (424612)Instruction limit reached! % 76.99/12.02 % (424612)------------------------------ % 76.99/12.02 % (424612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.99/12.02 % (424612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.99/12.02 % (424612)CaDiCaL version: 2.1.3 % 76.99/12.02 % (424612)Termination reason: Instruction limit % 76.99/12.02 % (424612)Termination phase: Saturation % 76.99/12.02 % (424612)Time elapsed: 0.203 s % 76.99/12.02 % (424612)Peak memory usage: 91 MB % 76.99/12.02 % (424612)Instructions burned: 274 (million) % 76.99/12.02 % (424623)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3431672514:i=5811:kws=precedence:nm=0:rtra=on_2931 on theBenchmark for (2931ds/5811Mi) % 76.99/12.02 % (424608)Instruction limit reached! % 76.99/12.02 % (424608)------------------------------ % 76.99/12.02 % (424608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.99/12.02 % (424608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.99/12.02 % (424608)CaDiCaL version: 2.1.3 % 76.99/12.02 % (424608)Termination reason: Instruction limit % 76.99/12.02 % (424608)Termination phase: Saturation % 76.99/12.02 % (424608)Time elapsed: 0.677 s % 76.99/12.02 % (424608)Peak memory usage: 137 MB % 76.99/12.02 % (424608)Instructions burned: 869 (million) % 76.99/12.02 % (424616)Instruction limit reached! % 76.99/12.02 % (424616)------------------------------ % 76.99/12.02 % (424616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.99/12.02 % (424616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.99/12.02 % (424616)CaDiCaL version: 2.1.3 % 76.99/12.02 % (424616)Termination reason: Instruction limit % 76.99/12.02 % (424616)Termination phase: Saturation % 76.99/12.02 % (424616)Time elapsed: 0.426 s % 76.99/12.02 % (424616)Peak memory usage: 137 MB % 76.99/12.02 % (424616)Instructions burned: 864 (million) % 76.99/12.02 % (424625)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=3306885881:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2930 on theBenchmark for (2930ds/2216Mi) % 76.99/12.02 % (424604)Instruction limit reached! % 76.99/12.02 % (424604)------------------------------ % 76.99/12.02 % (424604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.99/12.02 % (424604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.07/12.76 % (424604)CaDiCaL version: 2.1.3 % 81.07/12.76 % (424604)Termination reason: Instruction limit % 81.07/12.76 % (424604)Termination phase: Saturation % 81.07/12.76 % (424604)Time elapsed: 0.769 s % 81.07/12.76 % (424604)Peak memory usage: 92 MB % 81.07/12.76 % (424604)Instructions burned: 1095 (million) % 81.07/12.76 % (424630)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1272387441:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/801Mi) % 81.07/12.76 % (424631)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=571524669:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2927 on theBenchmark for (2927ds/1026Mi) % 81.07/12.76 % (424631)Refutation not found, incomplete strategy % 81.07/12.76 % (424631)------------------------------ % 81.07/12.76 % (424631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.07/12.76 % (424631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.07/12.76 % (424631)CaDiCaL version: 2.1.3 % 81.07/12.76 % (424631)Termination reason: Refutation not found, incomplete strategy % 81.07/12.76 % (424631)Time elapsed: 0.031 s % 81.07/12.76 % (424631)Peak memory usage: 88 MB % 81.07/12.76 % (424631)Instructions burned: 49 (million) % 81.07/12.76 % (424634)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1293295382:i=3509:rtra=on_2927 on theBenchmark for (2927ds/3509Mi) % 81.07/12.76 % (424630)Instruction limit reached! % 81.07/12.76 % (424630)------------------------------ % 81.07/12.76 % (424630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.07/12.76 % (424630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.07/12.76 % (424630)CaDiCaL version: 2.1.3 % 81.07/12.76 % (424630)Termination reason: Instruction limit % 81.07/12.76 % (424630)Termination phase: Saturation % 81.07/12.76 % (424630)Time elapsed: 0.378 s % 81.07/12.76 % (424630)Peak memory usage: 101 MB % 81.07/12.76 % (424630)Instructions burned: 802 (million) % 81.07/12.76 % (424631)------------------------------ % 81.07/12.76 % (424631)------------------------------ % 81.07/12.76 % (424642)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3751530726:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2921 on theBenchmark for (2921ds/2127Mi) % 81.07/12.76 % (424642)Refutation not found, incomplete strategy % 81.07/12.76 % (424642)------------------------------ % 81.07/12.76 % (424642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.07/12.76 % (424642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.07/12.76 % (424642)CaDiCaL version: 2.1.3 % 81.07/12.76 % (424642)Termination reason: Refutation not found, incomplete strategy % 81.07/12.76 % (424642)Time elapsed: 0.025 s % 81.07/12.76 % (424642)Peak memory usage: 88 MB % 81.07/12.76 % (424642)Instructions burned: 63 (million) % 81.07/12.76 % (424643)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1370387159:i=1959:rtra=on:fsd=on:proc=on_2920 on theBenchmark for (2920ds/1959Mi) % 81.07/12.76 % (424642)------------------------------ % 81.07/12.76 % (424642)------------------------------ % 81.07/12.76 % (424649)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1956142523:s2a=on:i=3553:nm=0:rtra=on_2915 on theBenchmark for (2915ds/3553Mi) % 81.07/12.76 % (424625)Instruction limit reached! % 81.07/12.76 % (424625)------------------------------ % 81.07/12.76 % (424625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.07/12.76 % (424625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.07/12.76 % (424625)CaDiCaL version: 2.1.3 % 81.07/12.76 % (424625)Termination reason: Instruction limit % 81.07/12.76 % (424625)Termination phase: Saturation % 81.07/12.76 % (424625)Time elapsed: 1.669 s % 81.07/12.76 % (424625)Peak memory usage: 122 MB % 81.07/12.76 % (424625)Instructions burned: 2217 (million) % 81.07/12.76 % (424643)Instruction limit reached! % 81.07/12.76 % (424643)------------------------------ % 81.07/12.76 % (424643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.07/12.76 % (424643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.07/12.76 % (424643)CaDiCaL version: 2.1.3 % 81.07/12.76 % (424643)Termination reason: Instruction limit % 81.07/12.76 % (424643)Termination phase: Saturation % 81.07/12.76 % (424643)Time elapsed: 0.808 s % 81.07/12.76 % (424643)Peak memory usage: 121 MB % 81.07/12.76 % (424643)Instructions burned: 1961 (million) % 81.07/12.76 % (424654)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1549362359:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2910 on theBenchmark for (2910ds/3201Mi) % 108.20/16.25 % (424655)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=2219957805:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2910 on theBenchmark for (2910ds/4093Mi) % 108.20/16.25 % (424654)Refutation not found, incomplete strategy % 108.20/16.25 % (424654)------------------------------ % 108.20/16.25 % (424654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.20/16.25 % (424654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.20/16.25 % (424654)CaDiCaL version: 2.1.3 % 108.20/16.25 % (424654)Termination reason: Refutation not found, incomplete strategy % 108.20/16.25 % (424654)Time elapsed: 0.385 s % 108.20/16.25 % (424654)Peak memory usage: 93 MB % 108.20/16.25 % (424654)Instructions burned: 499 (million) % 108.20/16.25 % (424634)Instruction limit reached! % 108.20/16.25 % (424634)------------------------------ % 108.20/16.25 % (424634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.20/16.25 % (424634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.20/16.25 % (424634)CaDiCaL version: 2.1.3 % 108.20/16.25 % (424634)Termination reason: Instruction limit % 108.20/16.25 % (424634)Termination phase: Saturation % 108.20/16.25 % (424634)Time elapsed: 2.310 s % 108.20/16.25 % (424634)Peak memory usage: 91 MB % 108.20/16.25 % (424634)Instructions burned: 3510 (million) % 108.20/16.25 % (424654)------------------------------ % 108.20/16.25 % (424654)------------------------------ % 108.20/16.25 % (424660)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=768136134:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2901 on theBenchmark for (2901ds/21173Mi) % 108.20/16.25 % (424660)Refutation not found, incomplete strategy % 108.20/16.25 % (424660)------------------------------ % 108.20/16.25 % (424660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.20/16.25 % (424660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.20/16.25 % (424660)CaDiCaL version: 2.1.3 % 108.20/16.25 % (424660)Termination reason: Refutation not found, incomplete strategy % 108.20/16.25 % (424660)Time elapsed: 0.053 s % 108.20/16.25 % (424660)Peak memory usage: 113 MB % 108.20/16.25 % (424660)Instructions burned: 25 (million) % 108.20/16.25 % (424662)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3662214047:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2900 on theBenchmark for (2900ds/10544Mi) % 108.20/16.25 % (424660)------------------------------ % 108.20/16.25 % (424660)------------------------------ % 108.20/16.25 % (424655)Instruction limit reached! % 108.20/16.25 % (424655)------------------------------ % 108.20/16.25 % (424655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.20/16.25 % (424655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.20/16.25 % (424655)CaDiCaL version: 2.1.3 % 108.20/16.25 % (424655)Termination reason: Instruction limit % 108.20/16.25 % (424655)Termination phase: Saturation % 108.20/16.25 % (424655)Time elapsed: 1.553 s % 108.20/16.25 % (424655)Peak memory usage: 134 MB % 108.20/16.25 % (424655)Instructions burned: 4095 (million) % 108.20/16.25 % (424670)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=629322682:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/1262Mi) % 108.20/16.25 % (424672)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1176069776:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2893 on theBenchmark for (2893ds/775Mi) % 108.20/16.25 % (424672)Refutation not found, incomplete strategy % 108.20/16.25 % (424672)------------------------------ % 108.20/16.25 % (424672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.20/16.25 % (424672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.20/16.25 % (424672)CaDiCaL version: 2.1.3 % 108.20/16.25 % (424672)Termination reason: Refutation not found, incomplete strategy % 108.20/16.25 % (424672)Time elapsed: 0.046 s % 108.20/16.25 % (424672)Peak memory usage: 88 MB % 108.20/16.25 % (424672)Instructions burned: 66 (million) % 108.20/16.25 % (424605)Instruction limit reached! % 108.20/16.25 % (424605)------------------------------ % 108.20/16.25 % (424605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.74/17.19 % (424605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.74/17.19 % (424605)CaDiCaL version: 2.1.3 % 114.74/17.19 % (424605)Termination reason: Instruction limit % 114.74/17.19 % (424605)Termination phase: Saturation % 114.74/17.19 % (424605)Time elapsed: 4.598 s % 114.74/17.19 % (424605)Peak memory usage: 92 MB % 114.74/17.19 % (424605)Instructions burned: 6400 (million) % 114.74/17.19 % (424649)Instruction limit reached! % 114.74/17.19 % (424649)------------------------------ % 114.74/17.19 % (424649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.74/17.19 % (424649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.74/17.19 % (424649)CaDiCaL version: 2.1.3 % 114.74/17.19 % (424649)Termination reason: Instruction limit % 114.74/17.19 % (424649)Termination phase: Saturation % 114.74/17.19 % (424649)Time elapsed: 2.527 s % 114.74/17.19 % (424649)Peak memory usage: 92 MB % 114.74/17.19 % (424649)Instructions burned: 3554 (million) % 114.74/17.19 % (424623)Instruction limit reached! % 114.74/17.19 % (424623)------------------------------ % 114.74/17.19 % (424623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.74/17.19 % (424623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.74/17.19 % (424623)CaDiCaL version: 2.1.3 % 114.74/17.19 % (424623)Termination reason: Instruction limit % 114.74/17.19 % (424623)Termination phase: Saturation % 114.74/17.19 % (424623)Time elapsed: 4.135 s % 114.74/17.19 % (424623)Peak memory usage: 121 MB % 114.74/17.19 % (424623)Instructions burned: 5811 (million) % 114.74/17.19 % (424670)Instruction limit reached! % 114.74/17.19 % (424670)------------------------------ % 114.74/17.19 % (424670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.74/17.19 % (424670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.74/17.19 % (424670)CaDiCaL version: 2.1.3 % 114.74/17.19 % (424670)Termination reason: Instruction limit % 114.74/17.19 % (424670)Termination phase: Saturation % 114.74/17.19 % (424670)Time elapsed: 0.525 s % 114.74/17.19 % (424670)Peak memory usage: 121 MB % 114.74/17.19 % (424670)Instructions burned: 1264 (million) % 114.74/17.19 % (424672)------------------------------ % 114.74/17.19 % (424672)------------------------------ % 114.74/17.19 % (424678)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=541572369:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2888 on theBenchmark for (2888ds/270Mi) % 114.74/17.19 % (424680)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=730167007:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2888 on theBenchmark for (2888ds/17165Mi) % 114.74/17.19 % (424681)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3438977937:s2a=on:i=13094:s2at=-1:rtra=on_2888 on theBenchmark for (2888ds/13094Mi) % 114.74/17.19 % (424683)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=883828654:st=2:i=12633:rtra=on:ss=axioms_2887 on theBenchmark for (2887ds/12633Mi) % 114.74/17.19 % (424683)Refutation not found, incomplete strategy % 114.74/17.19 % (424683)------------------------------ % 114.74/17.19 % (424683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.74/17.19 % (424683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.74/17.19 % (424683)CaDiCaL version: 2.1.3 % 114.74/17.19 % (424683)Termination reason: Refutation not found, incomplete strategy % 114.74/17.19 % (424683)Time elapsed: 0.030 s % 114.74/17.19 % (424683)Peak memory usage: 88 MB % 114.74/17.19 % (424683)Instructions burned: 35 (million) % 114.74/17.19 % (424678)Instruction limit reached! % 114.74/17.19 % (424678)------------------------------ % 114.74/17.19 % (424678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.74/17.19 % (424678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.74/17.19 % (424678)CaDiCaL version: 2.1.3 % 114.74/17.19 % (424678)Termination reason: Instruction limit % 114.74/17.19 % (424678)Termination phase: Saturation % 114.74/17.19 % (424678)Time elapsed: 0.202 s % 114.74/17.19 % (424678)Peak memory usage: 91 MB % 114.74/17.19 % (424678)Instructions burned: 270 (million) % 114.74/17.19 % (424686)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=547119539:i=1783:rtra=on:gtg=position_2886 on theBenchmark for (2886ds/1783Mi) % 114.74/17.19 % (424692)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=1481765282:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2884 on theBenchmark for (2884ds/5451Mi) % 130.18/19.32 % (424683)------------------------------ % 130.18/19.32 % (424683)------------------------------ % 130.18/19.32 % (424699)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=1455094862:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2880 on theBenchmark for (2880ds/4975Mi) % 130.18/19.32 % (424686)Instruction limit reached! % 130.18/19.32 % (424686)------------------------------ % 130.18/19.32 % (424686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.18/19.32 % (424686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/19.32 % (424686)CaDiCaL version: 2.1.3 % 130.18/19.32 % (424686)Termination reason: Instruction limit % 130.18/19.32 % (424686)Termination phase: Saturation % 130.18/19.32 % (424686)Time elapsed: 1.197 s % 130.18/19.32 % (424686)Peak memory usage: 121 MB % 130.18/19.32 % (424686)Instructions burned: 1784 (million) % 130.18/19.32 % (424710)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=3654927775:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2871 on theBenchmark for (2871ds/2076Mi) % 130.18/19.32 % (424710)Instruction limit reached! % 130.18/19.32 % (424710)------------------------------ % 130.18/19.32 % (424710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.18/19.32 % (424710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/19.32 % (424710)CaDiCaL version: 2.1.3 % 130.18/19.32 % (424710)Termination reason: Instruction limit % 130.18/19.32 % (424710)Termination phase: Saturation % 130.18/19.32 % (424710)Time elapsed: 0.793 s % 130.18/19.32 % (424710)Peak memory usage: 122 MB % 130.18/19.32 % (424710)Instructions burned: 2077 (million) % 130.18/19.32 % (424750)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3991810215:i=5145:rtra=on_2861 on theBenchmark for (2861ds/5145Mi) % 130.18/19.32 % (424692)Instruction limit reached! % 130.18/19.32 % (424692)------------------------------ % 130.18/19.32 % (424692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.18/19.32 % (424692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/19.32 % (424692)CaDiCaL version: 2.1.3 % 130.18/19.32 % (424692)Termination reason: Instruction limit % 130.18/19.32 % (424692)Termination phase: Saturation % 130.18/19.32 % (424692)Time elapsed: 2.481 s % 130.18/19.32 % (424692)Peak memory usage: 123 MB % 130.18/19.32 % (424692)Instructions burned: 5451 (million) % 130.18/19.32 % (424699)Instruction limit reached! % 130.18/19.32 % (424699)------------------------------ % 130.18/19.32 % (424699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.18/19.32 % (424699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/19.32 % (424699)CaDiCaL version: 2.1.3 % 130.18/19.32 % (424699)Termination reason: Instruction limit % 130.18/19.32 % (424699)Termination phase: Saturation % 130.18/19.32 % (424699)Time elapsed: 2.258 s % 130.18/19.32 % (424699)Peak memory usage: 148 MB % 130.18/19.32 % (424699)Instructions burned: 4975 (million) % 130.18/19.32 % (424752)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3967059869:i=3509:rtra=on_2856 on theBenchmark for (2856ds/3509Mi) % 130.18/19.32 % (424754)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3770081923:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2854 on theBenchmark for (2854ds/13800Mi) % 130.18/19.32 % (424754)Refutation not found, incomplete strategy % 130.18/19.32 % (424754)------------------------------ % 130.18/19.32 % (424754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.18/19.32 % (424754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/19.32 % (424754)CaDiCaL version: 2.1.3 % 130.18/19.32 % (424754)Termination reason: Refutation not found, incomplete strategy % 130.18/19.32 % (424754)Time elapsed: 0.022 s % 130.18/19.32 % (424754)Peak memory usage: 88 MB % 130.18/19.32 % (424754)Instructions burned: 63 (million) % 130.18/19.32 % (424754)------------------------------ % 130.18/19.32 % (424754)------------------------------ % 130.18/19.32 % (424756)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1465464306:i=1412:rtra=on:fsd=on:proc=on_2850 on theBenchmark for (2850ds/1412Mi) % 130.18/19.32 % (424680)Instruction limit reached! % 130.18/19.32 % (424680)------------------------------ % 130.18/19.32 % (424680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.18/19.32 % (424680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.86/29.40 % (424680)CaDiCaL version: 2.1.3 % 201.86/29.40 % (424680)Termination reason: Instruction limit % 201.86/29.40 % (424680)Termination phase: Saturation % 201.86/29.40 % (424680)Time elapsed: 3.970 s % 201.86/29.40 % (424680)Peak memory usage: 97 MB % 201.86/29.40 % (424680)Instructions burned: 17170 (million) % 201.86/29.40 % (424758)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 % 201.86/29.40 % (424758)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3441989721:i=11747:aac=none:nm=0:rtra=on:rawr=on_2846 on theBenchmark for (2846ds/11747Mi) % 201.86/29.40 % (424756)Instruction limit reached! % 201.86/29.40 % (424756)------------------------------ % 201.86/29.40 % (424756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.86/29.40 % (424756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.86/29.40 % (424756)CaDiCaL version: 2.1.3 % 201.86/29.40 % (424756)Termination reason: Instruction limit % 201.86/29.40 % (424756)Termination phase: Saturation % 201.86/29.40 % (424756)Time elapsed: 0.565 s % 201.86/29.40 % (424756)Peak memory usage: 121 MB % 201.86/29.40 % (424756)Instructions burned: 1413 (million) % 201.86/29.40 % (424760)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2131389123:s2a=on:i=3553:nm=0:rtra=on_2843 on theBenchmark for (2843ds/3553Mi) % 201.86/29.40 % (424752)Instruction limit reached! % 201.86/29.40 % (424752)------------------------------ % 201.86/29.40 % (424752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.86/29.40 % (424752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.86/29.40 % (424752)CaDiCaL version: 2.1.3 % 201.86/29.40 % (424752)Termination reason: Instruction limit % 201.86/29.40 % (424752)Termination phase: Saturation % 201.86/29.40 % (424752)Time elapsed: 1.336 s % 201.86/29.40 % (424752)Peak memory usage: 91 MB % 201.86/29.40 % (424752)Instructions burned: 3510 (million) % 201.86/29.40 % (424750)Instruction limit reached! % 201.86/29.40 % (424750)------------------------------ % 201.86/29.40 % (424750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.86/29.40 % (424750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.86/29.40 % (424750)CaDiCaL version: 2.1.3 % 201.86/29.40 % (424750)Termination reason: Instruction limit % 201.86/29.40 % (424750)Termination phase: Saturation % 201.86/29.40 % (424750)Time elapsed: 1.937 s % 201.86/29.40 % (424750)Peak memory usage: 95 MB % 201.86/29.40 % (424750)Instructions burned: 5145 (million) % 201.86/29.40 % (424762)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1534413317:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/3201Mi) % 201.86/29.40 % (424763)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=3696255034:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2841 on theBenchmark for (2841ds/4081Mi) % 201.86/29.40 % (424662)Instruction limit reached! % 201.86/29.40 % (424662)------------------------------ % 201.86/29.40 % (424662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.86/29.40 % (424662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.86/29.40 % (424662)CaDiCaL version: 2.1.3 % 201.86/29.40 % (424662)Termination reason: Instruction limit % 201.86/29.40 % (424662)Termination phase: Saturation % 201.86/29.40 % (424662)Time elapsed: 5.883 s % 201.86/29.40 % (424662)Peak memory usage: 167 MB % 201.86/29.40 % (424662)Instructions burned: 10546 (million) % 201.86/29.40 % (424762)Refutation not found, incomplete strategy % 201.86/29.40 % (424762)------------------------------ % 201.86/29.40 % (424762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.86/29.40 % (424762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.86/29.40 % (424762)CaDiCaL version: 2.1.3 % 201.86/29.40 % (424762)Termination reason: Refutation not found, incomplete strategy % 201.86/29.40 % (424762)Time elapsed: 0.172 s % 201.86/29.40 % (424762)Peak memory usage: 93 MB % 201.86/29.40 % (424762)Instructions burned: 439 (million) % 201.86/29.40 % (424766)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=1527427150:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2838 on theBenchmark for (2838ds/20260Mi) % 211.73/30.95 % (424766)Refutation not found, incomplete strategy % 211.73/30.95 % (424766)------------------------------ % 211.73/30.95 % (424766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.95 % (424766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.95 % (424766)CaDiCaL version: 2.1.3 % 211.73/30.95 % (424766)Termination reason: Refutation not found, incomplete strategy % 211.73/30.95 % (424766)Time elapsed: 0.035 s % 211.73/30.95 % (424766)Peak memory usage: 113 MB % 211.73/30.95 % (424766)Instructions burned: 25 (million) % 211.73/30.95 % (424762)------------------------------ % 211.73/30.95 % (424762)------------------------------ % 211.73/30.95 % (424766)------------------------------ % 211.73/30.95 % (424766)------------------------------ % 211.73/30.95 % (424768)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4277275578:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2835 on theBenchmark for (2835ds/58627Mi) % 211.73/30.95 % (424769)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=885206985:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/6258Mi) % 211.73/30.95 % (424681)Instruction limit reached! % 211.73/30.95 % (424681)------------------------------ % 211.73/30.95 % (424681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.95 % (424681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.95 % (424681)CaDiCaL version: 2.1.3 % 211.73/30.95 % (424681)Termination reason: Instruction limit % 211.73/30.95 % (424681)Termination phase: Saturation % 211.73/30.95 % (424681)Time elapsed: 5.422 s % 211.73/30.95 % (424681)Peak memory usage: 120 MB % 211.73/30.95 % (424681)Instructions burned: 13094 (million) % 211.73/30.95 % (424772)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=68232025:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2831 on theBenchmark for (2831ds/34001Mi) % 211.73/30.95 % (424760)Instruction limit reached! % 211.73/30.95 % (424760)------------------------------ % 211.73/30.95 % (424760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.95 % (424760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.95 % (424760)CaDiCaL version: 2.1.3 % 211.73/30.95 % (424760)Termination reason: Instruction limit % 211.73/30.95 % (424760)Termination phase: Saturation % 211.73/30.95 % (424760)Time elapsed: 1.325 s % 211.73/30.95 % (424760)Peak memory usage: 92 MB % 211.73/30.95 % (424760)Instructions burned: 3555 (million) % 211.73/30.95 % (424774)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=879295895:s2a=on:i=71622:s2at=-1:rtra=on_2828 on theBenchmark for (2828ds/71622Mi) % 211.73/30.95 % (424763)Instruction limit reached! % 211.73/30.95 % (424763)------------------------------ % 211.73/30.95 % (424763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.95 % (424763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.95 % (424763)CaDiCaL version: 2.1.3 % 211.73/30.95 % (424763)Termination reason: Instruction limit % 211.73/30.95 % (424763)Termination phase: Saturation % 211.73/30.95 % (424763)Time elapsed: 1.575 s % 211.73/30.95 % (424763)Peak memory usage: 134 MB % 211.73/30.95 % (424763)Instructions burned: 4082 (million) % 211.73/30.95 % (424776)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3632483831:i=24001:kws=precedence:nm=0:rtra=on_2823 on theBenchmark for (2823ds/24001Mi) % 211.73/30.95 % (424758)Instruction limit reached! % 211.73/30.95 % (424758)------------------------------ % 211.73/30.95 % (424758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.95 % (424758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.95 % (424758)CaDiCaL version: 2.1.3 % 211.73/30.95 % (424758)Termination reason: Instruction limit % 211.73/30.95 % (424758)Termination phase: Saturation % 211.73/30.95 % (424758)Time elapsed: 2.390 s % 211.73/30.95 % (424758)Peak memory usage: 138 MB % 211.73/30.95 % (424758)Instructions burned: 11749 (million) % 211.73/30.95 % (424778)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=499459933:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2821 on theBenchmark for (2821ds/2076Mi) % 211.73/30.95 % (424778)Instruction limit reached! % 211.73/30.95 % (424778)------------------------------ % 211.73/30.95 % (424778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.91/36.13 % (424778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.91/36.13 % (424778)CaDiCaL version: 2.1.3 % 248.91/36.13 % (424778)Termination reason: Instruction limit % 248.91/36.13 % (424778)Termination phase: Saturation % 248.91/36.13 % (424778)Time elapsed: 0.430 s % 248.91/36.13 % (424778)Peak memory usage: 122 MB % 248.91/36.13 % (424778)Instructions burned: 2078 (million) % 248.91/36.13 % (424780)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3894489293:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2815 on theBenchmark for (2815ds/83971Mi) % 248.91/36.13 % (424769)Instruction limit reached! % 248.91/36.13 % (424769)------------------------------ % 248.91/36.13 % (424769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.91/36.13 % (424769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.91/36.13 % (424769)CaDiCaL version: 2.1.3 % 248.91/36.13 % (424769)Termination reason: Instruction limit % 248.91/36.13 % (424769)Termination phase: Saturation % 248.91/36.13 % (424769)Time elapsed: 2.364 s % 248.91/36.13 % (424769)Peak memory usage: 122 MB % 248.91/36.13 % (424769)Instructions burned: 6259 (million) % 248.91/36.13 % (424782)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3273845032:i=83944:rtra=on_2808 on theBenchmark for (2808ds/83944Mi) % 248.91/36.13 % (424611)Refutation not found, non-redundant clauses discarded % 248.91/36.13 % (424611)------------------------------ % 248.91/36.13 % (424611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.91/36.13 % (424611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.91/36.13 % (424611)CaDiCaL version: 2.1.3 % 248.91/36.13 % (424611)Termination reason: Refutation not found, non-redundant clauses discarded % 248.91/36.13 % (424611)Time elapsed: 15.259 s % 248.91/36.13 % (424611)Peak memory usage: 114 MB % 248.91/36.13 % (424611)Instructions burned: 33095 (million) % 248.91/36.13 % (424611)------------------------------ % 248.91/36.13 % (424611)------------------------------ % 248.91/36.13 % (424784)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=639010769:i=9201:rtra=on_2777 on theBenchmark for (2777ds/9201Mi) % 248.91/36.13 % (424784)Instruction limit reached! % 248.91/36.13 % (424784)------------------------------ % 248.91/36.13 % (424784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.91/36.13 % (424784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.91/36.13 % (424784)CaDiCaL version: 2.1.3 % 248.91/36.13 % (424784)Termination reason: Instruction limit % 248.91/36.13 % (424784)Termination phase: Saturation % 248.91/36.13 % (424784)Time elapsed: 3.438 s % 248.91/36.13 % (424784)Peak memory usage: 95 MB % 248.91/36.13 % (424784)Instructions burned: 9202 (million) % 248.91/36.13 % (424786)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 % 248.91/36.13 % (424786)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4164944834:i=6806:aac=none:nm=0:rtra=on:rawr=on_2741 on theBenchmark for (2741ds/6806Mi) % 248.91/36.13 % (424776)Instruction limit reached! % 248.91/36.13 % (424776)------------------------------ % 248.91/36.13 % (424776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.91/36.13 % (424776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.91/36.13 % (424776)CaDiCaL version: 2.1.3 % 248.91/36.13 % (424776)Termination reason: Instruction limit % 248.91/36.13 % (424776)Termination phase: Saturation % 248.91/36.13 % (424776)Time elapsed: 9.518 s % 248.91/36.13 % (424776)Peak memory usage: 138 MB % 248.91/36.13 % (424776)Instructions burned: 24002 (million) % 248.91/36.13 % (424788)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1671886573:s2a=on:i=3553:nm=0:rtra=on_2726 on theBenchmark for (2726ds/3553Mi) % 248.91/36.13 % (424786)Instruction limit reached! % 248.91/36.13 % (424786)------------------------------ % 248.91/36.13 % (424786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.91/36.13 % (424786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.91/36.13 % (424786)CaDiCaL version: 2.1.3 % 248.91/36.13 % (424786)Termination reason: Instruction limit % 248.91/36.13 % (424786)Termination phase: Saturation % 248.91/36.13 % (424786)Time elapsed: 2.513 s % 248.91/36.13 % (424786)Peak memory usage: 121 MB % 248.91/36.13 % (424786)Instructions burned: 6806 (million) % 253.96/36.86 % (424790)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=706315294:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2714 on theBenchmark for (2714ds/2064Mi) % 253.96/36.86 % (424788)Instruction limit reached! % 253.96/36.86 % (424788)------------------------------ % 253.96/36.86 % (424788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.96/36.86 % (424788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.96/36.86 % (424788)CaDiCaL version: 2.1.3 % 253.96/36.86 % (424788)Termination reason: Instruction limit % 253.96/36.86 % (424788)Termination phase: Saturation % 253.96/36.86 % (424788)Time elapsed: 1.303 s % 253.96/36.86 % (424788)Peak memory usage: 92 MB % 253.96/36.86 % (424788)Instructions burned: 3553 (million) % 253.96/36.86 % (424792)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=1455121157:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2712 on theBenchmark for (2712ds/20260Mi) % 253.96/36.86 % (424792)Refutation not found, incomplete strategy % 253.96/36.86 % (424792)------------------------------ % 253.96/36.86 % (424792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.96/36.86 % (424792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.96/36.86 % (424792)CaDiCaL version: 2.1.3 % 253.96/36.86 % (424792)Termination reason: Refutation not found, incomplete strategy % 253.96/36.86 % (424792)Time elapsed: 0.035 s % 253.96/36.86 % (424792)Peak memory usage: 113 MB % 253.96/36.86 % (424792)Instructions burned: 24 (million) % 253.96/36.86 % (424792)------------------------------ % 253.96/36.86 % (424792)------------------------------ % 253.96/36.86 % (424794)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2530700695:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2707 on theBenchmark for (2707ds/1244Mi) % 253.96/36.86 % (424790)Instruction limit reached! % 253.96/36.86 % (424790)------------------------------ % 253.96/36.86 % (424790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.96/36.86 % (424790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.96/36.86 % (424790)CaDiCaL version: 2.1.3 % 253.96/36.86 % (424790)Termination reason: Instruction limit % 253.96/36.86 % (424790)Termination phase: Saturation % 253.96/36.86 % (424790)Time elapsed: 0.827 s % 253.96/36.86 % (424790)Peak memory usage: 138 MB % 253.96/36.86 % (424790)Instructions burned: 2066 (million) % 253.96/36.86 % (424796)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=713196228:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2704 on theBenchmark for (2704ds/58261Mi) % 253.96/36.86 % (424772)Instruction limit reached! % 253.96/36.86 % (424772)------------------------------ % 253.96/36.86 % (424772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.96/36.86 % (424772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.96/36.86 % (424772)CaDiCaL version: 2.1.3 % 253.96/36.86 % (424772)Termination reason: Instruction limit % 253.96/36.86 % (424772)Termination phase: Saturation % 253.96/36.86 % (424772)Time elapsed: 12.760 s % 253.96/36.86 % (424772)Peak memory usage: 105 MB % 253.96/36.86 % (424772)Instructions burned: 34003 (million) % 253.96/36.86 % (424794)Instruction limit reached! % 253.96/36.86 % (424794)------------------------------ % 253.96/36.86 % (424794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.96/36.86 % (424794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.96/36.86 % (424794)CaDiCaL version: 2.1.3 % 253.96/36.86 % (424794)Termination reason: Instruction limit % 253.96/36.86 % (424794)Termination phase: Saturation % 253.96/36.86 % (424794)Time elapsed: 0.503 s % 253.96/36.86 % (424794)Peak memory usage: 121 MB % 253.96/36.86 % (424794)Instructions burned: 1245 (million) % 253.96/36.86 % (424798)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 % 253.96/36.86 % (424798)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=711022216:i=6806:aac=none:nm=0:rtra=on:rawr=on_2702 on theBenchmark for (2702ds/6806Mi) % 253.96/36.86 % (424799)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=2119276369:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2701 on theBenchmark for (2701ds/4081Mi) % 255.83/37.13 % (424799)Instruction limit reached! % 255.83/37.13 % (424799)------------------------------ % 255.83/37.13 % (424799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.83/37.13 % (424799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.83/37.13 % (424799)CaDiCaL version: 2.1.3 % 255.83/37.13 % (424799)Termination reason: Instruction limit % 255.83/37.13 % (424799)Termination phase: Saturation % 255.83/37.13 % (424799)Time elapsed: 1.545 s % 255.83/37.13 % (424799)Peak memory usage: 134 MB % 255.83/37.13 % (424799)Instructions burned: 4084 (million) % 255.83/37.13 % (424802)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=413094939:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2684 on theBenchmark for (2684ds/1701Mi) % 255.83/37.13 % (424802)Instruction limit reached! % 255.83/37.13 % (424802)------------------------------ % 255.83/37.13 % (424802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.83/37.13 % (424802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.83/37.13 % (424802)CaDiCaL version: 2.1.3 % 255.83/37.13 % (424802)Termination reason: Instruction limit % 255.83/37.13 % (424802)Termination phase: Saturation % 255.83/37.13 % (424802)Time elapsed: 0.651 s % 255.83/37.13 % (424802)Peak memory usage: 121 MB % 255.83/37.13 % (424802)Instructions burned: 1703 (million) % 255.83/37.13 % (424798)Instruction limit reached! % 255.83/37.13 % (424798)------------------------------ % 255.83/37.13 % (424798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.83/37.13 % (424798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.83/37.13 % (424798)CaDiCaL version: 2.1.3 % 255.83/37.13 % (424798)Termination reason: Instruction limit % 255.83/37.13 % (424798)Termination phase: Saturation % 255.83/37.13 % (424798)Time elapsed: 2.519 s % 255.83/37.13 % (424798)Peak memory usage: 121 MB % 255.83/37.13 % (424798)Instructions burned: 6807 (million) % 255.83/37.13 % (424804)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=2314061437:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2675 on theBenchmark for (2675ds/57001Mi) % 255.83/37.13 % (424805)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 % 255.83/37.13 % (424805)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3904822821:i=8622:aac=none:nm=0:rtra=on:rawr=on_2675 on theBenchmark for (2675ds/8622Mi) % 255.83/37.13 % (424768)Refutation not found, non-redundant clauses discarded % 255.83/37.13 % (424768)------------------------------ % 255.83/37.13 % (424768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.83/37.13 % (424768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.83/37.13 % (424768)CaDiCaL version: 2.1.3 % 255.83/37.13 % (424768)Termination reason: Refutation not found, non-redundant clauses discarded % 255.83/37.13 % (424768)Time elapsed: 17.794 s % 255.83/37.13 % (424768)Peak memory usage: 119 MB % 255.83/37.13 % (424768)Instructions burned: 47847 (million) % 255.83/37.13 % (424768)------------------------------ % 255.83/37.13 % (424768)------------------------------ % 255.83/37.13 % (424808)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3550685065:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2653 on theBenchmark for (2653ds/24Mi) % 255.83/37.13 % (424808)Instruction limit reached! % 255.83/37.13 % (424808)------------------------------ % 255.83/37.13 % (424808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.83/37.13 % (424808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.83/37.13 % (424808)CaDiCaL version: 2.1.3 % 255.83/37.13 % (424808)Termination reason: Instruction limit % 255.83/37.13 % (424808)Termination phase: Property scanning % 255.83/37.13 % (424808)Time elapsed: 0.010 s % 255.83/37.13 % (424808)Peak memory usage: 86 MB % 255.83/37.13 % (424808)Instructions burned: 25 (million) % 255.83/37.13 % (424810)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2470211923:i=614:kws=precedence:nm=0:rtra=on_2652 on theBenchmark for (2652ds/614Mi) % 255.83/37.13 % (424810)Instruction limit reached! % 258.49/37.53 % (424810)------------------------------ % 258.49/37.53 % (424810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424810)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424810)Termination reason: Instruction limit % 258.49/37.53 % (424810)Termination phase: Saturation % 258.49/37.53 % (424810)Time elapsed: 0.264 s % 258.49/37.53 % (424810)Peak memory usage: 120 MB % 258.49/37.53 % (424810)Instructions burned: 616 (million) % 258.49/37.53 % (424812)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2342067434:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2647 on theBenchmark for (2647ds/402Mi) % 258.49/37.53 % (424780)Instruction limit reached! % 258.49/37.53 % (424780)------------------------------ % 258.49/37.53 % (424780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424780)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424780)Termination reason: Instruction limit % 258.49/37.53 % (424780)Termination phase: Saturation % 258.49/37.53 % (424780)Time elapsed: 17.131 s % 258.49/37.53 % (424780)Peak memory usage: 149 MB % 258.49/37.53 % (424780)Instructions burned: 83973 (million) % 258.49/37.53 % (424812)Instruction limit reached! % 258.49/37.53 % (424812)------------------------------ % 258.49/37.53 % (424812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424812)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424812)Termination reason: Instruction limit % 258.49/37.53 % (424812)Termination phase: Saturation % 258.49/37.53 % (424812)Time elapsed: 0.184 s % 258.49/37.53 % (424812)Peak memory usage: 118 MB % 258.49/37.53 % (424812)Instructions burned: 404 (million) % 258.49/37.53 % (424814)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=884465105:s2a=on:i=14:rtra=on:inst=on_2643 on theBenchmark for (2643ds/14Mi) % 258.49/37.53 % (424814)Instruction limit reached! % 258.49/37.53 % (424814)------------------------------ % 258.49/37.53 % (424814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424814)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424814)Termination reason: Instruction limit % 258.49/37.53 % (424814)Termination phase: Property scanning % 258.49/37.53 % (424814)Time elapsed: 0.004 s % 258.49/37.53 % (424814)Peak memory usage: 86 MB % 258.49/37.53 % (424814)Instructions burned: 18 (million) % 258.49/37.53 % (424805)Instruction limit reached! % 258.49/37.53 % (424805)------------------------------ % 258.49/37.53 % (424805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424805)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424805)Termination reason: Instruction limit % 258.49/37.53 % (424805)Termination phase: Saturation % 258.49/37.53 % (424805)Time elapsed: 3.233 s % 258.49/37.53 % (424805)Peak memory usage: 138 MB % 258.49/37.53 % (424805)Instructions burned: 8623 (million) % 258.49/37.53 % (424815)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1421862056:i=8:rtra=on_2642 on theBenchmark for (2642ds/8Mi) % 258.49/37.53 % (424815)Instruction limit reached! % 258.49/37.53 % (424815)------------------------------ % 258.49/37.53 % (424815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424815)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424815)Termination reason: Instruction limit % 258.49/37.53 % (424815)Termination phase: Property scanning % 258.49/37.53 % (424815)Time elapsed: 0.004 s % 258.49/37.53 % (424815)Peak memory usage: 85 MB % 258.49/37.53 % (424815)Instructions burned: 8 (million) % 258.49/37.53 % (424817)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=182206600:i=92:rtra=on_2641 on theBenchmark for (2641ds/92Mi) % 258.49/37.53 % (424817)Instruction limit reached! % 258.49/37.53 % (424817)------------------------------ % 258.49/37.53 % (424817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.49/37.53 % (424817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.49/37.53 % (424817)CaDiCaL version: 2.1.3 % 258.49/37.53 % (424817)Termination reason: Instruction limit % 258.49/37.53 % (424817)Termination phase: Saturation % 258.49/37.53 % (424817)Time elapsed: 0.034 s % 260.95/37.89 % (424817)Peak memory usage: 112 MB % 260.95/37.89 % (424817)Instructions burned: 96 (million) % 260.95/37.89 % (424818)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3158270594:i=66:rtra=on_2641 on theBenchmark for (2641ds/66Mi) % 260.95/37.89 % (424820)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2577318779:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2641 on theBenchmark for (2641ds/28Mi) % 260.95/37.89 % (424818)Instruction limit reached! % 260.95/37.89 % (424818)------------------------------ % 260.95/37.89 % (424818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.95/37.89 % (424818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.95/37.89 % (424818)CaDiCaL version: 2.1.3 % 260.95/37.89 % (424818)Termination reason: Instruction limit % 260.95/37.89 % (424818)Termination phase: Saturation % 260.95/37.89 % (424818)Time elapsed: 0.026 s % 260.95/37.89 % (424818)Peak memory usage: 87 MB % 260.95/37.89 % (424818)Instructions burned: 70 (million) % 260.95/37.89 % (424820)Instruction limit reached! % 260.95/37.89 % (424820)------------------------------ % 260.95/37.89 % (424820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.95/37.89 % (424820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.95/37.89 % (424820)CaDiCaL version: 2.1.3 % 260.95/37.89 % (424820)Termination reason: Instruction limit % 260.95/37.89 % (424820)Termination phase: Saturation % 260.95/37.89 % (424820)Time elapsed: 0.012 s % 260.95/37.89 % (424820)Peak memory usage: 86 MB % 260.95/37.89 % (424820)Instructions burned: 29 (million) % 260.95/37.89 % (424822)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=2690925831:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2640 on theBenchmark for (2640ds/58Mi) % 260.95/37.89 % (424822)Instruction limit reached! % 260.95/37.89 % (424822)------------------------------ % 260.95/37.89 % (424822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.95/37.89 % (424822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.95/37.89 % (424822)CaDiCaL version: 2.1.3 % 260.95/37.89 % (424822)Termination reason: Instruction limit % 260.95/37.89 % (424822)Termination phase: Saturation % 260.95/37.89 % (424822)Time elapsed: 0.012 s % 260.95/37.89 % (424822)Peak memory usage: 86 MB % 260.95/37.89 % (424822)Instructions burned: 60 (million) % 260.95/37.89 % (424828)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=2313722825:i=54:canc=cautious:fsr=off:rtra=on_2639 on theBenchmark for (2639ds/54Mi) % 260.95/37.89 % (424826)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=487749901:i=48:canc=force:rtra=on_2639 on theBenchmark for (2639ds/48Mi) % 260.95/37.89 % (424825)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4197374328:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2639 on theBenchmark for (2639ds/32Mi) % 260.95/37.89 % (424828)Instruction limit reached! % 260.95/37.89 % (424828)------------------------------ % 260.95/37.89 % (424828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.95/37.89 % (424828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.95/37.89 % (424828)CaDiCaL version: 2.1.3 % 260.95/37.89 % (424828)Termination reason: Instruction limit % 260.95/37.89 % (424828)Termination phase: Saturation % 260.95/37.89 % (424828)Time elapsed: 0.012 s % 260.95/37.89 % (424828)Peak memory usage: 86 MB % 260.95/37.89 % (424828)Instructions burned: 61 (million) % 260.95/37.89 % (424825)Instruction limit reached! % 260.95/37.89 % (424825)------------------------------ % 260.95/37.89 % (424825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.95/37.89 % (424825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.95/37.89 % (424825)CaDiCaL version: 2.1.3 % 260.95/37.89 % (424825)Termination reason: Instruction limit % 260.95/37.89 % (424825)Termination phase: Property scanning % 260.95/37.89 % (424825)Time elapsed: 0.013 s % 260.95/37.89 % (424825)Peak memory usage: 87 MB % 260.95/37.89 % (424825)Instructions burned: 32 (million) % 260.95/37.89 % (424826)Instruction limit reached! % 260.95/37.89 % (424826)------------------------------ % 260.95/37.89 % (424826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.95/37.89 % (424826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.95/37.89 % (424826)CaDiCaL version: 2.1.3 % 260.95/37.89 % (424826)Termination reason: Instruction limit % 263.95/38.25 % (424826)Termination phase: Property scanning % 263.95/38.25 % (424826)Time elapsed: 0.019 s % 263.95/38.25 % (424826)Peak memory usage: 87 MB % 263.95/38.25 % (424826)Instructions burned: 50 (million) % 263.95/38.25 % (424832)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3538701281:i=170:gtgl=4:rtra=on:gtg=exists_sym_2637 on theBenchmark for (2637ds/170Mi) % 263.95/38.25 % (424833)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=457485845:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2637 on theBenchmark for (2637ds/4Mi) % 263.95/38.25 % (424832)Instruction limit reached! % 263.95/38.25 % (424832)------------------------------ % 263.95/38.25 % (424832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.95/38.25 % (424832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.95/38.25 % (424832)CaDiCaL version: 2.1.3 % 263.95/38.25 % (424832)Termination reason: Instruction limit % 263.95/38.25 % (424832)Termination phase: Saturation % 263.95/38.25 % (424832)Time elapsed: 0.038 s % 263.95/38.25 % (424832)Peak memory usage: 90 MB % 263.95/38.25 % (424832)Instructions burned: 172 (million) % 263.95/38.25 % (424833)Instruction limit reached! % 263.95/38.25 % (424833)------------------------------ % 263.95/38.25 % (424833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.95/38.25 % (424833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.95/38.25 % (424833)CaDiCaL version: 2.1.3 % 263.95/38.25 % (424833)Termination reason: Instruction limit % 263.95/38.25 % (424833)Termination phase: Property scanning % 263.95/38.25 % (424833)Time elapsed: 0.003 s % 263.95/38.25 % (424833)Peak memory usage: 85 MB % 263.95/38.25 % (424833)Instructions burned: 5 (million) % 263.95/38.25 % (424834)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=101468552:i=362:rtra=on:ss=axioms:ev=cautious_2637 on theBenchmark for (2637ds/362Mi) % 263.95/38.25 % (424834)Refutation not found, incomplete strategy % 263.95/38.25 % (424834)------------------------------ % 263.95/38.25 % (424834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.95/38.25 % (424834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.95/38.25 % (424834)CaDiCaL version: 2.1.3 % 263.95/38.25 % (424834)Termination reason: Refutation not found, incomplete strategy % 263.95/38.25 % (424834)Time elapsed: 0.017 s % 263.95/38.25 % (424834)Peak memory usage: 88 MB % 263.95/38.25 % (424834)Instructions burned: 47 (million) % 263.95/38.25 % (424837)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2831085715:i=8:ep=RST:ins=2:rtra=on_2636 on theBenchmark for (2636ds/8Mi) % 263.95/38.25 % (424837)Instruction limit reached! % 263.95/38.25 % (424837)------------------------------ % 263.95/38.25 % (424837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.95/38.25 % (424837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.95/38.25 % (424837)CaDiCaL version: 2.1.3 % 263.95/38.25 % (424837)Termination reason: Instruction limit % 263.95/38.25 % (424837)Termination phase: Property scanning % 263.95/38.25 % (424837)Time elapsed: 0.003 s % 263.95/38.25 % (424837)Peak memory usage: 85 MB % 263.95/38.25 % (424837)Instructions burned: 14 (million) % 263.95/38.25 % (424838)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4278263265:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2636 on theBenchmark for (2636ds/132Mi) % 263.95/38.25 % (424838)Instruction limit reached! % 263.95/38.25 % (424838)------------------------------ % 263.95/38.25 % (424838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.95/38.25 % (424838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.95/38.25 % (424838)CaDiCaL version: 2.1.3 % 263.95/38.25 % (424838)Termination reason: Instruction limit % 263.95/38.25 % (424838)Termination phase: Saturation % 263.95/38.25 % (424838)Time elapsed: 0.093 s % 263.95/38.25 % (424838)Peak memory usage: 130 MB % 263.95/38.25 % (424838)Instructions burned: 133 (million) % 263.95/38.25 % (424841)lrs+10_1_thi=all:si=on:fd=off:random_seed=3742390916:i=106:rtra=on:gtg=all_2635 on theBenchmark for (2635ds/106Mi) % 263.95/38.25 % (424841)Instruction limit reached! % 263.95/38.25 % (424841)------------------------------ % 263.95/38.25 % (424841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.95/38.25 % (424841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.95/38.25 % (424841)CaDiCaL version: 2.1.3 % 263.95/38.25 % (424841)Termination reason: Instruction limit % 263.95/38.25 % (424841)Termination phase: Saturation % 267.27/38.73 % (424841)Time elapsed: 0.020 s % 267.27/38.73 % (424841)Peak memory usage: 88 MB % 267.27/38.73 % (424841)Instructions burned: 106 (million) % 267.27/38.73 % (424834)------------------------------ % 267.27/38.73 % (424834)------------------------------ % 267.27/38.73 % (424845)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1100559386:st=3:i=4:rtra=on:ss=axioms_2633 on theBenchmark for (2633ds/4Mi) % 267.27/38.73 % (424844)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=3041994533:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2633 on theBenchmark for (2633ds/16Mi) % 267.27/38.73 % (424845)Instruction limit reached! % 267.27/38.73 % (424845)------------------------------ % 267.27/38.73 % (424845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.27/38.73 % (424845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.27/38.73 % (424845)CaDiCaL version: 2.1.3 % 267.27/38.73 % (424845)Termination reason: Instruction limit % 267.27/38.73 % (424845)Termination phase: Property scanning % 267.27/38.73 % (424845)Time elapsed: 0.002 s % 267.27/38.73 % (424845)Peak memory usage: 85 MB % 267.27/38.73 % (424845)Instructions burned: 7 (million) % 267.27/38.73 % (424844)Instruction limit reached! % 267.27/38.73 % (424844)------------------------------ % 267.27/38.73 % (424844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.27/38.73 % (424844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.27/38.73 % (424844)CaDiCaL version: 2.1.3 % 267.27/38.73 % (424844)Termination reason: Instruction limit % 267.27/38.73 % (424844)Termination phase: Property scanning % 267.27/38.73 % (424844)Time elapsed: 0.007 s % 267.27/38.73 % (424844)Peak memory usage: 86 MB % 267.27/38.73 % (424844)Instructions burned: 18 (million) % 267.27/38.73 % (424846)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3050831504:i=4:doe=on:canc=force:asg=cautious:rtra=on_2633 on theBenchmark for (2633ds/4Mi) % 267.27/38.73 % (424846)Instruction limit reached! % 267.27/38.73 % (424846)------------------------------ % 267.27/38.73 % (424846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.27/38.73 % (424846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.27/38.73 % (424846)CaDiCaL version: 2.1.3 % 267.27/38.73 % (424846)Termination reason: Instruction limit % 267.27/38.73 % (424846)Termination phase: Property scanning % 267.27/38.73 % (424846)Time elapsed: 0.003 s % 267.27/38.73 % (424846)Peak memory usage: 85 MB % 267.27/38.73 % (424846)Instructions burned: 5 (million) % 267.27/38.73 % (424849)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4270095425:i=254:doe=on:rtra=on_2632 on theBenchmark for (2632ds/254Mi) % 267.27/38.73 % (424850)dis+10_1_si=on:random_seed=1742486609:i=20:ep=R:rtra=on_2632 on theBenchmark for (2632ds/20Mi) % 267.27/38.73 % (424850)Instruction limit reached! % 267.27/38.73 % (424850)------------------------------ % 267.27/38.73 % (424850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.27/38.73 % (424850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.27/38.73 % (424850)CaDiCaL version: 2.1.3 % 267.27/38.73 % (424850)Termination reason: Instruction limit % 267.27/38.73 % (424850)Termination phase: Property scanning % 267.27/38.73 % (424850)Time elapsed: 0.009 s % 267.27/38.73 % (424850)Peak memory usage: 86 MB % 267.27/38.73 % (424850)Instructions burned: 20 (million) % 267.27/38.73 % (424849)Instruction limit reached! % 267.27/38.73 % (424849)------------------------------ % 267.27/38.73 % (424849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.27/38.73 % (424849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.27/38.73 % (424849)CaDiCaL version: 2.1.3 % 267.27/38.73 % (424849)Termination reason: Instruction limit % 267.27/38.73 % (424849)Termination phase: Saturation % 267.27/38.73 % (424849)Time elapsed: 0.067 s % 267.27/38.73 % (424849)Peak memory usage: 114 MB % 267.27/38.73 % (424849)Instructions burned: 257 (million) % 267.27/38.73 % (424852)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2339495511:i=52:canc=cautious:av=off:rtra=on_2631 on theBenchmark for (2631ds/52Mi) % 267.27/38.73 % (424852)Instruction limit reached! % 267.27/38.73 % (424852)------------------------------ % 267.27/38.73 % (424852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.27/38.73 % (424852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.27/38.73 % (424852)CaDiCaL version: 2.1.3 % 267.27/38.73 % (424852)Termination reason: Instruction limit % 271.52/39.31 % (424852)Termination phase: Property scanning % 271.52/39.31 % (424852)Time elapsed: 0.021 s % 271.52/39.31 % (424852)Peak memory usage: 87 MB % 271.52/39.31 % (424852)Instructions burned: 54 (million) % 271.52/39.31 % (424856)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1917311386:i=4:fsr=off:rtra=on:inst=on_2630 on theBenchmark for (2630ds/4Mi) % 271.52/39.31 % (424856)Instruction limit reached! % 271.52/39.31 % (424856)------------------------------ % 271.52/39.31 % (424856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.52/39.31 % (424856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.52/39.31 % (424856)CaDiCaL version: 2.1.3 % 271.52/39.31 % (424856)Termination reason: Instruction limit % 271.52/39.31 % (424856)Termination phase: Property scanning % 271.52/39.31 % (424856)Time elapsed: 0.002 s % 271.52/39.31 % (424856)Peak memory usage: 85 MB % 271.52/39.31 % (424856)Instructions burned: 7 (million) % 271.52/39.31 % (424855)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4262173537:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2630 on theBenchmark for (2630ds/70Mi) % 271.52/39.31 % (424855)Instruction limit reached! % 271.52/39.31 % (424855)------------------------------ % 271.52/39.31 % (424855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.52/39.31 % (424855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.52/39.31 % (424855)CaDiCaL version: 2.1.3 % 271.52/39.31 % (424855)Termination reason: Instruction limit % 271.52/39.31 % (424855)Termination phase: Saturation % 271.52/39.31 % (424855)Time elapsed: 0.027 s % 271.52/39.31 % (424855)Peak memory usage: 87 MB % 271.52/39.31 % (424855)Instructions burned: 71 (million) % 271.52/39.31 % (424858)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=861559878:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2630 on theBenchmark for (2630ds/16Mi) % 271.52/39.31 % (424858)Instruction limit reached! % 271.52/39.31 % (424858)------------------------------ % 271.52/39.31 % (424858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.52/39.31 % (424858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.52/39.31 % (424858)CaDiCaL version: 2.1.3 % 271.52/39.31 % (424858)Termination reason: Instruction limit % 271.52/39.31 % (424858)Termination phase: Property scanning % 271.52/39.31 % (424858)Time elapsed: 0.007 s % 271.52/39.31 % (424858)Peak memory usage: 86 MB % 271.52/39.31 % (424858)Instructions burned: 17 (million) % 271.52/39.31 % (424860)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2777137290:i=740:ep=RS:fsr=off:rtra=on_2629 on theBenchmark for (2629ds/740Mi) % 271.52/39.31 % (424860)Refutation not found, incomplete strategy % 271.52/39.31 % (424860)------------------------------ % 271.52/39.31 % (424860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.52/39.31 % (424860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.52/39.31 % (424860)CaDiCaL version: 2.1.3 % 271.52/39.31 % (424860)Termination reason: Refutation not found, incomplete strategy % 271.52/39.31 % (424860)Time elapsed: 0.021 s % 271.52/39.31 % (424860)Peak memory usage: 89 MB % 271.52/39.31 % (424860)Instructions burned: 105 (million) % 271.52/39.31 % (424862)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=911256145:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2629 on theBenchmark for (2629ds/26Mi) % 271.52/39.31 % (424862)Instruction limit reached! % 271.52/39.31 % (424862)------------------------------ % 271.52/39.31 % (424862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.52/39.31 % (424862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.52/39.31 % (424862)CaDiCaL version: 2.1.3 % 271.52/39.31 % (424862)Termination reason: Instruction limit % 271.52/39.31 % (424862)Termination phase: Property scanning % 271.52/39.31 % (424862)Time elapsed: 0.011 s % 271.52/39.31 % (424862)Peak memory usage: 85 MB % 271.52/39.31 % (424862)Instructions burned: 27 (million) % 271.52/39.31 % (424865)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3918566398:i=452:rtra=on:gtg=position:ss=axioms_2628 on theBenchmark for (2628ds/452Mi) % 271.52/39.31 % (424860)------------------------------ % 271.52/39.31 % (424860)------------------------------ % 271.52/39.31 % (424865)Refutation not found, incomplete strategy % 271.52/39.31 % (424865)------------------------------ % 271.52/39.31 % (424865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.10/40.05 % (424865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.10/40.05 % (424865)CaDiCaL version: 2.1.3 % 277.10/40.05 % (424865)Termination reason: Refutation not found, incomplete strategy % 277.10/40.05 % (424865)Time elapsed: 0.047 s % 277.10/40.05 % (424865)Peak memory usage: 112 MB % 277.10/40.05 % (424865)Instructions burned: 66 (million) % 277.10/40.05 % (424867)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3639516286:i=20:rtra=on_2627 on theBenchmark for (2627ds/20Mi) % 277.10/40.05 % (424867)Instruction limit reached! % 277.10/40.05 % (424867)------------------------------ % 277.10/40.05 % (424867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.10/40.05 % (424867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.10/40.05 % (424867)CaDiCaL version: 2.1.3 % 277.10/40.05 % (424867)Termination reason: Instruction limit % 277.10/40.05 % (424867)Termination phase: Property scanning % 277.10/40.05 % (424867)Time elapsed: 0.010 s % 277.10/40.05 % (424867)Peak memory usage: 86 MB % 277.10/40.05 % (424867)Instructions burned: 22 (million) % 277.10/40.05 % (424869)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2159928874:i=142:rtra=on:gtg=exists_top_2626 on theBenchmark for (2626ds/142Mi) % 277.10/40.05 % (424869)Instruction limit reached! % 277.10/40.05 % (424869)------------------------------ % 277.10/40.05 % (424869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.10/40.05 % (424869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.10/40.05 % (424869)CaDiCaL version: 2.1.3 % 277.10/40.05 % (424869)Termination reason: Instruction limit % 277.10/40.05 % (424869)Termination phase: Saturation % 277.10/40.05 % (424869)Time elapsed: 0.056 s % 277.10/40.05 % (424869)Peak memory usage: 130 MB % 277.10/40.05 % (424869)Instructions burned: 142 (million) % 277.10/40.05 % (424871)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=3857991026:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2625 on theBenchmark for (2625ds/150Mi) % 277.10/40.05 % (424865)------------------------------ % 277.10/40.05 % (424865)------------------------------ % 277.10/40.05 % (424873)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=4033664176:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2625 on theBenchmark for (2625ds/588Mi) % 277.10/40.05 % (424871)Instruction limit reached! % 277.10/40.05 % (424871)------------------------------ % 277.10/40.05 % (424871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.10/40.05 % (424871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.10/40.05 % (424871)CaDiCaL version: 2.1.3 % 277.10/40.05 % (424871)Termination reason: Instruction limit % 277.10/40.05 % (424871)Termination phase: Saturation % 277.10/40.05 % (424871)Time elapsed: 0.057 s % 277.10/40.05 % (424871)Peak memory usage: 89 MB % 277.10/40.05 % (424871)Instructions burned: 151 (million) % 277.10/40.05 % (424873)Instruction limit reached! % 277.10/40.05 % (424873)------------------------------ % 277.10/40.05 % (424873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.10/40.05 % (424873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.10/40.05 % (424873)CaDiCaL version: 2.1.3 % 277.10/40.05 % (424873)Termination reason: Instruction limit % 277.10/40.05 % (424873)Termination phase: Saturation % 277.10/40.05 % (424873)Time elapsed: 0.124 s % 277.10/40.05 % (424873)Peak memory usage: 91 MB % 277.10/40.05 % (424873)Instructions burned: 588 (million) % 277.10/40.05 % (424875)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3909722380:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2624 on theBenchmark for (2624ds/260Mi) % 277.10/40.05 % (424877)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3643964239:i=262:rtra=on_2623 on theBenchmark for (2623ds/262Mi) % 277.10/40.05 % (424875)Instruction limit reached! % 277.10/40.05 % (424875)------------------------------ % 277.10/40.05 % (424875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.10/40.05 % (424875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.10/40.05 % (424875)CaDiCaL version: 2.1.3 % 277.10/40.05 % (424875)Termination reason: Instruction limit % 277.10/40.05 % (424875)Termination phase: Saturation % 277.10/40.05 % (424875)Time elapsed: 0.088 s % 277.10/40.05 % (424875)Peak memory usage: 89 MB % 277.10/40.05 % (424875)Instructions burned: 262 (million) % 280.60/40.68 % (424878)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1071277130:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2622 on theBenchmark for (2622ds/80Mi) % 280.60/40.68 % (424878)Instruction limit reached! % 280.60/40.68 % (424878)------------------------------ % 280.60/40.68 % (424878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.60/40.68 % (424878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.60/40.68 % (424878)CaDiCaL version: 2.1.3 % 280.60/40.68 % (424878)Termination reason: Instruction limit % 280.60/40.68 % (424878)Termination phase: Property scanning % 280.60/40.68 % (424878)Time elapsed: 0.016 s % 280.60/40.68 % (424878)Peak memory usage: 87 MB % 280.60/40.68 % (424878)Instructions burned: 80 (million) % 280.60/40.68 % (424877)Instruction limit reached! % 280.60/40.68 % (424877)------------------------------ % 280.60/40.68 % (424877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.60/40.68 % (424877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.60/40.68 % (424877)CaDiCaL version: 2.1.3 % 280.60/40.68 % (424877)Termination reason: Instruction limit % 280.60/40.68 % (424877)Termination phase: Saturation % 280.60/40.68 % (424877)Time elapsed: 0.148 s % 280.60/40.68 % (424877)Peak memory usage: 131 MB % 280.60/40.68 % (424877)Instructions burned: 262 (million) % 280.60/40.68 % (424883)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1956428974:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2621 on theBenchmark for (2621ds/1196Mi) % 280.60/40.68 % (424881)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=785060742:i=614:rtra=on:gtg=exists_top_2621 on theBenchmark for (2621ds/614Mi) % 280.60/40.68 % (424881)Refutation not found, incomplete strategy % 280.60/40.68 % (424881)------------------------------ % 280.60/40.68 % (424881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.60/40.68 % (424881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.60/40.68 % (424881)CaDiCaL version: 2.1.3 % 280.60/40.68 % (424881)Termination reason: Refutation not found, incomplete strategy % 280.60/40.68 % (424881)Time elapsed: 0.053 s % 280.60/40.68 % (424881)Peak memory usage: 90 MB % 280.60/40.68 % (424881)Instructions burned: 138 (million) % 280.60/40.68 % (424884)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1157438587:i=262:canc=cautious:fsr=off:rtra=on_2620 on theBenchmark for (2620ds/262Mi) % 280.60/40.68 % (424884)Instruction limit reached! % 280.60/40.68 % (424884)------------------------------ % 280.60/40.68 % (424884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.60/40.68 % (424884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.60/40.68 % (424884)CaDiCaL version: 2.1.3 % 280.60/40.68 % (424884)Termination reason: Instruction limit % 280.60/40.68 % (424884)Termination phase: Saturation % 280.60/40.68 % (424884)Time elapsed: 0.121 s % 280.60/40.68 % (424884)Peak memory usage: 113 MB % 280.60/40.68 % (424884)Instructions burned: 264 (million) % 280.60/40.68 % (424883)Instruction limit reached! % 280.60/40.68 % (424883)------------------------------ % 280.60/40.68 % (424883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.60/40.68 % (424883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.60/40.68 % (424883)CaDiCaL version: 2.1.3 % 280.60/40.68 % (424883)Termination reason: Instruction limit % 280.60/40.68 % (424883)Termination phase: Saturation % 280.60/40.68 % (424883)Time elapsed: 0.287 s % 280.60/40.68 % (424883)Peak memory usage: 139 MB % 280.60/40.68 % (424883)Instructions burned: 1201 (million) % 280.60/40.68 % (424881)------------------------------ % 280.60/40.68 % (424881)------------------------------ % 280.60/40.68 % (424888)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=2250600589:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2617 on theBenchmark for (2617ds/518Mi) % 280.60/40.68 % (424889)dis+10_1_si=on:random_seed=3386723385:s2a=on:i=2000:rtra=on:gtg=exists_all_2617 on theBenchmark for (2617ds/2000Mi) % 280.60/40.68 % (424888)Refutation not found, incomplete strategy % 280.60/40.68 % (424888)------------------------------ % 280.60/40.68 % (424888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.60/40.68 % (424888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.60/40.68 % (424888)CaDiCaL version: 2.1.3 % 280.60/40.68 % (424888)Termination reason: Refutation not found, incomplete strategy % 285.89/41.33 % (424888)Time elapsed: 0.049 s % 285.89/41.33 % (424888)Peak memory usage: 112 MB % 285.89/41.33 % (424888)Instructions burned: 68 (million) % 285.89/41.33 % (424890)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=581151027:i=766:fsr=off:rtra=on:ev=force_2617 on theBenchmark for (2617ds/766Mi) % 285.89/41.33 % (424888)------------------------------ % 285.89/41.33 % (424888)------------------------------ % 285.89/41.33 % (424890)Instruction limit reached! % 285.89/41.33 % (424890)------------------------------ % 285.89/41.33 % (424890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.89/41.33 % (424890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.89/41.33 % (424890)CaDiCaL version: 2.1.3 % 285.89/41.33 % (424890)Termination reason: Instruction limit % 285.89/41.33 % (424890)Termination phase: Saturation % 285.89/41.33 % (424890)Time elapsed: 0.298 s % 285.89/41.33 % (424890)Peak memory usage: 92 MB % 285.89/41.33 % (424890)Instructions burned: 768 (million) % 285.89/41.33 % (424889)Instruction limit reached! % 285.89/41.33 % (424889)------------------------------ % 285.89/41.33 % (424889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.89/41.33 % (424889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.89/41.33 % (424889)CaDiCaL version: 2.1.3 % 285.89/41.33 % (424889)Termination reason: Instruction limit % 285.89/41.33 % (424889)Termination phase: Saturation % 285.89/41.33 % (424889)Time elapsed: 0.417 s % 285.89/41.33 % (424889)Peak memory usage: 92 MB % 285.89/41.33 % (424889)Instructions burned: 2003 (million) % 285.89/41.33 % (424894)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=289024676:i=282:doe=on:rtra=on_2613 on theBenchmark for (2613ds/282Mi) % 285.89/41.33 % (424895)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3623411774:i=130:nm=16:rtra=on_2612 on theBenchmark for (2612ds/130Mi) % 285.89/41.33 % (424894)Instruction limit reached! % 285.89/41.33 % (424894)------------------------------ % 285.89/41.33 % (424894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.89/41.33 % (424894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.89/41.33 % (424894)CaDiCaL version: 2.1.3 % 285.89/41.33 % (424894)Termination reason: Instruction limit % 285.89/41.33 % (424894)Termination phase: Saturation % 285.89/41.33 % (424894)Time elapsed: 0.110 s % 285.89/41.33 % (424894)Peak memory usage: 90 MB % 285.89/41.33 % (424894)Instructions burned: 283 (million) % 285.89/41.33 % (424897)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1108603795:i=242:nm=16:rtra=on_2611 on theBenchmark for (2611ds/242Mi) % 285.89/41.33 % (424895)Instruction limit reached! % 285.89/41.33 % (424895)------------------------------ % 285.89/41.33 % (424895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.89/41.33 % (424895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.89/41.33 % (424895)CaDiCaL version: 2.1.3 % 285.89/41.33 % (424895)Termination reason: Instruction limit % 285.89/41.33 % (424895)Termination phase: Saturation % 285.89/41.33 % (424895)Time elapsed: 0.053 s % 285.89/41.33 % (424895)Peak memory usage: 90 MB % 285.89/41.33 % (424895)Instructions burned: 131 (million) % 285.89/41.33 % (424897)Instruction limit reached! % 285.89/41.33 % (424897)------------------------------ % 285.89/41.33 % (424897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.89/41.33 % (424897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.89/41.33 % (424897)CaDiCaL version: 2.1.3 % 285.89/41.33 % (424897)Termination reason: Instruction limit % 285.89/41.33 % (424897)Termination phase: Saturation % 285.89/41.33 % (424897)Time elapsed: 0.054 s % 285.89/41.33 % (424897)Peak memory usage: 92 MB % 285.89/41.33 % (424897)Instructions burned: 247 (million) % 285.89/41.33 % (424900)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=3306661668:s2a=on:i=256:s2at=5:ins=3:rtra=on_2610 on theBenchmark for (2610ds/256Mi) % 285.89/41.33 % (424902)dis+1010_1_to=kbo:si=on:random_seed=623052851:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2610 on theBenchmark for (2610ds/350Mi) % 285.89/41.33 % (424901)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=2201692395:i=78:ins=3:rtra=on_2610 on theBenchmark for (2610ds/78Mi) % 285.89/41.33 % (424901)Instruction limit reached! % 285.89/41.33 % (424901)------------------------------ % 285.89/41.33 % (424901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/42.22 % (424901)CaDiCaL version: 2.1.3 % 292.32/42.22 % (424901)Termination reason: Instruction limit % 292.32/42.22 % (424901)Termination phase: Saturation % 292.32/42.22 % (424901)Time elapsed: 0.029 s % 292.32/42.22 % (424901)Peak memory usage: 88 MB % 292.32/42.22 % (424901)Instructions burned: 78 (million) % 292.32/42.22 % (424900)Refutation not found, incomplete strategy % 292.32/42.22 % (424900)------------------------------ % 292.32/42.22 % (424900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/42.22 % (424900)CaDiCaL version: 2.1.3 % 292.32/42.22 % (424900)Termination reason: Refutation not found, incomplete strategy % 292.32/42.22 % (424900)Time elapsed: 0.092 s % 292.32/42.22 % (424900)Peak memory usage: 115 MB % 292.32/42.22 % (424900)Instructions burned: 172 (million) % 292.32/42.22 % (424902)Instruction limit reached! % 292.32/42.22 % (424902)------------------------------ % 292.32/42.22 % (424902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/42.22 % (424902)CaDiCaL version: 2.1.3 % 292.32/42.22 % (424902)Termination reason: Instruction limit % 292.32/42.22 % (424902)Termination phase: Saturation % 292.32/42.22 % (424902)Time elapsed: 0.077 s % 292.32/42.22 % (424902)Peak memory usage: 91 MB % 292.32/42.22 % (424902)Instructions burned: 351 (million) % 292.32/42.22 % (424907)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1946368108:s2a=on:i=966:doe=on:nm=32:rtra=on_2608 on theBenchmark for (2608ds/966Mi) % 292.32/42.22 % (424906)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1474647197:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2608 on theBenchmark for (2608ds/658Mi) % 292.32/42.22 % (424900)------------------------------ % 292.32/42.22 % (424900)------------------------------ % 292.32/42.22 % (424907)Instruction limit reached! % 292.32/42.22 % (424907)------------------------------ % 292.32/42.22 % (424907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/42.22 % (424907)CaDiCaL version: 2.1.3 % 292.32/42.22 % (424907)Termination reason: Instruction limit % 292.32/42.22 % (424907)Termination phase: Saturation % 292.32/42.22 % (424907)Time elapsed: 0.234 s % 292.32/42.22 % (424907)Peak memory usage: 138 MB % 292.32/42.22 % (424907)Instructions burned: 968 (million) % 292.32/42.22 % (424910)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=120733090:thitd=on:i=430:nm=0:rtra=on:ev=force_2605 on theBenchmark for (2605ds/430Mi) % 292.32/42.22 % (424906)Instruction limit reached! % 292.32/42.22 % (424906)------------------------------ % 292.32/42.22 % (424906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/42.22 % (424906)CaDiCaL version: 2.1.3 % 292.32/42.22 % (424906)Termination reason: Instruction limit % 292.32/42.22 % (424906)Termination phase: Saturation % 292.32/42.22 % (424906)Time elapsed: 0.281 s % 292.32/42.22 % (424906)Peak memory usage: 118 MB % 292.32/42.22 % (424906)Instructions burned: 659 (million) % 292.32/42.22 % (424911)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3990545688:i=698:rtra=on_2604 on theBenchmark for (2604ds/698Mi) % 292.32/42.22 % (424913)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=966764590:st=2:i=590:rtra=on:ss=axioms_2604 on theBenchmark for (2604ds/590Mi) % 292.32/42.22 % (424913)Refutation not found, incomplete strategy % 292.32/42.22 % (424913)------------------------------ % 292.32/42.22 % (424913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.32/42.22 % (424913)CaDiCaL version: 2.1.3 % 292.32/42.22 % (424913)Termination reason: Refutation not found, incomplete strategy % 292.32/42.22 % (424913)Time elapsed: 0.022 s % 292.32/42.22 % (424913)Peak memory usage: 88 MB % 292.32/42.22 % (424913)Instructions burned: 63 (million) % 292.32/42.22 % (424910)Instruction limit reached! % 292.32/42.22 % (424910)------------------------------ % 292.32/42.22 % (424910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.32/42.22 % (424910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.25/42.74 % (424910)CaDiCaL version: 2.1.3 % 295.25/42.74 % (424910)Termination reason: Instruction limit % 295.25/42.74 % (424910)Termination phase: Saturation % 295.25/42.74 % (424910)Time elapsed: 0.212 s % 295.25/42.74 % (424910)Peak memory usage: 135 MB % 295.25/42.74 % (424910)Instructions burned: 430 (million) % 295.25/42.74 % (424911)Instruction limit reached! % 295.25/42.74 % (424911)------------------------------ % 295.25/42.74 % (424911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.25/42.74 % (424911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.25/42.74 % (424911)CaDiCaL version: 2.1.3 % 295.25/42.74 % (424911)Termination reason: Instruction limit % 295.25/42.74 % (424911)Termination phase: Saturation % 295.25/42.74 % (424911)Time elapsed: 0.163 s % 295.25/42.74 % (424911)Peak memory usage: 120 MB % 295.25/42.74 % (424911)Instructions burned: 698 (million) % 295.25/42.74 % (424916)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1395147536:i=656:kws=inv_frequency:nm=20:rtra=on_2602 on theBenchmark for (2602ds/656Mi) % 295.25/42.74 % (424917)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1436734568:i=562:gtgl=2:rtra=on:gtg=all_2601 on theBenchmark for (2601ds/562Mi) % 295.25/42.74 % (424913)------------------------------ % 295.25/42.74 % (424913)------------------------------ % 295.25/42.74 % (424917)Instruction limit reached! % 295.25/42.74 % (424917)------------------------------ % 295.25/42.74 % (424917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.25/42.74 % (424917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.25/42.74 % (424917)CaDiCaL version: 2.1.3 % 295.25/42.74 % (424917)Termination reason: Instruction limit % 295.25/42.74 % (424917)Termination phase: Saturation % 295.25/42.74 % (424917)Time elapsed: 0.138 s % 295.25/42.74 % (424917)Peak memory usage: 120 MB % 295.25/42.74 % (424917)Instructions burned: 564 (million) % 295.25/42.74 % (424920)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2516022217:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2600 on theBenchmark for (2600ds/968Mi) % 295.25/42.74 % (424920)Refutation not found, incomplete strategy % 295.25/42.74 % (424920)------------------------------ % 295.25/42.74 % (424920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.25/42.74 % (424920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.25/42.74 % (424920)CaDiCaL version: 2.1.3 % 295.25/42.74 % (424920)Termination reason: Refutation not found, incomplete strategy % 295.25/42.74 % (424920)Time elapsed: 0.022 s % 295.25/42.74 % (424920)Peak memory usage: 88 MB % 295.25/42.74 % (424920)Instructions burned: 61 (million) % 295.25/42.74 % (424921)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=214965031:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2599 on theBenchmark for (2599ds/642Mi) % 295.25/42.74 % (424916)Instruction limit reached! % 295.25/42.74 % (424916)------------------------------ % 295.25/42.74 % (424916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.25/42.74 % (424916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.25/42.74 % (424916)CaDiCaL version: 2.1.3 % 295.25/42.74 % (424916)Termination reason: Instruction limit % 295.25/42.74 % (424916)Termination phase: Saturation % 295.25/42.74 % (424916)Time elapsed: 0.289 s % 295.25/42.74 % (424916)Peak memory usage: 119 MB % 295.25/42.74 % (424916)Instructions burned: 657 (million) % 295.25/42.74 % (424921)Refutation not found, incomplete strategy % 295.25/42.74 % (424921)------------------------------ % 295.25/42.74 % (424921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.25/42.74 % (424921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.25/42.74 % (424921)CaDiCaL version: 2.1.3 % 295.25/42.74 % (424921)Termination reason: Refutation not found, incomplete strategy % 295.25/42.74 % (424921)Time elapsed: 0.027 s % 295.25/42.74 % (424921)Peak memory usage: 112 MB % 295.25/42.74 % (424921)Instructions burned: 66 (million) % 295.25/42.74 % (424921)------------------------------ % 295.25/42.74 % (424921)------------------------------ % 295.25/42.74 % (424924)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1312884235:i=832:rtra=on:gtg=position:ss=axioms_2597 on theBenchmark for (2597ds/832Mi) % 295.25/42.74 % (424920)------------------------------ % 295.25/42.74 % (424920)------------------------------ % 295.25/42.74 % (424924)Refutation not found, incomplete strategy % 295.25/42.74 % (424924)------------------------------ % 295.25/42.74 % (424924)VersTerminated %------------------------------------------------------------------------------