%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : DAT108_1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n014.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 09:47:19 AM UTC 2026 % Result : Timeout 289.49s 41.48s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : DAT108_1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.17 % Computer : n014.cluster.edu % 0.10/0.17 % Model : x86_64 x86_64 % 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.17 % Memory : 8046.5625MB % 0.10/0.17 % OS : Linux 6.8.0-71-generic % 0.10/0.17 % CPULimit : 300 % 0.10/0.17 % WCLimit : 300 % 0.10/0.17 % DateTime : Tue Sep 29 00:08:31 UTC 2026 % 0.10/0.17 % CPUTime : % 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.20 Running first-order theorem proving % 0.10/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.77/1.20 % (2305340)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.77/1.20 % (2305347)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1864675423:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.77/1.20 % (2305345)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=722728388:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.77/1.20 % (2305346)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1809997179:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.77/1.20 % (2305350)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1788211940:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.77/1.20 % (2305351)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=354579348:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.77/1.20 % (2305349)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3231290977:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.77/1.20 % (2305348)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1284125507:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.77/1.20 % (2305349)Instruction limit reached! % 3.77/1.20 % (2305349)------------------------------ % 3.77/1.20 % (2305349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.77/1.20 % (2305349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/1.20 % (2305349)CaDiCaL version: 2.1.3 % 3.77/1.20 % (2305349)Termination reason: Instruction limit % 3.77/1.20 % (2305349)Termination phase: Saturation % 3.77/1.20 % (2305349)Time elapsed: 0.004 s % 3.77/1.20 % (2305349)Peak memory usage: 88 MB % 3.77/1.20 % (2305349)Instructions burned: 5 (million) % 3.77/1.20 % (2305348)Instruction limit reached! % 3.77/1.20 % (2305348)------------------------------ % 3.77/1.20 % (2305348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.77/1.20 % (2305348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/1.20 % (2305348)CaDiCaL version: 2.1.3 % 3.77/1.20 % (2305348)Termination reason: Instruction limit % 3.77/1.20 % (2305348)Termination phase: Saturation % 3.77/1.20 % (2305348)Time elapsed: 0.005 s % 3.77/1.20 % (2305348)Peak memory usage: 88 MB % 3.77/1.20 % (2305348)Instructions burned: 7 (million) % 3.77/1.20 % (2305345)Refutation not found, incomplete strategy % 3.77/1.20 % (2305345)------------------------------ % 3.77/1.20 % (2305345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.77/1.20 % (2305345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/1.20 % (2305345)CaDiCaL version: 2.1.3 % 3.77/1.20 % (2305345)Termination reason: Refutation not found, incomplete strategy % 3.77/1.20 % (2305345)Time elapsed: 0.027 s % 3.77/1.20 % (2305345)Peak memory usage: 111 MB % 3.77/1.20 % (2305345)Instructions burned: 5 (million) % 3.77/1.20 % (2305351)Instruction limit reached! % 3.77/1.20 % (2305351)------------------------------ % 3.77/1.20 % (2305351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.77/1.20 % (2305351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/1.20 % (2305351)CaDiCaL version: 2.1.3 % 3.77/1.20 % (2305351)Termination reason: Instruction limit % 3.77/1.20 % (2305351)Termination phase: Saturation % 3.77/1.20 % (2305351)Time elapsed: 0.045 s % 3.77/1.20 % (2305351)Peak memory usage: 115 MB % 3.77/1.20 % (2305351)Instructions burned: 33 (million) % 3.77/1.20 % (2305347)Instruction limit reached! % 3.77/1.20 % (2305347)------------------------------ % 3.77/1.20 % (2305347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.77/1.20 % (2305347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/1.20 % (2305347)CaDiCaL version: 2.1.3 % 3.77/1.20 % (2305347)Termination reason: Instruction limit % 3.77/1.20 % (2305347)Termination phase: Saturation % 3.77/1.20 % (2305347)Time elapsed: 0.081 s % 3.77/1.20 % (2305347)Peak memory usage: 117 MB % 3.77/1.20 % (2305347)Instructions burned: 202 (million) % 3.77/1.20 % (2305350)Instruction limit reached! % 3.77/1.20 % (2305350)------------------------------ % 3.77/1.20 % (2305350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.77/1.20 % (2305350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305350)CaDiCaL version: 2.1.3 % 4.84/1.44 % (2305350)Termination reason: Instruction limit % 4.84/1.44 % (2305350)Termination phase: Saturation % 4.84/1.44 % (2305350)Time elapsed: 0.052 s % 4.84/1.44 % (2305350)Peak memory usage: 115 MB % 4.84/1.44 % (2305350)Instructions burned: 46 (million) % 4.84/1.44 % (2305360)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=2503882279:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.84/1.44 % (2305362)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3353604806:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.84/1.44 % (2305359)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3565272193:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.84/1.44 % (2305359)Refutation not found, incomplete strategy % 4.84/1.44 % (2305359)------------------------------ % 4.84/1.44 % (2305359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.44 % (2305359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305359)CaDiCaL version: 2.1.3 % 4.84/1.44 % (2305359)Termination reason: Refutation not found, incomplete strategy % 4.84/1.44 % (2305359)Time elapsed: 0.001 s % 4.84/1.44 % (2305359)Peak memory usage: 87 MB % 4.84/1.44 % (2305362)Instruction limit reached! % 4.84/1.44 % (2305362)------------------------------ % 4.84/1.44 % (2305362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.44 % (2305362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305362)CaDiCaL version: 2.1.3 % 4.84/1.44 % (2305362)Termination reason: Instruction limit % 4.84/1.44 % (2305362)Termination phase: Saturation % 4.84/1.44 % (2305362)Time elapsed: 0.011 s % 4.84/1.44 % (2305362)Peak memory usage: 89 MB % 4.84/1.44 % (2305362)Instructions burned: 26 (million) % 4.84/1.44 % (2305360)Instruction limit reached! % 4.84/1.44 % (2305360)------------------------------ % 4.84/1.44 % (2305360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.44 % (2305360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305360)CaDiCaL version: 2.1.3 % 4.84/1.44 % (2305360)Termination reason: Instruction limit % 4.84/1.44 % (2305360)Termination phase: Saturation % 4.84/1.44 % (2305360)Time elapsed: 0.022 s % 4.84/1.44 % (2305360)Peak memory usage: 88 MB % 4.84/1.44 % (2305360)Instructions burned: 30 (million) % 4.84/1.44 % (2305361)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1517546669:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.84/1.44 % (2305361)Instruction limit reached! % 4.84/1.44 % (2305361)------------------------------ % 4.84/1.44 % (2305361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.44 % (2305361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305361)CaDiCaL version: 2.1.3 % 4.84/1.44 % (2305361)Termination reason: Instruction limit % 4.84/1.44 % (2305361)Termination phase: Saturation % 4.84/1.44 % (2305361)Time elapsed: 0.011 s % 4.84/1.44 % (2305361)Peak memory usage: 90 MB % 4.84/1.44 % (2305361)Instructions burned: 16 (million) % 4.84/1.44 % (2305363)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=2770250369:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.84/1.44 % (2305363)Refutation not found, incomplete strategy % 4.84/1.44 % (2305363)------------------------------ % 4.84/1.44 % (2305363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.44 % (2305363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305363)CaDiCaL version: 2.1.3 % 4.84/1.44 % (2305363)Termination reason: Refutation not found, incomplete strategy % 4.84/1.44 % (2305363)Time elapsed: 0.002 s % 4.84/1.44 % (2305363)Peak memory usage: 88 MB % 4.84/1.44 % (2305363)Instructions burned: 1 (million) % 4.84/1.44 % (2305346)Instruction limit reached! % 4.84/1.44 % (2305346)------------------------------ % 4.84/1.44 % (2305346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.84/1.44 % (2305346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.44 % (2305346)CaDiCaL version: 2.1.3 % 6.68/1.65 % (2305346)Termination reason: Instruction limit % 6.68/1.65 % (2305346)Termination phase: Saturation % 6.68/1.65 % (2305346)Time elapsed: 0.205 s % 6.68/1.65 % (2305346)Peak memory usage: 116 MB % 6.68/1.65 % (2305346)Instructions burned: 308 (million) % 6.68/1.65 % (2305367)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1770756960:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 6.68/1.65 % (2305367)Instruction limit reached! % 6.68/1.65 % (2305367)------------------------------ % 6.68/1.65 % (2305367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.68/1.65 % (2305367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.68/1.65 % (2305367)CaDiCaL version: 2.1.3 % 6.68/1.65 % (2305367)Termination reason: Instruction limit % 6.68/1.65 % (2305367)Termination phase: Saturation % 6.68/1.65 % (2305367)Time elapsed: 0.026 s % 6.68/1.65 % (2305367)Peak memory usage: 88 MB % 6.68/1.65 % (2305367)Instructions burned: 86 (million) % 6.68/1.65 % (2305345)------------------------------ % 6.68/1.65 % (2305345)------------------------------ % 6.68/1.65 % (2305368)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1438089988:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 6.68/1.65 % (2305368)Instruction limit reached! % 6.68/1.65 % (2305368)------------------------------ % 6.68/1.65 % (2305368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.68/1.65 % (2305368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.68/1.65 % (2305368)CaDiCaL version: 2.1.3 % 6.68/1.65 % (2305368)Termination reason: Instruction limit % 6.68/1.65 % (2305368)Termination phase: Saturation % 6.68/1.65 % (2305368)Time elapsed: 0.003 s % 6.68/1.65 % (2305368)Peak memory usage: 88 MB % 6.68/1.65 % (2305368)Instructions burned: 3 (million) % 6.68/1.65 % (2305371)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3119453269:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 6.68/1.65 % (2305371)Refutation not found, incomplete strategy % 6.68/1.65 % (2305371)------------------------------ % 6.68/1.65 % (2305371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.68/1.65 % (2305371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.68/1.65 % (2305371)CaDiCaL version: 2.1.3 % 6.68/1.65 % (2305371)Termination reason: Refutation not found, incomplete strategy % 6.68/1.65 % (2305371)Time elapsed: 0.001 s % 6.68/1.65 % (2305371)Peak memory usage: 87 MB % 6.68/1.65 % (2305372)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3307952783:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 6.68/1.65 % (2305372)Refutation not found, incomplete strategy % 6.68/1.65 % (2305372)------------------------------ % 6.68/1.65 % (2305372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.68/1.65 % (2305372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.68/1.65 % (2305372)CaDiCaL version: 2.1.3 % 6.68/1.65 % (2305372)Termination reason: Refutation not found, incomplete strategy % 6.68/1.65 % (2305372)Time elapsed: 0.002 s % 6.68/1.65 % (2305372)Peak memory usage: 88 MB % 6.68/1.65 % (2305372)Instructions burned: 1 (million) % 6.68/1.65 % (2305376)lrs+10_1_thi=all:si=on:fd=off:random_seed=2689879477:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi) % 6.68/1.65 % (2305359)------------------------------ % 6.68/1.65 % (2305359)------------------------------ % 6.68/1.65 % (2305374)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1850095660:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 6.68/1.65 % (2305377)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=2426081386:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 6.68/1.65 % (2305377)Refutation not found, incomplete strategy % 6.68/1.65 % (2305377)------------------------------ % 6.68/1.65 % (2305377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.68/1.65 % (2305377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.68/1.65 % (2305377)CaDiCaL version: 2.1.3 % 6.68/1.65 % (2305377)Termination reason: Refutation not found, incomplete strategy % 6.68/1.65 % (2305377)Time elapsed: 0.002 s % 6.68/1.65 % (2305377)Peak memory usage: 88 MB % 6.68/1.65 % (2305377)Instructions burned: 2 (million) % 6.99/1.80 % (2305376)Instruction limit reached! % 6.99/1.80 % (2305376)------------------------------ % 6.99/1.80 % (2305376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.99/1.80 % (2305376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.80 % (2305376)CaDiCaL version: 2.1.3 % 6.99/1.80 % (2305376)Termination reason: Instruction limit % 6.99/1.80 % (2305376)Termination phase: Saturation % 6.99/1.80 % (2305376)Time elapsed: 0.034 s % 6.99/1.80 % (2305376)Peak memory usage: 116 MB % 6.99/1.80 % (2305376)Instructions burned: 54 (million) % 6.99/1.80 % (2305363)------------------------------ % 6.99/1.80 % (2305363)------------------------------ % 6.99/1.80 % (2305374)Instruction limit reached! % 6.99/1.80 % (2305374)------------------------------ % 6.99/1.80 % (2305374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.99/1.80 % (2305374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.80 % (2305374)CaDiCaL version: 2.1.3 % 6.99/1.80 % (2305374)Termination reason: Instruction limit % 6.99/1.80 % (2305374)Termination phase: Saturation % 6.99/1.80 % (2305374)Time elapsed: 0.088 s % 6.99/1.80 % (2305374)Peak memory usage: 133 MB % 6.99/1.80 % (2305374)Instructions burned: 68 (million) % 6.99/1.80 % (2305382)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2392108096:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 6.99/1.80 % (2305382)Refutation not found, incomplete strategy % 6.99/1.80 % (2305382)------------------------------ % 6.99/1.80 % (2305382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.99/1.80 % (2305382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.80 % (2305382)CaDiCaL version: 2.1.3 % 6.99/1.80 % (2305382)Termination reason: Refutation not found, incomplete strategy % 6.99/1.80 % (2305382)Time elapsed: 0.001 s % 6.99/1.80 % (2305382)Peak memory usage: 87 MB % 6.99/1.80 % (2305384)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1104306719:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 6.99/1.80 % (2305384)Instruction limit reached! % 6.99/1.80 % (2305384)------------------------------ % 6.99/1.80 % (2305384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.99/1.80 % (2305384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.80 % (2305384)CaDiCaL version: 2.1.3 % 6.99/1.80 % (2305384)Termination reason: Instruction limit % 6.99/1.80 % (2305384)Termination phase: Saturation % 6.99/1.80 % (2305384)Time elapsed: 0.002 s % 6.99/1.80 % (2305384)Peak memory usage: 88 MB % 6.99/1.80 % (2305384)Instructions burned: 4 (million) % 6.99/1.80 % (2305371)------------------------------ % 6.99/1.80 % (2305371)------------------------------ % 6.99/1.80 % (2305385)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2952604613:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.99/1.80 % (2305372)------------------------------ % 6.99/1.80 % (2305372)------------------------------ % 6.99/1.80 % (2305386)dis+10_1_si=on:random_seed=608879277:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 6.99/1.80 % (2305386)Instruction limit reached! % 6.99/1.80 % (2305386)------------------------------ % 6.99/1.80 % (2305386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.99/1.80 % (2305386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.80 % (2305386)CaDiCaL version: 2.1.3 % 6.99/1.80 % (2305386)Termination reason: Instruction limit % 6.99/1.80 % (2305386)Termination phase: Saturation % 6.99/1.80 % (2305386)Time elapsed: 0.007 s % 6.99/1.80 % (2305386)Peak memory usage: 88 MB % 6.99/1.80 % (2305386)Instructions burned: 11 (million) % 6.99/1.80 % (2305389)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3086316878:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi) % 6.99/1.80 % (2305389)Refutation not found, incomplete strategy % 6.99/1.80 % (2305389)------------------------------ % 6.99/1.80 % (2305389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.99/1.80 % (2305389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.80 % (2305389)CaDiCaL version: 2.1.3 % 6.99/1.80 % (2305389)Termination reason: Refutation not found, incomplete strategy % 6.99/1.80 % (2305389)Time elapsed: 0.001 s % 6.99/1.80 % (2305389)Peak memory usage: 88 MB % 6.99/1.80 % (2305389)Instructions burned: 1 (million) % 6.99/1.80 % (2305377)------------------------------ % 10.21/2.04 % (2305377)------------------------------ % 10.21/2.04 % (2305385)Instruction limit reached! % 10.21/2.04 % (2305385)------------------------------ % 10.21/2.04 % (2305385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.04 % (2305385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.04 % (2305385)CaDiCaL version: 2.1.3 % 10.21/2.04 % (2305385)Termination reason: Instruction limit % 10.21/2.04 % (2305385)Termination phase: Saturation % 10.21/2.04 % (2305385)Time elapsed: 0.108 s % 10.21/2.04 % (2305385)Peak memory usage: 116 MB % 10.21/2.04 % (2305385)Instructions burned: 127 (million) % 10.21/2.04 % (2305391)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2062458052:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2992 on theBenchmark for (2992ds/35Mi) % 10.21/2.04 % (2305392)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1794501034:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi) % 10.21/2.04 % (2305392)Instruction limit reached! % 10.21/2.04 % (2305392)------------------------------ % 10.21/2.04 % (2305392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.04 % (2305392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.04 % (2305392)CaDiCaL version: 2.1.3 % 10.21/2.04 % (2305392)Termination reason: Instruction limit % 10.21/2.04 % (2305392)Termination phase: Saturation % 10.21/2.04 % (2305392)Time elapsed: 0.003 s % 10.21/2.04 % (2305392)Peak memory usage: 88 MB % 10.21/2.04 % (2305392)Instructions burned: 3 (million) % 10.21/2.04 % (2305391)Instruction limit reached! % 10.21/2.04 % (2305391)------------------------------ % 10.21/2.04 % (2305391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.04 % (2305391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.04 % (2305391)CaDiCaL version: 2.1.3 % 10.21/2.04 % (2305391)Termination reason: Instruction limit % 10.21/2.04 % (2305391)Termination phase: Saturation % 10.21/2.04 % (2305391)Time elapsed: 0.029 s % 10.21/2.04 % (2305391)Peak memory usage: 89 MB % 10.21/2.04 % (2305391)Instructions burned: 35 (million) % 10.21/2.04 % (2305394)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=312827310:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi) % 10.21/2.04 % (2305394)Instruction limit reached! % 10.21/2.04 % (2305394)------------------------------ % 10.21/2.04 % (2305394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.04 % (2305394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.04 % (2305394)CaDiCaL version: 2.1.3 % 10.21/2.04 % (2305394)Termination reason: Instruction limit % 10.21/2.04 % (2305394)Termination phase: Saturation % 10.21/2.04 % (2305394)Time elapsed: 0.008 s % 10.21/2.04 % (2305394)Peak memory usage: 88 MB % 10.21/2.04 % (2305394)Instructions burned: 9 (million) % 10.21/2.04 % (2305382)------------------------------ % 10.21/2.04 % (2305382)------------------------------ % 10.21/2.04 % (2305389)------------------------------ % 10.21/2.04 % (2305389)------------------------------ % 10.21/2.04 % (2305396)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4130681522:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 10.21/2.04 % (2305397)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3132809070:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi) % 10.21/2.04 % (2305400)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=979043115:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi) % 10.21/2.04 % (2305397)Instruction limit reached! % 10.21/2.04 % (2305397)------------------------------ % 10.21/2.04 % (2305397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.04 % (2305397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.04 % (2305397)CaDiCaL version: 2.1.3 % 10.21/2.04 % (2305397)Termination reason: Instruction limit % 10.21/2.04 % (2305397)Termination phase: Saturation % 10.21/2.04 % (2305397)Time elapsed: 0.031 s % 10.21/2.04 % (2305397)Peak memory usage: 116 MB % 10.21/2.04 % (2305397)Instructions burned: 13 (million) % 10.21/2.04 % (2305402)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2360176785:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 11.56/2.32 % (2305402)Instruction limit reached! % 11.56/2.32 % (2305402)------------------------------ % 11.56/2.32 % (2305402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.32 % (2305402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.32 % (2305402)CaDiCaL version: 2.1.3 % 11.56/2.32 % (2305402)Termination reason: Instruction limit % 11.56/2.32 % (2305402)Termination phase: Saturation % 11.56/2.32 % (2305402)Time elapsed: 0.008 s % 11.56/2.32 % (2305402)Peak memory usage: 88 MB % 11.56/2.32 % (2305402)Instructions burned: 11 (million) % 11.56/2.32 % (2305400)Refutation not found, incomplete strategy % 11.56/2.32 % (2305400)------------------------------ % 11.56/2.32 % (2305400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.32 % (2305400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.32 % (2305400)CaDiCaL version: 2.1.3 % 11.56/2.32 % (2305400)Termination reason: Refutation not found, incomplete strategy % 11.56/2.32 % (2305400)Time elapsed: 0.026 s % 11.56/2.32 % (2305400)Peak memory usage: 111 MB % 11.56/2.32 % (2305400)Instructions burned: 5 (million) % 11.56/2.32 % (2305403)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=953723204:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi) % 11.56/2.32 % (2305405)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=1590012360:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi) % 11.56/2.32 % (2305404)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=3652433093:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2990 on theBenchmark for (2990ds/75Mi) % 11.56/2.32 % (2305404)Instruction limit reached! % 11.56/2.32 % (2305404)------------------------------ % 11.56/2.32 % (2305404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.32 % (2305404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.32 % (2305404)CaDiCaL version: 2.1.3 % 11.56/2.32 % (2305404)Termination reason: Instruction limit % 11.56/2.32 % (2305404)Termination phase: Saturation % 11.56/2.32 % (2305404)Time elapsed: 0.053 s % 11.56/2.32 % (2305404)Peak memory usage: 90 MB % 11.56/2.32 % (2305404)Instructions burned: 76 (million) % 11.56/2.32 % (2305403)Instruction limit reached! % 11.56/2.32 % (2305403)------------------------------ % 11.56/2.32 % (2305403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.32 % (2305403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.32 % (2305403)CaDiCaL version: 2.1.3 % 11.56/2.32 % (2305403)Termination reason: Instruction limit % 11.56/2.32 % (2305403)Termination phase: Saturation % 11.56/2.32 % (2305403)Time elapsed: 0.084 s % 11.56/2.32 % (2305403)Peak memory usage: 132 MB % 11.56/2.32 % (2305403)Instructions burned: 71 (million) % 11.56/2.32 % (2305405)Instruction limit reached! % 11.56/2.32 % (2305405)------------------------------ % 11.56/2.32 % (2305405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.32 % (2305405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.32 % (2305405)CaDiCaL version: 2.1.3 % 11.56/2.32 % (2305405)Termination reason: Instruction limit % 11.56/2.32 % (2305405)Termination phase: Saturation % 11.56/2.32 % (2305405)Time elapsed: 0.098 s % 11.56/2.32 % (2305405)Peak memory usage: 90 MB % 11.56/2.32 % (2305405)Instructions burned: 296 (million) % 11.56/2.32 % (2305410)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=472104185:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi) % 11.56/2.32 % (2305396)Instruction limit reached! % 11.56/2.32 % (2305396)------------------------------ % 11.56/2.32 % (2305396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.32 % (2305396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.32 % (2305396)CaDiCaL version: 2.1.3 % 11.56/2.32 % (2305396)Termination reason: Instruction limit % 11.56/2.32 % (2305396)Termination phase: Saturation % 11.56/2.32 % (2305396)Time elapsed: 0.201 s % 11.56/2.32 % (2305396)Peak memory usage: 91 MB % 11.56/2.32 % (2305396)Instructions burned: 371 (million) % 11.56/2.32 % (2305411)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1288553991:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 12.90/2.67 % (2305417)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1652678653:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/598Mi) % 12.90/2.67 % (2305415)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3016558646:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi) % 12.90/2.67 % (2305410)Instruction limit reached! % 12.90/2.67 % (2305410)------------------------------ % 12.90/2.67 % (2305410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.90/2.67 % (2305410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.90/2.67 % (2305410)CaDiCaL version: 2.1.3 % 12.90/2.67 % (2305410)Termination reason: Instruction limit % 12.90/2.67 % (2305410)Termination phase: Saturation % 12.90/2.67 % (2305410)Time elapsed: 0.103 s % 12.90/2.67 % (2305410)Peak memory usage: 116 MB % 12.90/2.67 % (2305410)Instructions burned: 131 (million) % 12.90/2.67 % (2305416)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1434503650:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi) % 12.90/2.67 % (2305400)------------------------------ % 12.90/2.67 % (2305400)------------------------------ % 12.90/2.67 % (2305416)Refutation not found, incomplete strategy % 12.90/2.67 % (2305416)------------------------------ % 12.90/2.67 % (2305416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.90/2.67 % (2305416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.90/2.67 % (2305416)CaDiCaL version: 2.1.3 % 12.90/2.67 % (2305416)Termination reason: Refutation not found, incomplete strategy % 12.90/2.67 % (2305416)Time elapsed: 0.002 s % 12.90/2.67 % (2305416)Peak memory usage: 88 MB % 12.90/2.67 % (2305416)Instructions burned: 2 (million) % 12.90/2.67 % (2305420)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2059801827:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 12.90/2.67 % (2305411)Instruction limit reached! % 12.90/2.67 % (2305411)------------------------------ % 12.90/2.67 % (2305411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.90/2.67 % (2305411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.90/2.67 % (2305411)CaDiCaL version: 2.1.3 % 12.90/2.67 % (2305411)Termination reason: Instruction limit % 12.90/2.67 % (2305411)Termination phase: Saturation % 12.90/2.67 % (2305411)Time elapsed: 0.127 s % 12.90/2.67 % (2305411)Peak memory usage: 133 MB % 12.90/2.67 % (2305411)Instructions burned: 132 (million) % 12.90/2.67 % (2305415)Instruction limit reached! % 12.90/2.67 % (2305415)------------------------------ % 12.90/2.67 % (2305415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.90/2.67 % (2305415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.90/2.67 % (2305415)CaDiCaL version: 2.1.3 % 12.90/2.67 % (2305415)Termination reason: Instruction limit % 12.90/2.67 % (2305415)Termination phase: Saturation % 12.90/2.67 % (2305415)Time elapsed: 0.067 s % 12.90/2.67 % (2305415)Peak memory usage: 133 MB % 12.90/2.67 % (2305415)Instructions burned: 41 (million) % 12.90/2.67 % (2305423)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=3898736940:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 12.90/2.67 % (2305420)Instruction limit reached! % 12.90/2.67 % (2305420)------------------------------ % 12.90/2.67 % (2305420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.90/2.67 % (2305420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.90/2.67 % (2305420)CaDiCaL version: 2.1.3 % 12.90/2.67 % (2305420)Termination reason: Instruction limit % 12.90/2.67 % (2305420)Termination phase: Saturation % 12.90/2.67 % (2305420)Time elapsed: 0.100 s % 12.90/2.67 % (2305420)Peak memory usage: 117 MB % 12.90/2.67 % (2305420)Instructions burned: 132 (million) % 12.90/2.67 % (2305425)dis+10_1_si=on:random_seed=4166106185:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi) % 12.90/2.67 % (2305423)Refutation not found, incomplete strategy % 12.90/2.67 % (2305423)------------------------------ % 12.90/2.67 % (2305423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.90/2.67 % (2305423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.90/2.67 % (2305423)CaDiCaL version: 2.1.3 % 12.90/2.67 % (2305423)Termination reason: Refutation not found, incomplete strategy % 14.62/2.91 % (2305423)Time elapsed: 0.026 s % 14.62/2.91 % (2305423)Peak memory usage: 111 MB % 14.62/2.91 % (2305423)Instructions burned: 5 (million) % 14.62/2.91 % (2305427)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1130269030:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi) % 14.62/2.91 % (2305428)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3253881152:i=141:doe=on:rtra=on_2986 on theBenchmark for (2986ds/141Mi) % 14.62/2.91 % (2305417)Instruction limit reached! % 14.62/2.91 % (2305417)------------------------------ % 14.62/2.91 % (2305417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.62/2.91 % (2305417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.62/2.91 % (2305417)CaDiCaL version: 2.1.3 % 14.62/2.91 % (2305417)Termination reason: Instruction limit % 14.62/2.91 % (2305417)Termination phase: Saturation % 14.62/2.91 % (2305417)Time elapsed: 0.250 s % 14.62/2.91 % (2305417)Peak memory usage: 138 MB % 14.62/2.91 % (2305417)Instructions burned: 600 (million) % 14.62/2.91 % (2305416)------------------------------ % 14.62/2.91 % (2305416)------------------------------ % 14.62/2.91 % (2305430)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2821126323:i=65:nm=16:rtra=on_2986 on theBenchmark for (2986ds/65Mi) % 14.62/2.91 % (2305430)Refutation not found, incomplete strategy % 14.62/2.91 % (2305430)------------------------------ % 14.62/2.91 % (2305430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.62/2.91 % (2305430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.62/2.91 % (2305430)CaDiCaL version: 2.1.3 % 14.62/2.91 % (2305430)Termination reason: Refutation not found, incomplete strategy % 14.62/2.91 % (2305430)Time elapsed: 0.027 s % 14.62/2.91 % (2305430)Peak memory usage: 112 MB % 14.62/2.91 % (2305430)Instructions burned: 6 (million) % 14.62/2.91 % (2305428)Instruction limit reached! % 14.62/2.91 % (2305428)------------------------------ % 14.62/2.91 % (2305428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.62/2.91 % (2305428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.62/2.91 % (2305428)CaDiCaL version: 2.1.3 % 14.62/2.91 % (2305428)Termination reason: Instruction limit % 14.62/2.91 % (2305428)Termination phase: Saturation % 14.62/2.91 % (2305428)Time elapsed: 0.091 s % 14.62/2.91 % (2305428)Peak memory usage: 89 MB % 14.62/2.91 % (2305428)Instructions burned: 142 (million) % 14.62/2.91 % (2305434)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3618293967:i=121:nm=16:rtra=on_2985 on theBenchmark for (2985ds/121Mi) % 14.62/2.91 % (2305434)Instruction limit reached! % 14.62/2.91 % (2305434)------------------------------ % 14.62/2.91 % (2305434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.62/2.91 % (2305434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.62/2.91 % (2305434)CaDiCaL version: 2.1.3 % 14.62/2.91 % (2305434)Termination reason: Instruction limit % 14.62/2.91 % (2305434)Termination phase: Saturation % 14.62/2.91 % (2305434)Time elapsed: 0.038 s % 14.62/2.91 % (2305434)Peak memory usage: 89 MB % 14.62/2.91 % (2305434)Instructions burned: 124 (million) % 14.62/2.91 % (2305427)Instruction limit reached! % 14.62/2.91 % (2305427)------------------------------ % 14.62/2.91 % (2305427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.62/2.91 % (2305427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.62/2.91 % (2305427)CaDiCaL version: 2.1.3 % 14.62/2.91 % (2305427)Termination reason: Instruction limit % 14.62/2.91 % (2305427)Termination phase: Saturation % 14.62/2.91 % (2305427)Time elapsed: 0.215 s % 14.62/2.91 % (2305427)Peak memory usage: 91 MB % 14.62/2.91 % (2305427)Instructions burned: 384 (million) % 14.62/2.91 % (2305423)------------------------------ % 14.62/2.91 % (2305423)------------------------------ % 14.62/2.91 % (2305436)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=1862293526:s2a=on:i=128:s2at=5:ins=3:rtra=on_2984 on theBenchmark for (2984ds/128Mi) % 14.62/2.91 % (2305437)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=3959147174:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi) % 14.62/2.91 % (2305436)Refutation not found, incomplete strategy % 14.62/2.91 % (2305436)------------------------------ % 14.62/2.91 % (2305436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.81/3.23 % (2305436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.23 % (2305436)CaDiCaL version: 2.1.3 % 17.81/3.23 % (2305436)Termination reason: Refutation not found, incomplete strategy % 17.81/3.23 % (2305436)Time elapsed: 0.028 s % 17.81/3.23 % (2305436)Peak memory usage: 112 MB % 17.81/3.23 % (2305436)Instructions burned: 7 (million) % 17.81/3.23 % (2305437)Refutation not found, incomplete strategy % 17.81/3.23 % (2305437)------------------------------ % 17.81/3.23 % (2305437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.81/3.23 % (2305437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.23 % (2305437)CaDiCaL version: 2.1.3 % 17.81/3.23 % (2305437)Termination reason: Refutation not found, incomplete strategy % 17.81/3.23 % (2305437)Time elapsed: 0.027 s % 17.81/3.23 % (2305437)Peak memory usage: 112 MB % 17.81/3.23 % (2305437)Instructions burned: 6 (million) % 17.81/3.23 % (2305440)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3429829383:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi) % 17.81/3.23 % (2305439)dis+1010_1_to=kbo:si=on:random_seed=3212225643:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/175Mi) % 17.81/3.23 % (2305430)------------------------------ % 17.81/3.23 % (2305430)------------------------------ % 17.81/3.23 % (2305441)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3326771777:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi) % 17.81/3.23 % (2305440)Instruction limit reached! % 17.81/3.23 % (2305440)------------------------------ % 17.81/3.23 % (2305440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.81/3.23 % (2305440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.23 % (2305440)CaDiCaL version: 2.1.3 % 17.81/3.23 % (2305440)Termination reason: Instruction limit % 17.81/3.23 % (2305440)Termination phase: Saturation % 17.81/3.23 % (2305440)Time elapsed: 0.125 s % 17.81/3.23 % (2305440)Peak memory usage: 118 MB % 17.81/3.23 % (2305440)Instructions burned: 331 (million) % 17.81/3.23 % (2305439)Instruction limit reached! % 17.81/3.23 % (2305439)------------------------------ % 17.81/3.23 % (2305439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.81/3.23 % (2305439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.23 % (2305439)CaDiCaL version: 2.1.3 % 17.81/3.23 % (2305439)Termination reason: Instruction limit % 17.81/3.23 % (2305439)Termination phase: Saturation % 17.81/3.23 % (2305439)Time elapsed: 0.133 s % 17.81/3.23 % (2305439)Peak memory usage: 90 MB % 17.81/3.23 % (2305439)Instructions burned: 176 (million) % 17.81/3.23 % (2305447)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1486065006:thitd=on:i=215:nm=0:rtra=on:ev=force_2982 on theBenchmark for (2982ds/215Mi) % 17.81/3.23 % (2305436)------------------------------ % 17.81/3.23 % (2305436)------------------------------ % 17.81/3.23 % (2305448)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1802039661:i=349:rtra=on_2981 on theBenchmark for (2981ds/349Mi) % 17.81/3.23 % (2305437)------------------------------ % 17.81/3.23 % (2305437)------------------------------ % 17.81/3.23 % (2305425)Instruction limit reached! % 17.81/3.23 % (2305425)------------------------------ % 17.81/3.23 % (2305425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.81/3.23 % (2305425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.23 % (2305425)CaDiCaL version: 2.1.3 % 17.81/3.23 % (2305425)Termination reason: Instruction limit % 17.81/3.23 % (2305425)Termination phase: Saturation % 17.81/3.23 % (2305425)Time elapsed: 0.569 s % 17.81/3.23 % (2305425)Peak memory usage: 94 MB % 17.81/3.23 % (2305425)Instructions burned: 1000 (million) % 17.81/3.23 % (2305449)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=4181790710:st=2:i=295:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/295Mi) % 17.81/3.23 % (2305449)Refutation not found, incomplete strategy % 17.81/3.23 % (2305449)------------------------------ % 17.81/3.23 % (2305449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.81/3.23 % (2305449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.44 % (2305449)CaDiCaL version: 2.1.3 % 18.63/3.44 % (2305449)Termination reason: Refutation not found, incomplete strategy % 18.63/3.44 % (2305449)Time elapsed: 0.001 s % 18.63/3.44 % (2305449)Peak memory usage: 87 MB % 18.63/3.44 % (2305448)Instruction limit reached! % 18.63/3.44 % (2305448)------------------------------ % 18.63/3.44 % (2305448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.44 % (2305448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.44 % (2305448)CaDiCaL version: 2.1.3 % 18.63/3.44 % (2305448)Termination reason: Instruction limit % 18.63/3.44 % (2305448)Termination phase: Saturation % 18.63/3.44 % (2305448)Time elapsed: 0.129 s % 18.63/3.44 % (2305448)Peak memory usage: 118 MB % 18.63/3.44 % (2305448)Instructions burned: 349 (million) % 18.63/3.44 % (2305453)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1847740042:i=281:gtgl=2:rtra=on:gtg=all_2980 on theBenchmark for (2980ds/281Mi) % 18.63/3.44 % (2305452)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=302396188:i=328:kws=inv_frequency:nm=20:rtra=on_2980 on theBenchmark for (2980ds/328Mi) % 18.63/3.44 % (2305447)Instruction limit reached! % 18.63/3.44 % (2305447)------------------------------ % 18.63/3.44 % (2305447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.44 % (2305447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.44 % (2305447)CaDiCaL version: 2.1.3 % 18.63/3.44 % (2305447)Termination reason: Instruction limit % 18.63/3.44 % (2305447)Termination phase: Saturation % 18.63/3.44 % (2305447)Time elapsed: 0.169 s % 18.63/3.44 % (2305447)Peak memory usage: 135 MB % 18.63/3.44 % (2305447)Instructions burned: 215 (million) % 18.63/3.44 % (2305454)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2848291007:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/484Mi) % 18.63/3.44 % (2305454)Refutation not found, incomplete strategy % 18.63/3.44 % (2305454)------------------------------ % 18.63/3.44 % (2305454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.44 % (2305454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.44 % (2305454)CaDiCaL version: 2.1.3 % 18.63/3.44 % (2305454)Termination reason: Refutation not found, incomplete strategy % 18.63/3.44 % (2305454)Time elapsed: 0.001 s % 18.63/3.44 % (2305454)Peak memory usage: 87 MB % 18.63/3.44 % (2305441)Instruction limit reached! % 18.63/3.44 % (2305441)------------------------------ % 18.63/3.44 % (2305441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.44 % (2305441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.44 % (2305441)CaDiCaL version: 2.1.3 % 18.63/3.44 % (2305441)Termination reason: Instruction limit % 18.63/3.44 % (2305441)Termination phase: Saturation % 18.63/3.44 % (2305441)Time elapsed: 0.334 s % 18.63/3.44 % (2305441)Peak memory usage: 134 MB % 18.63/3.44 % (2305441)Instructions burned: 485 (million) % 18.63/3.44 % (2305458)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1697186019:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2979 on theBenchmark for (2979ds/321Mi) % 18.63/3.44 % (2305458)Refutation not found, incomplete strategy % 18.63/3.44 % (2305458)------------------------------ % 18.63/3.44 % (2305458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.44 % (2305458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.44 % (2305458)CaDiCaL version: 2.1.3 % 18.63/3.44 % (2305458)Termination reason: Refutation not found, incomplete strategy % 18.63/3.44 % (2305458)Time elapsed: 0.016 s % 18.63/3.44 % (2305458)Peak memory usage: 111 MB % 18.63/3.44 % (2305458)Instructions burned: 5 (million) % 18.63/3.44 % (2305460)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=379065816:i=416:rtra=on:gtg=position:ss=axioms_2979 on theBenchmark for (2979ds/416Mi) % 18.63/3.44 % (2305461)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3568642500:i=471:thf=on:kws=precedence:rtra=on_2978 on theBenchmark for (2978ds/471Mi) % 18.63/3.44 % (2305449)------------------------------ % 18.63/3.44 % (2305449)------------------------------ % 18.63/3.44 % (2305460)Refutation not found, incomplete strategy % 18.63/3.44 % (2305460)------------------------------ % 18.63/3.44 % (2305460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.44 % (2305460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.03/3.73 % (2305460)CaDiCaL version: 2.1.3 % 21.03/3.73 % (2305460)Termination reason: Refutation not found, incomplete strategy % 21.03/3.73 % (2305460)Time elapsed: 0.026 s % 21.03/3.73 % (2305460)Peak memory usage: 111 MB % 21.03/3.73 % (2305460)Instructions burned: 5 (million) % 21.03/3.73 % (2305453)Instruction limit reached! % 21.03/3.73 % (2305453)------------------------------ % 21.03/3.73 % (2305453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.03/3.73 % (2305453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.03/3.73 % (2305453)CaDiCaL version: 2.1.3 % 21.03/3.73 % (2305453)Termination reason: Instruction limit % 21.03/3.73 % (2305453)Termination phase: Saturation % 21.03/3.73 % (2305453)Time elapsed: 0.205 s % 21.03/3.73 % (2305453)Peak memory usage: 117 MB % 21.03/3.73 % (2305453)Instructions burned: 281 (million) % 21.03/3.73 % (2305452)Instruction limit reached! % 21.03/3.73 % (2305452)------------------------------ % 21.03/3.73 % (2305452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.03/3.73 % (2305452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.03/3.73 % (2305452)CaDiCaL version: 2.1.3 % 21.03/3.73 % (2305452)Termination reason: Instruction limit % 21.03/3.73 % (2305452)Termination phase: Saturation % 21.03/3.73 % (2305452)Time elapsed: 0.222 s % 21.03/3.73 % (2305452)Peak memory usage: 117 MB % 21.03/3.73 % (2305452)Instructions burned: 328 (million) % 21.03/3.73 % (2305458)------------------------------ % 21.03/3.73 % (2305458)------------------------------ % 21.03/3.73 % (2305454)------------------------------ % 21.03/3.73 % (2305454)------------------------------ % 21.03/3.73 % (2305465)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=4237433253:avsq=on:i=276:avsqr=1,2:rtra=on_2977 on theBenchmark for (2977ds/276Mi) % 21.03/3.73 % (2305467)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3577008704:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/387Mi) % 21.03/3.73 % (2305466)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4135198948:i=375:kws=inv_arity_squared:rtra=on_2977 on theBenchmark for (2977ds/375Mi) % 21.03/3.73 % (2305468)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=579981698:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2976 on theBenchmark for (2976ds/513Mi) % 21.03/3.73 % (2305467)Refutation not found, incomplete strategy % 21.03/3.73 % (2305467)------------------------------ % 21.03/3.73 % (2305467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.03/3.73 % (2305467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.03/3.73 % (2305467)CaDiCaL version: 2.1.3 % 21.03/3.73 % (2305467)Termination reason: Refutation not found, incomplete strategy % 21.03/3.73 % (2305467)Time elapsed: 0.026 s % 21.03/3.73 % (2305467)Peak memory usage: 111 MB % 21.03/3.73 % (2305467)Instructions burned: 5 (million) % 21.03/3.73 % (2305469)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3543245667:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi) % 21.03/3.73 % (2305460)------------------------------ % 21.03/3.73 % (2305460)------------------------------ % 21.03/3.73 % (2305461)Instruction limit reached! % 21.03/3.73 % (2305461)------------------------------ % 21.03/3.73 % (2305461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.03/3.73 % (2305461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.03/3.73 % (2305461)CaDiCaL version: 2.1.3 % 21.03/3.73 % (2305461)Termination reason: Instruction limit % 21.03/3.73 % (2305461)Termination phase: Saturation % 21.03/3.73 % (2305461)Time elapsed: 0.295 s % 21.03/3.73 % (2305461)Peak memory usage: 118 MB % 21.03/3.73 % (2305461)Instructions burned: 472 (million) % 21.03/3.73 % (2305468)Instruction limit reached! % 21.03/3.73 % (2305468)------------------------------ % 21.03/3.73 % (2305468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.03/3.73 % (2305468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.03/3.73 % (2305468)CaDiCaL version: 2.1.3 % 21.03/3.73 % (2305468)Termination reason: Instruction limit % 21.03/3.73 % (2305468)Termination phase: Saturation % 21.03/3.73 % (2305468)Time elapsed: 0.167 s % 21.03/3.73 % (2305468)Peak memory usage: 92 MB % 24.87/4.18 % (2305468)Instructions burned: 516 (million) % 24.87/4.18 % (2305465)Instruction limit reached! % 24.87/4.18 % (2305465)------------------------------ % 24.87/4.18 % (2305465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.87/4.18 % (2305465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.87/4.18 % (2305465)CaDiCaL version: 2.1.3 % 24.87/4.18 % (2305465)Termination reason: Instruction limit % 24.87/4.18 % (2305465)Termination phase: Saturation % 24.87/4.18 % (2305465)Time elapsed: 0.213 s % 24.87/4.18 % (2305465)Peak memory usage: 135 MB % 24.87/4.18 % (2305465)Instructions burned: 277 (million) % 24.87/4.18 % (2305475)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2258845734:i=359:rtra=on:gtg=exists_top:ss=axioms_2974 on theBenchmark for (2974ds/359Mi) % 24.87/4.18 % (2305466)Instruction limit reached! % 24.87/4.18 % (2305466)------------------------------ % 24.87/4.18 % (2305466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.87/4.18 % (2305466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.87/4.18 % (2305466)CaDiCaL version: 2.1.3 % 24.87/4.18 % (2305466)Termination reason: Instruction limit % 24.87/4.18 % (2305466)Termination phase: Saturation % 24.87/4.18 % (2305466)Time elapsed: 0.237 s % 24.87/4.18 % (2305466)Peak memory usage: 117 MB % 24.87/4.18 % (2305466)Instructions burned: 376 (million) % 24.87/4.18 % (2305475)Refutation not found, incomplete strategy % 24.87/4.18 % (2305475)------------------------------ % 24.87/4.18 % (2305475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.87/4.18 % (2305475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.87/4.18 % (2305475)CaDiCaL version: 2.1.3 % 24.87/4.18 % (2305475)Termination reason: Refutation not found, incomplete strategy % 24.87/4.18 % (2305475)Time elapsed: 0.001 s % 24.87/4.18 % (2305475)Peak memory usage: 88 MB % 24.87/4.18 % (2305477)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1096655306:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/261Mi) % 24.87/4.18 % (2305467)------------------------------ % 24.87/4.18 % (2305467)------------------------------ % 24.87/4.18 % (2305476)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3087001222:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2974 on theBenchmark for (2974ds/341Mi) % 24.87/4.18 % (2305477)Refutation not found, incomplete strategy % 24.87/4.18 % (2305477)------------------------------ % 24.87/4.18 % (2305477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.87/4.18 % (2305477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.87/4.18 % (2305477)CaDiCaL version: 2.1.3 % 24.87/4.18 % (2305477)Termination reason: Refutation not found, incomplete strategy % 24.87/4.18 % (2305477)Time elapsed: 0.016 s % 24.87/4.18 % (2305477)Peak memory usage: 111 MB % 24.87/4.18 % (2305477)Instructions burned: 5 (million) % 24.87/4.18 % (2305469)Instruction limit reached! % 24.87/4.18 % (2305469)------------------------------ % 24.87/4.18 % (2305469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.87/4.18 % (2305469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.87/4.18 % (2305469)CaDiCaL version: 2.1.3 % 24.87/4.18 % (2305469)Termination reason: Instruction limit % 24.87/4.18 % (2305469)Termination phase: Saturation % 24.87/4.18 % (2305469)Time elapsed: 0.255 s % 24.87/4.18 % (2305469)Peak memory usage: 134 MB % 24.87/4.18 % (2305469)Instructions burned: 334 (million) % 24.87/4.18 % (2305478)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=3218442389:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/235Mi) % 24.87/4.18 % (2305478)Refutation not found, incomplete strategy % 24.87/4.18 % (2305478)------------------------------ % 24.87/4.18 % (2305478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.87/4.18 % (2305478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.87/4.18 % (2305478)CaDiCaL version: 2.1.3 % 24.87/4.18 % (2305478)Termination reason: Refutation not found, incomplete strategy % 24.87/4.18 % (2305478)Time elapsed: 0.026 s % 24.87/4.18 % (2305478)Peak memory usage: 111 MB % 24.87/4.18 % (2305478)Instructions burned: 5 (million) % 24.87/4.18 % (2305480)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=687010749:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2973 on theBenchmark for (2973ds/273Mi) % 26.66/4.71 % (2305483)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3901525399:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi) % 26.66/4.71 % (2305477)------------------------------ % 26.66/4.71 % (2305477)------------------------------ % 26.66/4.71 % (2305485)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2456116869:i=4428:doe=on:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/4428Mi) % 26.66/4.71 % (2305475)------------------------------ % 26.66/4.71 % (2305475)------------------------------ % 26.66/4.71 % (2305476)Instruction limit reached! % 26.66/4.71 % (2305476)------------------------------ % 26.66/4.71 % (2305476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.66/4.71 % (2305476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.71 % (2305476)CaDiCaL version: 2.1.3 % 26.66/4.71 % (2305476)Termination reason: Instruction limit % 26.66/4.71 % (2305476)Termination phase: Saturation % 26.66/4.71 % (2305476)Time elapsed: 0.232 s % 26.66/4.71 % (2305476)Peak memory usage: 117 MB % 26.66/4.71 % (2305476)Instructions burned: 342 (million) % 26.66/4.71 % (2305483)Instruction limit reached! % 26.66/4.71 % (2305483)------------------------------ % 26.66/4.71 % (2305483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.66/4.71 % (2305483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.71 % (2305483)CaDiCaL version: 2.1.3 % 26.66/4.71 % (2305483)Termination reason: Instruction limit % 26.66/4.71 % (2305483)Termination phase: Saturation % 26.66/4.71 % (2305483)Time elapsed: 0.094 s % 26.66/4.71 % (2305483)Peak memory usage: 89 MB % 26.66/4.71 % (2305483)Instructions burned: 146 (million) % 26.66/4.71 % (2305488)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=3498795938:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi) % 26.66/4.71 % (2305480)Instruction limit reached! % 26.66/4.71 % (2305480)------------------------------ % 26.66/4.71 % (2305480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.66/4.71 % (2305480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.71 % (2305480)CaDiCaL version: 2.1.3 % 26.66/4.71 % (2305480)Termination reason: Instruction limit % 26.66/4.71 % (2305480)Termination phase: Saturation % 26.66/4.71 % (2305480)Time elapsed: 0.172 s % 26.66/4.71 % (2305480)Peak memory usage: 91 MB % 26.66/4.71 % (2305480)Instructions burned: 274 (million) % 26.66/4.71 % (2305478)------------------------------ % 26.66/4.71 % (2305478)------------------------------ % 26.66/4.71 % (2305490)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3646779526:i=1052:rtra=on_2970 on theBenchmark for (2970ds/1052Mi) % 26.66/4.71 % (2305491)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2858445683:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2970 on theBenchmark for (2970ds/655Mi) % 26.66/4.71 % (2305492)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3821667365:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2970 on theBenchmark for (2970ds/1054Mi) % 26.66/4.71 % (2305492)Refutation not found, incomplete strategy % 26.66/4.71 % (2305492)------------------------------ % 26.66/4.71 % (2305492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.66/4.71 % (2305492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.71 % (2305492)CaDiCaL version: 2.1.3 % 26.66/4.71 % (2305492)Termination reason: Refutation not found, incomplete strategy % 26.66/4.71 % (2305492)Time elapsed: 0.001 s % 26.66/4.71 % (2305492)Peak memory usage: 87 MB % 26.66/4.71 % (2305488)Instruction limit reached! % 26.66/4.71 % (2305488)------------------------------ % 26.66/4.71 % (2305488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.66/4.71 % (2305488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.66/4.71 % (2305488)CaDiCaL version: 2.1.3 % 26.66/4.71 % (2305488)Termination reason: Instruction limit % 26.66/4.71 % (2305488)Termination phase: Saturation % 26.66/4.71 % (2305488)Time elapsed: 0.116 s % 26.66/4.71 % (2305488)Peak memory usage: 134 MB % 26.66/4.71 % (2305488)Instructions burned: 277 (million) % 26.66/4.71 % (2305494)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=593119266:i=107:rtra=on_2970 on theBenchmark for (2970ds/107Mi) % 28.96/4.99 % (2305494)Refutation not found, incomplete strategy % 28.96/4.99 % (2305494)------------------------------ % 28.96/4.99 % (2305494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/4.99 % (2305494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/4.99 % (2305494)CaDiCaL version: 2.1.3 % 28.96/4.99 % (2305494)Termination reason: Refutation not found, incomplete strategy % 28.96/4.99 % (2305494)Time elapsed: 0.027 s % 28.96/4.99 % (2305494)Peak memory usage: 112 MB % 28.96/4.99 % (2305494)Instructions burned: 6 (million) % 28.96/4.99 % (2305499)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 % 28.96/4.99 % (2305499)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1089116995:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 28.96/4.99 % (2305496)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=782393349:s2a=on:i=450:doe=on:nm=32:rtra=on_2969 on theBenchmark for (2969ds/450Mi) % 28.96/4.99 % (2305492)------------------------------ % 28.96/4.99 % (2305492)------------------------------ % 28.96/4.99 % (2305494)------------------------------ % 28.96/4.99 % (2305494)------------------------------ % 28.96/4.99 % (2305491)Instruction limit reached! % 28.96/4.99 % (2305491)------------------------------ % 28.96/4.99 % (2305491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/4.99 % (2305491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/4.99 % (2305491)CaDiCaL version: 2.1.3 % 28.96/4.99 % (2305491)Termination reason: Instruction limit % 28.96/4.99 % (2305491)Termination phase: Saturation % 28.96/4.99 % (2305491)Time elapsed: 0.351 s % 28.96/4.99 % (2305491)Peak memory usage: 92 MB % 28.96/4.99 % (2305491)Instructions burned: 657 (million) % 28.96/4.99 % (2305503)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2908185439:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2967 on theBenchmark for (2967ds/130Mi) % 28.96/4.99 % (2305496)Instruction limit reached! % 28.96/4.99 % (2305496)------------------------------ % 28.96/4.99 % (2305496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/4.99 % (2305496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/4.99 % (2305496)CaDiCaL version: 2.1.3 % 28.96/4.99 % (2305496)Termination reason: Instruction limit % 28.96/4.99 % (2305496)Termination phase: Saturation % 28.96/4.99 % (2305496)Time elapsed: 0.310 s % 28.96/4.99 % (2305496)Peak memory usage: 134 MB % 28.96/4.99 % (2305496)Instructions burned: 451 (million) % 28.96/4.99 % (2305504)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2582678386:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi) % 28.96/4.99 % (2305499)Instruction limit reached! % 28.96/4.99 % (2305499)------------------------------ % 28.96/4.99 % (2305499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/4.99 % (2305499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/4.99 % (2305499)CaDiCaL version: 2.1.3 % 28.96/4.99 % (2305499)Termination reason: Instruction limit % 28.96/4.99 % (2305499)Termination phase: Saturation % 28.96/4.99 % (2305499)Time elapsed: 0.348 s % 28.96/4.99 % (2305499)Peak memory usage: 121 MB % 28.96/4.99 % (2305499)Instructions burned: 1092 (million) % 28.96/4.99 % (2305505)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=726713108:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi) % 28.96/4.99 % (2305505)Refutation not found, incomplete strategy % 28.96/4.99 % (2305505)------------------------------ % 28.96/4.99 % (2305505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.96/4.99 % (2305505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/4.99 % (2305505)CaDiCaL version: 2.1.3 % 28.96/4.99 % (2305505)Termination reason: Refutation not found, incomplete strategy % 28.96/4.99 % (2305505)Time elapsed: 0.002 s % 28.96/4.99 % (2305505)Peak memory usage: 88 MB % 28.96/4.99 % (2305505)Instructions burned: 1 (million) % 28.96/4.99 % (2305503)Instruction limit reached! % 28.96/4.99 % (2305503)------------------------------ % 33.92/5.54 % (2305503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.92/5.54 % (2305503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.92/5.54 % (2305503)CaDiCaL version: 2.1.3 % 33.92/5.54 % (2305503)Termination reason: Instruction limit % 33.92/5.54 % (2305503)Termination phase: Saturation % 33.92/5.54 % (2305503)Time elapsed: 0.102 s % 33.92/5.54 % (2305503)Peak memory usage: 116 MB % 33.92/5.54 % (2305503)Instructions burned: 131 (million) % 33.92/5.54 % (2305509)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=4526546:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi) % 33.92/5.54 % (2305509)Refutation not found, incomplete strategy % 33.92/5.54 % (2305509)------------------------------ % 33.92/5.54 % (2305509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.92/5.54 % (2305509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.92/5.54 % (2305509)CaDiCaL version: 2.1.3 % 33.92/5.54 % (2305509)Termination reason: Refutation not found, incomplete strategy % 33.92/5.54 % (2305509)Time elapsed: 0.001 s % 33.92/5.54 % (2305509)Peak memory usage: 88 MB % 33.92/5.54 % (2305509)Instructions burned: 2 (million) % 33.92/5.54 % (2305507)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2935737919:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi) % 33.92/5.54 % (2305490)Instruction limit reached! % 33.92/5.54 % (2305490)------------------------------ % 33.92/5.54 % (2305490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.92/5.54 % (2305490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.92/5.54 % (2305490)CaDiCaL version: 2.1.3 % 33.92/5.54 % (2305490)Termination reason: Instruction limit % 33.92/5.54 % (2305490)Termination phase: Saturation % 33.92/5.54 % (2305490)Time elapsed: 0.624 s % 33.92/5.54 % (2305490)Peak memory usage: 91 MB % 33.92/5.54 % (2305490)Instructions burned: 1053 (million) % 33.92/5.54 % (2305511)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1764670142:i=776:doe=on:rtra=on_2964 on theBenchmark for (2964ds/776Mi) % 33.92/5.54 % (2305504)Instruction limit reached! % 33.92/5.54 % (2305504)------------------------------ % 33.92/5.54 % (2305504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.92/5.54 % (2305504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.92/5.54 % (2305504)CaDiCaL version: 2.1.3 % 33.92/5.54 % (2305504)Termination reason: Instruction limit % 33.92/5.54 % (2305504)Termination phase: Saturation % 33.92/5.54 % (2305504)Time elapsed: 0.211 s % 33.92/5.54 % (2305504)Peak memory usage: 117 MB % 33.92/5.54 % (2305504)Instructions burned: 312 (million) % 33.92/5.54 % (2305509)------------------------------ % 33.92/5.54 % (2305509)------------------------------ % 33.92/5.54 % (2305505)------------------------------ % 33.92/5.54 % (2305505)------------------------------ % 33.92/5.54 % (2305514)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=566454545:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/646Mi) % 33.92/5.54 % (2305517)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=807339252:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi) % 33.92/5.54 % (2305516)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=320975170:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2963 on theBenchmark for (2963ds/784Mi) % 33.92/5.54 % (2305519)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=1124157135:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2962 on theBenchmark for (2962ds/246Mi) % 33.92/5.54 % (2305519)Refutation not found, incomplete strategy % 33.92/5.54 % (2305519)------------------------------ % 33.92/5.54 % (2305519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.92/5.54 % (2305519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.92/5.54 % (2305519)CaDiCaL version: 2.1.3 % 33.92/5.54 % (2305519)Termination reason: Refutation not found, incomplete strategy % 33.92/5.54 % (2305519)Time elapsed: 0.025 s % 33.92/5.54 % (2305519)Peak memory usage: 111 MB % 33.92/5.54 % (2305519)Instructions burned: 5 (million) % 33.92/5.54 % (2305507)Instruction limit reached! % 39.13/6.14 % (2305507)------------------------------ % 39.13/6.14 % (2305507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.13/6.14 % (2305507)CaDiCaL version: 2.1.3 % 39.13/6.14 % (2305507)Termination reason: Instruction limit % 39.13/6.14 % (2305507)Termination phase: Saturation % 39.13/6.14 % (2305507)Time elapsed: 0.456 s % 39.13/6.14 % (2305507)Peak memory usage: 92 MB % 39.13/6.14 % (2305507)Instructions burned: 836 (million) % 39.13/6.14 % (2305511)Instruction limit reached! % 39.13/6.14 % (2305511)------------------------------ % 39.13/6.14 % (2305511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.13/6.14 % (2305511)CaDiCaL version: 2.1.3 % 39.13/6.14 % (2305511)Termination reason: Instruction limit % 39.13/6.14 % (2305511)Termination phase: Saturation % 39.13/6.14 % (2305511)Time elapsed: 0.488 s % 39.13/6.14 % (2305511)Peak memory usage: 121 MB % 39.13/6.14 % (2305511)Instructions burned: 777 (million) % 39.13/6.14 % (2305519)------------------------------ % 39.13/6.14 % (2305519)------------------------------ % 39.13/6.14 % (2305517)Instruction limit reached! % 39.13/6.14 % (2305517)------------------------------ % 39.13/6.14 % (2305517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.13/6.14 % (2305517)CaDiCaL version: 2.1.3 % 39.13/6.14 % (2305517)Termination reason: Instruction limit % 39.13/6.14 % (2305517)Termination phase: Saturation % 39.13/6.14 % (2305517)Time elapsed: 0.368 s % 39.13/6.14 % (2305517)Peak memory usage: 126 MB % 39.13/6.14 % (2305517)Instructions burned: 1132 (million) % 39.13/6.14 % (2305523)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1540660293:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/775Mi) % 39.13/6.14 % (2305523)Refutation not found, incomplete strategy % 39.13/6.14 % (2305523)------------------------------ % 39.13/6.14 % (2305523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.13/6.14 % (2305523)CaDiCaL version: 2.1.3 % 39.13/6.14 % (2305523)Termination reason: Refutation not found, incomplete strategy % 39.13/6.14 % (2305523)Time elapsed: 0.001 s % 39.13/6.14 % (2305523)Peak memory usage: 87 MB % 39.13/6.14 % (2305514)Instruction limit reached! % 39.13/6.14 % (2305514)------------------------------ % 39.13/6.14 % (2305514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.13/6.14 % (2305514)CaDiCaL version: 2.1.3 % 39.13/6.14 % (2305514)Termination reason: Instruction limit % 39.13/6.14 % (2305514)Termination phase: Saturation % 39.13/6.14 % (2305514)Time elapsed: 0.472 s % 39.13/6.14 % (2305514)Peak memory usage: 138 MB % 39.13/6.14 % (2305514)Instructions burned: 646 (million) % 39.13/6.14 % (2305527)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1951612897:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2958 on theBenchmark for (2958ds/1094Mi) % 39.13/6.14 % (2305525)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2944682782:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi) % 39.13/6.14 % (2305524)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=757985415:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.13/6.14 % (2305516)Instruction limit reached! % 39.13/6.14 % (2305516)------------------------------ % 39.13/6.14 % (2305516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.13/6.14 % (2305516)CaDiCaL version: 2.1.3 % 39.13/6.14 % (2305516)Termination reason: Instruction limit % 39.13/6.14 % (2305516)Termination phase: Saturation % 39.13/6.14 % (2305516)Time elapsed: 0.494 s % 39.13/6.14 % (2305516)Peak memory usage: 120 MB % 39.13/6.14 % (2305516)Instructions burned: 784 (million) % 39.13/6.14 % (2305525)Instruction limit reached! % 39.13/6.14 % (2305525)------------------------------ % 39.13/6.14 % (2305525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.13/6.14 % (2305525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.02/8.50 % (2305525)CaDiCaL version: 2.1.3 % 56.02/8.50 % (2305525)Termination reason: Instruction limit % 56.02/8.50 % (2305525)Termination phase: Saturation % 56.02/8.50 % (2305525)Time elapsed: 0.060 s % 56.02/8.50 % (2305525)Peak memory usage: 89 MB % 56.02/8.50 % (2305525)Instructions burned: 102 (million) % 56.02/8.50 % (2305528)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2961347784:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi) % 56.02/8.50 % (2305523)------------------------------ % 56.02/8.50 % (2305523)------------------------------ % 56.02/8.50 % (2305532)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=3599035671:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/868Mi) % 56.02/8.50 % (2305524)Instruction limit reached! % 56.02/8.50 % (2305524)------------------------------ % 56.02/8.50 % (2305524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.02/8.50 % (2305524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.02/8.50 % (2305524)CaDiCaL version: 2.1.3 % 56.02/8.50 % (2305524)Termination reason: Instruction limit % 56.02/8.50 % (2305524)Termination phase: Saturation % 56.02/8.50 % (2305524)Time elapsed: 0.176 s % 56.02/8.50 % (2305524)Peak memory usage: 91 MB % 56.02/8.50 % (2305524)Instructions burned: 274 (million) % 56.02/8.50 % (2305533)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=2294841342:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi) % 56.02/8.50 % (2305533)Refutation not found, incomplete strategy % 56.02/8.50 % (2305533)------------------------------ % 56.02/8.50 % (2305533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.02/8.50 % (2305533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.02/8.50 % (2305533)CaDiCaL version: 2.1.3 % 56.02/8.50 % (2305533)Termination reason: Refutation not found, incomplete strategy % 56.02/8.50 % (2305533)Time elapsed: 0.002 s % 56.02/8.50 % (2305533)Peak memory usage: 88 MB % 56.02/8.50 % (2305533)Instructions burned: 1 (million) % 56.02/8.50 % (2305535)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1489541872:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi) % 56.02/8.50 % (2305538)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3382213689:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi) % 56.02/8.50 % (2305527)Instruction limit reached! % 56.02/8.50 % (2305527)------------------------------ % 56.02/8.50 % (2305527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.02/8.50 % (2305527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.02/8.50 % (2305527)CaDiCaL version: 2.1.3 % 56.02/8.50 % (2305527)Termination reason: Instruction limit % 56.02/8.50 % (2305527)Termination phase: Saturation % 56.02/8.50 % (2305527)Time elapsed: 0.348 s % 56.02/8.50 % (2305527)Peak memory usage: 92 MB % 56.02/8.50 % (2305527)Instructions burned: 1097 (million) % 56.02/8.50 % (2305541)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=2282833739:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/863Mi) % 56.02/8.50 % (2305533)------------------------------ % 56.02/8.50 % (2305533)------------------------------ % 56.02/8.50 % (2305538)Instruction limit reached! % 56.02/8.50 % (2305538)------------------------------ % 56.02/8.50 % (2305538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.02/8.50 % (2305538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.02/8.50 % (2305538)CaDiCaL version: 2.1.3 % 56.02/8.50 % (2305538)Termination reason: Instruction limit % 56.02/8.50 % (2305538)Termination phase: Saturation % 56.02/8.50 % (2305538)Time elapsed: 0.177 s % 56.02/8.50 % (2305538)Peak memory usage: 91 MB % 56.02/8.50 % (2305538)Instructions burned: 274 (million) % 56.02/8.50 % (2305543)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4010430758:i=5811:kws=precedence:nm=0:rtra=on_2952 on theBenchmark for (2952ds/5811Mi) % 56.02/8.50 % (2305544)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=2655659508:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 59.79/9.04 % (2305541)Instruction limit reached! % 59.79/9.04 % (2305541)------------------------------ % 59.79/9.04 % (2305541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.79/9.04 % (2305541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.79/9.04 % (2305541)CaDiCaL version: 2.1.3 % 59.79/9.04 % (2305541)Termination reason: Instruction limit % 59.79/9.04 % (2305541)Termination phase: Saturation % 59.79/9.04 % (2305541)Time elapsed: 0.270 s % 59.79/9.04 % (2305541)Peak memory usage: 119 MB % 59.79/9.04 % (2305541)Instructions burned: 866 (million) % 59.79/9.04 % (2305532)Instruction limit reached! % 59.79/9.04 % (2305532)------------------------------ % 59.79/9.04 % (2305532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.79/9.04 % (2305532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.79/9.04 % (2305532)CaDiCaL version: 2.1.3 % 59.79/9.04 % (2305532)Termination reason: Instruction limit % 59.79/9.04 % (2305532)Termination phase: Saturation % 59.79/9.04 % (2305532)Time elapsed: 0.544 s % 59.79/9.04 % (2305532)Peak memory usage: 120 MB % 59.79/9.04 % (2305532)Instructions burned: 868 (million) % 59.79/9.04 % (2305547)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=629528709:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/801Mi) % 59.79/9.04 % (2305548)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3281569027:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2949 on theBenchmark for (2949ds/1026Mi) % 59.79/9.04 % (2305548)Refutation not found, incomplete strategy % 59.79/9.04 % (2305548)------------------------------ % 59.79/9.04 % (2305548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.79/9.04 % (2305548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.79/9.04 % (2305548)CaDiCaL version: 2.1.3 % 59.79/9.04 % (2305548)Termination reason: Refutation not found, incomplete strategy % 59.79/9.04 % (2305548)Time elapsed: 0.001 s % 59.79/9.04 % (2305548)Peak memory usage: 87 MB % 59.79/9.04 % (2305547)Instruction limit reached! % 59.79/9.04 % (2305547)------------------------------ % 59.79/9.04 % (2305547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.79/9.04 % (2305547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.79/9.04 % (2305547)CaDiCaL version: 2.1.3 % 59.79/9.04 % (2305547)Termination reason: Instruction limit % 59.79/9.04 % (2305547)Termination phase: Saturation % 59.79/9.04 % (2305547)Time elapsed: 0.224 s % 59.79/9.04 % (2305547)Peak memory usage: 92 MB % 59.79/9.04 % (2305547)Instructions burned: 802 (million) % 59.79/9.04 % (2305485)Instruction limit reached! % 59.79/9.04 % (2305485)------------------------------ % 59.79/9.04 % (2305485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.79/9.04 % (2305485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.79/9.04 % (2305485)CaDiCaL version: 2.1.3 % 59.79/9.04 % (2305485)Termination reason: Instruction limit % 59.79/9.04 % (2305485)Termination phase: Saturation % 59.79/9.04 % (2305485)Time elapsed: 2.427 s % 59.79/9.04 % (2305485)Peak memory usage: 111 MB % 59.79/9.04 % (2305485)Instructions burned: 4429 (million) % 59.79/9.04 % (2305548)------------------------------ % 59.79/9.04 % (2305548)------------------------------ % 59.79/9.04 % (2305551)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1332469652:i=3509:rtra=on_2947 on theBenchmark for (2947ds/3509Mi) % 59.79/9.04 % (2305552)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=955337773:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2946 on theBenchmark for (2946ds/2127Mi) % 59.79/9.04 % (2305552)Refutation not found, incomplete strategy % 59.79/9.04 % (2305552)------------------------------ % 59.79/9.04 % (2305552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.79/9.04 % (2305552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.79/9.04 % (2305552)CaDiCaL version: 2.1.3 % 59.79/9.04 % (2305552)Termination reason: Refutation not found, incomplete strategy % 59.79/9.04 % (2305552)Time elapsed: 0.001 s % 59.79/9.04 % (2305552)Peak memory usage: 87 MB % 59.79/9.04 % (2305553)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3417268850:i=1959:rtra=on:fsd=on:proc=on_2946 on theBenchmark for (2946ds/1959Mi) % 81.85/12.18 % (2305552)------------------------------ % 81.85/12.18 % (2305552)------------------------------ % 81.85/12.18 % (2305557)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1915422828:s2a=on:i=3553:nm=0:rtra=on_2943 on theBenchmark for (2943ds/3553Mi) % 81.85/12.18 % (2305544)Instruction limit reached! % 81.85/12.18 % (2305544)------------------------------ % 81.85/12.18 % (2305544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.85/12.18 % (2305544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.85/12.18 % (2305544)CaDiCaL version: 2.1.3 % 81.85/12.18 % (2305544)Termination reason: Instruction limit % 81.85/12.18 % (2305544)Termination phase: Saturation % 81.85/12.18 % (2305544)Time elapsed: 1.215 s % 81.85/12.18 % (2305544)Peak memory usage: 130 MB % 81.85/12.18 % (2305544)Instructions burned: 2217 (million) % 81.85/12.18 % (2305559)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1683479734:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2938 on theBenchmark for (2938ds/3201Mi) % 81.85/12.18 % (2305553)Instruction limit reached! % 81.85/12.18 % (2305553)------------------------------ % 81.85/12.18 % (2305553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.85/12.18 % (2305553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.85/12.18 % (2305553)CaDiCaL version: 2.1.3 % 81.85/12.18 % (2305553)Termination reason: Instruction limit % 81.85/12.18 % (2305553)Termination phase: Saturation % 81.85/12.18 % (2305553)Time elapsed: 0.908 s % 81.85/12.18 % (2305553)Peak memory usage: 118 MB % 81.85/12.18 % (2305553)Instructions burned: 1960 (million) % 81.85/12.18 % (2305561)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=4166697279:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2935 on theBenchmark for (2935ds/4093Mi) % 81.85/12.18 % (2305551)Instruction limit reached! % 81.85/12.18 % (2305551)------------------------------ % 81.85/12.18 % (2305551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.85/12.18 % (2305551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.85/12.18 % (2305551)CaDiCaL version: 2.1.3 % 81.85/12.18 % (2305551)Termination reason: Instruction limit % 81.85/12.18 % (2305551)Termination phase: Saturation % 81.85/12.18 % (2305551)Time elapsed: 1.245 s % 81.85/12.18 % (2305551)Peak memory usage: 101 MB % 81.85/12.18 % (2305551)Instructions burned: 3511 (million) % 81.85/12.18 % (2305563)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=3229755535:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2933 on theBenchmark for (2933ds/21173Mi) % 81.85/12.18 % (2305563)Refutation not found, incomplete strategy % 81.85/12.18 % (2305563)------------------------------ % 81.85/12.18 % (2305563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.85/12.18 % (2305563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.85/12.18 % (2305563)CaDiCaL version: 2.1.3 % 81.85/12.18 % (2305563)Termination reason: Refutation not found, incomplete strategy % 81.85/12.18 % (2305563)Time elapsed: 0.015 s % 81.85/12.18 % (2305563)Peak memory usage: 112 MB % 81.85/12.18 % (2305563)Instructions burned: 5 (million) % 81.85/12.18 % (2305563)------------------------------ % 81.85/12.18 % (2305563)------------------------------ % 81.85/12.18 % (2305565)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3960203781:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2931 on theBenchmark for (2931ds/10544Mi) % 81.85/12.18 % (2305528)Instruction limit reached! % 81.85/12.18 % (2305528)------------------------------ % 81.85/12.18 % (2305528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.85/12.18 % (2305528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.85/12.18 % (2305528)CaDiCaL version: 2.1.3 % 81.85/12.18 % (2305528)Termination reason: Instruction limit % 81.85/12.18 % (2305528)Termination phase: Saturation % 81.85/12.18 % (2305528)Time elapsed: 3.444 s % 81.85/12.18 % (2305528)Peak memory usage: 117 MB % 81.85/12.18 % (2305528)Instructions burned: 6400 (million) % 81.85/12.18 % (2305559)Instruction limit reached! % 81.85/12.18 % (2305559)------------------------------ % 81.85/12.18 % (2305559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.85/12.18 % (2305559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.66/13.97 % (2305559)CaDiCaL version: 2.1.3 % 93.66/13.97 % (2305559)Termination reason: Instruction limit % 93.66/13.97 % (2305559)Termination phase: Saturation % 93.66/13.97 % (2305559)Time elapsed: 1.615 s % 93.66/13.97 % (2305559)Peak memory usage: 123 MB % 93.66/13.97 % (2305559)Instructions burned: 3201 (million) % 93.66/13.97 % (2305567)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=288090541:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2921 on theBenchmark for (2921ds/1262Mi) % 93.66/13.97 % (2305568)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2775453846:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2921 on theBenchmark for (2921ds/775Mi) % 93.66/13.97 % (2305568)Refutation not found, incomplete strategy % 93.66/13.97 % (2305568)------------------------------ % 93.66/13.97 % (2305568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.66/13.97 % (2305568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.66/13.97 % (2305568)CaDiCaL version: 2.1.3 % 93.66/13.97 % (2305568)Termination reason: Refutation not found, incomplete strategy % 93.66/13.97 % (2305568)Time elapsed: 0.001 s % 93.66/13.97 % (2305568)Peak memory usage: 87 MB % 93.66/13.97 % (2305543)Instruction limit reached! % 93.66/13.97 % (2305543)------------------------------ % 93.66/13.97 % (2305543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.66/13.97 % (2305543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.66/13.97 % (2305543)CaDiCaL version: 2.1.3 % 93.66/13.97 % (2305543)Termination reason: Instruction limit % 93.66/13.97 % (2305543)Termination phase: Saturation % 93.66/13.97 % (2305543)Time elapsed: 3.165 s % 93.66/13.97 % (2305543)Peak memory usage: 131 MB % 93.66/13.97 % (2305543)Instructions burned: 5811 (million) % 93.66/13.97 % (2305571)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=355198213:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2919 on theBenchmark for (2919ds/270Mi) % 93.66/13.97 % (2305557)Instruction limit reached! % 93.66/13.97 % (2305557)------------------------------ % 93.66/13.97 % (2305557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.66/13.97 % (2305557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.66/13.97 % (2305557)CaDiCaL version: 2.1.3 % 93.66/13.97 % (2305557)Termination reason: Instruction limit % 93.66/13.97 % (2305557)Termination phase: Saturation % 93.66/13.97 % (2305557)Time elapsed: 2.365 s % 93.66/13.97 % (2305557)Peak memory usage: 103 MB % 93.66/13.97 % (2305557)Instructions burned: 3554 (million) % 93.66/13.97 % (2305568)------------------------------ % 93.66/13.97 % (2305568)------------------------------ % 93.66/13.97 % (2305561)Instruction limit reached! % 93.66/13.97 % (2305561)------------------------------ % 93.66/13.97 % (2305561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.66/13.97 % (2305561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.66/13.97 % (2305561)CaDiCaL version: 2.1.3 % 93.66/13.97 % (2305561)Termination reason: Instruction limit % 93.66/13.97 % (2305561)Termination phase: Saturation % 93.66/13.97 % (2305561)Time elapsed: 1.712 s % 93.66/13.97 % (2305561)Peak memory usage: 141 MB % 93.66/13.97 % (2305561)Instructions burned: 4095 (million) % 93.66/13.97 % (2305573)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2875956849:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2918 on theBenchmark for (2918ds/17165Mi) % 93.66/13.97 % (2305571)Instruction limit reached! % 93.66/13.97 % (2305571)------------------------------ % 93.66/13.97 % (2305571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.66/13.97 % (2305571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.66/13.97 % (2305571)CaDiCaL version: 2.1.3 % 93.66/13.97 % (2305571)Termination reason: Instruction limit % 93.66/13.97 % (2305571)Termination phase: Saturation % 93.66/13.97 % (2305571)Time elapsed: 0.171 s % 93.66/13.97 % (2305571)Peak memory usage: 91 MB % 93.66/13.97 % (2305571)Instructions burned: 271 (million) % 93.66/13.97 % (2305574)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1362111855:s2a=on:i=13094:s2at=-1:rtra=on_2917 on theBenchmark for (2917ds/13094Mi) % 93.66/13.97 % (2305575)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1522777449:st=2:i=12633:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/12633Mi) % 93.66/13.97 % (2305575)Refutation not found, incomplete strategy % 122.75/18.00 % (2305575)------------------------------ % 122.75/18.00 % (2305575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.75/18.00 % (2305575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/18.00 % (2305575)CaDiCaL version: 2.1.3 % 122.75/18.00 % (2305575)Termination reason: Refutation not found, incomplete strategy % 122.75/18.00 % (2305575)Time elapsed: 0.001 s % 122.75/18.00 % (2305575)Peak memory usage: 87 MB % 122.75/18.00 % (2305577)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=686430013:i=1783:rtra=on:gtg=position_2916 on theBenchmark for (2916ds/1783Mi) % 122.75/18.00 % (2305575)------------------------------ % 122.75/18.00 % (2305575)------------------------------ % 122.75/18.00 % (2305567)Instruction limit reached! % 122.75/18.00 % (2305567)------------------------------ % 122.75/18.00 % (2305567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.75/18.00 % (2305567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/18.00 % (2305567)CaDiCaL version: 2.1.3 % 122.75/18.00 % (2305567)Termination reason: Instruction limit % 122.75/18.00 % (2305567)Termination phase: Saturation % 122.75/18.00 % (2305567)Time elapsed: 0.768 s % 122.75/18.00 % (2305567)Peak memory usage: 126 MB % 122.75/18.00 % (2305567)Instructions burned: 1262 (million) % 122.75/18.00 % (2305581)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=1322741612:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2913 on theBenchmark for (2913ds/5451Mi) % 122.75/18.00 % (2305582)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=2364432463:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2912 on theBenchmark for (2912ds/4975Mi) % 122.75/18.00 % (2305577)Instruction limit reached! % 122.75/18.00 % (2305577)------------------------------ % 122.75/18.00 % (2305577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.75/18.00 % (2305577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/18.00 % (2305577)CaDiCaL version: 2.1.3 % 122.75/18.00 % (2305577)Termination reason: Instruction limit % 122.75/18.00 % (2305577)Termination phase: Saturation % 122.75/18.00 % (2305577)Time elapsed: 1.021 s % 122.75/18.00 % (2305577)Peak memory usage: 127 MB % 122.75/18.00 % (2305577)Instructions burned: 1783 (million) % 122.75/18.00 % (2305585)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=3780852491:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2905 on theBenchmark for (2905ds/2076Mi) % 122.75/18.00 % (2305565)Instruction limit reached! % 122.75/18.00 % (2305565)------------------------------ % 122.75/18.00 % (2305565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.75/18.00 % (2305565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/18.00 % (2305565)CaDiCaL version: 2.1.3 % 122.75/18.00 % (2305565)Termination reason: Instruction limit % 122.75/18.00 % (2305565)Termination phase: Saturation % 122.75/18.00 % (2305565)Time elapsed: 3.507 s % 122.75/18.00 % (2305565)Peak memory usage: 205 MB % 122.75/18.00 % (2305565)Instructions burned: 10548 (million) % 122.75/18.00 % (2305587)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2956396546:i=5145:rtra=on_2894 on theBenchmark for (2894ds/5145Mi) % 122.75/18.00 % (2305585)Instruction limit reached! % 122.75/18.00 % (2305585)------------------------------ % 122.75/18.00 % (2305585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.75/18.00 % (2305585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/18.00 % (2305585)CaDiCaL version: 2.1.3 % 122.75/18.00 % (2305585)Termination reason: Instruction limit % 122.75/18.00 % (2305585)Termination phase: Saturation % 122.75/18.00 % (2305585)Time elapsed: 1.156 s % 122.75/18.00 % (2305585)Peak memory usage: 128 MB % 122.75/18.00 % (2305585)Instructions burned: 2077 (million) % 122.75/18.00 % (2305589)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2807120557:i=3509:rtra=on_2892 on theBenchmark for (2892ds/3509Mi) % 122.75/18.00 % (2305582)Instruction limit reached! % 122.75/18.00 % (2305582)------------------------------ % 122.75/18.00 % (2305582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.75/18.00 % (2305582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/18.00 % (2305582)CaDiCaL version: 2.1.3 % 217.22/31.27 % (2305582)Termination reason: Instruction limit % 217.22/31.27 % (2305582)Termination phase: Saturation % 217.22/31.27 % (2305582)Time elapsed: 2.668 s % 217.22/31.27 % (2305582)Peak memory usage: 129 MB % 217.22/31.27 % (2305582)Instructions burned: 4976 (million) % 217.22/31.27 % (2305591)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2147808984:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2884 on theBenchmark for (2884ds/13800Mi) % 217.22/31.27 % (2305591)Refutation not found, incomplete strategy % 217.22/31.27 % (2305591)------------------------------ % 217.22/31.27 % (2305591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.22/31.27 % (2305591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.22/31.27 % (2305591)CaDiCaL version: 2.1.3 % 217.22/31.27 % (2305591)Termination reason: Refutation not found, incomplete strategy % 217.22/31.27 % (2305591)Time elapsed: 0.001 s % 217.22/31.27 % (2305591)Peak memory usage: 87 MB % 217.22/31.27 % (2305581)Instruction limit reached! % 217.22/31.27 % (2305581)------------------------------ % 217.22/31.27 % (2305581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.22/31.27 % (2305581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.22/31.27 % (2305581)CaDiCaL version: 2.1.3 % 217.22/31.27 % (2305581)Termination reason: Instruction limit % 217.22/31.27 % (2305581)Termination phase: Saturation % 217.22/31.27 % (2305581)Time elapsed: 3.039 s % 217.22/31.27 % (2305581)Peak memory usage: 144 MB % 217.22/31.27 % (2305581)Instructions burned: 5451 (million) % 217.22/31.27 % (2305591)------------------------------ % 217.22/31.27 % (2305591)------------------------------ % 217.22/31.27 % (2305593)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=649752811:i=1412:rtra=on:fsd=on:proc=on_2881 on theBenchmark for (2881ds/1412Mi) % 217.22/31.27 % (2305594)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 % 217.22/31.27 % (2305594)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1857034955:i=11747:aac=none:nm=0:rtra=on:rawr=on_2880 on theBenchmark for (2880ds/11747Mi) % 217.22/31.27 % (2305587)Instruction limit reached! % 217.22/31.27 % (2305587)------------------------------ % 217.22/31.27 % (2305587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.22/31.27 % (2305587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.22/31.27 % (2305587)CaDiCaL version: 2.1.3 % 217.22/31.27 % (2305587)Termination reason: Instruction limit % 217.22/31.27 % (2305587)Termination phase: Saturation % 217.22/31.27 % (2305587)Time elapsed: 1.506 s % 217.22/31.27 % (2305587)Peak memory usage: 97 MB % 217.22/31.27 % (2305587)Instructions burned: 5146 (million) % 217.22/31.27 % (2305597)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3047696028:s2a=on:i=3553:nm=0:rtra=on_2878 on theBenchmark for (2878ds/3553Mi) % 217.22/31.27 % (2305593)Instruction limit reached! % 217.22/31.27 % (2305593)------------------------------ % 217.22/31.27 % (2305593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.22/31.27 % (2305593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.22/31.27 % (2305593)CaDiCaL version: 2.1.3 % 217.22/31.27 % (2305593)Termination reason: Instruction limit % 217.22/31.27 % (2305593)Termination phase: Saturation % 217.22/31.27 % (2305593)Time elapsed: 0.662 s % 217.22/31.27 % (2305593)Peak memory usage: 118 MB % 217.22/31.27 % (2305593)Instructions burned: 1414 (million) % 217.22/31.27 % (2305599)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2449319797:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2873 on theBenchmark for (2873ds/3201Mi) % 217.22/31.27 % (2305589)Instruction limit reached! % 217.22/31.27 % (2305589)------------------------------ % 217.22/31.27 % (2305589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.22/31.27 % (2305589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.22/31.27 % (2305589)CaDiCaL version: 2.1.3 % 217.22/31.27 % (2305589)Termination reason: Instruction limit % 217.22/31.27 % (2305589)Termination phase: Saturation % 217.22/31.27 % (2305589)Time elapsed: 2.270 s % 217.22/31.27 % (2305589)Peak memory usage: 103 MB % 217.22/31.27 % (2305589)Instructions burned: 3509 (million) % 217.22/31.27 % (2305601)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=4006649872:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2868 on theBenchmark for (2868ds/4081Mi) % 233.94/33.65 % (2305597)Instruction limit reached! % 233.94/33.65 % (2305597)------------------------------ % 233.94/33.65 % (2305597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.94/33.65 % (2305597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.94/33.65 % (2305597)CaDiCaL version: 2.1.3 % 233.94/33.65 % (2305597)Termination reason: Instruction limit % 233.94/33.65 % (2305597)Termination phase: Saturation % 233.94/33.65 % (2305597)Time elapsed: 1.254 s % 233.94/33.65 % (2305597)Peak memory usage: 103 MB % 233.94/33.65 % (2305597)Instructions burned: 3555 (million) % 233.94/33.65 % (2305603)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=3225196162:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2865 on theBenchmark for (2865ds/20260Mi) % 233.94/33.65 % (2305603)Refutation not found, incomplete strategy % 233.94/33.65 % (2305603)------------------------------ % 233.94/33.65 % (2305603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.94/33.65 % (2305603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.94/33.65 % (2305603)CaDiCaL version: 2.1.3 % 233.94/33.65 % (2305603)Termination reason: Refutation not found, incomplete strategy % 233.94/33.65 % (2305603)Time elapsed: 0.015 s % 233.94/33.65 % (2305603)Peak memory usage: 112 MB % 233.94/33.65 % (2305603)Instructions burned: 5 (million) % 233.94/33.65 % (2305603)------------------------------ % 233.94/33.65 % (2305603)------------------------------ % 233.94/33.65 % (2305605)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2024821867:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2862 on theBenchmark for (2862ds/58627Mi) % 233.94/33.65 % (2305599)Instruction limit reached! % 233.94/33.65 % (2305599)------------------------------ % 233.94/33.65 % (2305599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.94/33.65 % (2305599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.94/33.65 % (2305599)CaDiCaL version: 2.1.3 % 233.94/33.65 % (2305599)Termination reason: Instruction limit % 233.94/33.65 % (2305599)Termination phase: Saturation % 233.94/33.65 % (2305599)Time elapsed: 1.625 s % 233.94/33.65 % (2305599)Peak memory usage: 124 MB % 233.94/33.65 % (2305599)Instructions burned: 3203 (million) % 233.94/33.65 % (2305607)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1510419784:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2856 on theBenchmark for (2856ds/6258Mi) % 233.94/33.65 % (2305601)Instruction limit reached! % 233.94/33.65 % (2305601)------------------------------ % 233.94/33.65 % (2305601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.94/33.65 % (2305601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.94/33.65 % (2305601)CaDiCaL version: 2.1.3 % 233.94/33.65 % (2305601)Termination reason: Instruction limit % 233.94/33.65 % (2305601)Termination phase: Saturation % 233.94/33.65 % (2305601)Time elapsed: 1.723 s % 233.94/33.65 % (2305601)Peak memory usage: 142 MB % 233.94/33.65 % (2305601)Instructions burned: 4081 (million) % 233.94/33.65 % (2305609)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1242199254:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2849 on theBenchmark for (2849ds/34001Mi) % 233.94/33.65 % (2305574)Instruction limit reached! % 233.94/33.65 % (2305574)------------------------------ % 233.94/33.65 % (2305574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.94/33.65 % (2305574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.94/33.65 % (2305574)CaDiCaL version: 2.1.3 % 233.94/33.65 % (2305574)Termination reason: Instruction limit % 233.94/33.65 % (2305574)Termination phase: Saturation % 233.94/33.65 % (2305574)Time elapsed: 6.965 s % 233.94/33.65 % (2305574)Peak memory usage: 104 MB % 233.94/33.65 % (2305574)Instructions burned: 13095 (million) % 233.94/33.65 % (2305611)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=723103325:s2a=on:i=71622:s2at=-1:rtra=on_2846 on theBenchmark for (2846ds/71622Mi) % 233.94/33.65 % (2305573)Instruction limit reached! % 233.94/33.65 % (2305573)------------------------------ % 233.94/33.65 % (2305573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.94/33.65 % (2305573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.27/36.91 % (2305573)CaDiCaL version: 2.1.3 % 257.27/36.91 % (2305573)Termination reason: Instruction limit % 257.27/36.91 % (2305573)Termination phase: Saturation % 257.27/36.91 % (2305573)Time elapsed: 9.043 s % 257.27/36.91 % (2305573)Peak memory usage: 160 MB % 257.27/36.91 % (2305573)Instructions burned: 17167 (million) % 257.27/36.91 % (2305613)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1896289013:i=24001:kws=precedence:nm=0:rtra=on_2826 on theBenchmark for (2826ds/24001Mi) % 257.27/36.91 % (2305607)Instruction limit reached! % 257.27/36.91 % (2305607)------------------------------ % 257.27/36.91 % (2305607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.27/36.91 % (2305607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.27/36.91 % (2305607)CaDiCaL version: 2.1.3 % 257.27/36.91 % (2305607)Termination reason: Instruction limit % 257.27/36.91 % (2305607)Termination phase: Saturation % 257.27/36.91 % (2305607)Time elapsed: 3.493 s % 257.27/36.91 % (2305607)Peak memory usage: 158 MB % 257.27/36.91 % (2305607)Instructions burned: 6259 (million) % 257.27/36.91 % (2305615)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=1890776899:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2820 on theBenchmark for (2820ds/2076Mi) % 257.27/36.91 % (2305594)Instruction limit reached! % 257.27/36.91 % (2305594)------------------------------ % 257.27/36.91 % (2305594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.27/36.91 % (2305594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.27/36.91 % (2305594)CaDiCaL version: 2.1.3 % 257.27/36.91 % (2305594)Termination reason: Instruction limit % 257.27/36.91 % (2305594)Termination phase: Saturation % 257.27/36.91 % (2305594)Time elapsed: 6.939 s % 257.27/36.91 % (2305594)Peak memory usage: 149 MB % 257.27/36.91 % (2305594)Instructions burned: 11747 (million) % 257.27/36.91 % (2305617)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=4099146978:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2810 on theBenchmark for (2810ds/83971Mi) % 257.27/36.91 % (2305615)Instruction limit reached! % 257.27/36.91 % (2305615)------------------------------ % 257.27/36.91 % (2305615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.27/36.91 % (2305615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.27/36.91 % (2305615)CaDiCaL version: 2.1.3 % 257.27/36.91 % (2305615)Termination reason: Instruction limit % 257.27/36.91 % (2305615)Termination phase: Saturation % 257.27/36.91 % (2305615)Time elapsed: 1.127 s % 257.27/36.91 % (2305615)Peak memory usage: 129 MB % 257.27/36.91 % (2305615)Instructions burned: 2077 (million) % 257.27/36.91 % (2305619)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2619659343:i=83944:rtra=on_2807 on theBenchmark for (2807ds/83944Mi) % 257.27/36.91 % (2305535)Instruction limit reached! % 257.27/36.91 % (2305535)------------------------------ % 257.27/36.91 % (2305535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.27/36.91 % (2305535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.27/36.91 % (2305535)CaDiCaL version: 2.1.3 % 257.27/36.91 % (2305535)Termination reason: Instruction limit % 257.27/36.91 % (2305535)Termination phase: Saturation % 257.27/36.91 % (2305535)Time elapsed: 20.761 s % 257.27/36.91 % (2305535)Peak memory usage: 154 MB % 257.27/36.91 % (2305535)Instructions burned: 36817 (million) % 257.27/36.91 % (2305621)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=994817063:i=9201:rtra=on_2746 on theBenchmark for (2746ds/9201Mi) % 257.27/36.91 % (2305613)Instruction limit reached! % 257.27/36.91 % (2305613)------------------------------ % 257.27/36.91 % (2305613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.27/36.91 % (2305613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.27/36.91 % (2305613)CaDiCaL version: 2.1.3 % 257.27/36.91 % (2305613)Termination reason: Instruction limit % 257.27/36.91 % (2305613)Termination phase: Saturation % 257.27/36.91 % (2305613)Time elapsed: 12.994 s % 257.27/36.91 % (2305613)Peak memory usage: 169 MB % 257.27/36.91 % (2305613)Instructions burned: 24001 (million) % 257.27/36.91 % (2305623)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 % 257.27/36.91 % (2305623)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4185434043:i=6806:aac=none:nm=0:rtra=on:rawr=on_2694 on theBenchmark for (2694ds/6806Mi) % 269.72/38.64 % (2305605)Instruction limit reached! % 269.72/38.64 % (2305605)------------------------------ % 269.72/38.64 % (2305605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.72/38.64 % (2305605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.72/38.64 % (2305605)CaDiCaL version: 2.1.3 % 269.72/38.64 % (2305605)Termination reason: Instruction limit % 269.72/38.64 % (2305605)Termination phase: Saturation % 269.72/38.64 % (2305605)Time elapsed: 17.835 s % 269.72/38.64 % (2305605)Peak memory usage: 174 MB % 269.72/38.64 % (2305605)Instructions burned: 58628 (million) % 269.72/38.64 % (2305621)Instruction limit reached! % 269.72/38.64 % (2305621)------------------------------ % 269.72/38.64 % (2305621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.72/38.64 % (2305621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.72/38.64 % (2305621)CaDiCaL version: 2.1.3 % 269.72/38.64 % (2305621)Termination reason: Instruction limit % 269.72/38.64 % (2305621)Termination phase: Saturation % 269.72/38.64 % (2305621)Time elapsed: 6.267 s % 269.72/38.64 % (2305621)Peak memory usage: 112 MB % 269.72/38.64 % (2305621)Instructions burned: 9202 (million) % 269.72/38.64 % (2305625)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1757551150:s2a=on:i=3553:nm=0:rtra=on_2683 on theBenchmark for (2683ds/3553Mi) % 269.72/38.64 % (2305626)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=830658868:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2682 on theBenchmark for (2682ds/2064Mi) % 269.72/38.64 % (2305609)Instruction limit reached! % 269.72/38.64 % (2305609)------------------------------ % 269.72/38.64 % (2305609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.72/38.64 % (2305609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.72/38.64 % (2305609)CaDiCaL version: 2.1.3 % 269.72/38.64 % (2305609)Termination reason: Instruction limit % 269.72/38.64 % (2305609)Termination phase: Saturation % 269.72/38.64 % (2305609)Time elapsed: 17.114 s % 269.72/38.64 % (2305609)Peak memory usage: 228 MB % 269.72/38.64 % (2305609)Instructions burned: 34002 (million) % 269.72/38.64 % (2305629)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=891118649:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2676 on theBenchmark for (2676ds/20260Mi) % 269.72/38.64 % (2305629)Refutation not found, incomplete strategy % 269.72/38.64 % (2305629)------------------------------ % 269.72/38.64 % (2305629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.72/38.64 % (2305629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.72/38.64 % (2305629)CaDiCaL version: 2.1.3 % 269.72/38.64 % (2305629)Termination reason: Refutation not found, incomplete strategy % 269.72/38.64 % (2305629)Time elapsed: 0.025 s % 269.72/38.64 % (2305629)Peak memory usage: 112 MB % 269.72/38.64 % (2305629)Instructions burned: 5 (million) % 269.72/38.64 % (2305629)------------------------------ % 269.72/38.64 % (2305629)------------------------------ % 269.72/38.64 % (2305626)Instruction limit reached! % 269.72/38.64 % (2305626)------------------------------ % 269.72/38.64 % (2305626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.72/38.64 % (2305626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.72/38.64 % (2305626)CaDiCaL version: 2.1.3 % 269.72/38.64 % (2305626)Termination reason: Instruction limit % 269.72/38.64 % (2305626)Termination phase: Saturation % 269.72/38.64 % (2305626)Time elapsed: 0.917 s % 269.72/38.64 % (2305626)Peak memory usage: 138 MB % 269.72/38.64 % (2305626)Instructions burned: 2065 (million) % 269.72/38.64 % (2305631)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3015382009:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2672 on theBenchmark for (2672ds/1244Mi) % 269.72/38.64 % (2305632)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=1341949995:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2671 on theBenchmark for (2671ds/58261Mi) % 269.72/38.64 % (2305625)Instruction limit reached! % 269.72/38.64 % (2305625)------------------------------ % 269.72/38.64 % (2305625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.30/39.90 % (2305625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.30/39.90 % (2305625)CaDiCaL version: 2.1.3 % 278.30/39.90 % (2305625)Termination reason: Instruction limit % 278.30/39.90 % (2305625)Termination phase: Saturation % 278.30/39.90 % (2305625)Time elapsed: 1.256 s % 278.30/39.90 % (2305625)Peak memory usage: 106 MB % 278.30/39.90 % (2305625)Instructions burned: 3556 (million) % 278.30/39.90 % (2305635)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 % 278.30/39.90 % (2305635)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=60614584:i=6806:aac=none:nm=0:rtra=on:rawr=on_2669 on theBenchmark for (2669ds/6806Mi) % 278.30/39.90 % (2305631)Instruction limit reached! % 278.30/39.90 % (2305631)------------------------------ % 278.30/39.90 % (2305631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.30/39.90 % (2305631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.30/39.90 % (2305631)CaDiCaL version: 2.1.3 % 278.30/39.90 % (2305631)Termination reason: Instruction limit % 278.30/39.90 % (2305631)Termination phase: Saturation % 278.30/39.90 % (2305631)Time elapsed: 0.745 s % 278.30/39.90 % (2305631)Peak memory usage: 126 MB % 278.30/39.90 % (2305631)Instructions burned: 1245 (million) % 278.30/39.90 % (2305637)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=291392119:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2663 on theBenchmark for (2663ds/4081Mi) % 278.30/39.90 % (2305623)Instruction limit reached! % 278.30/39.90 % (2305623)------------------------------ % 278.30/39.90 % (2305623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.30/39.90 % (2305623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.30/39.90 % (2305623)CaDiCaL version: 2.1.3 % 278.30/39.90 % (2305623)Termination reason: Instruction limit % 278.30/39.90 % (2305623)Termination phase: Saturation % 278.30/39.90 % (2305623)Time elapsed: 4.022 s % 278.30/39.90 % (2305623)Peak memory usage: 138 MB % 278.30/39.90 % (2305623)Instructions burned: 6806 (million) % 278.30/39.90 % (2305639)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1586901552:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2653 on theBenchmark for (2653ds/1701Mi) % 278.30/39.90 % (2305635)Instruction limit reached! % 278.30/39.90 % (2305635)------------------------------ % 278.30/39.90 % (2305635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.30/39.90 % (2305635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.30/39.90 % (2305635)CaDiCaL version: 2.1.3 % 278.30/39.90 % (2305635)Termination reason: Instruction limit % 278.30/39.90 % (2305635)Termination phase: Saturation % 278.30/39.90 % (2305635)Time elapsed: 2.119 s % 278.30/39.90 % (2305635)Peak memory usage: 137 MB % 278.30/39.90 % (2305635)Instructions burned: 6808 (million) % 278.30/39.90 % (2305641)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=1800116403:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2647 on theBenchmark for (2647ds/57001Mi) % 278.30/39.90 % (2305639)Instruction limit reached! % 278.30/39.90 % (2305639)------------------------------ % 278.30/39.90 % (2305639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.30/39.90 % (2305639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.30/39.90 % (2305639)CaDiCaL version: 2.1.3 % 278.30/39.90 % (2305639)Termination reason: Instruction limit % 278.30/39.90 % (2305639)Termination phase: Saturation % 278.30/39.90 % (2305639)Time elapsed: 1.004 s % 278.30/39.90 % (2305639)Peak memory usage: 130 MB % 278.30/39.90 % (2305639)Instructions burned: 1702 (million) % 278.30/39.90 % (2305643)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 % 278.30/39.90 % (2305643)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=550379314:i=8622:aac=none:nm=0:rtra=on:rawr=on_2642 on theBenchmark for (2642ds/8622Mi) % 278.30/39.90 % (2305637)Instruction limit reached! % 278.30/39.90 % (2305637)------------------------------ % 278.30/39.90 % (2305637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.49/41.48 % (2305637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.49/41.48 % (2305637)CaDiCaL version: 2.1.3 % 289.49/41.48 % (2305637)Termination reason: Instruction limit % 289.49/41.48 % (2305637)Termination phase: Saturation % 289.49/41.48 % (2305637)Time elapsed: 2.523 s % 289.49/41.48 % (2305637)Peak memory usage: 150 MB % 289.49/41.48 % (2305637)Instructions burned: 4082 (million) % 289.49/41.48 % (2305645)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1185734659:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2637 on theBenchmark for (2637ds/24Mi) % 289.49/41.48 % (2305645)Refutation not found, incomplete strategy % 289.49/41.48 % (2305645)------------------------------ % 289.49/41.48 % (2305645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.49/41.48 % (2305645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.49/41.48 % (2305645)CaDiCaL version: 2.1.3 % 289.49/41.48 % (2305645)Termination reason: Refutation not found, incomplete strategy % 289.49/41.48 % (2305645)Time elapsed: 0.025 s % 289.49/41.48 % (2305645)Peak memory usage: 111 MB % 289.49/41.48 % (2305645)Instructions burned: 5 (million) % 289.49/41.48 % (2305645)------------------------------ % 289.49/41.48 % (2305645)------------------------------ % 289.49/41.48 % (2305647)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2697618077:i=614:kws=precedence:nm=0:rtra=on_2633 on theBenchmark for (2633ds/614Mi) % 289.49/41.48 % (2305647)Instruction limit reached! % 289.49/41.48 % (2305647)------------------------------ % 289.49/41.48 % (2305647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.49/41.48 % (2305647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.49/41.48 % (2305647)CaDiCaL version: 2.1.3 % 289.49/41.48 % (2305647)Termination reason: Instruction limit % 289.49/41.48 % (2305647)Termination phase: Saturation % 289.49/41.48 % (2305647)Time elapsed: 0.368 s % 289.49/41.48 % (2305647)Peak memory usage: 118 MB % 289.49/41.48 % (2305647)Instructions burned: 615 (million) % 289.49/41.48 % (2305649)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2354168161:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2628 on theBenchmark for (2628ds/402Mi) % 289.49/41.48 % (2305649)Instruction limit reached! % 289.49/41.48 % (2305649)------------------------------ % 289.49/41.48 % (2305649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.49/41.48 % (2305649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.49/41.48 % (2305649)CaDiCaL version: 2.1.3 % 289.49/41.48 % (2305649)Termination reason: Instruction limit % 289.49/41.48 % (2305649)Termination phase: Saturation % 289.49/41.48 % (2305649)Time elapsed: 0.268 s % 289.49/41.48 % (2305649)Peak memory usage: 118 MB % 289.49/41.48 % (2305649)Instructions burned: 403 (million) % 289.49/41.48 % (2305651)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=794206442:s2a=on:i=14:rtra=on:inst=on_2624 on theBenchmark for (2624ds/14Mi) % 289.49/41.48 % (2305651)Instruction limit reached! % 289.49/41.48 % (2305651)------------------------------ % 289.49/41.48 % (2305651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.49/41.48 % (2305651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.49/41.48 % (2305651)CaDiCaL version: 2.1.3 % 289.49/41.48 % (2305651)Termination reason: Instruction limit % 289.49/41.48 % (2305651)Termination phase: Saturation % 289.49/41.48 % (2305651)Time elapsed: 0.011 s % 289.49/41.48 % (2305651)Peak memory usage: 88 MB % 289.49/41.48 % (2305651)Instructions burned: 15 (million) % 289.49/41.48 % (2305653)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2744539849:i=8:rtra=on_2622 on theBenchmark for (2622ds/8Mi) % 289.49/41.48 % (2305653)Instruction limit reached! % 289.49/41.48 % (2305653)------------------------------ % 289.49/41.48 % (2305653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.49/41.48 % (2305653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.49/41.48 % (2305653)CaDiCaL version: 2.1.3 % 289.49/41.48 % (2305653)Termination reason: Instruction limit % 289.49/41.48 % (2305653)Termination phase: Saturation % 289.49/41.48 % (2305653)Time elapsed: 0.007 s % 289.49/41.48 % (2305653)Peak memory usage: 88 MB % 289.49/41.48 % (2305653)Instructions burned: 9 (million) % 289.49/41.48 % (2305655)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=298212530:i=92:rtra=on_2621 on theBenchmark for (2621ds/92Mi) % 295.74/42.34 % (2305655)Instruction limit reached! % 295.74/42.34 % (2305655)------------------------------ % 295.74/42.34 % (2305655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.74/42.34 % (2305655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.74/42.34 % (2305655)CaDiCaL version: 2.1.3 % 295.74/42.34 % (2305655)Termination reason: Instruction limit % 295.74/42.34 % (2305655)Termination phase: Saturation % 295.74/42.34 % (2305655)Time elapsed: 0.076 s % 295.74/42.34 % (2305655)Peak memory usage: 115 MB % 295.74/42.34 % (2305655)Instructions burned: 93 (million) % 295.74/42.34 % (2305657)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4219521075:i=66:rtra=on_2619 on theBenchmark for (2619ds/66Mi) % 295.74/42.34 % (2305657)Instruction limit reached! % 295.74/42.34 % (2305657)------------------------------ % 295.74/42.34 % (2305657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.74/42.34 % (2305657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.74/42.34 % (2305657)CaDiCaL version: 2.1.3 % 295.74/42.34 % (2305657)Termination reason: Instruction limit % 295.74/42.34 % (2305657)Termination phase: Saturation % 295.74/42.34 % (2305657)Time elapsed: 0.067 s % 295.74/42.34 % (2305657)Peak memory usage: 116 MB % 295.74/42.34 % (2305657)Instructions burned: 67 (million) % 295.74/42.34 % (2305659)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1618274419:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2617 on theBenchmark for (2617ds/28Mi) % 295.74/42.34 % (2305659)Refutation not found, incomplete strategy % 295.74/42.34 % (2305659)------------------------------ % 295.74/42.34 % (2305659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.74/42.34 % (2305659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.74/42.34 % (2305659)CaDiCaL version: 2.1.3 % 295.74/42.34 % (2305659)Termination reason: Refutation not found, incomplete strategy % 295.74/42.34 % (2305659)Time elapsed: 0.001 s % 295.74/42.34 % (2305659)Peak memory usage: 88 MB % 295.74/42.34 % (2305659)------------------------------ % 295.74/42.34 % (2305659)------------------------------ % 295.74/42.34 % (2305661)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=2850127505:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2613 on theBenchmark for (2613ds/58Mi) % 295.74/42.34 % (2305661)Instruction limit reached! % 295.74/42.34 % (2305661)------------------------------ % 295.74/42.34 % (2305661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.74/42.34 % (2305661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.74/42.34 % (2305661)CaDiCaL version: 2.1.3 % 295.74/42.34 % (2305661)Termination reason: Instruction limit % 295.74/42.34 % (2305661)Termination phase: Saturation % 295.74/42.34 % (2305661)Time elapsed: 0.039 s % 295.74/42.34 % (2305661)Peak memory usage: 89 MB % 295.74/42.34 % (2305661)Instructions burned: 59 (million) % 295.74/42.34 % (2305663)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=489459799:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2611 on theBenchmark for (2611ds/32Mi) % 295.74/42.34 % (2305663)Instruction limit reached! % 295.74/42.34 % (2305663)------------------------------ % 295.74/42.34 % (2305663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.74/42.34 % (2305663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.74/42.34 % (2305663)CaDiCaL version: 2.1.3 % 295.74/42.34 % (2305663)Termination reason: Instruction limit % 295.74/42.34 % (2305663)Termination phase: Saturation % 295.74/42.34 % (2305663)Time elapsed: 0.020 s % 295.74/42.34 % (2305663)Peak memory usage: 90 MB % 295.74/42.34 % (2305663)Instructions burned: 32 (million) % 295.74/42.34 % (2305665)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2363114537:i=48:canc=force:rtra=on_2610 on theBenchmark for (2610ds/48Mi) % 295.74/42.34 % (2305665)Instruction limit reached! % 295.74/42.34 % (2305665)------------------------------ % 295.74/42.34 % (2305665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.74/42.34 % (2305665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.74/42.34 % (2305665)CaDiCaL version: 2.1.3 % 295.74/42.34 % (2305665)Termination reason: Instruction limit % 295.74/42.34 % (2305665)Termination phase: Saturation % 295.74/42.34 % (2305665)Time elapsed: 0.033 s % 295.74/42.34 % (2305665)Peak memory usage: 89 MB % 295.74/42.34 % (2305665)Instructions burned: 49 (million) % 295.74/42.34 % (2305667)ott+1010_8_to=lpo:sil=128000:si=on:nTerminated %------------------------------------------------------------------------------