%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX143_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:58 PM UTC 2026 % Result : Timeout 292.16s 42.15s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWX143_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 15:04:19 UTC 2026 % 0.09/0.11 % CPUTime : % 0.09/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.13 Running first-order theorem proving % 0.09/0.13 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.82/1.17 % (3441547)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.82/1.17 % (3441620)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=4000045574:s2a=on:i=7:rtra=on:inst=on_2997 on theBenchmark for (2997ds/7Mi) % 3.82/1.17 % (3441622)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=928126006:i=46:rtra=on_2997 on theBenchmark for (2997ds/46Mi) % 3.82/1.17 % (3441623)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=623144497:i=33:rtra=on_2997 on theBenchmark for (2997ds/33Mi) % 3.82/1.17 % (3441621)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3016169700:i=4:rtra=on_2997 on theBenchmark for (2997ds/4Mi) % 3.82/1.17 % (3441618)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2060846425:i=307:kws=precedence:nm=0:rtra=on_2997 on theBenchmark for (2997ds/307Mi) % 3.82/1.17 % (3441617)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=15189133:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2997 on theBenchmark for (2997ds/12Mi) % 3.82/1.17 % (3441619)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1694646325:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/201Mi) % 3.82/1.17 % (3441620)Instruction limit reached! % 3.82/1.17 % (3441620)------------------------------ % 3.82/1.17 % (3441620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.17 % (3441620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.17 % (3441620)CaDiCaL version: 2.1.3 % 3.82/1.17 % (3441620)Termination reason: Instruction limit % 3.82/1.17 % (3441620)Termination phase: shuffling % 3.82/1.17 % (3441620)Time elapsed: 0.002 s % 3.82/1.17 % (3441620)Peak memory usage: 85 MB % 3.82/1.17 % (3441620)Instructions burned: 8 (million) % 3.82/1.17 % (3441621)Instruction limit reached! % 3.82/1.17 % (3441621)------------------------------ % 3.82/1.17 % (3441621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.17 % (3441621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.17 % (3441621)CaDiCaL version: 2.1.3 % 3.82/1.17 % (3441621)Termination reason: Instruction limit % 3.82/1.17 % (3441621)Termination phase: shuffling % 3.82/1.17 % (3441621)Time elapsed: 0.002 s % 3.82/1.17 % (3441621)Peak memory usage: 85 MB % 3.82/1.17 % (3441621)Instructions burned: 6 (million) % 3.82/1.17 % (3441617)Instruction limit reached! % 3.82/1.17 % (3441617)------------------------------ % 3.82/1.17 % (3441617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.17 % (3441617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.17 % (3441617)CaDiCaL version: 2.1.3 % 3.82/1.17 % (3441617)Termination reason: Instruction limit % 3.82/1.17 % (3441617)Termination phase: Property scanning % 3.82/1.17 % (3441617)Time elapsed: 0.005 s % 3.82/1.17 % (3441617)Peak memory usage: 85 MB % 3.82/1.17 % (3441617)Instructions burned: 12 (million) % 3.82/1.17 % (3441623)Instruction limit reached! % 3.82/1.17 % (3441623)------------------------------ % 3.82/1.17 % (3441623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.17 % (3441623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.17 % (3441623)CaDiCaL version: 2.1.3 % 3.82/1.17 % (3441623)Termination reason: Instruction limit % 3.82/1.17 % (3441623)Termination phase: Property scanning % 3.82/1.17 % (3441623)Time elapsed: 0.013 s % 3.82/1.17 % (3441623)Peak memory usage: 85 MB % 3.82/1.17 % (3441623)Instructions burned: 34 (million) % 3.82/1.17 % (3441622)Instruction limit reached! % 3.82/1.17 % (3441622)------------------------------ % 3.82/1.17 % (3441622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.17 % (3441622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.17 % (3441622)CaDiCaL version: 2.1.3 % 3.82/1.17 % (3441622)Termination reason: Instruction limit % 3.82/1.17 % (3441622)Termination phase: Property scanning % 3.82/1.17 % (3441622)Time elapsed: 0.018 s % 3.82/1.17 % (3441622)Peak memory usage: 85 MB % 3.82/1.17 % (3441622)Instructions burned: 47 (million) % 3.82/1.17 % (3441619)Instruction limit reached! % 3.82/1.17 % (3441619)------------------------------ % 3.82/1.17 % (3441619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.17 % (3441619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.53/1.36 % (3441619)CaDiCaL version: 2.1.3 % 4.53/1.36 % (3441619)Termination reason: Instruction limit % 4.53/1.36 % (3441619)Termination phase: Property scanning % 4.53/1.36 % (3441619)Time elapsed: 0.063 s % 4.53/1.36 % (3441619)Peak memory usage: 85 MB % 4.53/1.36 % (3441619)Instructions burned: 203 (million) % 4.53/1.36 % (3441618)Instruction limit reached! % 4.53/1.36 % (3441618)------------------------------ % 4.53/1.36 % (3441618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.53/1.36 % (3441618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.53/1.36 % (3441618)CaDiCaL version: 2.1.3 % 4.53/1.36 % (3441618)Termination reason: Instruction limit % 4.53/1.36 % (3441618)Termination phase: Saturation % 4.53/1.36 % (3441618)Time elapsed: 0.137 s % 4.53/1.36 % (3441618)Peak memory usage: 112 MB % 4.53/1.36 % (3441618)Instructions burned: 310 (million) % 4.53/1.36 % (3441639)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4175457626:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2995 on theBenchmark for (2995ds/14Mi) % 4.53/1.36 % (3441639)Instruction limit reached! % 4.53/1.36 % (3441639)------------------------------ % 4.53/1.36 % (3441639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.53/1.36 % (3441639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.53/1.36 % (3441639)CaDiCaL version: 2.1.3 % 4.53/1.36 % (3441639)Termination reason: Instruction limit % 4.53/1.36 % (3441639)Termination phase: shuffling % 4.53/1.36 % (3441639)Time elapsed: 0.005 s % 4.53/1.36 % (3441639)Peak memory usage: 85 MB % 4.53/1.36 % (3441639)Instructions burned: 15 (million) % 4.53/1.36 % (3441641)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=688942765:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/16Mi) % 4.53/1.36 % (3441640)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=2313540325:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2995 on theBenchmark for (2995ds/29Mi) % 4.53/1.36 % (3441642)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=337320139:i=24:canc=force:rtra=on_2995 on theBenchmark for (2995ds/24Mi) % 4.53/1.36 % (3441643)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=538943393:i=27:canc=cautious:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/27Mi) % 4.53/1.36 % (3441641)Instruction limit reached! % 4.53/1.36 % (3441641)------------------------------ % 4.53/1.36 % (3441641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.53/1.36 % (3441641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.53/1.36 % (3441641)CaDiCaL version: 2.1.3 % 4.53/1.36 % (3441641)Termination reason: Instruction limit % 4.53/1.36 % (3441641)Termination phase: shuffling % 4.53/1.36 % (3441641)Time elapsed: 0.004 s % 4.53/1.36 % (3441641)Peak memory usage: 85 MB % 4.53/1.36 % (3441641)Instructions burned: 18 (million) % 4.53/1.36 % (3441642)Instruction limit reached! % 4.53/1.36 % (3441642)------------------------------ % 4.53/1.36 % (3441642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.53/1.36 % (3441642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.53/1.36 % (3441642)CaDiCaL version: 2.1.3 % 4.53/1.36 % (3441642)Termination reason: Instruction limit % 4.53/1.36 % (3441642)Termination phase: Property scanning % 4.53/1.36 % (3441642)Time elapsed: 0.009 s % 4.53/1.36 % (3441642)Peak memory usage: 85 MB % 4.53/1.36 % (3441642)Instructions burned: 24 (million) % 4.53/1.36 % (3441643)Instruction limit reached! % 4.53/1.36 % (3441643)------------------------------ % 4.53/1.36 % (3441643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.53/1.36 % (3441643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.53/1.36 % (3441643)CaDiCaL version: 2.1.3 % 4.53/1.36 % (3441643)Termination reason: Instruction limit % 4.53/1.36 % (3441643)Termination phase: Property scanning % 4.53/1.36 % (3441643)Time elapsed: 0.011 s % 4.53/1.36 % (3441643)Peak memory usage: 85 MB % 4.53/1.36 % (3441643)Instructions burned: 29 (million) % 4.53/1.36 % (3441640)Instruction limit reached! % 4.53/1.36 % (3441640)------------------------------ % 4.53/1.36 % (3441640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.53/1.36 % (3441640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.55 % (3441640)CaDiCaL version: 2.1.3 % 5.71/1.55 % (3441640)Termination reason: Instruction limit % 5.71/1.55 % (3441640)Termination phase: Property scanning % 5.71/1.55 % (3441640)Time elapsed: 0.012 s % 5.71/1.55 % (3441640)Peak memory usage: 85 MB % 5.71/1.55 % (3441640)Instructions burned: 30 (million) % 5.71/1.55 % (3441646)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1013269737:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 5.71/1.55 % (3441646)Instruction limit reached! % 5.71/1.55 % (3441646)------------------------------ % 5.71/1.55 % (3441646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.55 % (3441646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.55 % (3441646)CaDiCaL version: 2.1.3 % 5.71/1.55 % (3441646)Termination reason: Instruction limit % 5.71/1.55 % (3441646)Termination phase: Property scanning % 5.71/1.55 % (3441646)Time elapsed: 0.035 s % 5.71/1.55 % (3441646)Peak memory usage: 85 MB % 5.71/1.55 % (3441646)Instructions burned: 87 (million) % 5.71/1.55 % (3441649)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3425646310:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 5.71/1.55 % (3441649)Instruction limit reached! % 5.71/1.55 % (3441649)------------------------------ % 5.71/1.55 % (3441649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.55 % (3441649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.55 % (3441649)CaDiCaL version: 2.1.3 % 5.71/1.55 % (3441649)Termination reason: Instruction limit % 5.71/1.55 % (3441649)Termination phase: shuffling % 5.71/1.55 % (3441649)Time elapsed: 0.006 s % 5.71/1.55 % (3441649)Peak memory usage: 85 MB % 5.71/1.55 % (3441649)Instructions burned: 18 (million) % 5.71/1.55 % (3441652)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=721968424:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 5.71/1.55 % (3441658)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4294676340:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi) % 5.71/1.55 % (3441658)Instruction limit reached! % 5.71/1.55 % (3441658)------------------------------ % 5.71/1.55 % (3441658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.55 % (3441658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.55 % (3441658)CaDiCaL version: 2.1.3 % 5.71/1.55 % (3441658)Termination reason: Instruction limit % 5.71/1.55 % (3441658)Termination phase: shuffling % 5.71/1.55 % (3441658)Time elapsed: 0.002 s % 5.71/1.55 % (3441658)Peak memory usage: 85 MB % 5.71/1.55 % (3441658)Instructions burned: 5 (million) % 5.71/1.55 % (3441660)lrs+10_1_thi=all:si=on:fd=off:random_seed=3031953258:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 5.71/1.55 % (3441661)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=2994451133:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 5.71/1.55 % (3441659)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2376555777:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 5.71/1.55 % (3441661)Instruction limit reached! % 5.71/1.55 % (3441661)------------------------------ % 5.71/1.55 % (3441661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.55 % (3441661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.55 % (3441661)CaDiCaL version: 2.1.3 % 5.71/1.55 % (3441661)Termination reason: Instruction limit % 5.71/1.55 % (3441661)Termination phase: Property scanning % 5.71/1.55 % (3441661)Time elapsed: 0.004 s % 5.71/1.55 % (3441661)Peak memory usage: 85 MB % 5.71/1.55 % (3441661)Instructions burned: 9 (million) % 5.71/1.55 % (3441652)Refutation not found, incomplete strategy % 5.71/1.55 % (3441652)------------------------------ % 5.71/1.55 % (3441652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.55 % (3441652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.55 % (3441652)CaDiCaL version: 2.1.3 % 5.71/1.55 % (3441652)Termination reason: Refutation not found, incomplete strategy % 5.71/1.55 % (3441652)Time elapsed: 0.050 s % 5.71/1.55 % (3441652)Peak memory usage: 88 MB % 5.71/1.55 % (3441652)Instructions burned: 174 (million) % 7.11/1.73 % (3441660)Instruction limit reached! % 7.11/1.73 % (3441660)------------------------------ % 7.11/1.73 % (3441660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.73 % (3441660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.73 % (3441660)CaDiCaL version: 2.1.3 % 7.11/1.73 % (3441660)Termination reason: Instruction limit % 7.11/1.73 % (3441660)Termination phase: Property scanning % 7.11/1.73 % (3441660)Time elapsed: 0.021 s % 7.11/1.73 % (3441660)Peak memory usage: 85 MB % 7.11/1.73 % (3441660)Instructions burned: 53 (million) % 7.11/1.73 % (3441659)Instruction limit reached! % 7.11/1.73 % (3441659)------------------------------ % 7.11/1.73 % (3441659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.73 % (3441659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.73 % (3441659)CaDiCaL version: 2.1.3 % 7.11/1.73 % (3441659)Termination reason: Instruction limit % 7.11/1.73 % (3441659)Termination phase: Property scanning % 7.11/1.73 % (3441659)Time elapsed: 0.026 s % 7.11/1.73 % (3441659)Peak memory usage: 85 MB % 7.11/1.73 % (3441659)Instructions burned: 66 (million) % 7.11/1.73 % (3441665)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1756796614:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 7.11/1.73 % (3441665)Instruction limit reached! % 7.11/1.73 % (3441665)------------------------------ % 7.11/1.73 % (3441665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.73 % (3441665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.73 % (3441665)CaDiCaL version: 2.1.3 % 7.11/1.73 % (3441665)Termination reason: Instruction limit % 7.11/1.73 % (3441665)Termination phase: shuffling % 7.11/1.73 % (3441665)Time elapsed: 0.002 s % 7.11/1.73 % (3441665)Peak memory usage: 85 MB % 7.11/1.73 % (3441665)Instructions burned: 5 (million) % 7.11/1.73 % (3441671)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2796305919:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 7.11/1.73 % (3441667)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3996570496:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 7.11/1.73 % (3441667)Instruction limit reached! % 7.11/1.73 % (3441667)------------------------------ % 7.11/1.73 % (3441667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.73 % (3441667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.73 % (3441667)CaDiCaL version: 2.1.3 % 7.11/1.73 % (3441667)Termination reason: Instruction limit % 7.11/1.73 % (3441667)Termination phase: shuffling % 7.11/1.73 % (3441667)Time elapsed: 0.001 s % 7.11/1.73 % (3441667)Peak memory usage: 85 MB % 7.11/1.73 % (3441667)Instructions burned: 2 (million) % 7.11/1.73 % (3441671)Instruction limit reached! % 7.11/1.73 % (3441671)------------------------------ % 7.11/1.73 % (3441671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.73 % (3441671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.73 % (3441671)CaDiCaL version: 2.1.3 % 7.11/1.73 % (3441671)Termination reason: Instruction limit % 7.11/1.73 % (3441671)Termination phase: Property scanning % 7.11/1.73 % (3441671)Time elapsed: 0.050 s % 7.11/1.73 % (3441671)Peak memory usage: 86 MB % 7.11/1.73 % (3441671)Instructions burned: 129 (million) % 7.11/1.73 % (3441677)dis+10_1_si=on:random_seed=2656405210:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 7.11/1.73 % (3441677)Instruction limit reached! % 7.11/1.73 % (3441677)------------------------------ % 7.11/1.73 % (3441677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.73 % (3441677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.73 % (3441677)CaDiCaL version: 2.1.3 % 7.11/1.73 % (3441677)Termination reason: Instruction limit % 7.11/1.73 % (3441677)Termination phase: shuffling % 7.11/1.73 % (3441677)Time elapsed: 0.003 s % 7.11/1.73 % (3441677)Peak memory usage: 85 MB % 7.11/1.73 % (3441677)Instructions burned: 13 (million) % 7.11/1.73 % (3441679)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1339195506:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 7.11/1.73 % (3441678)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=159763117:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 8.26/1.93 % (3441678)Instruction limit reached! % 8.26/1.93 % (3441678)------------------------------ % 8.26/1.93 % (3441678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.26/1.93 % (3441678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.26/1.93 % (3441678)CaDiCaL version: 2.1.3 % 8.26/1.93 % (3441678)Termination reason: Instruction limit % 8.26/1.93 % (3441678)Termination phase: Property scanning % 8.26/1.93 % (3441678)Time elapsed: 0.011 s % 8.26/1.93 % (3441678)Peak memory usage: 85 MB % 8.26/1.93 % (3441678)Instructions burned: 28 (million) % 8.26/1.93 % (3441679)Instruction limit reached! % 8.26/1.93 % (3441679)------------------------------ % 8.26/1.93 % (3441679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.26/1.93 % (3441679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.26/1.93 % (3441679)CaDiCaL version: 2.1.3 % 8.26/1.93 % (3441679)Termination reason: Instruction limit % 8.26/1.93 % (3441679)Termination phase: Property scanning % 8.26/1.93 % (3441679)Time elapsed: 0.014 s % 8.26/1.93 % (3441679)Peak memory usage: 85 MB % 8.26/1.93 % (3441679)Instructions burned: 35 (million) % 8.26/1.93 % (3441652)------------------------------ % 8.26/1.93 % (3441652)------------------------------ % 8.26/1.93 % (3441682)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2520586716:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 8.26/1.93 % (3441682)Instruction limit reached! % 8.26/1.93 % (3441682)------------------------------ % 8.26/1.93 % (3441682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.26/1.93 % (3441682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.26/1.93 % (3441682)CaDiCaL version: 2.1.3 % 8.26/1.93 % (3441682)Termination reason: Instruction limit % 8.26/1.93 % (3441682)Termination phase: shuffling % 8.26/1.93 % (3441682)Time elapsed: 0.002 s % 8.26/1.93 % (3441682)Peak memory usage: 85 MB % 8.26/1.93 % (3441682)Instructions burned: 5 (million) % 8.26/1.93 % (3441689)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3009518610:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 8.26/1.93 % (3441686)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3383392013:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 8.26/1.93 % (3441686)Instruction limit reached! % 8.26/1.93 % (3441686)------------------------------ % 8.26/1.93 % (3441686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.26/1.93 % (3441686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.26/1.93 % (3441686)CaDiCaL version: 2.1.3 % 8.26/1.93 % (3441686)Termination reason: Instruction limit % 8.26/1.93 % (3441686)Termination phase: shuffling % 8.26/1.93 % (3441686)Time elapsed: 0.004 s % 8.26/1.93 % (3441686)Peak memory usage: 85 MB % 8.26/1.93 % (3441686)Instructions burned: 10 (million) % 8.26/1.93 % (3441690)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1767627641:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi) % 8.26/1.93 % (3441690)Instruction limit reached! % 8.26/1.93 % (3441690)------------------------------ % 8.26/1.93 % (3441690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.26/1.93 % (3441690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.26/1.93 % (3441690)CaDiCaL version: 2.1.3 % 8.26/1.93 % (3441690)Termination reason: Instruction limit % 8.26/1.93 % (3441690)Termination phase: Property scanning % 8.26/1.93 % (3441690)Time elapsed: 0.006 s % 8.26/1.93 % (3441690)Peak memory usage: 85 MB % 8.26/1.93 % (3441690)Instructions burned: 14 (million) % 8.26/1.93 % (3441689)Instruction limit reached! % 8.26/1.93 % (3441689)------------------------------ % 8.26/1.93 % (3441689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.26/1.93 % (3441689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.26/1.93 % (3441689)CaDiCaL version: 2.1.3 % 8.26/1.93 % (3441689)Termination reason: Instruction limit % 8.26/1.93 % (3441689)Termination phase: Saturation % 8.26/1.93 % (3441689)Time elapsed: 0.074 s % 8.26/1.93 % (3441689)Peak memory usage: 88 MB % 8.26/1.93 % (3441689)Instructions burned: 370 (million) % 8.26/1.93 % (3441693)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3446544350:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 10.47/2.15 % (3441694)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2621879575:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 10.47/2.15 % (3441694)Instruction limit reached! % 10.47/2.15 % (3441694)------------------------------ % 10.47/2.15 % (3441694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.47/2.15 % (3441694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.47/2.15 % (3441694)CaDiCaL version: 2.1.3 % 10.47/2.15 % (3441694)Termination reason: Instruction limit % 10.47/2.15 % (3441694)Termination phase: shuffling % 10.47/2.15 % (3441694)Time elapsed: 0.004 s % 10.47/2.15 % (3441694)Peak memory usage: 85 MB % 10.47/2.15 % (3441694)Instructions burned: 10 (million) % 10.47/2.15 % (3441698)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=3046379330:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 10.47/2.15 % (3441696)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1751529439:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi) % 10.47/2.15 % (3441702)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3910158109:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 10.47/2.15 % (3441700)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=3007183696:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi) % 10.47/2.15 % (3441696)Instruction limit reached! % 10.47/2.15 % (3441696)------------------------------ % 10.47/2.15 % (3441696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.47/2.15 % (3441696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.47/2.15 % (3441696)CaDiCaL version: 2.1.3 % 10.47/2.15 % (3441696)Termination reason: Instruction limit % 10.47/2.15 % (3441696)Termination phase: Property scanning % 10.47/2.15 % (3441696)Time elapsed: 0.029 s % 10.47/2.15 % (3441696)Peak memory usage: 85 MB % 10.47/2.15 % (3441696)Instructions burned: 72 (million) % 10.47/2.15 % (3441698)Instruction limit reached! % 10.47/2.15 % (3441698)------------------------------ % 10.47/2.15 % (3441698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.47/2.15 % (3441698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.47/2.15 % (3441698)CaDiCaL version: 2.1.3 % 10.47/2.15 % (3441698)Termination reason: Instruction limit % 10.47/2.15 % (3441698)Termination phase: Property scanning % 10.47/2.15 % (3441698)Time elapsed: 0.030 s % 10.47/2.15 % (3441698)Peak memory usage: 85 MB % 10.47/2.15 % (3441698)Instructions burned: 77 (million) % 10.47/2.15 % (3441693)Instruction limit reached! % 10.47/2.15 % (3441693)------------------------------ % 10.47/2.15 % (3441693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.47/2.15 % (3441693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.47/2.15 % (3441693)CaDiCaL version: 2.1.3 % 10.47/2.15 % (3441693)Termination reason: Instruction limit % 10.47/2.15 % (3441693)Termination phase: Property scanning % 10.47/2.15 % (3441693)Time elapsed: 0.090 s % 10.47/2.15 % (3441693)Peak memory usage: 86 MB % 10.47/2.15 % (3441693)Instructions burned: 228 (million) % 10.47/2.15 % (3441702)Instruction limit reached! % 10.47/2.15 % (3441702)------------------------------ % 10.47/2.15 % (3441702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.47/2.15 % (3441702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.47/2.15 % (3441702)CaDiCaL version: 2.1.3 % 10.47/2.15 % (3441702)Termination reason: Instruction limit % 10.47/2.15 % (3441702)Termination phase: Property scanning % 10.47/2.15 % (3441702)Time elapsed: 0.037 s % 10.47/2.15 % (3441702)Peak memory usage: 85 MB % 10.47/2.15 % (3441702)Instructions burned: 138 (million) % 10.47/2.15 % (3441703)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2901645973:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 10.47/2.15 % (3441703)Instruction limit reached! % 10.47/2.15 % (3441703)------------------------------ % 10.47/2.15 % (3441703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.47/2.15 % (3441700)Instruction limit reached! % 10.47/2.15 % (3441700)------------------------------ % 10.47/2.15 % (3441700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.43 % (3441700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.43 % (3441703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.43 % (3441700)CaDiCaL version: 2.1.3 % 11.70/2.43 % (3441703)CaDiCaL version: 2.1.3 % 11.70/2.43 % (3441700)Termination reason: Instruction limit % 11.70/2.43 % (3441700)Termination phase: Property scanning % 11.70/2.43 % (3441703)Termination reason: Instruction limit % 11.70/2.43 % (3441703)Termination phase: Property scanning % 11.70/2.43 % (3441700)Time elapsed: 0.119 s % 11.70/2.43 % (3441703)Time elapsed: 0.053 s % 11.70/2.43 % (3441700)Peak memory usage: 86 MB % 11.70/2.43 % (3441703)Peak memory usage: 86 MB % 11.70/2.43 % (3441700)Instructions burned: 298 (million) % 11.70/2.43 % (3441703)Instructions burned: 135 (million) % 11.70/2.43 % (3441706)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1329984149:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/40Mi) % 11.70/2.43 % (3441711)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=661513944:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi) % 11.70/2.43 % (3441706)Instruction limit reached! % 11.70/2.43 % (3441706)------------------------------ % 11.70/2.43 % (3441706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.43 % (3441706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.43 % (3441706)CaDiCaL version: 2.1.3 % 11.70/2.43 % (3441706)Termination reason: Instruction limit % 11.70/2.43 % (3441706)Termination phase: Property scanning % 11.70/2.43 % (3441706)Time elapsed: 0.017 s % 11.70/2.43 % (3441706)Peak memory usage: 85 MB % 11.70/2.43 % (3441706)Instructions burned: 41 (million) % 11.70/2.43 % (3441712)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2245022435:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi) % 11.70/2.43 % (3441711)Instruction limit reached! % 11.70/2.43 % (3441711)------------------------------ % 11.70/2.43 % (3441711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.43 % (3441711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.43 % (3441711)CaDiCaL version: 2.1.3 % 11.70/2.43 % (3441711)Termination reason: Instruction limit % 11.70/2.43 % (3441711)Termination phase: Property scanning % 11.70/2.43 % (3441711)Time elapsed: 0.063 s % 11.70/2.43 % (3441711)Peak memory usage: 86 MB % 11.70/2.43 % (3441711)Instructions burned: 309 (million) % 11.70/2.43 % (3441713)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2744895281:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 11.70/2.43 % (3441714)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=1096620799:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 11.70/2.43 % (3441713)Instruction limit reached! % 11.70/2.43 % (3441713)------------------------------ % 11.70/2.43 % (3441713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.43 % (3441713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.43 % (3441713)CaDiCaL version: 2.1.3 % 11.70/2.43 % (3441713)Termination reason: Instruction limit % 11.70/2.43 % (3441713)Termination phase: Property scanning % 11.70/2.43 % (3441713)Time elapsed: 0.052 s % 11.70/2.43 % (3441713)Peak memory usage: 86 MB % 11.70/2.43 % (3441713)Instructions burned: 131 (million) % 11.70/2.43 % (3441717)dis+10_1_si=on:random_seed=1691530291:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi) % 11.70/2.43 % (3441718)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4029486126:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi) % 11.70/2.43 % (3441722)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1987765548:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 11.70/2.43 % (3441720)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2885598969:i=141:doe=on:rtra=on_2986 on theBenchmark for (2986ds/141Mi) % 11.70/2.43 % (3441714)Instruction limit reached! % 11.70/2.43 % (3441714)------------------------------ % 11.70/2.43 % (3441714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441714)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441714)Termination reason: Instruction limit % 12.81/2.68 % (3441714)Termination phase: SInE selection % 12.81/2.68 % (3441714)Time elapsed: 0.102 s % 12.81/2.68 % (3441714)Peak memory usage: 86 MB % 12.81/2.68 % (3441714)Instructions burned: 262 (million) % 12.81/2.68 % (3441722)Instruction limit reached! % 12.81/2.68 % (3441722)------------------------------ % 12.81/2.68 % (3441722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441722)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441722)Termination reason: Instruction limit % 12.81/2.68 % (3441722)Termination phase: Property scanning % 12.81/2.68 % (3441722)Time elapsed: 0.015 s % 12.81/2.68 % (3441722)Peak memory usage: 85 MB % 12.81/2.68 % (3441722)Instructions burned: 66 (million) % 12.81/2.68 % (3441720)Instruction limit reached! % 12.81/2.68 % (3441720)------------------------------ % 12.81/2.68 % (3441720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441720)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441720)Termination reason: Instruction limit % 12.81/2.68 % (3441720)Termination phase: Property scanning % 12.81/2.68 % (3441720)Time elapsed: 0.056 s % 12.81/2.68 % (3441720)Peak memory usage: 86 MB % 12.81/2.68 % (3441720)Instructions burned: 142 (million) % 12.81/2.68 % (3441718)Instruction limit reached! % 12.81/2.68 % (3441718)------------------------------ % 12.81/2.68 % (3441718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441718)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441718)Termination reason: Instruction limit % 12.81/2.68 % (3441718)Termination phase: Saturation % 12.81/2.68 % (3441718)Time elapsed: 0.148 s % 12.81/2.68 % (3441718)Peak memory usage: 88 MB % 12.81/2.68 % (3441718)Instructions burned: 385 (million) % 12.81/2.68 % (3441712)Instruction limit reached! % 12.81/2.68 % (3441712)------------------------------ % 12.81/2.68 % (3441712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441712)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441712)Termination reason: Instruction limit % 12.81/2.68 % (3441712)Termination phase: Saturation % 12.81/2.68 % (3441712)Time elapsed: 0.264 s % 12.81/2.68 % (3441712)Peak memory usage: 130 MB % 12.81/2.68 % (3441712)Instructions burned: 599 (million) % 12.81/2.68 % (3441726)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=867780630:i=121:nm=16:rtra=on_2984 on theBenchmark for (2984ds/121Mi) % 12.81/2.68 % (3441732)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=239895921:s2a=on:i=128:s2at=5:ins=3:rtra=on_2984 on theBenchmark for (2984ds/128Mi) % 12.81/2.68 % (3441726)Instruction limit reached! % 12.81/2.68 % (3441726)------------------------------ % 12.81/2.68 % (3441726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441726)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441726)Termination reason: Instruction limit % 12.81/2.68 % (3441726)Termination phase: Property scanning % 12.81/2.68 % (3441726)Time elapsed: 0.049 s % 12.81/2.68 % (3441726)Peak memory usage: 85 MB % 12.81/2.68 % (3441726)Instructions burned: 123 (million) % 12.81/2.68 % (3441733)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=535676965:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi) % 12.81/2.68 % (3441733)Instruction limit reached! % 12.81/2.68 % (3441733)------------------------------ % 12.81/2.68 % (3441733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.81/2.68 % (3441733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.81/2.68 % (3441733)CaDiCaL version: 2.1.3 % 12.81/2.68 % (3441733)Termination reason: Instruction limit % 12.81/2.68 % (3441733)Termination phase: Property scanning % 12.81/2.68 % (3441733)Time elapsed: 0.016 s % 12.81/2.68 % (3441733)Peak memory usage: 85 MB % 12.81/2.68 % (3441733)Instructions burned: 41 (million) % 12.81/2.68 % (3441732)Instruction limit reached! % 12.81/2.68 % (3441732)------------------------------ % 17.09/3.03 % (3441732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.03 % (3441732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.03 % (3441732)CaDiCaL version: 2.1.3 % 17.09/3.03 % (3441732)Termination reason: Instruction limit % 17.09/3.03 % (3441732)Termination phase: Property scanning % 17.09/3.03 % (3441732)Time elapsed: 0.051 s % 17.09/3.03 % (3441732)Peak memory usage: 86 MB % 17.09/3.03 % (3441732)Instructions burned: 128 (million) % 17.09/3.03 % (3441734)dis+1010_1_to=kbo:si=on:random_seed=2831080493:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/175Mi) % 17.09/3.03 % (3441736)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2477305228:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/329Mi) % 17.09/3.03 % (3441738)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1477388537:s2a=on:i=483:doe=on:nm=32:rtra=on_2982 on theBenchmark for (2982ds/483Mi) % 17.09/3.03 % (3441734)Instruction limit reached! % 17.09/3.03 % (3441734)------------------------------ % 17.09/3.03 % (3441734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.03 % (3441734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.03 % (3441734)CaDiCaL version: 2.1.3 % 17.09/3.03 % (3441734)Termination reason: Instruction limit % 17.09/3.03 % (3441734)Termination phase: Property scanning % 17.09/3.03 % (3441734)Time elapsed: 0.069 s % 17.09/3.03 % (3441734)Peak memory usage: 85 MB % 17.09/3.03 % (3441734)Instructions burned: 176 (million) % 17.09/3.03 % (3441743)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2325705422:i=349:rtra=on_2982 on theBenchmark for (2982ds/349Mi) % 17.09/3.03 % (3441741)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=775569660:thitd=on:i=215:nm=0:rtra=on:ev=force_2982 on theBenchmark for (2982ds/215Mi) % 17.09/3.03 % (3441717)Instruction limit reached! % 17.09/3.03 % (3441717)------------------------------ % 17.09/3.03 % (3441717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.03 % (3441717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.03 % (3441717)CaDiCaL version: 2.1.3 % 17.09/3.03 % (3441717)Termination reason: Instruction limit % 17.09/3.03 % (3441717)Termination phase: Saturation % 17.09/3.03 % (3441717)Time elapsed: 0.386 s % 17.09/3.03 % (3441717)Peak memory usage: 88 MB % 17.09/3.03 % (3441717)Instructions burned: 1002 (million) % 17.09/3.03 % (3441744)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1375457538:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi) % 17.09/3.03 % (3441736)Instruction limit reached! % 17.09/3.03 % (3441736)------------------------------ % 17.09/3.03 % (3441736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.03 % (3441736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.03 % (3441736)CaDiCaL version: 2.1.3 % 17.09/3.03 % (3441736)Termination reason: Instruction limit % 17.09/3.03 % (3441736)Termination phase: Property scanning % 17.09/3.03 % (3441736)Time elapsed: 0.130 s % 17.09/3.03 % (3441736)Peak memory usage: 85 MB % 17.09/3.03 % (3441736)Instructions burned: 331 (million) % 17.09/3.03 % (3441741)Instruction limit reached! % 17.09/3.03 % (3441741)------------------------------ % 17.09/3.03 % (3441741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.03 % (3441741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.09/3.03 % (3441741)CaDiCaL version: 2.1.3 % 17.09/3.03 % (3441741)Termination reason: Instruction limit % 17.09/3.03 % (3441741)Termination phase: Property scanning % 17.09/3.03 % (3441741)Time elapsed: 0.086 s % 17.09/3.03 % (3441741)Peak memory usage: 86 MB % 17.09/3.03 % (3441741)Instructions burned: 217 (million) % 17.09/3.03 % (3441748)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1398161156:i=328:kws=inv_frequency:nm=20:rtra=on_2981 on theBenchmark for (2981ds/328Mi) % 17.09/3.03 % (3441743)Instruction limit reached! % 17.09/3.03 % (3441743)------------------------------ % 17.09/3.03 % (3441743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.09/3.03 % (3441743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/3.29 % (3441743)CaDiCaL version: 2.1.3 % 18.25/3.29 % (3441743)Termination reason: Instruction limit % 18.25/3.29 % (3441743)Termination phase: Saturation % 18.25/3.29 % (3441743)Time elapsed: 0.153 s % 18.25/3.29 % (3441743)Peak memory usage: 111 MB % 18.25/3.29 % (3441743)Instructions burned: 350 (million) % 18.25/3.29 % (3441738)Instruction limit reached! % 18.25/3.29 % (3441738)------------------------------ % 18.25/3.29 % (3441738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.25/3.29 % (3441738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/3.29 % (3441738)CaDiCaL version: 2.1.3 % 18.25/3.29 % (3441738)Termination reason: Instruction limit % 18.25/3.29 % (3441738)Termination phase: Saturation % 18.25/3.29 % (3441738)Time elapsed: 0.218 s % 18.25/3.29 % (3441738)Peak memory usage: 128 MB % 18.25/3.29 % (3441738)Instructions burned: 483 (million) % 18.25/3.29 % (3441748)Instruction limit reached! % 18.25/3.29 % (3441748)------------------------------ % 18.25/3.29 % (3441748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.25/3.29 % (3441748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/3.29 % (3441748)CaDiCaL version: 2.1.3 % 18.25/3.29 % (3441748)Termination reason: Instruction limit % 18.25/3.29 % (3441748)Termination phase: Property scanning % 18.25/3.29 % (3441748)Time elapsed: 0.067 s % 18.25/3.29 % (3441748)Peak memory usage: 86 MB % 18.25/3.29 % (3441748)Instructions burned: 331 (million) % 18.25/3.29 % (3441744)Refutation not found, incomplete strategy % 18.25/3.29 % (3441744)------------------------------ % 18.25/3.29 % (3441744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.25/3.29 % (3441744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/3.29 % (3441744)CaDiCaL version: 2.1.3 % 18.25/3.29 % (3441744)Termination reason: Refutation not found, incomplete strategy % 18.25/3.29 % (3441744)Time elapsed: 0.111 s % 18.25/3.29 % (3441744)Peak memory usage: 88 MB % 18.25/3.29 % (3441744)Instructions burned: 289 (million) % 18.25/3.29 % (3441751)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2336428486:i=281:gtgl=2:rtra=on:gtg=all_2980 on theBenchmark for (2980ds/281Mi) % 18.25/3.29 % (3441754)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1194276105:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2979 on theBenchmark for (2979ds/321Mi) % 18.25/3.29 % (3441753)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2840782184:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/484Mi) % 18.25/3.29 % (3441751)Instruction limit reached! % 18.25/3.29 % (3441751)------------------------------ % 18.25/3.29 % (3441751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.25/3.29 % (3441751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/3.29 % (3441751)CaDiCaL version: 2.1.3 % 18.25/3.29 % (3441751)Termination reason: Instruction limit % 18.25/3.29 % (3441751)Termination phase: Property scanning % 18.25/3.29 % (3441751)Time elapsed: 0.081 s % 18.25/3.29 % (3441751)Peak memory usage: 86 MB % 18.25/3.29 % (3441751)Instructions burned: 285 (million) % 18.25/3.29 % (3441759)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1774537247:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi) % 18.25/3.29 % (3441757)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=162504013:i=416:rtra=on:gtg=position:ss=axioms_2979 on theBenchmark for (2979ds/416Mi) % 18.25/3.29 % (3441760)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=1959790997:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 18.25/3.29 % (3441753)Refutation not found, incomplete strategy % 18.25/3.29 % (3441753)------------------------------ % 18.25/3.29 % (3441753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.25/3.29 % (3441753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/3.29 % (3441753)CaDiCaL version: 2.1.3 % 18.25/3.29 % (3441753)Termination reason: Refutation not found, incomplete strategy % 18.25/3.29 % (3441753)Time elapsed: 0.107 s % 18.25/3.29 % (3441753)Peak memory usage: 88 MB % 18.25/3.29 % (3441753)Instructions burned: 282 (million) % 18.25/3.29 % (3441744)------------------------------ % 18.25/3.29 % (3441744)------------------------------ % 18.25/3.29 % (3441754)Refutation not found, incomplete strategy % 18.25/3.29 % (3441754)------------------------------ % 19.63/3.61 % (3441754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.61 % (3441754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.61 % (3441754)CaDiCaL version: 2.1.3 % 19.63/3.61 % (3441754)Termination reason: Refutation not found, incomplete strategy % 19.63/3.61 % (3441754)Time elapsed: 0.130 s % 19.63/3.61 % (3441754)Peak memory usage: 112 MB % 19.63/3.61 % (3441754)Instructions burned: 287 (million) % 19.63/3.61 % (3441770)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3200514413:i=375:kws=inv_arity_squared:rtra=on_2977 on theBenchmark for (2977ds/375Mi) % 19.63/3.61 % (3441760)Instruction limit reached! % 19.63/3.61 % (3441760)------------------------------ % 19.63/3.61 % (3441760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.61 % (3441760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.61 % (3441760)CaDiCaL version: 2.1.3 % 19.63/3.61 % (3441760)Termination reason: Instruction limit % 19.63/3.61 % (3441760)Termination phase: Property scanning % 19.63/3.61 % (3441760)Time elapsed: 0.106 s % 19.63/3.61 % (3441760)Peak memory usage: 86 MB % 19.63/3.61 % (3441760)Instructions burned: 278 (million) % 19.63/3.61 % (3441757)Refutation not found, incomplete strategy % 19.63/3.61 % (3441757)------------------------------ % 19.63/3.61 % (3441757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.61 % (3441757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.61 % (3441757)CaDiCaL version: 2.1.3 % 19.63/3.61 % (3441757)Termination reason: Refutation not found, incomplete strategy % 19.63/3.61 % (3441757)Time elapsed: 0.128 s % 19.63/3.61 % (3441757)Peak memory usage: 111 MB % 19.63/3.61 % (3441757)Instructions burned: 286 (million) % 19.63/3.61 % (3441759)Instruction limit reached! % 19.63/3.61 % (3441759)------------------------------ % 19.63/3.61 % (3441759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.61 % (3441759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.61 % (3441759)CaDiCaL version: 2.1.3 % 19.63/3.61 % (3441759)Termination reason: Instruction limit % 19.63/3.61 % (3441759)Termination phase: Saturation % 19.63/3.61 % (3441759)Time elapsed: 0.207 s % 19.63/3.61 % (3441759)Peak memory usage: 114 MB % 19.63/3.61 % (3441759)Instructions burned: 472 (million) % 19.63/3.61 % (3441770)Instruction limit reached! % 19.63/3.61 % (3441770)------------------------------ % 19.63/3.61 % (3441770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.61 % (3441770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.61 % (3441770)CaDiCaL version: 2.1.3 % 19.63/3.61 % (3441770)Termination reason: Instruction limit % 19.63/3.61 % (3441770)Termination phase: Saturation % 19.63/3.61 % (3441770)Time elapsed: 0.130 s % 19.63/3.61 % (3441770)Peak memory usage: 112 MB % 19.63/3.61 % (3441770)Instructions burned: 375 (million) % 19.63/3.61 % (3441774)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4057904347:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/387Mi) % 19.63/3.61 % (3441753)------------------------------ % 19.63/3.61 % (3441753)------------------------------ % 19.63/3.61 % (3441778)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2536631890:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2976 on theBenchmark for (2976ds/513Mi) % 19.63/3.61 % (3441754)------------------------------ % 19.63/3.61 % (3441754)------------------------------ % 19.63/3.61 % (3441757)------------------------------ % 19.63/3.61 % (3441757)------------------------------ % 19.63/3.61 % (3441781)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=53659084:i=334:rtra=on_2975 on theBenchmark for (2975ds/334Mi) % 19.63/3.61 % (3441774)Refutation not found, incomplete strategy % 19.63/3.61 % (3441774)------------------------------ % 19.63/3.61 % (3441774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.61 % (3441774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.61 % (3441774)CaDiCaL version: 2.1.3 % 19.63/3.61 % (3441774)Termination reason: Refutation not found, incomplete strategy % 19.63/3.61 % (3441774)Time elapsed: 0.137 s % 19.63/3.61 % (3441774)Peak memory usage: 112 MB % 19.63/3.61 % (3441774)Instructions burned: 302 (million) % 19.63/3.61 % (3441782)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=912811345:i=359:rtra=on:gtg=exists_top:ss=axioms_2975 on theBenchmark for (2975ds/359Mi) % 21.69/3.98 % (3441778)Instruction limit reached! % 21.69/3.98 % (3441778)------------------------------ % 21.69/3.98 % (3441778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.69/3.98 % (3441778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.69/3.98 % (3441778)CaDiCaL version: 2.1.3 % 21.69/3.98 % (3441778)Termination reason: Instruction limit % 21.69/3.98 % (3441778)Termination phase: Property scanning % 21.69/3.98 % (3441778)Time elapsed: 0.163 s % 21.69/3.98 % (3441778)Peak memory usage: 86 MB % 21.69/3.98 % (3441778)Instructions burned: 513 (million) % 21.69/3.98 % (3441786)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2989987720:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2974 on theBenchmark for (2974ds/341Mi) % 21.69/3.98 % (3441788)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=961744742:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/261Mi) % 21.69/3.98 % (3441781)Instruction limit reached! % 21.69/3.98 % (3441781)------------------------------ % 21.69/3.98 % (3441781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.69/3.98 % (3441781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.69/3.98 % (3441781)CaDiCaL version: 2.1.3 % 21.69/3.98 % (3441781)Termination reason: Instruction limit % 21.69/3.98 % (3441781)Termination phase: Saturation % 21.69/3.98 % (3441781)Time elapsed: 0.165 s % 21.69/3.98 % (3441781)Peak memory usage: 129 MB % 21.69/3.98 % (3441781)Instructions burned: 335 (million) % 21.69/3.98 % (3441782)Instruction limit reached! % 21.69/3.98 % (3441782)------------------------------ % 21.69/3.98 % (3441782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.69/3.98 % (3441782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.69/3.98 % (3441782)CaDiCaL version: 2.1.3 % 21.69/3.98 % (3441782)Termination reason: Instruction limit % 21.69/3.98 % (3441782)Termination phase: SInE selection % 21.69/3.98 % (3441782)Time elapsed: 0.144 s % 21.69/3.98 % (3441782)Peak memory usage: 86 MB % 21.69/3.98 % (3441782)Instructions burned: 359 (million) % 21.69/3.98 % (3441789)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=2047867126:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/235Mi) % 21.69/3.98 % (3441788)Refutation not found, incomplete strategy % 21.69/3.98 % (3441788)------------------------------ % 21.69/3.98 % (3441788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.69/3.98 % (3441788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.69/3.98 % (3441788)CaDiCaL version: 2.1.3 % 21.69/3.98 % (3441788)Termination reason: Refutation not found, incomplete strategy % 21.69/3.98 % (3441788)Time elapsed: 0.091 s % 21.69/3.98 % (3441788)Peak memory usage: 111 MB % 21.69/3.98 % (3441788)Instructions burned: 193 (million) % 21.69/3.98 % (3441786)Instruction limit reached! % 21.69/3.98 % (3441786)------------------------------ % 21.69/3.98 % (3441786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.69/3.98 % (3441786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.69/3.98 % (3441786)CaDiCaL version: 2.1.3 % 21.69/3.98 % (3441786)Termination reason: Instruction limit % 21.69/3.98 % (3441786)Termination phase: Property scanning % 21.69/3.98 % (3441786)Time elapsed: 0.136 s % 21.69/3.98 % (3441786)Peak memory usage: 86 MB % 21.69/3.98 % (3441786)Instructions burned: 343 (million) % 21.69/3.98 % (3441774)------------------------------ % 21.69/3.98 % (3441774)------------------------------ % 21.69/3.98 % (3441792)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3150911132:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2972 on theBenchmark for (2972ds/273Mi) % 21.69/3.98 % (3441789)Instruction limit reached! % 21.69/3.98 % (3441789)------------------------------ % 21.69/3.98 % (3441789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.69/3.98 % (3441789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.69/3.98 % (3441789)CaDiCaL version: 2.1.3 % 21.69/3.98 % (3441789)Termination reason: Instruction limit % 21.69/3.98 % (3441789)Termination phase: SInE selection % 25.52/4.36 % (3441789)Time elapsed: 0.093 s % 25.52/4.36 % (3441789)Peak memory usage: 86 MB % 25.52/4.36 % (3441789)Instructions burned: 237 (million) % 25.52/4.36 % (3441796)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=901249989:i=4428:doe=on:fsr=off:rtra=on_2971 on theBenchmark for (2971ds/4428Mi) % 25.52/4.36 % (3441795)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2395954895:i=146:doe=on:rtra=on_2971 on theBenchmark for (2971ds/146Mi) % 25.52/4.36 % (3441798)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=4152050201:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi) % 25.52/4.36 % (3441792)Instruction limit reached! % 25.52/4.36 % (3441792)------------------------------ % 25.52/4.36 % (3441792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.36 % (3441792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.36 % (3441792)CaDiCaL version: 2.1.3 % 25.52/4.36 % (3441792)Termination reason: Instruction limit % 25.52/4.36 % (3441792)Termination phase: Property scanning % 25.52/4.36 % (3441792)Time elapsed: 0.109 s % 25.52/4.36 % (3441792)Peak memory usage: 86 MB % 25.52/4.36 % (3441792)Instructions burned: 273 (million) % 25.52/4.36 % (3441798)Instruction limit reached! % 25.52/4.36 % (3441798)------------------------------ % 25.52/4.36 % (3441798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.36 % (3441798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.36 % (3441798)CaDiCaL version: 2.1.3 % 25.52/4.36 % (3441798)Termination reason: Instruction limit % 25.52/4.36 % (3441798)Termination phase: Property scanning % 25.52/4.36 % (3441798)Time elapsed: 0.056 s % 25.52/4.36 % (3441798)Peak memory usage: 86 MB % 25.52/4.36 % (3441798)Instructions burned: 278 (million) % 25.52/4.36 % (3441795)Instruction limit reached! % 25.52/4.36 % (3441795)------------------------------ % 25.52/4.36 % (3441795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.36 % (3441795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.36 % (3441795)CaDiCaL version: 2.1.3 % 25.52/4.36 % (3441795)Termination reason: Instruction limit % 25.52/4.36 % (3441795)Termination phase: Property scanning % 25.52/4.36 % (3441795)Time elapsed: 0.058 s % 25.52/4.36 % (3441795)Peak memory usage: 86 MB % 25.52/4.36 % (3441795)Instructions burned: 148 (million) % 25.52/4.36 % (3441788)------------------------------ % 25.52/4.36 % (3441788)------------------------------ % 25.52/4.36 % (3441799)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1509238625:i=1052:rtra=on_2970 on theBenchmark for (2970ds/1052Mi) % 25.52/4.36 % (3441801)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4230246641:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2970 on theBenchmark for (2970ds/655Mi) % 25.52/4.36 % (3441806)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3366179078:i=107:rtra=on_2969 on theBenchmark for (2969ds/107Mi) % 25.52/4.36 % (3441805)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=430745728:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2969 on theBenchmark for (2969ds/1054Mi) % 25.52/4.36 % (3441806)Instruction limit reached! % 25.52/4.36 % (3441806)------------------------------ % 25.52/4.36 % (3441806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.36 % (3441806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.36 % (3441806)CaDiCaL version: 2.1.3 % 25.52/4.36 % (3441806)Termination reason: Instruction limit % 25.52/4.36 % (3441806)Termination phase: Property scanning % 25.52/4.36 % (3441806)Time elapsed: 0.023 s % 25.52/4.36 % (3441806)Peak memory usage: 86 MB % 25.52/4.36 % (3441806)Instructions burned: 109 (million) % 25.52/4.36 % (3441807)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2136825331:s2a=on:i=450:doe=on:nm=32:rtra=on_2969 on theBenchmark for (2969ds/450Mi) % 25.52/4.36 % (3441805)Refutation not found, incomplete strategy % 25.52/4.36 % (3441805)------------------------------ % 25.52/4.36 % (3441805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.36 % (3441805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.36 % (3441805)CaDiCaL version: 2.1.3 % 27.31/4.72 % (3441805)Termination reason: Refutation not found, incomplete strategy % 27.31/4.72 % (3441805)Time elapsed: 0.067 s % 27.31/4.72 % (3441805)Peak memory usage: 88 MB % 27.31/4.72 % (3441805)Instructions burned: 181 (million) % 27.31/4.72 % (3441809)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 % 27.31/4.72 % (3441809)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3659096787:i=1090:aac=none:nm=0:rtra=on:rawr=on_2968 on theBenchmark for (2968ds/1090Mi) % 27.31/4.72 % (3441813)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4088744881:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2967 on theBenchmark for (2967ds/130Mi) % 27.31/4.72 % (3441813)Instruction limit reached! % 27.31/4.72 % (3441813)------------------------------ % 27.31/4.72 % (3441813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.72 % (3441813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.72 % (3441813)CaDiCaL version: 2.1.3 % 27.31/4.72 % (3441813)Termination reason: Instruction limit % 27.31/4.72 % (3441813)Termination phase: Property scanning % 27.31/4.72 % (3441813)Time elapsed: 0.028 s % 27.31/4.72 % (3441813)Peak memory usage: 85 MB % 27.31/4.72 % (3441813)Instructions burned: 135 (million) % 27.31/4.72 % (3441801)Instruction limit reached! % 27.31/4.72 % (3441801)------------------------------ % 27.31/4.72 % (3441801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.72 % (3441801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.72 % (3441801)CaDiCaL version: 2.1.3 % 27.31/4.72 % (3441801)Termination reason: Instruction limit % 27.31/4.72 % (3441801)Termination phase: Saturation % 27.31/4.72 % (3441801)Time elapsed: 0.249 s % 27.31/4.72 % (3441801)Peak memory usage: 89 MB % 27.31/4.72 % (3441801)Instructions burned: 655 (million) % 27.31/4.72 % (3441807)Instruction limit reached! % 27.31/4.72 % (3441807)------------------------------ % 27.31/4.72 % (3441807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.72 % (3441807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.72 % (3441807)CaDiCaL version: 2.1.3 % 27.31/4.72 % (3441807)Termination reason: Instruction limit % 27.31/4.72 % (3441807)Termination phase: Saturation % 27.31/4.72 % (3441807)Time elapsed: 0.207 s % 27.31/4.72 % (3441807)Peak memory usage: 129 MB % 27.31/4.72 % (3441807)Instructions burned: 451 (million) % 27.31/4.72 % (3441805)------------------------------ % 27.31/4.72 % (3441805)------------------------------ % 27.31/4.72 % (3441799)Instruction limit reached! % 27.31/4.72 % (3441799)------------------------------ % 27.31/4.72 % (3441799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.72 % (3441799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.72 % (3441799)CaDiCaL version: 2.1.3 % 27.31/4.72 % (3441799)Termination reason: Instruction limit % 27.31/4.72 % (3441799)Termination phase: Saturation % 27.31/4.72 % (3441799)Time elapsed: 0.387 s % 27.31/4.72 % (3441799)Peak memory usage: 95 MB % 27.31/4.72 % (3441799)Instructions burned: 1052 (million) % 27.31/4.72 % (3441817)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2202888547:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi) % 27.31/4.72 % (3441818)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=598900471:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi) % 27.31/4.72 % (3441822)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3466290723:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi) % 27.31/4.72 % (3441817)Instruction limit reached! % 27.31/4.72 % (3441817)------------------------------ % 27.31/4.72 % (3441817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.31/4.72 % (3441817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.31/4.72 % (3441817)CaDiCaL version: 2.1.3 % 27.31/4.72 % (3441817)Termination reason: Instruction limit % 27.31/4.72 % (3441817)Termination phase: Property scanning % 27.31/4.72 % (3441817)Time elapsed: 0.122 s % 27.31/4.72 % (3441817)Peak memory usage: 86 MB % 27.31/4.72 % (3441817)Instructions burned: 312 (million) % 27.31/4.72 % (3441819)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1321168339:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi) % 32.56/5.30 % (3441823)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3942597672:i=776:doe=on:rtra=on_2965 on theBenchmark for (2965ds/776Mi) % 32.56/5.30 % (3441822)Instruction limit reached! % 32.56/5.30 % (3441822)------------------------------ % 32.56/5.30 % (3441822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.56/5.30 % (3441822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.56/5.30 % (3441822)CaDiCaL version: 2.1.3 % 32.56/5.30 % (3441822)Termination reason: Instruction limit % 32.56/5.30 % (3441822)Termination phase: Property scanning % 32.56/5.30 % (3441822)Time elapsed: 0.102 s % 32.56/5.30 % (3441822)Peak memory usage: 86 MB % 32.56/5.30 % (3441822)Instructions burned: 308 (million) % 32.56/5.30 % (3441809)Instruction limit reached! % 32.56/5.30 % (3441809)------------------------------ % 32.56/5.30 % (3441809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.56/5.30 % (3441809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.56/5.30 % (3441809)CaDiCaL version: 2.1.3 % 32.56/5.30 % (3441809)Termination reason: Instruction limit % 32.56/5.30 % (3441809)Termination phase: Saturation % 32.56/5.30 % (3441809)Time elapsed: 0.447 s % 32.56/5.30 % (3441809)Peak memory usage: 115 MB % 32.56/5.30 % (3441809)Instructions burned: 1091 (million) % 32.56/5.30 % (3441818)Instruction limit reached! % 32.56/5.30 % (3441818)------------------------------ % 32.56/5.30 % (3441818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.56/5.30 % (3441818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.56/5.30 % (3441818)CaDiCaL version: 2.1.3 % 32.56/5.30 % (3441818)Termination reason: Instruction limit % 32.56/5.30 % (3441818)Termination phase: Property scanning % 32.56/5.30 % (3441818)Time elapsed: 0.196 s % 32.56/5.30 % (3441818)Peak memory usage: 87 MB % 32.56/5.30 % (3441818)Instructions burned: 494 (million) % 32.56/5.30 % (3441827)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1489004519:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/646Mi) % 32.56/5.30 % (3441830)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=2387685633:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2962 on theBenchmark for (2962ds/784Mi) % 32.56/5.30 % (3441832)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=916273866:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2962 on theBenchmark for (2962ds/246Mi) % 32.56/5.30 % (3441831)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=3575961009:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi) % 32.56/5.30 % (3441819)Instruction limit reached! % 32.56/5.30 % (3441819)------------------------------ % 32.56/5.30 % (3441819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.56/5.30 % (3441819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.56/5.30 % (3441819)CaDiCaL version: 2.1.3 % 32.56/5.30 % (3441819)Termination reason: Instruction limit % 32.56/5.30 % (3441819)Termination phase: Saturation % 32.56/5.30 % (3441819)Time elapsed: 0.323 s % 32.56/5.30 % (3441819)Peak memory usage: 92 MB % 32.56/5.30 % (3441819)Instructions burned: 835 (million) % 32.56/5.30 % (3441832)Instruction limit reached! % 32.56/5.30 % (3441832)------------------------------ % 32.56/5.30 % (3441832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.56/5.30 % (3441832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.56/5.30 % (3441832)CaDiCaL version: 2.1.3 % 32.56/5.30 % (3441832)Termination reason: Instruction limit % 32.56/5.30 % (3441832)Termination phase: SInE selection % 32.56/5.30 % (3441832)Time elapsed: 0.050 s % 32.56/5.30 % (3441832)Peak memory usage: 86 MB % 32.56/5.30 % (3441832)Instructions burned: 246 (million) % 32.56/5.30 % (3441823)Instruction limit reached! % 32.56/5.30 % (3441823)------------------------------ % 32.56/5.30 % (3441823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.56/5.30 % (3441823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.56/5.30 % (3441823)CaDiCaL version: 2.1.3 % 32.56/5.30 % (3441823)Termination reason: Instruction limit % 39.24/6.22 % (3441823)Termination phase: Saturation % 39.24/6.22 % (3441823)Time elapsed: 0.322 s % 39.24/6.22 % (3441823)Peak memory usage: 116 MB % 39.24/6.22 % (3441823)Instructions burned: 780 (million) % 39.24/6.22 % (3441838)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2759346845:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi) % 39.24/6.22 % (3441827)Instruction limit reached! % 39.24/6.22 % (3441827)------------------------------ % 39.24/6.22 % (3441827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.24/6.22 % (3441827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.24/6.22 % (3441827)CaDiCaL version: 2.1.3 % 39.24/6.22 % (3441827)Termination reason: Instruction limit % 39.24/6.22 % (3441827)Termination phase: Saturation % 39.24/6.22 % (3441827)Time elapsed: 0.280 s % 39.24/6.22 % (3441827)Peak memory usage: 130 MB % 39.24/6.22 % (3441827)Instructions burned: 646 (million) % 39.24/6.22 % (3441838)Instruction limit reached! % 39.24/6.22 % (3441838)------------------------------ % 39.24/6.22 % (3441838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.24/6.22 % (3441838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.24/6.22 % (3441838)CaDiCaL version: 2.1.3 % 39.24/6.22 % (3441838)Termination reason: Instruction limit % 39.24/6.22 % (3441838)Termination phase: Property scanning % 39.24/6.22 % (3441838)Time elapsed: 0.056 s % 39.24/6.22 % (3441838)Peak memory usage: 86 MB % 39.24/6.22 % (3441838)Instructions burned: 273 (million) % 39.24/6.22 % (3441837)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3433749246:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi) % 39.24/6.22 % (3441839)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1664730391:i=102:nm=16:rtra=on_2959 on theBenchmark for (2959ds/102Mi) % 39.24/6.22 % (3441830)Instruction limit reached! % 39.24/6.22 % (3441830)------------------------------ % 39.24/6.22 % (3441830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.24/6.22 % (3441830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.24/6.22 % (3441830)CaDiCaL version: 2.1.3 % 39.24/6.22 % (3441830)Termination reason: Instruction limit % 39.24/6.22 % (3441830)Termination phase: Saturation % 39.24/6.22 % (3441830)Time elapsed: 0.322 s % 39.24/6.22 % (3441830)Peak memory usage: 112 MB % 39.24/6.22 % (3441830)Instructions burned: 784 (million) % 39.24/6.22 % (3441839)Instruction limit reached! % 39.24/6.22 % (3441839)------------------------------ % 39.24/6.22 % (3441839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.24/6.22 % (3441839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.24/6.22 % (3441839)CaDiCaL version: 2.1.3 % 39.24/6.22 % (3441839)Termination reason: Instruction limit % 39.24/6.22 % (3441839)Termination phase: Property scanning % 39.24/6.22 % (3441839)Time elapsed: 0.040 s % 39.24/6.22 % (3441839)Peak memory usage: 86 MB % 39.24/6.22 % (3441839)Instructions burned: 103 (million) % 39.24/6.22 % (3441844)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2112467440:i=6400:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/6400Mi) % 39.24/6.22 % (3441843)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=4240133682:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2958 on theBenchmark for (2958ds/1094Mi) % 39.24/6.22 % (3441837)Refutation not found, incomplete strategy % 39.24/6.22 % (3441837)------------------------------ % 39.24/6.22 % (3441837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.24/6.22 % (3441837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.24/6.22 % (3441837)CaDiCaL version: 2.1.3 % 39.24/6.22 % (3441837)Termination reason: Refutation not found, incomplete strategy % 39.24/6.22 % (3441837)Time elapsed: 0.116 s % 39.24/6.22 % (3441837)Peak memory usage: 88 MB % 39.24/6.22 % (3441837)Instructions burned: 304 (million) % 39.24/6.22 % (3441831)Instruction limit reached! % 39.24/6.22 % (3441831)------------------------------ % 39.24/6.22 % (3441831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.24/6.22 % (3441831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.24/6.22 % (3441831)CaDiCaL version: 2.1.3 % 39.24/6.22 % (3441831)Termination reason: Instruction limit % 39.24/6.22 % (3441831)Termination phase: Saturation % 46.45/7.27 % (3441831)Time elapsed: 0.452 s % 46.45/7.27 % (3441831)Peak memory usage: 120 MB % 46.45/7.27 % (3441831)Instructions burned: 1133 (million) % 46.45/7.27 % (3441847)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=1420652959:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/868Mi) % 46.45/7.27 % (3441850)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=2059245597:i=1846:canc=cautious:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/1846Mi) % 46.45/7.27 % (3441837)------------------------------ % 46.45/7.27 % (3441837)------------------------------ % 46.45/7.27 % (3441851)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3272117098:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2956 on theBenchmark for (2956ds/36816Mi) % 46.45/7.27 % (3441796)Instruction limit reached! % 46.45/7.27 % (3441796)------------------------------ % 46.45/7.27 % (3441796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.45/7.27 % (3441796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.45/7.27 % (3441796)CaDiCaL version: 2.1.3 % 46.45/7.27 % (3441796)Termination reason: Instruction limit % 46.45/7.27 % (3441796)Termination phase: Saturation % 46.45/7.27 % (3441796)Time elapsed: 1.644 s % 46.45/7.27 % (3441796)Peak memory usage: 92 MB % 46.45/7.27 % (3441796)Instructions burned: 4429 (million) % 46.45/7.27 % (3441843)Instruction limit reached! % 46.45/7.27 % (3441843)------------------------------ % 46.45/7.27 % (3441843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.45/7.27 % (3441843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.45/7.27 % (3441843)CaDiCaL version: 2.1.3 % 46.45/7.27 % (3441843)Termination reason: Instruction limit % 46.45/7.27 % (3441843)Termination phase: Saturation % 46.45/7.27 % (3441843)Time elapsed: 0.411 s % 46.45/7.27 % (3441843)Peak memory usage: 95 MB % 46.45/7.27 % (3441843)Instructions burned: 1096 (million) % 46.45/7.27 % (3441854)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=656196247:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi) % 46.45/7.27 % (3441850)Refutation not found, incomplete strategy % 46.45/7.27 % (3441850)------------------------------ % 46.45/7.27 % (3441850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.45/7.27 % (3441850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.45/7.27 % (3441850)CaDiCaL version: 2.1.3 % 46.45/7.27 % (3441850)Termination reason: Refutation not found, incomplete strategy % 46.45/7.27 % (3441850)Time elapsed: 0.258 s % 46.45/7.27 % (3441850)Peak memory usage: 91 MB % 46.45/7.27 % (3441850)Instructions burned: 676 (million) % 46.45/7.27 % (3441847)Instruction limit reached! % 46.45/7.27 % (3441847)------------------------------ % 46.45/7.27 % (3441847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.45/7.27 % (3441847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.45/7.27 % (3441847)CaDiCaL version: 2.1.3 % 46.45/7.27 % (3441847)Termination reason: Instruction limit % 46.45/7.27 % (3441847)Termination phase: Saturation % 46.45/7.27 % (3441847)Time elapsed: 0.338 s % 46.45/7.27 % (3441847)Peak memory usage: 115 MB % 46.45/7.27 % (3441847)Instructions burned: 868 (million) % 46.45/7.27 % (3441857)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=913682779:i=5811:kws=precedence:nm=0:rtra=on_2953 on theBenchmark for (2953ds/5811Mi) % 46.45/7.27 % (3441856)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=2288740075:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/863Mi) % 46.45/7.27 % (3441854)Instruction limit reached! % 46.45/7.27 % (3441854)------------------------------ % 46.45/7.27 % (3441854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.45/7.27 % (3441854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.45/7.27 % (3441854)CaDiCaL version: 2.1.3 % 46.45/7.27 % (3441854)Termination reason: Instruction limit % 46.45/7.27 % (3441854)Termination phase: Property scanning % 46.45/7.27 % (3441854)Time elapsed: 0.108 s % 46.45/7.27 % (3441854)Peak memory usage: 86 MB % 46.45/7.27 % (3441854)Instructions burned: 273 (million) % 52.88/8.16 % (3441850)------------------------------ % 52.88/8.16 % (3441850)------------------------------ % 52.88/8.16 % (3441859)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=899770588:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 52.88/8.16 % (3441862)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=579606377:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2951 on theBenchmark for (2951ds/801Mi) % 52.88/8.16 % (3441863)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4040472976:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2950 on theBenchmark for (2950ds/1026Mi) % 52.88/8.16 % (3441863)Refutation not found, incomplete strategy % 52.88/8.16 % (3441863)------------------------------ % 52.88/8.16 % (3441863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.88/8.16 % (3441863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.88/8.16 % (3441863)CaDiCaL version: 2.1.3 % 52.88/8.16 % (3441863)Termination reason: Refutation not found, incomplete strategy % 52.88/8.16 % (3441863)Time elapsed: 0.037 s % 52.88/8.16 % (3441863)Peak memory usage: 88 MB % 52.88/8.16 % (3441863)Instructions burned: 181 (million) % 52.88/8.16 % (3441856)Instruction limit reached! % 52.88/8.16 % (3441856)------------------------------ % 52.88/8.16 % (3441856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.88/8.16 % (3441856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.88/8.16 % (3441856)CaDiCaL version: 2.1.3 % 52.88/8.16 % (3441856)Termination reason: Instruction limit % 52.88/8.16 % (3441856)Termination phase: Saturation % 52.88/8.16 % (3441856)Time elapsed: 0.335 s % 52.88/8.16 % (3441856)Peak memory usage: 115 MB % 52.88/8.16 % (3441856)Instructions burned: 863 (million) % 52.88/8.16 % (3441863)------------------------------ % 52.88/8.16 % (3441863)------------------------------ % 52.88/8.16 % (3441862)Instruction limit reached! % 52.88/8.16 % (3441862)------------------------------ % 52.88/8.16 % (3441862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.88/8.16 % (3441862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.88/8.16 % (3441862)CaDiCaL version: 2.1.3 % 52.88/8.16 % (3441862)Termination reason: Instruction limit % 52.88/8.16 % (3441862)Termination phase: Saturation % 52.88/8.16 % (3441862)Time elapsed: 0.300 s % 52.88/8.16 % (3441862)Peak memory usage: 92 MB % 52.88/8.16 % (3441862)Instructions burned: 802 (million) % 52.88/8.16 % (3441869)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3042895860:i=3509:rtra=on_2948 on theBenchmark for (2948ds/3509Mi) % 52.88/8.16 % (3441870)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3308290331:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2947 on theBenchmark for (2947ds/2127Mi) % 52.88/8.16 % (3441870)Refutation not found, incomplete strategy % 52.88/8.16 % (3441870)------------------------------ % 52.88/8.16 % (3441870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.88/8.16 % (3441870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.88/8.16 % (3441870)CaDiCaL version: 2.1.3 % 52.88/8.16 % (3441870)Termination reason: Refutation not found, incomplete strategy % 52.88/8.16 % (3441870)Time elapsed: 0.057 s % 52.88/8.16 % (3441870)Peak memory usage: 88 MB % 52.88/8.16 % (3441870)Instructions burned: 289 (million) % 52.88/8.16 % (3441874)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2329079029:i=1959:rtra=on:fsd=on:proc=on_2946 on theBenchmark for (2946ds/1959Mi) % 52.88/8.16 % (3441870)------------------------------ % 52.88/8.16 % (3441870)------------------------------ % 52.88/8.16 % (3441877)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2557417135:s2a=on:i=3553:nm=0:rtra=on_2943 on theBenchmark for (2943ds/3553Mi) % 52.88/8.16 % (3441859)Instruction limit reached! % 52.88/8.16 % (3441859)------------------------------ % 52.88/8.16 % (3441859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.88/8.16 % (3441859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.88/8.16 % (3441859)CaDiCaL version: 2.1.3 % 52.88/8.16 % (3441859)Termination reason: Instruction limit % 52.88/8.16 % (3441859)Termination phase: Saturation % 52.88/8.16 % (3441859)Time elapsed: 0.883 s % 52.88/8.16 % (3441859)Peak memory usage: 119 MB % 52.88/8.16 % (3441859)Instructions burned: 2216 (million) % 73.39/11.05 % (3441879)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1868871485:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2941 on theBenchmark for (2941ds/3201Mi) % 73.39/11.05 % (3441844)Instruction limit reached! % 73.39/11.05 % (3441844)------------------------------ % 73.39/11.05 % (3441844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.39/11.05 % (3441844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.39/11.05 % (3441844)CaDiCaL version: 2.1.3 % 73.39/11.05 % (3441844)Termination reason: Instruction limit % 73.39/11.05 % (3441844)Termination phase: Saturation % 73.39/11.05 % (3441844)Time elapsed: 2.052 s % 73.39/11.05 % (3441844)Peak memory usage: 91 MB % 73.39/11.05 % (3441844)Instructions burned: 6401 (million) % 73.39/11.05 % (3441874)Instruction limit reached! % 73.39/11.05 % (3441874)------------------------------ % 73.39/11.05 % (3441874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.39/11.05 % (3441874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.39/11.05 % (3441874)CaDiCaL version: 2.1.3 % 73.39/11.05 % (3441874)Termination reason: Instruction limit % 73.39/11.05 % (3441874)Termination phase: Saturation % 73.39/11.05 % (3441874)Time elapsed: 0.775 s % 73.39/11.05 % (3441874)Peak memory usage: 122 MB % 73.39/11.05 % (3441874)Instructions burned: 1961 (million) % 73.39/11.05 % (3441881)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=1277480860:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2936 on theBenchmark for (2936ds/4093Mi) % 73.39/11.05 % (3441882)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=1595682250:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2936 on theBenchmark for (2936ds/21173Mi) % 73.39/11.05 % (3441869)Instruction limit reached! % 73.39/11.05 % (3441869)------------------------------ % 73.39/11.05 % (3441869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.39/11.05 % (3441869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.39/11.05 % (3441869)CaDiCaL version: 2.1.3 % 73.39/11.05 % (3441869)Termination reason: Instruction limit % 73.39/11.05 % (3441869)Termination phase: Saturation % 73.39/11.05 % (3441869)Time elapsed: 1.254 s % 73.39/11.05 % (3441869)Peak memory usage: 92 MB % 73.39/11.05 % (3441869)Instructions burned: 3510 (million) % 73.39/11.05 % (3441882)Refutation not found, incomplete strategy % 73.39/11.05 % (3441882)------------------------------ % 73.39/11.05 % (3441882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.39/11.05 % (3441882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.39/11.05 % (3441882)CaDiCaL version: 2.1.3 % 73.39/11.05 % (3441882)Termination reason: Refutation not found, incomplete strategy % 73.39/11.05 % (3441882)Time elapsed: 0.080 s % 73.39/11.05 % (3441882)Peak memory usage: 113 MB % 73.39/11.05 % (3441882)Instructions burned: 147 (million) % 73.39/11.05 % (3441885)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=429589061:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2934 on theBenchmark for (2934ds/10544Mi) % 73.39/11.05 % (3441879)Refutation not found, incomplete strategy % 73.39/11.05 % (3441879)------------------------------ % 73.39/11.05 % (3441879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.39/11.05 % (3441879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.39/11.05 % (3441879)CaDiCaL version: 2.1.3 % 73.39/11.05 % (3441879)Termination reason: Refutation not found, incomplete strategy % 73.39/11.05 % (3441879)Time elapsed: 0.722 s % 73.39/11.05 % (3441879)Peak memory usage: 99 MB % 73.39/11.05 % (3441879)Instructions burned: 1828 (million) % 73.39/11.05 % (3441882)------------------------------ % 73.39/11.05 % (3441882)------------------------------ % 73.39/11.05 % (3441857)Instruction limit reached! % 73.39/11.05 % (3441857)------------------------------ % 73.39/11.05 % (3441857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.39/11.05 % (3441857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.39/11.05 % (3441857)CaDiCaL version: 2.1.3 % 73.39/11.05 % (3441857)Termination reason: Instruction limit % 73.39/11.05 % (3441857)Termination phase: Saturation % 73.39/11.05 % (3441857)Time elapsed: 2.106 s % 73.39/11.05 % (3441857)Peak memory usage: 124 MB % 84.05/12.65 % (3441857)Instructions burned: 5812 (million) % 84.05/12.65 % (3441879)------------------------------ % 84.05/12.65 % (3441879)------------------------------ % 84.05/12.65 % (3441887)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3173132400:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2931 on theBenchmark for (2931ds/1262Mi) % 84.05/12.65 % (3441890)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3595666387:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2930 on theBenchmark for (2930ds/775Mi) % 84.05/12.65 % (3441877)Instruction limit reached! % 84.05/12.65 % (3441877)------------------------------ % 84.05/12.65 % (3441877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.05/12.65 % (3441877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.05/12.65 % (3441877)CaDiCaL version: 2.1.3 % 84.05/12.65 % (3441877)Termination reason: Instruction limit % 84.05/12.65 % (3441877)Termination phase: Saturation % 84.05/12.65 % (3441877)Time elapsed: 1.341 s % 84.05/12.65 % (3441877)Peak memory usage: 93 MB % 84.05/12.65 % (3441877)Instructions burned: 3553 (million) % 84.05/12.65 % (3441890)Refutation not found, incomplete strategy % 84.05/12.65 % (3441890)------------------------------ % 84.05/12.65 % (3441890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.05/12.65 % (3441890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.05/12.65 % (3441890)CaDiCaL version: 2.1.3 % 84.05/12.65 % (3441890)Termination reason: Refutation not found, incomplete strategy % 84.05/12.65 % (3441890)Time elapsed: 0.118 s % 84.05/12.65 % (3441890)Peak memory usage: 88 MB % 84.05/12.65 % (3441890)Instructions burned: 304 (million) % 84.05/12.65 % (3441891)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=30316362:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2929 on theBenchmark for (2929ds/270Mi) % 84.05/12.65 % (3441894)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=471946820:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2927 on theBenchmark for (2927ds/17165Mi) % 84.05/12.65 % (3441891)Instruction limit reached! % 84.05/12.65 % (3441891)------------------------------ % 84.05/12.65 % (3441891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.05/12.65 % (3441891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.05/12.65 % (3441891)CaDiCaL version: 2.1.3 % 84.05/12.65 % (3441891)Termination reason: Instruction limit % 84.05/12.65 % (3441891)Termination phase: Property scanning % 84.05/12.65 % (3441891)Time elapsed: 0.108 s % 84.05/12.65 % (3441891)Peak memory usage: 86 MB % 84.05/12.65 % (3441891)Instructions burned: 271 (million) % 84.05/12.65 % (3441890)------------------------------ % 84.05/12.65 % (3441890)------------------------------ % 84.05/12.65 % (3441887)Instruction limit reached! % 84.05/12.65 % (3441887)------------------------------ % 84.05/12.65 % (3441887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.05/12.65 % (3441887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.05/12.65 % (3441887)CaDiCaL version: 2.1.3 % 84.05/12.65 % (3441887)Termination reason: Instruction limit % 84.05/12.65 % (3441887)Termination phase: Saturation % 84.05/12.65 % (3441887)Time elapsed: 0.505 s % 84.05/12.65 % (3441887)Peak memory usage: 116 MB % 84.05/12.65 % (3441887)Instructions burned: 1264 (million) % 84.05/12.65 % (3441897)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=225168357:s2a=on:i=13094:s2at=-1:rtra=on_2926 on theBenchmark for (2926ds/13094Mi) % 84.05/12.65 % (3441898)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2343102651:st=2:i=12633:rtra=on:ss=axioms_2925 on theBenchmark for (2925ds/12633Mi) % 84.05/12.65 % (3441900)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3086812828:i=1783:rtra=on:gtg=position_2924 on theBenchmark for (2924ds/1783Mi) % 84.05/12.65 % (3441898)Refutation not found, incomplete strategy % 84.05/12.65 % (3441898)------------------------------ % 84.05/12.65 % (3441898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.05/12.65 % (3441898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.05/12.65 % (3441898)CaDiCaL version: 2.1.3 % 84.05/12.65 % (3441898)Termination reason: Refutation not found, incomplete strategy % 84.05/12.65 % (3441898)Time elapsed: 0.105 s % 84.05/12.65 % (3441898)Peak memory usage: 88 MB % 95.49/14.24 % (3441898)Instructions burned: 257 (million) % 95.49/14.24 % (3441898)------------------------------ % 95.49/14.24 % (3441898)------------------------------ % 95.49/14.24 % (3441881)Instruction limit reached! % 95.49/14.24 % (3441881)------------------------------ % 95.49/14.24 % (3441881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.49/14.24 % (3441881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.49/14.24 % (3441881)CaDiCaL version: 2.1.3 % 95.49/14.24 % (3441881)Termination reason: Instruction limit % 95.49/14.24 % (3441881)Termination phase: Saturation % 95.49/14.24 % (3441881)Time elapsed: 1.586 s % 95.49/14.24 % (3441881)Peak memory usage: 136 MB % 95.49/14.24 % (3441881)Instructions burned: 4093 (million) % 95.49/14.24 % (3441903)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=2693870350:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2919 on theBenchmark for (2919ds/5451Mi) % 95.49/14.24 % (3441904)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=1365963514:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2919 on theBenchmark for (2919ds/4975Mi) % 95.49/14.24 % (3441900)Instruction limit reached! % 95.49/14.24 % (3441900)------------------------------ % 95.49/14.24 % (3441900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.49/14.24 % (3441900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.49/14.24 % (3441900)CaDiCaL version: 2.1.3 % 95.49/14.24 % (3441900)Termination reason: Instruction limit % 95.49/14.24 % (3441900)Termination phase: Saturation % 95.49/14.24 % (3441900)Time elapsed: 0.700 s % 95.49/14.24 % (3441900)Peak memory usage: 113 MB % 95.49/14.24 % (3441900)Instructions burned: 1785 (million) % 95.49/14.24 % (3441907)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=1144989586:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2914 on theBenchmark for (2914ds/2076Mi) % 95.49/14.24 % (3441907)Instruction limit reached! % 95.49/14.24 % (3441907)------------------------------ % 95.49/14.24 % (3441907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.49/14.24 % (3441907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.49/14.24 % (3441907)CaDiCaL version: 2.1.3 % 95.49/14.24 % (3441907)Termination reason: Instruction limit % 95.49/14.24 % (3441907)Termination phase: Saturation % 95.49/14.24 % (3441907)Time elapsed: 0.824 s % 95.49/14.24 % (3441907)Peak memory usage: 116 MB % 95.49/14.24 % (3441907)Instructions burned: 2078 (million) % 95.49/14.24 % (3441911)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2725600886:i=5145:rtra=on_2905 on theBenchmark for (2905ds/5145Mi) % 95.49/14.24 % (3441903)Instruction limit reached! % 95.49/14.24 % (3441903)------------------------------ % 95.49/14.24 % (3441903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.49/14.24 % (3441903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.49/14.24 % (3441903)CaDiCaL version: 2.1.3 % 95.49/14.24 % (3441903)Termination reason: Instruction limit % 95.49/14.24 % (3441903)Termination phase: Saturation % 95.49/14.24 % (3441903)Time elapsed: 2.109 s % 95.49/14.24 % (3441903)Peak memory usage: 125 MB % 95.49/14.24 % (3441903)Instructions burned: 5452 (million) % 95.49/14.24 % (3441904)Instruction limit reached! % 95.49/14.24 % (3441904)------------------------------ % 95.49/14.24 % (3441904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.49/14.24 % (3441904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.49/14.24 % (3441904)CaDiCaL version: 2.1.3 % 95.49/14.24 % (3441904)Termination reason: Instruction limit % 95.49/14.24 % (3441904)Termination phase: Saturation % 95.49/14.24 % (3441904)Time elapsed: 2.252 s % 95.49/14.24 % (3441904)Peak memory usage: 163 MB % 95.49/14.24 % (3441904)Instructions burned: 4976 (million) % 95.49/14.24 % (3441915)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1752091138:i=3509:rtra=on_2896 on theBenchmark for (2896ds/3509Mi) % 95.49/14.24 % (3441916)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2749599550:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2895 on theBenchmark for (2895ds/13800Mi) % 95.49/14.24 % (3441916)Refutation not found, incomplete strategy % 95.49/14.24 % (3441916)------------------------------ % 95.49/14.24 % (3441916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.19/23.25 % (3441916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.19/23.25 % (3441916)CaDiCaL version: 2.1.3 % 159.19/23.25 % (3441916)Termination reason: Refutation not found, incomplete strategy % 159.19/23.25 % (3441916)Time elapsed: 0.061 s % 159.19/23.25 % (3441916)Peak memory usage: 88 MB % 159.19/23.25 % (3441916)Instructions burned: 289 (million) % 159.19/23.25 % (3441916)------------------------------ % 159.19/23.25 % (3441916)------------------------------ % 159.19/23.25 % (3441921)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1332521233:i=1412:rtra=on:fsd=on:proc=on_2890 on theBenchmark for (2890ds/1412Mi) % 159.19/23.25 % (3441885)Instruction limit reached! % 159.19/23.25 % (3441885)------------------------------ % 159.19/23.25 % (3441885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.19/23.25 % (3441885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.19/23.25 % (3441885)CaDiCaL version: 2.1.3 % 159.19/23.25 % (3441885)Termination reason: Instruction limit % 159.19/23.25 % (3441885)Termination phase: Saturation % 159.19/23.25 % (3441885)Time elapsed: 4.268 s % 159.19/23.25 % (3441885)Peak memory usage: 169 MB % 159.19/23.25 % (3441885)Instructions burned: 10546 (million) % 159.19/23.25 % (3441923)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 % 159.19/23.25 % (3441923)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1494861186:i=11747:aac=none:nm=0:rtra=on:rawr=on_2889 on theBenchmark for (2889ds/11747Mi) % 159.19/23.25 % (3441911)Instruction limit reached! % 159.19/23.25 % (3441911)------------------------------ % 159.19/23.25 % (3441911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.19/23.25 % (3441911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.19/23.25 % (3441911)CaDiCaL version: 2.1.3 % 159.19/23.25 % (3441911)Termination reason: Instruction limit % 159.19/23.25 % (3441911)Termination phase: Saturation % 159.19/23.25 % (3441911)Time elapsed: 1.872 s % 159.19/23.25 % (3441911)Peak memory usage: 95 MB % 159.19/23.25 % (3441911)Instructions burned: 5148 (million) % 159.19/23.25 % (3441921)Instruction limit reached! % 159.19/23.25 % (3441921)------------------------------ % 159.19/23.25 % (3441921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.19/23.25 % (3441921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.19/23.25 % (3441921)CaDiCaL version: 2.1.3 % 159.19/23.25 % (3441921)Termination reason: Instruction limit % 159.19/23.25 % (3441921)Termination phase: Saturation % 159.19/23.25 % (3441921)Time elapsed: 0.457 s % 159.19/23.25 % (3441921)Peak memory usage: 116 MB % 159.19/23.25 % (3441921)Instructions burned: 1414 (million) % 159.19/23.25 % (3441926)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=575389288:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2884 on theBenchmark for (2884ds/3201Mi) % 159.19/23.25 % (3441925)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2211627751:s2a=on:i=3553:nm=0:rtra=on_2884 on theBenchmark for (2884ds/3553Mi) % 159.19/23.25 % (3441915)Instruction limit reached! % 159.19/23.25 % (3441915)------------------------------ % 159.19/23.25 % (3441915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.19/23.25 % (3441915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.19/23.25 % (3441915)CaDiCaL version: 2.1.3 % 159.19/23.25 % (3441915)Termination reason: Instruction limit % 159.19/23.25 % (3441915)Termination phase: Saturation % 159.19/23.25 % (3441915)Time elapsed: 1.311 s % 159.19/23.25 % (3441915)Peak memory usage: 94 MB % 159.19/23.25 % (3441915)Instructions burned: 3511 (million) % 159.19/23.25 % (3441929)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=834689434:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2881 on theBenchmark for (2881ds/4081Mi) % 159.19/23.25 % (3441897)Instruction limit reached! % 159.19/23.25 % (3441897)------------------------------ % 159.19/23.25 % (3441897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.19/23.25 % (3441897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.19/23.25 % (3441897)CaDiCaL version: 2.1.3 % 159.19/23.25 % (3441897)Termination reason: Instruction limit % 173.84/25.37 % (3441897)Termination phase: Saturation % 173.84/25.37 % (3441897)Time elapsed: 4.712 s % 173.84/25.37 % (3441897)Peak memory usage: 97 MB % 173.84/25.37 % (3441897)Instructions burned: 13094 (million) % 173.84/25.37 % (3441926)Refutation not found, incomplete strategy % 173.84/25.37 % (3441926)------------------------------ % 173.84/25.37 % (3441926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.84/25.37 % (3441926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.84/25.37 % (3441926)CaDiCaL version: 2.1.3 % 173.84/25.37 % (3441926)Termination reason: Refutation not found, incomplete strategy % 173.84/25.37 % (3441926)Time elapsed: 0.680 s % 173.84/25.37 % (3441926)Peak memory usage: 99 MB % 173.84/25.37 % (3441926)Instructions burned: 1824 (million) % 173.84/25.37 % (3441935)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=422873618:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2876 on theBenchmark for (2876ds/20260Mi) % 173.84/25.37 % (3441935)Refutation not found, incomplete strategy % 173.84/25.37 % (3441935)------------------------------ % 173.84/25.37 % (3441935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.84/25.37 % (3441935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.84/25.37 % (3441935)CaDiCaL version: 2.1.3 % 173.84/25.37 % (3441935)Termination reason: Refutation not found, incomplete strategy % 173.84/25.37 % (3441935)Time elapsed: 0.080 s % 173.84/25.37 % (3441935)Peak memory usage: 113 MB % 173.84/25.37 % (3441935)Instructions burned: 147 (million) % 173.84/25.37 % (3441926)------------------------------ % 173.84/25.37 % (3441926)------------------------------ % 173.84/25.37 % (3441935)------------------------------ % 173.84/25.37 % (3441935)------------------------------ % 173.84/25.37 % (3441937)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3311467832:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2873 on theBenchmark for (2873ds/58627Mi) % 173.84/25.37 % (3441940)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=216395772:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2871 on theBenchmark for (2871ds/6258Mi) % 173.84/25.37 % (3441925)Instruction limit reached! % 173.84/25.37 % (3441925)------------------------------ % 173.84/25.37 % (3441925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.84/25.37 % (3441925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.84/25.37 % (3441925)CaDiCaL version: 2.1.3 % 173.84/25.37 % (3441925)Termination reason: Instruction limit % 173.84/25.37 % (3441925)Termination phase: Saturation % 173.84/25.37 % (3441925)Time elapsed: 1.346 s % 173.84/25.37 % (3441925)Peak memory usage: 93 MB % 173.84/25.37 % (3441925)Instructions burned: 3554 (million) % 173.84/25.37 % (3441945)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3882267102:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2868 on theBenchmark for (2868ds/34001Mi) % 173.84/25.37 % (3441894)Instruction limit reached! % 173.84/25.37 % (3441894)------------------------------ % 173.84/25.37 % (3441894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.84/25.37 % (3441894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.84/25.37 % (3441894)CaDiCaL version: 2.1.3 % 173.84/25.37 % (3441894)Termination reason: Instruction limit % 173.84/25.37 % (3441894)Termination phase: Saturation % 173.84/25.37 % (3441894)Time elapsed: 5.999 s % 173.84/25.37 % (3441894)Peak memory usage: 93 MB % 173.84/25.37 % (3441894)Instructions burned: 17166 (million) % 173.84/25.37 % (3441949)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=909958253:s2a=on:i=71622:s2at=-1:rtra=on_2866 on theBenchmark for (2866ds/71622Mi) % 173.84/25.37 % (3441929)Instruction limit reached! % 173.84/25.37 % (3441929)------------------------------ % 173.84/25.37 % (3441929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.84/25.37 % (3441929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.84/25.37 % (3441929)CaDiCaL version: 2.1.3 % 173.84/25.37 % (3441929)Termination reason: Instruction limit % 173.84/25.37 % (3441929)Termination phase: Saturation % 173.84/25.37 % (3441929)Time elapsed: 1.561 s % 173.84/25.37 % (3441929)Peak memory usage: 134 MB % 173.84/25.37 % (3441929)Instructions burned: 4082 (million) % 173.84/25.37 % (3441955)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3905120605:i=24001:kws=precedence:nm=0:rtra=on_2863 on theBenchmark for (2863ds/24001Mi) % 211.94/30.76 % (3441940)Instruction limit reached! % 211.94/30.76 % (3441940)------------------------------ % 211.94/30.76 % (3441940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.94/30.76 % (3441940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.94/30.76 % (3441940)CaDiCaL version: 2.1.3 % 211.94/30.76 % (3441940)Termination reason: Instruction limit % 211.94/30.76 % (3441940)Termination phase: Saturation % 211.94/30.76 % (3441940)Time elapsed: 2.411 s % 211.94/30.76 % (3441940)Peak memory usage: 128 MB % 211.94/30.76 % (3441940)Instructions burned: 6260 (million) % 211.94/30.76 % (3441923)Instruction limit reached! % 211.94/30.76 % (3441923)------------------------------ % 211.94/30.76 % (3441923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.94/30.76 % (3441923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.94/30.76 % (3441923)CaDiCaL version: 2.1.3 % 211.94/30.76 % (3441923)Termination reason: Instruction limit % 211.94/30.76 % (3441923)Termination phase: Saturation % 211.94/30.76 % (3441923)Time elapsed: 4.313 s % 211.94/30.76 % (3441923)Peak memory usage: 126 MB % 211.94/30.76 % (3441923)Instructions burned: 11747 (million) % 211.94/30.76 % (3441961)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=2100315012:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2845 on theBenchmark for (2845ds/2076Mi) % 211.94/30.76 % (3441962)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=2433631842:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2843 on theBenchmark for (2843ds/83971Mi) % 211.94/30.76 % (3441961)Instruction limit reached! % 211.94/30.76 % (3441961)------------------------------ % 211.94/30.76 % (3441961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.94/30.76 % (3441961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.94/30.76 % (3441961)CaDiCaL version: 2.1.3 % 211.94/30.76 % (3441961)Termination reason: Instruction limit % 211.94/30.76 % (3441961)Termination phase: Saturation % 211.94/30.76 % (3441961)Time elapsed: 0.830 s % 211.94/30.76 % (3441961)Peak memory usage: 116 MB % 211.94/30.76 % (3441961)Instructions burned: 2078 (million) % 211.94/30.76 % (3441967)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=420906586:i=83944:rtra=on_2834 on theBenchmark for (2834ds/83944Mi) % 211.94/30.76 % (3441851)Instruction limit reached! % 211.94/30.76 % (3441851)------------------------------ % 211.94/30.76 % (3441851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.94/30.76 % (3441851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.94/30.76 % (3441851)CaDiCaL version: 2.1.3 % 211.94/30.76 % (3441851)Termination reason: Instruction limit % 211.94/30.76 % (3441851)Termination phase: Saturation % 211.94/30.76 % (3441851)Time elapsed: 13.756 s % 211.94/30.76 % (3441851)Peak memory usage: 118 MB % 211.94/30.76 % (3441851)Instructions burned: 36817 (million) % 211.94/30.76 % (3441985)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2592065928:i=9201:rtra=on_2816 on theBenchmark for (2816ds/9201Mi) % 211.94/30.76 % (3441985)Instruction limit reached! % 211.94/30.76 % (3441985)------------------------------ % 211.94/30.76 % (3441985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.94/30.76 % (3441985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.94/30.76 % (3441985)CaDiCaL version: 2.1.3 % 211.94/30.76 % (3441985)Termination reason: Instruction limit % 211.94/30.76 % (3441985)Termination phase: Saturation % 211.94/30.76 % (3441985)Time elapsed: 2.750 s % 211.94/30.76 % (3441985)Peak memory usage: 92 MB % 211.94/30.76 % (3441985)Instructions burned: 9204 (million) % 211.94/30.76 % (3442003)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 % 211.94/30.76 % (3442003)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=705315070:i=6806:aac=none:nm=0:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/6806Mi) % 211.94/30.76 % (3441955)Instruction limit reached! % 211.94/30.76 % (3441955)------------------------------ % 211.94/30.76 % (3441955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.94/30.76 % (3441955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.94/30.76 % (3441955)CaDiCaL version: 2.1.3 % 221.88/32.14 % (3441955)Termination reason: Instruction limit % 221.88/32.14 % (3441955)Termination phase: Saturation % 221.88/32.14 % (3441955)Time elapsed: 9.012 s % 221.88/32.14 % (3441955)Peak memory usage: 144 MB % 221.88/32.14 % (3441955)Instructions burned: 24002 (million) % 221.88/32.14 % (3442011)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2430899554:s2a=on:i=3553:nm=0:rtra=on_2770 on theBenchmark for (2770ds/3553Mi) % 221.88/32.14 % (3442003)Instruction limit reached! % 221.88/32.14 % (3442003)------------------------------ % 221.88/32.14 % (3442003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.88/32.14 % (3442003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.88/32.14 % (3442003)CaDiCaL version: 2.1.3 % 221.88/32.14 % (3442003)Termination reason: Instruction limit % 221.88/32.14 % (3442003)Termination phase: Saturation % 221.88/32.14 % (3442003)Time elapsed: 2.380 s % 221.88/32.14 % (3442003)Peak memory usage: 125 MB % 221.88/32.14 % (3442003)Instructions burned: 6807 (million) % 221.88/32.14 % (3442015)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=1250372015:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2762 on theBenchmark for (2762ds/2064Mi) % 221.88/32.14 % (3442011)Instruction limit reached! % 221.88/32.14 % (3442011)------------------------------ % 221.88/32.14 % (3442011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.88/32.14 % (3442011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.88/32.14 % (3442011)CaDiCaL version: 2.1.3 % 221.88/32.14 % (3442011)Termination reason: Instruction limit % 221.88/32.14 % (3442011)Termination phase: Saturation % 221.88/32.14 % (3442011)Time elapsed: 1.288 s % 221.88/32.14 % (3442011)Peak memory usage: 96 MB % 221.88/32.14 % (3442011)Instructions burned: 3555 (million) % 221.88/32.14 % (3442015)Instruction limit reached! % 221.88/32.14 % (3442015)------------------------------ % 221.88/32.14 % (3442015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.88/32.14 % (3442015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.88/32.14 % (3442015)CaDiCaL version: 2.1.3 % 221.88/32.14 % (3442015)Termination reason: Instruction limit % 221.88/32.14 % (3442015)Termination phase: Saturation % 221.88/32.14 % (3442015)Time elapsed: 0.636 s % 221.88/32.14 % (3442015)Peak memory usage: 133 MB % 221.88/32.14 % (3442015)Instructions burned: 2065 (million) % 221.88/32.14 % (3442021)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=2651033350:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2755 on theBenchmark for (2755ds/20260Mi) % 221.88/32.14 % (3442022)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=772290880:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/1244Mi) % 221.88/32.14 % (3442021)Refutation not found, incomplete strategy % 221.88/32.14 % (3442021)------------------------------ % 221.88/32.14 % (3442021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.88/32.14 % (3442021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.88/32.14 % (3442021)CaDiCaL version: 2.1.3 % 221.88/32.14 % (3442021)Termination reason: Refutation not found, incomplete strategy % 221.88/32.14 % (3442021)Time elapsed: 0.078 s % 221.88/32.14 % (3442021)Peak memory usage: 113 MB % 221.88/32.14 % (3442021)Instructions burned: 147 (million) % 221.88/32.14 % (3441945)Instruction limit reached! % 221.88/32.14 % (3441945)------------------------------ % 221.88/32.14 % (3441945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.88/32.14 % (3441945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.88/32.14 % (3441945)CaDiCaL version: 2.1.3 % 221.88/32.14 % (3441945)Termination reason: Instruction limit % 221.88/32.14 % (3441945)Termination phase: Saturation % 221.88/32.14 % (3441945)Time elapsed: 11.499 s % 221.88/32.14 % (3441945)Peak memory usage: 92 MB % 221.88/32.14 % (3441945)Instructions burned: 34001 (million) % 221.88/32.14 % (3442021)------------------------------ % 221.88/32.14 % (3442021)------------------------------ % 221.88/32.14 % (3442027)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=1483403576:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2752 on theBenchmark for (2752ds/58261Mi) % 221.88/32.14 % (3442022)Instruction limit reached! % 221.88/32.14 % (3442022)------------------------------ % 229.27/33.21 % (3442022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.27/33.21 % (3442022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.27/33.21 % (3442022)CaDiCaL version: 2.1.3 % 229.27/33.21 % (3442022)Termination reason: Instruction limit % 229.27/33.21 % (3442022)Termination phase: Saturation % 229.27/33.21 % (3442022)Time elapsed: 0.302 s % 229.27/33.21 % (3442022)Peak memory usage: 116 MB % 229.27/33.21 % (3442022)Instructions burned: 1247 (million) % 229.27/33.21 % (3442030)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=3246933060:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2749 on theBenchmark for (2749ds/4081Mi) % 229.27/33.21 % (3442028)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 % 229.27/33.21 % (3442028)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1856593074:i=6806:aac=none:nm=0:rtra=on:rawr=on_2750 on theBenchmark for (2750ds/6806Mi) % 229.27/33.21 % (3442030)Instruction limit reached! % 229.27/33.21 % (3442030)------------------------------ % 229.27/33.21 % (3442030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.27/33.21 % (3442030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.27/33.21 % (3442030)CaDiCaL version: 2.1.3 % 229.27/33.21 % (3442030)Termination reason: Instruction limit % 229.27/33.21 % (3442030)Termination phase: Saturation % 229.27/33.21 % (3442030)Time elapsed: 1.316 s % 229.27/33.21 % (3442030)Peak memory usage: 134 MB % 229.27/33.21 % (3442030)Instructions burned: 4081 (million) % 229.27/33.21 % (3442037)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2560015268:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2735 on theBenchmark for (2735ds/1701Mi) % 229.27/33.21 % (3442028)Instruction limit reached! % 229.27/33.21 % (3442028)------------------------------ % 229.27/33.21 % (3442028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.27/33.21 % (3442028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.27/33.21 % (3442028)CaDiCaL version: 2.1.3 % 229.27/33.21 % (3442028)Termination reason: Instruction limit % 229.27/33.21 % (3442028)Termination phase: Saturation % 229.27/33.21 % (3442028)Time elapsed: 1.988 s % 229.27/33.21 % (3442028)Peak memory usage: 125 MB % 229.27/33.21 % (3442028)Instructions burned: 6806 (million) % 229.27/33.21 % (3442039)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=3565519318:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2728 on theBenchmark for (2728ds/57001Mi) % 229.27/33.21 % (3442037)Instruction limit reached! % 229.27/33.21 % (3442037)------------------------------ % 229.27/33.21 % (3442037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.27/33.21 % (3442037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.27/33.21 % (3442037)CaDiCaL version: 2.1.3 % 229.27/33.21 % (3442037)Termination reason: Instruction limit % 229.27/33.21 % (3442037)Termination phase: Saturation % 229.27/33.21 % (3442037)Time elapsed: 0.675 s % 229.27/33.21 % (3442037)Peak memory usage: 116 MB % 229.27/33.21 % (3442037)Instructions burned: 1701 (million) % 229.27/33.21 % (3442041)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 % 229.27/33.21 % (3442041)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2909798877:i=8622:aac=none:nm=0:rtra=on:rawr=on_2726 on theBenchmark for (2726ds/8622Mi) % 229.27/33.21 % (3442041)Instruction limit reached! % 229.27/33.21 % (3442041)------------------------------ % 229.27/33.21 % (3442041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.27/33.21 % (3442041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.27/33.21 % (3442041)CaDiCaL version: 2.1.3 % 229.27/33.21 % (3442041)Termination reason: Instruction limit % 229.27/33.21 % (3442041)Termination phase: Saturation % 229.27/33.21 % (3442041)Time elapsed: 2.750 s % 229.27/33.21 % (3442041)Peak memory usage: 126 MB % 229.27/33.21 % (3442041)Instructions burned: 8625 (million) % 229.27/33.21 % (3442047)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1856747167:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2697 on theBenchmark for (2697ds/24Mi) % 239.10/34.60 % (3442047)Instruction limit reached! % 239.10/34.60 % (3442047)------------------------------ % 239.10/34.60 % (3442047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.10/34.60 % (3442047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.10/34.60 % (3442047)CaDiCaL version: 2.1.3 % 239.10/34.60 % (3442047)Termination reason: Instruction limit % 239.10/34.60 % (3442047)Termination phase: Property scanning % 239.10/34.60 % (3442047)Time elapsed: 0.011 s % 239.10/34.60 % (3442047)Peak memory usage: 85 MB % 239.10/34.60 % (3442047)Instructions burned: 25 (million) % 239.10/34.60 % (3442049)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2212984648:i=614:kws=precedence:nm=0:rtra=on_2695 on theBenchmark for (2695ds/614Mi) % 239.10/34.60 % (3442049)Instruction limit reached! % 239.10/34.60 % (3442049)------------------------------ % 239.10/34.60 % (3442049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.10/34.60 % (3442049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.10/34.60 % (3442049)CaDiCaL version: 2.1.3 % 239.10/34.60 % (3442049)Termination reason: Instruction limit % 239.10/34.60 % (3442049)Termination phase: Saturation % 239.10/34.60 % (3442049)Time elapsed: 0.249 s % 239.10/34.60 % (3442049)Peak memory usage: 113 MB % 239.10/34.60 % (3442049)Instructions burned: 615 (million) % 239.10/34.60 % (3442055)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=455311695:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2691 on theBenchmark for (2691ds/402Mi) % 239.10/34.60 % (3442055)Instruction limit reached! % 239.10/34.60 % (3442055)------------------------------ % 239.10/34.60 % (3442055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.10/34.60 % (3442055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.10/34.60 % (3442055)CaDiCaL version: 2.1.3 % 239.10/34.60 % (3442055)Termination reason: Instruction limit % 239.10/34.60 % (3442055)Termination phase: Property scanning % 239.10/34.60 % (3442055)Time elapsed: 0.088 s % 239.10/34.60 % (3442055)Peak memory usage: 86 MB % 239.10/34.60 % (3442055)Instructions burned: 405 (million) % 239.10/34.60 % (3442057)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3456963969:s2a=on:i=14:rtra=on:inst=on_2688 on theBenchmark for (2688ds/14Mi) % 239.10/34.60 % (3442057)Instruction limit reached! % 239.10/34.60 % (3442057)------------------------------ % 239.10/34.60 % (3442057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.10/34.60 % (3442057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.10/34.60 % (3442057)CaDiCaL version: 2.1.3 % 239.10/34.60 % (3442057)Termination reason: Instruction limit % 239.10/34.60 % (3442057)Termination phase: shuffling % 239.10/34.60 % (3442057)Time elapsed: 0.005 s % 239.10/34.60 % (3442057)Peak memory usage: 85 MB % 239.10/34.60 % (3442057)Instructions burned: 16 (million) % 239.10/34.60 % (3442063)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2551440516:i=8:rtra=on_2686 on theBenchmark for (2686ds/8Mi) % 239.10/34.60 % (3442063)Instruction limit reached! % 239.10/34.60 % (3442063)------------------------------ % 239.10/34.60 % (3442063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.10/34.60 % (3442063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.10/34.60 % (3442063)CaDiCaL version: 2.1.3 % 239.10/34.60 % (3442063)Termination reason: Instruction limit % 239.10/34.60 % (3442063)Termination phase: shuffling % 239.10/34.60 % (3442063)Time elapsed: 0.002 s % 239.10/34.60 % (3442063)Peak memory usage: 85 MB % 239.10/34.60 % (3442063)Instructions burned: 8 (million) % 239.10/34.60 % (3442065)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2963940221:i=92:rtra=on_2684 on theBenchmark for (2684ds/92Mi) % 239.10/34.60 % (3442065)Instruction limit reached! % 239.10/34.60 % (3442065)------------------------------ % 239.10/34.60 % (3442065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.10/34.60 % (3442065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.10/34.60 % (3442065)CaDiCaL version: 2.1.3 % 239.10/34.60 % (3442065)Termination reason: Instruction limit % 239.10/34.60 % (3442065)Termination phase: Property scanning % 239.10/34.60 % (3442065)Time elapsed: 0.038 s % 239.10/34.60 % (3442065)Peak memory usage: 85 MB % 239.10/34.60 % (3442065)Instructions burned: 93 (million) % 243.03/35.28 % (3442067)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=211671105:i=66:rtra=on_2682 on theBenchmark for (2682ds/66Mi) % 243.03/35.28 % (3442067)Instruction limit reached! % 243.03/35.28 % (3442067)------------------------------ % 243.03/35.28 % (3442067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.03/35.28 % (3442067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.03/35.28 % (3442067)CaDiCaL version: 2.1.3 % 243.03/35.28 % (3442067)Termination reason: Instruction limit % 243.03/35.28 % (3442067)Termination phase: Property scanning % 243.03/35.28 % (3442067)Time elapsed: 0.016 s % 243.03/35.28 % (3442067)Peak memory usage: 86 MB % 243.03/35.28 % (3442067)Instructions burned: 67 (million) % 243.03/35.28 % (3442069)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=475200594:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2680 on theBenchmark for (2680ds/28Mi) % 243.03/35.28 % (3442069)Instruction limit reached! % 243.03/35.28 % (3442069)------------------------------ % 243.03/35.28 % (3442069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.03/35.28 % (3442069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.03/35.28 % (3442069)CaDiCaL version: 2.1.3 % 243.03/35.28 % (3442069)Termination reason: Instruction limit % 243.03/35.28 % (3442069)Termination phase: Property scanning % 243.03/35.28 % (3442069)Time elapsed: 0.007 s % 243.03/35.28 % (3442069)Peak memory usage: 85 MB % 243.03/35.28 % (3442069)Instructions burned: 32 (million) % 243.03/35.28 % (3442071)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=3274602766:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2679 on theBenchmark for (2679ds/58Mi) % 243.03/35.28 % (3442071)Instruction limit reached! % 243.03/35.28 % (3442071)------------------------------ % 243.03/35.28 % (3442071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.03/35.28 % (3442071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.03/35.28 % (3442071)CaDiCaL version: 2.1.3 % 243.03/35.28 % (3442071)Termination reason: Instruction limit % 243.03/35.28 % (3442071)Termination phase: Property scanning % 243.03/35.28 % (3442071)Time elapsed: 0.024 s % 243.03/35.28 % (3442071)Peak memory usage: 86 MB % 243.03/35.28 % (3442071)Instructions burned: 59 (million) % 243.03/35.28 % (3442073)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3743406374:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2676 on theBenchmark for (2676ds/32Mi) % 243.03/35.28 % (3442073)Instruction limit reached! % 243.03/35.28 % (3442073)------------------------------ % 243.03/35.28 % (3442073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.03/35.28 % (3442073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.03/35.28 % (3442073)CaDiCaL version: 2.1.3 % 243.03/35.28 % (3442073)Termination reason: Instruction limit % 243.03/35.28 % (3442073)Termination phase: Property scanning % 243.03/35.28 % (3442073)Time elapsed: 0.009 s % 243.03/35.28 % (3442073)Peak memory usage: 85 MB % 243.03/35.28 % (3442073)Instructions burned: 36 (million) % 243.03/35.28 % (3442075)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1631336345:i=48:canc=force:rtra=on_2675 on theBenchmark for (2675ds/48Mi) % 243.03/35.28 % (3442075)Instruction limit reached! % 243.03/35.28 % (3442075)------------------------------ % 243.03/35.28 % (3442075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.03/35.28 % (3442075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.03/35.28 % (3442075)CaDiCaL version: 2.1.3 % 243.03/35.28 % (3442075)Termination reason: Instruction limit % 243.03/35.28 % (3442075)Termination phase: Property scanning % 243.03/35.28 % (3442075)Time elapsed: 0.020 s % 243.03/35.28 % (3442075)Peak memory usage: 86 MB % 243.03/35.28 % (3442075)Instructions burned: 49 (million) % 243.03/35.28 % (3442081)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=573850274:i=54:canc=cautious:fsr=off:rtra=on_2672 on theBenchmark for (2672ds/54Mi) % 243.03/35.28 % (3442081)Instruction limit reached! % 243.03/35.28 % (3442081)------------------------------ % 243.03/35.28 % (3442081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.03/35.28 % (3442081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.03/35.28 % (3442081)CaDiCaL version: 2.1.3 % 247.85/35.95 % (3442081)Termination reason: Instruction limit % 247.85/35.95 % (3442081)Termination phase: Property scanning % 247.85/35.95 % (3442081)Time elapsed: 0.012 s % 247.85/35.95 % (3442081)Peak memory usage: 85 MB % 247.85/35.95 % (3442081)Instructions burned: 58 (million) % 247.85/35.95 % (3442083)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2016827175:i=170:gtgl=4:rtra=on:gtg=exists_sym_2671 on theBenchmark for (2671ds/170Mi) % 247.85/35.95 % (3442083)Instruction limit reached! % 247.85/35.95 % (3442083)------------------------------ % 247.85/35.95 % (3442083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.85/35.95 % (3442083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.85/35.95 % (3442083)CaDiCaL version: 2.1.3 % 247.85/35.95 % (3442083)Termination reason: Instruction limit % 247.85/35.95 % (3442083)Termination phase: Property scanning % 247.85/35.95 % (3442083)Time elapsed: 0.068 s % 247.85/35.95 % (3442083)Peak memory usage: 85 MB % 247.85/35.95 % (3442083)Instructions burned: 171 (million) % 247.85/35.95 % (3442089)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3658873617:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2668 on theBenchmark for (2668ds/4Mi) % 247.85/35.95 % (3442089)Instruction limit reached! % 247.85/35.95 % (3442089)------------------------------ % 247.85/35.95 % (3442089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.85/35.95 % (3442089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.85/35.95 % (3442089)CaDiCaL version: 2.1.3 % 247.85/35.95 % (3442089)Termination reason: Instruction limit % 247.85/35.95 % (3442089)Termination phase: shuffling % 247.85/35.95 % (3442089)Time elapsed: 0.002 s % 247.85/35.95 % (3442089)Peak memory usage: 85 MB % 247.85/35.95 % (3442089)Instructions burned: 5 (million) % 247.85/35.95 % (3442091)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1474340469:i=362:rtra=on:ss=axioms:ev=cautious_2666 on theBenchmark for (2666ds/362Mi) % 247.85/35.95 % (3442091)Refutation not found, incomplete strategy % 247.85/35.95 % (3442091)------------------------------ % 247.85/35.95 % (3442091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.85/35.95 % (3442091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.85/35.95 % (3442091)CaDiCaL version: 2.1.3 % 247.85/35.95 % (3442091)Termination reason: Refutation not found, incomplete strategy % 247.85/35.95 % (3442091)Time elapsed: 0.036 s % 247.85/35.95 % (3442091)Peak memory usage: 88 MB % 247.85/35.95 % (3442091)Instructions burned: 174 (million) % 247.85/35.95 % (3442091)------------------------------ % 247.85/35.95 % (3442091)------------------------------ % 247.85/35.95 % (3442093)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3611144753:i=8:ep=RST:ins=2:rtra=on_2662 on theBenchmark for (2662ds/8Mi) % 247.85/35.95 % (3442093)Instruction limit reached! % 247.85/35.95 % (3442093)------------------------------ % 247.85/35.95 % (3442093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.85/35.95 % (3442093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.85/35.95 % (3442093)CaDiCaL version: 2.1.3 % 247.85/35.95 % (3442093)Termination reason: Instruction limit % 247.85/35.95 % (3442093)Termination phase: shuffling % 247.85/35.95 % (3442093)Time elapsed: 0.003 s % 247.85/35.95 % (3442093)Peak memory usage: 85 MB % 247.85/35.95 % (3442093)Instructions burned: 11 (million) % 247.85/35.95 % (3442095)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3855973208:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2660 on theBenchmark for (2660ds/132Mi) % 247.85/35.95 % (3442095)Instruction limit reached! % 247.85/35.95 % (3442095)------------------------------ % 247.85/35.95 % (3442095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.85/35.95 % (3442095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.85/35.95 % (3442095)CaDiCaL version: 2.1.3 % 247.85/35.95 % (3442095)Termination reason: Instruction limit % 247.85/35.95 % (3442095)Termination phase: Property scanning % 247.85/35.95 % (3442095)Time elapsed: 0.027 s % 247.85/35.95 % (3442095)Peak memory usage: 86 MB % 247.85/35.95 % (3442095)Instructions burned: 134 (million) % 247.85/35.95 % (3442097)lrs+10_1_thi=all:si=on:fd=off:random_seed=788901083:i=106:rtra=on:gtg=all_2659 on theBenchmark for (2659ds/106Mi) % 247.85/35.95 % (3442097)Instruction limit reached! % 247.85/35.95 % (3442097)------------------------------ % 247.85/35.95 % (3442097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.85/35.95 % (3442097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3442097)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3442097)Termination reason: Instruction limit % 254.87/37.01 % (3442097)Termination phase: Property scanning % 254.87/37.01 % (3442097)Time elapsed: 0.025 s % 254.87/37.01 % (3442097)Peak memory usage: 85 MB % 254.87/37.01 % (3442097)Instructions burned: 107 (million) % 254.87/37.01 % (3442099)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=857771191:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2657 on theBenchmark for (2657ds/16Mi) % 254.87/37.01 % (3442099)Instruction limit reached! % 254.87/37.01 % (3442099)------------------------------ % 254.87/37.01 % (3442099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.87/37.01 % (3442099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3442099)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3442099)Termination reason: Instruction limit % 254.87/37.01 % (3442099)Termination phase: Property scanning % 254.87/37.01 % (3442099)Time elapsed: 0.004 s % 254.87/37.01 % (3442099)Peak memory usage: 85 MB % 254.87/37.01 % (3442099)Instructions burned: 16 (million) % 254.87/37.01 % (3441937)Instruction limit reached! % 254.87/37.01 % (3441937)------------------------------ % 254.87/37.01 % (3441937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.87/37.01 % (3441937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3441937)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3441937)Termination reason: Instruction limit % 254.87/37.01 % (3441937)Termination phase: Saturation % 254.87/37.01 % (3441937)Time elapsed: 21.594 s % 254.87/37.01 % (3441937)Peak memory usage: 116 MB % 254.87/37.01 % (3441937)Instructions burned: 58629 (million) % 254.87/37.01 % (3442101)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1393701695:st=3:i=4:rtra=on:ss=axioms_2656 on theBenchmark for (2656ds/4Mi) % 254.87/37.01 % (3442101)Instruction limit reached! % 254.87/37.01 % (3442101)------------------------------ % 254.87/37.01 % (3442101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.87/37.01 % (3442101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3442101)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3442101)Termination reason: Instruction limit % 254.87/37.01 % (3442101)Termination phase: shuffling % 254.87/37.01 % (3442101)Time elapsed: 0.002 s % 254.87/37.01 % (3442101)Peak memory usage: 85 MB % 254.87/37.01 % (3442101)Instructions burned: 7 (million) % 254.87/37.01 % (3442102)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=283037103:i=4:doe=on:canc=force:asg=cautious:rtra=on_2655 on theBenchmark for (2655ds/4Mi) % 254.87/37.01 % (3442102)Instruction limit reached! % 254.87/37.01 % (3442102)------------------------------ % 254.87/37.01 % (3442102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.87/37.01 % (3442102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3442102)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3442102)Termination reason: Instruction limit % 254.87/37.01 % (3442102)Termination phase: shuffling % 254.87/37.01 % (3442102)Time elapsed: 0.002 s % 254.87/37.01 % (3442102)Peak memory usage: 85 MB % 254.87/37.01 % (3442102)Instructions burned: 5 (million) % 254.87/37.01 % (3442104)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2758075972:i=254:doe=on:rtra=on_2654 on theBenchmark for (2654ds/254Mi) % 254.87/37.01 % (3442104)Instruction limit reached! % 254.87/37.01 % (3442104)------------------------------ % 254.87/37.01 % (3442104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.87/37.01 % (3442104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3442104)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3442104)Termination reason: Instruction limit % 254.87/37.01 % (3442104)Termination phase: Property scanning % 254.87/37.01 % (3442104)Time elapsed: 0.106 s % 254.87/37.01 % (3442104)Peak memory usage: 86 MB % 254.87/37.01 % (3442104)Instructions burned: 255 (million) % 254.87/37.01 % (3442108)dis+10_1_si=on:random_seed=2119113577:i=20:ep=R:rtra=on_2653 on theBenchmark for (2653ds/20Mi) % 254.87/37.01 % (3442108)Instruction limit reached! % 254.87/37.01 % (3442108)------------------------------ % 254.87/37.01 % (3442108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.87/37.01 % (3442108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.87/37.01 % (3442108)CaDiCaL version: 2.1.3 % 254.87/37.01 % (3442108)Termination reason: Instruction limit % 254.87/37.01 % (3442108)Termination phase: Property scanning % 263.27/38.02 % (3442108)Time elapsed: 0.008 s % 263.27/38.02 % (3442108)Peak memory usage: 86 MB % 263.27/38.02 % (3442108)Instructions burned: 20 (million) % 263.27/38.02 % (3442110)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4230506:i=52:canc=cautious:av=off:rtra=on_2651 on theBenchmark for (2651ds/52Mi) % 263.27/38.02 % (3442110)Instruction limit reached! % 263.27/38.02 % (3442110)------------------------------ % 263.27/38.02 % (3442110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.27/38.02 % (3442110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.27/38.02 % (3442110)CaDiCaL version: 2.1.3 % 263.27/38.02 % (3442110)Termination reason: Instruction limit % 263.27/38.02 % (3442110)Termination phase: Property scanning % 263.27/38.02 % (3442110)Time elapsed: 0.012 s % 263.27/38.02 % (3442110)Peak memory usage: 85 MB % 263.27/38.02 % (3442110)Instructions burned: 57 (million) % 263.27/38.02 % (3442114)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=970094183:i=4:fsr=off:rtra=on:inst=on_2650 on theBenchmark for (2650ds/4Mi) % 263.27/38.02 % (3442112)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=876126977:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2650 on theBenchmark for (2650ds/70Mi) % 263.27/38.02 % (3442114)Instruction limit reached! % 263.27/38.02 % (3442114)------------------------------ % 263.27/38.02 % (3442114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.27/38.02 % (3442114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.27/38.02 % (3442114)CaDiCaL version: 2.1.3 % 263.27/38.02 % (3442114)Termination reason: Instruction limit % 263.27/38.02 % (3442114)Termination phase: shuffling % 263.27/38.02 % (3442114)Time elapsed: 0.001 s % 263.27/38.02 % (3442114)Peak memory usage: 85 MB % 263.27/38.02 % (3442114)Instructions burned: 6 (million) % 263.27/38.02 % (3442112)Instruction limit reached! % 263.27/38.02 % (3442112)------------------------------ % 263.27/38.02 % (3442112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.27/38.02 % (3442112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.27/38.02 % (3442112)CaDiCaL version: 2.1.3 % 263.27/38.02 % (3442112)Termination reason: Instruction limit % 263.27/38.02 % (3442112)Termination phase: Property scanning % 263.27/38.02 % (3442112)Time elapsed: 0.028 s % 263.27/38.02 % (3442112)Peak memory usage: 86 MB % 263.27/38.02 % (3442112)Instructions burned: 72 (million) % 263.27/38.02 % (3442117)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1827805244:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2648 on theBenchmark for (2648ds/16Mi) % 263.27/38.02 % (3442117)Instruction limit reached! % 263.27/38.02 % (3442117)------------------------------ % 263.27/38.02 % (3442117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.27/38.02 % (3442117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.27/38.02 % (3442117)CaDiCaL version: 2.1.3 % 263.27/38.02 % (3442117)Termination reason: Instruction limit % 263.27/38.02 % (3442117)Termination phase: shuffling % 263.27/38.02 % (3442117)Time elapsed: 0.004 s % 263.27/38.02 % (3442117)Peak memory usage: 85 MB % 263.27/38.02 % (3442117)Instructions burned: 19 (million) % 263.27/38.02 % (3442118)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1372732953:i=740:ep=RS:fsr=off:rtra=on_2648 on theBenchmark for (2648ds/740Mi) % 263.27/38.02 % (3442120)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1240782766:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2647 on theBenchmark for (2647ds/26Mi) % 263.27/38.02 % (3442120)Instruction limit reached! % 263.27/38.02 % (3442120)------------------------------ % 263.27/38.02 % (3442120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.27/38.02 % (3442120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.27/38.02 % (3442120)CaDiCaL version: 2.1.3 % 263.27/38.02 % (3442120)Termination reason: Instruction limit % 263.27/38.02 % (3442120)Termination phase: Property scanning % 263.27/38.02 % (3442120)Time elapsed: 0.006 s % 263.27/38.02 % (3442120)Peak memory usage: 85 MB % 263.27/38.02 % (3442120)Instructions burned: 30 (million) % 263.27/38.02 % (3442123)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2116521879:i=452:rtra=on:gtg=position:ss=axioms_2646 on theBenchmark for (2646ds/452Mi) % 263.27/38.02 % (3442118)Refutation not found, incomplete strategy % 272.57/39.44 % (3442118)------------------------------ % 272.57/39.44 % (3442118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.57/39.44 % (3442118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/39.44 % (3442118)CaDiCaL version: 2.1.3 % 272.57/39.44 % (3442118)Termination reason: Refutation not found, incomplete strategy % 272.57/39.44 % (3442118)Time elapsed: 0.244 s % 272.57/39.44 % (3442118)Peak memory usage: 89 MB % 272.57/39.44 % (3442118)Instructions burned: 640 (million) % 272.57/39.44 % (3442123)Refutation not found, incomplete strategy % 272.57/39.44 % (3442123)------------------------------ % 272.57/39.44 % (3442123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.57/39.44 % (3442123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/39.44 % (3442123)CaDiCaL version: 2.1.3 % 272.57/39.44 % (3442123)Termination reason: Refutation not found, incomplete strategy % 272.57/39.44 % (3442123)Time elapsed: 0.129 s % 272.57/39.44 % (3442123)Peak memory usage: 112 MB % 272.57/39.44 % (3442123)Instructions burned: 286 (million) % 272.57/39.44 % (3442118)------------------------------ % 272.57/39.44 % (3442118)------------------------------ % 272.57/39.44 % (3442123)------------------------------ % 272.57/39.44 % (3442123)------------------------------ % 272.57/39.44 % (3442127)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3412416817:i=20:rtra=on_2641 on theBenchmark for (2641ds/20Mi) % 272.57/39.44 % (3442127)Instruction limit reached! % 272.57/39.44 % (3442127)------------------------------ % 272.57/39.44 % (3442127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.57/39.44 % (3442127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/39.44 % (3442127)CaDiCaL version: 2.1.3 % 272.57/39.44 % (3442127)Termination reason: Instruction limit % 272.57/39.44 % (3442127)Termination phase: Property scanning % 272.57/39.44 % (3442127)Time elapsed: 0.008 s % 272.57/39.44 % (3442127)Peak memory usage: 85 MB % 272.57/39.44 % (3442127)Instructions burned: 22 (million) % 272.57/39.44 % (3442128)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2953577948:i=142:rtra=on:gtg=exists_top_2640 on theBenchmark for (2640ds/142Mi) % 272.57/39.44 % (3442128)Instruction limit reached! % 272.57/39.44 % (3442128)------------------------------ % 272.57/39.44 % (3442128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.57/39.44 % (3442128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/39.44 % (3442128)CaDiCaL version: 2.1.3 % 272.57/39.44 % (3442128)Termination reason: Instruction limit % 272.57/39.44 % (3442128)Termination phase: Property scanning % 272.57/39.44 % (3442128)Time elapsed: 0.056 s % 272.57/39.44 % (3442128)Peak memory usage: 86 MB % 272.57/39.44 % (3442128)Instructions burned: 142 (million) % 272.57/39.44 % (3442130)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=2856471752:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2639 on theBenchmark for (2639ds/150Mi) % 272.57/39.44 % (3442130)Instruction limit reached! % 272.57/39.44 % (3442130)------------------------------ % 272.57/39.44 % (3442130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.57/39.44 % (3442130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/39.44 % (3442130)CaDiCaL version: 2.1.3 % 272.57/39.44 % (3442130)Termination reason: Instruction limit % 272.57/39.44 % (3442130)Termination phase: Property scanning % 272.57/39.44 % (3442130)Time elapsed: 0.060 s % 272.57/39.44 % (3442130)Peak memory usage: 86 MB % 272.57/39.44 % (3442130)Instructions burned: 151 (million) % 272.57/39.44 % (3442132)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=2107311459:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2637 on theBenchmark for (2637ds/588Mi) % 272.57/39.44 % (3442134)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2119102334:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2636 on theBenchmark for (2636ds/260Mi) % 272.57/39.44 % (3442132)Instruction limit reached! % 272.57/39.44 % (3442132)------------------------------ % 272.57/39.44 % (3442132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.57/39.44 % (3442132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/39.44 % (3442132)CaDiCaL version: 2.1.3 % 272.57/39.44 % (3442132)Termination reason: Instruction limit % 272.57/39.44 % (3442132)Termination phase: Saturation % 278.60/40.27 % (3442132)Time elapsed: 0.230 s % 278.60/40.27 % (3442132)Peak memory usage: 96 MB % 278.60/40.27 % (3442132)Instructions burned: 589 (million) % 278.60/40.27 % (3442134)Instruction limit reached! % 278.60/40.27 % (3442134)------------------------------ % 278.60/40.27 % (3442134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.60/40.27 % (3442134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.60/40.27 % (3442134)CaDiCaL version: 2.1.3 % 278.60/40.27 % (3442134)Termination reason: Instruction limit % 278.60/40.27 % (3442134)Termination phase: Property scanning % 278.60/40.27 % (3442134)Time elapsed: 0.104 s % 278.60/40.27 % (3442134)Peak memory usage: 86 MB % 278.60/40.27 % (3442134)Instructions burned: 262 (million) % 278.60/40.27 % (3442138)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2650868030:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2633 on theBenchmark for (2633ds/80Mi) % 278.60/40.27 % (3442137)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=47738213:i=262:rtra=on_2633 on theBenchmark for (2633ds/262Mi) % 278.60/40.27 % (3442138)Instruction limit reached! % 278.60/40.27 % (3442138)------------------------------ % 278.60/40.27 % (3442138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.60/40.27 % (3442138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.60/40.27 % (3442138)CaDiCaL version: 2.1.3 % 278.60/40.27 % (3442138)Termination reason: Instruction limit % 278.60/40.27 % (3442138)Termination phase: Property scanning % 278.60/40.27 % (3442138)Time elapsed: 0.018 s % 278.60/40.27 % (3442138)Peak memory usage: 85 MB % 278.60/40.27 % (3442138)Instructions burned: 83 (million) % 278.60/40.27 % (3442137)Instruction limit reached! % 278.60/40.27 % (3442137)------------------------------ % 278.60/40.27 % (3442137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.60/40.27 % (3442137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.60/40.27 % (3442137)CaDiCaL version: 2.1.3 % 278.60/40.27 % (3442137)Termination reason: Instruction limit % 278.60/40.27 % (3442137)Termination phase: Saturation % 278.60/40.27 % (3442137)Time elapsed: 0.134 s % 278.60/40.27 % (3442137)Peak memory usage: 128 MB % 278.60/40.27 % (3442137)Instructions burned: 262 (million) % 278.60/40.27 % (3442141)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1863516159:i=614:rtra=on:gtg=exists_top_2631 on theBenchmark for (2631ds/614Mi) % 278.60/40.27 % (3442141)Instruction limit reached! % 278.60/40.27 % (3442141)------------------------------ % 278.60/40.27 % (3442141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.60/40.27 % (3442141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.60/40.27 % (3442141)CaDiCaL version: 2.1.3 % 278.60/40.27 % (3442141)Termination reason: Instruction limit % 278.60/40.27 % (3442141)Termination phase: Saturation % 278.60/40.27 % (3442141)Time elapsed: 0.123 s % 278.60/40.27 % (3442141)Peak memory usage: 88 MB % 278.60/40.27 % (3442141)Instructions burned: 617 (million) % 278.60/40.27 % (3442142)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2847191597:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2630 on theBenchmark for (2630ds/1196Mi) % 278.60/40.27 % (3442144)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1093219726:i=262:canc=cautious:fsr=off:rtra=on_2629 on theBenchmark for (2629ds/262Mi) % 278.60/40.27 % (3442144)Instruction limit reached! % 278.60/40.27 % (3442144)------------------------------ % 278.60/40.27 % (3442144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.60/40.27 % (3442144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.60/40.27 % (3442144)CaDiCaL version: 2.1.3 % 278.60/40.27 % (3442144)Termination reason: Instruction limit % 278.60/40.27 % (3442144)Termination phase: Property scanning % 278.60/40.27 % (3442144)Time elapsed: 0.082 s % 278.60/40.27 % (3442144)Peak memory usage: 86 MB % 278.60/40.27 % (3442144)Instructions burned: 262 (million) % 278.60/40.27 % (3442147)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=4276916208:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2626 on theBenchmark for (2626ds/518Mi) % 278.60/40.27 % (3442147)Refutation not found, incomplete strategy % 278.60/40.27 % (3442147)------------------------------ % 278.60/40.27 % (3442147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.60/40.27 % (3442147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.43/41.10 % (3442147)CaDiCaL version: 2.1.3 % 284.43/41.10 % (3442147)Termination reason: Refutation not found, incomplete strategy % 284.43/41.10 % (3442147)Time elapsed: 0.137 s % 284.43/41.10 % (3442147)Peak memory usage: 112 MB % 284.43/41.10 % (3442147)Instructions burned: 300 (million) % 284.43/41.10 % (3442142)Instruction limit reached! % 284.43/41.10 % (3442142)------------------------------ % 284.43/41.10 % (3442142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.43/41.10 % (3442142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.43/41.10 % (3442142)CaDiCaL version: 2.1.3 % 284.43/41.10 % (3442142)Termination reason: Instruction limit % 284.43/41.10 % (3442142)Termination phase: Saturation % 284.43/41.10 % (3442142)Time elapsed: 0.500 s % 284.43/41.10 % (3442142)Peak memory usage: 132 MB % 284.43/41.10 % (3442142)Instructions burned: 1196 (million) % 284.43/41.10 % (3442147)------------------------------ % 284.43/41.10 % (3442147)------------------------------ % 284.43/41.10 % (3442149)dis+10_1_si=on:random_seed=2141671250:s2a=on:i=2000:rtra=on:gtg=exists_all_2623 on theBenchmark for (2623ds/2000Mi) % 284.43/41.10 % (3442150)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=368763341:i=766:fsr=off:rtra=on:ev=force_2620 on theBenchmark for (2620ds/766Mi) % 284.43/41.10 % (3442150)Instruction limit reached! % 284.43/41.10 % (3442150)------------------------------ % 284.43/41.10 % (3442150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.43/41.10 % (3442150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.43/41.10 % (3442150)CaDiCaL version: 2.1.3 % 284.43/41.10 % (3442150)Termination reason: Instruction limit % 284.43/41.10 % (3442150)Termination phase: Saturation % 284.43/41.10 % (3442150)Time elapsed: 0.300 s % 284.43/41.10 % (3442150)Peak memory usage: 89 MB % 284.43/41.10 % (3442150)Instructions burned: 767 (million) % 284.43/41.10 % (3442149)Instruction limit reached! % 284.43/41.10 % (3442149)------------------------------ % 284.43/41.10 % (3442149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.43/41.10 % (3442149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.43/41.10 % (3442149)CaDiCaL version: 2.1.3 % 284.43/41.10 % (3442149)Termination reason: Instruction limit % 284.43/41.10 % (3442149)Termination phase: Saturation % 284.43/41.10 % (3442149)Time elapsed: 0.650 s % 284.43/41.10 % (3442149)Peak memory usage: 95 MB % 284.43/41.10 % (3442149)Instructions burned: 2003 (million) % 284.43/41.10 % (3442153)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=972638128:i=282:doe=on:rtra=on_2615 on theBenchmark for (2615ds/282Mi) % 284.43/41.10 % (3442153)Instruction limit reached! % 284.43/41.10 % (3442153)------------------------------ % 284.43/41.10 % (3442153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.43/41.10 % (3442153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.43/41.10 % (3442153)CaDiCaL version: 2.1.3 % 284.43/41.10 % (3442153)Termination reason: Instruction limit % 284.43/41.10 % (3442153)Termination phase: Property scanning % 284.43/41.10 % (3442153)Time elapsed: 0.114 s % 284.43/41.10 % (3442153)Peak memory usage: 86 MB % 284.43/41.10 % (3442153)Instructions burned: 284 (million) % 284.43/41.10 % (3442154)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=480721152:i=130:nm=16:rtra=on_2614 on theBenchmark for (2614ds/130Mi) % 284.43/41.10 % (3442154)Instruction limit reached! % 284.43/41.10 % (3442154)------------------------------ % 284.43/41.10 % (3442154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.43/41.10 % (3442154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.43/41.10 % (3442154)CaDiCaL version: 2.1.3 % 284.43/41.10 % (3442154)Termination reason: Instruction limit % 284.43/41.10 % (3442154)Termination phase: Property scanning % 284.43/41.10 % (3442154)Time elapsed: 0.053 s % 284.43/41.10 % (3442154)Peak memory usage: 86 MB % 284.43/41.10 % (3442154)Instructions burned: 131 (million) % 284.43/41.10 % (3442156)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4196340057:i=242:nm=16:rtra=on_2612 on theBenchmark for (2612ds/242Mi) % 284.43/41.10 % (3442158)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=1913677567:s2a=on:i=256:s2at=5:ins=3:rtra=on_2611 on theBenchmark for (2611ds/256Mi) % 284.43/41.10 % (3442156)Instruction limit reached! % 284.43/41.10 % (3442156)------------------------------ % 284.43/41.10 % (3442156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.16/42.15 % (3442156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.16/42.15 % (3442156)CaDiCaL version: 2.1.3 % 292.16/42.15 % (3442156)Termination reason: Instruction limit % 292.16/42.15 % (3442156)Termination phase: Property scanning % 292.16/42.15 % (3442156)Time elapsed: 0.098 s % 292.16/42.15 % (3442156)Peak memory usage: 86 MB % 292.16/42.15 % (3442156)Instructions burned: 243 (million) % 292.16/42.15 % (3442158)Instruction limit reached! % 292.16/42.15 % (3442158)------------------------------ % 292.16/42.15 % (3442158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.16/42.15 % (3442158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.16/42.15 % (3442158)CaDiCaL version: 2.1.3 % 292.16/42.15 % (3442158)Termination reason: Instruction limit % 292.16/42.15 % (3442158)Termination phase: Property scanning % 292.16/42.15 % (3442158)Time elapsed: 0.103 s % 292.16/42.15 % (3442158)Peak memory usage: 86 MB % 292.16/42.15 % (3442158)Instructions burned: 258 (million) % 292.16/42.15 % (3442161)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=45570328:i=78:ins=3:rtra=on_2609 on theBenchmark for (2609ds/78Mi) % 292.16/42.15 % (3442161)Instruction limit reached! % 292.16/42.15 % (3442161)------------------------------ % 292.16/42.15 % (3442161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.16/42.15 % (3442161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.16/42.15 % (3442161)CaDiCaL version: 2.1.3 % 292.16/42.15 % (3442161)Termination reason: Instruction limit % 292.16/42.15 % (3442161)Termination phase: Property scanning % 292.16/42.15 % (3442161)Time elapsed: 0.018 s % 292.16/42.15 % (3442161)Peak memory usage: 86 MB % 292.16/42.15 % (3442161)Instructions burned: 81 (million) % 292.16/42.15 % (3442164)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1849635624:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2607 on theBenchmark for (2607ds/658Mi) % 292.16/42.15 % (3442162)dis+1010_1_to=kbo:si=on:random_seed=1856116439:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2608 on theBenchmark for (2608ds/350Mi) % 292.16/42.15 % (3442164)Instruction limit reached! % 292.16/42.15 % (3442164)------------------------------ % 292.16/42.15 % (3442164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.16/42.15 % (3442164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.16/42.15 % (3442164)CaDiCaL version: 2.1.3 % 292.16/42.15 % (3442164)Termination reason: Instruction limit % 292.16/42.15 % (3442164)Termination phase: Property scanning % 292.16/42.15 % (3442164)Time elapsed: 0.132 s % 292.16/42.15 % (3442164)Peak memory usage: 87 MB % 292.16/42.15 % (3442164)Instructions burned: 660 (million) % 292.16/42.15 % (3442162)Instruction limit reached! % 292.16/42.15 % (3442162)------------------------------ % 292.16/42.15 % (3442162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.16/42.15 % (3442162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.16/42.15 % (3442162)CaDiCaL version: 2.1.3 % 292.16/42.15 % (3442162)Termination reason: Instruction limit % 292.16/42.15 % (3442162)Termination phase: Property scanning % 292.16/42.15 % (3442162)Time elapsed: 0.137 s % 292.16/42.15 % (3442162)Peak memory usage: 85 MB % 292.16/42.15 % (3442162)Instructions burned: 350 (million) % 292.16/42.15 % (3442167)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=65380506:s2a=on:i=966:doe=on:nm=32:rtra=on_2604 on theBenchmark for (2604ds/966Mi) % 292.16/42.15 % (3442168)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1563701172:thitd=on:i=430:nm=0:rtra=on:ev=force_2604 on theBenchmark for (2604ds/430Mi) % 292.16/42.15 % (3441949)Instruction limit reached! % 292.16/42.15 % (3441949)------------------------------ % 292.16/42.15 % (3441949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.16/42.15 % (3441949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.16/42.15 % (3441949)CaDiCaL version: 2.1.3 % 292.16/42.15 % (3441949)Termination reason: Instruction limit % 292.16/42.15 % (3441949)Termination phase: Saturation % 292.16/42.15 % (3441949)Time elapsed: 26.216 s % 292.16/42.15 % (3441949)Peak memory usage: 110 MB % 292.16/42.15 % (3441949)Instructions burned: 71624 (million) % 292.16/42.15 % (3442168)Instruction limit reached! % 292.16/42.15 % (3442168)------------------------------ % 292.16/42.15 % (3442168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.05/42.85 % (3442168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.05/42.85 % (3442168)CaDiCaL version: 2.1.3 % 296.05/42.85 % (3442168)Termination reason: Instruction limit % 296.05/42.85 % (3442168)Termination phase: Property scanning % 296.05/42.85 % (3442168)Time elapsed: 0.175 s % 296.05/42.85 % (3442168)Peak memory usage: 87 MB % 296.05/42.85 % (3442168)Instructions burned: 432 (million) % 296.05/42.85 % (3442171)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3349953694:i=698:rtra=on_2602 on theBenchmark for (2602ds/698Mi) % 296.05/42.85 % (3442167)Instruction limit reached! % 296.05/42.85 % (3442167)------------------------------ % 296.05/42.85 % (3442167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.05/42.85 % (3442167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.05/42.85 % (3442167)CaDiCaL version: 2.1.3 % 296.05/42.85 % (3442167)Termination reason: Instruction limit % 296.05/42.85 % (3442167)Termination phase: Saturation % 296.05/42.85 % (3442167)Time elapsed: 0.415 s % 296.05/42.85 % (3442167)Peak memory usage: 131 MB % 296.05/42.85 % (3442167)Instructions burned: 966 (million) % 296.05/42.85 % (3442172)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1063337415:st=2:i=590:rtra=on:ss=axioms_2600 on theBenchmark for (2600ds/590Mi) % 296.05/42.85 % (3442172)Refutation not found, incomplete strategy % 296.05/42.85 % (3442172)------------------------------ % 296.05/42.85 % (3442172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.05/42.85 % (3442172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.05/42.85 % (3442172)CaDiCaL version: 2.1.3 % 296.05/42.85 % (3442172)Termination reason: Refutation not found, incomplete strategy % 296.05/42.85 % (3442172)Time elapsed: 0.112 s % 296.05/42.85 % (3442172)Peak memory usage: 88 MB % 296.05/42.85 % (3442172)Instructions burned: 289 (million) % 296.05/42.85 % (3442174)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1058869630:i=656:kws=inv_frequency:nm=20:rtra=on_2599 on theBenchmark for (2599ds/656Mi) % 296.05/42.85 % (3442171)Instruction limit reached! % 296.05/42.85 % (3442171)------------------------------ % 296.05/42.85 % (3442171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.05/42.85 % (3442171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.05/42.85 % (3442171)CaDiCaL version: 2.1.3 % 296.05/42.85 % (3442171)Termination reason: Instruction limit % 296.05/42.85 % (3442171)Termination phase: Saturation % 296.05/42.85 % (3442171)Time elapsed: 0.294 s % 296.05/42.85 % (3442171)Peak memory usage: 115 MB % 296.05/42.85 % (3442171)Instructions burned: 699 (million) % 296.05/42.85 % (3442172)------------------------------ % 296.05/42.85 % (3442172)------------------------------ % 296.05/42.85 % (3442177)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1380246248:i=562:gtgl=2:rtra=on:gtg=all_2596 on theBenchmark for (2596ds/562Mi) % 296.05/42.85 % (3442174)Instruction limit reached! % 296.05/42.85 % (3442174)------------------------------ % 296.05/42.85 % (3442174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.05/42.85 % (3442174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.05/42.85 % (3442174)CaDiCaL version: 2.1.3 % 296.05/42.85 % (3442174)Termination reason: Instruction limit % 296.05/42.85 % (3442174)Termination phase: Saturation % 296.05/42.85 % (3442174)Time elapsed: 0.272 s % 296.05/42.85 % (3442174)Peak memory usage: 112 MB % 296.05/42.85 % (3442174)Instructions burned: 656 (million) % 296.05/42.85 % (3442180)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=649083665:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2595 on theBenchmark for (2595ds/968Mi) % 296.05/42.85 % (3442180)Refutation not found, incomplete strategy % 296.05/42.85 % (3442180)------------------------------ % 296.05/42.85 % (3442180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.05/42.85 % (3442180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.05/42.85 % (3442180)CaDiCaL version: 2.1.3 % 296.05/42.85 % (3442180)Termination reason: Refutation not found, incomplete strategy % 296.05/42.85 % (3442180)Time elapsed: 0.105 s % 296.05/42.85 % (3442180)Peak memory usage: 88 MB % 296.05/42.85 % (3442180)Instructions burned: 281 (million) % 296.05/42.85 % (3442177)Instruction limit reached! % 296.05/42.85 % (3442177)------------------------------ % 296.05/42.85 % (3442177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200Terminated % 300.39/43.32 % Vampire exiting %------------------------------------------------------------------------------