%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX085_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 : n020.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:51 PM UTC 2026 % Result : Timeout 295.90s 42.31s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX085_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.08/0.17 % Computer : n020.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 15:01:19 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 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.76/1.21 % (225020)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.76/1.21 % (225027)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1606900905:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.76/1.21 % (225026)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=185198854:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.76/1.21 % (225029)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1075673646:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.76/1.21 % (225028)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2059105704:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.76/1.21 % (225025)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2635141113:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.76/1.21 % (225031)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=934472503:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.76/1.21 % (225029)Instruction limit reached! % 3.76/1.21 % (225029)------------------------------ % 3.76/1.21 % (225029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.76/1.21 % (225029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/1.21 % (225029)CaDiCaL version: 2.1.3 % 3.76/1.21 % (225029)Termination reason: Instruction limit % 3.76/1.21 % (225029)Termination phase: Saturation % 3.76/1.21 % (225029)Time elapsed: 0.004 s % 3.76/1.21 % (225029)Peak memory usage: 88 MB % 3.76/1.21 % (225029)Instructions burned: 5 (million) % 3.76/1.21 % (225028)Instruction limit reached! % 3.76/1.21 % (225028)------------------------------ % 3.76/1.21 % (225028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.76/1.21 % (225028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/1.21 % (225028)CaDiCaL version: 2.1.3 % 3.76/1.21 % (225028)Termination reason: Instruction limit % 3.76/1.21 % (225028)Termination phase: Saturation % 3.76/1.21 % (225028)Time elapsed: 0.005 s % 3.76/1.21 % (225028)Peak memory usage: 88 MB % 3.76/1.21 % (225028)Instructions burned: 7 (million) % 3.76/1.21 % (225030)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=253560100:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.76/1.21 % (225025)Instruction limit reached! % 3.76/1.21 % (225025)------------------------------ % 3.76/1.21 % (225025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.76/1.21 % (225025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/1.21 % (225025)CaDiCaL version: 2.1.3 % 3.76/1.21 % (225025)Termination reason: Instruction limit % 3.76/1.21 % (225025)Termination phase: Saturation % 3.76/1.21 % (225025)Time elapsed: 0.031 s % 3.76/1.21 % (225025)Peak memory usage: 115 MB % 3.76/1.21 % (225025)Instructions burned: 12 (million) % 3.76/1.21 % (225027)Instruction limit reached! % 3.76/1.21 % (225027)------------------------------ % 3.76/1.21 % (225027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.76/1.21 % (225027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/1.21 % (225027)CaDiCaL version: 2.1.3 % 3.76/1.21 % (225027)Termination reason: Instruction limit % 3.76/1.21 % (225027)Termination phase: Saturation % 3.76/1.21 % (225027)Time elapsed: 0.069 s % 3.76/1.21 % (225027)Peak memory usage: 116 MB % 3.76/1.21 % (225027)Instructions burned: 203 (million) % 3.76/1.21 % (225031)Instruction limit reached! % 3.76/1.21 % (225031)------------------------------ % 3.76/1.21 % (225031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.76/1.21 % (225031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/1.21 % (225031)CaDiCaL version: 2.1.3 % 3.76/1.21 % (225031)Termination reason: Instruction limit % 3.76/1.21 % (225031)Termination phase: Saturation % 3.76/1.21 % (225031)Time elapsed: 0.046 s % 3.76/1.21 % (225031)Peak memory usage: 115 MB % 3.76/1.21 % (225031)Instructions burned: 33 (million) % 3.76/1.21 % (225030)Instruction limit reached! % 3.76/1.21 % (225030)------------------------------ % 3.76/1.21 % (225030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.76/1.21 % (225030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.76/1.21 % (225030)CaDiCaL version: 2.1.3 % 3.76/1.21 % (225030)Termination reason: Instruction limit % 4.48/1.37 % (225030)Termination phase: Saturation % 4.48/1.37 % (225030)Time elapsed: 0.055 s % 4.48/1.37 % (225030)Peak memory usage: 115 MB % 4.48/1.37 % (225030)Instructions burned: 46 (million) % 4.48/1.37 % (225039)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=3234390327:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.48/1.37 % (225038)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1544170905:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.48/1.37 % (225038)Instruction limit reached! % 4.48/1.37 % (225038)------------------------------ % 4.48/1.37 % (225038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.48/1.37 % (225042)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2024045118:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.48/1.37 % (225038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/1.37 % (225038)CaDiCaL version: 2.1.3 % 4.48/1.37 % (225038)Termination reason: Instruction limit % 4.48/1.37 % (225038)Termination phase: Saturation % 4.48/1.37 % (225038)Time elapsed: 0.011 s % 4.48/1.37 % (225038)Peak memory usage: 88 MB % 4.48/1.37 % (225038)Instructions burned: 15 (million) % 4.48/1.37 % (225041)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3063840325:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.48/1.37 % (225042)Instruction limit reached! % 4.48/1.37 % (225042)------------------------------ % 4.48/1.37 % (225042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.48/1.37 % (225042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/1.37 % (225042)CaDiCaL version: 2.1.3 % 4.48/1.37 % (225042)Termination reason: Instruction limit % 4.48/1.37 % (225042)Termination phase: Saturation % 4.48/1.37 % (225042)Time elapsed: 0.010 s % 4.48/1.37 % (225042)Peak memory usage: 89 MB % 4.48/1.37 % (225042)Instructions burned: 26 (million) % 4.48/1.37 % (225039)Instruction limit reached! % 4.48/1.37 % (225039)------------------------------ % 4.48/1.37 % (225039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.48/1.37 % (225039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/1.37 % (225039)CaDiCaL version: 2.1.3 % 4.48/1.37 % (225039)Termination reason: Instruction limit % 4.48/1.37 % (225039)Termination phase: Saturation % 4.48/1.37 % (225039)Time elapsed: 0.023 s % 4.48/1.37 % (225039)Peak memory usage: 88 MB % 4.48/1.37 % (225039)Instructions burned: 29 (million) % 4.48/1.37 % (225041)Instruction limit reached! % 4.48/1.37 % (225041)------------------------------ % 4.48/1.37 % (225041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.48/1.37 % (225041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/1.37 % (225041)CaDiCaL version: 2.1.3 % 4.48/1.37 % (225041)Termination reason: Instruction limit % 4.48/1.37 % (225041)Termination phase: Saturation % 4.48/1.37 % (225041)Time elapsed: 0.010 s % 4.48/1.37 % (225041)Peak memory usage: 90 MB % 4.48/1.37 % (225041)Instructions burned: 16 (million) % 4.48/1.37 % (225043)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=1060054609:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.48/1.37 % (225043)Instruction limit reached! % 4.48/1.37 % (225043)------------------------------ % 4.48/1.37 % (225043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.48/1.37 % (225043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/1.37 % (225043)CaDiCaL version: 2.1.3 % 4.48/1.37 % (225043)Termination reason: Instruction limit % 4.48/1.37 % (225043)Termination phase: Saturation % 4.48/1.37 % (225043)Time elapsed: 0.017 s % 4.48/1.37 % (225043)Peak memory usage: 89 MB % 4.48/1.37 % (225043)Instructions burned: 27 (million) % 4.48/1.37 % (225026)Instruction limit reached! % 4.48/1.37 % (225026)------------------------------ % 4.48/1.37 % (225026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.48/1.37 % (225026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/1.37 % (225026)CaDiCaL version: 2.1.3 % 4.48/1.37 % (225026)Termination reason: Instruction limit % 4.48/1.37 % (225026)Termination phase: Saturation % 5.64/1.55 % (225026)Time elapsed: 0.233 s % 5.64/1.55 % (225026)Peak memory usage: 116 MB % 5.64/1.55 % (225026)Instructions burned: 308 (million) % 5.64/1.55 % (225044)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=459823149:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.64/1.55 % (225051)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3397129252:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.64/1.55 % (225051)Instruction limit reached! % 5.64/1.55 % (225051)------------------------------ % 5.64/1.55 % (225051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.55 % (225051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.55 % (225051)CaDiCaL version: 2.1.3 % 5.64/1.55 % (225051)Termination reason: Instruction limit % 5.64/1.55 % (225051)Termination phase: Saturation % 5.64/1.55 % (225051)Time elapsed: 0.002 s % 5.64/1.55 % (225051)Peak memory usage: 88 MB % 5.64/1.55 % (225051)Instructions burned: 4 (million) % 5.64/1.55 % (225044)Instruction limit reached! % 5.64/1.55 % (225044)------------------------------ % 5.64/1.55 % (225044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.55 % (225044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.55 % (225044)CaDiCaL version: 2.1.3 % 5.64/1.55 % (225044)Termination reason: Instruction limit % 5.64/1.55 % (225044)Termination phase: Saturation % 5.64/1.55 % (225044)Time elapsed: 0.048 s % 5.64/1.55 % (225044)Peak memory usage: 89 MB % 5.64/1.55 % (225044)Instructions burned: 86 (million) % 5.64/1.55 % (225050)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1796865723:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.64/1.55 % (225049)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4141517358:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.64/1.55 % (225052)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=7747781:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.64/1.55 % (225049)Instruction limit reached! % 5.64/1.55 % (225049)------------------------------ % 5.64/1.55 % (225049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.55 % (225049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.55 % (225049)CaDiCaL version: 2.1.3 % 5.64/1.55 % (225049)Termination reason: Instruction limit % 5.64/1.55 % (225049)Termination phase: Saturation % 5.64/1.55 % (225049)Time elapsed: 0.002 s % 5.64/1.55 % (225049)Peak memory usage: 87 MB % 5.64/1.55 % (225049)Instructions burned: 2 (million) % 5.64/1.55 % (225054)lrs+10_1_thi=all:si=on:fd=off:random_seed=350965281:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.64/1.55 % (225056)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=2301439907:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 5.64/1.55 % (225058)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3465530432:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 5.64/1.55 % (225058)Instruction limit reached! % 5.64/1.55 % (225058)------------------------------ % 5.64/1.55 % (225058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.55 % (225058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.55 % (225058)CaDiCaL version: 2.1.3 % 5.64/1.55 % (225058)Termination reason: Instruction limit % 5.64/1.55 % (225058)Termination phase: Saturation % 5.64/1.55 % (225058)Time elapsed: 0.001 s % 5.64/1.55 % (225058)Peak memory usage: 88 MB % 5.64/1.55 % (225058)Instructions burned: 2 (million) % 5.64/1.55 % (225056)Instruction limit reached! % 5.64/1.55 % (225056)------------------------------ % 5.64/1.55 % (225056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.55 % (225056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.55 % (225056)CaDiCaL version: 2.1.3 % 5.64/1.55 % (225056)Termination reason: Instruction limit % 5.64/1.55 % (225056)Termination phase: Saturation % 5.64/1.55 % (225056)Time elapsed: 0.006 s % 5.64/1.55 % (225056)Peak memory usage: 88 MB % 5.64/1.55 % (225056)Instructions burned: 8 (million) % 5.64/1.55 % (225052)Instruction limit reached! % 5.64/1.55 % (225052)------------------------------ % 6.84/1.79 % (225052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225052)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225052)Termination reason: Instruction limit % 6.84/1.79 % (225052)Termination phase: Saturation % 6.84/1.79 % (225052)Time elapsed: 0.097 s % 6.84/1.79 % (225052)Peak memory usage: 134 MB % 6.84/1.79 % (225052)Instructions burned: 66 (million) % 6.84/1.79 % (225054)Instruction limit reached! % 6.84/1.79 % (225054)------------------------------ % 6.84/1.79 % (225054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225054)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225054)Termination reason: Instruction limit % 6.84/1.79 % (225054)Termination phase: Saturation % 6.84/1.79 % (225054)Time elapsed: 0.066 s % 6.84/1.79 % (225054)Peak memory usage: 117 MB % 6.84/1.79 % (225054)Instructions burned: 54 (million) % 6.84/1.79 % (225050)Instruction limit reached! % 6.84/1.79 % (225050)------------------------------ % 6.84/1.79 % (225050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225050)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225050)Termination reason: Instruction limit % 6.84/1.79 % (225050)Termination phase: Saturation % 6.84/1.79 % (225050)Time elapsed: 0.114 s % 6.84/1.79 % (225050)Peak memory usage: 89 MB % 6.84/1.79 % (225050)Instructions burned: 182 (million) % 6.84/1.79 % (225059)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2417113239:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.84/1.79 % (225059)Instruction limit reached! % 6.84/1.79 % (225059)------------------------------ % 6.84/1.79 % (225059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225059)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225059)Termination reason: Instruction limit % 6.84/1.79 % (225059)Termination phase: Saturation % 6.84/1.79 % (225059)Time elapsed: 0.002 s % 6.84/1.79 % (225059)Peak memory usage: 87 MB % 6.84/1.79 % (225059)Instructions burned: 2 (million) % 6.84/1.79 % (225063)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2876608372:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.84/1.79 % (225068)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=507247626:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.84/1.79 % (225068)Refutation not found, incomplete strategy % 6.84/1.79 % (225068)------------------------------ % 6.84/1.79 % (225068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225068)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225068)Termination reason: Refutation not found, incomplete strategy % 6.84/1.79 % (225068)Time elapsed: 0.002 s % 6.84/1.79 % (225068)Peak memory usage: 89 MB % 6.84/1.79 % (225068)Instructions burned: 4 (million) % 6.84/1.79 % (225067)dis+10_1_si=on:random_seed=3210180810:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.84/1.79 % (225063)Instruction limit reached! % 6.84/1.79 % (225063)------------------------------ % 6.84/1.79 % (225063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225063)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225063)Termination reason: Instruction limit % 6.84/1.79 % (225063)Termination phase: Saturation % 6.84/1.79 % (225063)Time elapsed: 0.093 s % 6.84/1.79 % (225063)Peak memory usage: 116 MB % 6.84/1.79 % (225063)Instructions burned: 127 (million) % 6.84/1.79 % (225067)Instruction limit reached! % 6.84/1.79 % (225067)------------------------------ % 6.84/1.79 % (225067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.84/1.79 % (225067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.84/1.79 % (225067)CaDiCaL version: 2.1.3 % 6.84/1.79 % (225067)Termination reason: Instruction limit % 6.84/1.79 % (225067)Termination phase: Saturation % 6.84/1.79 % (225067)Time elapsed: 0.009 s % 6.84/1.79 % (225067)Peak memory usage: 88 MB % 6.84/1.79 % (225067)Instructions burned: 11 (million) % 6.84/1.79 % (225070)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3906473964:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 10.15/2.08 % (225069)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=229583982: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) % 10.15/2.08 % (225070)Instruction limit reached! % 10.15/2.08 % (225070)------------------------------ % 10.15/2.08 % (225070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.08 % (225070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.08 % (225070)CaDiCaL version: 2.1.3 % 10.15/2.08 % (225070)Termination reason: Instruction limit % 10.15/2.08 % (225070)Termination phase: Saturation % 10.15/2.08 % (225070)Time elapsed: 0.002 s % 10.15/2.08 % (225070)Peak memory usage: 88 MB % 10.15/2.08 % (225070)Instructions burned: 2 (million) % 10.15/2.08 % (225071)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=35502438:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 10.15/2.08 % (225071)Instruction limit reached! % 10.15/2.08 % (225071)------------------------------ % 10.15/2.08 % (225071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.08 % (225071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.08 % (225071)CaDiCaL version: 2.1.3 % 10.15/2.08 % (225071)Termination reason: Instruction limit % 10.15/2.08 % (225071)Termination phase: Saturation % 10.15/2.08 % (225071)Time elapsed: 0.007 s % 10.15/2.08 % (225071)Peak memory usage: 88 MB % 10.15/2.08 % (225071)Instructions burned: 9 (million) % 10.15/2.08 % (225073)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2198287662:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 10.15/2.08 % (225069)Instruction limit reached! % 10.15/2.08 % (225069)------------------------------ % 10.15/2.08 % (225069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.08 % (225069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.08 % (225069)CaDiCaL version: 2.1.3 % 10.15/2.08 % (225069)Termination reason: Instruction limit % 10.15/2.08 % (225069)Termination phase: Saturation % 10.15/2.08 % (225069)Time elapsed: 0.029 s % 10.15/2.08 % (225069)Peak memory usage: 89 MB % 10.15/2.08 % (225069)Instructions burned: 35 (million) % 10.15/2.08 % (225068)------------------------------ % 10.15/2.08 % (225068)------------------------------ % 10.15/2.08 % (225077)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2570185176:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 10.15/2.08 % (225078)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1529716819:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 10.15/2.08 % (225081)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3384020324:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 10.15/2.08 % (225081)Instruction limit reached! % 10.15/2.08 % (225081)------------------------------ % 10.15/2.08 % (225081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.08 % (225081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.08 % (225081)CaDiCaL version: 2.1.3 % 10.15/2.08 % (225081)Termination reason: Instruction limit % 10.15/2.08 % (225081)Termination phase: Saturation % 10.15/2.08 % (225081)Time elapsed: 0.009 s % 10.15/2.08 % (225081)Peak memory usage: 88 MB % 10.15/2.08 % (225081)Instructions burned: 11 (million) % 10.15/2.08 % (225085)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=1646898529:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 10.15/2.08 % (225084)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2299907667:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 10.15/2.08 % (225078)Refutation not found, incomplete strategy % 10.15/2.08 % (225078)------------------------------ % 10.15/2.08 % (225078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.15/2.08 % (225078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.15/2.08 % (225078)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225078)Termination reason: Refutation not found, incomplete strategy % 11.32/2.33 % (225078)Time elapsed: 0.028 s % 11.32/2.33 % (225078)Peak memory usage: 112 MB % 11.32/2.33 % (225078)Instructions burned: 7 (million) % 11.32/2.33 % (225077)Instruction limit reached! % 11.32/2.33 % (225077)------------------------------ % 11.32/2.33 % (225077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.33 % (225077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.33 % (225077)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225077)Termination reason: Instruction limit % 11.32/2.33 % (225077)Termination phase: Saturation % 11.32/2.33 % (225077)Time elapsed: 0.033 s % 11.32/2.33 % (225077)Peak memory usage: 115 MB % 11.32/2.33 % (225077)Instructions burned: 14 (million) % 11.32/2.33 % (225086)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=3758360197:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi) % 11.32/2.33 % (225085)Instruction limit reached! % 11.32/2.33 % (225085)------------------------------ % 11.32/2.33 % (225085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.33 % (225085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.33 % (225085)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225085)Termination reason: Instruction limit % 11.32/2.33 % (225085)Termination phase: Saturation % 11.32/2.33 % (225085)Time elapsed: 0.057 s % 11.32/2.33 % (225085)Peak memory usage: 90 MB % 11.32/2.33 % (225085)Instructions burned: 75 (million) % 11.32/2.33 % (225073)Instruction limit reached! % 11.32/2.33 % (225073)------------------------------ % 11.32/2.33 % (225073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.33 % (225073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.33 % (225073)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225073)Termination reason: Instruction limit % 11.32/2.33 % (225073)Termination phase: Saturation % 11.32/2.33 % (225073)Time elapsed: 0.222 s % 11.32/2.33 % (225073)Peak memory usage: 94 MB % 11.32/2.33 % (225073)Instructions burned: 370 (million) % 11.32/2.33 % (225084)Instruction limit reached! % 11.32/2.33 % (225084)------------------------------ % 11.32/2.33 % (225084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.33 % (225084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.33 % (225084)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225084)Termination reason: Instruction limit % 11.32/2.33 % (225084)Termination phase: Saturation % 11.32/2.33 % (225084)Time elapsed: 0.095 s % 11.32/2.33 % (225084)Peak memory usage: 133 MB % 11.32/2.33 % (225084)Instructions burned: 71 (million) % 11.32/2.33 % (225090)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3575836017:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi) % 11.32/2.33 % (225086)Instruction limit reached! % 11.32/2.33 % (225086)------------------------------ % 11.32/2.33 % (225086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.33 % (225086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.33 % (225086)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225086)Termination reason: Instruction limit % 11.32/2.33 % (225086)Termination phase: Saturation % 11.32/2.33 % (225086)Time elapsed: 0.102 s % 11.32/2.33 % (225086)Peak memory usage: 90 MB % 11.32/2.33 % (225086)Instructions burned: 296 (million) % 11.32/2.33 % (225093)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1472569056:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.32/2.33 % (225095)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=4277864210:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 11.32/2.33 % (225096)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1498478040:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 11.32/2.33 % (225090)Instruction limit reached! % 11.32/2.33 % (225090)------------------------------ % 11.32/2.33 % (225090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.33 % (225090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.33 % (225090)CaDiCaL version: 2.1.3 % 11.32/2.33 % (225090)Termination reason: Instruction limit % 11.32/2.33 % (225090)Termination phase: Saturation % 11.32/2.33 % (225090)Time elapsed: 0.103 s % 11.32/2.33 % (225090)Peak memory usage: 116 MB % 11.32/2.33 % (225090)Instructions burned: 131 (million) % 13.08/2.66 % (225078)------------------------------ % 13.08/2.66 % (225078)------------------------------ % 13.08/2.66 % (225097)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=804209938:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 13.08/2.66 % (225099)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=24450909:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 13.08/2.66 % (225095)Instruction limit reached! % 13.08/2.66 % (225095)------------------------------ % 13.08/2.66 % (225095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.08/2.66 % (225095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.08/2.66 % (225095)CaDiCaL version: 2.1.3 % 13.08/2.66 % (225095)Termination reason: Instruction limit % 13.08/2.66 % (225095)Termination phase: Saturation % 13.08/2.66 % (225095)Time elapsed: 0.070 s % 13.08/2.66 % (225095)Peak memory usage: 133 MB % 13.08/2.66 % (225095)Instructions burned: 40 (million) % 13.08/2.66 % (225093)Instruction limit reached! % 13.08/2.66 % (225093)------------------------------ % 13.08/2.66 % (225093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.08/2.66 % (225093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.08/2.66 % (225093)CaDiCaL version: 2.1.3 % 13.08/2.66 % (225093)Termination reason: Instruction limit % 13.08/2.66 % (225093)Termination phase: Saturation % 13.08/2.66 % (225093)Time elapsed: 0.138 s % 13.08/2.66 % (225093)Peak memory usage: 133 MB % 13.08/2.66 % (225093)Instructions burned: 132 (million) % 13.08/2.66 % (225099)Instruction limit reached! % 13.08/2.66 % (225099)------------------------------ % 13.08/2.66 % (225099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.08/2.66 % (225099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.08/2.66 % (225099)CaDiCaL version: 2.1.3 % 13.08/2.66 % (225099)Termination reason: Instruction limit % 13.08/2.66 % (225099)Termination phase: Saturation % 13.08/2.66 % (225099)Time elapsed: 0.058 s % 13.08/2.66 % (225099)Peak memory usage: 118 MB % 13.08/2.66 % (225099)Instructions burned: 134 (million) % 13.08/2.66 % (225103)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=1505057329:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi) % 13.08/2.66 % (225104)dis+10_1_si=on:random_seed=4292442585:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi) % 13.08/2.66 % (225096)Instruction limit reached! % 13.08/2.66 % (225096)------------------------------ % 13.08/2.66 % (225096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.08/2.66 % (225096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.08/2.66 % (225096)CaDiCaL version: 2.1.3 % 13.08/2.66 % (225096)Termination reason: Instruction limit % 13.08/2.66 % (225096)Termination phase: Saturation % 13.08/2.66 % (225096)Time elapsed: 0.172 s % 13.08/2.66 % (225096)Peak memory usage: 90 MB % 13.08/2.66 % (225096)Instructions burned: 309 (million) % 13.08/2.66 % (225107)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1895212443:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 13.08/2.66 % (225109)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1195860692:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 13.08/2.66 % (225108)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3983901461:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi) % 13.08/2.66 % (225109)Refutation not found, incomplete strategy % 13.08/2.66 % (225109)------------------------------ % 13.08/2.66 % (225109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.08/2.66 % (225109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.08/2.66 % (225109)CaDiCaL version: 2.1.3 % 13.08/2.66 % (225109)Termination reason: Refutation not found, incomplete strategy % 13.08/2.66 % (225109)Time elapsed: 0.017 s % 13.08/2.66 % (225109)Peak memory usage: 112 MB % 13.08/2.66 % (225109)Instructions burned: 8 (million) % 13.08/2.66 % (225108)Instruction limit reached! % 13.08/2.66 % (225108)------------------------------ % 13.08/2.66 % (225108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.08/2.66 % (225108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.66/2.87 % (225108)CaDiCaL version: 2.1.3 % 14.66/2.87 % (225108)Termination reason: Instruction limit % 14.66/2.87 % (225108)Termination phase: Saturation % 14.66/2.87 % (225108)Time elapsed: 0.091 s % 14.66/2.87 % (225108)Peak memory usage: 90 MB % 14.66/2.87 % (225108)Instructions burned: 142 (million) % 14.66/2.87 % (225103)Instruction limit reached! % 14.66/2.87 % (225103)------------------------------ % 14.66/2.87 % (225103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.66/2.87 % (225103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.66/2.87 % (225103)CaDiCaL version: 2.1.3 % 14.66/2.87 % (225103)Termination reason: Instruction limit % 14.66/2.87 % (225103)Termination phase: Saturation % 14.66/2.87 % (225103)Time elapsed: 0.159 s % 14.66/2.87 % (225103)Peak memory usage: 116 MB % 14.66/2.87 % (225103)Instructions burned: 260 (million) % 14.66/2.87 % (225112)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=794262384:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi) % 14.66/2.87 % (225109)------------------------------ % 14.66/2.87 % (225109)------------------------------ % 14.66/2.87 % (225112)Instruction limit reached! % 14.66/2.87 % (225112)------------------------------ % 14.66/2.87 % (225112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.66/2.87 % (225112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.66/2.87 % (225112)CaDiCaL version: 2.1.3 % 14.66/2.87 % (225112)Termination reason: Instruction limit % 14.66/2.87 % (225112)Termination phase: Saturation % 14.66/2.87 % (225112)Time elapsed: 0.071 s % 14.66/2.87 % (225112)Peak memory usage: 89 MB % 14.66/2.87 % (225112)Instructions burned: 121 (million) % 14.66/2.87 % (225107)Instruction limit reached! % 14.66/2.87 % (225107)------------------------------ % 14.66/2.87 % (225107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.66/2.87 % (225107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.66/2.87 % (225107)CaDiCaL version: 2.1.3 % 14.66/2.87 % (225107)Termination reason: Instruction limit % 14.66/2.87 % (225107)Termination phase: Saturation % 14.66/2.87 % (225107)Time elapsed: 0.227 s % 14.66/2.87 % (225107)Peak memory usage: 91 MB % 14.66/2.87 % (225107)Instructions burned: 384 (million) % 14.66/2.87 % (225097)Instruction limit reached! % 14.66/2.87 % (225097)------------------------------ % 14.66/2.87 % (225097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.66/2.87 % (225097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.66/2.87 % (225097)CaDiCaL version: 2.1.3 % 14.66/2.87 % (225097)Termination reason: Instruction limit % 14.66/2.87 % (225097)Termination phase: Saturation % 14.66/2.87 % (225097)Time elapsed: 0.418 s % 14.66/2.87 % (225097)Peak memory usage: 138 MB % 14.66/2.87 % (225097)Instructions burned: 600 (million) % 14.66/2.87 % (225116)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=2279505417:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi) % 14.66/2.87 % (225117)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=2947504523:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi) % 14.66/2.87 % (225119)dis+1010_1_to=kbo:si=on:random_seed=640685388:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi) % 14.66/2.87 % (225117)Instruction limit reached! % 14.66/2.87 % (225117)------------------------------ % 14.66/2.87 % (225117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.66/2.87 % (225117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.66/2.87 % (225117)CaDiCaL version: 2.1.3 % 14.66/2.87 % (225117)Termination reason: Instruction limit % 14.66/2.87 % (225117)Termination phase: Saturation % 14.66/2.87 % (225117)Time elapsed: 0.048 s % 14.66/2.87 % (225117)Peak memory usage: 115 MB % 14.66/2.87 % (225117)Instructions burned: 40 (million) % 14.66/2.87 % (225120)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=267972284:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi) % 14.66/2.87 % (225119)Instruction limit reached! % 14.66/2.87 % (225119)------------------------------ % 14.66/2.87 % (225119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.66/2.87 % (225119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.99/3.28 % (225119)CaDiCaL version: 2.1.3 % 17.99/3.28 % (225119)Termination reason: Instruction limit % 17.99/3.28 % (225119)Termination phase: Saturation % 17.99/3.28 % (225119)Time elapsed: 0.065 s % 17.99/3.28 % (225119)Peak memory usage: 90 MB % 17.99/3.28 % (225119)Instructions burned: 176 (million) % 17.99/3.28 % (225116)Instruction limit reached! % 17.99/3.28 % (225116)------------------------------ % 17.99/3.28 % (225116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.99/3.28 % (225116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.99/3.28 % (225116)CaDiCaL version: 2.1.3 % 17.99/3.28 % (225116)Termination reason: Instruction limit % 17.99/3.28 % (225116)Termination phase: Saturation % 17.99/3.28 % (225116)Time elapsed: 0.098 s % 17.99/3.28 % (225116)Peak memory usage: 117 MB % 17.99/3.28 % (225116)Instructions burned: 128 (million) % 17.99/3.28 % (225121)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2318494773:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 17.99/3.28 % (225122)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3852535455:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi) % 17.99/3.28 % (225126)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=268782990:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi) % 17.99/3.28 % (225128)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3026081833:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi) % 17.99/3.28 % (225129)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=624437992:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi) % 17.99/3.28 % (225120)Instruction limit reached! % 17.99/3.28 % (225120)------------------------------ % 17.99/3.28 % (225120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.99/3.28 % (225120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.99/3.28 % (225120)CaDiCaL version: 2.1.3 % 17.99/3.28 % (225120)Termination reason: Instruction limit % 17.99/3.28 % (225120)Termination phase: Saturation % 17.99/3.28 % (225120)Time elapsed: 0.180 s % 17.99/3.28 % (225120)Peak memory usage: 116 MB % 17.99/3.28 % (225120)Instructions burned: 329 (million) % 17.99/3.28 % (225128)Instruction limit reached! % 17.99/3.28 % (225128)------------------------------ % 17.99/3.28 % (225128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.99/3.28 % (225128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.99/3.28 % (225128)CaDiCaL version: 2.1.3 % 17.99/3.28 % (225128)Termination reason: Instruction limit % 17.99/3.28 % (225128)Termination phase: Saturation % 17.99/3.28 % (225128)Time elapsed: 0.079 s % 17.99/3.28 % (225128)Peak memory usage: 89 MB % 17.99/3.28 % (225128)Instructions burned: 298 (million) % 17.99/3.28 % (225104)Instruction limit reached! % 17.99/3.28 % (225104)------------------------------ % 17.99/3.28 % (225104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.99/3.28 % (225104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.99/3.28 % (225104)CaDiCaL version: 2.1.3 % 17.99/3.28 % (225104)Termination reason: Instruction limit % 17.99/3.28 % (225104)Termination phase: Saturation % 17.99/3.28 % (225104)Time elapsed: 0.586 s % 17.99/3.28 % (225104)Peak memory usage: 94 MB % 17.99/3.28 % (225104)Instructions burned: 1001 (million) % 17.99/3.28 % (225122)Instruction limit reached! % 17.99/3.28 % (225122)------------------------------ % 17.99/3.28 % (225122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.99/3.28 % (225122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.99/3.28 % (225122)CaDiCaL version: 2.1.3 % 17.99/3.28 % (225122)Termination reason: Instruction limit % 17.99/3.28 % (225122)Termination phase: Saturation % 17.99/3.28 % (225122)Time elapsed: 0.175 s % 17.99/3.28 % (225122)Peak memory usage: 134 MB % 17.99/3.28 % (225122)Instructions burned: 217 (million) % 17.99/3.28 % (225136)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1329252344:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 17.99/3.28 % (225135)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2760512848:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi) % 17.99/3.28 % (225126)Instruction limit reached! % 17.99/3.28 % (225126)------------------------------ % 18.87/3.46 % (225126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225126)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225126)Termination reason: Instruction limit % 18.87/3.46 % (225126)Termination phase: Saturation % 18.87/3.46 % (225126)Time elapsed: 0.225 s % 18.87/3.46 % (225126)Peak memory usage: 117 MB % 18.87/3.46 % (225126)Instructions burned: 350 (million) % 18.87/3.46 % (225137)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=391501690:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi) % 18.87/3.46 % (225129)Instruction limit reached! % 18.87/3.46 % (225129)------------------------------ % 18.87/3.46 % (225129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225129)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225129)Termination reason: Instruction limit % 18.87/3.46 % (225129)Termination phase: Saturation % 18.87/3.46 % (225129)Time elapsed: 0.221 s % 18.87/3.46 % (225129)Peak memory usage: 117 MB % 18.87/3.46 % (225129)Instructions burned: 328 (million) % 18.87/3.46 % (225138)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1278017813:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 18.87/3.46 % (225138)Refutation not found, incomplete strategy % 18.87/3.46 % (225138)------------------------------ % 18.87/3.46 % (225138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225138)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225138)Termination reason: Refutation not found, incomplete strategy % 18.87/3.46 % (225138)Time elapsed: 0.028 s % 18.87/3.46 % (225138)Peak memory usage: 112 MB % 18.87/3.46 % (225138)Instructions burned: 7 (million) % 18.87/3.46 % (225121)Instruction limit reached! % 18.87/3.46 % (225121)------------------------------ % 18.87/3.46 % (225121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225121)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225121)Termination reason: Instruction limit % 18.87/3.46 % (225121)Termination phase: Saturation % 18.87/3.46 % (225121)Time elapsed: 0.400 s % 18.87/3.46 % (225121)Peak memory usage: 136 MB % 18.87/3.46 % (225121)Instructions burned: 483 (million) % 18.87/3.46 % (225136)Instruction limit reached! % 18.87/3.46 % (225136)------------------------------ % 18.87/3.46 % (225136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225136)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225136)Termination reason: Instruction limit % 18.87/3.46 % (225136)Termination phase: Saturation % 18.87/3.46 % (225136)Time elapsed: 0.144 s % 18.87/3.46 % (225136)Peak memory usage: 91 MB % 18.87/3.46 % (225136)Instructions burned: 485 (million) % 18.87/3.46 % (225141)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3753661604:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi) % 18.87/3.46 % (225137)Instruction limit reached! % 18.87/3.46 % (225137)------------------------------ % 18.87/3.46 % (225137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225137)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225137)Termination reason: Instruction limit % 18.87/3.46 % (225137)Termination phase: Saturation % 18.87/3.46 % (225137)Time elapsed: 0.168 s % 18.87/3.46 % (225137)Peak memory usage: 113 MB % 18.87/3.46 % (225137)Instructions burned: 323 (million) % 18.87/3.46 % (225135)Instruction limit reached! % 18.87/3.46 % (225135)------------------------------ % 18.87/3.46 % (225135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.46 % (225135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.46 % (225135)CaDiCaL version: 2.1.3 % 18.87/3.46 % (225135)Termination reason: Instruction limit % 18.87/3.46 % (225135)Termination phase: Saturation % 18.87/3.46 % (225135)Time elapsed: 0.205 s % 18.87/3.46 % (225135)Peak memory usage: 117 MB % 18.87/3.46 % (225135)Instructions burned: 282 (million) % 18.87/3.46 % (225143)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=3378090589:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 21.28/4.01 % (225145)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1378086595:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi) % 21.28/4.01 % (225146)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2259217107:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi) % 21.28/4.01 % (225148)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3551567102:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 21.28/4.01 % (225138)------------------------------ % 21.28/4.01 % (225138)------------------------------ % 21.28/4.01 % (225150)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2029916800:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi) % 21.28/4.01 % (225145)Instruction limit reached! % 21.28/4.01 % (225145)------------------------------ % 21.28/4.01 % (225145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.28/4.01 % (225145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.28/4.01 % (225145)CaDiCaL version: 2.1.3 % 21.28/4.01 % (225145)Termination reason: Instruction limit % 21.28/4.01 % (225145)Termination phase: Saturation % 21.28/4.01 % (225145)Time elapsed: 0.141 s % 21.28/4.01 % (225145)Peak memory usage: 118 MB % 21.28/4.01 % (225145)Instructions burned: 375 (million) % 21.28/4.01 % (225143)Instruction limit reached! % 21.28/4.01 % (225143)------------------------------ % 21.28/4.01 % (225143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.28/4.01 % (225143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.28/4.01 % (225143)CaDiCaL version: 2.1.3 % 21.28/4.01 % (225143)Termination reason: Instruction limit % 21.28/4.01 % (225143)Termination phase: Saturation % 21.28/4.01 % (225143)Time elapsed: 0.233 s % 21.28/4.01 % (225143)Peak memory usage: 137 MB % 21.28/4.01 % (225143)Instructions burned: 278 (million) % 21.28/4.01 % (225141)Instruction limit reached! % 21.28/4.01 % (225141)------------------------------ % 21.28/4.01 % (225141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.28/4.01 % (225141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.28/4.01 % (225141)CaDiCaL version: 2.1.3 % 21.28/4.01 % (225141)Termination reason: Instruction limit % 21.28/4.01 % (225141)Termination phase: Saturation % 21.28/4.01 % (225141)Time elapsed: 0.328 s % 21.28/4.01 % (225141)Peak memory usage: 119 MB % 21.28/4.01 % (225141)Instructions burned: 472 (million) % 21.28/4.01 % (225156)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=533874039:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi) % 21.28/4.01 % (225154)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1725392957:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi) % 21.28/4.01 % (225146)Instruction limit reached! % 21.28/4.01 % (225146)------------------------------ % 21.28/4.01 % (225146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.28/4.01 % (225146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.28/4.01 % (225146)CaDiCaL version: 2.1.3 % 21.28/4.01 % (225146)Termination reason: Instruction limit % 21.28/4.01 % (225146)Termination phase: Saturation % 21.28/4.01 % (225146)Time elapsed: 0.300 s % 21.28/4.01 % (225146)Peak memory usage: 119 MB % 21.28/4.01 % (225146)Instructions burned: 387 (million) % 21.28/4.01 % (225157)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1220646481:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi) % 21.28/4.01 % (225156)Instruction limit reached! % 21.28/4.01 % (225156)------------------------------ % 21.28/4.01 % (225156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.28/4.01 % (225156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.28/4.01 % (225156)CaDiCaL version: 2.1.3 % 21.28/4.01 % (225156)Termination reason: Instruction limit % 21.28/4.01 % (225156)Termination phase: Saturation % 21.28/4.01 % (225156)Time elapsed: 0.126 s % 21.28/4.01 % (225156)Peak memory usage: 118 MB % 25.81/4.46 % (225156)Instructions burned: 342 (million) % 25.81/4.46 % (225150)Instruction limit reached! % 25.81/4.46 % (225150)------------------------------ % 25.81/4.46 % (225150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.46 % (225150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.46 % (225150)CaDiCaL version: 2.1.3 % 25.81/4.46 % (225150)Termination reason: Instruction limit % 25.81/4.46 % (225150)Termination phase: Saturation % 25.81/4.46 % (225150)Time elapsed: 0.274 s % 25.81/4.46 % (225150)Peak memory usage: 135 MB % 25.81/4.46 % (225150)Instructions burned: 335 (million) % 25.81/4.46 % (225159)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=600700648:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi) % 25.81/4.46 % (225148)Instruction limit reached! % 25.81/4.46 % (225148)------------------------------ % 25.81/4.46 % (225148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.46 % (225148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.46 % (225148)CaDiCaL version: 2.1.3 % 25.81/4.46 % (225148)Termination reason: Instruction limit % 25.81/4.46 % (225148)Termination phase: Saturation % 25.81/4.46 % (225148)Time elapsed: 0.310 s % 25.81/4.46 % (225148)Peak memory usage: 92 MB % 25.81/4.46 % (225148)Instructions burned: 513 (million) % 25.81/4.46 % (225154)Instruction limit reached! % 25.81/4.46 % (225154)------------------------------ % 25.81/4.46 % (225154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.46 % (225154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.46 % (225154)CaDiCaL version: 2.1.3 % 25.81/4.46 % (225154)Termination reason: Instruction limit % 25.81/4.46 % (225154)Termination phase: Saturation % 25.81/4.46 % (225154)Time elapsed: 0.194 s % 25.81/4.46 % (225154)Peak memory usage: 91 MB % 25.81/4.46 % (225154)Instructions burned: 359 (million) % 25.81/4.46 % (225161)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3326157699:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi) % 25.81/4.46 % (225163)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1662794672:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi) % 25.81/4.46 % (225157)Instruction limit reached! % 25.81/4.46 % (225157)------------------------------ % 25.81/4.46 % (225157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.46 % (225157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.46 % (225157)CaDiCaL version: 2.1.3 % 25.81/4.46 % (225157)Termination reason: Instruction limit % 25.81/4.46 % (225157)Termination phase: Saturation % 25.81/4.46 % (225157)Time elapsed: 0.145 s % 25.81/4.46 % (225157)Peak memory usage: 116 MB % 25.81/4.46 % (225157)Instructions burned: 261 (million) % 25.81/4.46 % (225165)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2969629310:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 25.81/4.46 % (225159)Instruction limit reached! % 25.81/4.46 % (225159)------------------------------ % 25.81/4.46 % (225159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.46 % (225159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.46 % (225159)CaDiCaL version: 2.1.3 % 25.81/4.46 % (225159)Termination reason: Instruction limit % 25.81/4.46 % (225159)Termination phase: Saturation % 25.81/4.46 % (225159)Time elapsed: 0.148 s % 25.81/4.46 % (225159)Peak memory usage: 116 MB % 25.81/4.46 % (225159)Instructions burned: 237 (million) % 25.81/4.46 % (225163)Instruction limit reached! % 25.81/4.46 % (225163)------------------------------ % 25.81/4.46 % (225163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.81/4.46 % (225163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.81/4.46 % (225163)CaDiCaL version: 2.1.3 % 25.81/4.46 % (225163)Termination reason: Instruction limit % 25.81/4.46 % (225163)Termination phase: Saturation % 25.81/4.46 % (225163)Time elapsed: 0.052 s % 25.81/4.46 % (225163)Peak memory usage: 90 MB % 25.81/4.46 % (225163)Instructions burned: 147 (million) % 25.81/4.46 % (225166)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=3557017610:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi) % 29.23/4.90 % (225167)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3519848123:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi) % 29.23/4.90 % (225172)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2938721895:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi) % 29.23/4.90 % (225170)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3174244487:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi) % 29.23/4.90 % (225161)Instruction limit reached! % 29.23/4.90 % (225161)------------------------------ % 29.23/4.90 % (225161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.23/4.90 % (225161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.90 % (225161)CaDiCaL version: 2.1.3 % 29.23/4.90 % (225161)Termination reason: Instruction limit % 29.23/4.90 % (225161)Termination phase: Saturation % 29.23/4.90 % (225161)Time elapsed: 0.191 s % 29.23/4.90 % (225161)Peak memory usage: 91 MB % 29.23/4.90 % (225161)Instructions burned: 274 (million) % 29.23/4.90 % (225173)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=546192222:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi) % 29.23/4.90 % (225173)Refutation not found, incomplete strategy % 29.23/4.90 % (225173)------------------------------ % 29.23/4.90 % (225173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.23/4.90 % (225173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.90 % (225173)CaDiCaL version: 2.1.3 % 29.23/4.90 % (225173)Termination reason: Refutation not found, incomplete strategy % 29.23/4.90 % (225173)Time elapsed: 0.029 s % 29.23/4.90 % (225173)Peak memory usage: 112 MB % 29.23/4.90 % (225173)Instructions burned: 8 (million) % 29.23/4.90 % (225166)Instruction limit reached! % 29.23/4.90 % (225166)------------------------------ % 29.23/4.90 % (225166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.23/4.90 % (225166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.90 % (225166)CaDiCaL version: 2.1.3 % 29.23/4.90 % (225166)Termination reason: Instruction limit % 29.23/4.90 % (225166)Termination phase: Saturation % 29.23/4.90 % (225166)Time elapsed: 0.212 s % 29.23/4.90 % (225166)Peak memory usage: 136 MB % 29.23/4.90 % (225166)Instructions burned: 277 (million) % 29.23/4.90 % (225178)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=386402232:s2a=on:i=450:doe=on:nm=32:rtra=on_2970 on theBenchmark for (2970ds/450Mi) % 29.23/4.90 % (225180)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 % 29.23/4.90 % (225180)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2401515415:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi) % 29.23/4.90 % (225173)------------------------------ % 29.23/4.90 % (225173)------------------------------ % 29.23/4.90 % (225172)Instruction limit reached! % 29.23/4.90 % (225172)------------------------------ % 29.23/4.90 % (225172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.23/4.90 % (225172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.90 % (225172)CaDiCaL version: 2.1.3 % 29.23/4.90 % (225172)Termination reason: Instruction limit % 29.23/4.90 % (225172)Termination phase: Saturation % 29.23/4.90 % (225172)Time elapsed: 0.323 s % 29.23/4.90 % (225172)Peak memory usage: 92 MB % 29.23/4.90 % (225172)Instructions burned: 1055 (million) % 29.23/4.90 % (225184)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=84450848:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi) % 29.23/4.90 % (225170)Instruction limit reached! % 29.23/4.90 % (225170)------------------------------ % 29.23/4.90 % (225170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.23/4.90 % (225170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.90 % (225170)CaDiCaL version: 2.1.3 % 29.23/4.90 % (225170)Termination reason: Instruction limit % 29.23/4.90 % (225170)Termination phase: Saturation % 29.23/4.90 % (225170)Time elapsed: 0.448 s % 29.23/4.90 % (225170)Peak memory usage: 94 MB % 32.64/5.47 % (225170)Instructions burned: 657 (million) % 32.64/5.47 % (225183)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2842754223:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2967 on theBenchmark for (2967ds/130Mi) % 32.64/5.47 % (225178)Instruction limit reached! % 32.64/5.47 % (225178)------------------------------ % 32.64/5.47 % (225178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.47 % (225178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.47 % (225178)CaDiCaL version: 2.1.3 % 32.64/5.47 % (225178)Termination reason: Instruction limit % 32.64/5.47 % (225178)Termination phase: Saturation % 32.64/5.47 % (225178)Time elapsed: 0.347 s % 32.64/5.47 % (225178)Peak memory usage: 135 MB % 32.64/5.47 % (225178)Instructions burned: 452 (million) % 32.64/5.47 % (225184)Instruction limit reached! % 32.64/5.47 % (225184)------------------------------ % 32.64/5.47 % (225184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.47 % (225184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.47 % (225184)CaDiCaL version: 2.1.3 % 32.64/5.47 % (225184)Termination reason: Instruction limit % 32.64/5.47 % (225184)Termination phase: Saturation % 32.64/5.47 % (225184)Time elapsed: 0.114 s % 32.64/5.47 % (225184)Peak memory usage: 117 MB % 32.64/5.47 % (225184)Instructions burned: 313 (million) % 32.64/5.47 % (225183)Instruction limit reached! % 32.64/5.47 % (225183)------------------------------ % 32.64/5.47 % (225183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.47 % (225183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.47 % (225183)CaDiCaL version: 2.1.3 % 32.64/5.47 % (225183)Termination reason: Instruction limit % 32.64/5.47 % (225183)Termination phase: Saturation % 32.64/5.47 % (225183)Time elapsed: 0.101 s % 32.64/5.47 % (225183)Peak memory usage: 116 MB % 32.64/5.47 % (225183)Instructions burned: 131 (million) % 32.64/5.47 % (225186)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1040032537:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi) % 32.64/5.47 % (225167)Instruction limit reached! % 32.64/5.47 % (225167)------------------------------ % 32.64/5.47 % (225167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.47 % (225167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.47 % (225167)CaDiCaL version: 2.1.3 % 32.64/5.47 % (225167)Termination reason: Instruction limit % 32.64/5.47 % (225167)Termination phase: Saturation % 32.64/5.47 % (225167)Time elapsed: 0.695 s % 32.64/5.47 % (225167)Peak memory usage: 94 MB % 32.64/5.47 % (225167)Instructions burned: 1053 (million) % 32.64/5.47 % (225189)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3872107212:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi) % 32.64/5.47 % (225189)Refutation not found, incomplete strategy % 32.64/5.47 % (225189)------------------------------ % 32.64/5.47 % (225189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.47 % (225189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.47 % (225189)CaDiCaL version: 2.1.3 % 32.64/5.47 % (225189)Termination reason: Refutation not found, incomplete strategy % 32.64/5.47 % (225189)Time elapsed: 0.002 s % 32.64/5.47 % (225189)Peak memory usage: 89 MB % 32.64/5.47 % (225189)Instructions burned: 4 (million) % 32.64/5.47 % (225188)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1489194003:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi) % 32.64/5.47 % (225190)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2972103505:i=776:doe=on:rtra=on_2965 on theBenchmark for (2965ds/776Mi) % 32.64/5.47 % (225192)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1597652953:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/646Mi) % 32.64/5.47 % (225189)------------------------------ % 32.64/5.47 % (225189)------------------------------ % 32.64/5.47 % (225186)Instruction limit reached! % 32.64/5.47 % (225186)------------------------------ % 32.64/5.47 % (225186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.64/5.47 % (225186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.64/5.47 % (225186)CaDiCaL version: 2.1.3 % 32.64/5.47 % (225186)Termination reason: Instruction limit % 32.64/5.47 % (225186)Termination phase: Saturation % 40.41/6.48 % (225186)Time elapsed: 0.285 s % 40.41/6.48 % (225186)Peak memory usage: 92 MB % 40.41/6.48 % (225186)Instructions burned: 491 (million) % 40.41/6.48 % (225197)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=4279325288:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2962 on theBenchmark for (2962ds/784Mi) % 40.41/6.48 % (225180)Instruction limit reached! % 40.41/6.48 % (225180)------------------------------ % 40.41/6.48 % (225180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.41/6.48 % (225180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.41/6.48 % (225180)CaDiCaL version: 2.1.3 % 40.41/6.48 % (225180)Termination reason: Instruction limit % 40.41/6.48 % (225180)Termination phase: Saturation % 40.41/6.48 % (225180)Time elapsed: 0.732 s % 40.41/6.48 % (225180)Peak memory usage: 123 MB % 40.41/6.48 % (225180)Instructions burned: 1090 (million) % 40.41/6.48 % (225198)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=404026969:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2961 on theBenchmark for (2961ds/1131Mi) % 40.41/6.48 % (225190)Instruction limit reached! % 40.41/6.48 % (225190)------------------------------ % 40.41/6.48 % (225190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.41/6.48 % (225190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.41/6.48 % (225190)CaDiCaL version: 2.1.3 % 40.41/6.48 % (225190)Termination reason: Instruction limit % 40.41/6.48 % (225190)Termination phase: Saturation % 40.41/6.48 % (225190)Time elapsed: 0.396 s % 40.41/6.48 % (225190)Peak memory usage: 118 MB % 40.41/6.48 % (225190)Instructions burned: 776 (million) % 40.41/6.48 % (225188)Instruction limit reached! % 40.41/6.48 % (225188)------------------------------ % 40.41/6.48 % (225188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.41/6.48 % (225188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.41/6.48 % (225188)CaDiCaL version: 2.1.3 % 40.41/6.48 % (225188)Termination reason: Instruction limit % 40.41/6.48 % (225188)Termination phase: Saturation % 40.41/6.48 % (225188)Time elapsed: 0.489 s % 40.41/6.48 % (225188)Peak memory usage: 94 MB % 40.41/6.48 % (225188)Instructions burned: 835 (million) % 40.41/6.48 % (225200)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=4027654367:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi) % 40.41/6.48 % (225197)Instruction limit reached! % 40.41/6.48 % (225197)------------------------------ % 40.41/6.48 % (225197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.41/6.48 % (225197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.41/6.48 % (225197)CaDiCaL version: 2.1.3 % 40.41/6.48 % (225197)Termination reason: Instruction limit % 40.41/6.48 % (225197)Termination phase: Saturation % 40.41/6.48 % (225197)Time elapsed: 0.288 s % 40.41/6.48 % (225197)Peak memory usage: 122 MB % 40.41/6.48 % (225197)Instructions burned: 787 (million) % 40.41/6.48 % (225192)Instruction limit reached! % 40.41/6.48 % (225192)------------------------------ % 40.41/6.48 % (225192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.41/6.48 % (225192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.41/6.48 % (225192)CaDiCaL version: 2.1.3 % 40.41/6.48 % (225192)Termination reason: Instruction limit % 40.41/6.48 % (225192)Termination phase: Saturation % 40.41/6.48 % (225192)Time elapsed: 0.471 s % 40.41/6.48 % (225192)Peak memory usage: 138 MB % 40.41/6.48 % (225192)Instructions burned: 646 (million) % 40.41/6.48 % (225202)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3924595874:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/775Mi) % 40.41/6.48 % (225203)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1723302496:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 40.41/6.48 % (225200)Instruction limit reached! % 40.41/6.48 % (225200)------------------------------ % 40.41/6.48 % (225200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.41/6.48 % (225200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.41/6.48 % (225200)CaDiCaL version: 2.1.3 % 50.18/8.01 % (225200)Termination reason: Instruction limit % 50.18/8.01 % (225200)Termination phase: Saturation % 50.18/8.01 % (225200)Time elapsed: 0.151 s % 50.18/8.01 % (225200)Peak memory usage: 116 MB % 50.18/8.01 % (225200)Instructions burned: 247 (million) % 50.18/8.01 % (225205)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1753434855:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi) % 50.18/8.01 % (225205)Instruction limit reached! % 50.18/8.01 % (225205)------------------------------ % 50.18/8.01 % (225205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.18/8.01 % (225205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.18/8.01 % (225205)CaDiCaL version: 2.1.3 % 50.18/8.01 % (225205)Termination reason: Instruction limit % 50.18/8.01 % (225205)Termination phase: Saturation % 50.18/8.01 % (225205)Time elapsed: 0.031 s % 50.18/8.01 % (225205)Peak memory usage: 89 MB % 50.18/8.01 % (225205)Instructions burned: 102 (million) % 50.18/8.01 % (225207)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=180060342:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi) % 50.18/8.01 % (225210)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1932088195:i=6400:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/6400Mi) % 50.18/8.01 % (225211)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=1355907233:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/868Mi) % 50.18/8.01 % (225203)Instruction limit reached! % 50.18/8.01 % (225203)------------------------------ % 50.18/8.01 % (225203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.18/8.01 % (225203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.18/8.01 % (225203)CaDiCaL version: 2.1.3 % 50.18/8.01 % (225203)Termination reason: Instruction limit % 50.18/8.01 % (225203)Termination phase: Saturation % 50.18/8.01 % (225203)Time elapsed: 0.189 s % 50.18/8.01 % (225203)Peak memory usage: 91 MB % 50.18/8.01 % (225203)Instructions burned: 274 (million) % 50.18/8.01 % (225215)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=1770679217:i=1846:canc=cautious:fsr=off:rtra=on_2955 on theBenchmark for (2955ds/1846Mi) % 50.18/8.01 % (225202)Instruction limit reached! % 50.18/8.01 % (225202)------------------------------ % 50.18/8.01 % (225202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.18/8.01 % (225202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.18/8.01 % (225202)CaDiCaL version: 2.1.3 % 50.18/8.01 % (225202)Termination reason: Instruction limit % 50.18/8.01 % (225202)Termination phase: Saturation % 50.18/8.01 % (225202)Time elapsed: 0.484 s % 50.18/8.01 % (225202)Peak memory usage: 94 MB % 50.18/8.01 % (225202)Instructions burned: 777 (million) % 50.18/8.01 % (225211)Instruction limit reached! % 50.18/8.01 % (225211)------------------------------ % 50.18/8.01 % (225211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.18/8.01 % (225211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.18/8.01 % (225211)CaDiCaL version: 2.1.3 % 50.18/8.01 % (225211)Termination reason: Instruction limit % 50.18/8.01 % (225211)Termination phase: Saturation % 50.18/8.01 % (225211)Time elapsed: 0.295 s % 50.18/8.01 % (225211)Peak memory usage: 121 MB % 50.18/8.01 % (225211)Instructions burned: 871 (million) % 50.18/8.01 % (225198)Instruction limit reached! % 50.18/8.01 % (225198)------------------------------ % 50.18/8.01 % (225198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.18/8.01 % (225198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.18/8.01 % (225198)CaDiCaL version: 2.1.3 % 50.18/8.01 % (225198)Termination reason: Instruction limit % 50.18/8.01 % (225198)Termination phase: Saturation % 50.18/8.01 % (225198)Time elapsed: 0.761 s % 50.18/8.01 % (225198)Peak memory usage: 124 MB % 50.18/8.01 % (225198)Instructions burned: 1132 (million) % 50.18/8.01 % (225218)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3110476731:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2952 on theBenchmark for (2952ds/273Mi) % 50.18/8.01 % (225217)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2803372366:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2953 on theBenchmark for (2953ds/36816Mi) % 60.88/9.25 % (225219)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=3390229636:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/863Mi) % 60.88/9.25 % (225218)Instruction limit reached! % 60.88/9.25 % (225218)------------------------------ % 60.88/9.25 % (225218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.88/9.25 % (225218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.88/9.25 % (225218)CaDiCaL version: 2.1.3 % 60.88/9.25 % (225218)Termination reason: Instruction limit % 60.88/9.25 % (225218)Termination phase: Saturation % 60.88/9.25 % (225218)Time elapsed: 0.101 s % 60.88/9.25 % (225218)Peak memory usage: 91 MB % 60.88/9.25 % (225218)Instructions burned: 276 (million) % 60.88/9.25 % (225207)Instruction limit reached! % 60.88/9.25 % (225207)------------------------------ % 60.88/9.25 % (225207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.88/9.25 % (225207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.88/9.25 % (225207)CaDiCaL version: 2.1.3 % 60.88/9.25 % (225207)Termination reason: Instruction limit % 60.88/9.25 % (225207)Termination phase: Saturation % 60.88/9.25 % (225207)Time elapsed: 0.611 s % 60.88/9.25 % (225207)Peak memory usage: 91 MB % 60.88/9.25 % (225207)Instructions burned: 1094 (million) % 60.88/9.25 % (225223)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1576944279:i=5811:kws=precedence:nm=0:rtra=on_2950 on theBenchmark for (2950ds/5811Mi) % 60.88/9.25 % (225224)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=1703876559:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2950 on theBenchmark for (2950ds/2216Mi) % 60.88/9.25 % (225165)Instruction limit reached! % 60.88/9.25 % (225165)------------------------------ % 60.88/9.25 % (225165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.88/9.25 % (225165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.88/9.25 % (225165)CaDiCaL version: 2.1.3 % 60.88/9.25 % (225165)Termination reason: Instruction limit % 60.88/9.25 % (225165)Termination phase: Saturation % 60.88/9.25 % (225165)Time elapsed: 2.398 s % 60.88/9.25 % (225165)Peak memory usage: 105 MB % 60.88/9.25 % (225165)Instructions burned: 4428 (million) % 60.88/9.25 % (225227)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3525368450:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/801Mi) % 60.88/9.25 % (225219)Instruction limit reached! % 60.88/9.25 % (225219)------------------------------ % 60.88/9.25 % (225219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.88/9.25 % (225219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.88/9.25 % (225219)CaDiCaL version: 2.1.3 % 60.88/9.25 % (225219)Termination reason: Instruction limit % 60.88/9.25 % (225219)Termination phase: Saturation % 60.88/9.25 % (225219)Time elapsed: 0.474 s % 60.88/9.25 % (225219)Peak memory usage: 119 MB % 60.88/9.25 % (225219)Instructions burned: 863 (million) % 60.88/9.25 % (225215)Instruction limit reached! % 60.88/9.25 % (225215)------------------------------ % 60.88/9.25 % (225215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.88/9.25 % (225215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.88/9.25 % (225215)CaDiCaL version: 2.1.3 % 60.88/9.25 % (225215)Termination reason: Instruction limit % 60.88/9.25 % (225215)Termination phase: Saturation % 60.88/9.25 % (225215)Time elapsed: 0.851 s % 60.88/9.25 % (225215)Peak memory usage: 97 MB % 60.88/9.25 % (225215)Instructions burned: 1847 (million) % 60.88/9.25 % (225229)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2028199540:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2946 on theBenchmark for (2946ds/1026Mi) % 60.88/9.25 % (225230)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2532571905:i=3509:rtra=on_2945 on theBenchmark for (2945ds/3509Mi) % 60.88/9.25 % (225227)Instruction limit reached! % 60.88/9.25 % (225227)------------------------------ % 60.88/9.25 % (225227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.88/9.25 % (225227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.88/9.25 % (225227)CaDiCaL version: 2.1.3 % 60.88/9.25 % (225227)Termination reason: Instruction limit % 99.09/14.64 % (225227)Termination phase: Saturation % 99.09/14.64 % (225227)Time elapsed: 0.474 s % 99.09/14.64 % (225227)Peak memory usage: 93 MB % 99.09/14.64 % (225227)Instructions burned: 801 (million) % 99.09/14.64 % (225233)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3223947523:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/2127Mi) % 99.09/14.64 % (225229)Instruction limit reached! % 99.09/14.64 % (225229)------------------------------ % 99.09/14.64 % (225229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.09/14.64 % (225229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.09/14.64 % (225229)CaDiCaL version: 2.1.3 % 99.09/14.64 % (225229)Termination reason: Instruction limit % 99.09/14.64 % (225229)Termination phase: Saturation % 99.09/14.64 % (225229)Time elapsed: 0.578 s % 99.09/14.64 % (225229)Peak memory usage: 92 MB % 99.09/14.64 % (225229)Instructions burned: 1028 (million) % 99.09/14.64 % (225235)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2216407326:i=1959:rtra=on:fsd=on:proc=on_2938 on theBenchmark for (2938ds/1959Mi) % 99.09/14.64 % (225224)Instruction limit reached! % 99.09/14.64 % (225224)------------------------------ % 99.09/14.64 % (225224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.09/14.64 % (225224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.09/14.64 % (225224)CaDiCaL version: 2.1.3 % 99.09/14.64 % (225224)Termination reason: Instruction limit % 99.09/14.64 % (225224)Termination phase: Saturation % 99.09/14.64 % (225224)Time elapsed: 1.247 s % 99.09/14.64 % (225224)Peak memory usage: 120 MB % 99.09/14.64 % (225224)Instructions burned: 2222 (million) % 99.09/14.64 % (225237)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3854701668:s2a=on:i=3553:nm=0:rtra=on_2936 on theBenchmark for (2936ds/3553Mi) % 99.09/14.64 % (225223)Instruction limit reached! % 99.09/14.64 % (225223)------------------------------ % 99.09/14.64 % (225223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.09/14.64 % (225223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.09/14.64 % (225223)CaDiCaL version: 2.1.3 % 99.09/14.64 % (225223)Termination reason: Instruction limit % 99.09/14.64 % (225223)Termination phase: Saturation % 99.09/14.64 % (225223)Time elapsed: 1.642 s % 99.09/14.64 % (225223)Peak memory usage: 131 MB % 99.09/14.64 % (225223)Instructions burned: 5814 (million) % 99.09/14.64 % (225239)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3364241000:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2933 on theBenchmark for (2933ds/3201Mi) % 99.09/14.64 % (225233)Instruction limit reached! % 99.09/14.64 % (225233)------------------------------ % 99.09/14.64 % (225233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.09/14.64 % (225233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.09/14.64 % (225233)CaDiCaL version: 2.1.3 % 99.09/14.64 % (225233)Termination reason: Instruction limit % 99.09/14.64 % (225233)Termination phase: Saturation % 99.09/14.64 % (225233)Time elapsed: 1.120 s % 99.09/14.64 % (225233)Peak memory usage: 91 MB % 99.09/14.64 % (225233)Instructions burned: 2127 (million) % 99.09/14.64 % (225241)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=3595197679:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2928 on theBenchmark for (2928ds/4093Mi) % 99.09/14.64 % (225230)Instruction limit reached! % 99.09/14.64 % (225230)------------------------------ % 99.09/14.64 % (225230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.09/14.64 % (225230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.09/14.64 % (225230)CaDiCaL version: 2.1.3 % 99.09/14.64 % (225230)Termination reason: Instruction limit % 99.09/14.64 % (225230)Termination phase: Saturation % 99.09/14.64 % (225230)Time elapsed: 1.747 s % 99.09/14.64 % (225230)Peak memory usage: 103 MB % 99.09/14.64 % (225230)Instructions burned: 3509 (million) % 99.09/14.64 % (225235)Instruction limit reached! % 99.09/14.64 % (225235)------------------------------ % 99.09/14.64 % (225235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.09/14.64 % (225235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.09/14.64 % (225235)CaDiCaL version: 2.1.3 % 99.09/14.64 % (225235)Termination reason: Instruction limit % 99.09/14.64 % (225235)Termination phase: Saturation % 99.09/14.64 % (225235)Time elapsed: 1.105 s % 119.88/17.52 % (225235)Peak memory usage: 124 MB % 119.88/17.52 % (225235)Instructions burned: 1960 (million) % 119.88/17.52 % (225243)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=2220382038:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2926 on theBenchmark for (2926ds/21173Mi) % 119.88/17.52 % (225244)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1730184839:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2926 on theBenchmark for (2926ds/10544Mi) % 119.88/17.52 % (225239)Instruction limit reached! % 119.88/17.52 % (225239)------------------------------ % 119.88/17.52 % (225239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.88/17.52 % (225239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.88/17.52 % (225239)CaDiCaL version: 2.1.3 % 119.88/17.52 % (225239)Termination reason: Instruction limit % 119.88/17.52 % (225239)Termination phase: Saturation % 119.88/17.52 % (225239)Time elapsed: 0.798 s % 119.88/17.52 % (225239)Peak memory usage: 93 MB % 119.88/17.52 % (225239)Instructions burned: 3204 (million) % 119.88/17.52 % (225247)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2964944249:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2923 on theBenchmark for (2923ds/1262Mi) % 119.88/17.52 % (225210)Instruction limit reached! % 119.88/17.52 % (225210)------------------------------ % 119.88/17.52 % (225210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.88/17.52 % (225210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.88/17.52 % (225210)CaDiCaL version: 2.1.3 % 119.88/17.52 % (225210)Termination reason: Instruction limit % 119.88/17.52 % (225210)Termination phase: Saturation % 119.88/17.52 % (225210)Time elapsed: 3.416 s % 119.88/17.52 % (225210)Peak memory usage: 113 MB % 119.88/17.52 % (225210)Instructions burned: 6401 (million) % 119.88/17.52 % (225249)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1380762591:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2921 on theBenchmark for (2921ds/775Mi) % 119.88/17.52 % (225247)Instruction limit reached! % 119.88/17.52 % (225247)------------------------------ % 119.88/17.52 % (225247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.88/17.52 % (225247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.88/17.52 % (225247)CaDiCaL version: 2.1.3 % 119.88/17.52 % (225247)Termination reason: Instruction limit % 119.88/17.52 % (225247)Termination phase: Saturation % 119.88/17.52 % (225247)Time elapsed: 0.353 s % 119.88/17.52 % (225247)Peak memory usage: 117 MB % 119.88/17.52 % (225247)Instructions burned: 1262 (million) % 119.88/17.52 % (225251)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=957247349:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2918 on theBenchmark for (2918ds/270Mi) % 119.88/17.52 % (225251)Instruction limit reached! % 119.88/17.52 % (225251)------------------------------ % 119.88/17.52 % (225251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.88/17.52 % (225251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.88/17.52 % (225251)CaDiCaL version: 2.1.3 % 119.88/17.52 % (225251)Termination reason: Instruction limit % 119.88/17.52 % (225251)Termination phase: Saturation % 119.88/17.52 % (225251)Time elapsed: 0.096 s % 119.88/17.52 % (225251)Peak memory usage: 91 MB % 119.88/17.52 % (225251)Instructions burned: 274 (million) % 119.88/17.52 % (225253)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1480977307:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2916 on theBenchmark for (2916ds/17165Mi) % 119.88/17.52 % (225249)Instruction limit reached! % 119.88/17.52 % (225249)------------------------------ % 119.88/17.52 % (225249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.88/17.52 % (225249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.88/17.52 % (225249)CaDiCaL version: 2.1.3 % 119.88/17.52 % (225249)Termination reason: Instruction limit % 119.88/17.52 % (225249)Termination phase: Saturation % 119.88/17.52 % (225249)Time elapsed: 0.476 s % 119.88/17.52 % (225249)Peak memory usage: 94 MB % 119.88/17.52 % (225249)Instructions burned: 775 (million) % 119.88/17.52 % (225255)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4238137492:s2a=on:i=13094:s2at=-1:rtra=on_2915 on theBenchmark for (2915ds/13094Mi) % 153.24/22.23 % (225237)Instruction limit reached! % 153.24/22.23 % (225237)------------------------------ % 153.24/22.23 % (225237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.24/22.23 % (225237)CaDiCaL version: 2.1.3 % 153.24/22.23 % (225237)Termination reason: Instruction limit % 153.24/22.23 % (225237)Termination phase: Saturation % 153.24/22.23 % (225237)Time elapsed: 2.307 s % 153.24/22.23 % (225237)Peak memory usage: 104 MB % 153.24/22.23 % (225237)Instructions burned: 3554 (million) % 153.24/22.23 % (225257)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2590688797:st=2:i=12633:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/12633Mi) % 153.24/22.23 % (225241)Instruction limit reached! % 153.24/22.23 % (225241)------------------------------ % 153.24/22.23 % (225241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.24/22.23 % (225241)CaDiCaL version: 2.1.3 % 153.24/22.23 % (225241)Termination reason: Instruction limit % 153.24/22.23 % (225241)Termination phase: Saturation % 153.24/22.23 % (225241)Time elapsed: 2.097 s % 153.24/22.23 % (225241)Peak memory usage: 143 MB % 153.24/22.23 % (225241)Instructions burned: 4093 (million) % 153.24/22.23 % (225259)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1897239026:i=1783:rtra=on:gtg=position_2906 on theBenchmark for (2906ds/1783Mi) % 153.24/22.23 % (225259)Instruction limit reached! % 153.24/22.23 % (225259)------------------------------ % 153.24/22.23 % (225259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.24/22.23 % (225259)CaDiCaL version: 2.1.3 % 153.24/22.23 % (225259)Termination reason: Instruction limit % 153.24/22.23 % (225259)Termination phase: Saturation % 153.24/22.23 % (225259)Time elapsed: 0.988 s % 153.24/22.23 % (225259)Peak memory usage: 128 MB % 153.24/22.23 % (225259)Instructions burned: 1783 (million) % 153.24/22.23 % (225261)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=3807269421:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2894 on theBenchmark for (2894ds/5451Mi) % 153.24/22.23 % (225253)Instruction limit reached! % 153.24/22.23 % (225253)------------------------------ % 153.24/22.23 % (225253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.24/22.23 % (225253)CaDiCaL version: 2.1.3 % 153.24/22.23 % (225253)Termination reason: Instruction limit % 153.24/22.23 % (225253)Termination phase: Saturation % 153.24/22.23 % (225253)Time elapsed: 4.072 s % 153.24/22.23 % (225253)Peak memory usage: 277 MB % 153.24/22.23 % (225253)Instructions burned: 17169 (million) % 153.24/22.23 % (225263)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=3983131314:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2874 on theBenchmark for (2874ds/4975Mi) % 153.24/22.23 % (225261)Instruction limit reached! % 153.24/22.23 % (225261)------------------------------ % 153.24/22.23 % (225261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.24/22.23 % (225261)CaDiCaL version: 2.1.3 % 153.24/22.23 % (225261)Termination reason: Instruction limit % 153.24/22.23 % (225261)Termination phase: Saturation % 153.24/22.23 % (225261)Time elapsed: 3.126 s % 153.24/22.23 % (225261)Peak memory usage: 147 MB % 153.24/22.23 % (225261)Instructions burned: 5452 (million) % 153.24/22.23 % (225244)Instruction limit reached! % 153.24/22.23 % (225244)------------------------------ % 153.24/22.23 % (225244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.24/22.23 % (225244)CaDiCaL version: 2.1.3 % 153.24/22.23 % (225244)Termination reason: Instruction limit % 153.24/22.23 % (225244)Termination phase: Saturation % 153.24/22.23 % (225244)Time elapsed: 6.312 s % 153.24/22.23 % (225244)Peak memory usage: 167 MB % 153.24/22.23 % (225244)Instructions burned: 10544 (million) % 153.24/22.23 % (225263)Instruction limit reached! % 153.24/22.23 % (225263)------------------------------ % 153.24/22.23 % (225263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.24/22.23 % (225263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.89/29.27 % (225263)CaDiCaL version: 2.1.3 % 202.89/29.27 % (225263)Termination reason: Instruction limit % 202.89/29.27 % (225263)Termination phase: Saturation % 202.89/29.27 % (225263)Time elapsed: 1.340 s % 202.89/29.27 % (225263)Peak memory usage: 121 MB % 202.89/29.27 % (225263)Instructions burned: 4977 (million) % 202.89/29.27 % (225265)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=2570877045:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2861 on theBenchmark for (2861ds/2076Mi) % 202.89/29.27 % (225266)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2759190129:i=5145:rtra=on_2861 on theBenchmark for (2861ds/5145Mi) % 202.89/29.27 % (225268)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2703212759:i=3509:rtra=on_2860 on theBenchmark for (2860ds/3509Mi) % 202.89/29.27 % (225255)Instruction limit reached! % 202.89/29.27 % (225255)------------------------------ % 202.89/29.27 % (225255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.89/29.27 % (225255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.89/29.27 % (225255)CaDiCaL version: 2.1.3 % 202.89/29.27 % (225255)Termination reason: Instruction limit % 202.89/29.27 % (225255)Termination phase: Saturation % 202.89/29.27 % (225255)Time elapsed: 5.907 s % 202.89/29.27 % (225255)Peak memory usage: 160 MB % 202.89/29.27 % (225255)Instructions burned: 13094 (million) % 202.89/29.27 % (225271)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=350786846:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2854 on theBenchmark for (2854ds/13800Mi) % 202.89/29.27 % (225268)Instruction limit reached! % 202.89/29.27 % (225268)------------------------------ % 202.89/29.27 % (225268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.89/29.27 % (225268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.89/29.27 % (225268)CaDiCaL version: 2.1.3 % 202.89/29.27 % (225268)Termination reason: Instruction limit % 202.89/29.27 % (225268)Termination phase: Saturation % 202.89/29.27 % (225268)Time elapsed: 0.918 s % 202.89/29.27 % (225268)Peak memory usage: 104 MB % 202.89/29.27 % (225268)Instructions burned: 3512 (million) % 202.89/29.27 % (225273)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1255731427:i=1412:rtra=on:fsd=on:proc=on_2849 on theBenchmark for (2849ds/1412Mi) % 202.89/29.27 % (225265)Instruction limit reached! % 202.89/29.27 % (225265)------------------------------ % 202.89/29.27 % (225265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.89/29.27 % (225265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.89/29.27 % (225265)CaDiCaL version: 2.1.3 % 202.89/29.27 % (225265)Termination reason: Instruction limit % 202.89/29.27 % (225265)Termination phase: Saturation % 202.89/29.27 % (225265)Time elapsed: 1.268 s % 202.89/29.27 % (225265)Peak memory usage: 119 MB % 202.89/29.27 % (225265)Instructions burned: 2077 (million) % 202.89/29.27 % (225275)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 % 202.89/29.27 % (225275)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3789507997:i=11747:aac=none:nm=0:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/11747Mi) % 202.89/29.27 % (225273)Instruction limit reached! % 202.89/29.27 % (225273)------------------------------ % 202.89/29.27 % (225273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.89/29.27 % (225273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.89/29.27 % (225273)CaDiCaL version: 2.1.3 % 202.89/29.27 % (225273)Termination reason: Instruction limit % 202.89/29.27 % (225273)Termination phase: Saturation % 202.89/29.27 % (225273)Time elapsed: 0.416 s % 202.89/29.27 % (225273)Peak memory usage: 121 MB % 202.89/29.27 % (225273)Instructions burned: 1412 (million) % 202.89/29.27 % (225277)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4261743550:s2a=on:i=3553:nm=0:rtra=on_2844 on theBenchmark for (2844ds/3553Mi) % 202.89/29.27 % (225277)Instruction limit reached! % 202.89/29.27 % (225277)------------------------------ % 202.89/29.27 % (225277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.89/29.27 % (225277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.89/29.27 % (225277)CaDiCaL version: 2.1.3 % 202.89/29.27 % (225277)Termination reason: Instruction limit % 248.83/35.77 % (225277)Termination phase: Saturation % 248.83/35.77 % (225277)Time elapsed: 1.176 s % 248.83/35.77 % (225277)Peak memory usage: 104 MB % 248.83/35.77 % (225277)Instructions burned: 3554 (million) % 248.83/35.77 % (225257)Instruction limit reached! % 248.83/35.77 % (225257)------------------------------ % 248.83/35.77 % (225257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.83/35.77 % (225257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.83/35.77 % (225257)CaDiCaL version: 2.1.3 % 248.83/35.77 % (225257)Termination reason: Instruction limit % 248.83/35.77 % (225257)Termination phase: Saturation % 248.83/35.77 % (225257)Time elapsed: 7.909 s % 248.83/35.77 % (225257)Peak memory usage: 131 MB % 248.83/35.77 % (225257)Instructions burned: 12634 (million) % 248.83/35.77 % (225279)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=230041435:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/3201Mi) % 248.83/35.77 % (225280)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=1001922829:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2830 on theBenchmark for (2830ds/4081Mi) % 248.83/35.77 % (225266)Instruction limit reached! % 248.83/35.77 % (225266)------------------------------ % 248.83/35.77 % (225266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.83/35.77 % (225266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.83/35.77 % (225266)CaDiCaL version: 2.1.3 % 248.83/35.77 % (225266)Termination reason: Instruction limit % 248.83/35.77 % (225266)Termination phase: Saturation % 248.83/35.77 % (225266)Time elapsed: 3.228 s % 248.83/35.77 % (225266)Peak memory usage: 100 MB % 248.83/35.77 % (225266)Instructions burned: 5145 (million) % 248.83/35.77 % (225283)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=860291839:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2827 on theBenchmark for (2827ds/20260Mi) % 248.83/35.77 % (225279)Instruction limit reached! % 248.83/35.77 % (225279)------------------------------ % 248.83/35.77 % (225279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.83/35.77 % (225279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.83/35.77 % (225279)CaDiCaL version: 2.1.3 % 248.83/35.77 % (225279)Termination reason: Instruction limit % 248.83/35.77 % (225279)Termination phase: Saturation % 248.83/35.77 % (225279)Time elapsed: 0.795 s % 248.83/35.77 % (225279)Peak memory usage: 93 MB % 248.83/35.77 % (225279)Instructions burned: 3202 (million) % 248.83/35.77 % (225285)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=951214542:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2822 on theBenchmark for (2822ds/58627Mi) % 248.83/35.77 % (225280)Instruction limit reached! % 248.83/35.77 % (225280)------------------------------ % 248.83/35.77 % (225280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.83/35.77 % (225280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.83/35.77 % (225280)CaDiCaL version: 2.1.3 % 248.83/35.77 % (225280)Termination reason: Instruction limit % 248.83/35.77 % (225280)Termination phase: Saturation % 248.83/35.77 % (225280)Time elapsed: 2.009 s % 248.83/35.77 % (225280)Peak memory usage: 140 MB % 248.83/35.77 % (225280)Instructions burned: 4082 (million) % 248.83/35.77 % (225243)Instruction limit reached! % 248.83/35.77 % (225243)------------------------------ % 248.83/35.77 % (225243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.83/35.77 % (225243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.83/35.77 % (225243)CaDiCaL version: 2.1.3 % 248.83/35.77 % (225243)Termination reason: Instruction limit % 248.83/35.77 % (225243)Termination phase: Saturation % 248.83/35.77 % (225243)Time elapsed: 11.705 s % 248.83/35.77 % (225243)Peak memory usage: 137 MB % 248.83/35.77 % (225243)Instructions burned: 21175 (million) % 248.83/35.77 % (225287)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2998291503:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/6258Mi) % 248.83/35.77 % (225288)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=4261997773:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2808 on theBenchmark for (2808ds/34001Mi) % 248.83/35.77 % (225271)Instruction limit reached! % 285.37/40.97 % (225271)------------------------------ % 285.37/40.97 % (225271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/40.97 % (225271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/40.97 % (225271)CaDiCaL version: 2.1.3 % 285.37/40.97 % (225271)Termination reason: Instruction limit % 285.37/40.97 % (225271)Termination phase: Saturation % 285.37/40.97 % (225271)Time elapsed: 6.899 s % 285.37/40.97 % (225271)Peak memory usage: 94 MB % 285.37/40.97 % (225271)Instructions burned: 13800 (million) % 285.37/40.97 % (225291)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=642485828:s2a=on:i=71622:s2at=-1:rtra=on_2784 on theBenchmark for (2784ds/71622Mi) % 285.37/40.97 % (225287)Instruction limit reached! % 285.37/40.97 % (225287)------------------------------ % 285.37/40.97 % (225287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/40.97 % (225287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/40.97 % (225287)CaDiCaL version: 2.1.3 % 285.37/40.97 % (225287)Termination reason: Instruction limit % 285.37/40.97 % (225287)Termination phase: Saturation % 285.37/40.97 % (225287)Time elapsed: 3.180 s % 285.37/40.97 % (225287)Peak memory usage: 119 MB % 285.37/40.97 % (225287)Instructions burned: 6258 (million) % 285.37/40.97 % (225293)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3696897430:i=24001:kws=precedence:nm=0:rtra=on_2775 on theBenchmark for (2775ds/24001Mi) % 285.37/40.97 % (225275)Instruction limit reached! % 285.37/40.97 % (225275)------------------------------ % 285.37/40.97 % (225275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/40.97 % (225275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/40.97 % (225275)CaDiCaL version: 2.1.3 % 285.37/40.97 % (225275)Termination reason: Instruction limit % 285.37/40.97 % (225275)Termination phase: Saturation % 285.37/40.97 % (225275)Time elapsed: 7.689 s % 285.37/40.97 % (225275)Peak memory usage: 162 MB % 285.37/40.97 % (225275)Instructions burned: 11748 (million) % 285.37/40.97 % (225217)Instruction limit reached! % 285.37/40.97 % (225217)------------------------------ % 285.37/40.97 % (225217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/40.97 % (225217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/40.97 % (225217)CaDiCaL version: 2.1.3 % 285.37/40.97 % (225217)Termination reason: Instruction limit % 285.37/40.97 % (225217)Termination phase: Saturation % 285.37/40.97 % (225217)Time elapsed: 18.465 s % 285.37/40.97 % (225217)Peak memory usage: 94 MB % 285.37/40.97 % (225217)Instructions burned: 36817 (million) % 285.37/40.97 % (225295)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=857513568:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2768 on theBenchmark for (2768ds/2076Mi) % 285.37/40.97 % (225296)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=2074205761:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2767 on theBenchmark for (2767ds/83971Mi) % 285.37/40.97 % (225295)Instruction limit reached! % 285.37/40.97 % (225295)------------------------------ % 285.37/40.97 % (225295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/40.97 % (225295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/40.97 % (225295)CaDiCaL version: 2.1.3 % 285.37/40.97 % (225295)Termination reason: Instruction limit % 285.37/40.97 % (225295)Termination phase: Saturation % 285.37/40.97 % (225295)Time elapsed: 1.178 s % 285.37/40.97 % (225295)Peak memory usage: 124 MB % 285.37/40.97 % (225295)Instructions burned: 2076 (million) % 285.37/40.97 % (225299)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=246284716:i=83944:rtra=on_2755 on theBenchmark for (2755ds/83944Mi) % 285.37/40.97 % (225283)Instruction limit reached! % 285.37/40.97 % (225283)------------------------------ % 285.37/40.97 % (225283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.37/40.97 % (225283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.37/40.97 % (225283)CaDiCaL version: 2.1.3 % 285.37/40.97 % (225283)Termination reason: Instruction limit % 285.37/40.97 % (225283)Termination phase: Saturation % 285.37/40.97 % (225283)Time elapsed: 11.044 s % 285.37/40.97 % (225283)Peak memory usage: 135 MB % 285.37/40.97 % (225283)Instructions burned: 20260 (million) % 285.37/40.97 % (225301)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2632757316:i=9201:rtra=on_2715 on theBenchmark for (2715ds/9201Mi) % 295.90/42.31 % (225285)Instruction limit reached! % 295.90/42.31 % (225285)------------------------------ % 295.90/42.31 % (225285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.90/42.31 % (225285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.90/42.31 % (225285)CaDiCaL version: 2.1.3 % 295.90/42.31 % (225285)Termination reason: Instruction limit % 295.90/42.31 % (225285)Termination phase: Saturation % 295.90/42.31 % (225285)Time elapsed: 14.525 s % 295.90/42.31 % (225285)Peak memory usage: 97 MB % 295.90/42.31 % (225285)Instructions burned: 58629 (million) % 295.90/42.31 % (225303)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 % 295.90/42.31 % (225303)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3953409150:i=6806:aac=none:nm=0:rtra=on:rawr=on_2675 on theBenchmark for (2675ds/6806Mi) % 295.90/42.31 % (225301)Instruction limit reached! % 295.90/42.31 % (225301)------------------------------ % 295.90/42.31 % (225301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.90/42.31 % (225301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.90/42.31 % (225301)CaDiCaL version: 2.1.3 % 295.90/42.31 % (225301)Termination reason: Instruction limit % 295.90/42.31 % (225301)Termination phase: Saturation % 295.90/42.31 % (225301)Time elapsed: 4.136 s % 295.90/42.31 % (225301)Peak memory usage: 118 MB % 295.90/42.31 % (225301)Instructions burned: 9203 (million) % 295.90/42.31 % (225305)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2008133365:s2a=on:i=3553:nm=0:rtra=on_2672 on theBenchmark for (2672ds/3553Mi) % 295.90/42.31 % (225288)Instruction limit reached! % 295.90/42.31 % (225288)------------------------------ % 295.90/42.31 % (225288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.90/42.31 % (225288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.90/42.31 % (225288)CaDiCaL version: 2.1.3 % 295.90/42.31 % (225288)Termination reason: Instruction limit % 295.90/42.31 % (225288)Termination phase: Saturation % 295.90/42.31 % (225288)Time elapsed: 15.502 s % 295.90/42.31 % (225288)Peak memory usage: 472 MB % 295.90/42.31 % (225288)Instructions burned: 34002 (million) % 295.90/42.31 % (225303)Instruction limit reached! % 295.90/42.31 % (225303)------------------------------ % 295.90/42.31 % (225303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.90/42.31 % (225303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.90/42.31 % (225303)CaDiCaL version: 2.1.3 % 295.90/42.31 % (225303)Termination reason: Instruction limit % 295.90/42.31 % (225303)Termination phase: Saturation % 295.90/42.31 % (225303)Time elapsed: 2.336 s % 295.90/42.31 % (225303)Peak memory usage: 146 MB % 295.90/42.31 % (225303)Instructions burned: 6807 (million) % 295.90/42.31 % (225308)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=1426188598:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2650 on theBenchmark for (2650ds/20260Mi) % 295.90/42.31 % (225307)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=2028212172:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2651 on theBenchmark for (2651ds/2064Mi) % 295.90/42.31 % (225293)Instruction limit reached! % 295.90/42.31 % (225293)------------------------------ % 295.90/42.31 % (225293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.90/42.31 % (225293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.90/42.31 % (225293)CaDiCaL version: 2.1.3 % 295.90/42.31 % (225293)Termination reason: Instruction limit % 295.90/42.31 % (225293)Termination phase: Saturation % 295.90/42.31 % (225293)Time elapsed: 12.425 s % 295.90/42.31 % (225293)Peak memory usage: 156 MB % 295.90/42.31 % (225293)Instructions burned: 24003 (million) % 295.90/42.31 % (225305)Instruction limit reached! % 295.90/42.31 % (225305)------------------------------ % 295.90/42.31 % (225305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.90/42.31 % (225305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.90/42.31 % (225305)CaDiCaL version: 2.1.3 % 295.90/42.31 % (225305)Termination reason: Instruction limit % 295.90/42.31 % (225305)Termination phase: Saturation % 300.17/42.93 % (225305)Time elapsed: 2.182 s % 300.17/42.93 % (225305)Peak memory usage: 102 MB % 300.17/42.93 % (225305)Instructions burned: 3554 (million) % 300.17/42.93 % (225311)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=945844056:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2649 on theBenchmark for (2649ds/1244Mi) % 300.17/42.93 % (225312)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=1776274816:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2648 on theBenchmark for (2648ds/58261Mi) % 300.17/42.93 % (225311)Instruction limit reached! % 300.17/42.93 % (225311)------------------------------ % 300.17/42.93 % (225311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/42.93 % (225311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/42.93 % (225311)CaDiCaL version: 2.1.3 % 300.17/42.93 % (225311)Termination reason: Instruction limit % 300.17/42.93 % (225311)Termination phase: Saturation % 300.17/42.93 % (225311)Time elapsed: 0.675 s % 300.17/42.93 % (225311)Peak memory usage: 117 MB % 300.17/42.93 % (225311)Instructions burned: 1245 (million) % 300.17/42.93 % (225315)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 % 300.17/42.93 % (225315)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1904221110:i=6806:aac=none:nm=0:rtra=on:rawr=on_2640 on theBenchmark for (2640ds/6806Mi) % 300.17/42.93 % (225307)Instruction limit reached! % 300.17/42.93 % (225307)------------------------------ % 300.17/42.93 % (225307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/42.93 % (225307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/42.93 % (225307)CaDiCaL version: 2.1.3 % 300.17/42.93 % (225307)Termination reason: Instruction limit % 300.17/42.93 % (225307)Termination phase: Saturation % 300.17/42.93 % (225307)Time elapsed: 1.176 s % 300.17/42.93 % (225307)Peak memory usage: 141 MB % 300.17/42.93 % (225307)Instructions burned: 2065 (million) % 300.17/42.93 % (225317)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=132208218:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2637 on theBenchmark for (2637ds/4081Mi) % 300.17/42.93 % (225317)Instruction limit reached! % 300.17/42.93 % (225317)------------------------------ % 300.17/42.93 % (225317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/42.93 % (225317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/42.93 % (225317)CaDiCaL version: 2.1.3 % 300.17/42.93 % (225317)Termination reason: Instruction limit % 300.17/42.93 % (225317)Termination phase: Saturation % 300.17/42.93 % (225317)Time elapsed: 2.088 s % 300.17/42.93 % (225317)Peak memory usage: 141 MB % 300.17/42.93 % (225317)Instructions burned: 4082 (million) % 300.17/42.93 % (225319)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2651557211:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2615 on theBenchmark for (2615ds/1701Mi) % 300.17/42.93 % (225319)Instruction limit reached! % 300.17/42.93 % (225319)------------------------------ % 300.17/42.93 % (225319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/42.93 % (225319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/42.93 % (225319)CaDiCaL version: 2.1.3 % 300.17/42.93 % (225319)Termination reason: Instruction limit % 300.17/42.93 % (225319)Termination phase: Saturation % 300.17/42.93 % (225319)Time elapsed: 0.906 s % 300.17/42.93 % (225319)Peak memory usage: 117 MB % 300.17/42.93 % (225319)Instructions burned: 1702 (million) % 300.17/42.93 % (225321)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=496552137:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2604 on theBenchmark for (2604ds/57001Mi) % 300.17/42.93 % (225315)Instruction limit reached! % 300.17/42.93 % (225315)------------------------------ % 300.17/42.93 % (225315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/42.93 % (225315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/42.93 % (225315)CaDiCaL version: 2.1.3 % 300.17/42.93 % (225315)Termination reason: Instruction limit % 300.17/42.93 % (225315)Termination phase: Saturation % 300.17/42.93 % (225315)Time elaps % 300.17/42.94 Terminated %------------------------------------------------------------------------------