%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX120_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n019.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:55 PM UTC 2026 % Result : Timeout 300.55s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX120_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.17 % Computer : n019.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 15:02:18 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.57/1.14 % (4069321)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.57/1.14 % (4069332)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2638806245:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.57/1.14 % (4069332)Instruction limit reached! % 4.57/1.14 % (4069332)------------------------------ % 4.57/1.14 % (4069332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.57/1.14 % (4069332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.14 % (4069332)CaDiCaL version: 2.1.3 % 4.57/1.14 % (4069332)Termination reason: Instruction limit % 4.57/1.14 % (4069332)Termination phase: Saturation % 4.57/1.14 % (4069332)Time elapsed: 0.028 s % 4.57/1.14 % (4069332)Peak memory usage: 116 MB % 4.57/1.14 % (4069332)Instructions burned: 34 (million) % 4.57/1.14 % (4069329)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2995252366:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.57/1.14 % (4069327)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1541099222:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.57/1.14 % (4069330)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3907084174:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.57/1.14 % (4069328)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2448722987:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.57/1.14 % (4069331)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=267014015:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.57/1.14 % (4069326)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2843983273:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.57/1.14 % (4069330)Instruction limit reached! % 4.57/1.14 % (4069330)------------------------------ % 4.57/1.14 % (4069330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.57/1.14 % (4069330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.14 % (4069330)CaDiCaL version: 2.1.3 % 4.57/1.14 % (4069330)Termination reason: Instruction limit % 4.57/1.14 % (4069330)Termination phase: Saturation % 4.57/1.14 % (4069330)Time elapsed: 0.004 s % 4.57/1.14 % (4069330)Peak memory usage: 89 MB % 4.57/1.14 % (4069330)Instructions burned: 5 (million) % 4.57/1.14 % (4069329)Instruction limit reached! % 4.57/1.14 % (4069329)------------------------------ % 4.57/1.14 % (4069329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.57/1.14 % (4069329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.14 % (4069329)CaDiCaL version: 2.1.3 % 4.57/1.14 % (4069329)Termination reason: Instruction limit % 4.57/1.14 % (4069329)Termination phase: Saturation % 4.57/1.14 % (4069329)Time elapsed: 0.006 s % 4.57/1.14 % (4069329)Peak memory usage: 88 MB % 4.57/1.14 % (4069329)Instructions burned: 7 (million) % 4.57/1.14 % (4069326)Instruction limit reached! % 4.57/1.14 % (4069326)------------------------------ % 4.57/1.14 % (4069326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.57/1.14 % (4069326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.14 % (4069326)CaDiCaL version: 2.1.3 % 4.57/1.14 % (4069326)Termination reason: Instruction limit % 4.57/1.14 % (4069326)Termination phase: Saturation % 4.57/1.14 % (4069326)Time elapsed: 0.031 s % 4.57/1.14 % (4069326)Peak memory usage: 115 MB % 4.57/1.14 % (4069326)Instructions burned: 13 (million) % 4.57/1.14 % (4069331)Instruction limit reached! % 4.57/1.14 % (4069331)------------------------------ % 4.57/1.14 % (4069331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.57/1.14 % (4069331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.14 % (4069331)CaDiCaL version: 2.1.3 % 4.57/1.14 % (4069331)Termination reason: Instruction limit % 4.57/1.14 % (4069331)Termination phase: Saturation % 4.57/1.14 % (4069331)Time elapsed: 0.056 s % 4.57/1.14 % (4069331)Peak memory usage: 116 MB % 4.57/1.14 % (4069331)Instructions burned: 46 (million) % 4.57/1.14 % (4069380)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=937652217:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.57/1.14 % (4069380)Instruction limit reached! % 4.57/1.14 % (4069380)------------------------------ % 5.27/1.39 % (4069380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.27/1.39 % (4069380)CaDiCaL version: 2.1.3 % 5.27/1.39 % (4069380)Termination reason: Instruction limit % 5.27/1.39 % (4069380)Termination phase: Saturation % 5.27/1.39 % (4069380)Time elapsed: 0.006 s % 5.27/1.39 % (4069380)Peak memory usage: 88 MB % 5.27/1.39 % (4069380)Instructions burned: 15 (million) % 5.27/1.39 % (4069328)Instruction limit reached! % 5.27/1.39 % (4069328)------------------------------ % 5.27/1.39 % (4069328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.27/1.39 % (4069328)CaDiCaL version: 2.1.3 % 5.27/1.39 % (4069328)Termination reason: Instruction limit % 5.27/1.39 % (4069328)Termination phase: Saturation % 5.27/1.39 % (4069328)Time elapsed: 0.145 s % 5.27/1.39 % (4069328)Peak memory usage: 118 MB % 5.27/1.39 % (4069328)Instructions burned: 202 (million) % 5.27/1.39 % (4069400)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3011451425:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 5.27/1.39 % (4069398)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=2646332082:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 5.27/1.39 % (4069400)Instruction limit reached! % 5.27/1.39 % (4069400)------------------------------ % 5.27/1.39 % (4069400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.27/1.39 % (4069400)CaDiCaL version: 2.1.3 % 5.27/1.39 % (4069400)Termination reason: Instruction limit % 5.27/1.39 % (4069400)Termination phase: Saturation % 5.27/1.39 % (4069400)Time elapsed: 0.013 s % 5.27/1.39 % (4069400)Peak memory usage: 91 MB % 5.27/1.39 % (4069400)Instructions burned: 17 (million) % 5.27/1.39 % (4069398)Instruction limit reached! % 5.27/1.39 % (4069398)------------------------------ % 5.27/1.39 % (4069398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.27/1.39 % (4069398)CaDiCaL version: 2.1.3 % 5.27/1.39 % (4069398)Termination reason: Instruction limit % 5.27/1.39 % (4069398)Termination phase: Saturation % 5.27/1.39 % (4069398)Time elapsed: 0.022 s % 5.27/1.39 % (4069398)Peak memory usage: 89 MB % 5.27/1.39 % (4069398)Instructions burned: 30 (million) % 5.27/1.39 % (4069409)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1795836234:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 5.27/1.39 % (4069411)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=369876098:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 5.27/1.39 % (4069411)Refutation not found, incomplete strategy % 5.27/1.39 % (4069411)------------------------------ % 5.27/1.39 % (4069411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.27/1.39 % (4069411)CaDiCaL version: 2.1.3 % 5.27/1.39 % (4069411)Termination reason: Refutation not found, incomplete strategy % 5.27/1.39 % (4069411)Time elapsed: 0.006 s % 5.27/1.39 % (4069411)Peak memory usage: 90 MB % 5.27/1.39 % (4069411)Instructions burned: 7 (million) % 5.27/1.39 % (4069409)Instruction limit reached! % 5.27/1.39 % (4069409)------------------------------ % 5.27/1.39 % (4069409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.27/1.39 % (4069409)CaDiCaL version: 2.1.3 % 5.27/1.39 % (4069409)Termination reason: Instruction limit % 5.27/1.39 % (4069409)Termination phase: Saturation % 5.27/1.39 % (4069409)Time elapsed: 0.020 s % 5.27/1.39 % (4069409)Peak memory usage: 89 MB % 5.27/1.39 % (4069409)Instructions burned: 25 (million) % 5.27/1.39 % (4069327)Instruction limit reached! % 5.27/1.39 % (4069327)------------------------------ % 5.27/1.39 % (4069327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.27/1.39 % (4069327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.67 % (4069327)CaDiCaL version: 2.1.3 % 6.73/1.67 % (4069327)Termination reason: Instruction limit % 6.73/1.67 % (4069327)Termination phase: Saturation % 6.73/1.67 % (4069327)Time elapsed: 0.233 s % 6.73/1.67 % (4069327)Peak memory usage: 117 MB % 6.73/1.67 % (4069327)Instructions burned: 307 (million) % 6.73/1.67 % (4069430)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4192292702:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 6.73/1.67 % (4069430)Instruction limit reached! % 6.73/1.67 % (4069430)------------------------------ % 6.73/1.67 % (4069430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.67 % (4069426)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=656260678:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 6.73/1.67 % (4069430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.67 % (4069430)CaDiCaL version: 2.1.3 % 6.73/1.67 % (4069430)Termination reason: Instruction limit % 6.73/1.67 % (4069430)Termination phase: Saturation % 6.73/1.67 % (4069430)Time elapsed: 0.002 s % 6.73/1.67 % (4069430)Peak memory usage: 88 MB % 6.73/1.67 % (4069430)Instructions burned: 3 (million) % 6.73/1.67 % (4069426)Instruction limit reached! % 6.73/1.67 % (4069426)------------------------------ % 6.73/1.67 % (4069426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.67 % (4069426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.67 % (4069426)CaDiCaL version: 2.1.3 % 6.73/1.67 % (4069426)Termination reason: Instruction limit % 6.73/1.67 % (4069426)Termination phase: Saturation % 6.73/1.67 % (4069426)Time elapsed: 0.054 s % 6.73/1.67 % (4069426)Peak memory usage: 89 MB % 6.73/1.67 % (4069426)Instructions burned: 86 (million) % 6.73/1.67 % (4069444)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2307727634:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 6.73/1.67 % (4069449)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1961207057:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 6.73/1.67 % (4069449)Instruction limit reached! % 6.73/1.67 % (4069449)------------------------------ % 6.73/1.67 % (4069449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.67 % (4069449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.67 % (4069449)CaDiCaL version: 2.1.3 % 6.73/1.67 % (4069449)Termination reason: Instruction limit % 6.73/1.67 % (4069449)Termination phase: Saturation % 6.73/1.67 % (4069449)Time elapsed: 0.004 s % 6.73/1.67 % (4069449)Peak memory usage: 88 MB % 6.73/1.67 % (4069449)Instructions burned: 5 (million) % 6.73/1.67 % (4069457)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1010592887:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 6.73/1.67 % (4069460)lrs+10_1_thi=all:si=on:fd=off:random_seed=3228185701:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.73/1.67 % (4069469)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=3336015873:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 6.73/1.67 % (4069469)Instruction limit reached! % 6.73/1.67 % (4069469)------------------------------ % 6.73/1.67 % (4069469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.67 % (4069469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.67 % (4069469)CaDiCaL version: 2.1.3 % 6.73/1.67 % (4069469)Termination reason: Instruction limit % 6.73/1.67 % (4069469)Termination phase: Saturation % 6.73/1.67 % (4069469)Time elapsed: 0.006 s % 6.73/1.67 % (4069469)Peak memory usage: 88 MB % 6.73/1.67 % (4069469)Instructions burned: 9 (million) % 6.73/1.67 % (4069460)Instruction limit reached! % 6.73/1.67 % (4069460)------------------------------ % 6.73/1.67 % (4069460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.73/1.67 % (4069460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.67 % (4069460)CaDiCaL version: 2.1.3 % 6.73/1.67 % (4069460)Termination reason: Instruction limit % 6.73/1.67 % (4069460)Termination phase: Saturation % 6.73/1.67 % (4069460)Time elapsed: 0.090 s % 6.73/1.67 % (4069460)Peak memory usage: 116 MB % 6.73/1.67 % (4069460)Instructions burned: 54 (million) % 6.73/1.67 % (4069444)Instruction limit reached! % 11.30/2.07 % (4069444)------------------------------ % 11.30/2.07 % (4069444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.30/2.07 % (4069444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.30/2.07 % (4069444)CaDiCaL version: 2.1.3 % 11.30/2.07 % (4069444)Termination reason: Instruction limit % 11.30/2.07 % (4069444)Termination phase: Saturation % 11.30/2.07 % (4069444)Time elapsed: 0.192 s % 11.30/2.07 % (4069444)Peak memory usage: 90 MB % 11.30/2.07 % (4069444)Instructions burned: 182 (million) % 11.30/2.07 % (4069457)Instruction limit reached! % 11.30/2.07 % (4069457)------------------------------ % 11.30/2.07 % (4069457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.30/2.07 % (4069457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.30/2.07 % (4069457)CaDiCaL version: 2.1.3 % 11.30/2.07 % (4069457)Termination reason: Instruction limit % 11.30/2.07 % (4069457)Termination phase: Saturation % 11.30/2.07 % (4069457)Time elapsed: 0.143 s % 11.30/2.07 % (4069457)Peak memory usage: 134 MB % 11.30/2.07 % (4069457)Instructions burned: 66 (million) % 11.30/2.07 % (4069411)------------------------------ % 11.30/2.07 % (4069411)------------------------------ % 11.30/2.07 % (4069491)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=665000296:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 11.30/2.07 % (4069491)Instruction limit reached! % 11.30/2.07 % (4069491)------------------------------ % 11.30/2.07 % (4069491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.30/2.07 % (4069491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.30/2.07 % (4069491)CaDiCaL version: 2.1.3 % 11.30/2.07 % (4069491)Termination reason: Instruction limit % 11.30/2.07 % (4069491)Termination phase: Property scanning % 11.30/2.07 % (4069491)Time elapsed: 0.003 s % 11.30/2.07 % (4069491)Peak memory usage: 86 MB % 11.30/2.07 % (4069491)Instructions burned: 2 (million) % 11.30/2.07 % (4069483)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4159487520:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 11.30/2.07 % (4069483)Instruction limit reached! % 11.30/2.07 % (4069483)------------------------------ % 11.30/2.07 % (4069483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.30/2.07 % (4069483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.30/2.07 % (4069483)CaDiCaL version: 2.1.3 % 11.30/2.07 % (4069483)Termination reason: Instruction limit % 11.30/2.07 % (4069483)Termination phase: Property scanning % 11.30/2.07 % (4069483)Time elapsed: 0.003 s % 11.30/2.07 % (4069483)Peak memory usage: 86 MB % 11.30/2.07 % (4069483)Instructions burned: 2 (million) % 11.30/2.07 % (4069515)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3637427695:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi) % 11.30/2.07 % (4069515)Instruction limit reached! % 11.30/2.07 % (4069515)------------------------------ % 11.30/2.07 % (4069515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.30/2.07 % (4069515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.30/2.07 % (4069515)CaDiCaL version: 2.1.3 % 11.30/2.07 % (4069515)Termination reason: Instruction limit % 11.30/2.07 % (4069515)Termination phase: Saturation % 11.30/2.07 % (4069515)Time elapsed: 0.090 s % 11.30/2.07 % (4069515)Peak memory usage: 117 MB % 11.30/2.07 % (4069515)Instructions burned: 127 (million) % 11.30/2.07 % (4069521)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2589943907:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 11.30/2.07 % (4069520)dis+10_1_si=on:random_seed=2700030895:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 11.30/2.07 % (4069524)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4049735539:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2992 on theBenchmark for (2992ds/35Mi) % 11.30/2.07 % (4069521)Refutation not found, incomplete strategy % 11.30/2.07 % (4069521)------------------------------ % 11.30/2.07 % (4069521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.30/2.07 % (4069521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.30/2.07 % (4069521)CaDiCaL version: 2.1.3 % 11.30/2.07 % (4069521)Termination reason: Refutation not found, incomplete strategy % 11.30/2.07 % (4069521)Time elapsed: 0.007 s % 11.30/2.07 % (4069521)Peak memory usage: 89 MB % 12.81/2.53 % (4069521)Instructions burned: 5 (million) % 12.81/2.53 % (4069520)Instruction limit reached! % 12.81/2.53 % (4069520)------------------------------ % 12.81/2.53 % (4069520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.53 % (4069520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.53 % (4069520)CaDiCaL version: 2.1.3 % 12.81/2.53 % (4069520)Termination reason: Instruction limit % 12.81/2.53 % (4069520)Termination phase: Saturation % 12.81/2.53 % (4069520)Time elapsed: 0.013 s % 12.81/2.53 % (4069520)Peak memory usage: 88 MB % 12.81/2.53 % (4069520)Instructions burned: 11 (million) % 12.81/2.53 % (4069530)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1223084716:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 12.81/2.53 % (4069525)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1149532597:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi) % 12.81/2.53 % (4069525)Instruction limit reached! % 12.81/2.53 % (4069525)------------------------------ % 12.81/2.53 % (4069525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.53 % (4069525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.53 % (4069525)CaDiCaL version: 2.1.3 % 12.81/2.53 % (4069525)Termination reason: Instruction limit % 12.81/2.53 % (4069525)Termination phase: Property scanning % 12.81/2.53 % (4069525)Time elapsed: 0.004 s % 12.81/2.53 % (4069525)Peak memory usage: 86 MB % 12.81/2.53 % (4069525)Instructions burned: 3 (million) % 12.81/2.53 % (4069530)Instruction limit reached! % 12.81/2.53 % (4069530)------------------------------ % 12.81/2.53 % (4069530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.53 % (4069530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.53 % (4069530)CaDiCaL version: 2.1.3 % 12.81/2.53 % (4069530)Termination reason: Instruction limit % 12.81/2.53 % (4069530)Termination phase: Saturation % 12.81/2.53 % (4069530)Time elapsed: 0.009 s % 12.81/2.53 % (4069530)Peak memory usage: 89 MB % 12.81/2.53 % (4069530)Instructions burned: 8 (million) % 12.81/2.53 % (4069524)Instruction limit reached! % 12.81/2.53 % (4069524)------------------------------ % 12.81/2.53 % (4069524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.53 % (4069524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.53 % (4069524)CaDiCaL version: 2.1.3 % 12.81/2.53 % (4069524)Termination reason: Instruction limit % 12.81/2.53 % (4069524)Termination phase: Saturation % 12.81/2.53 % (4069524)Time elapsed: 0.047 s % 12.81/2.53 % (4069524)Peak memory usage: 89 MB % 12.81/2.53 % (4069524)Instructions burned: 35 (million) % 12.81/2.53 % (4069536)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=147358264:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi) % 12.81/2.53 % (4069536)Refutation not found, incomplete strategy % 12.81/2.53 % (4069536)------------------------------ % 12.81/2.53 % (4069536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.53 % (4069536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.53 % (4069536)CaDiCaL version: 2.1.3 % 12.81/2.53 % (4069536)Termination reason: Refutation not found, incomplete strategy % 12.81/2.53 % (4069536)Time elapsed: 0.007 s % 12.81/2.53 % (4069536)Peak memory usage: 88 MB % 12.81/2.53 % (4069536)Instructions burned: 4 (million) % 12.81/2.53 % (4069540)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1875058672:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 12.81/2.53 % (4069540)Instruction limit reached! % 12.81/2.53 % (4069540)------------------------------ % 12.81/2.53 % (4069540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.53 % (4069540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.53 % (4069540)CaDiCaL version: 2.1.3 % 12.81/2.53 % (4069540)Termination reason: Instruction limit % 12.81/2.53 % (4069540)Termination phase: Saturation % 12.81/2.53 % (4069540)Time elapsed: 0.021 s % 12.81/2.53 % (4069540)Peak memory usage: 113 MB % 12.81/2.53 % (4069540)Instructions burned: 13 (million) % 12.81/2.53 % (4069545)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2324081339:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi) % 12.81/2.53 % (4069547)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3847511261:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 14.64/2.88 % (4069548)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3977014422:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi) % 14.64/2.88 % (4069547)Instruction limit reached! % 14.64/2.88 % (4069547)------------------------------ % 14.64/2.88 % (4069547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.88 % (4069547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.88 % (4069547)CaDiCaL version: 2.1.3 % 14.64/2.88 % (4069547)Termination reason: Instruction limit % 14.64/2.88 % (4069547)Termination phase: Saturation % 14.64/2.88 % (4069547)Time elapsed: 0.008 s % 14.64/2.88 % (4069547)Peak memory usage: 88 MB % 14.64/2.88 % (4069547)Instructions burned: 10 (million) % 14.64/2.88 % (4069549)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=2142638600:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2990 on theBenchmark for (2990ds/75Mi) % 14.64/2.88 % (4069521)------------------------------ % 14.64/2.88 % (4069521)------------------------------ % 14.64/2.88 % (4069549)Instruction limit reached! % 14.64/2.88 % (4069549)------------------------------ % 14.64/2.88 % (4069549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.88 % (4069549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.88 % (4069549)CaDiCaL version: 2.1.3 % 14.64/2.88 % (4069549)Termination reason: Instruction limit % 14.64/2.88 % (4069549)Termination phase: Saturation % 14.64/2.88 % (4069549)Time elapsed: 0.088 s % 14.64/2.88 % (4069549)Peak memory usage: 90 MB % 14.64/2.88 % (4069549)Instructions burned: 75 (million) % 14.64/2.88 % (4069560)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=3370770574:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 14.64/2.88 % (4069548)Instruction limit reached! % 14.64/2.88 % (4069548)------------------------------ % 14.64/2.88 % (4069548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.88 % (4069548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.88 % (4069548)CaDiCaL version: 2.1.3 % 14.64/2.88 % (4069548)Termination reason: Instruction limit % 14.64/2.88 % (4069548)Termination phase: Saturation % 14.64/2.88 % (4069548)Time elapsed: 0.139 s % 14.64/2.88 % (4069548)Peak memory usage: 133 MB % 14.64/2.88 % (4069548)Instructions burned: 71 (million) % 14.64/2.88 % (4069536)------------------------------ % 14.64/2.88 % (4069536)------------------------------ % 14.64/2.88 % (4069545)Instruction limit reached! % 14.64/2.88 % (4069545)------------------------------ % 14.64/2.88 % (4069545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.88 % (4069545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.88 % (4069545)CaDiCaL version: 2.1.3 % 14.64/2.88 % (4069545)Termination reason: Instruction limit % 14.64/2.88 % (4069545)Termination phase: Saturation % 14.64/2.88 % (4069545)Time elapsed: 0.247 s % 14.64/2.88 % (4069545)Peak memory usage: 117 MB % 14.64/2.88 % (4069545)Instructions burned: 226 (million) % 14.64/2.88 % (4069565)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=140090539:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 14.64/2.88 % (4069572)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2625387680:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi) % 14.64/2.88 % (4069568)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=619518784:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 14.64/2.88 % (4069569)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=782191125:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi) % 14.64/2.88 % (4069560)Instruction limit reached! % 14.64/2.88 % (4069560)------------------------------ % 14.64/2.88 % (4069560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.64/2.88 % (4069560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.64/2.88 % (4069560)CaDiCaL version: 2.1.3 % 14.64/2.88 % (4069560)Termination reason: Instruction limit % 14.64/2.88 % (4069560)Termination phase: Saturation % 14.64/2.88 % (4069560)Time elapsed: 0.270 s % 19.75/3.35 % (4069560)Peak memory usage: 91 MB % 19.75/3.35 % (4069560)Instructions burned: 294 (million) % 19.75/3.35 % (4069565)Instruction limit reached! % 19.75/3.35 % (4069565)------------------------------ % 19.75/3.35 % (4069565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.35 % (4069565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.35 % (4069565)CaDiCaL version: 2.1.3 % 19.75/3.35 % (4069565)Termination reason: Instruction limit % 19.75/3.35 % (4069565)Termination phase: Saturation % 19.75/3.35 % (4069565)Time elapsed: 0.179 s % 19.75/3.35 % (4069565)Peak memory usage: 117 MB % 19.75/3.35 % (4069565)Instructions burned: 130 (million) % 19.75/3.35 % (4069575)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=263427931:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi) % 19.75/3.35 % (4069569)Instruction limit reached! % 19.75/3.35 % (4069569)------------------------------ % 19.75/3.35 % (4069569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.35 % (4069569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.35 % (4069569)CaDiCaL version: 2.1.3 % 19.75/3.35 % (4069569)Termination reason: Instruction limit % 19.75/3.35 % (4069569)Termination phase: Saturation % 19.75/3.35 % (4069569)Time elapsed: 0.100 s % 19.75/3.35 % (4069569)Peak memory usage: 133 MB % 19.75/3.35 % (4069569)Instructions burned: 40 (million) % 19.75/3.35 % (4069577)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=404891610:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 19.75/3.35 % (4069572)Instruction limit reached! % 19.75/3.35 % (4069572)------------------------------ % 19.75/3.35 % (4069572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.35 % (4069572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.35 % (4069572)CaDiCaL version: 2.1.3 % 19.75/3.35 % (4069572)Termination reason: Instruction limit % 19.75/3.35 % (4069572)Termination phase: Saturation % 19.75/3.35 % (4069572)Time elapsed: 0.193 s % 19.75/3.35 % (4069572)Peak memory usage: 92 MB % 19.75/3.35 % (4069572)Instructions burned: 307 (million) % 19.75/3.35 % (4069568)Instruction limit reached! % 19.75/3.35 % (4069568)------------------------------ % 19.75/3.35 % (4069568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.35 % (4069568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.35 % (4069568)CaDiCaL version: 2.1.3 % 19.75/3.35 % (4069568)Termination reason: Instruction limit % 19.75/3.35 % (4069568)Termination phase: Saturation % 19.75/3.35 % (4069568)Time elapsed: 0.206 s % 19.75/3.35 % (4069568)Peak memory usage: 136 MB % 19.75/3.35 % (4069568)Instructions burned: 131 (million) % 19.75/3.35 % (4069585)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=2730277877:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 19.75/3.35 % (4069577)Instruction limit reached! % 19.75/3.35 % (4069577)------------------------------ % 19.75/3.35 % (4069577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.75/3.35 % (4069577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.75/3.35 % (4069577)CaDiCaL version: 2.1.3 % 19.75/3.35 % (4069577)Termination reason: Instruction limit % 19.75/3.35 % (4069577)Termination phase: Saturation % 19.75/3.35 % (4069577)Time elapsed: 0.153 s % 19.75/3.35 % (4069577)Peak memory usage: 117 MB % 19.75/3.35 % (4069577)Instructions burned: 131 (million) % 19.75/3.35 % (4069587)dis+10_1_si=on:random_seed=3099184281:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi) % 19.75/3.35 % (4069589)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2923844491:i=383:fsr=off:rtra=on:ev=force_2983 on theBenchmark for (2983ds/383Mi) % 19.75/3.35 % (4069591)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4019892641:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi) % 19.75/3.35 % (4069592)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2629407540:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi) % 19.75/3.35 % (4069592)Instruction limit reached! % 19.75/3.35 % (4069592)------------------------------ % 19.75/3.35 % (4069592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069592)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069592)Termination reason: Instruction limit % 22.19/3.82 % (4069592)Termination phase: Saturation % 22.19/3.82 % (4069592)Time elapsed: 0.057 s % 22.19/3.82 % (4069592)Peak memory usage: 117 MB % 22.19/3.82 % (4069592)Instructions burned: 65 (million) % 22.19/3.82 % (4069591)Instruction limit reached! % 22.19/3.82 % (4069591)------------------------------ % 22.19/3.82 % (4069591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069591)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069591)Termination reason: Instruction limit % 22.19/3.82 % (4069591)Termination phase: Saturation % 22.19/3.82 % (4069591)Time elapsed: 0.102 s % 22.19/3.82 % (4069591)Peak memory usage: 91 MB % 22.19/3.82 % (4069591)Instructions burned: 141 (million) % 22.19/3.82 % (4069597)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=841721356:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi) % 22.19/3.82 % (4069585)Instruction limit reached! % 22.19/3.82 % (4069585)------------------------------ % 22.19/3.82 % (4069585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069585)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069585)Termination reason: Instruction limit % 22.19/3.82 % (4069585)Termination phase: Saturation % 22.19/3.82 % (4069585)Time elapsed: 0.318 s % 22.19/3.82 % (4069585)Peak memory usage: 119 MB % 22.19/3.82 % (4069585)Instructions burned: 259 (million) % 22.19/3.82 % (4069597)Instruction limit reached! % 22.19/3.82 % (4069597)------------------------------ % 22.19/3.82 % (4069597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069597)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069597)Termination reason: Instruction limit % 22.19/3.82 % (4069597)Termination phase: Saturation % 22.19/3.82 % (4069597)Time elapsed: 0.130 s % 22.19/3.82 % (4069597)Peak memory usage: 90 MB % 22.19/3.82 % (4069597)Instructions burned: 121 (million) % 22.19/3.82 % (4069575)Instruction limit reached! % 22.19/3.82 % (4069575)------------------------------ % 22.19/3.82 % (4069575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069575)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069575)Termination reason: Instruction limit % 22.19/3.82 % (4069575)Termination phase: Saturation % 22.19/3.82 % (4069575)Time elapsed: 0.619 s % 22.19/3.82 % (4069575)Peak memory usage: 137 MB % 22.19/3.82 % (4069575)Instructions burned: 598 (million) % 22.19/3.82 % (4069603)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=296032537:s2a=on:i=128:s2at=5:ins=3:rtra=on_2979 on theBenchmark for (2979ds/128Mi) % 22.19/3.82 % (4069589)Instruction limit reached! % 22.19/3.82 % (4069589)------------------------------ % 22.19/3.82 % (4069589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069589)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069589)Termination reason: Instruction limit % 22.19/3.82 % (4069589)Termination phase: Saturation % 22.19/3.82 % (4069589)Time elapsed: 0.393 s % 22.19/3.82 % (4069589)Peak memory usage: 91 MB % 22.19/3.82 % (4069589)Instructions burned: 383 (million) % 22.19/3.82 % (4069604)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=2288830473:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi) % 22.19/3.82 % (4069603)Instruction limit reached! % 22.19/3.82 % (4069603)------------------------------ % 22.19/3.82 % (4069603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.19/3.82 % (4069603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.82 % (4069603)CaDiCaL version: 2.1.3 % 22.19/3.82 % (4069603)Termination reason: Instruction limit % 22.19/3.82 % (4069603)Termination phase: Saturation % 22.19/3.82 % (4069603)Time elapsed: 0.098 s % 22.19/3.82 % (4069603)Peak memory usage: 119 MB % 22.19/3.82 % (4069603)Instructions burned: 129 (million) % 22.19/3.82 % (4069604)Instruction limit reached! % 22.19/3.82 % (4069604)------------------------------ % 27.23/4.52 % (4069604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.52 % (4069604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.52 % (4069604)CaDiCaL version: 2.1.3 % 27.23/4.52 % (4069604)Termination reason: Instruction limit % 27.23/4.52 % (4069604)Termination phase: Saturation % 27.23/4.52 % (4069604)Time elapsed: 0.076 s % 27.23/4.52 % (4069604)Peak memory usage: 117 MB % 27.23/4.52 % (4069604)Instructions burned: 39 (million) % 27.23/4.52 % (4069606)dis+1010_1_to=kbo:si=on:random_seed=1900699766:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi) % 27.23/4.52 % (4069607)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1689299945:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/329Mi) % 27.23/4.52 % (4069609)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1599556305:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 27.23/4.52 % (4069610)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2130511822:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi) % 27.23/4.52 % (4069606)Instruction limit reached! % 27.23/4.52 % (4069606)------------------------------ % 27.23/4.52 % (4069606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.52 % (4069606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.52 % (4069606)CaDiCaL version: 2.1.3 % 27.23/4.52 % (4069606)Termination reason: Instruction limit % 27.23/4.52 % (4069606)Termination phase: Saturation % 27.23/4.52 % (4069606)Time elapsed: 0.197 s % 27.23/4.52 % (4069606)Peak memory usage: 91 MB % 27.23/4.52 % (4069606)Instructions burned: 176 (million) % 27.23/4.52 % (4069616)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=985420103:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi) % 27.23/4.52 % (4069614)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3281717744:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi) % 27.23/4.52 % (4069587)Instruction limit reached! % 27.23/4.52 % (4069587)------------------------------ % 27.23/4.52 % (4069587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.52 % (4069587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.52 % (4069587)CaDiCaL version: 2.1.3 % 27.23/4.52 % (4069587)Termination reason: Instruction limit % 27.23/4.52 % (4069587)Termination phase: Saturation % 27.23/4.52 % (4069587)Time elapsed: 0.793 s % 27.23/4.52 % (4069587)Peak memory usage: 97 MB % 27.23/4.52 % (4069587)Instructions burned: 1001 (million) % 27.23/4.52 % (4069616)Instruction limit reached! % 27.23/4.52 % (4069616)------------------------------ % 27.23/4.52 % (4069616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.52 % (4069616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.52 % (4069616)CaDiCaL version: 2.1.3 % 27.23/4.52 % (4069616)Termination reason: Instruction limit % 27.23/4.52 % (4069616)Termination phase: Saturation % 27.23/4.52 % (4069616)Time elapsed: 0.147 s % 27.23/4.52 % (4069616)Peak memory usage: 91 MB % 27.23/4.52 % (4069616)Instructions burned: 296 (million) % 27.23/4.52 % (4069610)Instruction limit reached! % 27.23/4.52 % (4069610)------------------------------ % 27.23/4.52 % (4069610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.52 % (4069610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.52 % (4069610)CaDiCaL version: 2.1.3 % 27.23/4.52 % (4069610)Termination reason: Instruction limit % 27.23/4.52 % (4069610)Termination phase: Saturation % 27.23/4.52 % (4069610)Time elapsed: 0.276 s % 27.23/4.52 % (4069610)Peak memory usage: 135 MB % 27.23/4.52 % (4069610)Instructions burned: 215 (million) % 27.23/4.52 % (4069607)Instruction limit reached! % 27.23/4.52 % (4069607)------------------------------ % 27.23/4.52 % (4069607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.52 % (4069607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.52 % (4069607)CaDiCaL version: 2.1.3 % 27.23/4.52 % (4069607)Termination reason: Instruction limit % 27.23/4.52 % (4069607)Termination phase: Saturation % 27.23/4.52 % (4069607)Time elapsed: 0.371 s % 27.23/4.52 % (4069607)Peak memory usage: 119 MB % 27.23/4.52 % (4069607)Instructions burned: 332 (million) % 28.40/4.85 % (4069621)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1532803173:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi) % 28.40/4.85 % (4069625)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3459038562:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi) % 28.40/4.85 % (4069626)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1553509413:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi) % 28.40/4.85 % (4069614)Instruction limit reached! % 28.40/4.85 % (4069614)------------------------------ % 28.40/4.85 % (4069614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.40/4.85 % (4069614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.40/4.85 % (4069614)CaDiCaL version: 2.1.3 % 28.40/4.85 % (4069614)Termination reason: Instruction limit % 28.40/4.85 % (4069614)Termination phase: Saturation % 28.40/4.85 % (4069614)Time elapsed: 0.394 s % 28.40/4.85 % (4069614)Peak memory usage: 119 MB % 28.40/4.85 % (4069614)Instructions burned: 349 (million) % 28.40/4.85 % (4069627)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1727022356:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi) % 28.40/4.85 % (4069609)Instruction limit reached! % 28.40/4.85 % (4069609)------------------------------ % 28.40/4.85 % (4069609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.40/4.85 % (4069609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.40/4.85 % (4069609)CaDiCaL version: 2.1.3 % 28.40/4.85 % (4069609)Termination reason: Instruction limit % 28.40/4.85 % (4069609)Termination phase: Saturation % 28.40/4.85 % (4069609)Time elapsed: 0.615 s % 28.40/4.85 % (4069609)Peak memory usage: 136 MB % 28.40/4.85 % (4069609)Instructions burned: 483 (million) % 28.40/4.85 % (4069628)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2493000930:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi) % 28.40/4.85 % (4069626)Instruction limit reached! % 28.40/4.85 % (4069626)------------------------------ % 28.40/4.85 % (4069626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.40/4.85 % (4069626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.40/4.85 % (4069626)CaDiCaL version: 2.1.3 % 28.40/4.85 % (4069626)Termination reason: Instruction limit % 28.40/4.85 % (4069626)Termination phase: Saturation % 28.40/4.85 % (4069626)Time elapsed: 0.235 s % 28.40/4.85 % (4069626)Peak memory usage: 92 MB % 28.40/4.85 % (4069626)Instructions burned: 485 (million) % 28.40/4.85 % (4069632)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1423804975:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 28.40/4.85 % (4069621)Instruction limit reached! % 28.40/4.85 % (4069621)------------------------------ % 28.40/4.85 % (4069621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.40/4.85 % (4069621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.40/4.85 % (4069621)CaDiCaL version: 2.1.3 % 28.40/4.85 % (4069621)Termination reason: Instruction limit % 28.40/4.85 % (4069621)Termination phase: Saturation % 28.40/4.85 % (4069621)Time elapsed: 0.359 s % 28.40/4.85 % (4069621)Peak memory usage: 118 MB % 28.40/4.85 % (4069621)Instructions burned: 329 (million) % 28.40/4.85 % (4069625)Instruction limit reached! % 28.40/4.85 % (4069625)------------------------------ % 28.40/4.85 % (4069625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.40/4.85 % (4069625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.40/4.85 % (4069625)CaDiCaL version: 2.1.3 % 28.40/4.85 % (4069625)Termination reason: Instruction limit % 28.40/4.85 % (4069625)Termination phase: Saturation % 28.40/4.85 % (4069625)Time elapsed: 0.332 s % 28.40/4.85 % (4069625)Peak memory usage: 120 MB % 28.40/4.85 % (4069625)Instructions burned: 281 (million) % 28.40/4.85 % (4069627)Instruction limit reached! % 28.40/4.85 % (4069627)------------------------------ % 28.40/4.85 % (4069627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.40/4.85 % (4069627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.40/4.85 % (4069627)CaDiCaL version: 2.1.3 % 28.40/4.85 % (4069627)Termination reason: Instruction limit % 28.40/4.85 % (4069627)Termination phase: Saturation % 35.39/5.80 % (4069627)Time elapsed: 0.291 s % 35.39/5.80 % (4069627)Peak memory usage: 113 MB % 35.39/5.80 % (4069627)Instructions burned: 322 (million) % 35.39/5.80 % (4069635)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=70582165:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi) % 35.39/5.80 % (4069639)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1995192743:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi) % 35.39/5.80 % (4069642)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2733996473:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/387Mi) % 35.39/5.80 % (4069643)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1643289669:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2966 on theBenchmark for (2966ds/513Mi) % 35.39/5.80 % (4069628)Instruction limit reached! % 35.39/5.80 % (4069628)------------------------------ % 35.39/5.80 % (4069628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.39/5.80 % (4069628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.39/5.80 % (4069628)CaDiCaL version: 2.1.3 % 35.39/5.80 % (4069628)Termination reason: Instruction limit % 35.39/5.80 % (4069628)Termination phase: Saturation % 35.39/5.80 % (4069628)Time elapsed: 0.408 s % 35.39/5.80 % (4069628)Peak memory usage: 119 MB % 35.39/5.80 % (4069628)Instructions burned: 417 (million) % 35.39/5.80 % (4069644)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2712506429:i=334:rtra=on_2966 on theBenchmark for (2966ds/334Mi) % 35.39/5.80 % (4069639)Instruction limit reached! % 35.39/5.80 % (4069639)------------------------------ % 35.39/5.80 % (4069639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.39/5.80 % (4069639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.39/5.80 % (4069639)CaDiCaL version: 2.1.3 % 35.39/5.80 % (4069639)Termination reason: Instruction limit % 35.39/5.80 % (4069639)Termination phase: Saturation % 35.39/5.80 % (4069639)Time elapsed: 0.232 s % 35.39/5.80 % (4069639)Peak memory usage: 121 MB % 35.39/5.80 % (4069639)Instructions burned: 376 (million) % 35.39/5.80 % (4069635)Instruction limit reached! % 35.39/5.80 % (4069635)------------------------------ % 35.39/5.80 % (4069635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.39/5.80 % (4069635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.39/5.80 % (4069635)CaDiCaL version: 2.1.3 % 35.39/5.80 % (4069635)Termination reason: Instruction limit % 35.39/5.80 % (4069635)Termination phase: Saturation % 35.39/5.80 % (4069635)Time elapsed: 0.353 s % 35.39/5.80 % (4069635)Peak memory usage: 136 MB % 35.39/5.80 % (4069635)Instructions burned: 276 (million) % 35.39/5.80 % (4069632)Instruction limit reached! % 35.39/5.80 % (4069632)------------------------------ % 35.39/5.80 % (4069632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.39/5.80 % (4069632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.39/5.80 % (4069632)CaDiCaL version: 2.1.3 % 35.39/5.80 % (4069632)Termination reason: Instruction limit % 35.39/5.80 % (4069632)Termination phase: Saturation % 35.39/5.80 % (4069632)Time elapsed: 0.537 s % 35.39/5.80 % (4069632)Peak memory usage: 122 MB % 35.39/5.80 % (4069632)Instructions burned: 471 (million) % 35.39/5.80 % (4069649)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1438489898:i=359:rtra=on:gtg=exists_top:ss=axioms_2964 on theBenchmark for (2964ds/359Mi) % 35.39/5.80 % (4069651)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2426641894:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2963 on theBenchmark for (2963ds/341Mi) % 35.39/5.80 % (4069644)Instruction limit reached! % 35.39/5.80 % (4069644)------------------------------ % 35.39/5.80 % (4069644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.39/5.80 % (4069644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.39/5.80 % (4069644)CaDiCaL version: 2.1.3 % 35.39/5.80 % (4069644)Termination reason: Instruction limit % 35.39/5.80 % (4069644)Termination phase: Saturation % 35.39/5.80 % (4069644)Time elapsed: 0.419 s % 35.39/5.80 % (4069644)Peak memory usage: 136 MB % 35.39/5.80 % (4069644)Instructions burned: 334 (million) % 41.13/6.49 % (4069642)Instruction limit reached! % 41.13/6.49 % (4069642)------------------------------ % 41.13/6.49 % (4069642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.49 % (4069642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.49 % (4069642)CaDiCaL version: 2.1.3 % 41.13/6.49 % (4069642)Termination reason: Instruction limit % 41.13/6.49 % (4069642)Termination phase: Saturation % 41.13/6.49 % (4069642)Time elapsed: 0.531 s % 41.13/6.49 % (4069642)Peak memory usage: 120 MB % 41.13/6.49 % (4069642)Instructions burned: 388 (million) % 41.13/6.49 % (4069652)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1794114678:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/261Mi) % 41.13/6.49 % (4069653)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=3209476247:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi) % 41.13/6.49 % (4069643)Instruction limit reached! % 41.13/6.49 % (4069643)------------------------------ % 41.13/6.49 % (4069643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.49 % (4069643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.49 % (4069643)CaDiCaL version: 2.1.3 % 41.13/6.49 % (4069643)Termination reason: Instruction limit % 41.13/6.49 % (4069643)Termination phase: Saturation % 41.13/6.49 % (4069643)Time elapsed: 0.536 s % 41.13/6.49 % (4069643)Peak memory usage: 93 MB % 41.13/6.49 % (4069643)Instructions burned: 513 (million) % 41.13/6.49 % (4069651)Instruction limit reached! % 41.13/6.49 % (4069651)------------------------------ % 41.13/6.49 % (4069651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.49 % (4069651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.49 % (4069651)CaDiCaL version: 2.1.3 % 41.13/6.49 % (4069651)Termination reason: Instruction limit % 41.13/6.49 % (4069651)Termination phase: Saturation % 41.13/6.49 % (4069651)Time elapsed: 0.213 s % 41.13/6.49 % (4069651)Peak memory usage: 118 MB % 41.13/6.49 % (4069651)Instructions burned: 341 (million) % 41.13/6.49 % (4069649)Instruction limit reached! % 41.13/6.49 % (4069649)------------------------------ % 41.13/6.49 % (4069649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.49 % (4069649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.49 % (4069649)CaDiCaL version: 2.1.3 % 41.13/6.49 % (4069649)Termination reason: Instruction limit % 41.13/6.49 % (4069649)Termination phase: Saturation % 41.13/6.49 % (4069649)Time elapsed: 0.399 s % 41.13/6.49 % (4069649)Peak memory usage: 91 MB % 41.13/6.49 % (4069649)Instructions burned: 360 (million) % 41.13/6.49 % (4069660)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2995074997:i=4428:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/4428Mi) % 41.13/6.49 % (4069661)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=889406011:avsq=on:i=276:avsqr=1,2:rtra=on_2958 on theBenchmark for (2958ds/276Mi) % 41.13/6.49 % (4069658)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4194826453:i=146:doe=on:rtra=on_2959 on theBenchmark for (2959ds/146Mi) % 41.13/6.49 % (4069657)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2782192661:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 41.13/6.49 % (4069652)Instruction limit reached! % 41.13/6.49 % (4069652)------------------------------ % 41.13/6.49 % (4069652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.49 % (4069652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.49 % (4069652)CaDiCaL version: 2.1.3 % 41.13/6.49 % (4069652)Termination reason: Instruction limit % 41.13/6.49 % (4069652)Termination phase: Saturation % 41.13/6.49 % (4069652)Time elapsed: 0.298 s % 41.13/6.49 % (4069652)Peak memory usage: 119 MB % 41.13/6.49 % (4069652)Instructions burned: 261 (million) % 41.13/6.49 % (4069653)Instruction limit reached! % 41.13/6.49 % (4069653)------------------------------ % 41.13/6.49 % (4069653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.13/6.49 % (4069653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.13/6.49 % (4069653)CaDiCaL version: 2.1.3 % 47.08/7.26 % (4069653)Termination reason: Instruction limit % 47.08/7.26 % (4069653)Termination phase: Saturation % 47.08/7.26 % (4069653)Time elapsed: 0.297 s % 47.08/7.26 % (4069653)Peak memory usage: 118 MB % 47.08/7.26 % (4069653)Instructions burned: 236 (million) % 47.08/7.26 % (4069658)Instruction limit reached! % 47.08/7.26 % (4069658)------------------------------ % 47.08/7.26 % (4069658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.08/7.26 % (4069658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.08/7.26 % (4069658)CaDiCaL version: 2.1.3 % 47.08/7.26 % (4069658)Termination reason: Instruction limit % 47.08/7.26 % (4069658)Termination phase: Saturation % 47.08/7.26 % (4069658)Time elapsed: 0.155 s % 47.08/7.26 % (4069658)Peak memory usage: 90 MB % 47.08/7.26 % (4069658)Instructions burned: 147 (million) % 47.08/7.26 % (4069662)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=608042078:i=1052:rtra=on_2957 on theBenchmark for (2957ds/1052Mi) % 47.08/7.26 % (4069661)Instruction limit reached! % 47.08/7.26 % (4069661)------------------------------ % 47.08/7.26 % (4069661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.08/7.26 % (4069661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.08/7.26 % (4069661)CaDiCaL version: 2.1.3 % 47.08/7.26 % (4069661)Termination reason: Instruction limit % 47.08/7.26 % (4069661)Termination phase: Saturation % 47.08/7.26 % (4069661)Time elapsed: 0.326 s % 47.08/7.26 % (4069661)Peak memory usage: 136 MB % 47.08/7.26 % (4069661)Instructions burned: 276 (million) % 47.08/7.26 % (4069668)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1548465899:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi) % 47.08/7.26 % (4069657)Instruction limit reached! % 47.08/7.26 % (4069657)------------------------------ % 47.08/7.26 % (4069657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.08/7.26 % (4069657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.08/7.26 % (4069657)CaDiCaL version: 2.1.3 % 47.08/7.26 % (4069657)Termination reason: Instruction limit % 47.08/7.26 % (4069657)Termination phase: Saturation % 47.08/7.26 % (4069657)Time elapsed: 0.321 s % 47.08/7.26 % (4069657)Peak memory usage: 92 MB % 47.08/7.26 % (4069657)Instructions burned: 273 (million) % 47.08/7.26 % (4069667)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=978049177:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi) % 47.08/7.26 % (4069669)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3701390180:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi) % 47.08/7.26 % (4069669)Refutation not found, incomplete strategy % 47.08/7.26 % (4069669)------------------------------ % 47.08/7.26 % (4069669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.08/7.26 % (4069669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.08/7.26 % (4069669)CaDiCaL version: 2.1.3 % 47.08/7.26 % (4069669)Termination reason: Refutation not found, incomplete strategy % 47.08/7.26 % (4069669)Time elapsed: 0.032 s % 47.08/7.26 % (4069669)Peak memory usage: 116 MB % 47.08/7.26 % (4069669)Instructions burned: 12 (million) % 47.08/7.26 % (4069673)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 % 47.08/7.26 % (4069672)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=641470088:s2a=on:i=450:doe=on:nm=32:rtra=on_2953 on theBenchmark for (2953ds/450Mi) % 47.08/7.26 % (4069673)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3089567214:i=1090:aac=none:nm=0:rtra=on:rawr=on_2953 on theBenchmark for (2953ds/1090Mi) % 47.08/7.26 % (4069669)------------------------------ % 47.08/7.26 % (4069669)------------------------------ % 47.08/7.26 % (4069683)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1108139800:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2949 on theBenchmark for (2949ds/130Mi) % 47.08/7.26 % (4069667)Instruction limit reached! % 47.08/7.26 % (4069667)------------------------------ % 47.08/7.26 % (4069667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.08/7.26 % (4069667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069667)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069667)Termination reason: Instruction limit % 50.22/7.87 % (4069667)Termination phase: Saturation % 50.22/7.87 % (4069667)Time elapsed: 0.685 s % 50.22/7.87 % (4069667)Peak memory usage: 95 MB % 50.22/7.87 % (4069667)Instructions burned: 655 (million) % 50.22/7.87 % (4069683)Instruction limit reached! % 50.22/7.87 % (4069683)------------------------------ % 50.22/7.87 % (4069683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.22/7.87 % (4069683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069683)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069683)Termination reason: Instruction limit % 50.22/7.87 % (4069683)Termination phase: Saturation % 50.22/7.87 % (4069683)Time elapsed: 0.171 s % 50.22/7.87 % (4069683)Peak memory usage: 117 MB % 50.22/7.87 % (4069683)Instructions burned: 130 (million) % 50.22/7.87 % (4069672)Instruction limit reached! % 50.22/7.87 % (4069672)------------------------------ % 50.22/7.87 % (4069672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.22/7.87 % (4069672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069672)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069672)Termination reason: Instruction limit % 50.22/7.87 % (4069672)Termination phase: Saturation % 50.22/7.87 % (4069672)Time elapsed: 0.554 s % 50.22/7.87 % (4069672)Peak memory usage: 135 MB % 50.22/7.87 % (4069672)Instructions burned: 450 (million) % 50.22/7.87 % (4069662)Instruction limit reached! % 50.22/7.87 % (4069662)------------------------------ % 50.22/7.87 % (4069662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.22/7.87 % (4069662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069662)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069662)Termination reason: Instruction limit % 50.22/7.87 % (4069662)Termination phase: Saturation % 50.22/7.87 % (4069662)Time elapsed: 1.062 s % 50.22/7.87 % (4069662)Peak memory usage: 94 MB % 50.22/7.87 % (4069662)Instructions burned: 1052 (million) % 50.22/7.87 % (4069692)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1714942633:i=312:kws=inv_frequency:nm=20:rtra=on_2946 on theBenchmark for (2946ds/312Mi) % 50.22/7.87 % (4069668)Instruction limit reached! % 50.22/7.87 % (4069668)------------------------------ % 50.22/7.87 % (4069668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.22/7.87 % (4069668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069668)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069668)Termination reason: Instruction limit % 50.22/7.87 % (4069668)Termination phase: Saturation % 50.22/7.87 % (4069668)Time elapsed: 1.018 s % 50.22/7.87 % (4069668)Peak memory usage: 92 MB % 50.22/7.87 % (4069668)Instructions burned: 1054 (million) % 50.22/7.87 % (4069693)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=4037779998:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 50.22/7.87 % (4069694)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2636994263:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 50.22/7.87 % (4069695)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=35464342:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2944 on theBenchmark for (2944ds/307Mi) % 50.22/7.87 % (4069699)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1686127128:i=776:doe=on:rtra=on_2943 on theBenchmark for (2943ds/776Mi) % 50.22/7.87 % (4069692)Instruction limit reached! % 50.22/7.87 % (4069692)------------------------------ % 50.22/7.87 % (4069692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.22/7.87 % (4069692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069692)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069692)Termination reason: Instruction limit % 50.22/7.87 % (4069692)Termination phase: Saturation % 50.22/7.87 % (4069692)Time elapsed: 0.352 s % 50.22/7.87 % (4069692)Peak memory usage: 118 MB % 50.22/7.87 % (4069692)Instructions burned: 312 (million) % 50.22/7.87 % (4069673)Instruction limit reached! % 50.22/7.87 % (4069673)------------------------------ % 50.22/7.87 % (4069673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.22/7.87 % (4069673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.22/7.87 % (4069673)CaDiCaL version: 2.1.3 % 50.22/7.87 % (4069673)Termination reason: Instruction limit % 61.53/9.28 % (4069673)Termination phase: Saturation % 61.53/9.28 % (4069673)Time elapsed: 1.124 s % 61.53/9.28 % (4069673)Peak memory usage: 124 MB % 61.53/9.28 % (4069673)Instructions burned: 1092 (million) % 61.53/9.28 % (4069695)Instruction limit reached! % 61.53/9.28 % (4069695)------------------------------ % 61.53/9.28 % (4069695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.53/9.28 % (4069695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.53/9.28 % (4069695)CaDiCaL version: 2.1.3 % 61.53/9.28 % (4069695)Termination reason: Instruction limit % 61.53/9.28 % (4069695)Termination phase: Saturation % 61.53/9.28 % (4069695)Time elapsed: 0.324 s % 61.53/9.28 % (4069695)Peak memory usage: 91 MB % 61.53/9.28 % (4069695)Instructions burned: 307 (million) % 61.53/9.28 % (4069693)Instruction limit reached! % 61.53/9.28 % (4069693)------------------------------ % 61.53/9.28 % (4069693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.53/9.28 % (4069693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.53/9.28 % (4069693)CaDiCaL version: 2.1.3 % 61.53/9.28 % (4069693)Termination reason: Instruction limit % 61.53/9.29 % (4069693)Termination phase: Saturation % 61.53/9.29 % (4069693)Time elapsed: 0.499 s % 61.53/9.29 % (4069693)Peak memory usage: 94 MB % 61.53/9.29 % (4069693)Instructions burned: 492 (million) % 61.53/9.29 % (4069704)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4190374905:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 61.53/9.29 % (4069705)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=1825829805:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2939 on theBenchmark for (2939ds/784Mi) % 61.53/9.29 % (4069706)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=1148760136:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi) % 61.53/9.29 % (4069707)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=583304730:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi) % 61.53/9.29 % (4069660)Instruction limit reached! % 61.53/9.29 % (4069660)------------------------------ % 61.53/9.29 % (4069660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.53/9.29 % (4069660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.53/9.29 % (4069660)CaDiCaL version: 2.1.3 % 61.53/9.29 % (4069660)Termination reason: Instruction limit % 61.53/9.29 % (4069660)Termination phase: Saturation % 61.53/9.29 % (4069660)Time elapsed: 2.258 s % 61.53/9.29 % (4069660)Peak memory usage: 111 MB % 61.53/9.29 % (4069660)Instructions burned: 4428 (million) % 61.53/9.29 % (4069694)Instruction limit reached! % 61.53/9.29 % (4069694)------------------------------ % 61.53/9.29 % (4069694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.53/9.29 % (4069694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.53/9.29 % (4069694)CaDiCaL version: 2.1.3 % 61.53/9.29 % (4069694)Termination reason: Instruction limit % 61.53/9.29 % (4069694)Termination phase: Saturation % 61.53/9.29 % (4069694)Time elapsed: 0.865 s % 61.53/9.29 % (4069694)Peak memory usage: 95 MB % 61.53/9.29 % (4069694)Instructions burned: 836 (million) % 61.53/9.29 % (4069699)Instruction limit reached! % 61.53/9.29 % (4069699)------------------------------ % 61.53/9.29 % (4069699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.53/9.29 % (4069699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.53/9.29 % (4069699)CaDiCaL version: 2.1.3 % 61.53/9.29 % (4069699)Termination reason: Instruction limit % 61.53/9.29 % (4069699)Termination phase: Saturation % 61.53/9.29 % (4069699)Time elapsed: 0.706 s % 61.53/9.29 % (4069699)Peak memory usage: 119 MB % 61.53/9.29 % (4069699)Instructions burned: 777 (million) % 61.53/9.29 % (4069714)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2106235767:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/775Mi) % 61.53/9.29 % (4069707)Instruction limit reached! % 61.53/9.29 % (4069707)------------------------------ % 61.53/9.29 % (4069707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.53/9.29 % (4069707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.46/12.20 % (4069707)CaDiCaL version: 2.1.3 % 82.46/12.20 % (4069707)Termination reason: Instruction limit % 82.46/12.20 % (4069707)Termination phase: Saturation % 82.46/12.20 % (4069707)Time elapsed: 0.295 s % 82.46/12.20 % (4069707)Peak memory usage: 119 MB % 82.46/12.20 % (4069707)Instructions burned: 246 (million) % 82.46/12.20 % (4069715)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2348335770:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2933 on theBenchmark for (2933ds/273Mi) % 82.46/12.20 % (4069716)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4190310354:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi) % 82.46/12.20 % (4069704)Instruction limit reached! % 82.46/12.20 % (4069704)------------------------------ % 82.46/12.20 % (4069704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.46/12.20 % (4069704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.46/12.20 % (4069704)CaDiCaL version: 2.1.3 % 82.46/12.20 % (4069704)Termination reason: Instruction limit % 82.46/12.20 % (4069704)Termination phase: Saturation % 82.46/12.20 % (4069704)Time elapsed: 0.714 s % 82.46/12.20 % (4069704)Peak memory usage: 138 MB % 82.46/12.20 % (4069704)Instructions burned: 646 (million) % 82.46/12.20 % (4069716)Instruction limit reached! % 82.46/12.20 % (4069716)------------------------------ % 82.46/12.20 % (4069716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.46/12.20 % (4069716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.46/12.20 % (4069716)CaDiCaL version: 2.1.3 % 82.46/12.20 % (4069716)Termination reason: Instruction limit % 82.46/12.20 % (4069716)Termination phase: Saturation % 82.46/12.20 % (4069716)Time elapsed: 0.115 s % 82.46/12.20 % (4069716)Peak memory usage: 89 MB % 82.46/12.20 % (4069716)Instructions burned: 102 (million) % 82.46/12.20 % (4069718)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1623382882:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 82.46/12.20 % (4069714)Instruction limit reached! % 82.46/12.20 % (4069714)------------------------------ % 82.46/12.20 % (4069714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.46/12.20 % (4069714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.46/12.20 % (4069714)CaDiCaL version: 2.1.3 % 82.46/12.20 % (4069714)Termination reason: Instruction limit % 82.46/12.20 % (4069714)Termination phase: Saturation % 82.46/12.20 % (4069714)Time elapsed: 0.415 s % 82.46/12.20 % (4069714)Peak memory usage: 94 MB % 82.46/12.20 % (4069714)Instructions burned: 775 (million) % 82.46/12.20 % (4069715)Instruction limit reached! % 82.46/12.20 % (4069715)------------------------------ % 82.46/12.20 % (4069715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.46/12.20 % (4069715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.46/12.20 % (4069715)CaDiCaL version: 2.1.3 % 82.46/12.20 % (4069715)Termination reason: Instruction limit % 82.46/12.20 % (4069715)Termination phase: Saturation % 82.46/12.20 % (4069715)Time elapsed: 0.320 s % 82.46/12.20 % (4069715)Peak memory usage: 92 MB % 82.46/12.20 % (4069715)Instructions burned: 273 (million) % 82.46/12.20 % (4069705)Instruction limit reached! % 82.46/12.20 % (4069705)------------------------------ % 82.46/12.20 % (4069705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.46/12.20 % (4069705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.46/12.20 % (4069705)CaDiCaL version: 2.1.3 % 82.46/12.20 % (4069705)Termination reason: Instruction limit % 82.46/12.20 % (4069705)Termination phase: Saturation % 82.46/12.20 % (4069705)Time elapsed: 0.915 s % 82.46/12.20 % (4069705)Peak memory usage: 123 MB % 82.46/12.20 % (4069705)Instructions burned: 784 (million) % 82.46/12.20 % (4069721)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4100397117:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 82.46/12.20 % (4069722)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=2141038039:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi) % 82.46/12.20 % (4069724)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=3496554264:i=1846:canc=cautious:fsr=off:rtra=on_2927 on theBenchmark for (2927ds/1846Mi) % 100.84/14.81 % (4069727)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3156551415:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2927 on theBenchmark for (2927ds/273Mi) % 100.84/14.81 % (4069725)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3427454736:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2927 on theBenchmark for (2927ds/36816Mi) % 100.84/14.81 % (4069706)Instruction limit reached! % 100.84/14.81 % (4069706)------------------------------ % 100.84/14.81 % (4069706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.84/14.81 % (4069706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.84/14.81 % (4069706)CaDiCaL version: 2.1.3 % 100.84/14.81 % (4069706)Termination reason: Instruction limit % 100.84/14.81 % (4069706)Termination phase: Saturation % 100.84/14.81 % (4069706)Time elapsed: 1.196 s % 100.84/14.81 % (4069706)Peak memory usage: 122 MB % 100.84/14.81 % (4069706)Instructions burned: 1131 (million) % 100.84/14.81 % (4069727)Instruction limit reached! % 100.84/14.81 % (4069727)------------------------------ % 100.84/14.81 % (4069727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.84/14.81 % (4069727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.84/14.81 % (4069727)CaDiCaL version: 2.1.3 % 100.84/14.81 % (4069727)Termination reason: Instruction limit % 100.84/14.81 % (4069727)Termination phase: Saturation % 100.84/14.81 % (4069727)Time elapsed: 0.358 s % 100.84/14.81 % (4069727)Peak memory usage: 92 MB % 100.84/14.81 % (4069727)Instructions burned: 274 (million) % 100.84/14.81 % (4069734)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=3761414080:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2923 on theBenchmark for (2923ds/863Mi) % 100.84/14.81 % (4069724)Instruction limit reached! % 100.84/14.81 % (4069724)------------------------------ % 100.84/14.81 % (4069724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.84/14.81 % (4069724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.84/14.81 % (4069724)CaDiCaL version: 2.1.3 % 100.84/14.81 % (4069724)Termination reason: Instruction limit % 100.84/14.81 % (4069724)Termination phase: Saturation % 100.84/14.81 % (4069724)Time elapsed: 0.645 s % 100.84/14.81 % (4069724)Peak memory usage: 95 MB % 100.84/14.81 % (4069724)Instructions burned: 1848 (million) % 100.84/14.81 % (4069735)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3639505129:i=5811:kws=precedence:nm=0:rtra=on_2921 on theBenchmark for (2921ds/5811Mi) % 100.84/14.81 % (4069718)Instruction limit reached! % 100.84/14.81 % (4069718)------------------------------ % 100.84/14.81 % (4069718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.84/14.81 % (4069718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.84/14.81 % (4069718)CaDiCaL version: 2.1.3 % 100.84/14.81 % (4069718)Termination reason: Instruction limit % 100.84/14.81 % (4069718)Termination phase: Saturation % 100.84/14.81 % (4069718)Time elapsed: 1.136 s % 100.84/14.81 % (4069718)Peak memory usage: 97 MB % 100.84/14.81 % (4069718)Instructions burned: 1094 (million) % 100.84/14.81 % (4069737)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=3140137130:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2919 on theBenchmark for (2919ds/2216Mi) % 100.84/14.81 % (4069722)Instruction limit reached! % 100.84/14.81 % (4069722)------------------------------ % 100.84/14.81 % (4069722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.84/14.81 % (4069722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.84/14.81 % (4069722)CaDiCaL version: 2.1.3 % 100.84/14.81 % (4069722)Termination reason: Instruction limit % 100.84/14.81 % (4069722)Termination phase: Saturation % 100.84/14.81 % (4069722)Time elapsed: 0.933 s % 100.84/14.81 % (4069722)Peak memory usage: 121 MB % 100.84/14.81 % (4069722)Instructions burned: 868 (million) % 100.84/14.81 % (4069739)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4075783037:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2917 on theBenchmark for (2917ds/801Mi) % 100.84/14.81 % (4069741)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=152702023:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2917 on theBenchmark for (2917ds/1026Mi) % 100.84/14.81 % (4069734)Instruction limit reached! % 100.84/14.81 % (4069734)------------------------------ % 149.76/21.61 % (4069734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.76/21.61 % (4069734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.61 % (4069734)CaDiCaL version: 2.1.3 % 149.76/21.61 % (4069734)Termination reason: Instruction limit % 149.76/21.61 % (4069734)Termination phase: Saturation % 149.76/21.61 % (4069734)Time elapsed: 0.908 s % 149.76/21.61 % (4069734)Peak memory usage: 121 MB % 149.76/21.61 % (4069734)Instructions burned: 864 (million) % 149.76/21.61 % (4069744)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=530158316:i=3509:rtra=on_2911 on theBenchmark for (2911ds/3509Mi) % 149.76/21.61 % (4069737)Instruction limit reached! % 149.76/21.61 % (4069737)------------------------------ % 149.76/21.61 % (4069737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.76/21.61 % (4069737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.61 % (4069737)CaDiCaL version: 2.1.3 % 149.76/21.61 % (4069737)Termination reason: Instruction limit % 149.76/21.61 % (4069737)Termination phase: Saturation % 149.76/21.61 % (4069737)Time elapsed: 1.079 s % 149.76/21.61 % (4069737)Peak memory usage: 121 MB % 149.76/21.61 % (4069737)Instructions burned: 2216 (million) % 149.76/21.61 % (4069739)Instruction limit reached! % 149.76/21.61 % (4069739)------------------------------ % 149.76/21.61 % (4069739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.76/21.61 % (4069739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.61 % (4069739)CaDiCaL version: 2.1.3 % 149.76/21.61 % (4069739)Termination reason: Instruction limit % 149.76/21.61 % (4069739)Termination phase: Saturation % 149.76/21.61 % (4069739)Time elapsed: 0.853 s % 149.76/21.61 % (4069739)Peak memory usage: 95 MB % 149.76/21.61 % (4069739)Instructions burned: 801 (million) % 149.76/21.61 % (4069746)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2432120405:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2906 on theBenchmark for (2906ds/2127Mi) % 149.76/21.61 % (4069741)Instruction limit reached! % 149.76/21.61 % (4069741)------------------------------ % 149.76/21.61 % (4069741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.76/21.61 % (4069741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.61 % (4069741)CaDiCaL version: 2.1.3 % 149.76/21.61 % (4069741)Termination reason: Instruction limit % 149.76/21.61 % (4069741)Termination phase: Saturation % 149.76/21.61 % (4069741)Time elapsed: 1.015 s % 149.76/21.61 % (4069741)Peak memory usage: 92 MB % 149.76/21.61 % (4069741)Instructions burned: 1026 (million) % 149.76/21.61 % (4069747)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4205978581:i=1959:rtra=on:fsd=on:proc=on_2906 on theBenchmark for (2906ds/1959Mi) % 149.76/21.61 % (4069749)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2722381606:s2a=on:i=3553:nm=0:rtra=on_2903 on theBenchmark for (2903ds/3553Mi) % 149.76/21.61 % (4069746)Instruction limit reached! % 149.76/21.61 % (4069746)------------------------------ % 149.76/21.61 % (4069746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.76/21.61 % (4069746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.61 % (4069746)CaDiCaL version: 2.1.3 % 149.76/21.61 % (4069746)Termination reason: Instruction limit % 149.76/21.61 % (4069746)Termination phase: Saturation % 149.76/21.61 % (4069746)Time elapsed: 0.947 s % 149.76/21.61 % (4069746)Peak memory usage: 92 MB % 149.76/21.61 % (4069746)Instructions burned: 2129 (million) % 149.76/21.61 % (4069752)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=292323551:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/3201Mi) % 149.76/21.61 % (4069747)Instruction limit reached! % 149.76/21.61 % (4069747)------------------------------ % 149.76/21.61 % (4069747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.76/21.61 % (4069747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.61 % (4069747)CaDiCaL version: 2.1.3 % 149.76/21.61 % (4069747)Termination reason: Instruction limit % 149.76/21.61 % (4069747)Termination phase: Saturation % 149.76/21.61 % (4069747)Time elapsed: 1.752 s % 149.76/21.61 % (4069747)Peak memory usage: 120 MB % 149.76/21.61 % (4069747)Instructions burned: 1959 (million) % 149.76/21.61 % (4069754)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=2662110780:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2885 on theBenchmark for (2885ds/4093Mi) % 185.12/26.65 % (4069744)Instruction limit reached! % 185.12/26.65 % (4069744)------------------------------ % 185.12/26.65 % (4069744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.12/26.65 % (4069744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.12/26.65 % (4069744)CaDiCaL version: 2.1.3 % 185.12/26.65 % (4069744)Termination reason: Instruction limit % 185.12/26.65 % (4069744)Termination phase: Saturation % 185.12/26.65 % (4069744)Time elapsed: 2.821 s % 185.12/26.65 % (4069744)Peak memory usage: 107 MB % 185.12/26.65 % (4069744)Instructions burned: 3510 (million) % 185.12/26.65 % (4069756)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=773640522:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2880 on theBenchmark for (2880ds/21173Mi) % 185.12/26.65 % (4069752)Instruction limit reached! % 185.12/26.65 % (4069752)------------------------------ % 185.12/26.65 % (4069752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.12/26.65 % (4069752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.12/26.65 % (4069752)CaDiCaL version: 2.1.3 % 185.12/26.65 % (4069752)Termination reason: Instruction limit % 185.12/26.65 % (4069752)Termination phase: Saturation % 185.12/26.65 % (4069752)Time elapsed: 1.438 s % 185.12/26.65 % (4069752)Peak memory usage: 93 MB % 185.12/26.65 % (4069752)Instructions burned: 3202 (million) % 185.12/26.65 % (4069758)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4216236132:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2877 on theBenchmark for (2877ds/10544Mi) % 185.12/26.65 % (4069721)Instruction limit reached! % 185.12/26.65 % (4069721)------------------------------ % 185.12/26.65 % (4069721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.12/26.65 % (4069721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.12/26.65 % (4069721)CaDiCaL version: 2.1.3 % 185.12/26.65 % (4069721)Termination reason: Instruction limit % 185.12/26.65 % (4069721)Termination phase: Saturation % 185.12/26.65 % (4069721)Time elapsed: 5.979 s % 185.12/26.65 % (4069721)Peak memory usage: 121 MB % 185.12/26.65 % (4069721)Instructions burned: 6401 (million) % 185.12/26.65 % (4069749)Instruction limit reached! % 185.12/26.65 % (4069749)------------------------------ % 185.12/26.65 % (4069749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.12/26.65 % (4069749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.12/26.65 % (4069749)CaDiCaL version: 2.1.3 % 185.12/26.65 % (4069749)Termination reason: Instruction limit % 185.12/26.65 % (4069749)Termination phase: Saturation % 185.12/26.65 % (4069749)Time elapsed: 3.422 s % 185.12/26.65 % (4069749)Peak memory usage: 106 MB % 185.12/26.65 % (4069749)Instructions burned: 3553 (million) % 185.12/26.65 % (4069760)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1104979464:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2867 on theBenchmark for (2867ds/1262Mi) % 185.12/26.65 % (4069761)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2171501914:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2866 on theBenchmark for (2866ds/775Mi) % 185.12/26.65 % (4069735)Instruction limit reached! % 185.12/26.65 % (4069735)------------------------------ % 185.12/26.65 % (4069735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.12/26.65 % (4069735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.12/26.65 % (4069735)CaDiCaL version: 2.1.3 % 185.12/26.65 % (4069735)Termination reason: Instruction limit % 185.12/26.65 % (4069735)Termination phase: Saturation % 185.12/26.65 % (4069735)Time elapsed: 5.724 s % 185.12/26.65 % (4069735)Peak memory usage: 133 MB % 185.12/26.65 % (4069735)Instructions burned: 5811 (million) % 185.12/26.65 % (4069768)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=890638125:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2861 on theBenchmark for (2861ds/270Mi) % 185.12/26.65 % (4069761)Instruction limit reached! % 185.12/26.65 % (4069761)------------------------------ % 185.12/26.65 % (4069761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.12/26.65 % (4069761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.12/26.65 % (4069761)CaDiCaL version: 2.1.3 % 185.12/26.65 % (4069761)Termination reason: Instruction limit % 217.87/31.26 % (4069761)Termination phase: Saturation % 217.87/31.26 % (4069761)Time elapsed: 0.748 s % 217.87/31.26 % (4069761)Peak memory usage: 94 MB % 217.87/31.26 % (4069761)Instructions burned: 776 (million) % 217.87/31.26 % (4069768)Instruction limit reached! % 217.87/31.26 % (4069768)------------------------------ % 217.87/31.26 % (4069768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.87/31.26 % (4069768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.87/31.26 % (4069768)CaDiCaL version: 2.1.3 % 217.87/31.26 % (4069768)Termination reason: Instruction limit % 217.87/31.26 % (4069768)Termination phase: Saturation % 217.87/31.26 % (4069768)Time elapsed: 0.318 s % 217.87/31.26 % (4069768)Peak memory usage: 93 MB % 217.87/31.26 % (4069768)Instructions burned: 271 (million) % 217.87/31.26 % (4069770)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2818661108:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2856 on theBenchmark for (2856ds/17165Mi) % 217.87/31.26 % (4069760)Instruction limit reached! % 217.87/31.26 % (4069760)------------------------------ % 217.87/31.26 % (4069760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.87/31.26 % (4069760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.87/31.26 % (4069760)CaDiCaL version: 2.1.3 % 217.87/31.26 % (4069760)Termination reason: Instruction limit % 217.87/31.26 % (4069760)Termination phase: Saturation % 217.87/31.26 % (4069760)Time elapsed: 1.148 s % 217.87/31.26 % (4069760)Peak memory usage: 120 MB % 217.87/31.26 % (4069760)Instructions burned: 1262 (million) % 217.87/31.26 % (4069771)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3700245057:s2a=on:i=13094:s2at=-1:rtra=on_2855 on theBenchmark for (2855ds/13094Mi) % 217.87/31.26 % (4069775)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3401769496:st=2:i=12633:rtra=on:ss=axioms_2853 on theBenchmark for (2853ds/12633Mi) % 217.87/31.26 % (4069754)Instruction limit reached! % 217.87/31.26 % (4069754)------------------------------ % 217.87/31.26 % (4069754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.87/31.26 % (4069754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.87/31.26 % (4069754)CaDiCaL version: 2.1.3 % 217.87/31.26 % (4069754)Termination reason: Instruction limit % 217.87/31.26 % (4069754)Termination phase: Saturation % 217.87/31.26 % (4069754)Time elapsed: 3.632 s % 217.87/31.26 % (4069754)Peak memory usage: 141 MB % 217.87/31.26 % (4069754)Instructions burned: 4093 (million) % 217.87/31.26 % (4069778)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1238523809:i=1783:rtra=on:gtg=position_2846 on theBenchmark for (2846ds/1783Mi) % 217.87/31.26 % (4069778)Instruction limit reached! % 217.87/31.26 % (4069778)------------------------------ % 217.87/31.26 % (4069778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.87/31.26 % (4069778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.87/31.26 % (4069778)CaDiCaL version: 2.1.3 % 217.87/31.26 % (4069778)Termination reason: Instruction limit % 217.87/31.26 % (4069778)Termination phase: Saturation % 217.87/31.26 % (4069778)Time elapsed: 1.784 s % 217.87/31.26 % (4069778)Peak memory usage: 123 MB % 217.87/31.26 % (4069778)Instructions burned: 1784 (million) % 217.87/31.26 % (4069780)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=2450524167:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2825 on theBenchmark for (2825ds/5451Mi) % 217.87/31.26 % (4069758)Instruction limit reached! % 217.87/31.26 % (4069758)------------------------------ % 217.87/31.26 % (4069758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.87/31.26 % (4069758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.87/31.26 % (4069758)CaDiCaL version: 2.1.3 % 217.87/31.26 % (4069758)Termination reason: Instruction limit % 217.87/31.26 % (4069758)Termination phase: Saturation % 217.87/31.26 % (4069758)Time elapsed: 6.087 s % 217.87/31.26 % (4069758)Peak memory usage: 193 MB % 217.87/31.26 % (4069758)Instructions burned: 10545 (million) % 217.87/31.26 % (4069782)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=3761644708:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2814 on theBenchmark for (2814ds/4975Mi) % 217.87/31.26 % (4069782)Instruction limit reached! % 217.87/31.26 % (4069782)------------------------------ % 217.87/31.26 % (4069782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.47/40.49 % (4069782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.47/40.49 % (4069782)CaDiCaL version: 2.1.3 % 283.47/40.49 % (4069782)Termination reason: Instruction limit % 283.47/40.49 % (4069782)Termination phase: Saturation % 283.47/40.49 % (4069782)Time elapsed: 2.320 s % 283.47/40.49 % (4069782)Peak memory usage: 122 MB % 283.47/40.49 % (4069782)Instructions burned: 4976 (million) % 283.47/40.49 % (4069787)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=3538528748:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2788 on theBenchmark for (2788ds/2076Mi) % 283.47/40.49 % (4069780)Instruction limit reached! % 283.47/40.49 % (4069780)------------------------------ % 283.47/40.49 % (4069780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.47/40.49 % (4069780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.47/40.49 % (4069780)CaDiCaL version: 2.1.3 % 283.47/40.49 % (4069780)Termination reason: Instruction limit % 283.47/40.49 % (4069780)Termination phase: Saturation % 283.47/40.49 % (4069780)Time elapsed: 4.669 s % 283.47/40.49 % (4069780)Peak memory usage: 121 MB % 283.47/40.49 % (4069780)Instructions burned: 5452 (million) % 283.47/40.49 % (4069787)Instruction limit reached! % 283.47/40.49 % (4069787)------------------------------ % 283.47/40.49 % (4069787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.47/40.49 % (4069787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.47/40.49 % (4069787)CaDiCaL version: 2.1.3 % 283.47/40.49 % (4069787)Termination reason: Instruction limit % 283.47/40.49 % (4069787)Termination phase: Saturation % 283.47/40.49 % (4069787)Time elapsed: 1.032 s % 283.47/40.49 % (4069787)Peak memory usage: 122 MB % 283.47/40.49 % (4069787)Instructions burned: 2077 (million) % 283.47/40.49 % (4069792)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4082779553:i=3509:rtra=on_2775 on theBenchmark for (2775ds/3509Mi) % 283.47/40.49 % (4069791)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2721668835:i=5145:rtra=on_2775 on theBenchmark for (2775ds/5145Mi) % 283.47/40.49 % (4069792)Instruction limit reached! % 283.47/40.49 % (4069792)------------------------------ % 283.47/40.49 % (4069792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.47/40.49 % (4069792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.47/40.49 % (4069792)CaDiCaL version: 2.1.3 % 283.47/40.49 % (4069792)Termination reason: Instruction limit % 283.47/40.49 % (4069792)Termination phase: Saturation % 283.47/40.49 % (4069792)Time elapsed: 1.487 s % 283.47/40.49 % (4069792)Peak memory usage: 106 MB % 283.47/40.49 % (4069792)Instructions burned: 3514 (million) % 283.47/40.49 % (4069775)Instruction limit reached! % 283.47/40.49 % (4069775)------------------------------ % 283.47/40.49 % (4069775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.47/40.49 % (4069775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.47/40.49 % (4069775)CaDiCaL version: 2.1.3 % 283.47/40.49 % (4069775)Termination reason: Instruction limit % 283.47/40.49 % (4069775)Termination phase: Saturation % 283.47/40.49 % (4069775)Time elapsed: 9.370 s % 283.47/40.49 % (4069775)Peak memory usage: 144 MB % 283.47/40.49 % (4069775)Instructions burned: 12634 (million) % 283.47/40.49 % (4069795)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2301476799:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2758 on theBenchmark for (2758ds/13800Mi) % 283.47/40.49 % (4069796)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3449346916:i=1412:rtra=on:fsd=on:proc=on_2756 on theBenchmark for (2756ds/1412Mi) % 283.47/40.49 % (4069796)Instruction limit reached! % 283.47/40.49 % (4069796)------------------------------ % 283.47/40.49 % (4069796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.47/40.49 % (4069796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.47/40.49 % (4069796)CaDiCaL version: 2.1.3 % 283.47/40.49 % (4069796)Termination reason: Instruction limit % 283.47/40.49 % (4069796)Termination phase: Saturation % 283.47/40.49 % (4069796)Time elapsed: 1.286 s % 283.47/40.49 % (4069796)Peak memory usage: 120 MB % 283.47/40.49 % (4069796)Instructions burned: 1412 (million) % 283.47/40.49 % (4069801)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_Terminated %------------------------------------------------------------------------------