%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW743_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:31:11 PM UTC 2026 % Result : Timeout 300.30s 43.12s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW743_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.20 % Computer : n001.cluster.edu % 0.11/0.20 % Model : x86_64 x86_64 % 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.20 % Memory : 8046.5625MB % 0.11/0.20 % OS : Linux 6.8.0-71-generic % 0.11/0.20 % CPULimit : 300 % 0.11/0.20 % WCLimit : 300 % 0.11/0.20 % DateTime : Mon Sep 28 14:34:34 UTC 2026 % 0.11/0.20 % CPUTime : % 0.11/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.24 Running first-order theorem proving % 0.11/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.29/1.19 % (388383)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.29/1.19 % (388390)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3006238068:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.29/1.19 % (388393)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4158292808:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.29/1.19 % (388392)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3075530038:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.29/1.19 % (388389)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1923905010:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.29/1.19 % (388391)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3415002316:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.29/1.19 % (388388)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2466122863:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.29/1.19 % (388392)Instruction limit reached! % 3.29/1.19 % (388392)------------------------------ % 3.29/1.19 % (388392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.19 % (388392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.19 % (388392)CaDiCaL version: 2.1.3 % 3.29/1.19 % (388392)Termination reason: Instruction limit % 3.29/1.19 % (388392)Termination phase: Property scanning % 3.29/1.19 % (388392)Time elapsed: 0.002 s % 3.29/1.19 % (388392)Peak memory usage: 85 MB % 3.29/1.19 % (388392)Instructions burned: 4 (million) % 3.29/1.19 % (388391)Instruction limit reached! % 3.29/1.19 % (388391)------------------------------ % 3.29/1.19 % (388391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.19 % (388391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.19 % (388391)CaDiCaL version: 2.1.3 % 3.29/1.19 % (388391)Termination reason: Instruction limit % 3.29/1.19 % (388391)Termination phase: Property scanning % 3.29/1.19 % (388391)Time elapsed: 0.003 s % 3.29/1.19 % (388391)Peak memory usage: 85 MB % 3.29/1.19 % (388391)Instructions burned: 7 (million) % 3.29/1.19 % (388394)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2943693947:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.29/1.19 % (388388)Instruction limit reached! % 3.29/1.19 % (388388)------------------------------ % 3.29/1.19 % (388388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.19 % (388388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.19 % (388388)CaDiCaL version: 2.1.3 % 3.29/1.19 % (388388)Termination reason: Instruction limit % 3.29/1.19 % (388388)Termination phase: Property scanning % 3.29/1.19 % (388388)Time elapsed: 0.005 s % 3.29/1.19 % (388388)Peak memory usage: 85 MB % 3.29/1.19 % (388388)Instructions burned: 13 (million) % 3.29/1.19 % (388394)Instruction limit reached! % 3.29/1.19 % (388394)------------------------------ % 3.29/1.19 % (388394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.19 % (388394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.19 % (388394)CaDiCaL version: 2.1.3 % 3.29/1.19 % (388394)Termination reason: Instruction limit % 3.29/1.19 % (388394)Termination phase: Property scanning % 3.29/1.19 % (388394)Time elapsed: 0.016 s % 3.29/1.19 % (388394)Peak memory usage: 87 MB % 3.29/1.19 % (388394)Instructions burned: 34 (million) % 3.29/1.19 % (388393)Instruction limit reached! % 3.29/1.19 % (388393)------------------------------ % 3.29/1.19 % (388393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.19 % (388393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.19 % (388393)CaDiCaL version: 2.1.3 % 3.29/1.19 % (388393)Termination reason: Instruction limit % 3.29/1.19 % (388393)Termination phase: Saturation % 3.29/1.19 % (388393)Time elapsed: 0.029 s % 3.29/1.19 % (388393)Peak memory usage: 96 MB % 3.29/1.19 % (388393)Instructions burned: 46 (million) % 3.29/1.19 % (388390)Instruction limit reached! % 3.29/1.19 % (388390)------------------------------ % 3.29/1.19 % (388390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.29/1.19 % (388390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.29/1.19 % (388390)CaDiCaL version: 2.1.3 % 4.34/1.35 % (388390)Termination reason: Instruction limit % 4.34/1.35 % (388390)Termination phase: Saturation % 4.34/1.35 % (388390)Time elapsed: 0.083 s % 4.34/1.35 % (388390)Peak memory usage: 120 MB % 4.34/1.35 % (388390)Instructions burned: 203 (million) % 4.34/1.35 % (388407)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4051566641:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.34/1.35 % (388404)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=104170602:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.34/1.35 % (388403)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=1141603082:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.34/1.35 % (388402)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1786517027:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.34/1.35 % (388402)Refutation not found, incomplete strategy % 4.34/1.35 % (388402)------------------------------ % 4.34/1.35 % (388402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.35 % (388402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.35 % (388402)CaDiCaL version: 2.1.3 % 4.34/1.35 % (388402)Termination reason: Refutation not found, incomplete strategy % 4.34/1.35 % (388402)Time elapsed: 0.005 s % 4.34/1.35 % (388402)Peak memory usage: 88 MB % 4.34/1.35 % (388402)Instructions burned: 10 (million) % 4.34/1.35 % (388404)Instruction limit reached! % 4.34/1.35 % (388404)------------------------------ % 4.34/1.35 % (388404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.35 % (388404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.35 % (388404)CaDiCaL version: 2.1.3 % 4.34/1.35 % (388404)Termination reason: Instruction limit % 4.34/1.35 % (388404)Termination phase: Preprocessing 3 % 4.34/1.35 % (388404)Time elapsed: 0.008 s % 4.34/1.35 % (388404)Peak memory usage: 86 MB % 4.34/1.35 % (388404)Instructions burned: 17 (million) % 4.34/1.35 % (388403)Instruction limit reached! % 4.34/1.35 % (388403)------------------------------ % 4.34/1.35 % (388403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.35 % (388403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.35 % (388403)CaDiCaL version: 2.1.3 % 4.34/1.35 % (388403)Termination reason: Instruction limit % 4.34/1.35 % (388403)Termination phase: Clausification % 4.34/1.35 % (388403)Time elapsed: 0.019 s % 4.34/1.35 % (388403)Peak memory usage: 93 MB % 4.34/1.35 % (388403)Instructions burned: 29 (million) % 4.34/1.35 % (388407)Instruction limit reached! % 4.34/1.35 % (388407)------------------------------ % 4.34/1.35 % (388407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.35 % (388407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.35 % (388407)CaDiCaL version: 2.1.3 % 4.34/1.35 % (388407)Termination reason: Instruction limit % 4.34/1.35 % (388407)Termination phase: Saturation % 4.34/1.35 % (388407)Time elapsed: 0.023 s % 4.34/1.35 % (388407)Peak memory usage: 91 MB % 4.34/1.35 % (388407)Instructions burned: 85 (million) % 4.34/1.35 % (388405)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1428408477:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.34/1.35 % (388406)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=3594667769:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi) % 4.34/1.35 % (388405)Instruction limit reached! % 4.34/1.35 % (388405)------------------------------ % 4.34/1.35 % (388405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.35 % (388405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.35 % (388405)CaDiCaL version: 2.1.3 % 4.34/1.35 % (388405)Termination reason: Instruction limit % 4.34/1.35 % (388405)Termination phase: Preprocessing 3 % 4.34/1.35 % (388405)Time elapsed: 0.013 s % 4.34/1.35 % (388405)Peak memory usage: 87 MB % 4.34/1.35 % (388405)Instructions burned: 25 (million) % 4.34/1.35 % (388406)Instruction limit reached! % 4.34/1.35 % (388406)------------------------------ % 4.34/1.35 % (388406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.35 % (388406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.50 % (388406)CaDiCaL version: 2.1.3 % 5.43/1.50 % (388406)Termination reason: Instruction limit % 5.43/1.50 % (388406)Termination phase: Property scanning % 5.43/1.50 % (388406)Time elapsed: 0.015 s % 5.43/1.50 % (388406)Peak memory usage: 87 MB % 5.43/1.50 % (388406)Instructions burned: 31 (million) % 5.43/1.50 % (388414)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3331781898:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.43/1.50 % (388414)Instruction limit reached! % 5.43/1.50 % (388414)------------------------------ % 5.43/1.50 % (388414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.43/1.50 % (388414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.50 % (388414)CaDiCaL version: 2.1.3 % 5.43/1.50 % (388414)Termination reason: Instruction limit % 5.43/1.50 % (388414)Termination phase: Property scanning % 5.43/1.50 % (388414)Time elapsed: 0.002 s % 5.43/1.50 % (388414)Peak memory usage: 85 MB % 5.43/1.50 % (388414)Instructions burned: 8 (million) % 5.43/1.50 % (388412)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2030570133:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi) % 5.43/1.50 % (388412)Instruction limit reached! % 5.43/1.50 % (388412)------------------------------ % 5.43/1.50 % (388412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.43/1.50 % (388412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.50 % (388412)CaDiCaL version: 2.1.3 % 5.43/1.50 % (388412)Termination reason: Instruction limit % 5.43/1.50 % (388412)Termination phase: Property scanning % 5.43/1.50 % (388412)Time elapsed: 0.002 s % 5.43/1.50 % (388412)Peak memory usage: 85 MB % 5.43/1.50 % (388412)Instructions burned: 4 (million) % 5.43/1.50 % (388413)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2782027935:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.43/1.50 % (388413)Refutation not found, incomplete strategy % 5.43/1.50 % (388413)------------------------------ % 5.43/1.50 % (388413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.43/1.50 % (388413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.50 % (388413)CaDiCaL version: 2.1.3 % 5.43/1.50 % (388413)Termination reason: Refutation not found, incomplete strategy % 5.43/1.50 % (388413)Time elapsed: 0.005 s % 5.43/1.50 % (388413)Peak memory usage: 88 MB % 5.43/1.50 % (388413)Instructions burned: 9 (million) % 5.43/1.50 % (388417)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1829729378:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.43/1.50 % (388420)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=526617186:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 5.43/1.50 % (388418)lrs+10_1_thi=all:si=on:fd=off:random_seed=2474307797:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.43/1.50 % (388420)Instruction limit reached! % 5.43/1.50 % (388420)------------------------------ % 5.43/1.50 % (388420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.43/1.50 % (388420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.50 % (388420)CaDiCaL version: 2.1.3 % 5.43/1.50 % (388420)Termination reason: Instruction limit % 5.43/1.50 % (388420)Termination phase: Property scanning % 5.43/1.50 % (388420)Time elapsed: 0.002 s % 5.43/1.50 % (388420)Peak memory usage: 85 MB % 5.43/1.50 % (388420)Instructions burned: 9 (million) % 5.43/1.50 % (388389)Instruction limit reached! % 5.43/1.50 % (388389)------------------------------ % 5.43/1.50 % (388389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.43/1.50 % (388389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.50 % (388389)CaDiCaL version: 2.1.3 % 5.43/1.50 % (388389)Termination reason: Instruction limit % 5.43/1.50 % (388389)Termination phase: Clausification % 5.43/1.50 % (388389)Time elapsed: 0.326 s % 5.43/1.50 % (388389)Peak memory usage: 260 MB % 5.43/1.50 % (388389)Instructions burned: 307 (million) % 5.43/1.50 % (388418)Instruction limit reached! % 5.43/1.50 % (388418)------------------------------ % 5.43/1.50 % (388418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.69 % (388418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.69 % (388418)CaDiCaL version: 2.1.3 % 5.85/1.69 % (388418)Termination reason: Instruction limit % 5.85/1.69 % (388418)Termination phase: Property scanning % 5.85/1.69 % (388418)Time elapsed: 0.024 s % 5.85/1.69 % (388418)Peak memory usage: 88 MB % 5.85/1.69 % (388418)Instructions burned: 55 (million) % 5.85/1.69 % (388417)Instruction limit reached! % 5.85/1.69 % (388417)------------------------------ % 5.85/1.69 % (388417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.69 % (388417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.69 % (388417)CaDiCaL version: 2.1.3 % 5.85/1.69 % (388417)Termination reason: Instruction limit % 5.85/1.69 % (388417)Termination phase: Saturation % 5.85/1.69 % (388417)Time elapsed: 0.074 s % 5.85/1.69 % (388417)Peak memory usage: 130 MB % 5.85/1.69 % (388417)Instructions burned: 67 (million) % 5.85/1.69 % (388402)------------------------------ % 5.85/1.69 % (388402)------------------------------ % 5.85/1.69 % (388422)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=108509087:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 5.85/1.69 % (388422)Instruction limit reached! % 5.85/1.69 % (388422)------------------------------ % 5.85/1.69 % (388422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.69 % (388422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.69 % (388422)CaDiCaL version: 2.1.3 % 5.85/1.69 % (388422)Termination reason: Instruction limit % 5.85/1.69 % (388422)Termination phase: Property scanning % 5.85/1.69 % (388422)Time elapsed: 0.002 s % 5.85/1.69 % (388422)Peak memory usage: 85 MB % 5.85/1.69 % (388422)Instructions burned: 4 (million) % 5.85/1.69 % (388427)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1691349552:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 5.85/1.69 % (388427)Instruction limit reached! % 5.85/1.69 % (388427)------------------------------ % 5.85/1.69 % (388427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.69 % (388427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.69 % (388427)CaDiCaL version: 2.1.3 % 5.85/1.69 % (388427)Termination reason: Instruction limit % 5.85/1.69 % (388427)Termination phase: Property scanning % 5.85/1.69 % (388427)Time elapsed: 0.001 s % 5.85/1.69 % (388427)Peak memory usage: 85 MB % 5.85/1.69 % (388427)Instructions burned: 4 (million) % 5.85/1.69 % (388428)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3451701375:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 5.85/1.69 % (388429)dis+10_1_si=on:random_seed=3400128041:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 5.85/1.69 % (388429)Instruction limit reached! % 5.85/1.69 % (388429)------------------------------ % 5.85/1.69 % (388429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.69 % (388429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.69 % (388429)CaDiCaL version: 2.1.3 % 5.85/1.69 % (388429)Termination reason: Instruction limit % 5.85/1.69 % (388429)Termination phase: Preprocessing 1 % 5.85/1.69 % (388429)Time elapsed: 0.005 s % 5.85/1.69 % (388429)Peak memory usage: 85 MB % 5.85/1.69 % (388429)Instructions burned: 12 (million) % 5.85/1.69 % (388435)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=815209999:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 5.85/1.69 % (388430)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1313309038:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 5.85/1.69 % (388435)Instruction limit reached! % 5.85/1.69 % (388435)------------------------------ % 5.85/1.69 % (388435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.69 % (388435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.69 % (388435)CaDiCaL version: 2.1.3 % 5.85/1.69 % (388435)Termination reason: Instruction limit % 5.85/1.69 % (388435)Termination phase: Property scanning % 5.85/1.69 % (388435)Time elapsed: 0.002 s % 5.85/1.69 % (388435)Peak memory usage: 85 MB % 5.85/1.69 % (388435)Instructions burned: 9 (million) % 5.85/1.69 % (388431)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2044127452: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_2994 on theBenchmark for (2994ds/35Mi) % 7.96/1.97 % (388430)Instruction limit reached! % 7.96/1.97 % (388430)------------------------------ % 7.96/1.97 % (388430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.96/1.97 % (388430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.97 % (388430)CaDiCaL version: 2.1.3 % 7.96/1.97 % (388430)Termination reason: Instruction limit % 7.96/1.97 % (388430)Termination phase: Clausification % 7.96/1.97 % (388430)Time elapsed: 0.013 s % 7.96/1.97 % (388430)Peak memory usage: 87 MB % 7.96/1.97 % (388430)Instructions burned: 27 (million) % 7.96/1.97 % (388431)Instruction limit reached! % 7.96/1.97 % (388431)------------------------------ % 7.96/1.97 % (388431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.96/1.97 % (388431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.97 % (388431)CaDiCaL version: 2.1.3 % 7.96/1.97 % (388431)Termination reason: Instruction limit % 7.96/1.97 % (388431)Termination phase: Property scanning % 7.96/1.97 % (388431)Time elapsed: 0.017 s % 7.96/1.97 % (388431)Peak memory usage: 87 MB % 7.96/1.97 % (388431)Instructions burned: 35 (million) % 7.96/1.97 % (388413)------------------------------ % 7.96/1.97 % (388413)------------------------------ % 7.96/1.97 % (388433)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2783639832:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.96/1.97 % (388433)Instruction limit reached! % 7.96/1.97 % (388433)------------------------------ % 7.96/1.97 % (388433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.96/1.97 % (388433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.97 % (388433)CaDiCaL version: 2.1.3 % 7.96/1.97 % (388433)Termination reason: Instruction limit % 7.96/1.97 % (388433)Termination phase: Property scanning % 7.96/1.97 % (388433)Time elapsed: 0.002 s % 7.96/1.97 % (388433)Peak memory usage: 85 MB % 7.96/1.97 % (388433)Instructions burned: 4 (million) % 7.96/1.97 % (388428)Instruction limit reached! % 7.96/1.97 % (388428)------------------------------ % 7.96/1.97 % (388428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.96/1.97 % (388428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.97 % (388428)CaDiCaL version: 2.1.3 % 7.96/1.97 % (388428)Termination reason: Instruction limit % 7.96/1.97 % (388428)Termination phase: Saturation % 7.96/1.97 % (388428)Time elapsed: 0.096 s % 7.96/1.97 % (388428)Peak memory usage: 118 MB % 7.96/1.97 % (388428)Instructions burned: 127 (million) % 7.96/1.97 % (388441)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=987180665:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.96/1.97 % (388441)Instruction limit reached! % 7.96/1.97 % (388441)------------------------------ % 7.96/1.97 % (388441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.96/1.97 % (388441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.97 % (388441)CaDiCaL version: 2.1.3 % 7.96/1.97 % (388441)Termination reason: Instruction limit % 7.96/1.97 % (388441)Termination phase: Property scanning % 7.96/1.97 % (388441)Time elapsed: 0.003 s % 7.96/1.97 % (388441)Peak memory usage: 85 MB % 7.96/1.97 % (388441)Instructions burned: 15 (million) % 7.96/1.97 % (388438)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1206875423:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 7.96/1.97 % (388443)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=119637487:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.96/1.97 % (388444)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4203420248:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 7.96/1.97 % (388444)Instruction limit reached! % 7.96/1.97 % (388444)------------------------------ % 7.96/1.97 % (388444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.96/1.97 % (388444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.96/1.97 % (388444)CaDiCaL version: 2.1.3 % 7.96/1.97 % (388444)Termination reason: Instruction limit % 7.96/1.97 % (388444)Termination phase: Preprocessing 2 % 7.96/1.97 % (388444)Time elapsed: 0.005 s % 7.96/1.97 % (388444)Peak memory usage: 86 MB % 7.96/1.97 % (388444)Instructions burned: 10 (million) % 10.58/2.21 % (388443)Refutation not found, incomplete strategy % 10.58/2.21 % (388443)------------------------------ % 10.58/2.21 % (388443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.58/2.21 % (388443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.58/2.21 % (388443)CaDiCaL version: 2.1.3 % 10.58/2.21 % (388443)Termination reason: Refutation not found, incomplete strategy % 10.58/2.21 % (388443)Time elapsed: 0.032 s % 10.58/2.21 % (388443)Peak memory usage: 111 MB % 10.58/2.21 % (388443)Instructions burned: 18 (million) % 10.58/2.21 % (388447)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=1415897494:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 10.58/2.21 % (388446)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=649965617:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 10.58/2.21 % (388450)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3416746543:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 10.58/2.21 % (388447)Instruction limit reached! % 10.58/2.21 % (388447)------------------------------ % 10.58/2.21 % (388447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.58/2.21 % (388447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.58/2.21 % (388447)CaDiCaL version: 2.1.3 % 10.58/2.21 % (388447)Termination reason: Instruction limit % 10.58/2.21 % (388447)Termination phase: Saturation % 10.58/2.21 % (388447)Time elapsed: 0.039 s % 10.58/2.21 % (388447)Peak memory usage: 91 MB % 10.58/2.21 % (388447)Instructions burned: 75 (million) % 10.58/2.21 % (388449)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=1045828957:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.58/2.21 % (388450)Instruction limit reached! % 10.58/2.21 % (388450)------------------------------ % 10.58/2.21 % (388450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.58/2.21 % (388450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.58/2.21 % (388450)CaDiCaL version: 2.1.3 % 10.58/2.21 % (388450)Termination reason: Instruction limit % 10.58/2.21 % (388450)Termination phase: Clausification % 10.58/2.21 % (388450)Time elapsed: 0.056 s % 10.58/2.21 % (388450)Peak memory usage: 126 MB % 10.58/2.21 % (388450)Instructions burned: 130 (million) % 10.58/2.21 % (388446)Instruction limit reached! % 10.58/2.21 % (388446)------------------------------ % 10.58/2.21 % (388446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.58/2.21 % (388446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.58/2.21 % (388446)CaDiCaL version: 2.1.3 % 10.58/2.21 % (388446)Termination reason: Instruction limit % 10.58/2.21 % (388446)Termination phase: Saturation % 10.58/2.21 % (388446)Time elapsed: 0.077 s % 10.58/2.21 % (388446)Peak memory usage: 130 MB % 10.58/2.21 % (388446)Instructions burned: 72 (million) % 10.58/2.21 % (388454)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=917032011:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.58/2.21 % (388460)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1372874642:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 10.58/2.21 % (388438)Instruction limit reached! % 10.58/2.21 % (388438)------------------------------ % 10.58/2.21 % (388438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.58/2.21 % (388438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.58/2.21 % (388438)CaDiCaL version: 2.1.3 % 10.58/2.21 % (388438)Termination reason: Instruction limit % 10.58/2.21 % (388438)Termination phase: Saturation % 10.58/2.21 % (388438)Time elapsed: 0.218 s % 10.58/2.21 % (388438)Peak memory usage: 95 MB % 10.58/2.21 % (388438)Instructions burned: 371 (million) % 10.58/2.21 % (388460)Refutation not found, incomplete strategy % 10.58/2.21 % (388460)------------------------------ % 10.58/2.21 % (388460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.58/2.21 % (388460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.58/2.21 % (388460)CaDiCaL version: 2.1.3 % 10.58/2.21 % (388460)Termination reason: Refutation not found, incomplete strategy % 10.58/2.21 % (388460)Time elapsed: 0.023 s % 12.09/2.53 % (388460)Peak memory usage: 91 MB % 12.09/2.53 % (388460)Instructions burned: 84 (million) % 12.09/2.53 % (388458)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2617934546:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 12.09/2.53 % (388458)Instruction limit reached! % 12.09/2.53 % (388458)------------------------------ % 12.09/2.53 % (388458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.53 % (388458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.53 % (388458)CaDiCaL version: 2.1.3 % 12.09/2.53 % (388458)Termination reason: Instruction limit % 12.09/2.53 % (388458)Termination phase: Property scanning % 12.09/2.53 % (388458)Time elapsed: 0.020 s % 12.09/2.53 % (388458)Peak memory usage: 87 MB % 12.09/2.53 % (388458)Instructions burned: 43 (million) % 12.09/2.53 % (388461)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=818480689:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 12.09/2.53 % (388454)Instruction limit reached! % 12.09/2.53 % (388454)------------------------------ % 12.09/2.53 % (388454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.53 % (388454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.53 % (388454)CaDiCaL version: 2.1.3 % 12.09/2.53 % (388454)Termination reason: Instruction limit % 12.09/2.53 % (388454)Termination phase: Saturation % 12.09/2.53 % (388454)Time elapsed: 0.118 s % 12.09/2.53 % (388454)Peak memory usage: 135 MB % 12.09/2.53 % (388454)Instructions burned: 132 (million) % 12.09/2.53 % (388443)------------------------------ % 12.09/2.53 % (388443)------------------------------ % 12.09/2.53 % (388464)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2401036037:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 12.09/2.53 % (388460)------------------------------ % 12.09/2.53 % (388460)------------------------------ % 12.09/2.53 % (388466)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=3743786336:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 12.09/2.53 % (388466)Refutation not found, incomplete strategy % 12.09/2.53 % (388466)------------------------------ % 12.09/2.53 % (388466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.53 % (388466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.53 % (388466)CaDiCaL version: 2.1.3 % 12.09/2.53 % (388466)Termination reason: Refutation not found, incomplete strategy % 12.09/2.53 % (388466)Time elapsed: 0.033 s % 12.09/2.53 % (388466)Peak memory usage: 111 MB % 12.09/2.53 % (388466)Instructions burned: 20 (million) % 12.09/2.53 % (388449)Instruction limit reached! % 12.09/2.53 % (388449)------------------------------ % 12.09/2.53 % (388449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.53 % (388449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.53 % (388449)CaDiCaL version: 2.1.3 % 12.09/2.53 % (388449)Termination reason: Instruction limit % 12.09/2.53 % (388449)Termination phase: Clausification % 12.09/2.53 % (388449)Time elapsed: 0.303 s % 12.09/2.53 % (388449)Peak memory usage: 244 MB % 12.09/2.53 % (388449)Instructions burned: 295 (million) % 12.09/2.53 % (388468)dis+10_1_si=on:random_seed=2608486872:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 12.09/2.53 % (388469)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=24747141:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 12.09/2.53 % (388464)Instruction limit reached! % 12.09/2.53 % (388464)------------------------------ % 12.09/2.53 % (388464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.53 % (388464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.53 % (388464)CaDiCaL version: 2.1.3 % 12.09/2.53 % (388464)Termination reason: Instruction limit % 12.09/2.53 % (388464)Termination phase: Saturation % 12.09/2.53 % (388464)Time elapsed: 0.092 s % 12.09/2.53 % (388464)Peak memory usage: 116 MB % 12.09/2.53 % (388464)Instructions burned: 131 (million) % 12.09/2.53 % (388472)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3571917977:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 12.09/2.53 % (388472)Instruction limit reached! % 12.09/2.53 % (388472)------------------------------ % 13.14/2.71 % (388472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388472)CaDiCaL version: 2.1.3 % 13.14/2.71 % (388472)Termination reason: Instruction limit % 13.14/2.71 % (388472)Termination phase: Saturation % 13.14/2.71 % (388472)Time elapsed: 0.043 s % 13.14/2.71 % (388472)Peak memory usage: 93 MB % 13.14/2.71 % (388472)Instructions burned: 142 (million) % 13.14/2.71 % (388475)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1841879497:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 13.14/2.71 % (388476)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3062568825:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.14/2.71 % (388475)Instruction limit reached! % 13.14/2.71 % (388475)------------------------------ % 13.14/2.71 % (388475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388475)CaDiCaL version: 2.1.3 % 13.14/2.71 % (388475)Termination reason: Instruction limit % 13.14/2.71 % (388475)Termination phase: Saturation % 13.14/2.71 % (388475)Time elapsed: 0.032 s % 13.14/2.71 % (388475)Peak memory usage: 90 MB % 13.14/2.71 % (388475)Instructions burned: 66 (million) % 13.14/2.71 % (388478)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=2716872913:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.14/2.71 % (388461)Instruction limit reached! % 13.14/2.71 % (388461)------------------------------ % 13.14/2.71 % (388461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388461)CaDiCaL version: 2.1.3 % 13.14/2.71 % (388461)Termination reason: Instruction limit % 13.14/2.71 % (388461)Termination phase: Saturation % 13.14/2.71 % (388461)Time elapsed: 0.363 s % 13.14/2.71 % (388461)Peak memory usage: 139 MB % 13.14/2.71 % (388461)Instructions burned: 598 (million) % 13.14/2.71 % (388469)Instruction limit reached! % 13.14/2.71 % (388469)------------------------------ % 13.14/2.71 % (388469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388469)CaDiCaL version: 2.1.3 % 13.14/2.71 % (388469)Termination reason: Instruction limit % 13.14/2.71 % (388469)Termination phase: Saturation % 13.14/2.71 % (388469)Time elapsed: 0.207 s % 13.14/2.71 % (388469)Peak memory usage: 94 MB % 13.14/2.71 % (388469)Instructions burned: 383 (million) % 13.14/2.71 % (388478)Refutation not found, incomplete strategy % 13.14/2.71 % (388478)------------------------------ % 13.14/2.71 % (388478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388478)CaDiCaL version: 2.1.3 % 13.14/2.71 % (388478)Termination reason: Refutation not found, incomplete strategy % 13.14/2.71 % (388478)Time elapsed: 0.039 s % 13.14/2.71 % (388478)Peak memory usage: 115 MB % 13.14/2.71 % (388478)Instructions burned: 89 (million) % 13.14/2.71 % (388476)Instruction limit reached! % 13.14/2.71 % (388476)------------------------------ % 13.14/2.71 % (388476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388476)CaDiCaL version: 2.1.3 % 13.14/2.71 % (388476)Termination reason: Instruction limit % 13.14/2.71 % (388476)Termination phase: Saturation % 13.14/2.71 % (388476)Time elapsed: 0.063 s % 13.14/2.71 % (388476)Peak memory usage: 91 MB % 13.14/2.71 % (388476)Instructions burned: 122 (million) % 13.14/2.71 % (388466)------------------------------ % 13.14/2.71 % (388466)------------------------------ % 13.14/2.71 % (388481)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=1884179142:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.14/2.71 % (388481)Instruction limit reached! % 13.14/2.71 % (388481)------------------------------ % 13.14/2.71 % (388481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.14/2.71 % (388481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.71 % (388481)CaDiCaL version: 2.1.3 % 15.17/3.02 % (388481)Termination reason: Instruction limit % 15.17/3.02 % (388481)Termination phase: Property scanning % 15.17/3.02 % (388481)Time elapsed: 0.019 s % 15.17/3.02 % (388481)Peak memory usage: 88 MB % 15.17/3.02 % (388481)Instructions burned: 39 (million) % 15.17/3.02 % (388483)dis+1010_1_to=kbo:si=on:random_seed=3127857792:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi) % 15.17/3.02 % (388484)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2876383329:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 15.17/3.02 % (388485)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1376966888:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.17/3.02 % (388486)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=29244406:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.17/3.02 % (388478)------------------------------ % 15.17/3.02 % (388478)------------------------------ % 15.17/3.02 % (388493)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=675586768:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi) % 15.17/3.02 % (388489)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1150110782:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi) % 15.17/3.02 % (388493)Refutation not found, incomplete strategy % 15.17/3.02 % (388493)------------------------------ % 15.17/3.02 % (388493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.17/3.02 % (388493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.17/3.02 % (388493)CaDiCaL version: 2.1.3 % 15.17/3.02 % (388493)Termination reason: Refutation not found, incomplete strategy % 15.17/3.02 % (388493)Time elapsed: 0.003 s % 15.17/3.02 % (388493)Peak memory usage: 88 MB % 15.17/3.02 % (388493)Instructions burned: 14 (million) % 15.17/3.02 % (388483)Instruction limit reached! % 15.17/3.02 % (388483)------------------------------ % 15.17/3.02 % (388483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.17/3.02 % (388483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.17/3.02 % (388483)CaDiCaL version: 2.1.3 % 15.17/3.02 % (388483)Termination reason: Instruction limit % 15.17/3.02 % (388483)Termination phase: Clausification % 15.17/3.02 % (388483)Time elapsed: 0.175 s % 15.17/3.02 % (388483)Peak memory usage: 179 MB % 15.17/3.02 % (388483)Instructions burned: 175 (million) % 15.17/3.02 % (388486)Instruction limit reached! % 15.17/3.02 % (388486)------------------------------ % 15.17/3.02 % (388486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.17/3.02 % (388486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.17/3.02 % (388486)CaDiCaL version: 2.1.3 % 15.17/3.02 % (388486)Termination reason: Instruction limit % 15.17/3.02 % (388486)Termination phase: Clausification % 15.17/3.02 % (388486)Time elapsed: 0.166 s % 15.17/3.02 % (388486)Peak memory usage: 154 MB % 15.17/3.02 % (388486)Instructions burned: 216 (million) % 15.17/3.02 % (388468)Instruction limit reached! % 15.17/3.02 % (388468)------------------------------ % 15.17/3.02 % (388468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.17/3.02 % (388468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.17/3.02 % (388468)CaDiCaL version: 2.1.3 % 15.17/3.02 % (388468)Termination reason: Instruction limit % 15.17/3.02 % (388468)Termination phase: Saturation % 15.17/3.02 % (388468)Time elapsed: 0.555 s % 15.17/3.02 % (388468)Peak memory usage: 97 MB % 15.17/3.02 % (388468)Instructions burned: 1001 (million) % 15.17/3.02 % (388484)Instruction limit reached! % 15.17/3.02 % (388484)------------------------------ % 15.17/3.02 % (388484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.17/3.02 % (388484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.17/3.02 % (388484)CaDiCaL version: 2.1.3 % 15.17/3.02 % (388484)Termination reason: Instruction limit % 15.17/3.02 % (388484)Termination phase: Saturation % 15.17/3.02 % (388484)Time elapsed: 0.237 s % 15.17/3.02 % (388484)Peak memory usage: 121 MB % 15.17/3.02 % (388484)Instructions burned: 329 (million) % 15.17/3.02 % (388493)------------------------------ % 15.17/3.02 % (388493)------------------------------ % 15.17/3.02 % (388496)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=957615093:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 17.45/3.29 % (388485)Instruction limit reached! % 17.45/3.29 % (388485)------------------------------ % 17.45/3.29 % (388485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.45/3.29 % (388485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/3.29 % (388485)CaDiCaL version: 2.1.3 % 17.45/3.29 % (388485)Termination reason: Instruction limit % 17.45/3.29 % (388485)Termination phase: Saturation % 17.45/3.29 % (388485)Time elapsed: 0.296 s % 17.45/3.29 % (388485)Peak memory usage: 139 MB % 17.45/3.29 % (388485)Instructions burned: 484 (million) % 17.45/3.29 % (388497)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=614923826:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi) % 17.45/3.29 % (388489)Instruction limit reached! % 17.45/3.29 % (388489)------------------------------ % 17.45/3.29 % (388489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.45/3.29 % (388489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/3.29 % (388489)CaDiCaL version: 2.1.3 % 17.45/3.29 % (388489)Termination reason: Instruction limit % 17.45/3.29 % (388489)Termination phase: Saturation % 17.45/3.29 % (388489)Time elapsed: 0.213 s % 17.45/3.29 % (388489)Peak memory usage: 122 MB % 17.45/3.29 % (388489)Instructions burned: 349 (million) % 17.45/3.29 % (388498)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=4293061258:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 17.45/3.29 % (388498)Refutation not found, incomplete strategy % 17.45/3.29 % (388498)------------------------------ % 17.45/3.29 % (388498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.45/3.29 % (388498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/3.29 % (388498)CaDiCaL version: 2.1.3 % 17.45/3.29 % (388498)Termination reason: Refutation not found, incomplete strategy % 17.45/3.29 % (388498)Time elapsed: 0.006 s % 17.45/3.29 % (388498)Peak memory usage: 88 MB % 17.45/3.29 % (388498)Instructions burned: 14 (million) % 17.45/3.29 % (388500)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1249357364:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi) % 17.45/3.29 % (388499)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=407728111:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.45/3.29 % (388500)Refutation not found, incomplete strategy % 17.45/3.29 % (388500)------------------------------ % 17.45/3.29 % (388500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.45/3.29 % (388500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/3.29 % (388500)CaDiCaL version: 2.1.3 % 17.45/3.29 % (388500)Termination reason: Refutation not found, incomplete strategy % 17.45/3.29 % (388500)Time elapsed: 0.019 s % 17.45/3.29 % (388500)Peak memory usage: 111 MB % 17.45/3.29 % (388500)Instructions burned: 18 (million) % 17.45/3.29 % (388499)Refutation not found, incomplete strategy % 17.45/3.29 % (388499)------------------------------ % 17.45/3.29 % (388499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.45/3.29 % (388499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/3.29 % (388499)CaDiCaL version: 2.1.3 % 17.45/3.29 % (388499)Termination reason: Refutation not found, incomplete strategy % 17.45/3.29 % (388499)Time elapsed: 0.032 s % 17.45/3.29 % (388499)Peak memory usage: 112 MB % 17.45/3.29 % (388499)Instructions burned: 18 (million) % 17.45/3.29 % (388503)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=527072959:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 17.45/3.29 % (388505)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=1570888643:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 17.45/3.29 % (388497)Instruction limit reached! % 17.45/3.29 % (388497)------------------------------ % 17.45/3.29 % (388497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.45/3.29 % (388497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.45/3.29 % (388497)CaDiCaL version: 2.1.3 % 17.45/3.29 % (388497)Termination reason: Instruction limit % 17.45/3.29 % (388497)Termination phase: Saturation % 18.99/3.77 % (388497)Time elapsed: 0.169 s % 18.99/3.77 % (388497)Peak memory usage: 121 MB % 18.99/3.77 % (388497)Instructions burned: 281 (million) % 18.99/3.77 % (388496)Instruction limit reached! % 18.99/3.77 % (388496)------------------------------ % 18.99/3.77 % (388496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.77 % (388496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.77 % (388496)CaDiCaL version: 2.1.3 % 18.99/3.77 % (388496)Termination reason: Instruction limit % 18.99/3.77 % (388496)Termination phase: Saturation % 18.99/3.77 % (388496)Time elapsed: 0.198 s % 18.99/3.77 % (388496)Peak memory usage: 121 MB % 18.99/3.77 % (388496)Instructions burned: 329 (million) % 18.99/3.77 % (388500)------------------------------ % 18.99/3.77 % (388500)------------------------------ % 18.99/3.77 % (388498)------------------------------ % 18.99/3.77 % (388498)------------------------------ % 18.99/3.77 % (388512)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3790798417:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 18.99/3.77 % (388510)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=427121999:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 18.99/3.77 % (388511)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=614729548:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi) % 18.99/3.77 % (388499)------------------------------ % 18.99/3.77 % (388499)------------------------------ % 18.99/3.77 % (388505)Instruction limit reached! % 18.99/3.77 % (388505)------------------------------ % 18.99/3.77 % (388505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.77 % (388505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.77 % (388505)CaDiCaL version: 2.1.3 % 18.99/3.77 % (388505)Termination reason: Instruction limit % 18.99/3.77 % (388505)Termination phase: Saturation % 18.99/3.77 % (388505)Time elapsed: 0.191 s % 18.99/3.77 % (388505)Peak memory usage: 138 MB % 18.99/3.77 % (388505)Instructions burned: 278 (million) % 18.99/3.77 % (388511)Refutation not found, incomplete strategy % 18.99/3.77 % (388511)------------------------------ % 18.99/3.77 % (388511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.77 % (388511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.77 % (388511)CaDiCaL version: 2.1.3 % 18.99/3.77 % (388511)Termination reason: Refutation not found, incomplete strategy % 18.99/3.77 % (388511)Time elapsed: 0.033 s % 18.99/3.77 % (388511)Peak memory usage: 111 MB % 18.99/3.77 % (388511)Instructions burned: 20 (million) % 18.99/3.77 % (388503)Instruction limit reached! % 18.99/3.77 % (388503)------------------------------ % 18.99/3.77 % (388503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.77 % (388503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.77 % (388503)CaDiCaL version: 2.1.3 % 18.99/3.77 % (388503)Termination reason: Instruction limit % 18.99/3.77 % (388503)Termination phase: Saturation % 18.99/3.77 % (388503)Time elapsed: 0.274 s % 18.99/3.77 % (388503)Peak memory usage: 122 MB % 18.99/3.77 % (388503)Instructions burned: 473 (million) % 18.99/3.77 % (388513)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4125777520:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi) % 18.99/3.77 % (388517)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3986121368:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 18.99/3.77 % (388517)Refutation not found, incomplete strategy % 18.99/3.77 % (388517)------------------------------ % 18.99/3.77 % (388517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.77 % (388517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.99/3.77 % (388517)CaDiCaL version: 2.1.3 % 18.99/3.77 % (388517)Termination reason: Refutation not found, incomplete strategy % 18.99/3.77 % (388517)Time elapsed: 0.009 s % 18.99/3.77 % (388517)Peak memory usage: 88 MB % 18.99/3.77 % (388517)Instructions burned: 19 (million) % 18.99/3.77 % (388512)Instruction limit reached! % 18.99/3.77 % (388512)------------------------------ % 18.99/3.77 % (388512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.99/3.77 % (388512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.82/4.14 % (388512)CaDiCaL version: 2.1.3 % 23.82/4.14 % (388512)Termination reason: Instruction limit % 23.82/4.14 % (388512)Termination phase: Saturation % 23.82/4.14 % (388512)Time elapsed: 0.165 s % 23.82/4.14 % (388512)Peak memory usage: 97 MB % 23.82/4.14 % (388512)Instructions burned: 513 (million) % 23.82/4.14 % (388518)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2287566496:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2977 on theBenchmark for (2977ds/341Mi) % 23.82/4.14 % (388519)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3505009204:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi) % 23.82/4.14 % (388510)Instruction limit reached! % 23.82/4.14 % (388510)------------------------------ % 23.82/4.14 % (388510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.82/4.14 % (388510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.82/4.14 % (388510)CaDiCaL version: 2.1.3 % 23.82/4.14 % (388510)Termination reason: Instruction limit % 23.82/4.14 % (388510)Termination phase: Saturation % 23.82/4.14 % (388510)Time elapsed: 0.231 s % 23.82/4.14 % (388510)Peak memory usage: 121 MB % 23.82/4.14 % (388510)Instructions burned: 375 (million) % 23.82/4.14 % (388522)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=2344915583:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi) % 23.82/4.14 % (388519)Refutation not found, incomplete strategy % 23.82/4.14 % (388519)------------------------------ % 23.82/4.14 % (388519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.82/4.14 % (388519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.82/4.14 % (388519)CaDiCaL version: 2.1.3 % 23.82/4.14 % (388519)Termination reason: Refutation not found, incomplete strategy % 23.82/4.14 % (388519)Time elapsed: 0.030 s % 23.82/4.14 % (388519)Peak memory usage: 111 MB % 23.82/4.14 % (388519)Instructions burned: 14 (million) % 23.82/4.14 % (388522)Refutation not found, incomplete strategy % 23.82/4.14 % (388522)------------------------------ % 23.82/4.14 % (388522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.82/4.14 % (388522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.82/4.14 % (388522)CaDiCaL version: 2.1.3 % 23.82/4.14 % (388522)Termination reason: Refutation not found, incomplete strategy % 23.82/4.14 % (388522)Time elapsed: 0.019 s % 23.82/4.14 % (388522)Peak memory usage: 111 MB % 23.82/4.14 % (388522)Instructions burned: 20 (million) % 23.82/4.14 % (388511)------------------------------ % 23.82/4.14 % (388511)------------------------------ % 23.82/4.14 % (388513)Instruction limit reached! % 23.82/4.14 % (388513)------------------------------ % 23.82/4.14 % (388513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.82/4.14 % (388513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.82/4.14 % (388513)CaDiCaL version: 2.1.3 % 23.82/4.14 % (388513)Termination reason: Instruction limit % 23.82/4.14 % (388513)Termination phase: Saturation % 23.82/4.14 % (388513)Time elapsed: 0.225 s % 23.82/4.14 % (388513)Peak memory usage: 138 MB % 23.82/4.14 % (388513)Instructions burned: 334 (million) % 23.82/4.14 % (388525)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3736740838:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi) % 23.82/4.14 % (388518)Instruction limit reached! % 23.82/4.14 % (388518)------------------------------ % 23.82/4.14 % (388518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.82/4.14 % (388518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.82/4.14 % (388518)CaDiCaL version: 2.1.3 % 23.82/4.14 % (388518)Termination reason: Instruction limit % 23.82/4.14 % (388518)Termination phase: Saturation % 23.82/4.14 % (388518)Time elapsed: 0.210 s % 23.82/4.14 % (388518)Peak memory usage: 119 MB % 23.82/4.14 % (388518)Instructions burned: 341 (million) % 23.82/4.14 % (388517)------------------------------ % 23.82/4.14 % (388517)------------------------------ % 23.82/4.14 % (388522)------------------------------ % 23.82/4.14 % (388522)------------------------------ % 23.82/4.14 % (388527)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2408821961:i=146:doe=on:rtra=on_2975 on theBenchmark for (2975ds/146Mi) % 25.84/4.66 % (388528)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1641243395:i=4428:doe=on:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/4428Mi) % 25.84/4.66 % (388532)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2054741047:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 25.84/4.66 % (388530)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=2157102486:avsq=on:i=276:avsqr=1,2:rtra=on_2974 on theBenchmark for (2974ds/276Mi) % 25.84/4.66 % (388527)Instruction limit reached! % 25.84/4.66 % (388527)------------------------------ % 25.84/4.66 % (388527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.66 % (388527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.66 % (388527)CaDiCaL version: 2.1.3 % 25.84/4.66 % (388527)Termination reason: Instruction limit % 25.84/4.66 % (388527)Termination phase: Saturation % 25.84/4.66 % (388527)Time elapsed: 0.084 s % 25.84/4.66 % (388527)Peak memory usage: 93 MB % 25.84/4.66 % (388527)Instructions burned: 146 (million) % 25.84/4.66 % (388531)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2920626801:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 25.84/4.66 % (388525)Instruction limit reached! % 25.84/4.66 % (388525)------------------------------ % 25.84/4.66 % (388525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.66 % (388525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.66 % (388525)CaDiCaL version: 2.1.3 % 25.84/4.66 % (388525)Termination reason: Instruction limit % 25.84/4.66 % (388525)Termination phase: Saturation % 25.84/4.66 % (388525)Time elapsed: 0.168 s % 25.84/4.66 % (388525)Peak memory usage: 94 MB % 25.84/4.66 % (388525)Instructions burned: 273 (million) % 25.84/4.66 % (388519)------------------------------ % 25.84/4.66 % (388519)------------------------------ % 25.84/4.66 % (388539)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1018660520:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2973 on theBenchmark for (2973ds/1054Mi) % 25.84/4.66 % (388541)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=595602659:i=107:rtra=on_2972 on theBenchmark for (2972ds/107Mi) % 25.84/4.66 % (388539)Refutation not found, incomplete strategy % 25.84/4.66 % (388539)------------------------------ % 25.84/4.66 % (388539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.66 % (388539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.66 % (388539)CaDiCaL version: 2.1.3 % 25.84/4.66 % (388539)Termination reason: Refutation not found, incomplete strategy % 25.84/4.66 % (388539)Time elapsed: 0.005 s % 25.84/4.66 % (388539)Peak memory usage: 87 MB % 25.84/4.66 % (388539)Instructions burned: 10 (million) % 25.84/4.66 % (388542)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1117004686:s2a=on:i=450:doe=on:nm=32:rtra=on_2972 on theBenchmark for (2972ds/450Mi) % 25.84/4.66 % (388541)Refutation not found, incomplete strategy % 25.84/4.66 % (388541)------------------------------ % 25.84/4.66 % (388541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.66 % (388541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.66 % (388541)CaDiCaL version: 2.1.3 % 25.84/4.66 % (388541)Termination reason: Refutation not found, incomplete strategy % 25.84/4.66 % (388541)Time elapsed: 0.064 s % 25.84/4.66 % (388541)Peak memory usage: 114 MB % 25.84/4.66 % (388541)Instructions burned: 80 (million) % 25.84/4.66 % (388530)Instruction limit reached! % 25.84/4.66 % (388530)------------------------------ % 25.84/4.66 % (388530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.66 % (388530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.84/4.66 % (388530)CaDiCaL version: 2.1.3 % 25.84/4.66 % (388530)Termination reason: Instruction limit % 25.84/4.66 % (388530)Termination phase: Saturation % 25.84/4.66 % (388530)Time elapsed: 0.381 s % 25.84/4.66 % (388530)Peak memory usage: 138 MB % 25.84/4.66 % (388530)Instructions burned: 277 (million) % 25.84/4.66 % (388532)Instruction limit reached! % 25.84/4.66 % (388532)------------------------------ % 25.84/4.66 % (388532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.84/4.66 % (388532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.18/5.12 % (388532)CaDiCaL version: 2.1.3 % 30.18/5.12 % (388532)Termination reason: Instruction limit % 30.18/5.12 % (388532)Termination phase: Saturation % 30.18/5.12 % (388532)Time elapsed: 0.394 s % 30.18/5.12 % (388532)Peak memory usage: 97 MB % 30.18/5.12 % (388532)Instructions burned: 657 (million) % 30.18/5.12 % (388539)------------------------------ % 30.18/5.12 % (388539)------------------------------ % 30.18/5.12 % (388547)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2338146911:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi) % 30.18/5.12 % (388542)Instruction limit reached! % 30.18/5.12 % (388542)------------------------------ % 30.18/5.12 % (388542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.18/5.12 % (388542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.18/5.12 % (388542)CaDiCaL version: 2.1.3 % 30.18/5.12 % (388542)Termination reason: Instruction limit % 30.18/5.12 % (388542)Termination phase: Saturation % 30.18/5.12 % (388542)Time elapsed: 0.274 s % 30.18/5.12 % (388542)Peak memory usage: 139 MB % 30.18/5.12 % (388542)Instructions burned: 451 (million) % 30.18/5.12 % (388541)------------------------------ % 30.18/5.12 % (388541)------------------------------ % 30.18/5.12 % (388546)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 % 30.18/5.12 % (388546)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2305260024:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 30.18/5.12 % (388547)Instruction limit reached! % 30.18/5.12 % (388547)------------------------------ % 30.18/5.12 % (388547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.18/5.12 % (388547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.18/5.12 % (388547)CaDiCaL version: 2.1.3 % 30.18/5.12 % (388547)Termination reason: Instruction limit % 30.18/5.12 % (388547)Termination phase: Clausification % 30.18/5.12 % (388547)Time elapsed: 0.070 s % 30.18/5.12 % (388547)Peak memory usage: 145 MB % 30.18/5.12 % (388547)Instructions burned: 130 (million) % 30.18/5.12 % (388548)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=282833031:i=312:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/312Mi) % 30.18/5.12 % (388550)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2209299315:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi) % 30.18/5.12 % (388553)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2007777464:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 30.18/5.12 % (388552)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=772159498:s2a=on:i=835:s2at=2:rtra=on_2967 on theBenchmark for (2967ds/835Mi) % 30.18/5.12 % (388553)Refutation not found, incomplete strategy % 30.18/5.12 % (388553)------------------------------ % 30.18/5.12 % (388553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.18/5.12 % (388553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.18/5.12 % (388553)CaDiCaL version: 2.1.3 % 30.18/5.12 % (388553)Termination reason: Refutation not found, incomplete strategy % 30.18/5.12 % (388553)Time elapsed: 0.026 s % 30.18/5.12 % (388553)Peak memory usage: 91 MB % 30.18/5.12 % (388553)Instructions burned: 95 (million) % 30.18/5.12 % (388550)Refutation not found, incomplete strategy % 30.18/5.12 % (388550)------------------------------ % 30.18/5.12 % (388550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.18/5.12 % (388550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.18/5.12 % (388550)CaDiCaL version: 2.1.3 % 30.18/5.12 % (388550)Termination reason: Refutation not found, incomplete strategy % 30.18/5.12 % (388550)Time elapsed: 0.038 s % 30.18/5.12 % (388550)Peak memory usage: 91 MB % 30.18/5.12 % (388550)Instructions burned: 78 (million) % 30.18/5.12 % (388548)Instruction limit reached! % 30.18/5.12 % (388548)------------------------------ % 30.18/5.12 % (388548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.18/5.12 % (388548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.18/5.12 % (388548)CaDiCaL version: 2.1.3 % 34.44/5.92 % (388548)Termination reason: Instruction limit % 34.44/5.92 % (388548)Termination phase: Saturation % 34.44/5.92 % (388548)Time elapsed: 0.183 s % 34.44/5.92 % (388548)Peak memory usage: 121 MB % 34.44/5.92 % (388548)Instructions burned: 314 (million) % 34.44/5.92 % (388531)Instruction limit reached! % 34.44/5.92 % (388531)------------------------------ % 34.44/5.92 % (388531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.92 % (388531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.92 % (388531)CaDiCaL version: 2.1.3 % 34.44/5.92 % (388531)Termination reason: Instruction limit % 34.44/5.92 % (388531)Termination phase: Saturation % 34.44/5.92 % (388531)Time elapsed: 0.745 s % 34.44/5.92 % (388531)Peak memory usage: 96 MB % 34.44/5.92 % (388531)Instructions burned: 1053 (million) % 34.44/5.92 % (388553)------------------------------ % 34.44/5.92 % (388553)------------------------------ % 34.44/5.92 % (388560)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=577325180:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2964 on theBenchmark for (2964ds/784Mi) % 34.44/5.92 % (388558)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1262840840:i=776:doe=on:rtra=on_2965 on theBenchmark for (2965ds/776Mi) % 34.44/5.92 % (388559)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1591863530:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2965 on theBenchmark for (2965ds/646Mi) % 34.44/5.92 % (388550)------------------------------ % 34.44/5.92 % (388550)------------------------------ % 34.44/5.92 % (388564)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=2460230904:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2963 on theBenchmark for (2963ds/1131Mi) % 34.44/5.92 % (388552)Instruction limit reached! % 34.44/5.92 % (388552)------------------------------ % 34.44/5.92 % (388552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.92 % (388552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.92 % (388552)CaDiCaL version: 2.1.3 % 34.44/5.92 % (388552)Termination reason: Instruction limit % 34.44/5.92 % (388552)Termination phase: Saturation % 34.44/5.92 % (388552)Time elapsed: 0.486 s % 34.44/5.92 % (388552)Peak memory usage: 97 MB % 34.44/5.92 % (388552)Instructions burned: 836 (million) % 34.44/5.92 % (388560)Instruction limit reached! % 34.44/5.92 % (388560)------------------------------ % 34.44/5.92 % (388560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.92 % (388560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.92 % (388560)CaDiCaL version: 2.1.3 % 34.44/5.92 % (388560)Termination reason: Instruction limit % 34.44/5.92 % (388560)Termination phase: Saturation % 34.44/5.92 % (388560)Time elapsed: 0.248 s % 34.44/5.92 % (388560)Peak memory usage: 120 MB % 34.44/5.92 % (388560)Instructions burned: 784 (million) % 34.44/5.92 % (388567)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4120756050:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/775Mi) % 34.44/5.92 % (388567)Refutation not found, incomplete strategy % 34.44/5.92 % (388567)------------------------------ % 34.44/5.92 % (388567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.92 % (388567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.92 % (388567)CaDiCaL version: 2.1.3 % 34.44/5.92 % (388567)Termination reason: Refutation not found, incomplete strategy % 34.44/5.92 % (388567)Time elapsed: 0.004 s % 34.44/5.92 % (388567)Peak memory usage: 88 MB % 34.44/5.92 % (388567)Instructions burned: 16 (million) % 34.44/5.92 % (388566)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=1690574077:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/246Mi) % 34.44/5.92 % (388559)Instruction limit reached! % 34.44/5.92 % (388559)------------------------------ % 34.44/5.92 % (388559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.92 % (388559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.92 % (388559)CaDiCaL version: 2.1.3 % 34.44/5.92 % (388559)Termination reason: Instruction limit % 34.44/5.92 % (388559)Termination phase: Saturation % 34.44/5.92 % (388559)Time elapsed: 0.376 s % 34.44/5.92 % (388559)Peak memory usage: 139 MB % 46.28/7.39 % (388559)Instructions burned: 649 (million) % 46.28/7.39 % (388566)Refutation not found, incomplete strategy % 46.28/7.39 % (388566)------------------------------ % 46.28/7.39 % (388566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.28/7.39 % (388566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.28/7.39 % (388566)CaDiCaL version: 2.1.3 % 46.28/7.39 % (388566)Termination reason: Refutation not found, incomplete strategy % 46.28/7.39 % (388566)Time elapsed: 0.032 s % 46.28/7.39 % (388566)Peak memory usage: 111 MB % 46.28/7.39 % (388566)Instructions burned: 20 (million) % 46.28/7.39 % (388558)Instruction limit reached! % 46.28/7.39 % (388558)------------------------------ % 46.28/7.39 % (388558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.28/7.39 % (388558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.28/7.39 % (388558)CaDiCaL version: 2.1.3 % 46.28/7.39 % (388558)Termination reason: Instruction limit % 46.28/7.39 % (388558)Termination phase: Saturation % 46.28/7.39 % (388558)Time elapsed: 0.418 s % 46.28/7.39 % (388558)Peak memory usage: 122 MB % 46.28/7.39 % (388558)Instructions burned: 778 (million) % 46.28/7.39 % (388567)------------------------------ % 46.28/7.39 % (388567)------------------------------ % 46.28/7.39 % (388570)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4034483353:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi) % 46.28/7.39 % (388571)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3336871063:i=102:nm=16:rtra=on_2959 on theBenchmark for (2959ds/102Mi) % 46.28/7.39 % (388572)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=750026818:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2959 on theBenchmark for (2959ds/1094Mi) % 46.28/7.39 % (388571)Instruction limit reached! % 46.28/7.39 % (388571)------------------------------ % 46.28/7.39 % (388571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.28/7.39 % (388571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.28/7.39 % (388571)CaDiCaL version: 2.1.3 % 46.28/7.39 % (388571)Termination reason: Instruction limit % 46.28/7.39 % (388571)Termination phase: Saturation % 46.28/7.39 % (388571)Time elapsed: 0.052 s % 46.28/7.39 % (388571)Peak memory usage: 90 MB % 46.28/7.39 % (388571)Instructions burned: 103 (million) % 46.28/7.39 % (388566)------------------------------ % 46.28/7.39 % (388566)------------------------------ % 46.28/7.39 % (388546)Instruction limit reached! % 46.28/7.39 % (388546)------------------------------ % 46.28/7.39 % (388546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.28/7.39 % (388546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.28/7.39 % (388546)CaDiCaL version: 2.1.3 % 46.28/7.39 % (388546)Termination reason: Instruction limit % 46.28/7.39 % (388546)Termination phase: Clausification % 46.28/7.39 % (388546)Time elapsed: 1.062 s % 46.28/7.39 % (388546)Peak memory usage: 632 MB % 46.28/7.39 % (388546)Instructions burned: 1091 (million) % 46.28/7.39 % (388570)Instruction limit reached! % 46.28/7.39 % (388570)------------------------------ % 46.28/7.39 % (388570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.28/7.39 % (388570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.28/7.39 % (388570)CaDiCaL version: 2.1.3 % 46.28/7.39 % (388570)Termination reason: Instruction limit % 46.28/7.39 % (388570)Termination phase: Saturation % 46.28/7.39 % (388570)Time elapsed: 0.161 s % 46.28/7.39 % (388570)Peak memory usage: 94 MB % 46.28/7.39 % (388570)Instructions burned: 273 (million) % 46.28/7.39 % (388576)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2710429703:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi) % 46.28/7.39 % (388577)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=81061788:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/868Mi) % 46.28/7.39 % (388578)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=2888912775:i=1846:canc=cautious:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/1846Mi) % 46.28/7.39 % (388578)Refutation not found, incomplete strategy % 46.28/7.39 % (388578)------------------------------ % 46.28/7.39 % (388578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.86/8.44 % (388578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.86/8.44 % (388578)CaDiCaL version: 2.1.3 % 53.86/8.44 % (388578)Termination reason: Refutation not found, incomplete strategy % 53.86/8.44 % (388578)Time elapsed: 0.037 s % 53.86/8.44 % (388578)Peak memory usage: 91 MB % 53.86/8.44 % (388578)Instructions burned: 75 (million) % 53.86/8.44 % (388564)Instruction limit reached! % 53.86/8.44 % (388564)------------------------------ % 53.86/8.44 % (388564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.86/8.44 % (388564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.86/8.44 % (388564)CaDiCaL version: 2.1.3 % 53.86/8.44 % (388564)Termination reason: Instruction limit % 53.86/8.44 % (388564)Termination phase: Saturation % 53.86/8.44 % (388564)Time elapsed: 0.682 s % 53.86/8.44 % (388564)Peak memory usage: 121 MB % 53.86/8.44 % (388564)Instructions burned: 1132 (million) % 53.86/8.44 % (388579)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3269638351:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2956 on theBenchmark for (2956ds/36816Mi) % 53.86/8.44 % (388572)Instruction limit reached! % 53.86/8.44 % (388572)------------------------------ % 53.86/8.44 % (388572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.86/8.44 % (388572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.86/8.44 % (388572)CaDiCaL version: 2.1.3 % 53.86/8.44 % (388572)Termination reason: Instruction limit % 53.86/8.44 % (388572)Termination phase: Saturation % 53.86/8.44 % (388572)Time elapsed: 0.302 s % 53.86/8.44 % (388572)Peak memory usage: 100 MB % 53.86/8.44 % (388572)Instructions burned: 1096 (million) % 53.86/8.44 % (388585)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=3808482061:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 53.86/8.44 % (388583)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=636593035:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi) % 53.86/8.44 % (388578)------------------------------ % 53.86/8.44 % (388578)------------------------------ % 53.86/8.44 % (388583)Instruction limit reached! % 53.86/8.44 % (388583)------------------------------ % 53.86/8.44 % (388583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.86/8.44 % (388583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.86/8.44 % (388583)CaDiCaL version: 2.1.3 % 53.86/8.44 % (388583)Termination reason: Instruction limit % 53.86/8.44 % (388583)Termination phase: Saturation % 53.86/8.44 % (388583)Time elapsed: 0.163 s % 53.86/8.44 % (388583)Peak memory usage: 94 MB % 53.86/8.44 % (388583)Instructions burned: 274 (million) % 53.86/8.44 % (388588)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=431059940:i=5811:kws=precedence:nm=0:rtra=on_2953 on theBenchmark for (2953ds/5811Mi) % 53.86/8.44 % (388589)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=1397510993:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 53.86/8.44 % (388585)Instruction limit reached! % 53.86/8.44 % (388585)------------------------------ % 53.86/8.44 % (388585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.86/8.44 % (388585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.86/8.44 % (388585)CaDiCaL version: 2.1.3 % 53.86/8.44 % (388585)Termination reason: Instruction limit % 53.86/8.44 % (388585)Termination phase: Clausification % 53.86/8.44 % (388585)Time elapsed: 0.543 s % 53.86/8.44 % (388585)Peak memory usage: 593 MB % 53.86/8.44 % (388585)Instructions burned: 864 (million) % 53.86/8.44 % (388528)Instruction limit reached! % 53.86/8.44 % (388528)------------------------------ % 53.86/8.44 % (388528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.86/8.44 % (388528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.86/8.44 % (388528)CaDiCaL version: 2.1.3 % 53.86/8.44 % (388528)Termination reason: Instruction limit % 53.86/8.44 % (388528)Termination phase: Saturation % 53.86/8.44 % (388528)Time elapsed: 2.560 s % 53.86/8.44 % (388528)Peak memory usage: 115 MB % 53.86/8.44 % (388528)Instructions burned: 4430 (million) % 53.86/8.44 % (388592)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1705086945:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/801Mi) % 61.29/9.52 % (388577)Instruction limit reached! % 61.29/9.52 % (388577)------------------------------ % 61.29/9.52 % (388577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.29/9.52 % (388577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.29/9.52 % (388577)CaDiCaL version: 2.1.3 % 61.29/9.52 % (388577)Termination reason: Instruction limit % 61.29/9.52 % (388577)Termination phase: Clausification % 61.29/9.52 % (388577)Time elapsed: 0.928 s % 61.29/9.52 % (388577)Peak memory usage: 593 MB % 61.29/9.52 % (388577)Instructions burned: 868 (million) % 61.29/9.52 % (388593)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1421067268:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2947 on theBenchmark for (2947ds/1026Mi) % 61.29/9.52 % (388593)Refutation not found, incomplete strategy % 61.29/9.52 % (388593)------------------------------ % 61.29/9.52 % (388593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.29/9.52 % (388593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.29/9.52 % (388593)CaDiCaL version: 2.1.3 % 61.29/9.52 % (388593)Termination reason: Refutation not found, incomplete strategy % 61.29/9.52 % (388593)Time elapsed: 0.005 s % 61.29/9.52 % (388593)Peak memory usage: 87 MB % 61.29/9.52 % (388593)Instructions burned: 10 (million) % 61.29/9.52 % (388592)Instruction limit reached! % 61.29/9.52 % (388592)------------------------------ % 61.29/9.52 % (388592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.29/9.52 % (388592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.29/9.52 % (388592)CaDiCaL version: 2.1.3 % 61.29/9.52 % (388592)Termination reason: Instruction limit % 61.29/9.52 % (388592)Termination phase: Saturation % 61.29/9.52 % (388592)Time elapsed: 0.235 s % 61.29/9.52 % (388592)Peak memory usage: 96 MB % 61.29/9.52 % (388592)Instructions burned: 802 (million) % 61.29/9.52 % (388596)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2454692275:i=3509:rtra=on_2946 on theBenchmark for (2946ds/3509Mi) % 61.29/9.52 % (388597)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=743788725:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2945 on theBenchmark for (2945ds/2127Mi) % 61.29/9.52 % (388597)Refutation not found, incomplete strategy % 61.29/9.52 % (388597)------------------------------ % 61.29/9.52 % (388597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.29/9.52 % (388597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.29/9.52 % (388597)CaDiCaL version: 2.1.3 % 61.29/9.52 % (388597)Termination reason: Refutation not found, incomplete strategy % 61.29/9.52 % (388597)Time elapsed: 0.003 s % 61.29/9.52 % (388597)Peak memory usage: 88 MB % 61.29/9.52 % (388597)Instructions burned: 14 (million) % 61.29/9.52 % (388593)------------------------------ % 61.29/9.52 % (388593)------------------------------ % 61.29/9.52 % (388597)------------------------------ % 61.29/9.52 % (388597)------------------------------ % 61.29/9.52 % (388600)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3706521539:i=1959:rtra=on:fsd=on:proc=on_2944 on theBenchmark for (2944ds/1959Mi) % 61.29/9.52 % (388601)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2384818906:s2a=on:i=3553:nm=0:rtra=on_2942 on theBenchmark for (2942ds/3553Mi) % 61.29/9.52 % (388589)Instruction limit reached! % 61.29/9.52 % (388589)------------------------------ % 61.29/9.52 % (388589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.29/9.52 % (388589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.29/9.52 % (388589)CaDiCaL version: 2.1.3 % 61.29/9.52 % (388589)Termination reason: Instruction limit % 61.29/9.52 % (388589)Termination phase: Saturation % 61.29/9.52 % (388589)Time elapsed: 1.099 s % 61.29/9.52 % (388589)Peak memory usage: 127 MB % 61.29/9.52 % (388589)Instructions burned: 2216 (million) % 61.29/9.52 % (388604)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3187555218:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2940 on theBenchmark for (2940ds/3201Mi) % 61.29/9.52 % (388600)Instruction limit reached! % 61.29/9.52 % (388600)------------------------------ % 61.29/9.52 % (388600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.29/9.52 % (388600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.82/12.11 % (388600)CaDiCaL version: 2.1.3 % 79.82/12.11 % (388600)Termination reason: Instruction limit % 79.82/12.11 % (388600)Termination phase: Saturation % 79.82/12.11 % (388600)Time elapsed: 0.981 s % 79.82/12.11 % (388600)Peak memory usage: 127 MB % 79.82/12.11 % (388600)Instructions burned: 1959 (million) % 79.82/12.11 % (388606)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=2546319478:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2932 on theBenchmark for (2932ds/4093Mi) % 79.82/12.11 % (388601)Instruction limit reached! % 79.82/12.11 % (388601)------------------------------ % 79.82/12.11 % (388601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.82/12.11 % (388601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.82/12.11 % (388601)CaDiCaL version: 2.1.3 % 79.82/12.11 % (388601)Termination reason: Instruction limit % 79.82/12.11 % (388601)Termination phase: NewCNF % 79.82/12.11 % (388601)Time elapsed: 1.157 s % 79.82/12.11 % (388601)Peak memory usage: 427 MB % 79.82/12.11 % (388601)Instructions burned: 3554 (million) % 79.82/12.11 % (388608)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=638249327:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 79.82/12.11 % (388608)Refutation not found, incomplete strategy % 79.82/12.11 % (388608)------------------------------ % 79.82/12.11 % (388608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.82/12.11 % (388608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.82/12.11 % (388608)CaDiCaL version: 2.1.3 % 79.82/12.11 % (388608)Termination reason: Refutation not found, incomplete strategy % 79.82/12.11 % (388608)Time elapsed: 0.018 s % 79.82/12.11 % (388608)Peak memory usage: 112 MB % 79.82/12.11 % (388608)Instructions burned: 13 (million) % 79.82/12.11 % (388608)------------------------------ % 79.82/12.11 % (388608)------------------------------ % 79.82/12.11 % (388610)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4263337579:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2927 on theBenchmark for (2927ds/10544Mi) % 79.82/12.11 % (388596)Instruction limit reached! % 79.82/12.11 % (388596)------------------------------ % 79.82/12.11 % (388596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.82/12.11 % (388596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.82/12.11 % (388596)CaDiCaL version: 2.1.3 % 79.82/12.11 % (388596)Termination reason: Instruction limit % 79.82/12.11 % (388596)Termination phase: Saturation % 79.82/12.11 % (388596)Time elapsed: 2.069 s % 79.82/12.11 % (388596)Peak memory usage: 116 MB % 79.82/12.11 % (388596)Instructions burned: 3509 (million) % 79.82/12.11 % (388604)Instruction limit reached! % 79.82/12.11 % (388604)------------------------------ % 79.82/12.11 % (388604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.82/12.11 % (388604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.82/12.11 % (388604)CaDiCaL version: 2.1.3 % 79.82/12.11 % (388604)Termination reason: Instruction limit % 79.82/12.11 % (388604)Termination phase: Saturation % 79.82/12.11 % (388604)Time elapsed: 1.496 s % 79.82/12.11 % (388604)Peak memory usage: 97 MB % 79.82/12.11 % (388604)Instructions burned: 3203 (million) % 79.82/12.11 % (388612)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2890386299:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2924 on theBenchmark for (2924ds/1262Mi) % 79.82/12.11 % (388613)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2619492865:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2923 on theBenchmark for (2923ds/775Mi) % 79.82/12.11 % (388579)Refutation not found, incomplete strategy % 79.82/12.11 % (388579)------------------------------ % 79.82/12.11 % (388579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.82/12.11 % (388579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.82/12.11 % (388579)CaDiCaL version: 2.1.3 % 79.82/12.11 % (388579)Termination reason: Refutation not found, incomplete strategy % 79.82/12.11 % (388579)Time elapsed: 3.296 s % 79.82/12.11 % (388579)Peak memory usage: 169 MB % 79.82/12.11 % (388579)Instructions burned: 6799 (million) % 79.82/12.11 % (388613)Refutation not found, incomplete strategy % 99.52/15.77 % (388613)------------------------------ % 99.52/15.77 % (388613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.77 % (388613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.77 % (388613)CaDiCaL version: 2.1.3 % 99.52/15.77 % (388613)Termination reason: Refutation not found, incomplete strategy % 99.52/15.77 % (388613)Time elapsed: 0.008 s % 99.52/15.77 % (388613)Peak memory usage: 88 MB % 99.52/15.77 % (388613)Instructions burned: 16 (million) % 99.52/15.77 % (388576)Instruction limit reached! % 99.52/15.77 % (388576)------------------------------ % 99.52/15.77 % (388576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.77 % (388576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.77 % (388576)CaDiCaL version: 2.1.3 % 99.52/15.77 % (388576)Termination reason: Instruction limit % 99.52/15.77 % (388576)Termination phase: Saturation % 99.52/15.77 % (388576)Time elapsed: 3.617 s % 99.52/15.77 % (388576)Peak memory usage: 128 MB % 99.52/15.77 % (388576)Instructions burned: 6400 (million) % 99.52/15.77 % (388613)------------------------------ % 99.52/15.77 % (388613)------------------------------ % 99.52/15.77 % (388579)------------------------------ % 99.52/15.77 % (388579)------------------------------ % 99.52/15.77 % (388616)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2948209395:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2920 on theBenchmark for (2920ds/270Mi) % 99.52/15.77 % (388617)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=993679231:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2920 on theBenchmark for (2920ds/17165Mi) % 99.52/15.77 % (388618)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2719568086:s2a=on:i=13094:s2at=-1:rtra=on_2919 on theBenchmark for (2919ds/13094Mi) % 99.52/15.77 % (388616)Instruction limit reached! % 99.52/15.77 % (388616)------------------------------ % 99.52/15.77 % (388616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.77 % (388616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.77 % (388616)CaDiCaL version: 2.1.3 % 99.52/15.77 % (388616)Termination reason: Instruction limit % 99.52/15.77 % (388616)Termination phase: Saturation % 99.52/15.77 % (388616)Time elapsed: 0.160 s % 99.52/15.77 % (388616)Peak memory usage: 94 MB % 99.52/15.77 % (388616)Instructions burned: 270 (million) % 99.52/15.77 % (388612)Instruction limit reached! % 99.52/15.77 % (388612)------------------------------ % 99.52/15.77 % (388612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.77 % (388612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.77 % (388612)CaDiCaL version: 2.1.3 % 99.52/15.77 % (388612)Termination reason: Instruction limit % 99.52/15.77 % (388612)Termination phase: Saturation % 99.52/15.77 % (388612)Time elapsed: 0.641 s % 99.52/15.77 % (388612)Peak memory usage: 123 MB % 99.52/15.77 % (388612)Instructions burned: 1264 (million) % 99.52/15.77 % (388622)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=365854504:st=2:i=12633:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/12633Mi) % 99.52/15.77 % (388622)Refutation not found, incomplete strategy % 99.52/15.77 % (388622)------------------------------ % 99.52/15.77 % (388622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.52/15.77 % (388622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.52/15.77 % (388622)CaDiCaL version: 2.1.3 % 99.52/15.77 % (388622)Termination reason: Refutation not found, incomplete strategy % 99.52/15.77 % (388622)Time elapsed: 0.006 s % 99.52/15.77 % (388622)Peak memory usage: 88 MB % 99.52/15.77 % (388622)Instructions burned: 14 (million) % 99.52/15.77 % (388623)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1407366621:i=1783:rtra=on:gtg=position_2916 on theBenchmark for (2916ds/1783Mi) % 99.52/15.77 % (388622)------------------------------ % 99.52/15.77 % (388622)------------------------------ % 99.52/15.77 % (388626)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=1489922139:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2913 on theBenchmark for (2913ds/5451Mi) % 99.52/15.77 % (388606)Instruction limit reached! % 99.52/15.77 % (388606)------------------------------ % 99.52/15.77 % (388606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.63/19.56 % (388606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.63/19.56 % (388606)CaDiCaL version: 2.1.3 % 132.63/19.56 % (388606)Termination reason: Instruction limit % 132.63/19.56 % (388606)Termination phase: Saturation % 132.63/19.56 % (388606)Time elapsed: 1.992 s % 132.63/19.56 % (388606)Peak memory usage: 144 MB % 132.63/19.56 % (388606)Instructions burned: 4095 (million) % 132.63/19.56 % (388628)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=2690558548:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2911 on theBenchmark for (2911ds/4975Mi) % 132.63/19.56 % (388623)Instruction limit reached! % 132.63/19.56 % (388623)------------------------------ % 132.63/19.56 % (388623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.63/19.56 % (388623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.63/19.56 % (388623)CaDiCaL version: 2.1.3 % 132.63/19.56 % (388623)Termination reason: Instruction limit % 132.63/19.56 % (388623)Termination phase: Saturation % 132.63/19.56 % (388623)Time elapsed: 0.921 s % 132.63/19.56 % (388623)Peak memory usage: 125 MB % 132.63/19.56 % (388623)Instructions burned: 1783 (million) % 132.63/19.56 % (388630)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=1221489862:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2906 on theBenchmark for (2906ds/2076Mi) % 132.63/19.56 % (388610)Instruction limit reached! % 132.63/19.56 % (388610)------------------------------ % 132.63/19.56 % (388610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.63/19.56 % (388610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.63/19.56 % (388610)CaDiCaL version: 2.1.3 % 132.63/19.56 % (388610)Termination reason: Instruction limit % 132.63/19.56 % (388610)Termination phase: Saturation % 132.63/19.56 % (388610)Time elapsed: 3.004 s % 132.63/19.56 % (388610)Peak memory usage: 169 MB % 132.63/19.56 % (388610)Instructions burned: 10546 (million) % 132.63/19.56 % (388632)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=485675503:i=5145:rtra=on_2896 on theBenchmark for (2896ds/5145Mi) % 132.63/19.56 % (388588)Instruction limit reached! % 132.63/19.56 % (388588)------------------------------ % 132.63/19.56 % (388588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.63/19.56 % (388588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.63/19.56 % (388588)CaDiCaL version: 2.1.3 % 132.63/19.56 % (388588)Termination reason: Instruction limit % 132.63/19.56 % (388588)Termination phase: Clausification % 132.63/19.56 % (388588)Time elapsed: 5.726 s % 132.63/19.56 % (388588)Peak memory usage: 3028 MB % 132.63/19.56 % (388588)Instructions burned: 5812 (million) % 132.63/19.56 % (388630)Instruction limit reached! % 132.63/19.56 % (388630)------------------------------ % 132.63/19.56 % (388630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.63/19.56 % (388630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.63/19.56 % (388630)CaDiCaL version: 2.1.3 % 132.63/19.56 % (388630)Termination reason: Instruction limit % 132.63/19.56 % (388630)Termination phase: Saturation % 132.63/19.56 % (388630)Time elapsed: 1.022 s % 132.63/19.56 % (388630)Peak memory usage: 125 MB % 132.63/19.56 % (388630)Instructions burned: 2078 (million) % 132.63/19.56 % (388634)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=977650584:i=3509:rtra=on_2894 on theBenchmark for (2894ds/3509Mi) % 132.63/19.56 % (388636)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1868135158:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2890 on theBenchmark for (2890ds/13800Mi) % 132.63/19.56 % (388636)Refutation not found, incomplete strategy % 132.63/19.56 % (388636)------------------------------ % 132.63/19.56 % (388636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.63/19.56 % (388636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.63/19.56 % (388636)CaDiCaL version: 2.1.3 % 132.63/19.56 % (388636)Termination reason: Refutation not found, incomplete strategy % 132.63/19.56 % (388636)Time elapsed: 0.007 s % 132.63/19.56 % (388636)Peak memory usage: 88 MB % 132.63/19.56 % (388636)Instructions burned: 14 (million) % 132.63/19.56 % (388636)------------------------------ % 132.63/19.56 % (388636)------------------------------ % 132.63/19.56 % (388638)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1025511890:i=1412:rtra=on:fsd=on:proc=on_2887 on theBenchmark for (2887ds/1412Mi) % 213.15/30.88 % (388632)Instruction limit reached! % 213.15/30.88 % (388632)------------------------------ % 213.15/30.88 % (388632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.15/30.88 % (388632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.15/30.88 % (388632)CaDiCaL version: 2.1.3 % 213.15/30.88 % (388632)Termination reason: Instruction limit % 213.15/30.88 % (388632)Termination phase: Saturation % 213.15/30.88 % (388632)Time elapsed: 1.540 s % 213.15/30.88 % (388632)Peak memory usage: 112 MB % 213.15/30.88 % (388632)Instructions burned: 5147 (million) % 213.15/30.88 % (388640)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 % 213.15/30.88 % (388640)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2863429051:i=11747:aac=none:nm=0:rtra=on:rawr=on_2879 on theBenchmark for (2879ds/11747Mi) % 213.15/30.88 % (388638)Instruction limit reached! % 213.15/30.88 % (388638)------------------------------ % 213.15/30.88 % (388638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.15/30.88 % (388638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.15/30.88 % (388638)CaDiCaL version: 2.1.3 % 213.15/30.88 % (388638)Termination reason: Instruction limit % 213.15/30.88 % (388638)Termination phase: Saturation % 213.15/30.88 % (388638)Time elapsed: 0.721 s % 213.15/30.88 % (388638)Peak memory usage: 125 MB % 213.15/30.88 % (388638)Instructions burned: 1412 (million) % 213.15/30.88 % (388642)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=339270154:s2a=on:i=3553:nm=0:rtra=on_2878 on theBenchmark for (2878ds/3553Mi) % 213.15/30.88 % (388634)Instruction limit reached! % 213.15/30.88 % (388634)------------------------------ % 213.15/30.88 % (388634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.15/30.88 % (388634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.15/30.88 % (388634)CaDiCaL version: 2.1.3 % 213.15/30.88 % (388634)Termination reason: Instruction limit % 213.15/30.88 % (388634)Termination phase: Saturation % 213.15/30.88 % (388634)Time elapsed: 2.343 s % 213.15/30.88 % (388634)Peak memory usage: 110 MB % 213.15/30.88 % (388634)Instructions burned: 3510 (million) % 213.15/30.88 % (388760)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=267804014:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/3201Mi) % 213.15/30.88 % (388626)Instruction limit reached! % 213.15/30.88 % (388626)------------------------------ % 213.15/30.88 % (388626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.15/30.88 % (388626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.15/30.88 % (388626)CaDiCaL version: 2.1.3 % 213.15/30.88 % (388626)Termination reason: Instruction limit % 213.15/30.88 % (388626)Termination phase: Clausification % 213.15/30.88 % (388626)Time elapsed: 5.529 s % 213.15/30.88 % (388626)Peak memory usage: 2839 MB % 213.15/30.88 % (388626)Instructions burned: 5451 (million) % 213.15/30.88 % (388628)Instruction limit reached! % 213.15/30.88 % (388628)------------------------------ % 213.15/30.88 % (388628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.15/30.88 % (388628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.15/30.88 % (388628)CaDiCaL version: 2.1.3 % 213.15/30.88 % (388628)Termination reason: Instruction limit % 213.15/30.88 % (388628)Termination phase: Clausification % 213.15/30.88 % (388628)Time elapsed: 5.493 s % 213.15/30.88 % (388628)Peak memory usage: 2947 MB % 213.15/30.88 % (388628)Instructions burned: 4975 (million) % 213.15/30.88 % (388642)Instruction limit reached! % 213.15/30.88 % (388642)------------------------------ % 213.15/30.88 % (388642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.15/30.88 % (388642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.15/30.88 % (388642)CaDiCaL version: 2.1.3 % 213.15/30.88 % (388642)Termination reason: Instruction limit % 213.15/30.88 % (388642)Termination phase: NewCNF % 213.15/30.88 % (388642)Time elapsed: 2.495 s % 213.15/30.88 % (388642)Peak memory usage: 427 MB % 213.15/30.88 % (388642)Instructions burned: 3553 (million) % 213.15/30.88 % (388939)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=573145859:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2851 on theBenchmark for (2851ds/4081Mi) % 238.71/34.48 % (388942)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=37419542:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2850 on theBenchmark for (2850ds/20260Mi) % 238.71/34.48 % (388942)Refutation not found, incomplete strategy % 238.71/34.48 % (388942)------------------------------ % 238.71/34.48 % (388942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.71/34.48 % (388942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.71/34.48 % (388942)CaDiCaL version: 2.1.3 % 238.71/34.48 % (388942)Termination reason: Refutation not found, incomplete strategy % 238.71/34.48 % (388942)Time elapsed: 0.045 s % 238.71/34.48 % (388942)Peak memory usage: 112 MB % 238.71/34.48 % (388942)Instructions burned: 13 (million) % 238.71/34.48 % (388760)Instruction limit reached! % 238.71/34.48 % (388760)------------------------------ % 238.71/34.48 % (388760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.71/34.48 % (388760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.71/34.48 % (388760)CaDiCaL version: 2.1.3 % 238.71/34.48 % (388760)Termination reason: Instruction limit % 238.71/34.48 % (388760)Termination phase: Saturation % 238.71/34.48 % (388760)Time elapsed: 2.193 s % 238.71/34.48 % (388760)Peak memory usage: 97 MB % 238.71/34.48 % (388760)Instructions burned: 3201 (million) % 238.71/34.48 % (388948)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3263722932:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2848 on theBenchmark for (2848ds/58627Mi) % 238.71/34.48 % (388951)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3769041147:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2846 on theBenchmark for (2846ds/6258Mi) % 238.71/34.48 % (388942)------------------------------ % 238.71/34.48 % (388942)------------------------------ % 238.71/34.48 % (388618)Instruction limit reached! % 238.71/34.48 % (388618)------------------------------ % 238.71/34.48 % (388618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.71/34.48 % (388618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.71/34.48 % (388618)CaDiCaL version: 2.1.3 % 238.71/34.48 % (388618)Termination reason: Instruction limit % 238.71/34.48 % (388618)Termination phase: Saturation % 238.71/34.48 % (388618)Time elapsed: 7.457 s % 238.71/34.48 % (388618)Peak memory usage: 108 MB % 238.71/34.48 % (388618)Instructions burned: 13095 (million) % 238.71/34.48 % (388958)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=619546295:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2843 on theBenchmark for (2843ds/34001Mi) % 238.71/34.48 % (388959)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3733875699:s2a=on:i=71622:s2at=-1:rtra=on_2843 on theBenchmark for (2843ds/71622Mi) % 238.71/34.48 % (388617)Instruction limit reached! % 238.71/34.48 % (388617)------------------------------ % 238.71/34.48 % (388617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.71/34.48 % (388617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.71/34.48 % (388617)CaDiCaL version: 2.1.3 % 238.71/34.48 % (388617)Termination reason: Instruction limit % 238.71/34.48 % (388617)Termination phase: Saturation % 238.71/34.48 % (388617)Time elapsed: 8.228 s % 238.71/34.48 % (388617)Peak memory usage: 147 MB % 238.71/34.48 % (388617)Instructions burned: 17165 (million) % 238.71/34.48 % (388964)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=715623188:i=24001:kws=precedence:nm=0:rtra=on_2836 on theBenchmark for (2836ds/24001Mi) % 238.71/34.48 % (388939)Instruction limit reached! % 238.71/34.48 % (388939)------------------------------ % 238.71/34.48 % (388939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.71/34.48 % (388939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.71/34.48 % (388939)CaDiCaL version: 2.1.3 % 238.71/34.48 % (388939)Termination reason: Instruction limit % 238.71/34.48 % (388939)Termination phase: Saturation % 238.71/34.48 % (388939)Time elapsed: 3.542 s % 238.71/34.48 % (388939)Peak memory usage: 144 MB % 238.71/34.48 % (388939)Instructions burned: 4082 (million) % 238.71/34.48 % (388974)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=1156590908:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2813 on theBenchmark for (2813dTerminated %------------------------------------------------------------------------------