%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX118_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:55 PM UTC 2026 % Result : Timeout 300.38s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX118_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.17 % Computer : n011.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 15:02:16 UTC 2026 % 0.06/0.17 % CPUTime : % 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.19 Running first-order theorem proving % 0.06/0.19 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.57/1.14 % (3448451)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.57/1.14 % (3448460)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2428112989:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.57/1.14 % (3448460)Instruction limit reached! % 3.57/1.14 % (3448460)------------------------------ % 3.57/1.14 % (3448460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.57/1.14 % (3448460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/1.14 % (3448460)CaDiCaL version: 2.1.3 % 3.57/1.14 % (3448460)Termination reason: Instruction limit % 3.57/1.14 % (3448460)Termination phase: Saturation % 3.57/1.14 % (3448460)Time elapsed: 0.003 s % 3.57/1.14 % (3448460)Peak memory usage: 89 MB % 3.57/1.14 % (3448460)Instructions burned: 6 (million) % 3.57/1.14 % (3448462)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4237874134:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.57/1.14 % (3448457)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3377635222:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.57/1.14 % (3448458)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1514249257:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.57/1.14 % (3448456)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=121723657:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.57/1.14 % (3448461)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3723184437:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.57/1.14 % (3448459)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1108792150:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.57/1.14 % (3448459)Instruction limit reached! % 3.57/1.14 % (3448459)------------------------------ % 3.57/1.14 % (3448459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.57/1.14 % (3448459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/1.14 % (3448459)CaDiCaL version: 2.1.3 % 3.57/1.14 % (3448459)Termination reason: Instruction limit % 3.57/1.14 % (3448459)Termination phase: Saturation % 3.57/1.14 % (3448459)Time elapsed: 0.005 s % 3.57/1.14 % (3448459)Peak memory usage: 88 MB % 3.57/1.14 % (3448459)Instructions burned: 7 (million) % 3.57/1.14 % (3448456)Instruction limit reached! % 3.57/1.14 % (3448456)------------------------------ % 3.57/1.14 % (3448456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.57/1.14 % (3448456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/1.14 % (3448456)CaDiCaL version: 2.1.3 % 3.57/1.14 % (3448456)Termination reason: Instruction limit % 3.57/1.14 % (3448456)Termination phase: Saturation % 3.57/1.14 % (3448456)Time elapsed: 0.030 s % 3.57/1.14 % (3448456)Peak memory usage: 117 MB % 3.57/1.14 % (3448456)Instructions burned: 12 (million) % 3.57/1.14 % (3448462)Instruction limit reached! % 3.57/1.14 % (3448462)------------------------------ % 3.57/1.14 % (3448462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.57/1.14 % (3448462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/1.14 % (3448462)CaDiCaL version: 2.1.3 % 3.57/1.14 % (3448462)Termination reason: Instruction limit % 3.57/1.14 % (3448462)Termination phase: Saturation % 3.57/1.14 % (3448462)Time elapsed: 0.047 s % 3.57/1.14 % (3448462)Peak memory usage: 117 MB % 3.57/1.14 % (3448462)Instructions burned: 34 (million) % 3.57/1.14 % (3448461)Instruction limit reached! % 3.57/1.14 % (3448461)------------------------------ % 3.57/1.14 % (3448461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.57/1.14 % (3448461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/1.14 % (3448461)CaDiCaL version: 2.1.3 % 3.57/1.14 % (3448461)Termination reason: Instruction limit % 3.57/1.14 % (3448461)Termination phase: Saturation % 3.57/1.14 % (3448461)Time elapsed: 0.056 s % 3.57/1.14 % (3448461)Peak memory usage: 117 MB % 3.57/1.14 % (3448461)Instructions burned: 46 (million) % 3.57/1.14 % (3448464)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3236357585:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.57/1.14 % (3448464)Instruction limit reached! % 3.57/1.14 % (3448464)------------------------------ % 4.00/1.29 % (3448464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.00/1.29 % (3448464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/1.29 % (3448464)CaDiCaL version: 2.1.3 % 4.00/1.29 % (3448464)Termination reason: Instruction limit % 4.00/1.29 % (3448464)Termination phase: Saturation % 4.00/1.29 % (3448464)Time elapsed: 0.006 s % 4.00/1.29 % (3448464)Peak memory usage: 88 MB % 4.00/1.29 % (3448464)Instructions burned: 15 (million) % 4.00/1.29 % (3448458)Instruction limit reached! % 4.00/1.29 % (3448458)------------------------------ % 4.00/1.29 % (3448458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.00/1.29 % (3448458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/1.29 % (3448458)CaDiCaL version: 2.1.3 % 4.00/1.29 % (3448458)Termination reason: Instruction limit % 4.00/1.29 % (3448458)Termination phase: Saturation % 4.00/1.29 % (3448458)Time elapsed: 0.120 s % 4.00/1.29 % (3448458)Peak memory usage: 113 MB % 4.00/1.29 % (3448458)Instructions burned: 203 (million) % 4.00/1.29 % (3448471)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=1347706046:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.00/1.29 % (3448472)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2555561974:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.00/1.29 % (3448471)Instruction limit reached! % 4.00/1.29 % (3448471)------------------------------ % 4.00/1.29 % (3448471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.00/1.29 % (3448471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/1.29 % (3448471)CaDiCaL version: 2.1.3 % 4.00/1.29 % (3448471)Termination reason: Instruction limit % 4.00/1.29 % (3448471)Termination phase: Saturation % 4.00/1.29 % (3448471)Time elapsed: 0.024 s % 4.00/1.29 % (3448471)Peak memory usage: 89 MB % 4.00/1.29 % (3448471)Instructions burned: 30 (million) % 4.00/1.29 % (3448472)Instruction limit reached! % 4.00/1.29 % (3448472)------------------------------ % 4.00/1.29 % (3448472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.00/1.29 % (3448472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/1.29 % (3448472)CaDiCaL version: 2.1.3 % 4.00/1.29 % (3448472)Termination reason: Instruction limit % 4.00/1.29 % (3448472)Termination phase: Saturation % 4.00/1.29 % (3448472)Time elapsed: 0.012 s % 4.00/1.29 % (3448472)Peak memory usage: 90 MB % 4.00/1.29 % (3448472)Instructions burned: 17 (million) % 4.00/1.29 % (3448476)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3472432301:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.00/1.29 % (3448473)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1956834401:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.00/1.29 % (3448473)Instruction limit reached! % 4.00/1.29 % (3448473)------------------------------ % 4.00/1.29 % (3448473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.00/1.29 % (3448473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/1.29 % (3448473)CaDiCaL version: 2.1.3 % 4.00/1.29 % (3448473)Termination reason: Instruction limit % 4.00/1.29 % (3448473)Termination phase: Saturation % 4.00/1.29 % (3448473)Time elapsed: 0.018 s % 4.00/1.29 % (3448473)Peak memory usage: 89 MB % 4.00/1.29 % (3448473)Instructions burned: 24 (million) % 4.00/1.29 % (3448474)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=2181847107:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.00/1.29 % (3448476)Instruction limit reached! % 4.00/1.29 % (3448476)------------------------------ % 4.00/1.29 % (3448476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.00/1.29 % (3448476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/1.29 % (3448476)CaDiCaL version: 2.1.3 % 4.00/1.29 % (3448476)Termination reason: Instruction limit % 4.00/1.29 % (3448476)Termination phase: Saturation % 4.00/1.29 % (3448476)Time elapsed: 0.025 s % 4.00/1.29 % (3448476)Peak memory usage: 89 MB % 4.00/1.29 % (3448476)Instructions burned: 86 (million) % 4.00/1.29 % (3448474)Instruction limit reached! % 4.00/1.29 % (3448474)------------------------------ % 4.00/1.29 % (3448474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.02/1.42 % (3448474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.02/1.42 % (3448474)CaDiCaL version: 2.1.3 % 5.02/1.42 % (3448474)Termination reason: Instruction limit % 5.02/1.42 % (3448474)Termination phase: Saturation % 5.02/1.42 % (3448474)Time elapsed: 0.021 s % 5.02/1.42 % (3448474)Peak memory usage: 89 MB % 5.02/1.42 % (3448474)Instructions burned: 27 (million) % 5.02/1.42 % (3448457)Instruction limit reached! % 5.02/1.42 % (3448457)------------------------------ % 5.02/1.42 % (3448457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.02/1.42 % (3448457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.02/1.42 % (3448457)CaDiCaL version: 2.1.3 % 5.02/1.42 % (3448457)Termination reason: Instruction limit % 5.02/1.42 % (3448457)Termination phase: Saturation % 5.02/1.42 % (3448457)Time elapsed: 0.235 s % 5.02/1.42 % (3448457)Peak memory usage: 118 MB % 5.02/1.42 % (3448457)Instructions burned: 307 (million) % 5.02/1.42 % (3448477)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4222917644:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi) % 5.02/1.42 % (3448477)Instruction limit reached! % 5.02/1.42 % (3448477)------------------------------ % 5.02/1.42 % (3448477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.02/1.42 % (3448477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.02/1.42 % (3448477)CaDiCaL version: 2.1.3 % 5.02/1.42 % (3448477)Termination reason: Instruction limit % 5.02/1.42 % (3448477)Termination phase: Saturation % 5.02/1.42 % (3448477)Time elapsed: 0.002 s % 5.02/1.42 % (3448477)Peak memory usage: 88 MB % 5.02/1.42 % (3448477)Instructions burned: 2 (million) % 5.02/1.42 % (3448486)lrs+10_1_thi=all:si=on:fd=off:random_seed=2271675437:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.02/1.42 % (3448480)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2440355872:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.02/1.42 % (3448481)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1234516229:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.02/1.42 % (3448481)Instruction limit reached! % 5.02/1.42 % (3448481)------------------------------ % 5.02/1.42 % (3448481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.02/1.42 % (3448481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.02/1.42 % (3448481)CaDiCaL version: 2.1.3 % 5.02/1.42 % (3448481)Termination reason: Instruction limit % 5.02/1.42 % (3448481)Termination phase: Saturation % 5.02/1.42 % (3448481)Time elapsed: 0.004 s % 5.02/1.42 % (3448481)Peak memory usage: 88 MB % 5.02/1.42 % (3448481)Instructions burned: 5 (million) % 5.02/1.42 % (3448486)Instruction limit reached! % 5.02/1.42 % (3448486)------------------------------ % 5.02/1.42 % (3448486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.02/1.42 % (3448486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.02/1.42 % (3448486)CaDiCaL version: 2.1.3 % 5.02/1.42 % (3448486)Termination reason: Instruction limit % 5.02/1.42 % (3448486)Termination phase: Saturation % 5.02/1.42 % (3448486)Time elapsed: 0.036 s % 5.02/1.42 % (3448486)Peak memory usage: 116 MB % 5.02/1.42 % (3448486)Instructions burned: 53 (million) % 5.02/1.42 % (3448485)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3386974420:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.02/1.42 % (3448488)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1804139719:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 5.02/1.42 % (3448487)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=2104517080:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 5.02/1.42 % (3448488)Instruction limit reached! % 5.02/1.42 % (3448488)------------------------------ % 5.02/1.42 % (3448488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.02/1.42 % (3448488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.02/1.42 % (3448488)CaDiCaL version: 2.1.3 % 5.02/1.42 % (3448488)Termination reason: Instruction limit % 5.02/1.42 % (3448488)Termination phase: Saturation % 6.53/1.66 % (3448488)Time elapsed: 0.002 s % 6.53/1.66 % (3448488)Peak memory usage: 88 MB % 6.53/1.66 % (3448488)Instructions burned: 2 (million) % 6.53/1.66 % (3448487)Instruction limit reached! % 6.53/1.66 % (3448487)------------------------------ % 6.53/1.66 % (3448487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.53/1.66 % (3448487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.66 % (3448487)CaDiCaL version: 2.1.3 % 6.53/1.66 % (3448487)Termination reason: Instruction limit % 6.53/1.66 % (3448487)Termination phase: Saturation % 6.53/1.66 % (3448487)Time elapsed: 0.006 s % 6.53/1.66 % (3448487)Peak memory usage: 89 MB % 6.53/1.66 % (3448487)Instructions burned: 8 (million) % 6.53/1.66 % (3448490)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2060331423:i=2:doe=on:canc=force:asg=cautious:rtra=on_2996 on theBenchmark for (2996ds/2Mi) % 6.53/1.66 % (3448490)Instruction limit reached! % 6.53/1.66 % (3448490)------------------------------ % 6.53/1.66 % (3448490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.53/1.66 % (3448490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.66 % (3448490)CaDiCaL version: 2.1.3 % 6.53/1.66 % (3448490)Termination reason: Instruction limit % 6.53/1.66 % (3448490)Termination phase: Saturation % 6.53/1.66 % (3448490)Time elapsed: 0.002 s % 6.53/1.66 % (3448490)Peak memory usage: 88 MB % 6.53/1.66 % (3448490)Instructions burned: 2 (million) % 6.53/1.66 % (3448496)dis+10_1_si=on:random_seed=2023335247:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi) % 6.53/1.66 % (3448496)Instruction limit reached! % 6.53/1.66 % (3448496)------------------------------ % 6.53/1.66 % (3448496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.53/1.66 % (3448496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.66 % (3448496)CaDiCaL version: 2.1.3 % 6.53/1.66 % (3448496)Termination reason: Instruction limit % 6.53/1.66 % (3448496)Termination phase: Saturation % 6.53/1.66 % (3448496)Time elapsed: 0.004 s % 6.53/1.66 % (3448496)Peak memory usage: 88 MB % 6.53/1.66 % (3448496)Instructions burned: 10 (million) % 6.53/1.66 % (3448485)Instruction limit reached! % 6.53/1.66 % (3448485)------------------------------ % 6.53/1.66 % (3448485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.53/1.66 % (3448485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.66 % (3448485)CaDiCaL version: 2.1.3 % 6.53/1.66 % (3448485)Termination reason: Instruction limit % 6.53/1.66 % (3448485)Termination phase: Saturation % 6.53/1.66 % (3448485)Time elapsed: 0.097 s % 6.53/1.66 % (3448485)Peak memory usage: 135 MB % 6.53/1.66 % (3448485)Instructions burned: 66 (million) % 6.53/1.66 % (3448480)Instruction limit reached! % 6.53/1.66 % (3448480)------------------------------ % 6.53/1.66 % (3448480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.53/1.66 % (3448480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.66 % (3448480)CaDiCaL version: 2.1.3 % 6.53/1.66 % (3448480)Termination reason: Instruction limit % 6.53/1.66 % (3448480)Termination phase: Saturation % 6.53/1.66 % (3448480)Time elapsed: 0.126 s % 6.53/1.66 % (3448480)Peak memory usage: 90 MB % 6.53/1.66 % (3448480)Instructions burned: 181 (million) % 6.53/1.66 % (3448494)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2570967035:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.53/1.66 % (3448499)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1171842624:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.53/1.66 % (3448501)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2365751483: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) % 6.53/1.66 % (3448499)Refutation not found, incomplete strategy % 6.53/1.66 % (3448499)------------------------------ % 6.53/1.66 % (3448499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.53/1.66 % (3448499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.66 % (3448499)CaDiCaL version: 2.1.3 % 6.53/1.66 % (3448499)Termination reason: Refutation not found, incomplete strategy % 6.53/1.66 % (3448499)Time elapsed: 0.004 s % 6.53/1.66 % (3448499)Peak memory usage: 89 MB % 6.53/1.66 % (3448499)Instructions burned: 4 (million) % 6.53/1.66 % (3448502)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3577313722:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.49/1.86 % (3448504)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3196887215:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.49/1.86 % (3448502)Instruction limit reached! % 7.49/1.86 % (3448502)------------------------------ % 7.49/1.86 % (3448502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.49/1.86 % (3448502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.49/1.86 % (3448502)CaDiCaL version: 2.1.3 % 7.49/1.86 % (3448502)Termination reason: Instruction limit % 7.49/1.86 % (3448502)Termination phase: Saturation % 7.49/1.86 % (3448502)Time elapsed: 0.002 s % 7.49/1.86 % (3448502)Peak memory usage: 88 MB % 7.49/1.86 % (3448502)Instructions burned: 3 (million) % 7.49/1.86 % (3448504)Instruction limit reached! % 7.49/1.86 % (3448504)------------------------------ % 7.49/1.86 % (3448504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.49/1.86 % (3448504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.49/1.86 % (3448504)CaDiCaL version: 2.1.3 % 7.49/1.86 % (3448504)Termination reason: Instruction limit % 7.49/1.86 % (3448504)Termination phase: Saturation % 7.49/1.86 % (3448504)Time elapsed: 0.004 s % 7.49/1.86 % (3448504)Peak memory usage: 88 MB % 7.49/1.86 % (3448504)Instructions burned: 9 (million) % 7.49/1.86 % (3448501)Instruction limit reached! % 7.49/1.86 % (3448501)------------------------------ % 7.49/1.86 % (3448501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.49/1.86 % (3448501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.49/1.86 % (3448501)CaDiCaL version: 2.1.3 % 7.49/1.86 % (3448501)Termination reason: Instruction limit % 7.49/1.86 % (3448501)Termination phase: Saturation % 7.49/1.86 % (3448501)Time elapsed: 0.027 s % 7.49/1.86 % (3448501)Peak memory usage: 89 MB % 7.49/1.86 % (3448501)Instructions burned: 35 (million) % 7.49/1.86 % (3448494)Instruction limit reached! % 7.49/1.86 % (3448494)------------------------------ % 7.49/1.86 % (3448494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.49/1.86 % (3448494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.49/1.86 % (3448494)CaDiCaL version: 2.1.3 % 7.49/1.86 % (3448494)Termination reason: Instruction limit % 7.49/1.86 % (3448494)Termination phase: Saturation % 7.49/1.86 % (3448494)Time elapsed: 0.113 s % 7.49/1.86 % (3448494)Peak memory usage: 117 MB % 7.49/1.86 % (3448494)Instructions burned: 128 (million) % 7.49/1.86 % (3448506)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3134715099:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi) % 7.49/1.86 % (3448505)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1679421502:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 7.49/1.86 % (3448506)Instruction limit reached! % 7.49/1.86 % (3448506)------------------------------ % 7.49/1.86 % (3448506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.49/1.86 % (3448506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.49/1.86 % (3448506)CaDiCaL version: 2.1.3 % 7.49/1.86 % (3448506)Termination reason: Instruction limit % 7.49/1.86 % (3448506)Termination phase: Saturation % 7.49/1.86 % (3448506)Time elapsed: 0.032 s % 7.49/1.86 % (3448506)Peak memory usage: 116 MB % 7.49/1.86 % (3448506)Instructions burned: 13 (million) % 7.49/1.86 % (3448512)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=190017313:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.49/1.86 % (3448513)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1142500141:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 7.49/1.86 % (3448514)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=657245954:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 7.49/1.86 % (3448513)Instruction limit reached! % 7.49/1.86 % (3448513)------------------------------ % 7.49/1.86 % (3448513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.49/1.86 % (3448513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.49/1.86 % (3448513)CaDiCaL version: 2.1.3 % 10.26/2.12 % (3448513)Termination reason: Instruction limit % 10.26/2.12 % (3448513)Termination phase: Saturation % 10.26/2.12 % (3448513)Time elapsed: 0.009 s % 10.26/2.12 % (3448513)Peak memory usage: 88 MB % 10.26/2.12 % (3448513)Instructions burned: 11 (million) % 10.26/2.12 % (3448516)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=3542006563:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 10.26/2.12 % (3448512)Instruction limit reached! % 10.26/2.12 % (3448512)------------------------------ % 10.26/2.12 % (3448512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.26/2.12 % (3448512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.26/2.12 % (3448512)CaDiCaL version: 2.1.3 % 10.26/2.12 % (3448512)Termination reason: Instruction limit % 10.26/2.12 % (3448512)Termination phase: Saturation % 10.26/2.12 % (3448512)Time elapsed: 0.089 s % 10.26/2.12 % (3448512)Peak memory usage: 118 MB % 10.26/2.12 % (3448512)Instructions burned: 226 (million) % 10.26/2.12 % (3448518)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=1038910362:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.26/2.12 % (3448499)------------------------------ % 10.26/2.12 % (3448499)------------------------------ % 10.26/2.12 % (3448514)Instruction limit reached! % 10.26/2.12 % (3448514)------------------------------ % 10.26/2.12 % (3448514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.26/2.12 % (3448514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.26/2.12 % (3448514)CaDiCaL version: 2.1.3 % 10.26/2.12 % (3448514)Termination reason: Instruction limit % 10.26/2.12 % (3448514)Termination phase: Saturation % 10.26/2.12 % (3448514)Time elapsed: 0.095 s % 10.26/2.12 % (3448514)Peak memory usage: 135 MB % 10.26/2.12 % (3448514)Instructions burned: 71 (million) % 10.26/2.12 % (3448516)Instruction limit reached! % 10.26/2.12 % (3448516)------------------------------ % 10.26/2.12 % (3448516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.26/2.12 % (3448516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.26/2.12 % (3448516)CaDiCaL version: 2.1.3 % 10.26/2.12 % (3448516)Termination reason: Instruction limit % 10.26/2.12 % (3448516)Termination phase: Saturation % 10.26/2.12 % (3448516)Time elapsed: 0.072 s % 10.26/2.12 % (3448516)Peak memory usage: 91 MB % 10.26/2.12 % (3448516)Instructions burned: 75 (million) % 10.26/2.12 % (3448522)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1279208159:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 10.26/2.12 % (3448524)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2584785403:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.26/2.12 % (3448505)Instruction limit reached! % 10.26/2.12 % (3448505)------------------------------ % 10.26/2.12 % (3448505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.26/2.12 % (3448505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.26/2.12 % (3448505)CaDiCaL version: 2.1.3 % 10.26/2.12 % (3448505)Termination reason: Instruction limit % 10.26/2.12 % (3448505)Termination phase: Saturation % 10.26/2.12 % (3448505)Time elapsed: 0.230 s % 10.26/2.12 % (3448505)Peak memory usage: 94 MB % 10.26/2.12 % (3448505)Instructions burned: 370 (million) % 10.26/2.12 % (3448527)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2423598388:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 10.26/2.12 % (3448524)Instruction limit reached! % 10.26/2.12 % (3448524)------------------------------ % 10.26/2.12 % (3448524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.26/2.12 % (3448524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.26/2.12 % (3448524)CaDiCaL version: 2.1.3 % 10.26/2.12 % (3448524)Termination reason: Instruction limit % 10.26/2.12 % (3448524)Termination phase: Saturation % 10.26/2.12 % (3448524)Time elapsed: 0.079 s % 10.26/2.12 % (3448524)Peak memory usage: 135 MB % 10.26/2.12 % (3448524)Instructions burned: 133 (million) % 10.26/2.12 % (3448526)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2249851293:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 10.26/2.12 % (3448522)Instruction limit reached! % 10.26/2.12 % (3448522)------------------------------ % 11.83/2.42 % (3448522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.42 % (3448522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.42 % (3448522)CaDiCaL version: 2.1.3 % 11.83/2.42 % (3448522)Termination reason: Instruction limit % 11.83/2.42 % (3448522)Termination phase: Saturation % 11.83/2.42 % (3448522)Time elapsed: 0.109 s % 11.83/2.42 % (3448522)Peak memory usage: 118 MB % 11.83/2.42 % (3448522)Instructions burned: 131 (million) % 11.83/2.42 % (3448528)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2376579498:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi) % 11.83/2.42 % (3448518)Instruction limit reached! % 11.83/2.42 % (3448518)------------------------------ % 11.83/2.42 % (3448518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.42 % (3448518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.42 % (3448518)CaDiCaL version: 2.1.3 % 11.83/2.42 % (3448518)Termination reason: Instruction limit % 11.83/2.42 % (3448518)Termination phase: Saturation % 11.83/2.42 % (3448518)Time elapsed: 0.204 s % 11.83/2.42 % (3448518)Peak memory usage: 90 MB % 11.83/2.42 % (3448518)Instructions burned: 294 (million) % 11.83/2.42 % (3448531)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3501332448:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.83/2.42 % (3448526)Instruction limit reached! % 11.83/2.42 % (3448526)------------------------------ % 11.83/2.42 % (3448526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.42 % (3448526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.42 % (3448526)CaDiCaL version: 2.1.3 % 11.83/2.42 % (3448526)Termination reason: Instruction limit % 11.83/2.42 % (3448526)Termination phase: Saturation % 11.83/2.42 % (3448526)Time elapsed: 0.071 s % 11.83/2.42 % (3448526)Peak memory usage: 134 MB % 11.83/2.42 % (3448526)Instructions burned: 40 (million) % 11.83/2.42 % (3448534)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=528579415:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 11.83/2.42 % (3448536)dis+10_1_si=on:random_seed=2283830842:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.83/2.42 % (3448531)Instruction limit reached! % 11.83/2.42 % (3448531)------------------------------ % 11.83/2.42 % (3448531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.42 % (3448531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.42 % (3448531)CaDiCaL version: 2.1.3 % 11.83/2.42 % (3448531)Termination reason: Instruction limit % 11.83/2.42 % (3448531)Termination phase: Saturation % 11.83/2.42 % (3448531)Time elapsed: 0.101 s % 11.83/2.42 % (3448531)Peak memory usage: 118 MB % 11.83/2.42 % (3448531)Instructions burned: 132 (million) % 11.83/2.42 % (3448537)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2418006157:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 11.83/2.42 % (3448534)Instruction limit reached! % 11.83/2.42 % (3448534)------------------------------ % 11.83/2.42 % (3448534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.42 % (3448534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.42 % (3448534)CaDiCaL version: 2.1.3 % 11.83/2.42 % (3448534)Termination reason: Instruction limit % 11.83/2.42 % (3448534)Termination phase: Saturation % 11.83/2.42 % (3448534)Time elapsed: 0.098 s % 11.83/2.42 % (3448534)Peak memory usage: 118 MB % 11.83/2.42 % (3448534)Instructions burned: 263 (million) % 11.83/2.42 % (3448539)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2526357034:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi) % 11.83/2.42 % (3448527)Instruction limit reached! % 11.83/2.42 % (3448527)------------------------------ % 11.83/2.42 % (3448527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.83/2.42 % (3448527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.83/2.42 % (3448527)CaDiCaL version: 2.1.3 % 11.83/2.42 % (3448527)Termination reason: Instruction limit % 11.83/2.42 % (3448527)Termination phase: Saturation % 11.83/2.42 % (3448527)Time elapsed: 0.213 s % 11.83/2.42 % (3448527)Peak memory usage: 92 MB % 11.83/2.42 % (3448527)Instructions burned: 307 (million) % 13.30/2.67 % (3448544)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3820193315:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.30/2.67 % (3448542)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=968236441:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.30/2.67 % (3448539)Instruction limit reached! % 13.30/2.67 % (3448539)------------------------------ % 13.30/2.67 % (3448539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.30/2.67 % (3448539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.30/2.67 % (3448539)CaDiCaL version: 2.1.3 % 13.30/2.67 % (3448539)Termination reason: Instruction limit % 13.30/2.67 % (3448539)Termination phase: Saturation % 13.30/2.67 % (3448539)Time elapsed: 0.093 s % 13.30/2.67 % (3448539)Peak memory usage: 90 MB % 13.30/2.67 % (3448539)Instructions burned: 141 (million) % 13.30/2.67 % (3448544)Instruction limit reached! % 13.30/2.67 % (3448544)------------------------------ % 13.30/2.67 % (3448544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.30/2.67 % (3448544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.30/2.67 % (3448544)CaDiCaL version: 2.1.3 % 13.30/2.67 % (3448544)Termination reason: Instruction limit % 13.30/2.67 % (3448544)Termination phase: Saturation % 13.30/2.67 % (3448544)Time elapsed: 0.044 s % 13.30/2.67 % (3448544)Peak memory usage: 89 MB % 13.30/2.67 % (3448544)Instructions burned: 122 (million) % 13.30/2.67 % (3448546)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=540499731:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.30/2.67 % (3448542)Instruction limit reached! % 13.30/2.67 % (3448542)------------------------------ % 13.30/2.67 % (3448542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.30/2.67 % (3448542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.30/2.67 % (3448542)CaDiCaL version: 2.1.3 % 13.30/2.67 % (3448542)Termination reason: Instruction limit % 13.30/2.67 % (3448542)Termination phase: Saturation % 13.30/2.67 % (3448542)Time elapsed: 0.070 s % 13.30/2.67 % (3448542)Peak memory usage: 118 MB % 13.30/2.67 % (3448542)Instructions burned: 66 (million) % 13.30/2.67 % (3448528)Instruction limit reached! % 13.30/2.67 % (3448528)------------------------------ % 13.30/2.67 % (3448528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.30/2.67 % (3448528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.30/2.67 % (3448528)CaDiCaL version: 2.1.3 % 13.30/2.67 % (3448528)Termination reason: Instruction limit % 13.30/2.67 % (3448528)Termination phase: Saturation % 13.30/2.67 % (3448528)Time elapsed: 0.381 s % 13.30/2.67 % (3448528)Peak memory usage: 136 MB % 13.30/2.67 % (3448528)Instructions burned: 598 (million) % 13.30/2.67 % (3448550)dis+1010_1_to=kbo:si=on:random_seed=1185879904:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 13.30/2.67 % (3448537)Instruction limit reached! % 13.30/2.67 % (3448537)------------------------------ % 13.30/2.67 % (3448537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.30/2.67 % (3448537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.30/2.68 % (3448537)CaDiCaL version: 2.1.3 % 13.30/2.68 % (3448537)Termination reason: Instruction limit % 13.30/2.68 % (3448537)Termination phase: Saturation % 13.30/2.68 % (3448537)Time elapsed: 0.237 s % 13.30/2.68 % (3448537)Peak memory usage: 91 MB % 13.30/2.68 % (3448537)Instructions burned: 384 (million) % 13.30/2.68 % (3448549)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=3708209331:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.30/2.68 % (3448546)Instruction limit reached! % 13.30/2.68 % (3448546)------------------------------ % 13.30/2.68 % (3448546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.30/2.68 % (3448546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.30/2.68 % (3448546)CaDiCaL version: 2.1.3 % 13.30/2.68 % (3448546)Termination reason: Instruction limit % 13.30/2.68 % (3448546)Termination phase: Saturation % 13.30/2.68 % (3448546)Time elapsed: 0.100 s % 13.30/2.68 % (3448546)Peak memory usage: 119 MB % 13.30/2.68 % (3448546)Instructions burned: 129 (million) % 13.30/2.68 % (3448550)Instruction limit reached! % 13.30/2.68 % (3448550)------------------------------ % 15.05/2.95 % (3448550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/2.95 % (3448550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/2.95 % (3448550)CaDiCaL version: 2.1.3 % 15.05/2.95 % (3448550)Termination reason: Instruction limit % 15.05/2.95 % (3448550)Termination phase: Saturation % 15.05/2.95 % (3448550)Time elapsed: 0.071 s % 15.05/2.95 % (3448550)Peak memory usage: 91 MB % 15.05/2.95 % (3448550)Instructions burned: 176 (million) % 15.05/2.95 % (3448552)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1984513615:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 15.05/2.95 % (3448549)Instruction limit reached! % 15.05/2.95 % (3448549)------------------------------ % 15.05/2.95 % (3448549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/2.95 % (3448549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/2.95 % (3448549)CaDiCaL version: 2.1.3 % 15.05/2.95 % (3448549)Termination reason: Instruction limit % 15.05/2.95 % (3448549)Termination phase: Saturation % 15.05/2.95 % (3448549)Time elapsed: 0.052 s % 15.05/2.95 % (3448549)Peak memory usage: 118 MB % 15.05/2.95 % (3448549)Instructions burned: 39 (million) % 15.05/2.95 % (3448554)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1547723037:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.05/2.95 % (3448555)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2327315242:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.05/2.95 % (3448558)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=434027516:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 15.05/2.95 % (3448557)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=488433210:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.05/2.95 % (3448560)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=899607151:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi) % 15.05/2.95 % (3448558)Instruction limit reached! % 15.05/2.95 % (3448558)------------------------------ % 15.05/2.95 % (3448558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/2.95 % (3448558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/2.95 % (3448558)CaDiCaL version: 2.1.3 % 15.05/2.95 % (3448558)Termination reason: Instruction limit % 15.05/2.95 % (3448558)Termination phase: Saturation % 15.05/2.95 % (3448558)Time elapsed: 0.085 s % 15.05/2.95 % (3448558)Peak memory usage: 91 MB % 15.05/2.95 % (3448558)Instructions burned: 296 (million) % 15.05/2.95 % (3448552)Instruction limit reached! % 15.05/2.95 % (3448552)------------------------------ % 15.05/2.95 % (3448552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/2.95 % (3448552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/2.95 % (3448552)CaDiCaL version: 2.1.3 % 15.05/2.95 % (3448552)Termination reason: Instruction limit % 15.05/2.95 % (3448552)Termination phase: Saturation % 15.05/2.95 % (3448552)Time elapsed: 0.176 s % 15.05/2.95 % (3448552)Peak memory usage: 113 MB % 15.05/2.95 % (3448552)Instructions burned: 330 (million) % 15.05/2.95 % (3448555)Instruction limit reached! % 15.05/2.95 % (3448555)------------------------------ % 15.05/2.95 % (3448555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/2.95 % (3448555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/2.95 % (3448555)CaDiCaL version: 2.1.3 % 15.05/2.95 % (3448555)Termination reason: Instruction limit % 15.05/2.95 % (3448555)Termination phase: Saturation % 15.05/2.95 % (3448555)Time elapsed: 0.177 s % 15.05/2.95 % (3448555)Peak memory usage: 137 MB % 15.05/2.95 % (3448555)Instructions burned: 215 (million) % 15.05/2.95 % (3448566)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=901879674:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 15.05/2.95 % (3448536)Instruction limit reached! % 15.05/2.95 % (3448536)------------------------------ % 15.05/2.95 % (3448536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/2.95 % (3448536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/2.95 % (3448536)CaDiCaL version: 2.1.3 % 15.05/2.95 % (3448536)Termination reason: Instruction limit % 18.08/3.19 % (3448536)Termination phase: Saturation % 18.08/3.19 % (3448536)Time elapsed: 0.629 s % 18.08/3.19 % (3448536)Peak memory usage: 96 MB % 18.08/3.19 % (3448536)Instructions burned: 1001 (million) % 18.08/3.19 % (3448567)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3478983079:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi) % 18.08/3.19 % (3448557)Instruction limit reached! % 18.08/3.19 % (3448557)------------------------------ % 18.08/3.19 % (3448557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.08/3.19 % (3448557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/3.19 % (3448557)CaDiCaL version: 2.1.3 % 18.08/3.19 % (3448557)Termination reason: Instruction limit % 18.08/3.19 % (3448557)Termination phase: Saturation % 18.08/3.19 % (3448557)Time elapsed: 0.235 s % 18.08/3.19 % (3448557)Peak memory usage: 119 MB % 18.08/3.19 % (3448557)Instructions burned: 349 (million) % 18.08/3.19 % (3448566)Instruction limit reached! % 18.08/3.19 % (3448566)------------------------------ % 18.08/3.19 % (3448566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.08/3.19 % (3448566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/3.19 % (3448566)CaDiCaL version: 2.1.3 % 18.08/3.19 % (3448566)Termination reason: Instruction limit % 18.08/3.19 % (3448566)Termination phase: Saturation % 18.08/3.19 % (3448566)Time elapsed: 0.117 s % 18.08/3.19 % (3448566)Peak memory usage: 119 MB % 18.08/3.19 % (3448566)Instructions burned: 283 (million) % 18.08/3.19 % (3448560)Instruction limit reached! % 18.08/3.19 % (3448560)------------------------------ % 18.08/3.19 % (3448560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.08/3.19 % (3448560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/3.19 % (3448560)CaDiCaL version: 2.1.3 % 18.08/3.19 % (3448560)Termination reason: Instruction limit % 18.08/3.19 % (3448560)Termination phase: Saturation % 18.08/3.19 % (3448560)Time elapsed: 0.237 s % 18.08/3.19 % (3448560)Peak memory usage: 120 MB % 18.08/3.19 % (3448560)Instructions burned: 329 (million) % 18.08/3.19 % (3448569)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2799912425:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 18.08/3.19 % (3448554)Instruction limit reached! % 18.08/3.19 % (3448554)------------------------------ % 18.08/3.19 % (3448554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.08/3.19 % (3448554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/3.19 % (3448554)CaDiCaL version: 2.1.3 % 18.08/3.19 % (3448554)Termination reason: Instruction limit % 18.08/3.19 % (3448554)Termination phase: Saturation % 18.08/3.19 % (3448554)Time elapsed: 0.359 s % 18.08/3.19 % (3448554)Peak memory usage: 137 MB % 18.08/3.19 % (3448554)Instructions burned: 483 (million) % 18.08/3.19 % (3448570)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=877767131:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 18.08/3.19 % (3448572)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=127594602:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 18.08/3.19 % (3448574)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1276467497:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi) % 18.08/3.19 % (3448573)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=2270123422:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 18.08/3.19 % (3448577)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4048370376:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 18.08/3.19 % (3448569)Instruction limit reached! % 18.08/3.19 % (3448569)------------------------------ % 18.08/3.19 % (3448569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.08/3.19 % (3448569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.08/3.19 % (3448569)CaDiCaL version: 2.1.3 % 18.08/3.19 % (3448569)Termination reason: Instruction limit % 18.08/3.19 % (3448569)Termination phase: Saturation % 18.08/3.19 % (3448569)Time elapsed: 0.156 s % 18.08/3.19 % (3448569)Peak memory usage: 114 MB % 19.47/3.74 % (3448569)Instructions burned: 321 (million) % 19.47/3.74 % (3448567)Instruction limit reached! % 19.47/3.74 % (3448567)------------------------------ % 19.47/3.74 % (3448567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.74 % (3448567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.74 % (3448567)CaDiCaL version: 2.1.3 % 19.47/3.74 % (3448567)Termination reason: Instruction limit % 19.47/3.74 % (3448567)Termination phase: Saturation % 19.47/3.74 % (3448567)Time elapsed: 0.302 s % 19.47/3.74 % (3448567)Peak memory usage: 94 MB % 19.47/3.74 % (3448567)Instructions burned: 486 (million) % 19.47/3.74 % (3448574)Instruction limit reached! % 19.47/3.74 % (3448574)------------------------------ % 19.47/3.74 % (3448574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.74 % (3448574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.74 % (3448574)CaDiCaL version: 2.1.3 % 19.47/3.74 % (3448574)Termination reason: Instruction limit % 19.47/3.74 % (3448574)Termination phase: Saturation % 19.47/3.74 % (3448574)Time elapsed: 0.143 s % 19.47/3.74 % (3448574)Peak memory usage: 120 MB % 19.47/3.74 % (3448574)Instructions burned: 375 (million) % 19.47/3.74 % (3448570)Instruction limit reached! % 19.47/3.74 % (3448570)------------------------------ % 19.47/3.74 % (3448570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.74 % (3448570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.74 % (3448570)CaDiCaL version: 2.1.3 % 19.47/3.74 % (3448570)Termination reason: Instruction limit % 19.47/3.74 % (3448570)Termination phase: Saturation % 19.47/3.74 % (3448570)Time elapsed: 0.251 s % 19.47/3.74 % (3448570)Peak memory usage: 119 MB % 19.47/3.74 % (3448570)Instructions burned: 416 (million) % 19.47/3.74 % (3448582)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=967531054:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 19.47/3.74 % (3448584)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2591056825:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 19.47/3.74 % (3448573)Instruction limit reached! % 19.47/3.74 % (3448573)------------------------------ % 19.47/3.74 % (3448573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.74 % (3448573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.74 % (3448573)CaDiCaL version: 2.1.3 % 19.47/3.74 % (3448573)Termination reason: Instruction limit % 19.47/3.74 % (3448573)Termination phase: Saturation % 19.47/3.74 % (3448573)Time elapsed: 0.221 s % 19.47/3.74 % (3448573)Peak memory usage: 136 MB % 19.47/3.74 % (3448573)Instructions burned: 277 (million) % 19.47/3.74 % (3448583)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2318784569:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi) % 19.47/3.74 % (3448572)Instruction limit reached! % 19.47/3.74 % (3448572)------------------------------ % 19.47/3.74 % (3448572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.74 % (3448572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.74 % (3448572)CaDiCaL version: 2.1.3 % 19.47/3.74 % (3448572)Termination reason: Instruction limit % 19.47/3.74 % (3448572)Termination phase: Saturation % 19.47/3.74 % (3448572)Time elapsed: 0.322 s % 19.47/3.74 % (3448572)Peak memory usage: 120 MB % 19.47/3.74 % (3448572)Instructions burned: 472 (million) % 19.47/3.74 % (3448585)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=978327546:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 19.47/3.74 % (3448584)Instruction limit reached! % 19.47/3.74 % (3448584)------------------------------ % 19.47/3.74 % (3448584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.74 % (3448584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.74 % (3448584)CaDiCaL version: 2.1.3 % 19.47/3.74 % (3448584)Termination reason: Instruction limit % 19.47/3.74 % (3448584)Termination phase: Saturation % 19.47/3.74 % (3448584)Time elapsed: 0.111 s % 19.47/3.74 % (3448584)Peak memory usage: 91 MB % 19.47/3.74 % (3448584)Instructions burned: 361 (million) % 19.47/3.74 % (3448577)Instruction limit reached! % 19.47/3.74 % (3448577)------------------------------ % 19.47/3.74 % (3448577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448577)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448577)Termination reason: Instruction limit % 24.41/4.10 % (3448577)Termination phase: Saturation % 24.41/4.10 % (3448577)Time elapsed: 0.281 s % 24.41/4.10 % (3448577)Peak memory usage: 120 MB % 24.41/4.10 % (3448577)Instructions burned: 388 (million) % 24.41/4.10 % (3448589)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3231539372:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi) % 24.41/4.10 % (3448590)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=3511825324:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi) % 24.41/4.10 % (3448592)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=292702504:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2976 on theBenchmark for (2976ds/273Mi) % 24.41/4.10 % (3448593)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=673664515:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 24.41/4.10 % (3448582)Instruction limit reached! % 24.41/4.10 % (3448582)------------------------------ % 24.41/4.10 % (3448582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448582)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448582)Termination reason: Instruction limit % 24.41/4.10 % (3448582)Termination phase: Saturation % 24.41/4.10 % (3448582)Time elapsed: 0.308 s % 24.41/4.10 % (3448582)Peak memory usage: 92 MB % 24.41/4.10 % (3448582)Instructions burned: 513 (million) % 24.41/4.10 % (3448592)Instruction limit reached! % 24.41/4.10 % (3448592)------------------------------ % 24.41/4.10 % (3448592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448592)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448592)Termination reason: Instruction limit % 24.41/4.10 % (3448592)Termination phase: Saturation % 24.41/4.10 % (3448592)Time elapsed: 0.106 s % 24.41/4.10 % (3448592)Peak memory usage: 92 MB % 24.41/4.10 % (3448592)Instructions burned: 275 (million) % 24.41/4.10 % (3448583)Instruction limit reached! % 24.41/4.10 % (3448583)------------------------------ % 24.41/4.10 % (3448583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448583)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448583)Termination reason: Instruction limit % 24.41/4.10 % (3448583)Termination phase: Saturation % 24.41/4.10 % (3448583)Time elapsed: 0.269 s % 24.41/4.10 % (3448583)Peak memory usage: 136 MB % 24.41/4.10 % (3448583)Instructions burned: 335 (million) % 24.41/4.10 % (3448589)Instruction limit reached! % 24.41/4.10 % (3448589)------------------------------ % 24.41/4.10 % (3448589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448589)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448589)Termination reason: Instruction limit % 24.41/4.10 % (3448589)Termination phase: Saturation % 24.41/4.10 % (3448589)Time elapsed: 0.169 s % 24.41/4.10 % (3448589)Peak memory usage: 118 MB % 24.41/4.10 % (3448589)Instructions burned: 262 (million) % 24.41/4.10 % (3448585)Instruction limit reached! % 24.41/4.10 % (3448585)------------------------------ % 24.41/4.10 % (3448585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448585)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448585)Termination reason: Instruction limit % 24.41/4.10 % (3448585)Termination phase: Saturation % 24.41/4.10 % (3448585)Time elapsed: 0.240 s % 24.41/4.10 % (3448585)Peak memory usage: 118 MB % 24.41/4.10 % (3448585)Instructions burned: 341 (million) % 24.41/4.10 % (3448593)Instruction limit reached! % 24.41/4.10 % (3448593)------------------------------ % 24.41/4.10 % (3448593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.41/4.10 % (3448593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.41/4.10 % (3448593)CaDiCaL version: 2.1.3 % 24.41/4.10 % (3448593)Termination reason: Instruction limit % 25.89/4.59 % (3448593)Termination phase: Saturation % 25.89/4.59 % (3448593)Time elapsed: 0.100 s % 25.89/4.59 % (3448593)Peak memory usage: 91 MB % 25.89/4.59 % (3448593)Instructions burned: 147 (million) % 25.89/4.59 % (3448590)Instruction limit reached! % 25.89/4.59 % (3448590)------------------------------ % 25.89/4.59 % (3448590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.89/4.59 % (3448590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.89/4.59 % (3448590)CaDiCaL version: 2.1.3 % 25.89/4.59 % (3448590)Termination reason: Instruction limit % 25.89/4.59 % (3448590)Termination phase: Saturation % 25.89/4.59 % (3448590)Time elapsed: 0.168 s % 25.89/4.59 % (3448590)Peak memory usage: 119 MB % 25.89/4.59 % (3448590)Instructions burned: 236 (million) % 25.89/4.59 % (3448599)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=121706161:avsq=on:i=276:avsqr=1,2:rtra=on_2974 on theBenchmark for (2974ds/276Mi) % 25.89/4.59 % (3448598)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1058729079:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 25.89/4.59 % (3448600)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2338024202:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 25.89/4.59 % (3448601)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2438963375:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 25.89/4.59 % (3448602)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2799063620:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 25.89/4.59 % (3448604)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1072241181:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi) % 25.89/4.59 % (3448599)Instruction limit reached! % 25.89/4.59 % (3448599)------------------------------ % 25.89/4.59 % (3448599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.89/4.59 % (3448599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.89/4.59 % (3448599)CaDiCaL version: 2.1.3 % 25.89/4.59 % (3448599)Termination reason: Instruction limit % 25.89/4.59 % (3448599)Termination phase: Saturation % 25.89/4.59 % (3448599)Time elapsed: 0.103 s % 25.89/4.59 % (3448599)Peak memory usage: 136 MB % 25.89/4.59 % (3448599)Instructions burned: 279 (million) % 25.89/4.59 % (3448603)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3096470701:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 25.89/4.59 % (3448603)Refutation not found, incomplete strategy % 25.89/4.59 % (3448603)------------------------------ % 25.89/4.59 % (3448603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.89/4.59 % (3448603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.89/4.59 % (3448603)CaDiCaL version: 2.1.3 % 25.89/4.59 % (3448603)Termination reason: Refutation not found, incomplete strategy % 25.89/4.59 % (3448603)Time elapsed: 0.032 s % 25.89/4.59 % (3448603)Peak memory usage: 117 MB % 25.89/4.59 % (3448603)Instructions burned: 12 (million) % 25.89/4.59 % (3448612)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 % 25.89/4.59 % (3448612)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1092041757:i=1090:aac=none:nm=0:rtra=on:rawr=on_2973 on theBenchmark for (2973ds/1090Mi) % 25.89/4.59 % (3448603)------------------------------ % 25.89/4.59 % (3448603)------------------------------ % 25.89/4.59 % (3448604)Instruction limit reached! % 25.89/4.59 % (3448604)------------------------------ % 25.89/4.59 % (3448604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.89/4.59 % (3448604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.89/4.59 % (3448604)CaDiCaL version: 2.1.3 % 25.89/4.59 % (3448604)Termination reason: Instruction limit % 25.89/4.59 % (3448604)Termination phase: Saturation % 25.89/4.59 % (3448604)Time elapsed: 0.354 s % 25.89/4.59 % (3448604)Peak memory usage: 137 MB % 25.89/4.59 % (3448604)Instructions burned: 450 (million) % 25.89/4.59 % (3448601)Instruction limit reached! % 29.69/4.97 % (3448601)------------------------------ % 29.69/4.97 % (3448601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.69/4.97 % (3448601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.69/4.97 % (3448601)CaDiCaL version: 2.1.3 % 29.69/4.97 % (3448601)Termination reason: Instruction limit % 29.69/4.97 % (3448601)Termination phase: Saturation % 29.69/4.97 % (3448601)Time elapsed: 0.439 s % 29.69/4.97 % (3448601)Peak memory usage: 94 MB % 29.69/4.97 % (3448601)Instructions burned: 656 (million) % 29.69/4.97 % (3448614)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4029330358:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2970 on theBenchmark for (2970ds/130Mi) % 29.69/4.97 % (3448612)Instruction limit reached! % 29.69/4.97 % (3448612)------------------------------ % 29.69/4.97 % (3448612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.69/4.97 % (3448612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.69/4.97 % (3448612)CaDiCaL version: 2.1.3 % 29.69/4.97 % (3448612)Termination reason: Instruction limit % 29.69/4.97 % (3448612)Termination phase: Saturation % 29.69/4.97 % (3448612)Time elapsed: 0.359 s % 29.69/4.97 % (3448612)Peak memory usage: 121 MB % 29.69/4.97 % (3448612)Instructions burned: 1093 (million) % 29.69/4.97 % (3448615)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2342884013:i=312:kws=inv_frequency:nm=20:rtra=on_2969 on theBenchmark for (2969ds/312Mi) % 29.69/4.97 % (3448617)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1800292705:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi) % 29.69/4.97 % (3448614)Instruction limit reached! % 29.69/4.97 % (3448614)------------------------------ % 29.69/4.97 % (3448614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.69/4.97 % (3448614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.69/4.97 % (3448614)CaDiCaL version: 2.1.3 % 29.69/4.97 % (3448614)Termination reason: Instruction limit % 29.69/4.97 % (3448614)Termination phase: Saturation % 29.69/4.97 % (3448614)Time elapsed: 0.122 s % 29.69/4.97 % (3448614)Peak memory usage: 118 MB % 29.69/4.97 % (3448614)Instructions burned: 131 (million) % 29.69/4.97 % (3448618)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=583278507:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 29.69/4.97 % (3448602)Instruction limit reached! % 29.69/4.97 % (3448602)------------------------------ % 29.69/4.97 % (3448602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.69/4.97 % (3448602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.69/4.97 % (3448602)CaDiCaL version: 2.1.3 % 29.69/4.97 % (3448602)Termination reason: Instruction limit % 29.69/4.97 % (3448602)Termination phase: Saturation % 29.69/4.97 % (3448602)Time elapsed: 0.654 s % 29.69/4.97 % (3448602)Peak memory usage: 92 MB % 29.69/4.97 % (3448602)Instructions burned: 1054 (million) % 29.69/4.97 % (3448621)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3814809666:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 29.69/4.97 % (3448600)Instruction limit reached! % 29.69/4.97 % (3448600)------------------------------ % 29.69/4.97 % (3448600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.69/4.97 % (3448600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.69/4.97 % (3448600)CaDiCaL version: 2.1.3 % 29.69/4.97 % (3448600)Termination reason: Instruction limit % 29.69/4.97 % (3448600)Termination phase: Saturation % 29.69/4.97 % (3448600)Time elapsed: 0.723 s % 29.69/4.97 % (3448600)Peak memory usage: 95 MB % 29.69/4.97 % (3448600)Instructions burned: 1053 (million) % 29.69/4.97 % (3448615)Instruction limit reached! % 29.69/4.97 % (3448615)------------------------------ % 29.69/4.97 % (3448615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.69/4.97 % (3448615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.69/4.97 % (3448615)CaDiCaL version: 2.1.3 % 29.69/4.97 % (3448615)Termination reason: Instruction limit % 29.69/4.97 % (3448615)Termination phase: Saturation % 29.69/4.97 % (3448615)Time elapsed: 0.227 s % 29.69/4.97 % (3448615)Peak memory usage: 120 MB % 29.69/4.97 % (3448615)Instructions burned: 312 (million) % 29.69/4.97 % (3448623)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1765942689:i=776:doe=on:rtra=on_2966 on theBenchmark for (2966ds/776Mi) % 36.36/5.91 % (3448625)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3920360181:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 36.36/5.91 % (3448626)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=978198734:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/784Mi) % 36.36/5.91 % (3448618)Instruction limit reached! % 36.36/5.91 % (3448618)------------------------------ % 36.36/5.91 % (3448618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.36/5.91 % (3448618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.36/5.91 % (3448618)CaDiCaL version: 2.1.3 % 36.36/5.91 % (3448618)Termination reason: Instruction limit % 36.36/5.91 % (3448618)Termination phase: Saturation % 36.36/5.91 % (3448618)Time elapsed: 0.281 s % 36.36/5.91 % (3448618)Peak memory usage: 96 MB % 36.36/5.91 % (3448618)Instructions burned: 838 (million) % 36.36/5.91 % (3448617)Instruction limit reached! % 36.36/5.91 % (3448617)------------------------------ % 36.36/5.91 % (3448617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.36/5.91 % (3448617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.36/5.91 % (3448617)CaDiCaL version: 2.1.3 % 36.36/5.91 % (3448617)Termination reason: Instruction limit % 36.36/5.91 % (3448617)Termination phase: Saturation % 36.36/5.91 % (3448617)Time elapsed: 0.332 s % 36.36/5.91 % (3448617)Peak memory usage: 94 MB % 36.36/5.91 % (3448617)Instructions burned: 491 (million) % 36.36/5.91 % (3448621)Instruction limit reached! % 36.36/5.91 % (3448621)------------------------------ % 36.36/5.91 % (3448621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.36/5.91 % (3448621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.36/5.91 % (3448621)CaDiCaL version: 2.1.3 % 36.36/5.91 % (3448621)Termination reason: Instruction limit % 36.36/5.91 % (3448621)Termination phase: Saturation % 36.36/5.91 % (3448621)Time elapsed: 0.208 s % 36.36/5.91 % (3448621)Peak memory usage: 91 MB % 36.36/5.91 % (3448621)Instructions burned: 307 (million) % 36.36/5.91 % (3448630)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=4235605437:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2964 on theBenchmark for (2964ds/1131Mi) % 36.36/5.91 % (3448631)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=1728112116:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/246Mi) % 36.36/5.91 % (3448632)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=798688483:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/775Mi) % 36.36/5.91 % (3448631)Instruction limit reached! % 36.36/5.91 % (3448631)------------------------------ % 36.36/5.91 % (3448631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.36/5.91 % (3448631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.36/5.91 % (3448631)CaDiCaL version: 2.1.3 % 36.36/5.91 % (3448631)Termination reason: Instruction limit % 36.36/5.91 % (3448631)Termination phase: Saturation % 36.36/5.91 % (3448631)Time elapsed: 0.177 s % 36.36/5.91 % (3448631)Peak memory usage: 119 MB % 36.36/5.91 % (3448631)Instructions burned: 248 (million) % 36.36/5.91 % (3448623)Instruction limit reached! % 36.36/5.91 % (3448623)------------------------------ % 36.36/5.91 % (3448623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.36/5.91 % (3448623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.36/5.91 % (3448623)CaDiCaL version: 2.1.3 % 36.36/5.91 % (3448623)Termination reason: Instruction limit % 36.36/5.91 % (3448623)Termination phase: Saturation % 36.36/5.91 % (3448623)Time elapsed: 0.433 s % 36.36/5.91 % (3448623)Peak memory usage: 120 MB % 36.36/5.91 % (3448623)Instructions burned: 778 (million) % 36.36/5.91 % (3448625)Instruction limit reached! % 36.36/5.91 % (3448625)------------------------------ % 36.36/5.91 % (3448625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.36/5.91 % (3448625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.36/5.91 % (3448625)CaDiCaL version: 2.1.3 % 36.36/5.91 % (3448625)Termination reason: Instruction limit % 36.36/5.91 % (3448625)Termination phase: Saturation % 49.67/7.61 % (3448625)Time elapsed: 0.465 s % 49.67/7.61 % (3448625)Peak memory usage: 138 MB % 49.67/7.61 % (3448625)Instructions burned: 646 (million) % 49.67/7.61 % (3448636)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1533690310:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 49.67/7.61 % (3448630)Instruction limit reached! % 49.67/7.61 % (3448630)------------------------------ % 49.67/7.61 % (3448630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.67/7.61 % (3448630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.67/7.61 % (3448630)CaDiCaL version: 2.1.3 % 49.67/7.61 % (3448630)Termination reason: Instruction limit % 49.67/7.61 % (3448630)Termination phase: Saturation % 49.67/7.61 % (3448630)Time elapsed: 0.398 s % 49.67/7.61 % (3448630)Peak memory usage: 126 MB % 49.67/7.61 % (3448630)Instructions burned: 1132 (million) % 49.67/7.61 % (3448637)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=493760890:i=102:nm=16:rtra=on_2960 on theBenchmark for (2960ds/102Mi) % 49.67/7.61 % (3448638)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2766691988:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2960 on theBenchmark for (2960ds/1094Mi) % 49.67/7.61 % (3448637)Instruction limit reached! % 49.67/7.61 % (3448637)------------------------------ % 49.67/7.61 % (3448637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.67/7.61 % (3448637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.67/7.61 % (3448637)CaDiCaL version: 2.1.3 % 49.67/7.61 % (3448637)Termination reason: Instruction limit % 49.67/7.61 % (3448637)Termination phase: Saturation % 49.67/7.61 % (3448637)Time elapsed: 0.068 s % 49.67/7.61 % (3448637)Peak memory usage: 89 MB % 49.67/7.61 % (3448637)Instructions burned: 102 (million) % 49.67/7.61 % (3448626)Instruction limit reached! % 49.67/7.61 % (3448626)------------------------------ % 49.67/7.61 % (3448626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.67/7.61 % (3448626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.67/7.61 % (3448626)CaDiCaL version: 2.1.3 % 49.67/7.61 % (3448626)Termination reason: Instruction limit % 49.67/7.61 % (3448626)Termination phase: Saturation % 49.67/7.61 % (3448626)Time elapsed: 0.581 s % 49.67/7.61 % (3448626)Peak memory usage: 122 MB % 49.67/7.61 % (3448626)Instructions burned: 785 (million) % 49.67/7.61 % (3448640)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=539806506:i=6400:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/6400Mi) % 49.67/7.61 % (3448636)Instruction limit reached! % 49.67/7.61 % (3448636)------------------------------ % 49.67/7.61 % (3448636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.67/7.61 % (3448636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.67/7.61 % (3448636)CaDiCaL version: 2.1.3 % 49.67/7.61 % (3448636)Termination reason: Instruction limit % 49.67/7.61 % (3448636)Termination phase: Saturation % 49.67/7.61 % (3448636)Time elapsed: 0.202 s % 49.67/7.61 % (3448636)Peak memory usage: 92 MB % 49.67/7.61 % (3448636)Instructions burned: 273 (million) % 49.67/7.61 % (3448632)Instruction limit reached! % 49.67/7.61 % (3448632)------------------------------ % 49.67/7.61 % (3448632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.67/7.61 % (3448632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.67/7.61 % (3448632)CaDiCaL version: 2.1.3 % 49.67/7.61 % (3448632)Termination reason: Instruction limit % 49.67/7.61 % (3448632)Termination phase: Saturation % 49.67/7.61 % (3448632)Time elapsed: 0.506 s % 49.67/7.61 % (3448632)Peak memory usage: 95 MB % 49.67/7.61 % (3448632)Instructions burned: 775 (million) % 49.67/7.61 % (3448643)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=1332863470:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/868Mi) % 49.67/7.61 % (3448644)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=1135626294:i=1846:canc=cautious:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/1846Mi) % 49.67/7.61 % (3448646)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2002642805:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2957 on theBenchmark for (2957ds/36816Mi) % 56.43/8.62 % (3448647)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=28500129:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 56.43/8.62 % (3448647)Instruction limit reached! % 56.43/8.62 % (3448647)------------------------------ % 56.43/8.62 % (3448647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.43/8.62 % (3448647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.43/8.62 % (3448647)CaDiCaL version: 2.1.3 % 56.43/8.62 % (3448647)Termination reason: Instruction limit % 56.43/8.62 % (3448647)Termination phase: Saturation % 56.43/8.62 % (3448647)Time elapsed: 0.186 s % 56.43/8.62 % (3448647)Peak memory usage: 94 MB % 56.43/8.62 % (3448647)Instructions burned: 274 (million) % 56.43/8.62 % (3448652)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=3242401977:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/863Mi) % 56.43/8.62 % (3448643)Instruction limit reached! % 56.43/8.62 % (3448643)------------------------------ % 56.43/8.62 % (3448643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.43/8.62 % (3448643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.43/8.62 % (3448643)CaDiCaL version: 2.1.3 % 56.43/8.62 % (3448643)Termination reason: Instruction limit % 56.43/8.62 % (3448643)Termination phase: Saturation % 56.43/8.62 % (3448643)Time elapsed: 0.513 s % 56.43/8.62 % (3448643)Peak memory usage: 120 MB % 56.43/8.62 % (3448643)Instructions burned: 868 (million) % 56.43/8.62 % (3448638)Instruction limit reached! % 56.43/8.62 % (3448638)------------------------------ % 56.43/8.62 % (3448638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.43/8.62 % (3448638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.43/8.62 % (3448638)CaDiCaL version: 2.1.3 % 56.43/8.62 % (3448638)Termination reason: Instruction limit % 56.43/8.62 % (3448638)Termination phase: Saturation % 56.43/8.62 % (3448638)Time elapsed: 0.671 s % 56.43/8.62 % (3448638)Peak memory usage: 94 MB % 56.43/8.62 % (3448638)Instructions burned: 1095 (million) % 56.43/8.62 % (3448654)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2046612064:i=5811:kws=precedence:nm=0:rtra=on_2952 on theBenchmark for (2952ds/5811Mi) % 56.43/8.62 % (3448655)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=4048688524:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 56.43/8.62 % (3448598)Instruction limit reached! % 56.43/8.62 % (3448598)------------------------------ % 56.43/8.62 % (3448598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.43/8.62 % (3448598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.43/8.62 % (3448598)CaDiCaL version: 2.1.3 % 56.43/8.62 % (3448598)Termination reason: Instruction limit % 56.43/8.62 % (3448598)Termination phase: Saturation % 56.43/8.62 % (3448598)Time elapsed: 2.472 s % 56.43/8.62 % (3448598)Peak memory usage: 111 MB % 56.43/8.62 % (3448598)Instructions burned: 4430 (million) % 56.43/8.62 % (3448652)Instruction limit reached! % 56.43/8.62 % (3448652)------------------------------ % 56.43/8.62 % (3448652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.43/8.62 % (3448652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.43/8.62 % (3448652)CaDiCaL version: 2.1.3 % 56.43/8.62 % (3448652)Termination reason: Instruction limit % 56.43/8.62 % (3448652)Termination phase: Saturation % 56.43/8.62 % (3448652)Time elapsed: 0.468 s % 56.43/8.62 % (3448652)Peak memory usage: 119 MB % 56.43/8.62 % (3448652)Instructions burned: 864 (million) % 56.43/8.62 % (3448658)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3117386752:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2949 on theBenchmark for (2949ds/801Mi) % 56.43/8.62 % (3448659)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1916268404:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2948 on theBenchmark for (2948ds/1026Mi) % 56.43/8.62 % (3448644)Instruction limit reached! % 56.43/8.62 % (3448644)------------------------------ % 56.43/8.62 % (3448644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.43/8.62 % (3448644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448644)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448644)Termination reason: Instruction limit % 90.90/13.45 % (3448644)Termination phase: Saturation % 90.90/13.45 % (3448644)Time elapsed: 1.038 s % 90.90/13.45 % (3448644)Peak memory usage: 102 MB % 90.90/13.45 % (3448644)Instructions burned: 1847 (million) % 90.90/13.45 % (3448662)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=52703716:i=3509:rtra=on_2947 on theBenchmark for (2947ds/3509Mi) % 90.90/13.45 % (3448658)Instruction limit reached! % 90.90/13.45 % (3448658)------------------------------ % 90.90/13.45 % (3448658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.90/13.45 % (3448658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448658)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448658)Termination reason: Instruction limit % 90.90/13.45 % (3448658)Termination phase: Saturation % 90.90/13.45 % (3448658)Time elapsed: 0.507 s % 90.90/13.45 % (3448658)Peak memory usage: 95 MB % 90.90/13.45 % (3448658)Instructions burned: 803 (million) % 90.90/13.45 % (3448664)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1751132056:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2942 on theBenchmark for (2942ds/2127Mi) % 90.90/13.45 % (3448659)Instruction limit reached! % 90.90/13.45 % (3448659)------------------------------ % 90.90/13.45 % (3448659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.90/13.45 % (3448659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448659)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448659)Termination reason: Instruction limit % 90.90/13.45 % (3448659)Termination phase: Saturation % 90.90/13.45 % (3448659)Time elapsed: 0.626 s % 90.90/13.45 % (3448659)Peak memory usage: 92 MB % 90.90/13.45 % (3448659)Instructions burned: 1027 (million) % 90.90/13.45 % (3448666)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1368594665:i=1959:rtra=on:fsd=on:proc=on_2941 on theBenchmark for (2941ds/1959Mi) % 90.90/13.45 % (3448640)Instruction limit reached! % 90.90/13.45 % (3448640)------------------------------ % 90.90/13.45 % (3448640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.90/13.45 % (3448640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448640)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448640)Termination reason: Instruction limit % 90.90/13.45 % (3448640)Termination phase: Saturation % 90.90/13.45 % (3448640)Time elapsed: 1.944 s % 90.90/13.45 % (3448640)Peak memory usage: 118 MB % 90.90/13.45 % (3448640)Instructions burned: 6403 (million) % 90.90/13.45 % (3448668)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2515932806:s2a=on:i=3553:nm=0:rtra=on_2939 on theBenchmark for (2939ds/3553Mi) % 90.90/13.45 % (3448655)Instruction limit reached! % 90.90/13.45 % (3448655)------------------------------ % 90.90/13.45 % (3448655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.90/13.45 % (3448655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448655)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448655)Termination reason: Instruction limit % 90.90/13.45 % (3448655)Termination phase: Saturation % 90.90/13.45 % (3448655)Time elapsed: 1.283 s % 90.90/13.45 % (3448655)Peak memory usage: 123 MB % 90.90/13.45 % (3448655)Instructions burned: 2216 (million) % 90.90/13.45 % (3448670)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1378721455:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2937 on theBenchmark for (2937ds/3201Mi) % 90.90/13.45 % (3448664)Instruction limit reached! % 90.90/13.45 % (3448664)------------------------------ % 90.90/13.45 % (3448664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.90/13.45 % (3448664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448664)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448664)Termination reason: Instruction limit % 90.90/13.45 % (3448664)Termination phase: Saturation % 90.90/13.45 % (3448664)Time elapsed: 1.029 s % 90.90/13.45 % (3448664)Peak memory usage: 90 MB % 90.90/13.45 % (3448664)Instructions burned: 2128 (million) % 90.90/13.45 % (3448662)Instruction limit reached! % 90.90/13.45 % (3448662)------------------------------ % 90.90/13.45 % (3448662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.90/13.45 % (3448662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.90/13.45 % (3448662)CaDiCaL version: 2.1.3 % 90.90/13.45 % (3448662)Termination reason: Instruction limit % 90.90/13.45 % (3448662)Termination phase: Saturation % 112.63/16.59 % (3448662)Time elapsed: 1.571 s % 112.63/16.59 % (3448662)Peak memory usage: 107 MB % 112.63/16.59 % (3448662)Instructions burned: 3511 (million) % 112.63/16.59 % (3448672)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=124866662:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2931 on theBenchmark for (2931ds/4093Mi) % 112.63/16.59 % (3448673)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=3782635340:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2930 on theBenchmark for (2930ds/21173Mi) % 112.63/16.59 % (3448666)Instruction limit reached! % 112.63/16.59 % (3448666)------------------------------ % 112.63/16.59 % (3448666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.63/16.59 % (3448666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.63/16.59 % (3448666)CaDiCaL version: 2.1.3 % 112.63/16.59 % (3448666)Termination reason: Instruction limit % 112.63/16.59 % (3448666)Termination phase: Saturation % 112.63/16.59 % (3448666)Time elapsed: 1.130 s % 112.63/16.59 % (3448666)Peak memory usage: 122 MB % 112.63/16.59 % (3448666)Instructions burned: 1961 (million) % 112.63/16.59 % (3448676)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1206372059:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2928 on theBenchmark for (2928ds/10544Mi) % 112.63/16.59 % (3448668)Instruction limit reached! % 112.63/16.59 % (3448668)------------------------------ % 112.63/16.59 % (3448668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.63/16.59 % (3448668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.63/16.59 % (3448668)CaDiCaL version: 2.1.3 % 112.63/16.59 % (3448668)Termination reason: Instruction limit % 112.63/16.59 % (3448668)Termination phase: Saturation % 112.63/16.59 % (3448668)Time elapsed: 1.224 s % 112.63/16.59 % (3448668)Peak memory usage: 107 MB % 112.63/16.59 % (3448668)Instructions burned: 3553 (million) % 112.63/16.59 % (3448678)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=41573527:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2926 on theBenchmark for (2926ds/1262Mi) % 112.63/16.59 % (3448654)Instruction limit reached! % 112.63/16.59 % (3448654)------------------------------ % 112.63/16.59 % (3448654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.63/16.59 % (3448654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.63/16.59 % (3448654)CaDiCaL version: 2.1.3 % 112.63/16.59 % (3448654)Termination reason: Instruction limit % 112.63/16.59 % (3448654)Termination phase: Saturation % 112.63/16.59 % (3448654)Time elapsed: 2.917 s % 112.63/16.59 % (3448654)Peak memory usage: 129 MB % 112.63/16.59 % (3448654)Instructions burned: 5811 (million) % 112.63/16.59 % (3448678)Instruction limit reached! % 112.63/16.59 % (3448678)------------------------------ % 112.63/16.59 % (3448678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.63/16.59 % (3448678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.63/16.59 % (3448678)CaDiCaL version: 2.1.3 % 112.63/16.59 % (3448678)Termination reason: Instruction limit % 112.63/16.59 % (3448678)Termination phase: Saturation % 112.63/16.59 % (3448678)Time elapsed: 0.373 s % 112.63/16.59 % (3448678)Peak memory usage: 123 MB % 112.63/16.59 % (3448678)Instructions burned: 1263 (million) % 112.63/16.59 % (3448670)Instruction limit reached! % 112.63/16.59 % (3448670)------------------------------ % 112.63/16.59 % (3448670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.63/16.59 % (3448670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.63/16.59 % (3448670)CaDiCaL version: 2.1.3 % 112.63/16.59 % (3448670)Termination reason: Instruction limit % 112.63/16.59 % (3448670)Termination phase: Saturation % 112.63/16.59 % (3448670)Time elapsed: 1.504 s % 112.63/16.59 % (3448670)Peak memory usage: 92 MB % 112.63/16.59 % (3448670)Instructions burned: 3202 (million) % 112.63/16.59 % (3448680)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2329945332:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2922 on theBenchmark for (2922ds/775Mi) % 112.63/16.59 % (3448682)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1917248120:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2921 on theBenchmark for (2921ds/17165Mi) % 112.63/16.59 % (3448681)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3265593490:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2921 on theBenchmark for (2921ds/270Mi) % 130.91/19.10 % (3448681)Instruction limit reached! % 130.91/19.10 % (3448681)------------------------------ % 130.91/19.10 % (3448681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.91/19.10 % (3448681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.91/19.10 % (3448681)CaDiCaL version: 2.1.3 % 130.91/19.10 % (3448681)Termination reason: Instruction limit % 130.91/19.10 % (3448681)Termination phase: Saturation % 130.91/19.10 % (3448681)Time elapsed: 0.190 s % 130.91/19.10 % (3448681)Peak memory usage: 92 MB % 130.91/19.10 % (3448681)Instructions burned: 271 (million) % 130.91/19.10 % (3448686)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3519947133:s2a=on:i=13094:s2at=-1:rtra=on_2918 on theBenchmark for (2918ds/13094Mi) % 130.91/19.10 % (3448680)Instruction limit reached! % 130.91/19.10 % (3448680)------------------------------ % 130.91/19.10 % (3448680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.91/19.10 % (3448680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.91/19.10 % (3448680)CaDiCaL version: 2.1.3 % 130.91/19.10 % (3448680)Termination reason: Instruction limit % 130.91/19.10 % (3448680)Termination phase: Saturation % 130.91/19.10 % (3448680)Time elapsed: 0.495 s % 130.91/19.10 % (3448680)Peak memory usage: 95 MB % 130.91/19.10 % (3448680)Instructions burned: 775 (million) % 130.91/19.10 % (3448688)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1780698954:st=2:i=12633:rtra=on:ss=axioms_2915 on theBenchmark for (2915ds/12633Mi) % 130.91/19.10 % (3448672)Instruction limit reached! % 130.91/19.10 % (3448672)------------------------------ % 130.91/19.10 % (3448672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.91/19.10 % (3448672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.91/19.10 % (3448672)CaDiCaL version: 2.1.3 % 130.91/19.10 % (3448672)Termination reason: Instruction limit % 130.91/19.10 % (3448672)Termination phase: Saturation % 130.91/19.10 % (3448672)Time elapsed: 1.903 s % 130.91/19.10 % (3448672)Peak memory usage: 138 MB % 130.91/19.10 % (3448672)Instructions burned: 4094 (million) % 130.91/19.10 % (3448690)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3305317892:i=1783:rtra=on:gtg=position_2910 on theBenchmark for (2910ds/1783Mi) % 130.91/19.10 % (3448690)Instruction limit reached! % 130.91/19.10 % (3448690)------------------------------ % 130.91/19.10 % (3448690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.91/19.10 % (3448690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.91/19.10 % (3448690)CaDiCaL version: 2.1.3 % 130.91/19.10 % (3448690)Termination reason: Instruction limit % 130.91/19.10 % (3448690)Termination phase: Saturation % 130.91/19.10 % (3448690)Time elapsed: 0.913 s % 130.91/19.10 % (3448690)Peak memory usage: 120 MB % 130.91/19.10 % (3448690)Instructions burned: 1785 (million) % 130.91/19.10 % (3448692)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=3193408012:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2900 on theBenchmark for (2900ds/5451Mi) % 130.91/19.10 % (3448676)Instruction limit reached! % 130.91/19.10 % (3448676)------------------------------ % 130.91/19.10 % (3448676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.91/19.10 % (3448676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.91/19.10 % (3448676)CaDiCaL version: 2.1.3 % 130.91/19.10 % (3448676)Termination reason: Instruction limit % 130.91/19.10 % (3448676)Termination phase: Saturation % 130.91/19.10 % (3448676)Time elapsed: 4.813 s % 130.91/19.10 % (3448676)Peak memory usage: 145 MB % 130.91/19.10 % (3448676)Instructions burned: 10546 (million) % 130.91/19.10 % (3448694)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=3917929477:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2879 on theBenchmark for (2879ds/4975Mi) % 130.91/19.10 % (3448692)Instruction limit reached! % 130.91/19.10 % (3448692)------------------------------ % 130.91/19.10 % (3448692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.91/19.10 % (3448692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.91/19.10 % (3448692)CaDiCaL version: 2.1.3 % 130.91/19.10 % (3448692)Termination reason: Instruction limit % 167.11/24.16 % (3448692)Termination phase: Saturation % 167.11/24.16 % (3448692)Time elapsed: 2.721 s % 167.11/24.16 % (3448692)Peak memory usage: 120 MB % 167.11/24.16 % (3448692)Instructions burned: 5452 (million) % 167.11/24.16 % (3448696)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=1694929563:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2871 on theBenchmark for (2871ds/2076Mi) % 167.11/24.16 % (3448682)Instruction limit reached! % 167.11/24.16 % (3448682)------------------------------ % 167.11/24.16 % (3448682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.11/24.16 % (3448682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/24.16 % (3448682)CaDiCaL version: 2.1.3 % 167.11/24.16 % (3448682)Termination reason: Instruction limit % 167.11/24.16 % (3448682)Termination phase: Saturation % 167.11/24.16 % (3448682)Time elapsed: 5.803 s % 167.11/24.16 % (3448682)Peak memory usage: 292 MB % 167.11/24.16 % (3448682)Instructions burned: 17166 (million) % 167.11/24.16 % (3448698)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=555974799:i=5145:rtra=on_2862 on theBenchmark for (2862ds/5145Mi) % 167.11/24.16 % (3448696)Instruction limit reached! % 167.11/24.16 % (3448696)------------------------------ % 167.11/24.16 % (3448696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.11/24.16 % (3448696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/24.16 % (3448696)CaDiCaL version: 2.1.3 % 167.11/24.16 % (3448696)Termination reason: Instruction limit % 167.11/24.16 % (3448696)Termination phase: Saturation % 167.11/24.16 % (3448696)Time elapsed: 1.141 s % 167.11/24.16 % (3448696)Peak memory usage: 121 MB % 167.11/24.16 % (3448696)Instructions burned: 2078 (million) % 167.11/24.16 % (3448700)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2054116784:i=3509:rtra=on_2858 on theBenchmark for (2858ds/3509Mi) % 167.11/24.16 % (3448694)Instruction limit reached! % 167.11/24.16 % (3448694)------------------------------ % 167.11/24.16 % (3448694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.11/24.16 % (3448694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/24.16 % (3448694)CaDiCaL version: 2.1.3 % 167.11/24.16 % (3448694)Termination reason: Instruction limit % 167.11/24.16 % (3448694)Termination phase: Saturation % 167.11/24.16 % (3448694)Time elapsed: 2.666 s % 167.11/24.16 % (3448694)Peak memory usage: 126 MB % 167.11/24.16 % (3448694)Instructions burned: 4975 (million) % 167.11/24.16 % (3448702)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1937498333:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2850 on theBenchmark for (2850ds/13800Mi) % 167.11/24.16 % (3448698)Instruction limit reached! % 167.11/24.16 % (3448698)------------------------------ % 167.11/24.16 % (3448698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.11/24.16 % (3448698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/24.16 % (3448698)CaDiCaL version: 2.1.3 % 167.11/24.16 % (3448698)Termination reason: Instruction limit % 167.11/24.16 % (3448698)Termination phase: Saturation % 167.11/24.16 % (3448698)Time elapsed: 1.732 s % 167.11/24.16 % (3448698)Peak memory usage: 111 MB % 167.11/24.16 % (3448698)Instructions burned: 5145 (million) % 167.11/24.16 % (3448704)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4081722718:i=1412:rtra=on:fsd=on:proc=on_2844 on theBenchmark for (2844ds/1412Mi) % 167.11/24.16 % (3448700)Instruction limit reached! % 167.11/24.16 % (3448700)------------------------------ % 167.11/24.16 % (3448700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.11/24.16 % (3448700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.11/24.16 % (3448700)CaDiCaL version: 2.1.3 % 167.11/24.16 % (3448700)Termination reason: Instruction limit % 167.11/24.16 % (3448700)Termination phase: Saturation % 167.11/24.16 % (3448700)Time elapsed: 1.594 s % 167.11/24.16 % (3448700)Peak memory usage: 108 MB % 167.11/24.16 % (3448700)Instructions burned: 3510 (million) % 167.11/24.16 % (3448706)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 % 167.11/24.16 % (3448706)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1673530227:i=11747:aac=none:nm=0:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/11747Mi) % 243.15/35.24 % (3448704)Instruction limit reached! % 243.15/35.24 % (3448704)------------------------------ % 243.15/35.24 % (3448704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.15/35.24 % (3448704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.15/35.24 % (3448704)CaDiCaL version: 2.1.3 % 243.15/35.24 % (3448704)Termination reason: Instruction limit % 243.15/35.24 % (3448704)Termination phase: Saturation % 243.15/35.24 % (3448704)Time elapsed: 0.413 s % 243.15/35.24 % (3448704)Peak memory usage: 120 MB % 243.15/35.24 % (3448704)Instructions burned: 1414 (million) % 243.15/35.24 % (3448708)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1334208259:s2a=on:i=3553:nm=0:rtra=on_2839 on theBenchmark for (2839ds/3553Mi) % 243.15/35.24 % (3448686)Instruction limit reached! % 243.15/35.24 % (3448686)------------------------------ % 243.15/35.24 % (3448686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.15/35.24 % (3448686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.15/35.24 % (3448686)CaDiCaL version: 2.1.3 % 243.15/35.24 % (3448686)Termination reason: Instruction limit % 243.15/35.24 % (3448686)Termination phase: Saturation % 243.15/35.24 % (3448686)Time elapsed: 7.918 s % 243.15/35.24 % (3448686)Peak memory usage: 135 MB % 243.15/35.24 % (3448686)Instructions burned: 13095 (million) % 243.15/35.24 % (3448710)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2637662116:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/3201Mi) % 243.15/35.24 % (3448688)Instruction limit reached! % 243.15/35.24 % (3448688)------------------------------ % 243.15/35.24 % (3448688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.15/35.24 % (3448688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.15/35.24 % (3448688)CaDiCaL version: 2.1.3 % 243.15/35.24 % (3448688)Termination reason: Instruction limit % 243.15/35.24 % (3448688)Termination phase: Saturation % 243.15/35.24 % (3448688)Time elapsed: 8.185 s % 243.15/35.24 % (3448688)Peak memory usage: 146 MB % 243.15/35.24 % (3448688)Instructions burned: 12634 (million) % 243.15/35.24 % (3448712)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=2414893662:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2832 on theBenchmark for (2832ds/4081Mi) % 243.15/35.24 % (3448708)Instruction limit reached! % 243.15/35.24 % (3448708)------------------------------ % 243.15/35.24 % (3448708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.15/35.24 % (3448708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.15/35.24 % (3448708)CaDiCaL version: 2.1.3 % 243.15/35.24 % (3448708)Termination reason: Instruction limit % 243.15/35.24 % (3448708)Termination phase: Saturation % 243.15/35.24 % (3448708)Time elapsed: 1.211 s % 243.15/35.24 % (3448708)Peak memory usage: 106 MB % 243.15/35.24 % (3448708)Instructions burned: 3553 (million) % 243.15/35.24 % (3448714)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=65960764:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2826 on theBenchmark for (2826ds/20260Mi) % 243.15/35.24 % (3448710)Instruction limit reached! % 243.15/35.24 % (3448710)------------------------------ % 243.15/35.24 % (3448710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.15/35.24 % (3448710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.15/35.24 % (3448710)CaDiCaL version: 2.1.3 % 243.15/35.24 % (3448710)Termination reason: Instruction limit % 243.15/35.24 % (3448710)Termination phase: Saturation % 243.15/35.24 % (3448710)Time elapsed: 1.514 s % 243.15/35.24 % (3448710)Peak memory usage: 92 MB % 243.15/35.24 % (3448710)Instructions burned: 3201 (million) % 243.15/35.24 % (3448716)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3454397167:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2821 on theBenchmark for (2821ds/58627Mi) % 243.15/35.24 % (3448673)Instruction limit reached! % 243.15/35.24 % (3448673)------------------------------ % 243.15/35.24 % (3448673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.15/35.24 % (3448673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.15/35.24 % (3448673)CaDiCaL version: 2.1.3 % 243.15/35.24 % (3448673)Termination reason: Instruction limit % 243.15/35.24 % (3448673)Termination phase: Saturation % 300.38/42.94 % (3448673)Time elapsed: 11.351 s % 300.38/42.94 % (3448673)Peak memory usage: 137 MB % 300.38/42.94 % (3448673)Instructions burned: 21173 (million) % 300.38/42.94 % (3448718)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4289214214:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/6258Mi) % 300.38/42.94 % (3448712)Instruction limit reached! % 300.38/42.94 % (3448712)------------------------------ % 300.38/42.94 % (3448712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.38/42.94 % (3448712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.38/42.94 % (3448712)CaDiCaL version: 2.1.3 % 300.38/42.94 % (3448712)Termination reason: Instruction limit % 300.38/42.94 % (3448712)Termination phase: Saturation % 300.38/42.94 % (3448712)Time elapsed: 1.975 s % 300.38/42.94 % (3448712)Peak memory usage: 139 MB % 300.38/42.94 % (3448712)Instructions burned: 4083 (million) % 300.38/42.94 % (3448720)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2226770455:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2811 on theBenchmark for (2811ds/34001Mi) % 300.38/42.94 % (3448702)Instruction limit reached! % 300.38/42.94 % (3448702)------------------------------ % 300.38/42.94 % (3448702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.38/42.94 % (3448702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.38/42.94 % (3448702)CaDiCaL version: 2.1.3 % 300.38/42.94 % (3448702)Termination reason: Instruction limit % 300.38/42.94 % (3448702)Termination phase: Saturation % 300.38/42.94 % (3448702)Time elapsed: 6.282 s % 300.38/42.94 % (3448702)Peak memory usage: 92 MB % 300.38/42.94 % (3448702)Instructions burned: 13802 (million) % 300.38/42.94 % (3448722)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=978260327:s2a=on:i=71622:s2at=-1:rtra=on_2786 on theBenchmark for (2786ds/71622Mi) % 300.38/42.94 % (3448718)Instruction limit reached! % 300.38/42.94 % (3448718)------------------------------ % 300.38/42.94 % (3448718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.38/42.94 % (3448718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.38/42.94 % (3448718)CaDiCaL version: 2.1.3 % 300.38/42.94 % (3448718)Termination reason: Instruction limit % 300.38/42.94 % (3448718)Termination phase: Saturation % 300.38/42.94 % (3448718)Time elapsed: 3.416 s % 300.38/42.94 % (3448718)Peak memory usage: 129 MB % 300.38/42.94 % (3448718)Instructions burned: 6259 (million) % 300.38/42.94 % (3448724)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2044531378:i=24001:kws=precedence:nm=0:rtra=on_2779 on theBenchmark for (2779ds/24001Mi) % 300.38/42.94 % (3448706)Instruction limit reached! % 300.38/42.94 % (3448706)------------------------------ % 300.38/42.94 % (3448706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.38/42.94 % (3448706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.38/42.94 % (3448706)CaDiCaL version: 2.1.3 % 300.38/42.94 % (3448706)Termination reason: Instruction limit % 300.38/42.94 % (3448706)Termination phase: Saturation % 300.38/42.94 % (3448706)Time elapsed: 6.384 s % 300.38/42.94 % (3448706)Peak memory usage: 131 MB % 300.38/42.94 % (3448706)Instructions burned: 11749 (million) % 300.38/42.94 % (3448726)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=3064753433:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2776 on theBenchmark for (2776ds/2076Mi) % 300.38/42.94 % (3448714)Instruction limit reached! % 300.38/42.94 % (3448714)------------------------------ % 300.38/42.94 % (3448714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.38/42.94 % (3448714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.38/42.94 % (3448714)CaDiCaL version: 2.1.3 % 300.38/42.94 % (3448714)Termination reason: Instruction limit % 300.38/42.94 % (3448714)Termination phase: Saturation % 300.38/42.94 % (3448714)Time elapsed: 5.606 s % 300.38/42.94 % (3448714)Peak memory usage: 138 MB % 300.38/42.94 % (3448714)Instructions burned: 20261 (million) % 300.38/42.94 % (3448728)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1741532899:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2769 on theBenchmark for (2769ds/83971Mi) % 300.38/42.94 % (3448726)Instruction limit reached! % 300.38/42.94 % (3448726)------------------------------ % 300.38/42.94 % (3448726)Version: Vampire 5.0.1 (Release build, commit ea896 % 300.38/42.94 Terminated %------------------------------------------------------------------------------