%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW839_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n009.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:37:55 PM UTC 2026 % Result : Timeout 297.07s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW839_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.26 % Computer : n009.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 14:31:00 UTC 2026 % 0.10/0.26 % CPUTime : % 0.10/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.27/0.32 Running first-order theorem proving % 0.27/0.32 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.84/1.77 % (3070674)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.84/1.77 % (3070685)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=240223639:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.84/1.77 % (3070690)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3926072186:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.84/1.77 % (3070685)Instruction limit reached! % 4.84/1.77 % (3070685)------------------------------ % 4.84/1.77 % (3070685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.77 % (3070685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.77 % (3070685)CaDiCaL version: 2.1.3 % 4.84/1.77 % (3070685)Termination reason: Instruction limit % 4.84/1.77 % (3070685)Termination phase: Property scanning % 4.84/1.77 % (3070685)Time elapsed: 0.006 s % 4.84/1.77 % (3070685)Peak memory usage: 86 MB % 4.84/1.77 % (3070685)Instructions burned: 14 (million) % 4.84/1.77 % (3070691)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2140882413:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.84/1.77 % (3070687)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2980780354:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.84/1.77 % (3070689)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3089348231:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.84/1.77 % (3070686)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3169803710:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.84/1.77 % (3070688)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2720052801:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.84/1.77 % (3070689)Instruction limit reached! % 4.84/1.77 % (3070689)------------------------------ % 4.84/1.77 % (3070689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.77 % (3070689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.77 % (3070689)CaDiCaL version: 2.1.3 % 4.84/1.77 % (3070689)Termination reason: Instruction limit % 4.84/1.77 % (3070689)Termination phase: Property scanning % 4.84/1.77 % (3070689)Time elapsed: 0.004 s % 4.84/1.77 % (3070689)Peak memory usage: 85 MB % 4.84/1.77 % (3070689)Instructions burned: 4 (million) % 4.84/1.77 % (3070688)Instruction limit reached! % 4.84/1.77 % (3070688)------------------------------ % 4.84/1.77 % (3070688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.77 % (3070688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.77 % (3070688)CaDiCaL version: 2.1.3 % 4.84/1.77 % (3070688)Termination reason: Instruction limit % 4.84/1.77 % (3070688)Termination phase: Property scanning % 4.84/1.77 % (3070688)Time elapsed: 0.007 s % 4.84/1.77 % (3070688)Peak memory usage: 85 MB % 4.84/1.77 % (3070688)Instructions burned: 7 (million) % 4.84/1.77 % (3070690)Instruction limit reached! % 4.84/1.77 % (3070690)------------------------------ % 4.84/1.77 % (3070690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.77 % (3070690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.77 % (3070690)CaDiCaL version: 2.1.3 % 4.84/1.77 % (3070690)Termination reason: Instruction limit % 4.84/1.77 % (3070690)Termination phase: Saturation % 4.84/1.77 % (3070690)Time elapsed: 0.074 s % 4.84/1.77 % (3070690)Peak memory usage: 116 MB % 4.84/1.77 % (3070690)Instructions burned: 46 (million) % 4.84/1.77 % (3070691)Instruction limit reached! % 4.84/1.77 % (3070691)------------------------------ % 4.84/1.77 % (3070691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.77 % (3070691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.77 % (3070691)CaDiCaL version: 2.1.3 % 4.84/1.77 % (3070691)Termination reason: Instruction limit % 4.84/1.77 % (3070691)Termination phase: Saturation % 4.84/1.77 % (3070691)Time elapsed: 0.054 s % 4.84/1.77 % (3070691)Peak memory usage: 106 MB % 4.84/1.77 % (3070691)Instructions burned: 33 (million) % 4.84/1.77 % (3070694)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2895065590:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 4.84/1.77 % (3070694)Refutation not found, incomplete strategy % 4.84/1.77 % (3070694)------------------------------ % 8.69/2.12 % (3070694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.12 % (3070694)CaDiCaL version: 2.1.3 % 8.69/2.12 % (3070694)Termination reason: Refutation not found, incomplete strategy % 8.69/2.12 % (3070694)Time elapsed: 0.004 s % 8.69/2.12 % (3070694)Peak memory usage: 88 MB % 8.69/2.12 % (3070694)Instructions burned: 7 (million) % 8.69/2.12 % (3070687)Instruction limit reached! % 8.69/2.12 % (3070687)------------------------------ % 8.69/2.12 % (3070687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.12 % (3070687)CaDiCaL version: 2.1.3 % 8.69/2.12 % (3070687)Termination reason: Instruction limit % 8.69/2.12 % (3070687)Termination phase: Saturation % 8.69/2.12 % (3070687)Time elapsed: 0.206 s % 8.69/2.12 % (3070687)Peak memory usage: 117 MB % 8.69/2.12 % (3070687)Instructions burned: 202 (million) % 8.69/2.12 % (3070703)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=212647607:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 8.69/2.12 % (3070702)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=4188156956:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 8.69/2.12 % (3070703)Instruction limit reached! % 8.69/2.12 % (3070703)------------------------------ % 8.69/2.12 % (3070703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.12 % (3070703)CaDiCaL version: 2.1.3 % 8.69/2.12 % (3070703)Termination reason: Instruction limit % 8.69/2.12 % (3070703)Termination phase: Property scanning % 8.69/2.12 % (3070703)Time elapsed: 0.013 s % 8.69/2.12 % (3070703)Peak memory usage: 87 MB % 8.69/2.12 % (3070703)Instructions burned: 16 (million) % 8.69/2.12 % (3070702)Instruction limit reached! % 8.69/2.12 % (3070702)------------------------------ % 8.69/2.12 % (3070702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.12 % (3070702)CaDiCaL version: 2.1.3 % 8.69/2.12 % (3070702)Termination reason: Instruction limit % 8.69/2.12 % (3070702)Termination phase: Saturation % 8.69/2.12 % (3070702)Time elapsed: 0.027 s % 8.69/2.12 % (3070702)Peak memory usage: 88 MB % 8.69/2.12 % (3070702)Instructions burned: 30 (million) % 8.69/2.12 % (3070704)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3647430125:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 8.69/2.12 % (3070686)Instruction limit reached! % 8.69/2.12 % (3070686)------------------------------ % 8.69/2.12 % (3070686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.12 % (3070686)CaDiCaL version: 2.1.3 % 8.69/2.12 % (3070686)Termination reason: Instruction limit % 8.69/2.12 % (3070686)Termination phase: Saturation % 8.69/2.12 % (3070686)Time elapsed: 0.309 s % 8.69/2.12 % (3070686)Peak memory usage: 118 MB % 8.69/2.12 % (3070686)Instructions burned: 307 (million) % 8.69/2.12 % (3070705)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=2287260279:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 8.69/2.12 % (3070704)Instruction limit reached! % 8.69/2.12 % (3070704)------------------------------ % 8.69/2.12 % (3070704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.69/2.12 % (3070704)CaDiCaL version: 2.1.3 % 8.69/2.12 % (3070704)Termination reason: Instruction limit % 8.69/2.12 % (3070704)Termination phase: Function definition elimination % 8.69/2.12 % (3070704)Time elapsed: 0.018 s % 8.69/2.12 % (3070704)Peak memory usage: 87 MB % 8.69/2.12 % (3070704)Instructions burned: 24 (million) % 8.69/2.12 % (3070705)Instruction limit reached! % 8.69/2.12 % (3070705)------------------------------ % 8.69/2.12 % (3070705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.69/2.12 % (3070705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.38 % (3070705)CaDiCaL version: 2.1.3 % 9.82/2.38 % (3070705)Termination reason: Instruction limit % 9.82/2.38 % (3070705)Termination phase: Property scanning % 9.82/2.38 % (3070705)Time elapsed: 0.025 s % 9.82/2.38 % (3070705)Peak memory usage: 87 MB % 9.82/2.38 % (3070705)Instructions burned: 27 (million) % 9.82/2.38 % (3070694)------------------------------ % 9.82/2.38 % (3070694)------------------------------ % 9.82/2.38 % (3070708)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2439329876:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 9.82/2.38 % (3070714)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3084446496:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 9.82/2.38 % (3070714)Instruction limit reached! % 9.82/2.38 % (3070714)------------------------------ % 9.82/2.38 % (3070714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.38 % (3070714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.38 % (3070714)CaDiCaL version: 2.1.3 % 9.82/2.38 % (3070714)Termination reason: Instruction limit % 9.82/2.38 % (3070714)Termination phase: Property scanning % 9.82/2.38 % (3070714)Time elapsed: 0.003 s % 9.82/2.38 % (3070714)Peak memory usage: 85 MB % 9.82/2.38 % (3070714)Instructions burned: 3 (million) % 9.82/2.38 % (3070708)Instruction limit reached! % 9.82/2.38 % (3070708)------------------------------ % 9.82/2.38 % (3070708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.38 % (3070708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.38 % (3070708)CaDiCaL version: 2.1.3 % 9.82/2.38 % (3070708)Termination reason: Instruction limit % 9.82/2.38 % (3070708)Termination phase: Saturation % 9.82/2.38 % (3070708)Time elapsed: 0.079 s % 9.82/2.38 % (3070708)Peak memory usage: 89 MB % 9.82/2.38 % (3070708)Instructions burned: 86 (million) % 9.82/2.38 % (3070719)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2765379187:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 9.82/2.38 % (3070716)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1752209102:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.82/2.38 % (3070716)Refutation not found, incomplete strategy % 9.82/2.38 % (3070716)------------------------------ % 9.82/2.38 % (3070716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.38 % (3070716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.38 % (3070716)CaDiCaL version: 2.1.3 % 9.82/2.38 % (3070716)Termination reason: Refutation not found, incomplete strategy % 9.82/2.38 % (3070716)Time elapsed: 0.007 s % 9.82/2.38 % (3070716)Peak memory usage: 87 MB % 9.82/2.38 % (3070716)Instructions burned: 6 (million) % 9.82/2.38 % (3070718)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1595532290:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.82/2.38 % (3070718)Instruction limit reached! % 9.82/2.38 % (3070718)------------------------------ % 9.82/2.38 % (3070718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.38 % (3070718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.38 % (3070718)CaDiCaL version: 2.1.3 % 9.82/2.38 % (3070718)Termination reason: Instruction limit % 9.82/2.38 % (3070718)Termination phase: Property scanning % 9.82/2.38 % (3070718)Time elapsed: 0.004 s % 9.82/2.38 % (3070718)Peak memory usage: 85 MB % 9.82/2.38 % (3070718)Instructions burned: 4 (million) % 9.82/2.38 % (3070720)lrs+10_1_thi=all:si=on:fd=off:random_seed=1723497676:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 9.82/2.38 % (3070721)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=3733498609:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 9.82/2.38 % (3070721)Instruction limit reached! % 9.82/2.38 % (3070721)------------------------------ % 9.82/2.38 % (3070721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.38 % (3070721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.38 % (3070721)CaDiCaL version: 2.1.3 % 9.82/2.38 % (3070721)Termination reason: Instruction limit % 9.82/2.38 % (3070721)Termination phase: shuffling % 11.08/2.69 % (3070721)Time elapsed: 0.004 s % 11.08/2.69 % (3070721)Peak memory usage: 85 MB % 11.08/2.69 % (3070721)Instructions burned: 8 (million) % 11.08/2.69 % (3070720)Instruction limit reached! % 11.08/2.69 % (3070720)------------------------------ % 11.08/2.69 % (3070720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.69 % (3070720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.69 % (3070720)CaDiCaL version: 2.1.3 % 11.08/2.69 % (3070720)Termination reason: Instruction limit % 11.08/2.69 % (3070720)Termination phase: Saturation % 11.08/2.69 % (3070720)Time elapsed: 0.080 s % 11.08/2.69 % (3070720)Peak memory usage: 116 MB % 11.08/2.69 % (3070720)Instructions burned: 53 (million) % 11.08/2.69 % (3070719)Instruction limit reached! % 11.08/2.69 % (3070719)------------------------------ % 11.08/2.69 % (3070719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.69 % (3070719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.69 % (3070719)CaDiCaL version: 2.1.3 % 11.08/2.69 % (3070719)Termination reason: Instruction limit % 11.08/2.69 % (3070719)Termination phase: Saturation % 11.08/2.69 % (3070719)Time elapsed: 0.125 s % 11.08/2.69 % (3070719)Peak memory usage: 134 MB % 11.08/2.69 % (3070719)Instructions burned: 66 (million) % 11.08/2.69 % (3070727)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=314170540:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi) % 11.08/2.69 % (3070726)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2668180459:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 11.08/2.69 % (3070727)Instruction limit reached! % 11.08/2.69 % (3070727)------------------------------ % 11.08/2.69 % (3070727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.69 % (3070727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.69 % (3070727)CaDiCaL version: 2.1.3 % 11.08/2.69 % (3070727)Termination reason: Instruction limit % 11.08/2.69 % (3070727)Termination phase: Property scanning % 11.08/2.69 % (3070727)Time elapsed: 0.003 s % 11.08/2.69 % (3070727)Peak memory usage: 85 MB % 11.08/2.69 % (3070727)Instructions burned: 3 (million) % 11.08/2.69 % (3070726)Instruction limit reached! % 11.08/2.69 % (3070726)------------------------------ % 11.08/2.69 % (3070726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.69 % (3070726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.69 % (3070726)CaDiCaL version: 2.1.3 % 11.08/2.69 % (3070726)Termination reason: Instruction limit % 11.08/2.69 % (3070726)Termination phase: Property scanning % 11.08/2.69 % (3070726)Time elapsed: 0.003 s % 11.08/2.69 % (3070726)Peak memory usage: 85 MB % 11.08/2.69 % (3070726)Instructions burned: 3 (million) % 11.08/2.69 % (3070734)dis+10_1_si=on:random_seed=828351071:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 11.08/2.69 % (3070734)Instruction limit reached! % 11.08/2.69 % (3070734)------------------------------ % 11.08/2.69 % (3070734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.69 % (3070734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.69 % (3070734)CaDiCaL version: 2.1.3 % 11.08/2.69 % (3070734)Termination reason: Instruction limit % 11.08/2.69 % (3070734)Termination phase: shuffling % 11.08/2.69 % (3070734)Time elapsed: 0.005 s % 11.08/2.69 % (3070734)Peak memory usage: 86 MB % 11.08/2.69 % (3070734)Instructions burned: 11 (million) % 11.08/2.69 % (3070732)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1560958102:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 11.08/2.69 % (3070735)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1118487295:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 11.08/2.69 % (3070736)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3368475919: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_2990 on theBenchmark for (2990ds/35Mi) % 11.08/2.69 % (3070716)------------------------------ % 11.08/2.69 % (3070716)------------------------------ % 11.08/2.69 % (3070735)Instruction limit reached! % 11.08/2.69 % (3070735)------------------------------ % 11.08/2.69 % (3070735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.08/2.69 % (3070735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.08/2.69 % (3070735)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070735)Termination reason: Instruction limit % 13.25/2.99 % (3070735)Termination phase: Property scanning % 13.25/2.99 % (3070735)Time elapsed: 0.025 s % 13.25/2.99 % (3070735)Peak memory usage: 87 MB % 13.25/2.99 % (3070735)Instructions burned: 27 (million) % 13.25/2.99 % (3070736)Instruction limit reached! % 13.25/2.99 % (3070736)------------------------------ % 13.25/2.99 % (3070736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.25/2.99 % (3070736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.25/2.99 % (3070736)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070736)Termination reason: Instruction limit % 13.25/2.99 % (3070736)Termination phase: Saturation % 13.25/2.99 % (3070736)Time elapsed: 0.032 s % 13.25/2.99 % (3070736)Peak memory usage: 89 MB % 13.25/2.99 % (3070736)Instructions burned: 35 (million) % 13.25/2.99 % (3070732)Instruction limit reached! % 13.25/2.99 % (3070732)------------------------------ % 13.25/2.99 % (3070732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.25/2.99 % (3070732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.25/2.99 % (3070732)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070732)Termination reason: Instruction limit % 13.25/2.99 % (3070732)Termination phase: Saturation % 13.25/2.99 % (3070732)Time elapsed: 0.155 s % 13.25/2.99 % (3070732)Peak memory usage: 117 MB % 13.25/2.99 % (3070732)Instructions burned: 127 (million) % 13.25/2.99 % (3070742)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4176046075:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 13.25/2.99 % (3070739)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1811721408:i=2:fsr=off:rtra=on:inst=on_2989 on theBenchmark for (2989ds/2Mi) % 13.25/2.99 % (3070739)Instruction limit reached! % 13.25/2.99 % (3070739)------------------------------ % 13.25/2.99 % (3070739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.25/2.99 % (3070739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.25/2.99 % (3070739)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070739)Termination reason: Instruction limit % 13.25/2.99 % (3070739)Termination phase: Property scanning % 13.25/2.99 % (3070739)Time elapsed: 0.002 s % 13.25/2.99 % (3070739)Peak memory usage: 85 MB % 13.25/2.99 % (3070739)Instructions burned: 2 (million) % 13.25/2.99 % (3070740)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2909963164:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 13.25/2.99 % (3070740)Instruction limit reached! % 13.25/2.99 % (3070740)------------------------------ % 13.25/2.99 % (3070740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.25/2.99 % (3070740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.25/2.99 % (3070740)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070740)Termination reason: Instruction limit % 13.25/2.99 % (3070740)Termination phase: Property scanning % 13.25/2.99 % (3070740)Time elapsed: 0.008 s % 13.25/2.99 % (3070740)Peak memory usage: 85 MB % 13.25/2.99 % (3070740)Instructions burned: 8 (million) % 13.25/2.99 % (3070742)Instruction limit reached! % 13.25/2.99 % (3070742)------------------------------ % 13.25/2.99 % (3070742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.25/2.99 % (3070742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.25/2.99 % (3070742)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070742)Termination reason: Instruction limit % 13.25/2.99 % (3070742)Termination phase: Saturation % 13.25/2.99 % (3070742)Time elapsed: 0.166 s % 13.25/2.99 % (3070742)Peak memory usage: 91 MB % 13.25/2.99 % (3070742)Instructions burned: 372 (million) % 13.25/2.99 % (3070748)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=890299841:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi) % 13.25/2.99 % (3070747)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=136325170:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/13Mi) % 13.25/2.99 % (3070747)Instruction limit reached! % 13.25/2.99 % (3070747)------------------------------ % 13.25/2.99 % (3070747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.25/2.99 % (3070747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.25/2.99 % (3070747)CaDiCaL version: 2.1.3 % 13.25/2.99 % (3070747)Termination reason: Instruction limit % 13.25/2.99 % (3070747)Termination phase: Property scanning % 18.11/3.58 % (3070747)Time elapsed: 0.012 s % 18.11/3.58 % (3070747)Peak memory usage: 85 MB % 18.11/3.58 % (3070747)Instructions burned: 13 (million) % 18.11/3.58 % (3070749)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1821125832:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 18.11/3.58 % (3070749)Instruction limit reached! % 18.11/3.58 % (3070749)------------------------------ % 18.11/3.58 % (3070749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.11/3.58 % (3070749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.11/3.58 % (3070749)CaDiCaL version: 2.1.3 % 18.11/3.58 % (3070749)Termination reason: Instruction limit % 18.11/3.58 % (3070749)Termination phase: Preprocessing 3 % 18.11/3.58 % (3070749)Time elapsed: 0.010 s % 18.11/3.58 % (3070749)Peak memory usage: 86 MB % 18.11/3.58 % (3070749)Instructions burned: 10 (million) % 18.11/3.58 % (3070748)Refutation not found, incomplete strategy % 18.11/3.58 % (3070748)------------------------------ % 18.11/3.58 % (3070748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.11/3.58 % (3070748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.11/3.58 % (3070748)CaDiCaL version: 2.1.3 % 18.11/3.58 % (3070748)Termination reason: Refutation not found, incomplete strategy % 18.11/3.58 % (3070748)Time elapsed: 0.046 s % 18.11/3.58 % (3070748)Peak memory usage: 111 MB % 18.11/3.58 % (3070748)Instructions burned: 15 (million) % 18.11/3.58 % (3070755)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=2728697690:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi) % 18.11/3.58 % (3070752)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=146306273:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 18.11/3.58 % (3070753)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=3030151367:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 18.11/3.58 % (3070753)Instruction limit reached! % 18.11/3.58 % (3070753)------------------------------ % 18.11/3.58 % (3070753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.11/3.58 % (3070753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.11/3.58 % (3070753)CaDiCaL version: 2.1.3 % 18.11/3.58 % (3070753)Termination reason: Instruction limit % 18.11/3.58 % (3070753)Termination phase: Saturation % 18.11/3.58 % (3070753)Time elapsed: 0.074 s % 18.11/3.58 % (3070753)Peak memory usage: 91 MB % 18.11/3.58 % (3070753)Instructions burned: 75 (million) % 18.11/3.58 % (3070752)Instruction limit reached! % 18.11/3.58 % (3070752)------------------------------ % 18.11/3.58 % (3070752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.11/3.58 % (3070752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.11/3.58 % (3070752)CaDiCaL version: 2.1.3 % 18.11/3.58 % (3070752)Termination reason: Instruction limit % 18.11/3.58 % (3070752)Termination phase: Saturation % 18.11/3.58 % (3070752)Time elapsed: 0.123 s % 18.11/3.58 % (3070752)Peak memory usage: 133 MB % 18.11/3.58 % (3070752)Instructions burned: 71 (million) % 18.11/3.58 % (3070757)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1851564670:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi) % 18.11/3.58 % (3070760)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1289903040:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 18.11/3.58 % (3070757)Instruction limit reached! % 18.11/3.58 % (3070757)------------------------------ % 18.11/3.58 % (3070757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.11/3.58 % (3070757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.11/3.58 % (3070757)CaDiCaL version: 2.1.3 % 18.11/3.58 % (3070757)Termination reason: Instruction limit % 18.11/3.58 % (3070757)Termination phase: Saturation % 18.11/3.58 % (3070757)Time elapsed: 0.085 s % 18.11/3.58 % (3070757)Peak memory usage: 117 MB % 18.11/3.58 % (3070757)Instructions burned: 131 (million) % 18.11/3.58 % (3070762)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3334329246:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 18.11/3.58 % (3070755)Instruction limit reached! % 20.00/4.04 % (3070755)------------------------------ % 20.00/4.04 % (3070755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.00/4.04 % (3070755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.00/4.04 % (3070755)CaDiCaL version: 2.1.3 % 20.00/4.04 % (3070755)Termination reason: Instruction limit % 20.00/4.04 % (3070755)Termination phase: Saturation % 20.00/4.04 % (3070755)Time elapsed: 0.275 s % 20.00/4.04 % (3070755)Peak memory usage: 91 MB % 20.00/4.04 % (3070755)Instructions burned: 295 (million) % 20.00/4.04 % (3070762)Instruction limit reached! % 20.00/4.04 % (3070762)------------------------------ % 20.00/4.04 % (3070762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.00/4.04 % (3070762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.00/4.04 % (3070762)CaDiCaL version: 2.1.3 % 20.00/4.04 % (3070762)Termination reason: Instruction limit % 20.00/4.04 % (3070762)Termination phase: Saturation % 20.00/4.04 % (3070762)Time elapsed: 0.052 s % 20.00/4.04 % (3070762)Peak memory usage: 100 MB % 20.00/4.04 % (3070762)Instructions burned: 40 (million) % 20.00/4.04 % (3070766)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=223309089:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 20.00/4.04 % (3070760)Instruction limit reached! % 20.00/4.04 % (3070760)------------------------------ % 20.00/4.04 % (3070760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.00/4.04 % (3070760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.00/4.04 % (3070760)CaDiCaL version: 2.1.3 % 20.00/4.04 % (3070760)Termination reason: Instruction limit % 20.00/4.04 % (3070760)Termination phase: Saturation % 20.00/4.04 % (3070760)Time elapsed: 0.186 s % 20.00/4.04 % (3070760)Peak memory usage: 134 MB % 20.00/4.04 % (3070760)Instructions burned: 131 (million) % 20.00/4.04 % (3070766)Refutation not found, incomplete strategy % 20.00/4.04 % (3070766)------------------------------ % 20.00/4.04 % (3070766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.00/4.04 % (3070766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.00/4.04 % (3070766)CaDiCaL version: 2.1.3 % 20.00/4.04 % (3070766)Termination reason: Refutation not found, incomplete strategy % 20.00/4.04 % (3070766)Time elapsed: 0.051 s % 20.00/4.04 % (3070766)Peak memory usage: 90 MB % 20.00/4.04 % (3070766)Instructions burned: 54 (million) % 20.00/4.04 % (3070748)------------------------------ % 20.00/4.04 % (3070748)------------------------------ % 20.00/4.04 % (3070768)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=933926070:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 20.00/4.04 % (3070770)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4251707191:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 20.00/4.04 % (3070770)Instruction limit reached! % 20.00/4.04 % (3070770)------------------------------ % 20.00/4.04 % (3070770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.00/4.04 % (3070770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.00/4.04 % (3070770)CaDiCaL version: 2.1.3 % 20.00/4.04 % (3070770)Termination reason: Instruction limit % 20.00/4.04 % (3070770)Termination phase: Saturation % 20.00/4.04 % (3070770)Time elapsed: 0.084 s % 20.00/4.04 % (3070770)Peak memory usage: 118 MB % 20.00/4.04 % (3070770)Instructions burned: 133 (million) % 20.00/4.04 % (3070772)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=1503528256:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 20.00/4.04 % (3070773)dis+10_1_si=on:random_seed=3669109746:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 20.00/4.04 % (3070775)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2591513891:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 20.00/4.04 % (3070772)Refutation not found, incomplete strategy % 20.00/4.04 % (3070772)------------------------------ % 20.00/4.04 % (3070772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.00/4.04 % (3070772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.00/4.04 % (3070772)CaDiCaL version: 2.1.3 % 20.00/4.04 % (3070772)Termination reason: Refutation not found, incomplete strategy % 24.42/4.42 % (3070772)Time elapsed: 0.046 s % 24.42/4.42 % (3070772)Peak memory usage: 111 MB % 24.42/4.42 % (3070772)Instructions burned: 16 (million) % 24.42/4.42 % (3070777)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=397864920:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 24.42/4.42 % (3070779)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4052328935:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 24.42/4.42 % (3070766)------------------------------ % 24.42/4.42 % (3070766)------------------------------ % 24.42/4.42 % (3070779)Refutation not found, incomplete strategy % 24.42/4.42 % (3070779)------------------------------ % 24.42/4.42 % (3070779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.42/4.42 % (3070779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.42/4.42 % (3070779)CaDiCaL version: 2.1.3 % 24.42/4.42 % (3070779)Termination reason: Refutation not found, incomplete strategy % 24.42/4.42 % (3070779)Time elapsed: 0.043 s % 24.42/4.42 % (3070779)Peak memory usage: 113 MB % 24.42/4.42 % (3070779)Instructions burned: 45 (million) % 24.42/4.42 % (3070777)Instruction limit reached! % 24.42/4.42 % (3070777)------------------------------ % 24.42/4.42 % (3070777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.42/4.42 % (3070777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.42/4.42 % (3070777)CaDiCaL version: 2.1.3 % 24.42/4.42 % (3070777)Termination reason: Instruction limit % 24.42/4.42 % (3070777)Termination phase: Saturation % 24.42/4.42 % (3070777)Time elapsed: 0.137 s % 24.42/4.42 % (3070777)Peak memory usage: 90 MB % 24.42/4.42 % (3070777)Instructions burned: 141 (million) % 24.42/4.42 % (3070775)Instruction limit reached! % 24.42/4.42 % (3070775)------------------------------ % 24.42/4.42 % (3070775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.42/4.42 % (3070775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.42/4.42 % (3070775)CaDiCaL version: 2.1.3 % 24.42/4.42 % (3070775)Termination reason: Instruction limit % 24.42/4.42 % (3070775)Termination phase: Saturation % 24.42/4.42 % (3070775)Time elapsed: 0.380 s % 24.42/4.42 % (3070775)Peak memory usage: 96 MB % 24.42/4.42 % (3070775)Instructions burned: 383 (million) % 24.42/4.42 % (3070772)------------------------------ % 24.42/4.42 % (3070772)------------------------------ % 24.42/4.42 % (3070779)------------------------------ % 24.42/4.42 % (3070779)------------------------------ % 24.42/4.42 % (3070786)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=50355549:i=121:nm=16:rtra=on_2977 on theBenchmark for (2977ds/121Mi) % 24.42/4.42 % (3070768)Instruction limit reached! % 24.42/4.42 % (3070768)------------------------------ % 24.42/4.42 % (3070768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.42/4.42 % (3070768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.42/4.42 % (3070768)CaDiCaL version: 2.1.3 % 24.42/4.42 % (3070768)Termination reason: Instruction limit % 24.42/4.42 % (3070768)Termination phase: Saturation % 24.42/4.42 % (3070768)Time elapsed: 0.666 s % 24.42/4.42 % (3070768)Peak memory usage: 141 MB % 24.42/4.42 % (3070768)Instructions burned: 598 (million) % 24.42/4.42 % (3070787)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=177963812:s2a=on:i=128:s2at=5:ins=3:rtra=on_2976 on theBenchmark for (2976ds/128Mi) % 24.42/4.43 % (3070787)Refutation not found, incomplete strategy % 24.42/4.43 % (3070787)------------------------------ % 24.42/4.43 % (3070787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.42/4.43 % (3070787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.42/4.43 % (3070787)CaDiCaL version: 2.1.3 % 24.42/4.43 % (3070787)Termination reason: Refutation not found, incomplete strategy % 24.42/4.43 % (3070787)Time elapsed: 0.070 s % 24.42/4.43 % (3070787)Peak memory usage: 114 MB % 24.42/4.43 % (3070787)Instructions burned: 52 (million) % 24.42/4.43 % (3070786)Instruction limit reached! % 24.42/4.43 % (3070786)------------------------------ % 24.42/4.43 % (3070786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.42/4.43 % (3070786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.42/4.43 % (3070786)CaDiCaL version: 2.1.3 % 24.42/4.43 % (3070786)Termination reason: Instruction limit % 24.42/4.43 % (3070786)Termination phase: Saturation % 24.42/4.43 % (3070786)Time elapsed: 0.112 s % 25.84/4.90 % (3070786)Peak memory usage: 90 MB % 25.84/4.90 % (3070786)Instructions burned: 121 (million) % 25.84/4.90 % (3070791)dis+1010_1_to=kbo:si=on:random_seed=2936544595:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 25.84/4.90 % (3070790)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=4241946414:i=39:ins=3:rtra=on_2975 on theBenchmark for (2975ds/39Mi) % 25.84/4.90 % (3070792)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2069040662:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/329Mi) % 25.84/4.90 % (3070790)Instruction limit reached! % 25.84/4.90 % (3070790)------------------------------ % 25.84/4.90 % (3070790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.90 % (3070790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.90 % (3070790)CaDiCaL version: 2.1.3 % 25.84/4.90 % (3070790)Termination reason: Instruction limit % 25.84/4.90 % (3070790)Termination phase: Saturation % 25.84/4.90 % (3070790)Time elapsed: 0.037 s % 25.84/4.90 % (3070790)Peak memory usage: 89 MB % 25.84/4.90 % (3070790)Instructions burned: 39 (million) % 25.84/4.90 % (3070795)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1212587150:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 25.84/4.90 % (3070791)Instruction limit reached! % 25.84/4.90 % (3070791)------------------------------ % 25.84/4.90 % (3070791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.90 % (3070791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.90 % (3070791)CaDiCaL version: 2.1.3 % 25.84/4.90 % (3070791)Termination reason: Instruction limit % 25.84/4.90 % (3070791)Termination phase: Saturation % 25.84/4.90 % (3070791)Time elapsed: 0.172 s % 25.84/4.90 % (3070791)Peak memory usage: 90 MB % 25.84/4.90 % (3070791)Instructions burned: 175 (million) % 25.84/4.90 % (3070792)Instruction limit reached! % 25.84/4.90 % (3070792)------------------------------ % 25.84/4.90 % (3070792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.90 % (3070792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.90 % (3070792)CaDiCaL version: 2.1.3 % 25.84/4.90 % (3070792)Termination reason: Instruction limit % 25.84/4.90 % (3070792)Termination phase: Saturation % 25.84/4.90 % (3070792)Time elapsed: 0.183 s % 25.84/4.90 % (3070792)Peak memory usage: 118 MB % 25.84/4.90 % (3070792)Instructions burned: 331 (million) % 25.84/4.90 % (3070773)Instruction limit reached! % 25.84/4.90 % (3070773)------------------------------ % 25.84/4.90 % (3070773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.90 % (3070773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.90 % (3070773)CaDiCaL version: 2.1.3 % 25.84/4.90 % (3070773)Termination reason: Instruction limit % 25.84/4.90 % (3070773)Termination phase: Saturation % 25.84/4.90 % (3070773)Time elapsed: 0.881 s % 25.84/4.90 % (3070773)Peak memory usage: 94 MB % 25.84/4.90 % (3070773)Instructions burned: 1000 (million) % 25.84/4.90 % (3070798)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=811058943:thitd=on:i=215:nm=0:rtra=on:ev=force_2973 on theBenchmark for (2973ds/215Mi) % 25.84/4.90 % (3070802)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=556490351:i=349:rtra=on_2972 on theBenchmark for (2972ds/349Mi) % 25.84/4.90 % (3070787)------------------------------ % 25.84/4.90 % (3070787)------------------------------ % 25.84/4.90 % (3070795)Instruction limit reached! % 25.84/4.90 % (3070795)------------------------------ % 25.84/4.90 % (3070795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.90 % (3070795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.90 % (3070795)CaDiCaL version: 2.1.3 % 25.84/4.90 % (3070795)Termination reason: Instruction limit % 25.84/4.90 % (3070795)Termination phase: Saturation % 25.84/4.90 % (3070795)Time elapsed: 0.352 s % 25.84/4.90 % (3070795)Peak memory usage: 137 MB % 25.84/4.90 % (3070795)Instructions burned: 484 (million) % 25.84/4.90 % (3070805)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=708123042:i=328:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/328Mi) % 25.84/4.90 % (3070804)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=959338152:st=2:i=295:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/295Mi) % 31.30/5.46 % (3070804)Refutation not found, incomplete strategy % 31.30/5.46 % (3070804)------------------------------ % 31.30/5.46 % (3070804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/5.46 % (3070804)CaDiCaL version: 2.1.3 % 31.30/5.46 % (3070804)Termination reason: Refutation not found, incomplete strategy % 31.30/5.46 % (3070804)Time elapsed: 0.011 s % 31.30/5.46 % (3070804)Peak memory usage: 88 MB % 31.30/5.46 % (3070804)Instructions burned: 11 (million) % 31.30/5.46 % (3070798)Instruction limit reached! % 31.30/5.46 % (3070798)------------------------------ % 31.30/5.46 % (3070798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/5.46 % (3070798)CaDiCaL version: 2.1.3 % 31.30/5.46 % (3070798)Termination reason: Instruction limit % 31.30/5.46 % (3070798)Termination phase: Saturation % 31.30/5.46 % (3070798)Time elapsed: 0.271 s % 31.30/5.46 % (3070798)Peak memory usage: 138 MB % 31.30/5.46 % (3070798)Instructions burned: 218 (million) % 31.30/5.46 % (3070807)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=53229408:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi) % 31.30/5.46 % (3070805)Instruction limit reached! % 31.30/5.46 % (3070805)------------------------------ % 31.30/5.46 % (3070805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/5.46 % (3070805)CaDiCaL version: 2.1.3 % 31.30/5.46 % (3070805)Termination reason: Instruction limit % 31.30/5.46 % (3070805)Termination phase: Saturation % 31.30/5.46 % (3070805)Time elapsed: 0.185 s % 31.30/5.46 % (3070805)Peak memory usage: 119 MB % 31.30/5.46 % (3070805)Instructions burned: 328 (million) % 31.30/5.46 % (3070809)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2597669295:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi) % 31.30/5.46 % (3070809)Refutation not found, incomplete strategy % 31.30/5.46 % (3070809)------------------------------ % 31.30/5.46 % (3070809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/5.46 % (3070809)CaDiCaL version: 2.1.3 % 31.30/5.46 % (3070809)Termination reason: Refutation not found, incomplete strategy % 31.30/5.46 % (3070809)Time elapsed: 0.010 s % 31.30/5.46 % (3070809)Peak memory usage: 87 MB % 31.30/5.46 % (3070809)Instructions burned: 11 (million) % 31.30/5.46 % (3070802)Instruction limit reached! % 31.30/5.46 % (3070802)------------------------------ % 31.30/5.46 % (3070802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/5.46 % (3070802)CaDiCaL version: 2.1.3 % 31.30/5.46 % (3070802)Termination reason: Instruction limit % 31.30/5.46 % (3070802)Termination phase: Saturation % 31.30/5.46 % (3070802)Time elapsed: 0.337 s % 31.30/5.46 % (3070802)Peak memory usage: 117 MB % 31.30/5.46 % (3070802)Instructions burned: 349 (million) % 31.30/5.46 % (3070811)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4110229567:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi) % 31.30/5.46 % (3070811)Refutation not found, incomplete strategy % 31.30/5.46 % (3070811)------------------------------ % 31.30/5.46 % (3070811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.30/5.46 % (3070811)CaDiCaL version: 2.1.3 % 31.30/5.46 % (3070811)Termination reason: Refutation not found, incomplete strategy % 31.30/5.46 % (3070811)Time elapsed: 0.047 s % 31.30/5.46 % (3070811)Peak memory usage: 112 MB % 31.30/5.46 % (3070811)Instructions burned: 15 (million) % 31.30/5.46 % (3070814)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4108139091:i=416:rtra=on:gtg=position:ss=axioms_2967 on theBenchmark for (2967ds/416Mi) % 31.30/5.46 % (3070807)Instruction limit reached! % 31.30/5.46 % (3070807)------------------------------ % 31.30/5.46 % (3070807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.30/5.46 % (3070807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.94 % (3070807)CaDiCaL version: 2.1.3 % 33.03/5.94 % (3070807)Termination reason: Instruction limit % 33.03/5.94 % (3070807)Termination phase: Saturation % 33.03/5.94 % (3070807)Time elapsed: 0.281 s % 33.03/5.94 % (3070807)Peak memory usage: 117 MB % 33.03/5.94 % (3070807)Instructions burned: 281 (million) % 33.03/5.94 % (3070804)------------------------------ % 33.03/5.94 % (3070804)------------------------------ % 33.03/5.94 % (3070815)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3491138367:i=471:thf=on:kws=precedence:rtra=on_2966 on theBenchmark for (2966ds/471Mi) % 33.03/5.94 % (3070814)Refutation not found, incomplete strategy % 33.03/5.94 % (3070814)------------------------------ % 33.03/5.94 % (3070814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.94 % (3070814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.94 % (3070814)CaDiCaL version: 2.1.3 % 33.03/5.94 % (3070814)Termination reason: Refutation not found, incomplete strategy % 33.03/5.94 % (3070814)Time elapsed: 0.046 s % 33.03/5.94 % (3070814)Peak memory usage: 111 MB % 33.03/5.94 % (3070814)Instructions burned: 15 (million) % 33.03/5.94 % (3070817)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=1010212104:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 33.03/5.94 % (3070809)------------------------------ % 33.03/5.94 % (3070809)------------------------------ % 33.03/5.94 % (3070811)------------------------------ % 33.03/5.94 % (3070811)------------------------------ % 33.03/5.94 % (3070817)Instruction limit reached! % 33.03/5.94 % (3070817)------------------------------ % 33.03/5.94 % (3070817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.94 % (3070817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.94 % (3070817)CaDiCaL version: 2.1.3 % 33.03/5.94 % (3070817)Termination reason: Instruction limit % 33.03/5.94 % (3070817)Termination phase: Saturation % 33.03/5.94 % (3070817)Time elapsed: 0.175 s % 33.03/5.94 % (3070817)Peak memory usage: 136 MB % 33.03/5.94 % (3070817)Instructions burned: 277 (million) % 33.03/5.94 % (3070821)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1538734415:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/387Mi) % 33.03/5.94 % (3070820)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3831334336:i=375:kws=inv_arity_squared:rtra=on_2964 on theBenchmark for (2964ds/375Mi) % 33.03/5.94 % (3070821)Refutation not found, incomplete strategy % 33.03/5.94 % (3070821)------------------------------ % 33.03/5.94 % (3070821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.94 % (3070821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.94 % (3070821)CaDiCaL version: 2.1.3 % 33.03/5.94 % (3070821)Termination reason: Refutation not found, incomplete strategy % 33.03/5.94 % (3070821)Time elapsed: 0.047 s % 33.03/5.94 % (3070821)Peak memory usage: 111 MB % 33.03/5.94 % (3070821)Instructions burned: 16 (million) % 33.03/5.94 % (3070825)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=59508651:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi) % 33.03/5.94 % (3070814)------------------------------ % 33.03/5.94 % (3070814)------------------------------ % 33.03/5.94 % (3070826)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3403533748:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 33.03/5.94 % (3070824)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=473955303:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2962 on theBenchmark for (2962ds/513Mi) % 33.03/5.94 % (3070815)Instruction limit reached! % 33.03/5.94 % (3070815)------------------------------ % 33.03/5.94 % (3070815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.94 % (3070815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.94 % (3070815)CaDiCaL version: 2.1.3 % 33.03/5.94 % (3070815)Termination reason: Instruction limit % 33.03/5.94 % (3070815)Termination phase: Saturation % 33.03/5.94 % (3070815)Time elapsed: 0.437 s % 33.03/5.94 % (3070815)Peak memory usage: 118 MB % 33.03/5.94 % (3070815)Instructions burned: 471 (million) % 39.57/6.62 % (3070825)Instruction limit reached! % 39.57/6.62 % (3070825)------------------------------ % 39.57/6.62 % (3070825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.57/6.62 % (3070825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.62 % (3070825)CaDiCaL version: 2.1.3 % 39.57/6.62 % (3070825)Termination reason: Instruction limit % 39.57/6.62 % (3070825)Termination phase: Saturation % 39.57/6.62 % (3070825)Time elapsed: 0.202 s % 39.57/6.62 % (3070825)Peak memory usage: 137 MB % 39.57/6.62 % (3070825)Instructions burned: 334 (million) % 39.57/6.62 % (3070820)Instruction limit reached! % 39.57/6.62 % (3070820)------------------------------ % 39.57/6.62 % (3070820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.57/6.62 % (3070820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.62 % (3070820)CaDiCaL version: 2.1.3 % 39.57/6.62 % (3070820)Termination reason: Instruction limit % 39.57/6.62 % (3070820)Termination phase: Saturation % 39.57/6.62 % (3070820)Time elapsed: 0.393 s % 39.57/6.62 % (3070820)Peak memory usage: 120 MB % 39.57/6.62 % (3070820)Instructions burned: 375 (million) % 39.57/6.62 % (3070831)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2702816810:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 39.57/6.62 % (3070821)------------------------------ % 39.57/6.62 % (3070821)------------------------------ % 39.57/6.62 % (3070833)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=176695019:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 39.57/6.62 % (3070833)Refutation not found, incomplete strategy % 39.57/6.62 % (3070833)------------------------------ % 39.57/6.62 % (3070833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.57/6.62 % (3070833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.62 % (3070833)CaDiCaL version: 2.1.3 % 39.57/6.62 % (3070833)Termination reason: Refutation not found, incomplete strategy % 39.57/6.62 % (3070833)Time elapsed: 0.042 s % 39.57/6.62 % (3070833)Peak memory usage: 111 MB % 39.57/6.62 % (3070833)Instructions burned: 11 (million) % 39.57/6.62 % (3070826)Instruction limit reached! % 39.57/6.62 % (3070826)------------------------------ % 39.57/6.62 % (3070826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.57/6.62 % (3070826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.62 % (3070826)CaDiCaL version: 2.1.3 % 39.57/6.62 % (3070826)Termination reason: Instruction limit % 39.57/6.62 % (3070826)Termination phase: Saturation % 39.57/6.62 % (3070826)Time elapsed: 0.335 s % 39.57/6.62 % (3070826)Peak memory usage: 91 MB % 39.57/6.62 % (3070826)Instructions burned: 360 (million) % 39.57/6.62 % (3070834)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=3245279511:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2958 on theBenchmark for (2958ds/235Mi) % 39.57/6.62 % (3070834)Refutation not found, incomplete strategy % 39.57/6.62 % (3070834)------------------------------ % 39.57/6.62 % (3070834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.57/6.62 % (3070834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.62 % (3070834)CaDiCaL version: 2.1.3 % 39.57/6.62 % (3070834)Termination reason: Refutation not found, incomplete strategy % 39.57/6.62 % (3070834)Time elapsed: 0.035 s % 39.57/6.62 % (3070834)Peak memory usage: 111 MB % 39.57/6.62 % (3070834)Instructions burned: 16 (million) % 39.57/6.62 % (3070835)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=750373914:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 39.57/6.62 % (3070824)Instruction limit reached! % 39.57/6.62 % (3070824)------------------------------ % 39.57/6.62 % (3070824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.57/6.62 % (3070824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.62 % (3070824)CaDiCaL version: 2.1.3 % 39.57/6.62 % (3070824)Termination reason: Instruction limit % 39.57/6.62 % (3070824)Termination phase: Saturation % 39.57/6.62 % (3070824)Time elapsed: 0.525 s % 39.57/6.62 % (3070824)Peak memory usage: 94 MB % 39.57/6.62 % (3070824)Instructions burned: 513 (million) % 39.57/6.62 % (3070835)Instruction limit reached! % 45.11/7.35 % (3070835)------------------------------ % 45.11/7.35 % (3070835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.11/7.35 % (3070835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.11/7.35 % (3070835)CaDiCaL version: 2.1.3 % 45.11/7.35 % (3070835)Termination reason: Instruction limit % 45.11/7.35 % (3070835)Termination phase: Saturation % 45.11/7.35 % (3070835)Time elapsed: 0.122 s % 45.11/7.35 % (3070835)Peak memory usage: 92 MB % 45.11/7.35 % (3070835)Instructions burned: 275 (million) % 45.11/7.35 % (3070838)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1233634556:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi) % 45.11/7.35 % (3070831)Instruction limit reached! % 45.11/7.35 % (3070831)------------------------------ % 45.11/7.35 % (3070831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.11/7.35 % (3070831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.11/7.35 % (3070831)CaDiCaL version: 2.1.3 % 45.11/7.35 % (3070831)Termination reason: Instruction limit % 45.11/7.35 % (3070831)Termination phase: Saturation % 45.11/7.35 % (3070831)Time elapsed: 0.373 s % 45.11/7.35 % (3070831)Peak memory usage: 124 MB % 45.11/7.35 % (3070831)Instructions burned: 341 (million) % 45.11/7.35 % (3070839)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4274051517:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi) % 45.11/7.35 % (3070833)------------------------------ % 45.11/7.35 % (3070833)------------------------------ % 45.11/7.35 % (3070834)------------------------------ % 45.11/7.35 % (3070834)------------------------------ % 45.11/7.35 % (3070838)Instruction limit reached! % 45.11/7.35 % (3070838)------------------------------ % 45.11/7.35 % (3070838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.11/7.35 % (3070838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.11/7.35 % (3070838)CaDiCaL version: 2.1.3 % 45.11/7.35 % (3070838)Termination reason: Instruction limit % 45.11/7.35 % (3070838)Termination phase: Saturation % 45.11/7.35 % (3070838)Time elapsed: 0.147 s % 45.11/7.35 % (3070838)Peak memory usage: 90 MB % 45.11/7.35 % (3070838)Instructions burned: 146 (million) % 45.11/7.35 % (3070843)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=3783568994:avsq=on:i=276:avsqr=1,2:rtra=on_2954 on theBenchmark for (2954ds/276Mi) % 45.11/7.35 % (3070847)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1601607233:i=1052:rtra=on_2954 on theBenchmark for (2954ds/1052Mi) % 45.11/7.35 % (3070849)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=851243091:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/655Mi) % 45.11/7.35 % (3070850)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3801294615:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2953 on theBenchmark for (2953ds/1054Mi) % 45.11/7.35 % (3070850)Refutation not found, incomplete strategy % 45.11/7.35 % (3070850)------------------------------ % 45.11/7.35 % (3070850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.11/7.35 % (3070850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.11/7.35 % (3070850)CaDiCaL version: 2.1.3 % 45.11/7.35 % (3070850)Termination reason: Refutation not found, incomplete strategy % 45.11/7.35 % (3070850)Time elapsed: 0.007 s % 45.11/7.35 % (3070850)Peak memory usage: 87 MB % 45.11/7.35 % (3070850)Instructions burned: 7 (million) % 45.11/7.35 % (3070851)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3228236984:i=107:rtra=on_2953 on theBenchmark for (2953ds/107Mi) % 45.11/7.35 % (3070852)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2882303753:s2a=on:i=450:doe=on:nm=32:rtra=on_2952 on theBenchmark for (2952ds/450Mi) % 45.11/7.35 % (3070851)Refutation not found, incomplete strategy % 45.11/7.35 % (3070851)------------------------------ % 45.11/7.35 % (3070851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.11/7.35 % (3070851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.11/7.35 % (3070851)CaDiCaL version: 2.1.3 % 45.11/7.35 % (3070851)Termination reason: Refutation not found, incomplete strategy % 45.11/7.35 % (3070851)Time elapsed: 0.077 s % 45.11/7.35 % (3070851)Peak memory usage: 113 MB % 50.91/8.09 % (3070851)Instructions burned: 48 (million) % 50.91/8.09 % (3070843)Instruction limit reached! % 50.91/8.09 % (3070843)------------------------------ % 50.91/8.09 % (3070843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.91/8.09 % (3070843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.91/8.09 % (3070843)CaDiCaL version: 2.1.3 % 50.91/8.09 % (3070843)Termination reason: Instruction limit % 50.91/8.09 % (3070843)Termination phase: Saturation % 50.91/8.09 % (3070843)Time elapsed: 0.308 s % 50.91/8.09 % (3070843)Peak memory usage: 135 MB % 50.91/8.09 % (3070843)Instructions burned: 276 (million) % 50.91/8.09 % (3070847)Instruction limit reached! % 50.91/8.09 % (3070847)------------------------------ % 50.91/8.09 % (3070847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.91/8.09 % (3070847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.91/8.09 % (3070847)CaDiCaL version: 2.1.3 % 50.91/8.09 % (3070847)Termination reason: Instruction limit % 50.91/8.09 % (3070847)Termination phase: Saturation % 50.91/8.09 % (3070847)Time elapsed: 0.489 s % 50.91/8.09 % (3070847)Peak memory usage: 96 MB % 50.91/8.09 % (3070847)Instructions burned: 1052 (million) % 50.91/8.09 % (3070850)------------------------------ % 50.91/8.09 % (3070850)------------------------------ % 50.91/8.09 % (3070860)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 % 50.91/8.09 % (3070860)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3059882115:i=1090:aac=none:nm=0:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/1090Mi) % 50.91/8.09 % (3070849)Instruction limit reached! % 50.91/8.09 % (3070849)------------------------------ % 50.91/8.09 % (3070849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.91/8.09 % (3070849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.91/8.09 % (3070849)CaDiCaL version: 2.1.3 % 50.91/8.09 % (3070849)Termination reason: Instruction limit % 50.91/8.09 % (3070849)Termination phase: Saturation % 50.91/8.09 % (3070849)Time elapsed: 0.529 s % 50.91/8.09 % (3070849)Peak memory usage: 91 MB % 50.91/8.09 % (3070849)Instructions burned: 655 (million) % 50.91/8.09 % (3070851)------------------------------ % 50.91/8.09 % (3070851)------------------------------ % 50.91/8.09 % (3070852)Instruction limit reached! % 50.91/8.09 % (3070852)------------------------------ % 50.91/8.09 % (3070852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.91/8.09 % (3070852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.91/8.09 % (3070852)CaDiCaL version: 2.1.3 % 50.91/8.09 % (3070852)Termination reason: Instruction limit % 50.91/8.09 % (3070852)Termination phase: Saturation % 50.91/8.09 % (3070852)Time elapsed: 0.478 s % 50.91/8.09 % (3070852)Peak memory usage: 137 MB % 50.91/8.09 % (3070852)Instructions burned: 450 (million) % 50.91/8.09 % (3070861)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=539371728:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2947 on theBenchmark for (2947ds/130Mi) % 50.91/8.09 % (3070861)Instruction limit reached! % 50.91/8.09 % (3070861)------------------------------ % 50.91/8.09 % (3070861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.91/8.09 % (3070861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.91/8.09 % (3070861)CaDiCaL version: 2.1.3 % 50.91/8.09 % (3070861)Termination reason: Instruction limit % 50.91/8.09 % (3070861)Termination phase: Saturation % 50.91/8.09 % (3070861)Time elapsed: 0.085 s % 50.91/8.09 % (3070861)Peak memory usage: 117 MB % 50.91/8.09 % (3070861)Instructions burned: 130 (million) % 50.91/8.09 % (3070862)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1328358031:i=312:kws=inv_frequency:nm=20:rtra=on_2946 on theBenchmark for (2946ds/312Mi) % 50.91/8.09 % (3070864)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=620784248:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 50.91/8.09 % (3070865)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3928589971:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 50.91/8.09 % (3070864)Refutation not found, incomplete strategy % 50.91/8.09 % (3070864)------------------------------ % 50.91/8.09 % (3070864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/9.02 % (3070864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/9.02 % (3070864)CaDiCaL version: 2.1.3 % 55.77/9.02 % (3070864)Termination reason: Refutation not found, incomplete strategy % 55.77/9.02 % (3070864)Time elapsed: 0.046 s % 55.77/9.02 % (3070864)Peak memory usage: 89 MB % 55.77/9.02 % (3070864)Instructions burned: 47 (million) % 55.77/9.02 % (3070867)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2224042124:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2945 on theBenchmark for (2945ds/307Mi) % 55.77/9.02 % (3070869)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1220389889:i=776:doe=on:rtra=on_2944 on theBenchmark for (2944ds/776Mi) % 55.77/9.02 % (3070867)Refutation not found, incomplete strategy % 55.77/9.02 % (3070867)------------------------------ % 55.77/9.02 % (3070867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/9.02 % (3070867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/9.02 % (3070867)CaDiCaL version: 2.1.3 % 55.77/9.02 % (3070867)Termination reason: Refutation not found, incomplete strategy % 55.77/9.02 % (3070867)Time elapsed: 0.054 s % 55.77/9.02 % (3070867)Peak memory usage: 89 MB % 55.77/9.02 % (3070867)Instructions burned: 55 (million) % 55.77/9.02 % (3070862)Instruction limit reached! % 55.77/9.02 % (3070862)------------------------------ % 55.77/9.02 % (3070862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/9.02 % (3070862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/9.02 % (3070862)CaDiCaL version: 2.1.3 % 55.77/9.02 % (3070862)Termination reason: Instruction limit % 55.77/9.02 % (3070862)Termination phase: Saturation % 55.77/9.02 % (3070862)Time elapsed: 0.326 s % 55.77/9.02 % (3070862)Peak memory usage: 118 MB % 55.77/9.02 % (3070862)Instructions burned: 314 (million) % 55.77/9.02 % (3070864)------------------------------ % 55.77/9.02 % (3070864)------------------------------ % 55.77/9.02 % (3070874)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3886641881:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 55.77/9.02 % (3070867)------------------------------ % 55.77/9.02 % (3070867)------------------------------ % 55.77/9.02 % (3070869)Instruction limit reached! % 55.77/9.02 % (3070869)------------------------------ % 55.77/9.02 % (3070869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/9.02 % (3070869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/9.02 % (3070869)CaDiCaL version: 2.1.3 % 55.77/9.02 % (3070869)Termination reason: Instruction limit % 55.77/9.02 % (3070869)Termination phase: Saturation % 55.77/9.02 % (3070869)Time elapsed: 0.417 s % 55.77/9.02 % (3070869)Peak memory usage: 123 MB % 55.77/9.02 % (3070869)Instructions burned: 777 (million) % 55.77/9.02 % (3070860)Instruction limit reached! % 55.77/9.02 % (3070860)------------------------------ % 55.77/9.02 % (3070860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/9.02 % (3070860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/9.02 % (3070860)CaDiCaL version: 2.1.3 % 55.77/9.02 % (3070860)Termination reason: Instruction limit % 55.77/9.02 % (3070860)Termination phase: Saturation % 55.77/9.02 % (3070860)Time elapsed: 1.028 s % 55.77/9.02 % (3070860)Peak memory usage: 126 MB % 55.77/9.02 % (3070860)Instructions burned: 1090 (million) % 55.77/9.02 % (3070875)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=3089828217:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2938 on theBenchmark for (2938ds/784Mi) % 55.77/9.02 % (3070877)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=893307596:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2937 on theBenchmark for (2937ds/1131Mi) % 55.77/9.02 % (3070865)Instruction limit reached! % 55.77/9.02 % (3070865)------------------------------ % 55.77/9.02 % (3070865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.77/9.02 % (3070865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.77/9.02 % (3070865)CaDiCaL version: 2.1.3 % 55.77/9.02 % (3070865)Termination reason: Instruction limit % 55.77/9.02 % (3070865)Termination phase: Saturation % 55.77/9.02 % (3070865)Time elapsed: 0.739 s % 55.77/9.02 % (3070865)Peak memory usage: 95 MB % 66.85/10.37 % (3070865)Instructions burned: 835 (million) % 66.85/10.37 % (3070878)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=1040757618:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi) % 66.85/10.37 % (3070878)Refutation not found, incomplete strategy % 66.85/10.37 % (3070878)------------------------------ % 66.85/10.37 % (3070878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.85/10.37 % (3070878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.85/10.37 % (3070878)CaDiCaL version: 2.1.3 % 66.85/10.37 % (3070878)Termination reason: Refutation not found, incomplete strategy % 66.85/10.37 % (3070878)Time elapsed: 0.047 s % 66.85/10.37 % (3070878)Peak memory usage: 112 MB % 66.85/10.37 % (3070878)Instructions burned: 16 (million) % 66.85/10.37 % (3070881)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=292388753:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/775Mi) % 66.85/10.37 % (3070881)Refutation not found, incomplete strategy % 66.85/10.37 % (3070881)------------------------------ % 66.85/10.37 % (3070881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.85/10.37 % (3070881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.85/10.37 % (3070881)CaDiCaL version: 2.1.3 % 66.85/10.37 % (3070881)Termination reason: Refutation not found, incomplete strategy % 66.85/10.37 % (3070881)Time elapsed: 0.012 s % 66.85/10.37 % (3070881)Peak memory usage: 88 MB % 66.85/10.37 % (3070881)Instructions burned: 12 (million) % 66.85/10.37 % (3070883)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2880174554:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi) % 66.85/10.37 % (3070878)------------------------------ % 66.85/10.37 % (3070878)------------------------------ % 66.85/10.37 % (3070874)Instruction limit reached! % 66.85/10.37 % (3070874)------------------------------ % 66.85/10.37 % (3070874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.85/10.37 % (3070874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.85/10.37 % (3070874)CaDiCaL version: 2.1.3 % 66.85/10.37 % (3070874)Termination reason: Instruction limit % 66.85/10.37 % (3070874)Termination phase: Saturation % 66.85/10.37 % (3070874)Time elapsed: 0.698 s % 66.85/10.37 % (3070874)Peak memory usage: 141 MB % 66.85/10.37 % (3070874)Instructions burned: 647 (million) % 66.85/10.37 % (3070883)Instruction limit reached! % 66.85/10.37 % (3070883)------------------------------ % 66.85/10.37 % (3070883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.85/10.37 % (3070883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.85/10.37 % (3070883)CaDiCaL version: 2.1.3 % 66.85/10.37 % (3070883)Termination reason: Instruction limit % 66.85/10.37 % (3070883)Termination phase: Saturation % 66.85/10.37 % (3070883)Time elapsed: 0.264 s % 66.85/10.37 % (3070883)Peak memory usage: 91 MB % 66.85/10.37 % (3070883)Instructions burned: 273 (million) % 66.85/10.37 % (3070877)Instruction limit reached! % 66.85/10.37 % (3070877)------------------------------ % 66.85/10.37 % (3070877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.85/10.37 % (3070877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.85/10.37 % (3070877)CaDiCaL version: 2.1.3 % 66.85/10.37 % (3070877)Termination reason: Instruction limit % 66.85/10.37 % (3070877)Termination phase: Saturation % 66.85/10.37 % (3070877)Time elapsed: 0.625 s % 66.85/10.37 % (3070877)Peak memory usage: 133 MB % 66.85/10.37 % (3070877)Instructions burned: 1132 (million) % 66.85/10.37 % (3070881)------------------------------ % 66.85/10.37 % (3070881)------------------------------ % 66.85/10.37 % (3070889)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=916951675:i=102:nm=16:rtra=on_2931 on theBenchmark for (2931ds/102Mi) % 66.85/10.37 % (3070891)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2898934367:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2930 on theBenchmark for (2930ds/1094Mi) % 66.85/10.37 % (3070875)Instruction limit reached! % 66.85/10.37 % (3070875)------------------------------ % 66.85/10.37 % (3070875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.85/10.37 % (3070875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.85/10.37 % (3070875)CaDiCaL version: 2.1.3 % 87.05/13.15 % (3070875)Termination reason: Instruction limit % 87.05/13.15 % (3070875)Termination phase: Saturation % 87.05/13.15 % (3070875)Time elapsed: 0.773 s % 87.05/13.15 % (3070875)Peak memory usage: 123 MB % 87.05/13.15 % (3070875)Instructions burned: 784 (million) % 87.05/13.15 % (3070894)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2324329049:i=6400:doe=on:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/6400Mi) % 87.05/13.15 % (3070889)Instruction limit reached! % 87.05/13.15 % (3070889)------------------------------ % 87.05/13.15 % (3070889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.05/13.15 % (3070889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.05/13.15 % (3070889)CaDiCaL version: 2.1.3 % 87.05/13.15 % (3070889)Termination reason: Instruction limit % 87.05/13.15 % (3070889)Termination phase: Saturation % 87.05/13.15 % (3070889)Time elapsed: 0.088 s % 87.05/13.15 % (3070889)Peak memory usage: 90 MB % 87.05/13.15 % (3070889)Instructions burned: 102 (million) % 87.05/13.15 % (3070895)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=110390877:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi) % 87.05/13.15 % (3070896)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=587594933:i=1846:canc=cautious:fsr=off:rtra=on_2928 on theBenchmark for (2928ds/1846Mi) % 87.05/13.15 % (3070902)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4244229211:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2927 on theBenchmark for (2927ds/273Mi) % 87.05/13.15 % (3070896)Refutation not found, incomplete strategy % 87.05/13.15 % (3070896)------------------------------ % 87.05/13.15 % (3070896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.05/13.15 % (3070896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.05/13.15 % (3070896)CaDiCaL version: 2.1.3 % 87.05/13.15 % (3070896)Termination reason: Refutation not found, incomplete strategy % 87.05/13.15 % (3070896)Time elapsed: 0.040 s % 87.05/13.15 % (3070896)Peak memory usage: 89 MB % 87.05/13.15 % (3070896)Instructions burned: 43 (million) % 87.05/13.15 % (3070901)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4041196803:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2928 on theBenchmark for (2928ds/36816Mi) % 87.05/13.15 % (3070902)Instruction limit reached! % 87.05/13.15 % (3070902)------------------------------ % 87.05/13.15 % (3070902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.05/13.15 % (3070902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.05/13.15 % (3070902)CaDiCaL version: 2.1.3 % 87.05/13.15 % (3070902)Termination reason: Instruction limit % 87.05/13.15 % (3070902)Termination phase: Saturation % 87.05/13.15 % (3070902)Time elapsed: 0.274 s % 87.05/13.15 % (3070902)Peak memory usage: 91 MB % 87.05/13.15 % (3070902)Instructions burned: 273 (million) % 87.05/13.15 % (3070896)------------------------------ % 87.05/13.15 % (3070896)------------------------------ % 87.05/13.15 % (3070908)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=606521914:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2923 on theBenchmark for (2923ds/863Mi) % 87.05/13.15 % (3070910)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=545454954:i=5811:kws=precedence:nm=0:rtra=on_2921 on theBenchmark for (2921ds/5811Mi) % 87.05/13.15 % (3070891)Instruction limit reached! % 87.05/13.15 % (3070891)------------------------------ % 87.05/13.15 % (3070891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.05/13.15 % (3070891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.05/13.15 % (3070891)CaDiCaL version: 2.1.3 % 87.05/13.15 % (3070891)Termination reason: Instruction limit % 87.05/13.15 % (3070891)Termination phase: Saturation % 87.05/13.15 % (3070891)Time elapsed: 0.913 s % 87.05/13.15 % (3070891)Peak memory usage: 92 MB % 87.05/13.15 % (3070891)Instructions burned: 1094 (million) % 87.05/13.15 % (3070895)Instruction limit reached! % 87.05/13.15 % (3070895)------------------------------ % 87.05/13.15 % (3070895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.05/13.15 % (3070895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.05/13.15 % (3070895)CaDiCaL version: 2.1.3 % 94.41/14.28 % (3070895)Termination reason: Instruction limit % 94.41/14.28 % (3070895)Termination phase: Saturation % 94.41/14.28 % (3070895)Time elapsed: 0.795 s % 94.41/14.28 % (3070895)Peak memory usage: 121 MB % 94.41/14.28 % (3070895)Instructions burned: 869 (million) % 94.41/14.28 % (3070839)Instruction limit reached! % 94.41/14.28 % (3070839)------------------------------ % 94.41/14.28 % (3070839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.41/14.28 % (3070839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.41/14.28 % (3070839)CaDiCaL version: 2.1.3 % 94.41/14.28 % (3070839)Termination reason: Instruction limit % 94.41/14.28 % (3070839)Termination phase: Saturation % 94.41/14.28 % (3070839)Time elapsed: 3.563 s % 94.41/14.28 % (3070839)Peak memory usage: 105 MB % 94.41/14.28 % (3070839)Instructions burned: 4428 (million) % 94.41/14.28 % (3070915)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=1736823097:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2918 on theBenchmark for (2918ds/2216Mi) % 94.41/14.28 % (3070916)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3644402655:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2918 on theBenchmark for (2918ds/801Mi) % 94.41/14.28 % (3070917)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=909635786:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2918 on theBenchmark for (2918ds/1026Mi) % 94.41/14.28 % (3070917)Refutation not found, incomplete strategy % 94.41/14.28 % (3070917)------------------------------ % 94.41/14.28 % (3070917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.41/14.28 % (3070917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.41/14.28 % (3070917)CaDiCaL version: 2.1.3 % 94.41/14.28 % (3070917)Termination reason: Refutation not found, incomplete strategy % 94.41/14.28 % (3070917)Time elapsed: 0.007 s % 94.41/14.28 % (3070917)Peak memory usage: 87 MB % 94.41/14.28 % (3070917)Instructions burned: 7 (million) % 94.41/14.28 % (3070908)Instruction limit reached! % 94.41/14.28 % (3070908)------------------------------ % 94.41/14.28 % (3070908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.41/14.28 % (3070908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.41/14.28 % (3070908)CaDiCaL version: 2.1.3 % 94.41/14.28 % (3070908)Termination reason: Instruction limit % 94.41/14.28 % (3070908)Termination phase: Saturation % 94.41/14.28 % (3070908)Time elapsed: 0.750 s % 94.41/14.28 % (3070908)Peak memory usage: 121 MB % 94.41/14.28 % (3070908)Instructions burned: 864 (million) % 94.41/14.28 % (3070917)------------------------------ % 94.41/14.28 % (3070917)------------------------------ % 94.41/14.28 % (3070922)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2048873842:i=3509:rtra=on_2912 on theBenchmark for (2912ds/3509Mi) % 94.41/14.28 % (3070916)Instruction limit reached! % 94.41/14.28 % (3070916)------------------------------ % 94.41/14.28 % (3070916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.41/14.28 % (3070916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.41/14.28 % (3070916)CaDiCaL version: 2.1.3 % 94.41/14.28 % (3070916)Termination reason: Instruction limit % 94.41/14.28 % (3070916)Termination phase: Saturation % 94.41/14.28 % (3070916)Time elapsed: 0.655 s % 94.41/14.28 % (3070916)Peak memory usage: 91 MB % 94.41/14.28 % (3070916)Instructions burned: 802 (million) % 94.41/14.28 % (3070923)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4012600942:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/2127Mi) % 94.41/14.28 % (3070923)Refutation not found, incomplete strategy % 94.41/14.28 % (3070923)------------------------------ % 94.41/14.28 % (3070923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.41/14.28 % (3070923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.41/14.28 % (3070923)CaDiCaL version: 2.1.3 % 94.41/14.28 % (3070923)Termination reason: Refutation not found, incomplete strategy % 94.41/14.28 % (3070923)Time elapsed: 0.011 s % 94.41/14.28 % (3070923)Peak memory usage: 87 MB % 94.41/14.28 % (3070923)Instructions burned: 11 (million) % 94.41/14.28 % (3070925)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3411356409:i=1959:rtra=on:fsd=on:proc=on_2909 on theBenchmark for (2909ds/1959Mi) % 94.41/14.28 % (3070923)------------------------------ % 94.41/14.28 % (3070923)------------------------------ % 131.96/19.50 % (3070894)Instruction limit reached! % 131.96/19.50 % (3070894)------------------------------ % 131.96/19.50 % (3070894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (3070894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (3070894)CaDiCaL version: 2.1.3 % 131.96/19.50 % (3070894)Termination reason: Instruction limit % 131.96/19.50 % (3070894)Termination phase: Saturation % 131.96/19.50 % (3070894)Time elapsed: 2.438 s % 131.96/19.50 % (3070894)Peak memory usage: 117 MB % 131.96/19.50 % (3070894)Instructions burned: 6400 (million) % 131.96/19.50 % (3070929)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3843964985:s2a=on:i=3553:nm=0:rtra=on_2905 on theBenchmark for (2905ds/3553Mi) % 131.96/19.50 % (3070931)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3351804423:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2903 on theBenchmark for (2903ds/3201Mi) % 131.96/19.50 % (3070915)Instruction limit reached! % 131.96/19.50 % (3070915)------------------------------ % 131.96/19.50 % (3070915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (3070915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (3070915)CaDiCaL version: 2.1.3 % 131.96/19.50 % (3070915)Termination reason: Instruction limit % 131.96/19.50 % (3070915)Termination phase: Saturation % 131.96/19.50 % (3070915)Time elapsed: 2.073 s % 131.96/19.50 % (3070915)Peak memory usage: 140 MB % 131.96/19.50 % (3070915)Instructions burned: 2216 (million) % 131.96/19.50 % (3070938)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=4002158050:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2895 on theBenchmark for (2895ds/4093Mi) % 131.96/19.50 % (3070931)Refutation not found, incomplete strategy % 131.96/19.50 % (3070931)------------------------------ % 131.96/19.50 % (3070931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (3070931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (3070931)CaDiCaL version: 2.1.3 % 131.96/19.50 % (3070931)Termination reason: Refutation not found, incomplete strategy % 131.96/19.50 % (3070931)Time elapsed: 0.970 s % 131.96/19.50 % (3070931)Peak memory usage: 97 MB % 131.96/19.50 % (3070931)Instructions burned: 2004 (million) % 131.96/19.50 % (3070925)Instruction limit reached! % 131.96/19.50 % (3070925)------------------------------ % 131.96/19.50 % (3070925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (3070925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (3070925)CaDiCaL version: 2.1.3 % 131.96/19.50 % (3070925)Termination reason: Instruction limit % 131.96/19.50 % (3070925)Termination phase: Saturation % 131.96/19.50 % (3070925)Time elapsed: 1.792 s % 131.96/19.50 % (3070925)Peak memory usage: 137 MB % 131.96/19.50 % (3070925)Instructions burned: 1959 (million) % 131.96/19.50 % (3070931)------------------------------ % 131.96/19.50 % (3070931)------------------------------ % 131.96/19.50 % (3070942)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=3274929925:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2888 on theBenchmark for (2888ds/21173Mi) % 131.96/19.50 % (3070942)Refutation not found, incomplete strategy % 131.96/19.50 % (3070942)------------------------------ % 131.96/19.50 % (3070942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (3070942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (3070942)CaDiCaL version: 2.1.3 % 131.96/19.50 % (3070942)Termination reason: Refutation not found, incomplete strategy % 131.96/19.50 % (3070942)Time elapsed: 0.043 s % 131.96/19.50 % (3070942)Peak memory usage: 113 MB % 131.96/19.50 % (3070942)Instructions burned: 11 (million) % 131.96/19.50 % (3070943)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3778364112:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2887 on theBenchmark for (2887ds/10544Mi) % 131.96/19.50 % (3070942)------------------------------ % 131.96/19.50 % (3070942)------------------------------ % 131.96/19.50 % (3070946)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=739297507:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2880 on theBenchmark for (2880ds/1262Mi) % 131.96/19.50 % (3070922)Instruction limit reached! % 155.44/22.84 % (3070922)------------------------------ % 155.44/22.84 % (3070922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.44/22.84 % (3070922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.84 % (3070922)CaDiCaL version: 2.1.3 % 155.44/22.84 % (3070922)Termination reason: Instruction limit % 155.44/22.84 % (3070922)Termination phase: Saturation % 155.44/22.84 % (3070922)Time elapsed: 3.297 s % 155.44/22.84 % (3070922)Peak memory usage: 111 MB % 155.44/22.84 % (3070922)Instructions burned: 3510 (million) % 155.44/22.84 % (3070948)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2795726869:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2877 on theBenchmark for (2877ds/775Mi) % 155.44/22.84 % (3070948)Refutation not found, incomplete strategy % 155.44/22.84 % (3070948)------------------------------ % 155.44/22.84 % (3070948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.44/22.84 % (3070948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.84 % (3070948)CaDiCaL version: 2.1.3 % 155.44/22.84 % (3070948)Termination reason: Refutation not found, incomplete strategy % 155.44/22.84 % (3070948)Time elapsed: 0.012 s % 155.44/22.84 % (3070948)Peak memory usage: 88 MB % 155.44/22.84 % (3070948)Instructions burned: 12 (million) % 155.44/22.84 % (3070910)Instruction limit reached! % 155.44/22.84 % (3070910)------------------------------ % 155.44/22.84 % (3070910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.44/22.84 % (3070910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.84 % (3070910)CaDiCaL version: 2.1.3 % 155.44/22.84 % (3070910)Termination reason: Instruction limit % 155.44/22.84 % (3070910)Termination phase: Saturation % 155.44/22.84 % (3070910)Time elapsed: 4.779 s % 155.44/22.84 % (3070910)Peak memory usage: 137 MB % 155.44/22.84 % (3070910)Instructions burned: 5811 (million) % 155.44/22.84 % (3070948)------------------------------ % 155.44/22.84 % (3070948)------------------------------ % 155.44/22.84 % (3070938)Instruction limit reached! % 155.44/22.84 % (3070938)------------------------------ % 155.44/22.84 % (3070938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.44/22.84 % (3070938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.84 % (3070938)CaDiCaL version: 2.1.3 % 155.44/22.84 % (3070938)Termination reason: Instruction limit % 155.44/22.84 % (3070938)Termination phase: Saturation % 155.44/22.84 % (3070938)Time elapsed: 2.293 s % 155.44/22.84 % (3070938)Peak memory usage: 170 MB % 155.44/22.84 % (3070938)Instructions burned: 4093 (million) % 155.44/22.84 % (3070952)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3559186735:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2871 on theBenchmark for (2871ds/270Mi) % 155.44/22.84 % (3070953)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=4235862833:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2870 on theBenchmark for (2870ds/17165Mi) % 155.44/22.84 % (3070929)Instruction limit reached! % 155.44/22.84 % (3070929)------------------------------ % 155.44/22.84 % (3070929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.44/22.84 % (3070929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.84 % (3070929)CaDiCaL version: 2.1.3 % 155.44/22.84 % (3070929)Termination reason: Instruction limit % 155.44/22.84 % (3070929)Termination phase: Saturation % 155.44/22.84 % (3070929)Time elapsed: 3.376 s % 155.44/22.84 % (3070929)Peak memory usage: 113 MB % 155.44/22.84 % (3070929)Instructions burned: 3554 (million) % 155.44/22.84 % (3070954)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2900017236:s2a=on:i=13094:s2at=-1:rtra=on_2869 on theBenchmark for (2869ds/13094Mi) % 155.44/22.84 % (3070946)Instruction limit reached! % 155.44/22.84 % (3070946)------------------------------ % 155.44/22.84 % (3070946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.44/22.84 % (3070946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.84 % (3070946)CaDiCaL version: 2.1.3 % 155.44/22.84 % (3070946)Termination reason: Instruction limit % 155.44/22.84 % (3070946)Termination phase: Saturation % 155.44/22.84 % (3070946)Time elapsed: 1.167 s % 155.44/22.84 % (3070946)Peak memory usage: 123 MB % 155.44/22.84 % (3070946)Instructions burned: 1262 (million) % 155.44/22.84 % (3070952)Instruction limit reached! % 155.44/22.84 % (3070952)------------------------------ % 155.44/22.84 % (3070952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.89/26.81 % (3070952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.89/26.81 % (3070952)CaDiCaL version: 2.1.3 % 183.89/26.81 % (3070952)Termination reason: Instruction limit % 183.89/26.81 % (3070952)Termination phase: Saturation % 183.89/26.81 % (3070952)Time elapsed: 0.268 s % 183.89/26.81 % (3070952)Peak memory usage: 92 MB % 183.89/26.81 % (3070952)Instructions burned: 270 (million) % 183.89/26.81 % (3070957)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=914791348:st=2:i=12633:rtra=on:ss=axioms_2868 on theBenchmark for (2868ds/12633Mi) % 183.89/26.81 % (3070957)Refutation not found, incomplete strategy % 183.89/26.81 % (3070957)------------------------------ % 183.89/26.81 % (3070957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.89/26.81 % (3070957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.89/26.81 % (3070957)CaDiCaL version: 2.1.3 % 183.89/26.81 % (3070957)Termination reason: Refutation not found, incomplete strategy % 183.89/26.81 % (3070957)Time elapsed: 0.011 s % 183.89/26.81 % (3070957)Peak memory usage: 88 MB % 183.89/26.81 % (3070957)Instructions burned: 10 (million) % 183.89/26.81 % (3070960)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3541579131:i=1783:rtra=on:gtg=position_2866 on theBenchmark for (2866ds/1783Mi) % 183.89/26.81 % (3070962)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=61524403:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2866 on theBenchmark for (2866ds/5451Mi) % 183.89/26.81 % (3070957)------------------------------ % 183.89/26.81 % (3070957)------------------------------ % 183.89/26.81 % (3070966)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=3482126753:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2862 on theBenchmark for (2862ds/4975Mi) % 183.89/26.81 % (3070960)Instruction limit reached! % 183.89/26.81 % (3070960)------------------------------ % 183.89/26.81 % (3070960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.89/26.81 % (3070960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.89/26.81 % (3070960)CaDiCaL version: 2.1.3 % 183.89/26.81 % (3070960)Termination reason: Instruction limit % 183.89/26.81 % (3070960)Termination phase: Saturation % 183.89/26.81 % (3070960)Time elapsed: 1.693 s % 183.89/26.81 % (3070960)Peak memory usage: 127 MB % 183.89/26.81 % (3070960)Instructions burned: 1783 (million) % 183.89/26.81 % (3070970)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=1872370571:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2847 on theBenchmark for (2847ds/2076Mi) % 183.89/26.81 % (3070970)Instruction limit reached! % 183.89/26.81 % (3070970)------------------------------ % 183.89/26.81 % (3070970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.89/26.81 % (3070970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.89/26.81 % (3070970)CaDiCaL version: 2.1.3 % 183.89/26.81 % (3070970)Termination reason: Instruction limit % 183.89/26.81 % (3070970)Termination phase: Saturation % 183.89/26.81 % (3070970)Time elapsed: 2.0000 s % 183.89/26.81 % (3070970)Peak memory usage: 139 MB % 183.89/26.81 % (3070970)Instructions burned: 2077 (million) % 183.89/26.81 % (3070974)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1774853287:i=5145:rtra=on_2824 on theBenchmark for (2824ds/5145Mi) % 183.89/26.81 % (3070966)Instruction limit reached! % 183.89/26.81 % (3070966)------------------------------ % 183.89/26.81 % (3070966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.89/26.81 % (3070966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.89/26.81 % (3070966)CaDiCaL version: 2.1.3 % 183.89/26.81 % (3070966)Termination reason: Instruction limit % 183.89/26.81 % (3070966)Termination phase: Saturation % 183.89/26.81 % (3070966)Time elapsed: 4.221 s % 183.89/26.81 % (3070966)Peak memory usage: 138 MB % 183.89/26.81 % (3070966)Instructions burned: 4975 (million) % 183.89/26.81 % (3070976)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4274313894:i=3509:rtra=on_2816 on theBenchmark for (2816ds/3509Mi) % 183.89/26.81 % (3070962)Instruction limit reached! % 183.89/26.81 % (3070962)------------------------------ % 183.89/26.81 % (3070962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.89/26.81 % (3070962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.07/42.73 % (3070962)CaDiCaL version: 2.1.3 % 297.07/42.73 % (3070962)Termination reason: Instruction limit % 297.07/42.73 % (3070962)Termination phase: Saturation % 297.07/42.73 % (3070962)Time elapsed: 5.010 s % 297.07/42.73 % (3070962)Peak memory usage: 143 MB % 297.07/42.73 % (3070962)Instructions burned: 5452 (million) % 297.07/42.73 % (3070978)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=136981933:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2813 on theBenchmark for (2813ds/13800Mi) % 297.07/42.73 % (3070978)Refutation not found, incomplete strategy % 297.07/42.73 % (3070978)------------------------------ % 297.07/42.73 % (3070978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.07/42.73 % (3070978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.07/42.73 % (3070978)CaDiCaL version: 2.1.3 % 297.07/42.73 % (3070978)Termination reason: Refutation not found, incomplete strategy % 297.07/42.73 % (3070978)Time elapsed: 0.011 s % 297.07/42.73 % (3070978)Peak memory usage: 88 MB % 297.07/42.73 % (3070978)Instructions burned: 11 (million) % 297.07/42.73 % (3070978)------------------------------ % 297.07/42.73 % (3070978)------------------------------ % 297.07/42.73 % (3070954)Instruction limit reached! % 297.07/42.73 % (3070954)------------------------------ % 297.07/42.73 % (3070954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.07/42.73 % (3070954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.07/42.73 % (3070954)CaDiCaL version: 2.1.3 % 297.07/42.73 % (3070954)Termination reason: Instruction limit % 297.07/42.73 % (3070954)Termination phase: Saturation % 297.07/42.73 % (3070954)Time elapsed: 6.181 s % 297.07/42.73 % (3070954)Peak memory usage: 136 MB % 297.07/42.73 % (3070954)Instructions burned: 13094 (million) % 297.07/42.73 % (3070982)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=753873414:i=1412:rtra=on:fsd=on:proc=on_2807 on theBenchmark for (2807ds/1412Mi) % 297.07/42.73 % (3070983)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 % 297.07/42.73 % (3070983)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=180525084:i=11747:aac=none:nm=0:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/11747Mi) % 297.07/42.73 % (3070982)Instruction limit reached! % 297.07/42.73 % (3070982)------------------------------ % 297.07/42.73 % (3070982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.07/42.73 % (3070982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.07/42.73 % (3070982)CaDiCaL version: 2.1.3 % 297.07/42.73 % (3070982)Termination reason: Instruction limit % 297.07/42.73 % (3070982)Termination phase: Saturation % 297.07/42.73 % (3070982)Time elapsed: 1.311 s % 297.07/42.73 % (3070982)Peak memory usage: 133 MB % 297.07/42.73 % (3070982)Instructions burned: 1412 (million) % 297.07/42.73 % (3070986)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1696959835:s2a=on:i=3553:nm=0:rtra=on_2791 on theBenchmark for (2791ds/3553Mi) % 297.07/42.73 % (3070943)Instruction limit reached! % 297.07/42.73 % (3070943)------------------------------ % 297.07/42.73 % (3070943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.07/42.73 % (3070943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.07/42.73 % (3070943)CaDiCaL version: 2.1.3 % 297.07/42.73 % (3070943)Termination reason: Instruction limit % 297.07/42.73 % (3070943)Termination phase: Saturation % 297.07/42.73 % (3070943)Time elapsed: 10.049 s % 297.07/42.73 % (3070943)Peak memory usage: 260 MB % 297.07/42.73 % (3070943)Instructions burned: 10544 (million) % 297.07/42.73 % (3070988)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2064738812:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/3201Mi) % 297.07/42.73 % (3070976)Instruction limit reached! % 297.07/42.73 % (3070976)------------------------------ % 297.07/42.73 % (3070976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.07/42.73 % (3070976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.07/42.73 % (3070976)CaDiCaL version: 2.1.3 % 297.07/42.73 % (3070976)Termination reason: Instruction limit % 297.07/42.73 % (3070976)Termination phase: Saturation % 297.07/42.73 % (3070976)Time elapsed: 3.371 s % 297.07/42.73 % (3070976)Peak memory usage: 112 MB % 297.07/42.73 % (3070976)Instructions burned: 3509 (million) % 300.25/43.18 % (3070990)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=3302263027:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2780 on theBenchmark for (2780ds/4081Mi) % 300.25/43.18 % (3070974)Instruction limit reached! % 300.25/43.18 % (3070974)------------------------------ % 300.25/43.18 % (3070974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.25/43.18 % (3070974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/43.18 % (3070974)CaDiCaL version: 2.1.3 % 300.25/43.18 % (3070974)Termination reason: Instruction limit % 300.25/43.18 % (3070974)Termination phase: Saturation % 300.25/43.18 % (3070974)Time elapsed: 4.578 s % 300.25/43.18 % (3070974)Peak memory usage: 127 MB % 300.25/43.18 % (3070974)Instructions burned: 5145 (million) % 300.25/43.18 % (3070992)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=1310571769:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2776 on theBenchmark for (2776ds/20260Mi) % 300.25/43.18 % (3070992)Refutation not found, incomplete strategy % 300.25/43.18 % (3070992)------------------------------ % 300.25/43.18 % (3070992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.25/43.18 % (3070992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/43.18 % (3070992)CaDiCaL version: 2.1.3 % 300.25/43.18 % (3070992)Termination reason: Refutation not found, incomplete strategy % 300.25/43.18 % (3070992)Time elapsed: 0.043 s % 300.25/43.18 % (3070992)Peak memory usage: 113 MB % 300.25/43.18 % (3070992)Instructions burned: 11 (million) % 300.25/43.18 % (3070992)------------------------------ % 300.25/43.18 % (3070992)------------------------------ % 300.25/43.18 % (3070994)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4188591831:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2769 on theBenchmark for (2769ds/58627Mi) % 300.25/43.18 % (3070988)Refutation not found, incomplete strategy % 300.25/43.18 % (3070988)------------------------------ % 300.25/43.18 % (3070988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.25/43.18 % (3070988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/43.18 % (3070988)CaDiCaL version: 2.1.3 % 300.25/43.18 % (3070988)Termination reason: Refutation not found, incomplete strategy % 300.25/43.18 % (3070988)Time elapsed: 2.455 s % 300.25/43.18 % (3070988)Peak memory usage: 98 MB % 300.25/43.18 % (3070988)Instructions burned: 2930 (million) % 300.25/43.18 % (3070986)Instruction limit reached! % 300.25/43.18 % (3070986)------------------------------ % 300.25/43.18 % (3070986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.25/43.18 % (3070986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/43.18 % (3070986)CaDiCaL version: 2.1.3 % 300.25/43.18 % (3070986)Termination reason: Instruction limit % 300.25/43.18 % (3070986)Termination phase: Saturation % 300.25/43.18 % (3070986)Time elapsed: 3.366 s % 300.25/43.18 % (3070986)Peak memory usage: 113 MB % 300.25/43.18 % (3070986)Instructions burned: 3553 (million) % 300.25/43.18 % (3070996)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2498006420:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/6258Mi) % 300.25/43.18 % (3070988)------------------------------ % 300.25/43.18 % (3070988)------------------------------ % 300.25/43.18 % (3070998)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=802804505:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2752 on theBenchmark for (2752ds/34001Mi) % 300.25/43.18 % (3070983)Instruction limit reached! % 300.25/43.18 % (3070983)------------------------------ % 300.25/43.18 % (3070983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.25/43.18 % (3070983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/43.18 % (3070983)CaDiCaL version: 2.1.3 % 300.25/43.18 % (3070983)Termination reason: Instruction limit % 300.25/43.18 % (3070983)Termination phase: Saturation % 300.25/43.18 % (3070983)Time elapsed: 6.0000 s % 300.25/43.18 % (3070983)Peak memory usage: 216 MB % 300.25/43.18 % (3070983)Instructions burned: 11748 (million) % 300.25/43.18 % (3071002)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1440660807:s2a=on:i=71622:s2at=-1:rtra=on_2743 on theBenchmark for (2743d % 300.25/43.18 Terminated %------------------------------------------------------------------------------