%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX115_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 : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:55 PM UTC 2026 % Result : Timeout 300.42s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX115_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.09/0.16 % Computer : n015.cluster.edu % 0.09/0.16 % Model : x86_64 x86_64 % 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.16 % Memory : 8046.5625MB % 0.09/0.16 % OS : Linux 6.8.0-71-generic % 0.09/0.16 % CPULimit : 300 % 0.09/0.16 % WCLimit : 300 % 0.09/0.16 % DateTime : Mon Sep 28 15:05:17 UTC 2026 % 0.09/0.16 % CPUTime : % 0.09/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.20 Running first-order theorem proving % 0.09/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.58/1.16 % (2697415)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.58/1.16 % (2697443)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1418074078:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.58/1.16 % (2697443)Instruction limit reached! % 3.58/1.16 % (2697443)------------------------------ % 3.58/1.16 % (2697443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.58/1.16 % (2697443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/1.16 % (2697443)CaDiCaL version: 2.1.3 % 3.58/1.16 % (2697443)Termination reason: Instruction limit % 3.58/1.16 % (2697443)Termination phase: Saturation % 3.58/1.16 % (2697443)Time elapsed: 0.003 s % 3.58/1.16 % (2697443)Peak memory usage: 88 MB % 3.58/1.16 % (2697443)Instructions burned: 9 (million) % 3.58/1.16 % (2697446)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3344604069:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.58/1.16 % (2697444)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1211124274:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.58/1.16 % (2697445)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3064460181:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.58/1.16 % (2697442)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3115534585:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.58/1.16 % (2697440)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3472047076:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.58/1.16 % (2697441)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3748143783:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.58/1.16 % (2697444)Instruction limit reached! % 3.58/1.16 % (2697444)------------------------------ % 3.58/1.16 % (2697444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.58/1.16 % (2697444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/1.16 % (2697444)CaDiCaL version: 2.1.3 % 3.58/1.16 % (2697444)Termination reason: Instruction limit % 3.58/1.16 % (2697444)Termination phase: Property scanning % 3.58/1.16 % (2697444)Time elapsed: 0.003 s % 3.58/1.16 % (2697444)Peak memory usage: 86 MB % 3.58/1.16 % (2697444)Instructions burned: 4 (million) % 3.58/1.16 % (2697440)Instruction limit reached! % 3.58/1.16 % (2697440)------------------------------ % 3.58/1.16 % (2697440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.58/1.16 % (2697440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/1.16 % (2697440)CaDiCaL version: 2.1.3 % 3.58/1.16 % (2697440)Termination reason: Instruction limit % 3.58/1.16 % (2697440)Termination phase: Saturation % 3.58/1.16 % (2697440)Time elapsed: 0.027 s % 3.58/1.16 % (2697440)Peak memory usage: 110 MB % 3.58/1.16 % (2697440)Instructions burned: 12 (million) % 3.58/1.16 % (2697446)Instruction limit reached! % 3.58/1.16 % (2697446)------------------------------ % 3.58/1.16 % (2697446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.58/1.16 % (2697446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/1.16 % (2697446)CaDiCaL version: 2.1.3 % 3.58/1.16 % (2697446)Termination reason: Instruction limit % 3.58/1.16 % (2697446)Termination phase: Saturation % 3.58/1.16 % (2697446)Time elapsed: 0.045 s % 3.58/1.16 % (2697446)Peak memory usage: 116 MB % 3.58/1.16 % (2697446)Instructions burned: 34 (million) % 3.58/1.16 % (2697445)Instruction limit reached! % 3.58/1.16 % (2697445)------------------------------ % 3.58/1.16 % (2697445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.58/1.16 % (2697445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/1.16 % (2697445)CaDiCaL version: 2.1.3 % 3.58/1.16 % (2697445)Termination reason: Instruction limit % 3.58/1.16 % (2697445)Termination phase: Saturation % 3.58/1.16 % (2697445)Time elapsed: 0.055 s % 3.58/1.16 % (2697445)Peak memory usage: 116 MB % 3.58/1.16 % (2697445)Instructions burned: 47 (million) % 3.58/1.16 % (2697448)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4007512202:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.58/1.16 % (2697448)Instruction limit reached! % 3.58/1.16 % (2697448)------------------------------ % 3.97/1.29 % (2697448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.97/1.29 % (2697448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/1.29 % (2697448)CaDiCaL version: 2.1.3 % 3.97/1.29 % (2697448)Termination reason: Instruction limit % 3.97/1.29 % (2697448)Termination phase: Saturation % 3.97/1.29 % (2697448)Time elapsed: 0.005 s % 3.97/1.29 % (2697448)Peak memory usage: 89 MB % 3.97/1.29 % (2697448)Instructions burned: 15 (million) % 3.97/1.29 % (2697455)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=2027272015:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 3.97/1.29 % (2697442)Instruction limit reached! % 3.97/1.29 % (2697442)------------------------------ % 3.97/1.29 % (2697442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.97/1.29 % (2697442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/1.29 % (2697442)CaDiCaL version: 2.1.3 % 3.97/1.29 % (2697442)Termination reason: Instruction limit % 3.97/1.29 % (2697442)Termination phase: Saturation % 3.97/1.29 % (2697442)Time elapsed: 0.149 s % 3.97/1.29 % (2697442)Peak memory usage: 118 MB % 3.97/1.29 % (2697442)Instructions burned: 203 (million) % 3.97/1.29 % (2697455)Instruction limit reached! % 3.97/1.29 % (2697455)------------------------------ % 3.97/1.29 % (2697455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.97/1.29 % (2697455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/1.29 % (2697455)CaDiCaL version: 2.1.3 % 3.97/1.29 % (2697455)Termination reason: Instruction limit % 3.97/1.29 % (2697455)Termination phase: Saturation % 3.97/1.29 % (2697455)Time elapsed: 0.022 s % 3.97/1.29 % (2697455)Peak memory usage: 89 MB % 3.97/1.29 % (2697455)Instructions burned: 29 (million) % 3.97/1.29 % (2697460)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1490862111:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 3.97/1.29 % (2697456)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1913613142:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 3.97/1.29 % (2697456)Instruction limit reached! % 3.97/1.29 % (2697456)------------------------------ % 3.97/1.29 % (2697456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.97/1.29 % (2697456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/1.29 % (2697456)CaDiCaL version: 2.1.3 % 3.97/1.29 % (2697456)Termination reason: Instruction limit % 3.97/1.29 % (2697456)Termination phase: Saturation % 3.97/1.29 % (2697456)Time elapsed: 0.010 s % 3.97/1.29 % (2697456)Peak memory usage: 89 MB % 3.97/1.29 % (2697456)Instructions burned: 16 (million) % 3.97/1.29 % (2697457)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2666862833:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 3.97/1.29 % (2697460)Instruction limit reached! % 3.97/1.29 % (2697460)------------------------------ % 3.97/1.29 % (2697460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.97/1.29 % (2697460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/1.29 % (2697460)CaDiCaL version: 2.1.3 % 3.97/1.29 % (2697460)Termination reason: Instruction limit % 3.97/1.29 % (2697460)Termination phase: Saturation % 3.97/1.29 % (2697460)Time elapsed: 0.026 s % 3.97/1.29 % (2697460)Peak memory usage: 89 MB % 3.97/1.29 % (2697460)Instructions burned: 85 (million) % 3.97/1.29 % (2697459)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=72563479:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 3.97/1.29 % (2697457)Instruction limit reached! % 3.97/1.29 % (2697457)------------------------------ % 3.97/1.29 % (2697457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.97/1.29 % (2697457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/1.29 % (2697457)CaDiCaL version: 2.1.3 % 3.97/1.29 % (2697457)Termination reason: Instruction limit % 3.97/1.29 % (2697457)Termination phase: Saturation % 3.97/1.29 % (2697457)Time elapsed: 0.017 s % 3.97/1.29 % (2697457)Peak memory usage: 89 MB % 3.97/1.29 % (2697457)Instructions burned: 24 (million) % 3.97/1.29 % (2697459)Instruction limit reached! % 3.97/1.29 % (2697459)------------------------------ % 3.97/1.29 % (2697459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.94/1.45 % (2697459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.94/1.45 % (2697459)CaDiCaL version: 2.1.3 % 4.94/1.45 % (2697459)Termination reason: Instruction limit % 4.94/1.45 % (2697459)Termination phase: Saturation % 4.94/1.45 % (2697459)Time elapsed: 0.017 s % 4.94/1.45 % (2697459)Peak memory usage: 90 MB % 4.94/1.45 % (2697459)Instructions burned: 28 (million) % 4.94/1.45 % (2697441)Instruction limit reached! % 4.94/1.45 % (2697441)------------------------------ % 4.94/1.45 % (2697441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.94/1.45 % (2697441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.94/1.45 % (2697441)CaDiCaL version: 2.1.3 % 4.94/1.45 % (2697441)Termination reason: Instruction limit % 4.94/1.45 % (2697441)Termination phase: Saturation % 4.94/1.45 % (2697441)Time elapsed: 0.221 s % 4.94/1.45 % (2697441)Peak memory usage: 117 MB % 4.94/1.45 % (2697441)Instructions burned: 308 (million) % 4.94/1.45 % (2697466)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1386747796:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 4.94/1.45 % (2697466)Instruction limit reached! % 4.94/1.45 % (2697466)------------------------------ % 4.94/1.45 % (2697466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.94/1.45 % (2697466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.94/1.45 % (2697466)CaDiCaL version: 2.1.3 % 4.94/1.45 % (2697466)Termination reason: Instruction limit % 4.94/1.45 % (2697466)Termination phase: Equality resolution with deletion % 4.94/1.45 % (2697466)Time elapsed: 0.002 s % 4.94/1.45 % (2697466)Peak memory usage: 86 MB % 4.94/1.45 % (2697466)Instructions burned: 6 (million) % 4.94/1.45 % (2697462)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=454461392:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 4.94/1.45 % (2697462)Instruction limit reached! % 4.94/1.45 % (2697462)------------------------------ % 4.94/1.45 % (2697462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.94/1.45 % (2697462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.94/1.45 % (2697462)CaDiCaL version: 2.1.3 % 4.94/1.45 % (2697462)Termination reason: Instruction limit % 4.94/1.45 % (2697462)Termination phase: Preprocessing 3 % 4.94/1.45 % (2697462)Time elapsed: 0.002 s % 4.94/1.45 % (2697462)Peak memory usage: 86 MB % 4.94/1.45 % (2697462)Instructions burned: 2 (million) % 4.94/1.45 % (2697465)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=465041998:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 4.94/1.45 % (2697469)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3764272747:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 4.94/1.45 % (2697470)lrs+10_1_thi=all:si=on:fd=off:random_seed=3823573339:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 4.94/1.45 % (2697471)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=1055169676:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 4.94/1.45 % (2697471)Instruction limit reached! % 4.94/1.45 % (2697471)------------------------------ % 4.94/1.45 % (2697471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.94/1.45 % (2697471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.94/1.45 % (2697471)CaDiCaL version: 2.1.3 % 4.94/1.45 % (2697471)Termination reason: Instruction limit % 4.94/1.45 % (2697471)Termination phase: Property scanning % 4.94/1.45 % (2697471)Time elapsed: 0.005 s % 4.94/1.45 % (2697471)Peak memory usage: 87 MB % 4.94/1.45 % (2697471)Instructions burned: 9 (million) % 4.94/1.45 % (2697472)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2821568723:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 4.94/1.45 % (2697472)Instruction limit reached! % 4.94/1.45 % (2697472)------------------------------ % 4.94/1.45 % (2697472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.94/1.45 % (2697472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.94/1.45 % (2697472)CaDiCaL version: 2.1.3 % 4.94/1.45 % (2697472)Termination reason: Instruction limit % 6.34/1.69 % (2697472)Termination phase: Preprocessing 3 % 6.34/1.69 % (2697472)Time elapsed: 0.002 s % 6.34/1.69 % (2697472)Peak memory usage: 86 MB % 6.34/1.69 % (2697472)Instructions burned: 2 (million) % 6.34/1.69 % (2697470)Instruction limit reached! % 6.34/1.69 % (2697470)------------------------------ % 6.34/1.69 % (2697470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.34/1.69 % (2697470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.34/1.69 % (2697470)CaDiCaL version: 2.1.3 % 6.34/1.69 % (2697470)Termination reason: Instruction limit % 6.34/1.69 % (2697470)Termination phase: Saturation % 6.34/1.69 % (2697470)Time elapsed: 0.059 s % 6.34/1.69 % (2697470)Peak memory usage: 116 MB % 6.34/1.69 % (2697470)Instructions burned: 53 (million) % 6.34/1.69 % (2697474)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2557331167:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.34/1.69 % (2697474)Instruction limit reached! % 6.34/1.69 % (2697474)------------------------------ % 6.34/1.69 % (2697474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.34/1.69 % (2697474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.34/1.69 % (2697474)CaDiCaL version: 2.1.3 % 6.34/1.69 % (2697474)Termination reason: Instruction limit % 6.34/1.69 % (2697474)Termination phase: Preprocessing 3 % 6.34/1.69 % (2697474)Time elapsed: 0.001 s % 6.34/1.69 % (2697474)Peak memory usage: 86 MB % 6.34/1.69 % (2697474)Instructions burned: 2 (million) % 6.34/1.69 % (2697465)Instruction limit reached! % 6.34/1.69 % (2697465)------------------------------ % 6.34/1.69 % (2697465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.34/1.69 % (2697465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.34/1.69 % (2697465)CaDiCaL version: 2.1.3 % 6.34/1.69 % (2697465)Termination reason: Instruction limit % 6.34/1.69 % (2697465)Termination phase: Saturation % 6.34/1.69 % (2697465)Time elapsed: 0.099 s % 6.34/1.69 % (2697465)Peak memory usage: 90 MB % 6.34/1.69 % (2697465)Instructions burned: 181 (million) % 6.34/1.69 % (2697469)Instruction limit reached! % 6.34/1.69 % (2697469)------------------------------ % 6.34/1.69 % (2697469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.34/1.69 % (2697469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.34/1.69 % (2697469)CaDiCaL version: 2.1.3 % 6.34/1.69 % (2697469)Termination reason: Instruction limit % 6.34/1.69 % (2697469)Termination phase: Saturation % 6.34/1.69 % (2697469)Time elapsed: 0.088 s % 6.34/1.69 % (2697469)Peak memory usage: 134 MB % 6.34/1.69 % (2697469)Instructions burned: 66 (million) % 6.34/1.69 % (2697477)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3579142799:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.34/1.69 % (2697485)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3700338706:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi) % 6.34/1.69 % (2697485)Instruction limit reached! % 6.34/1.69 % (2697485)------------------------------ % 6.34/1.69 % (2697485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.34/1.69 % (2697485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.34/1.69 % (2697485)CaDiCaL version: 2.1.3 % 6.34/1.69 % (2697485)Termination reason: Instruction limit % 6.34/1.69 % (2697485)Termination phase: Saturation % 6.34/1.69 % (2697485)Time elapsed: 0.015 s % 6.34/1.69 % (2697485)Peak memory usage: 89 MB % 6.34/1.69 % (2697485)Instructions burned: 37 (million) % 6.34/1.69 % (2697482)dis+10_1_si=on:random_seed=3234652899:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.34/1.69 % (2697482)Instruction limit reached! % 6.34/1.69 % (2697482)------------------------------ % 6.34/1.69 % (2697482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.34/1.69 % (2697482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.34/1.69 % (2697482)CaDiCaL version: 2.1.3 % 6.34/1.69 % (2697482)Termination reason: Instruction limit % 6.34/1.69 % (2697482)Termination phase: Saturation % 6.34/1.69 % (2697482)Time elapsed: 0.006 s % 6.34/1.69 % (2697482)Peak memory usage: 88 MB % 6.34/1.69 % (2697482)Instructions burned: 10 (million) % 6.34/1.69 % (2697483)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=708124871:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 7.70/1.88 % (2697483)Refutation not found, incomplete strategy % 7.70/1.88 % (2697483)------------------------------ % 7.70/1.88 % (2697483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.70/1.88 % (2697483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.88 % (2697483)CaDiCaL version: 2.1.3 % 7.70/1.88 % (2697483)Termination reason: Refutation not found, incomplete strategy % 7.70/1.88 % (2697483)Time elapsed: 0.008 s % 7.70/1.88 % (2697483)Peak memory usage: 89 MB % 7.70/1.88 % (2697483)Instructions burned: 12 (million) % 7.70/1.88 % (2697487)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2477727209:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.70/1.88 % (2697486)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1666575200:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.70/1.88 % (2697486)Instruction limit reached! % 7.70/1.88 % (2697486)------------------------------ % 7.70/1.88 % (2697486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.70/1.88 % (2697486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.88 % (2697486)CaDiCaL version: 2.1.3 % 7.70/1.88 % (2697486)Termination reason: Instruction limit % 7.70/1.88 % (2697486)Termination phase: Preprocessing 3 % 7.70/1.88 % (2697486)Time elapsed: 0.002 s % 7.70/1.88 % (2697486)Peak memory usage: 86 MB % 7.70/1.88 % (2697486)Instructions burned: 2 (million) % 7.70/1.88 % (2697487)Instruction limit reached! % 7.70/1.88 % (2697487)------------------------------ % 7.70/1.88 % (2697487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.70/1.88 % (2697487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.88 % (2697487)CaDiCaL version: 2.1.3 % 7.70/1.88 % (2697487)Termination reason: Instruction limit % 7.70/1.88 % (2697487)Termination phase: Saturation % 7.70/1.88 % (2697487)Time elapsed: 0.005 s % 7.70/1.88 % (2697487)Peak memory usage: 88 MB % 7.70/1.88 % (2697487)Instructions burned: 9 (million) % 7.70/1.88 % (2697477)Instruction limit reached! % 7.70/1.88 % (2697477)------------------------------ % 7.70/1.88 % (2697477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.70/1.88 % (2697477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.88 % (2697477)CaDiCaL version: 2.1.3 % 7.70/1.88 % (2697477)Termination reason: Instruction limit % 7.70/1.88 % (2697477)Termination phase: Saturation % 7.70/1.88 % (2697477)Time elapsed: 0.109 s % 7.70/1.88 % (2697477)Peak memory usage: 117 MB % 7.70/1.88 % (2697477)Instructions burned: 128 (million) % 7.70/1.88 % (2697488)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=106337513:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 7.70/1.88 % (2697488)Refutation not found, incomplete strategy % 7.70/1.88 % (2697488)------------------------------ % 7.70/1.88 % (2697488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.70/1.88 % (2697488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.88 % (2697488)CaDiCaL version: 2.1.3 % 7.70/1.88 % (2697488)Termination reason: Refutation not found, incomplete strategy % 7.70/1.88 % (2697488)Time elapsed: 0.012 s % 7.70/1.88 % (2697488)Peak memory usage: 89 MB % 7.70/1.88 % (2697488)Instructions burned: 18 (million) % 7.70/1.88 % (2697491)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=76673417:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.70/1.88 % (2697494)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=537901643:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.70/1.88 % (2697491)Instruction limit reached! % 7.70/1.88 % (2697491)------------------------------ % 7.70/1.88 % (2697491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.70/1.88 % (2697491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.70/1.88 % (2697491)CaDiCaL version: 2.1.3 % 7.70/1.88 % (2697491)Termination reason: Instruction limit % 7.70/1.88 % (2697491)Termination phase: Saturation % 7.70/1.88 % (2697491)Time elapsed: 0.030 s % 7.70/1.88 % (2697491)Peak memory usage: 112 MB % 7.70/1.88 % (2697491)Instructions burned: 13 (million) % 7.70/1.88 % (2697498)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4281842610:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 10.03/2.12 % (2697497)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3619518980:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 10.03/2.12 % (2697497)Instruction limit reached! % 10.03/2.12 % (2697497)------------------------------ % 10.03/2.12 % (2697497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.03/2.12 % (2697497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.03/2.12 % (2697497)CaDiCaL version: 2.1.3 % 10.03/2.12 % (2697497)Termination reason: Instruction limit % 10.03/2.12 % (2697497)Termination phase: Saturation % 10.03/2.12 % (2697497)Time elapsed: 0.007 s % 10.03/2.12 % (2697497)Peak memory usage: 88 MB % 10.03/2.12 % (2697497)Instructions burned: 11 (million) % 10.03/2.12 % (2697500)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=3419083997:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 10.03/2.12 % (2697500)Instruction limit reached! % 10.03/2.12 % (2697500)------------------------------ % 10.03/2.12 % (2697500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.03/2.12 % (2697500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.03/2.12 % (2697500)CaDiCaL version: 2.1.3 % 10.03/2.12 % (2697500)Termination reason: Instruction limit % 10.03/2.12 % (2697500)Termination phase: Saturation % 10.03/2.12 % (2697500)Time elapsed: 0.053 s % 10.03/2.12 % (2697500)Peak memory usage: 91 MB % 10.03/2.12 % (2697500)Instructions burned: 76 (million) % 10.03/2.12 % (2697498)Instruction limit reached! % 10.03/2.12 % (2697498)------------------------------ % 10.03/2.12 % (2697498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.03/2.12 % (2697498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.03/2.12 % (2697498)CaDiCaL version: 2.1.3 % 10.03/2.12 % (2697498)Termination reason: Instruction limit % 10.03/2.12 % (2697498)Termination phase: Saturation % 10.03/2.12 % (2697498)Time elapsed: 0.089 s % 10.03/2.12 % (2697498)Peak memory usage: 133 MB % 10.03/2.12 % (2697498)Instructions burned: 72 (million) % 10.03/2.12 % (2697483)------------------------------ % 10.03/2.12 % (2697483)------------------------------ % 10.03/2.12 % (2697503)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=255758717:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.03/2.12 % (2697494)Instruction limit reached! % 10.03/2.12 % (2697494)------------------------------ % 10.03/2.12 % (2697494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.03/2.12 % (2697494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.03/2.12 % (2697494)CaDiCaL version: 2.1.3 % 10.03/2.12 % (2697494)Termination reason: Instruction limit % 10.03/2.12 % (2697494)Termination phase: Saturation % 10.03/2.12 % (2697494)Time elapsed: 0.165 s % 10.03/2.12 % (2697494)Peak memory usage: 120 MB % 10.03/2.12 % (2697494)Instructions burned: 227 (million) % 10.03/2.12 % (2697488)------------------------------ % 10.03/2.12 % (2697488)------------------------------ % 10.03/2.12 % (2697507)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3766725619:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi) % 10.03/2.12 % (2697503)Instruction limit reached! % 10.03/2.12 % (2697503)------------------------------ % 10.03/2.12 % (2697503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.03/2.12 % (2697503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.03/2.12 % (2697503)CaDiCaL version: 2.1.3 % 10.03/2.12 % (2697503)Termination reason: Instruction limit % 10.03/2.12 % (2697503)Termination phase: Saturation % 10.03/2.12 % (2697503)Time elapsed: 0.099 s % 10.03/2.12 % (2697503)Peak memory usage: 91 MB % 10.03/2.12 % (2697503)Instructions burned: 294 (million) % 10.03/2.12 % (2697508)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1850834351:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.03/2.12 % (2697510)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=4259903906:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 10.03/2.12 % (2697511)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2321568928:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 11.66/2.42 % (2697507)Instruction limit reached! % 11.66/2.42 % (2697507)------------------------------ % 11.66/2.42 % (2697507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.42 % (2697507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.42 % (2697507)CaDiCaL version: 2.1.3 % 11.66/2.42 % (2697507)Termination reason: Instruction limit % 11.66/2.42 % (2697507)Termination phase: Saturation % 11.66/2.42 % (2697507)Time elapsed: 0.111 s % 11.66/2.42 % (2697507)Peak memory usage: 116 MB % 11.66/2.42 % (2697507)Instructions burned: 131 (million) % 11.66/2.42 % (2697512)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3996692503:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 11.66/2.42 % (2697510)Instruction limit reached! % 11.66/2.42 % (2697510)------------------------------ % 11.66/2.42 % (2697510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.42 % (2697510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.42 % (2697510)CaDiCaL version: 2.1.3 % 11.66/2.42 % (2697510)Termination reason: Instruction limit % 11.66/2.42 % (2697510)Termination phase: Saturation % 11.66/2.42 % (2697510)Time elapsed: 0.067 s % 11.66/2.42 % (2697510)Peak memory usage: 134 MB % 11.66/2.42 % (2697510)Instructions burned: 41 (million) % 11.66/2.42 % (2697514)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3303602986:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.66/2.42 % (2697515)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=2640747528:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 11.66/2.42 % (2697508)Instruction limit reached! % 11.66/2.42 % (2697508)------------------------------ % 11.66/2.42 % (2697508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.42 % (2697508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.42 % (2697508)CaDiCaL version: 2.1.3 % 11.66/2.42 % (2697508)Termination reason: Instruction limit % 11.66/2.42 % (2697508)Termination phase: Saturation % 11.66/2.42 % (2697508)Time elapsed: 0.138 s % 11.66/2.42 % (2697508)Peak memory usage: 134 MB % 11.66/2.42 % (2697508)Instructions burned: 132 (million) % 11.66/2.42 % (2697514)Instruction limit reached! % 11.66/2.42 % (2697514)------------------------------ % 11.66/2.42 % (2697514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.42 % (2697514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.42 % (2697514)CaDiCaL version: 2.1.3 % 11.66/2.42 % (2697514)Termination reason: Instruction limit % 11.66/2.42 % (2697514)Termination phase: Saturation % 11.66/2.42 % (2697514)Time elapsed: 0.101 s % 11.66/2.42 % (2697514)Peak memory usage: 117 MB % 11.66/2.42 % (2697514)Instructions burned: 132 (million) % 11.66/2.42 % (2697519)dis+10_1_si=on:random_seed=304034974:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.66/2.42 % (2697515)Instruction limit reached! % 11.66/2.42 % (2697515)------------------------------ % 11.66/2.42 % (2697515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.42 % (2697515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.42 % (2697515)CaDiCaL version: 2.1.3 % 11.66/2.42 % (2697515)Termination reason: Instruction limit % 11.66/2.42 % (2697515)Termination phase: Saturation % 11.66/2.42 % (2697515)Time elapsed: 0.101 s % 11.66/2.42 % (2697515)Peak memory usage: 119 MB % 11.66/2.42 % (2697515)Instructions burned: 264 (million) % 11.66/2.42 % (2697523)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3344985010:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 11.66/2.42 % (2697511)Instruction limit reached! % 11.66/2.42 % (2697511)------------------------------ % 11.66/2.42 % (2697511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.66/2.42 % (2697511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.66/2.42 % (2697511)CaDiCaL version: 2.1.3 % 11.66/2.42 % (2697511)Termination reason: Instruction limit % 11.66/2.42 % (2697511)Termination phase: Saturation % 11.66/2.42 % (2697511)Time elapsed: 0.197 s % 11.66/2.42 % (2697511)Peak memory usage: 92 MB % 11.66/2.42 % (2697511)Instructions burned: 308 (million) % 13.40/2.70 % (2697524)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2924159033:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.40/2.70 % (2697527)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3633891203:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 13.40/2.70 % (2697525)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2220934505:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.40/2.70 % (2697527)Instruction limit reached! % 13.40/2.70 % (2697527)------------------------------ % 13.40/2.70 % (2697527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.70 % (2697527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.70 % (2697527)CaDiCaL version: 2.1.3 % 13.40/2.70 % (2697527)Termination reason: Instruction limit % 13.40/2.70 % (2697527)Termination phase: Saturation % 13.40/2.70 % (2697527)Time elapsed: 0.039 s % 13.40/2.70 % (2697527)Peak memory usage: 89 MB % 13.40/2.70 % (2697527)Instructions burned: 124 (million) % 13.40/2.70 % (2697524)Instruction limit reached! % 13.40/2.70 % (2697524)------------------------------ % 13.40/2.70 % (2697524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.70 % (2697524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.70 % (2697524)CaDiCaL version: 2.1.3 % 13.40/2.70 % (2697524)Termination reason: Instruction limit % 13.40/2.70 % (2697524)Termination phase: Saturation % 13.40/2.70 % (2697524)Time elapsed: 0.084 s % 13.40/2.70 % (2697524)Peak memory usage: 90 MB % 13.40/2.70 % (2697524)Instructions burned: 149 (million) % 13.40/2.70 % (2697529)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=2197897560:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.40/2.70 % (2697525)Instruction limit reached! % 13.40/2.70 % (2697525)------------------------------ % 13.40/2.70 % (2697525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.70 % (2697525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.70 % (2697525)CaDiCaL version: 2.1.3 % 13.40/2.70 % (2697525)Termination reason: Instruction limit % 13.40/2.70 % (2697525)Termination phase: Saturation % 13.40/2.70 % (2697525)Time elapsed: 0.065 s % 13.40/2.70 % (2697525)Peak memory usage: 116 MB % 13.40/2.70 % (2697525)Instructions burned: 66 (million) % 13.40/2.70 % (2697533)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=312276807:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.40/2.70 % (2697523)Instruction limit reached! % 13.40/2.70 % (2697523)------------------------------ % 13.40/2.70 % (2697523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.70 % (2697523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.70 % (2697523)CaDiCaL version: 2.1.3 % 13.40/2.70 % (2697523)Termination reason: Instruction limit % 13.40/2.70 % (2697523)Termination phase: Saturation % 13.40/2.70 % (2697523)Time elapsed: 0.210 s % 13.40/2.70 % (2697523)Peak memory usage: 92 MB % 13.40/2.70 % (2697523)Instructions burned: 384 (million) % 13.40/2.70 % (2697533)Instruction limit reached! % 13.40/2.70 % (2697533)------------------------------ % 13.40/2.70 % (2697533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.70 % (2697533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.70 % (2697533)CaDiCaL version: 2.1.3 % 13.40/2.70 % (2697533)Termination reason: Instruction limit % 13.40/2.70 % (2697533)Termination phase: Saturation % 13.40/2.70 % (2697533)Time elapsed: 0.028 s % 13.40/2.70 % (2697533)Peak memory usage: 118 MB % 13.40/2.70 % (2697533)Instructions burned: 41 (million) % 13.40/2.70 % (2697512)Instruction limit reached! % 13.40/2.70 % (2697512)------------------------------ % 13.40/2.70 % (2697512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.40/2.70 % (2697512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.40/2.70 % (2697512)CaDiCaL version: 2.1.3 % 13.40/2.70 % (2697512)Termination reason: Instruction limit % 13.40/2.70 % (2697512)Termination phase: Saturation % 13.40/2.70 % (2697512)Time elapsed: 0.369 s % 13.40/2.70 % (2697512)Peak memory usage: 139 MB % 13.40/2.70 % (2697512)Instructions burned: 598 (million) % 13.40/2.70 % (2697529)Instruction limit reached! % 13.40/2.70 % (2697529)------------------------------ % 13.40/2.70 % (2697529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.06/2.96 % (2697529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.06/2.96 % (2697529)CaDiCaL version: 2.1.3 % 15.06/2.96 % (2697529)Termination reason: Instruction limit % 15.06/2.96 % (2697529)Termination phase: Saturation % 15.06/2.96 % (2697529)Time elapsed: 0.097 s % 15.06/2.96 % (2697529)Peak memory usage: 118 MB % 15.06/2.96 % (2697529)Instructions burned: 129 (million) % 15.06/2.96 % (2697534)dis+1010_1_to=kbo:si=on:random_seed=3983181365:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 15.06/2.96 % (2697536)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1686618322:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 15.06/2.96 % (2697539)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2947370888:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.06/2.96 % (2697538)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3647817442:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.06/2.96 % (2697540)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1340825799:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.06/2.96 % (2697534)Instruction limit reached! % 15.06/2.96 % (2697534)------------------------------ % 15.06/2.96 % (2697534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.06/2.96 % (2697534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.06/2.96 % (2697534)CaDiCaL version: 2.1.3 % 15.06/2.96 % (2697534)Termination reason: Instruction limit % 15.06/2.96 % (2697534)Termination phase: Saturation % 15.06/2.96 % (2697534)Time elapsed: 0.093 s % 15.06/2.96 % (2697534)Peak memory usage: 91 MB % 15.06/2.96 % (2697534)Instructions burned: 176 (million) % 15.06/2.96 % (2697539)Instruction limit reached! % 15.06/2.96 % (2697539)------------------------------ % 15.06/2.96 % (2697539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.06/2.96 % (2697539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.06/2.96 % (2697539)CaDiCaL version: 2.1.3 % 15.06/2.96 % (2697539)Termination reason: Instruction limit % 15.06/2.96 % (2697539)Termination phase: Saturation % 15.06/2.96 % (2697539)Time elapsed: 0.090 s % 15.06/2.96 % (2697539)Peak memory usage: 135 MB % 15.06/2.96 % (2697539)Instructions burned: 216 (million) % 15.06/2.96 % (2697542)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=233829622:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 15.06/2.96 % (2697549)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=195903804:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 15.06/2.96 % (2697547)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=905074700:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi) % 15.06/2.96 % (2697536)Instruction limit reached! % 15.06/2.96 % (2697536)------------------------------ % 15.06/2.96 % (2697536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.06/2.96 % (2697536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.06/2.96 % (2697536)CaDiCaL version: 2.1.3 % 15.06/2.96 % (2697536)Termination reason: Instruction limit % 15.06/2.96 % (2697536)Termination phase: Saturation % 15.06/2.96 % (2697536)Time elapsed: 0.219 s % 15.06/2.96 % (2697536)Peak memory usage: 118 MB % 15.06/2.96 % (2697536)Instructions burned: 330 (million) % 15.06/2.96 % (2697519)Instruction limit reached! % 15.06/2.96 % (2697519)------------------------------ % 15.06/2.96 % (2697519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.06/2.96 % (2697519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.06/2.96 % (2697519)CaDiCaL version: 2.1.3 % 15.06/2.96 % (2697519)Termination reason: Instruction limit % 15.06/2.96 % (2697519)Termination phase: Saturation % 15.06/2.96 % (2697519)Time elapsed: 0.566 s % 15.06/2.96 % (2697519)Peak memory usage: 95 MB % 15.06/2.96 % (2697519)Instructions burned: 1001 (million) % 15.06/2.96 % (2697542)Instruction limit reached! % 15.06/2.96 % (2697542)------------------------------ % 15.06/2.96 % (2697542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.06/2.96 % (2697542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.18 % (2697542)CaDiCaL version: 2.1.3 % 17.78/3.18 % (2697542)Termination reason: Instruction limit % 17.78/3.18 % (2697542)Termination phase: Saturation % 17.78/3.18 % (2697542)Time elapsed: 0.155 s % 17.78/3.18 % (2697542)Peak memory usage: 90 MB % 17.78/3.18 % (2697542)Instructions burned: 296 (million) % 17.78/3.18 % (2697549)Instruction limit reached! % 17.78/3.18 % (2697549)------------------------------ % 17.78/3.18 % (2697549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.18 % (2697549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.18 % (2697549)CaDiCaL version: 2.1.3 % 17.78/3.18 % (2697549)Termination reason: Instruction limit % 17.78/3.18 % (2697549)Termination phase: Saturation % 17.78/3.18 % (2697549)Time elapsed: 0.100 s % 17.78/3.18 % (2697549)Peak memory usage: 118 MB % 17.78/3.18 % (2697549)Instructions burned: 284 (million) % 17.78/3.18 % (2697540)Instruction limit reached! % 17.78/3.18 % (2697540)------------------------------ % 17.78/3.18 % (2697540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.18 % (2697540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.18 % (2697540)CaDiCaL version: 2.1.3 % 17.78/3.18 % (2697540)Termination reason: Instruction limit % 17.78/3.18 % (2697540)Termination phase: Saturation % 17.78/3.18 % (2697540)Time elapsed: 0.246 s % 17.78/3.18 % (2697540)Peak memory usage: 117 MB % 17.78/3.18 % (2697540)Instructions burned: 349 (million) % 17.78/3.18 % (2697552)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=590062542:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 17.78/3.18 % (2697553)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3534854817:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.78/3.18 % (2697554)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3772727114:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 17.78/3.18 % (2697555)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4243621985:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 17.78/3.18 % (2697547)Instruction limit reached! % 17.78/3.18 % (2697547)------------------------------ % 17.78/3.18 % (2697547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.18 % (2697547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.18 % (2697547)CaDiCaL version: 2.1.3 % 17.78/3.18 % (2697547)Termination reason: Instruction limit % 17.78/3.18 % (2697547)Termination phase: Saturation % 17.78/3.18 % (2697547)Time elapsed: 0.199 s % 17.78/3.18 % (2697547)Peak memory usage: 118 MB % 17.78/3.18 % (2697547)Instructions burned: 329 (million) % 17.78/3.18 % (2697538)Instruction limit reached! % 17.78/3.18 % (2697538)------------------------------ % 17.78/3.18 % (2697538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.18 % (2697538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.18 % (2697538)CaDiCaL version: 2.1.3 % 17.78/3.18 % (2697538)Termination reason: Instruction limit % 17.78/3.18 % (2697538)Termination phase: Saturation % 17.78/3.18 % (2697538)Time elapsed: 0.362 s % 17.78/3.18 % (2697538)Peak memory usage: 137 MB % 17.78/3.18 % (2697538)Instructions burned: 483 (million) % 17.78/3.18 % (2697556)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=444403155:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi) % 17.78/3.18 % (2697561)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1367013582:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi) % 17.78/3.18 % (2697562)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3768114865:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 17.78/3.18 % (2697553)Instruction limit reached! % 17.78/3.18 % (2697553)------------------------------ % 17.78/3.18 % (2697553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.78/3.18 % (2697553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.78/3.18 % (2697553)CaDiCaL version: 2.1.3 % 17.78/3.18 % (2697553)Termination reason: Instruction limit % 18.46/3.48 % (2697553)Termination phase: Saturation % 18.46/3.48 % (2697553)Time elapsed: 0.163 s % 18.46/3.48 % (2697553)Peak memory usage: 114 MB % 18.46/3.48 % (2697553)Instructions burned: 321 (million) % 18.46/3.48 % (2697555)Instruction limit reached! % 18.46/3.48 % (2697555)------------------------------ % 18.46/3.48 % (2697555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.46/3.48 % (2697555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.46/3.48 % (2697555)CaDiCaL version: 2.1.3 % 18.46/3.48 % (2697555)Termination reason: Instruction limit % 18.46/3.48 % (2697555)Termination phase: Saturation % 18.46/3.48 % (2697555)Time elapsed: 0.162 s % 18.46/3.48 % (2697555)Peak memory usage: 121 MB % 18.46/3.48 % (2697555)Instructions burned: 471 (million) % 18.46/3.48 % (2697552)Instruction limit reached! % 18.46/3.48 % (2697552)------------------------------ % 18.46/3.48 % (2697552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.46/3.48 % (2697552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.46/3.48 % (2697552)CaDiCaL version: 2.1.3 % 18.46/3.48 % (2697552)Termination reason: Instruction limit % 18.46/3.48 % (2697552)Termination phase: Saturation % 18.46/3.48 % (2697552)Time elapsed: 0.263 s % 18.46/3.48 % (2697552)Peak memory usage: 93 MB % 18.46/3.48 % (2697552)Instructions burned: 484 (million) % 18.46/3.48 % (2697554)Instruction limit reached! % 18.46/3.48 % (2697554)------------------------------ % 18.46/3.48 % (2697554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.46/3.48 % (2697554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.46/3.48 % (2697554)CaDiCaL version: 2.1.3 % 18.46/3.48 % (2697554)Termination reason: Instruction limit % 18.46/3.48 % (2697554)Termination phase: Saturation % 18.46/3.48 % (2697554)Time elapsed: 0.240 s % 18.46/3.48 % (2697554)Peak memory usage: 120 MB % 18.46/3.48 % (2697554)Instructions burned: 416 (million) % 18.46/3.48 % (2697567)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1736477067:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 18.46/3.48 % (2697566)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=890251841:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 18.46/3.48 % (2697556)Instruction limit reached! % 18.46/3.48 % (2697556)------------------------------ % 18.46/3.48 % (2697556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.46/3.48 % (2697556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.46/3.48 % (2697556)CaDiCaL version: 2.1.3 % 18.46/3.48 % (2697556)Termination reason: Instruction limit % 18.46/3.48 % (2697556)Termination phase: Saturation % 18.46/3.48 % (2697556)Time elapsed: 0.226 s % 18.46/3.48 % (2697556)Peak memory usage: 137 MB % 18.46/3.48 % (2697556)Instructions burned: 276 (million) % 18.46/3.48 % (2697568)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2578784359:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 18.46/3.48 % (2697569)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2210605407:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 18.46/3.48 % (2697561)Instruction limit reached! % 18.46/3.48 % (2697561)------------------------------ % 18.46/3.48 % (2697561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.46/3.48 % (2697561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.46/3.48 % (2697561)CaDiCaL version: 2.1.3 % 18.46/3.48 % (2697561)Termination reason: Instruction limit % 18.46/3.48 % (2697561)Termination phase: Saturation % 18.46/3.48 % (2697561)Time elapsed: 0.231 s % 18.46/3.48 % (2697561)Peak memory usage: 119 MB % 18.46/3.48 % (2697561)Instructions burned: 375 (million) % 18.46/3.48 % (2697567)Instruction limit reached! % 18.46/3.48 % (2697567)------------------------------ % 18.46/3.48 % (2697567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.46/3.48 % (2697567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.46/3.48 % (2697567)CaDiCaL version: 2.1.3 % 18.46/3.48 % (2697567)Termination reason: Instruction limit % 18.46/3.48 % (2697567)Termination phase: Saturation % 18.46/3.48 % (2697567)Time elapsed: 0.145 s % 18.46/3.48 % (2697567)Peak memory usage: 137 MB % 18.46/3.48 % (2697567)Instructions burned: 336 (million) % 18.46/3.48 % (2697562)Instruction limit reached! % 21.87/3.99 % (2697562)------------------------------ % 21.87/3.99 % (2697562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.99 % (2697562)CaDiCaL version: 2.1.3 % 21.87/3.99 % (2697562)Termination reason: Instruction limit % 21.87/3.99 % (2697562)Termination phase: Saturation % 21.87/3.99 % (2697562)Time elapsed: 0.265 s % 21.87/3.99 % (2697562)Peak memory usage: 120 MB % 21.87/3.99 % (2697562)Instructions burned: 387 (million) % 21.87/3.99 % (2697572)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1882401436:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi) % 21.87/3.99 % (2697576)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=379377761:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2977 on theBenchmark for (2977ds/273Mi) % 21.87/3.99 % (2697575)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=1911518612:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi) % 21.87/3.99 % (2697578)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2320589313:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 21.87/3.99 % (2697568)Instruction limit reached! % 21.87/3.99 % (2697568)------------------------------ % 21.87/3.99 % (2697568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.99 % (2697568)CaDiCaL version: 2.1.3 % 21.87/3.99 % (2697568)Termination reason: Instruction limit % 21.87/3.99 % (2697568)Termination phase: Saturation % 21.87/3.99 % (2697568)Time elapsed: 0.197 s % 21.87/3.99 % (2697568)Peak memory usage: 92 MB % 21.87/3.99 % (2697568)Instructions burned: 360 (million) % 21.87/3.99 % (2697569)Instruction limit reached! % 21.87/3.99 % (2697569)------------------------------ % 21.87/3.99 % (2697569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.99 % (2697569)CaDiCaL version: 2.1.3 % 21.87/3.99 % (2697569)Termination reason: Instruction limit % 21.87/3.99 % (2697569)Termination phase: Saturation % 21.87/3.99 % (2697569)Time elapsed: 0.191 s % 21.87/3.99 % (2697569)Peak memory usage: 118 MB % 21.87/3.99 % (2697569)Instructions burned: 342 (million) % 21.87/3.99 % (2697566)Instruction limit reached! % 21.87/3.99 % (2697566)------------------------------ % 21.87/3.99 % (2697566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.99 % (2697566)CaDiCaL version: 2.1.3 % 21.87/3.99 % (2697566)Termination reason: Instruction limit % 21.87/3.99 % (2697566)Termination phase: Saturation % 21.87/3.99 % (2697566)Time elapsed: 0.282 s % 21.87/3.99 % (2697566)Peak memory usage: 92 MB % 21.87/3.99 % (2697566)Instructions burned: 514 (million) % 21.87/3.99 % (2697576)Instruction limit reached! % 21.87/3.99 % (2697576)------------------------------ % 21.87/3.99 % (2697576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.99 % (2697576)CaDiCaL version: 2.1.3 % 21.87/3.99 % (2697576)Termination reason: Instruction limit % 21.87/3.99 % (2697576)Termination phase: Saturation % 21.87/3.99 % (2697576)Time elapsed: 0.097 s % 21.87/3.99 % (2697576)Peak memory usage: 93 MB % 21.87/3.99 % (2697576)Instructions burned: 273 (million) % 21.87/3.99 % (2697572)Instruction limit reached! % 21.87/3.99 % (2697572)------------------------------ % 21.87/3.99 % (2697572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.99 % (2697572)CaDiCaL version: 2.1.3 % 21.87/3.99 % (2697572)Termination reason: Instruction limit % 21.87/3.99 % (2697572)Termination phase: Saturation % 21.87/3.99 % (2697572)Time elapsed: 0.188 s % 21.87/3.99 % (2697572)Peak memory usage: 119 MB % 21.87/3.99 % (2697572)Instructions burned: 262 (million) % 21.87/3.99 % (2697578)Instruction limit reached! % 21.87/3.99 % (2697578)------------------------------ % 21.87/3.99 % (2697578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.87/3.99 % (2697578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.75/4.39 % (2697578)CaDiCaL version: 2.1.3 % 25.75/4.39 % (2697578)Termination reason: Instruction limit % 25.75/4.39 % (2697578)Termination phase: Saturation % 25.75/4.39 % (2697578)Time elapsed: 0.085 s % 25.75/4.39 % (2697578)Peak memory usage: 90 MB % 25.75/4.39 % (2697578)Instructions burned: 147 (million) % 25.75/4.39 % (2697585)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1561746365:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2975 on theBenchmark for (2975ds/655Mi) % 25.75/4.39 % (2697583)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=3279209780:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 25.75/4.39 % (2697582)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1388435478:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 25.75/4.39 % (2697584)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=561730988:i=1052:rtra=on_2975 on theBenchmark for (2975ds/1052Mi) % 25.75/4.39 % (2697575)Instruction limit reached! % 25.75/4.39 % (2697575)------------------------------ % 25.75/4.39 % (2697575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.75/4.39 % (2697575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.75/4.39 % (2697575)CaDiCaL version: 2.1.3 % 25.75/4.39 % (2697575)Termination reason: Instruction limit % 25.75/4.39 % (2697575)Termination phase: Saturation % 25.75/4.39 % (2697575)Time elapsed: 0.186 s % 25.75/4.39 % (2697575)Peak memory usage: 119 MB % 25.75/4.39 % (2697575)Instructions burned: 236 (million) % 25.75/4.39 % (2697586)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2442386330:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 25.75/4.39 % (2697587)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3263255462:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 25.75/4.39 % (2697587)Refutation not found, incomplete strategy % 25.75/4.39 % (2697587)------------------------------ % 25.75/4.39 % (2697587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.75/4.39 % (2697587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.75/4.39 % (2697587)CaDiCaL version: 2.1.3 % 25.75/4.39 % (2697587)Termination reason: Refutation not found, incomplete strategy % 25.75/4.39 % (2697587)Time elapsed: 0.036 s % 25.75/4.39 % (2697587)Peak memory usage: 116 MB % 25.75/4.39 % (2697587)Instructions burned: 20 (million) % 25.75/4.39 % (2697585)Instruction limit reached! % 25.75/4.39 % (2697585)------------------------------ % 25.75/4.39 % (2697585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.75/4.39 % (2697585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.75/4.39 % (2697585)CaDiCaL version: 2.1.3 % 25.75/4.39 % (2697585)Termination reason: Instruction limit % 25.75/4.39 % (2697585)Termination phase: Saturation % 25.75/4.39 % (2697585)Time elapsed: 0.139 s % 25.75/4.39 % (2697585)Peak memory usage: 90 MB % 25.75/4.39 % (2697585)Instructions burned: 661 (million) % 25.75/4.39 % (2697592)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3557064565:s2a=on:i=450:doe=on:nm=32:rtra=on_2973 on theBenchmark for (2973ds/450Mi) % 25.75/4.39 % (2697583)Instruction limit reached! % 25.75/4.39 % (2697583)------------------------------ % 25.75/4.39 % (2697583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.75/4.39 % (2697583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.75/4.39 % (2697583)CaDiCaL version: 2.1.3 % 25.75/4.39 % (2697583)Termination reason: Instruction limit % 25.75/4.39 % (2697583)Termination phase: Saturation % 25.75/4.39 % (2697583)Time elapsed: 0.215 s % 25.75/4.39 % (2697583)Peak memory usage: 135 MB % 25.75/4.39 % (2697583)Instructions burned: 277 (million) % 25.75/4.39 % (2697595)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 25.75/4.39 % (2697595)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3344523438:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi) % 27.92/4.80 % (2697597)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=900084704:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2971 on theBenchmark for (2971ds/130Mi) % 27.92/4.80 % (2697587)------------------------------ % 27.92/4.80 % (2697587)------------------------------ % 27.92/4.80 % (2697597)Instruction limit reached! % 27.92/4.80 % (2697597)------------------------------ % 27.92/4.80 % (2697597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.92/4.80 % (2697597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.92/4.80 % (2697597)CaDiCaL version: 2.1.3 % 27.92/4.80 % (2697597)Termination reason: Instruction limit % 27.92/4.80 % (2697597)Termination phase: Saturation % 27.92/4.80 % (2697597)Time elapsed: 0.107 s % 27.92/4.80 % (2697597)Peak memory usage: 117 MB % 27.92/4.80 % (2697597)Instructions burned: 131 (million) % 27.92/4.80 % (2697600)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3605839251:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi) % 27.92/4.80 % (2697592)Instruction limit reached! % 27.92/4.80 % (2697592)------------------------------ % 27.92/4.80 % (2697592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.92/4.80 % (2697592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.92/4.80 % (2697592)CaDiCaL version: 2.1.3 % 27.92/4.80 % (2697592)Termination reason: Instruction limit % 27.92/4.80 % (2697592)Termination phase: Saturation % 27.92/4.80 % (2697592)Time elapsed: 0.337 s % 27.92/4.80 % (2697592)Peak memory usage: 137 MB % 27.92/4.80 % (2697592)Instructions burned: 451 (million) % 27.92/4.80 % (2697601)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3806551197:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 27.92/4.80 % (2697595)Instruction limit reached! % 27.92/4.80 % (2697595)------------------------------ % 27.92/4.80 % (2697595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.92/4.80 % (2697595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.92/4.80 % (2697595)CaDiCaL version: 2.1.3 % 27.92/4.80 % (2697595)Termination reason: Instruction limit % 27.92/4.80 % (2697595)Termination phase: Saturation % 27.92/4.80 % (2697595)Time elapsed: 0.339 s % 27.92/4.80 % (2697595)Peak memory usage: 126 MB % 27.92/4.80 % (2697595)Instructions burned: 1093 (million) % 27.92/4.80 % (2697603)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=574472252:s2a=on:i=835:s2at=2:rtra=on_2969 on theBenchmark for (2969ds/835Mi) % 27.92/4.80 % (2697584)Instruction limit reached! % 27.92/4.80 % (2697584)------------------------------ % 27.92/4.80 % (2697584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.92/4.80 % (2697584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.92/4.80 % (2697584)CaDiCaL version: 2.1.3 % 27.92/4.80 % (2697584)Termination reason: Instruction limit % 27.92/4.80 % (2697584)Termination phase: Saturation % 27.92/4.80 % (2697584)Time elapsed: 0.613 s % 27.92/4.80 % (2697584)Peak memory usage: 94 MB % 27.92/4.80 % (2697584)Instructions burned: 1052 (million) % 27.92/4.80 % (2697586)Instruction limit reached! % 27.92/4.80 % (2697586)------------------------------ % 27.92/4.80 % (2697586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.92/4.80 % (2697586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.92/4.80 % (2697586)CaDiCaL version: 2.1.3 % 27.92/4.80 % (2697586)Termination reason: Instruction limit % 27.92/4.80 % (2697586)Termination phase: Saturation % 27.92/4.80 % (2697586)Time elapsed: 0.582 s % 27.92/4.80 % (2697586)Peak memory usage: 93 MB % 27.92/4.80 % (2697586)Instructions burned: 1054 (million) % 27.92/4.80 % (2697600)Instruction limit reached! % 27.92/4.80 % (2697600)------------------------------ % 27.92/4.80 % (2697600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.92/4.80 % (2697600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.92/4.80 % (2697600)CaDiCaL version: 2.1.3 % 27.92/4.80 % (2697600)Termination reason: Instruction limit % 27.92/4.80 % (2697600)Termination phase: Saturation % 27.92/4.80 % (2697600)Time elapsed: 0.185 s % 27.92/4.80 % (2697600)Peak memory usage: 118 MB % 27.92/4.80 % (2697600)Instructions burned: 314 (million) % 27.92/4.80 % (2697605)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=4108812416:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 27.92/4.80 % (2697607)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=520629401:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 34.23/5.74 % (2697605)Instruction limit reached! % 34.23/5.74 % (2697605)------------------------------ % 34.23/5.74 % (2697605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.74 % (2697605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.74 % (2697605)CaDiCaL version: 2.1.3 % 34.23/5.74 % (2697605)Termination reason: Instruction limit % 34.23/5.74 % (2697605)Termination phase: Saturation % 34.23/5.74 % (2697605)Time elapsed: 0.097 s % 34.23/5.74 % (2697605)Peak memory usage: 91 MB % 34.23/5.74 % (2697605)Instructions burned: 309 (million) % 34.23/5.74 % (2697608)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1491614010:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2967 on theBenchmark for (2967ds/646Mi) % 34.23/5.74 % (2697609)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=916744057:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2967 on theBenchmark for (2967ds/784Mi) % 34.23/5.74 % (2697601)Instruction limit reached! % 34.23/5.74 % (2697601)------------------------------ % 34.23/5.74 % (2697601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.74 % (2697601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.74 % (2697601)CaDiCaL version: 2.1.3 % 34.23/5.74 % (2697601)Termination reason: Instruction limit % 34.23/5.74 % (2697601)Termination phase: Saturation % 34.23/5.74 % (2697601)Time elapsed: 0.260 s % 34.23/5.74 % (2697601)Peak memory usage: 93 MB % 34.23/5.74 % (2697601)Instructions burned: 492 (million) % 34.23/5.74 % (2697613)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=2754674214:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2966 on theBenchmark for (2966ds/1131Mi) % 34.23/5.74 % (2697615)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=22347917:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2965 on theBenchmark for (2965ds/246Mi) % 34.23/5.74 % (2697603)Instruction limit reached! % 34.23/5.74 % (2697603)------------------------------ % 34.23/5.74 % (2697603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.74 % (2697603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.74 % (2697603)CaDiCaL version: 2.1.3 % 34.23/5.74 % (2697603)Termination reason: Instruction limit % 34.23/5.74 % (2697603)Termination phase: Saturation % 34.23/5.74 % (2697603)Time elapsed: 0.476 s % 34.23/5.74 % (2697603)Peak memory usage: 94 MB % 34.23/5.74 % (2697603)Instructions burned: 835 (million) % 34.23/5.74 % (2697615)Instruction limit reached! % 34.23/5.74 % (2697615)------------------------------ % 34.23/5.74 % (2697615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.74 % (2697615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.74 % (2697615)CaDiCaL version: 2.1.3 % 34.23/5.74 % (2697615)Termination reason: Instruction limit % 34.23/5.74 % (2697615)Termination phase: Saturation % 34.23/5.74 % (2697615)Time elapsed: 0.180 s % 34.23/5.74 % (2697615)Peak memory usage: 119 MB % 34.23/5.74 % (2697615)Instructions burned: 246 (million) % 34.23/5.74 % (2697613)Instruction limit reached! % 34.23/5.74 % (2697613)------------------------------ % 34.23/5.74 % (2697613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.74 % (2697613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.74 % (2697613)CaDiCaL version: 2.1.3 % 34.23/5.74 % (2697613)Termination reason: Instruction limit % 34.23/5.74 % (2697613)Termination phase: Saturation % 34.23/5.74 % (2697613)Time elapsed: 0.284 s % 34.23/5.74 % (2697613)Peak memory usage: 120 MB % 34.23/5.74 % (2697613)Instructions burned: 1132 (million) % 34.23/5.74 % (2697608)Instruction limit reached! % 34.23/5.74 % (2697608)------------------------------ % 34.23/5.74 % (2697608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.74 % (2697608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.74 % (2697608)CaDiCaL version: 2.1.3 % 34.23/5.74 % (2697608)Termination reason: Instruction limit % 34.23/5.74 % (2697608)Termination phase: Saturation % 34.23/5.74 % (2697608)Time elapsed: 0.379 s % 34.23/5.74 % (2697608)Peak memory usage: 137 MB % 45.65/7.07 % (2697608)Instructions burned: 648 (million) % 45.65/7.07 % (2697607)Instruction limit reached! % 45.65/7.07 % (2697607)------------------------------ % 45.65/7.07 % (2697607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.65/7.07 % (2697607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.65/7.07 % (2697607)CaDiCaL version: 2.1.3 % 45.65/7.07 % (2697607)Termination reason: Instruction limit % 45.65/7.07 % (2697607)Termination phase: Saturation % 45.65/7.07 % (2697607)Time elapsed: 0.403 s % 45.65/7.07 % (2697607)Peak memory usage: 119 MB % 45.65/7.07 % (2697607)Instructions burned: 777 (million) % 45.65/7.07 % (2697618)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1356662616:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/775Mi) % 45.65/7.07 % (2697620)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1211915867:i=102:nm=16:rtra=on_2962 on theBenchmark for (2962ds/102Mi) % 45.65/7.07 % (2697619)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3029716081:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 45.65/7.07 % (2697620)Instruction limit reached! % 45.65/7.07 % (2697620)------------------------------ % 45.65/7.07 % (2697620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.65/7.07 % (2697620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.65/7.07 % (2697620)CaDiCaL version: 2.1.3 % 45.65/7.07 % (2697620)Termination reason: Instruction limit % 45.65/7.07 % (2697620)Termination phase: Saturation % 45.65/7.07 % (2697620)Time elapsed: 0.033 s % 45.65/7.07 % (2697620)Peak memory usage: 89 MB % 45.65/7.07 % (2697620)Instructions burned: 105 (million) % 45.65/7.07 % (2697621)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3662591466:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2962 on theBenchmark for (2962ds/1094Mi) % 45.65/7.07 % (2697622)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1119521580:i=6400:doe=on:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/6400Mi) % 45.65/7.07 % (2697609)Instruction limit reached! % 45.65/7.07 % (2697609)------------------------------ % 45.65/7.07 % (2697609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.65/7.07 % (2697609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.65/7.07 % (2697609)CaDiCaL version: 2.1.3 % 45.65/7.07 % (2697609)Termination reason: Instruction limit % 45.65/7.07 % (2697609)Termination phase: Saturation % 45.65/7.07 % (2697609)Time elapsed: 0.508 s % 45.65/7.07 % (2697609)Peak memory usage: 121 MB % 45.65/7.07 % (2697609)Instructions burned: 784 (million) % 45.65/7.07 % (2697626)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=2253312598:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2961 on theBenchmark for (2961ds/868Mi) % 45.65/7.07 % (2697629)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=59343377:i=1846:canc=cautious:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/1846Mi) % 45.65/7.07 % (2697619)Instruction limit reached! % 45.65/7.07 % (2697619)------------------------------ % 45.65/7.07 % (2697619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.65/7.07 % (2697619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.65/7.07 % (2697619)CaDiCaL version: 2.1.3 % 45.65/7.07 % (2697619)Termination reason: Instruction limit % 45.65/7.07 % (2697619)Termination phase: Saturation % 45.65/7.07 % (2697619)Time elapsed: 0.180 s % 45.65/7.07 % (2697619)Peak memory usage: 92 MB % 45.65/7.07 % (2697619)Instructions burned: 273 (million) % 45.65/7.07 % (2697632)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2128073419:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2959 on theBenchmark for (2959ds/36816Mi) % 45.65/7.07 % (2697618)Instruction limit reached! % 45.65/7.07 % (2697618)------------------------------ % 45.65/7.07 % (2697618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.65/7.07 % (2697618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.65/7.07 % (2697618)CaDiCaL version: 2.1.3 % 45.65/7.07 % (2697618)Termination reason: Instruction limit % 45.65/7.07 % (2697618)Termination phase: Saturation % 55.25/8.60 % (2697618)Time elapsed: 0.357 s % 55.25/8.60 % (2697618)Peak memory usage: 94 MB % 55.25/8.60 % (2697618)Instructions burned: 776 (million) % 55.25/8.60 % (2697634)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1914217091:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 55.25/8.60 % (2697629)Instruction limit reached! % 55.25/8.60 % (2697629)------------------------------ % 55.25/8.60 % (2697629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2697629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2697629)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2697629)Termination reason: Instruction limit % 55.25/8.60 % (2697629)Termination phase: Saturation % 55.25/8.60 % (2697629)Time elapsed: 0.464 s % 55.25/8.60 % (2697629)Peak memory usage: 97 MB % 55.25/8.60 % (2697629)Instructions burned: 1848 (million) % 55.25/8.60 % (2697626)Instruction limit reached! % 55.25/8.60 % (2697626)------------------------------ % 55.25/8.60 % (2697626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2697626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2697626)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2697626)Termination reason: Instruction limit % 55.25/8.60 % (2697626)Termination phase: Saturation % 55.25/8.60 % (2697626)Time elapsed: 0.495 s % 55.25/8.60 % (2697626)Peak memory usage: 121 MB % 55.25/8.60 % (2697626)Instructions burned: 870 (million) % 55.25/8.60 % (2697634)Instruction limit reached! % 55.25/8.60 % (2697634)------------------------------ % 55.25/8.60 % (2697634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2697634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2697634)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2697634)Termination reason: Instruction limit % 55.25/8.60 % (2697634)Termination phase: Saturation % 55.25/8.60 % (2697634)Time elapsed: 0.175 s % 55.25/8.60 % (2697634)Peak memory usage: 93 MB % 55.25/8.60 % (2697634)Instructions burned: 273 (million) % 55.25/8.60 % (2697621)Instruction limit reached! % 55.25/8.60 % (2697621)------------------------------ % 55.25/8.60 % (2697621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2697621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2697621)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2697621)Termination reason: Instruction limit % 55.25/8.60 % (2697621)Termination phase: Saturation % 55.25/8.60 % (2697621)Time elapsed: 0.604 s % 55.25/8.60 % (2697621)Peak memory usage: 95 MB % 55.25/8.60 % (2697621)Instructions burned: 1094 (million) % 55.25/8.60 % (2697636)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=4074118804:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 55.25/8.60 % (2697638)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=3660942637:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2955 on theBenchmark for (2955ds/2216Mi) % 55.25/8.60 % (2697637)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1958900533:i=5811:kws=precedence:nm=0:rtra=on_2955 on theBenchmark for (2955ds/5811Mi) % 55.25/8.60 % (2697639)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=285616157:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/801Mi) % 55.25/8.60 % (2697636)Instruction limit reached! % 55.25/8.60 % (2697636)------------------------------ % 55.25/8.60 % (2697636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2697636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2697636)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2697636)Termination reason: Instruction limit % 55.25/8.60 % (2697636)Termination phase: Saturation % 55.25/8.60 % (2697636)Time elapsed: 0.280 s % 55.25/8.60 % (2697636)Peak memory usage: 122 MB % 55.25/8.60 % (2697636)Instructions burned: 865 (million) % 55.25/8.60 % (2697644)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2394527730:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2951 on theBenchmark for (2951ds/1026Mi) % 55.25/8.60 % (2697639)Instruction limit reached! % 55.25/8.60 % (2697639)------------------------------ % 55.25/8.60 % (2697639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/12.30 % (2697639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/12.30 % (2697639)CaDiCaL version: 2.1.3 % 83.04/12.30 % (2697639)Termination reason: Instruction limit % 83.04/12.30 % (2697639)Termination phase: Saturation % 83.04/12.30 % (2697639)Time elapsed: 0.500 s % 83.04/12.30 % (2697639)Peak memory usage: 96 MB % 83.04/12.30 % (2697639)Instructions burned: 801 (million) % 83.04/12.30 % (2697582)Instruction limit reached! % 83.04/12.30 % (2697582)------------------------------ % 83.04/12.30 % (2697582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/12.30 % (2697582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/12.30 % (2697582)CaDiCaL version: 2.1.3 % 83.04/12.30 % (2697582)Termination reason: Instruction limit % 83.04/12.30 % (2697582)Termination phase: Saturation % 83.04/12.30 % (2697582)Time elapsed: 2.578 s % 83.04/12.30 % (2697582)Peak memory usage: 120 MB % 83.04/12.30 % (2697582)Instructions burned: 4431 (million) % 83.04/12.30 % (2697644)Instruction limit reached! % 83.04/12.30 % (2697644)------------------------------ % 83.04/12.30 % (2697644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/12.30 % (2697644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/12.30 % (2697644)CaDiCaL version: 2.1.3 % 83.04/12.30 % (2697644)Termination reason: Instruction limit % 83.04/12.30 % (2697644)Termination phase: Saturation % 83.04/12.30 % (2697644)Time elapsed: 0.308 s % 83.04/12.30 % (2697644)Peak memory usage: 94 MB % 83.04/12.30 % (2697644)Instructions burned: 1026 (million) % 83.04/12.30 % (2697646)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2614922297:i=3509:rtra=on_2948 on theBenchmark for (2948ds/3509Mi) % 83.04/12.30 % (2697647)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=49303498:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2948 on theBenchmark for (2948ds/2127Mi) % 83.04/12.30 % (2697648)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3808023865:i=1959:rtra=on:fsd=on:proc=on_2947 on theBenchmark for (2947ds/1959Mi) % 83.04/12.30 % (2697638)Instruction limit reached! % 83.04/12.30 % (2697638)------------------------------ % 83.04/12.30 % (2697638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/12.30 % (2697638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/12.30 % (2697638)CaDiCaL version: 2.1.3 % 83.04/12.30 % (2697638)Termination reason: Instruction limit % 83.04/12.30 % (2697638)Termination phase: Saturation % 83.04/12.30 % (2697638)Time elapsed: 1.114 s % 83.04/12.30 % (2697638)Peak memory usage: 127 MB % 83.04/12.30 % (2697638)Instructions burned: 2218 (million) % 83.04/12.30 % (2697652)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3629803495:s2a=on:i=3553:nm=0:rtra=on_2942 on theBenchmark for (2942ds/3553Mi) % 83.04/12.30 % (2697648)Instruction limit reached! % 83.04/12.30 % (2697648)------------------------------ % 83.04/12.30 % (2697648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/12.30 % (2697648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/12.30 % (2697648)CaDiCaL version: 2.1.3 % 83.04/12.30 % (2697648)Termination reason: Instruction limit % 83.04/12.30 % (2697648)Termination phase: Saturation % 83.04/12.30 % (2697648)Time elapsed: 0.539 s % 83.04/12.30 % (2697648)Peak memory usage: 123 MB % 83.04/12.30 % (2697648)Instructions burned: 1959 (million) % 83.04/12.30 % (2697654)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2459403098:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2941 on theBenchmark for (2941ds/3201Mi) % 83.04/12.30 % (2697647)Instruction limit reached! % 83.04/12.30 % (2697647)------------------------------ % 83.04/12.30 % (2697647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/12.30 % (2697647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/12.30 % (2697647)CaDiCaL version: 2.1.3 % 83.04/12.30 % (2697647)Termination reason: Instruction limit % 83.04/12.30 % (2697647)Termination phase: Saturation % 83.04/12.30 % (2697647)Time elapsed: 1.004 s % 83.04/12.30 % (2697647)Peak memory usage: 95 MB % 83.04/12.30 % (2697647)Instructions burned: 2129 (million) % 83.04/12.30 % (2697656)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=4184956777:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2936 on theBenchmark for (2936ds/4093Mi) % 100.05/14.85 % (2697646)Instruction limit reached! % 100.05/14.85 % (2697646)------------------------------ % 100.05/14.85 % (2697646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.05/14.85 % (2697646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.85 % (2697646)CaDiCaL version: 2.1.3 % 100.05/14.85 % (2697646)Termination reason: Instruction limit % 100.05/14.85 % (2697646)Termination phase: Saturation % 100.05/14.85 % (2697646)Time elapsed: 1.320 s % 100.05/14.85 % (2697646)Peak memory usage: 91 MB % 100.05/14.85 % (2697646)Instructions burned: 3509 (million) % 100.05/14.85 % (2697658)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=371394876:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2934 on theBenchmark for (2934ds/21173Mi) % 100.05/14.85 % (2697654)Instruction limit reached! % 100.05/14.85 % (2697654)------------------------------ % 100.05/14.85 % (2697654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.05/14.85 % (2697654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.85 % (2697654)CaDiCaL version: 2.1.3 % 100.05/14.85 % (2697654)Termination reason: Instruction limit % 100.05/14.85 % (2697654)Termination phase: Saturation % 100.05/14.85 % (2697654)Time elapsed: 0.813 s % 100.05/14.85 % (2697654)Peak memory usage: 94 MB % 100.05/14.85 % (2697654)Instructions burned: 3206 (million) % 100.05/14.85 % (2697660)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=470102399:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2932 on theBenchmark for (2932ds/10544Mi) % 100.05/14.85 % (2697622)Instruction limit reached! % 100.05/14.85 % (2697622)------------------------------ % 100.05/14.85 % (2697622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.05/14.85 % (2697622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.85 % (2697622)CaDiCaL version: 2.1.3 % 100.05/14.85 % (2697622)Termination reason: Instruction limit % 100.05/14.85 % (2697622)Termination phase: Saturation % 100.05/14.85 % (2697622)Time elapsed: 3.614 s % 100.05/14.85 % (2697622)Peak memory usage: 125 MB % 100.05/14.85 % (2697622)Instructions burned: 6402 (million) % 100.05/14.85 % (2697652)Instruction limit reached! % 100.05/14.85 % (2697652)------------------------------ % 100.05/14.85 % (2697652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.05/14.85 % (2697652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.85 % (2697652)CaDiCaL version: 2.1.3 % 100.05/14.85 % (2697652)Termination reason: Instruction limit % 100.05/14.85 % (2697652)Termination phase: Saturation % 100.05/14.85 % (2697652)Time elapsed: 1.707 s % 100.05/14.85 % (2697652)Peak memory usage: 109 MB % 100.05/14.85 % (2697652)Instructions burned: 3554 (million) % 100.05/14.85 % (2697662)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3774238071:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2924 on theBenchmark for (2924ds/1262Mi) % 100.05/14.85 % (2697637)Instruction limit reached! % 100.05/14.85 % (2697637)------------------------------ % 100.05/14.85 % (2697637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.05/14.85 % (2697637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.85 % (2697637)CaDiCaL version: 2.1.3 % 100.05/14.85 % (2697637)Termination reason: Instruction limit % 100.05/14.85 % (2697637)Termination phase: Saturation % 100.05/14.85 % (2697637)Time elapsed: 3.033 s % 100.05/14.85 % (2697637)Peak memory usage: 130 MB % 100.05/14.85 % (2697637)Instructions burned: 5812 (million) % 100.05/14.85 % (2697663)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=683613384:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2924 on theBenchmark for (2924ds/775Mi) % 100.05/14.85 % (2697665)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2259422242:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/270Mi) % 100.05/14.85 % (2697665)Instruction limit reached! % 100.05/14.85 % (2697665)------------------------------ % 100.05/14.85 % (2697665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.05/14.85 % (2697665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.85 % (2697665)CaDiCaL version: 2.1.3 % 100.05/14.85 % (2697665)Termination reason: Instruction limit % 100.05/14.85 % (2697665)Termination phase: Saturation % 123.86/18.06 % (2697665)Time elapsed: 0.178 s % 123.86/18.06 % (2697665)Peak memory usage: 93 MB % 123.86/18.06 % (2697665)Instructions burned: 271 (million) % 123.86/18.06 % (2697663)Instruction limit reached! % 123.86/18.06 % (2697663)------------------------------ % 123.86/18.06 % (2697663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.86/18.06 % (2697663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.86/18.06 % (2697663)CaDiCaL version: 2.1.3 % 123.86/18.06 % (2697663)Termination reason: Instruction limit % 123.86/18.06 % (2697663)Termination phase: Saturation % 123.86/18.06 % (2697663)Time elapsed: 0.382 s % 123.86/18.06 % (2697663)Peak memory usage: 95 MB % 123.86/18.06 % (2697663)Instructions burned: 775 (million) % 123.86/18.06 % (2697668)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1230790817:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2920 on theBenchmark for (2920ds/17165Mi) % 123.86/18.06 % (2697669)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=990663607:s2a=on:i=13094:s2at=-1:rtra=on_2919 on theBenchmark for (2919ds/13094Mi) % 123.86/18.06 % (2697662)Instruction limit reached! % 123.86/18.06 % (2697662)------------------------------ % 123.86/18.06 % (2697662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.86/18.06 % (2697662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.86/18.06 % (2697662)CaDiCaL version: 2.1.3 % 123.86/18.06 % (2697662)Termination reason: Instruction limit % 123.86/18.06 % (2697662)Termination phase: Saturation % 123.86/18.06 % (2697662)Time elapsed: 0.652 s % 123.86/18.06 % (2697662)Peak memory usage: 121 MB % 123.86/18.06 % (2697662)Instructions burned: 1263 (million) % 123.86/18.06 % (2697672)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2868528972:st=2:i=12633:rtra=on:ss=axioms_2917 on theBenchmark for (2917ds/12633Mi) % 123.86/18.06 % (2697656)Instruction limit reached! % 123.86/18.06 % (2697656)------------------------------ % 123.86/18.06 % (2697656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.86/18.06 % (2697656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.86/18.06 % (2697656)CaDiCaL version: 2.1.3 % 123.86/18.06 % (2697656)Termination reason: Instruction limit % 123.86/18.06 % (2697656)Termination phase: Saturation % 123.86/18.06 % (2697656)Time elapsed: 2.080 s % 123.86/18.06 % (2697656)Peak memory usage: 141 MB % 123.86/18.06 % (2697656)Instructions burned: 4094 (million) % 123.86/18.06 % (2697674)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2087199421:i=1783:rtra=on:gtg=position_2914 on theBenchmark for (2914ds/1783Mi) % 123.86/18.06 % (2697674)Instruction limit reached! % 123.86/18.06 % (2697674)------------------------------ % 123.86/18.06 % (2697674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.86/18.06 % (2697674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.86/18.06 % (2697674)CaDiCaL version: 2.1.3 % 123.86/18.06 % (2697674)Termination reason: Instruction limit % 123.86/18.06 % (2697674)Termination phase: Saturation % 123.86/18.06 % (2697674)Time elapsed: 0.927 s % 123.86/18.06 % (2697674)Peak memory usage: 122 MB % 123.86/18.06 % (2697674)Instructions burned: 1784 (million) % 123.86/18.06 % (2697676)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=3475279640:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2904 on theBenchmark for (2904ds/5451Mi) % 123.86/18.06 % (2697660)Instruction limit reached! % 123.86/18.06 % (2697660)------------------------------ % 123.86/18.06 % (2697660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.86/18.06 % (2697660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.86/18.06 % (2697660)CaDiCaL version: 2.1.3 % 123.86/18.06 % (2697660)Termination reason: Instruction limit % 123.86/18.06 % (2697660)Termination phase: Saturation % 123.86/18.06 % (2697660)Time elapsed: 3.511 s % 123.86/18.06 % (2697660)Peak memory usage: 185 MB % 123.86/18.06 % (2697660)Instructions burned: 10545 (million) % 123.86/18.06 % (2697678)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=3884593280:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2896 on theBenchmark for (2896ds/4975Mi) % 123.86/18.06 % (2697678)Instruction limit reached! % 123.86/18.06 % (2697678)------------------------------ % 123.86/18.06 % (2697678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.86/18.06 % (2697678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.93/29.78 % (2697678)CaDiCaL version: 2.1.3 % 206.93/29.78 % (2697678)Termination reason: Instruction limit % 206.93/29.78 % (2697678)Termination phase: Saturation % 206.93/29.78 % (2697678)Time elapsed: 1.209 s % 206.93/29.78 % (2697678)Peak memory usage: 122 MB % 206.93/29.78 % (2697678)Instructions burned: 4984 (million) % 206.93/29.78 % (2697680)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=605995400:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2883 on theBenchmark for (2883ds/2076Mi) % 206.93/29.78 % (2697680)Instruction limit reached! % 206.93/29.78 % (2697680)------------------------------ % 206.93/29.78 % (2697680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.93/29.78 % (2697680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.93/29.78 % (2697680)CaDiCaL version: 2.1.3 % 206.93/29.78 % (2697680)Termination reason: Instruction limit % 206.93/29.78 % (2697680)Termination phase: Saturation % 206.93/29.78 % (2697680)Time elapsed: 0.553 s % 206.93/29.78 % (2697680)Peak memory usage: 124 MB % 206.93/29.78 % (2697680)Instructions burned: 2081 (million) % 206.93/29.78 % (2697682)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2744325818:i=5145:rtra=on_2876 on theBenchmark for (2876ds/5145Mi) % 206.93/29.78 % (2697676)Instruction limit reached! % 206.93/29.78 % (2697676)------------------------------ % 206.93/29.78 % (2697676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.93/29.78 % (2697676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.93/29.78 % (2697676)CaDiCaL version: 2.1.3 % 206.93/29.78 % (2697676)Termination reason: Instruction limit % 206.93/29.78 % (2697676)Termination phase: Saturation % 206.93/29.78 % (2697676)Time elapsed: 2.792 s % 206.93/29.78 % (2697676)Peak memory usage: 123 MB % 206.93/29.78 % (2697676)Instructions burned: 5451 (million) % 206.93/29.78 % (2697684)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3505422791:i=3509:rtra=on_2874 on theBenchmark for (2874ds/3509Mi) % 206.93/29.78 % (2697682)Instruction limit reached! % 206.93/29.78 % (2697682)------------------------------ % 206.93/29.78 % (2697682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.93/29.78 % (2697682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.93/29.78 % (2697682)CaDiCaL version: 2.1.3 % 206.93/29.78 % (2697682)Termination reason: Instruction limit % 206.93/29.78 % (2697682)Termination phase: Saturation % 206.93/29.78 % (2697682)Time elapsed: 1.379 s % 206.93/29.78 % (2697682)Peak memory usage: 105 MB % 206.93/29.78 % (2697682)Instructions burned: 5146 (million) % 206.93/29.78 % (2697672)Instruction limit reached! % 206.93/29.78 % (2697672)------------------------------ % 206.93/29.78 % (2697672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.93/29.78 % (2697672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.93/29.78 % (2697672)CaDiCaL version: 2.1.3 % 206.93/29.78 % (2697672)Termination reason: Instruction limit % 206.93/29.78 % (2697672)Termination phase: Saturation % 206.93/29.78 % (2697672)Time elapsed: 5.401 s % 206.93/29.78 % (2697672)Peak memory usage: 107 MB % 206.93/29.78 % (2697672)Instructions burned: 12634 (million) % 206.93/29.78 % (2697824)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=473255906:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2862 on theBenchmark for (2862ds/13800Mi) % 206.93/29.78 % (2697825)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=621126814:i=1412:rtra=on:fsd=on:proc=on_2861 on theBenchmark for (2861ds/1412Mi) % 206.93/29.78 % (2697684)Instruction limit reached! % 206.93/29.78 % (2697684)------------------------------ % 206.93/29.78 % (2697684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.93/29.78 % (2697684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.93/29.78 % (2697684)CaDiCaL version: 2.1.3 % 206.93/29.78 % (2697684)Termination reason: Instruction limit % 206.93/29.78 % (2697684)Termination phase: Saturation % 206.93/29.78 % (2697684)Time elapsed: 1.459 s % 206.93/29.78 % (2697684)Peak memory usage: 94 MB % 206.93/29.78 % (2697684)Instructions burned: 3510 (million) % 206.93/29.78 % (2697828)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 % 206.93/29.78 % (2697828)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3175836406:i=11747:aac=none:nm=0:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/11747Mi) % 284.01/40.61 % (2697669)Instruction limit reached! % 284.01/40.61 % (2697669)------------------------------ % 284.01/40.61 % (2697669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.01/40.61 % (2697669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.01/40.61 % (2697669)CaDiCaL version: 2.1.3 % 284.01/40.61 % (2697669)Termination reason: Instruction limit % 284.01/40.61 % (2697669)Termination phase: Saturation % 284.01/40.61 % (2697669)Time elapsed: 6.182 s % 284.01/40.61 % (2697669)Peak memory usage: 128 MB % 284.01/40.61 % (2697669)Instructions burned: 13094 (million) % 284.01/40.61 % (2697856)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2713050450:s2a=on:i=3553:nm=0:rtra=on_2856 on theBenchmark for (2856ds/3553Mi) % 284.01/40.61 % (2697825)Instruction limit reached! % 284.01/40.61 % (2697825)------------------------------ % 284.01/40.61 % (2697825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.01/40.61 % (2697825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.01/40.61 % (2697825)CaDiCaL version: 2.1.3 % 284.01/40.61 % (2697825)Termination reason: Instruction limit % 284.01/40.61 % (2697825)Termination phase: Saturation % 284.01/40.61 % (2697825)Time elapsed: 0.716 s % 284.01/40.61 % (2697825)Peak memory usage: 122 MB % 284.01/40.61 % (2697825)Instructions burned: 1413 (million) % 284.01/40.61 % (2697919)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3744527881:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2853 on theBenchmark for (2853ds/3201Mi) % 284.01/40.61 % (2697658)Instruction limit reached! % 284.01/40.61 % (2697658)------------------------------ % 284.01/40.61 % (2697658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.01/40.61 % (2697658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.01/40.61 % (2697658)CaDiCaL version: 2.1.3 % 284.01/40.61 % (2697658)Termination reason: Instruction limit % 284.01/40.61 % (2697658)Termination phase: Saturation % 284.01/40.61 % (2697658)Time elapsed: 9.731 s % 284.01/40.61 % (2697658)Peak memory usage: 147 MB % 284.01/40.61 % (2697658)Instructions burned: 21174 (million) % 284.01/40.61 % (2698020)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=288246728:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2835 on theBenchmark for (2835ds/4081Mi) % 284.01/40.61 % (2697856)Instruction limit reached! % 284.01/40.61 % (2697856)------------------------------ % 284.01/40.61 % (2697856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.01/40.61 % (2697856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.01/40.61 % (2697856)CaDiCaL version: 2.1.3 % 284.01/40.61 % (2697856)Termination reason: Instruction limit % 284.01/40.61 % (2697856)Termination phase: Saturation % 284.01/40.61 % (2697856)Time elapsed: 2.314 s % 284.01/40.61 % (2697856)Peak memory usage: 100 MB % 284.01/40.61 % (2697856)Instructions burned: 3554 (million) % 284.01/40.61 % (2698023)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=4044859188:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2831 on theBenchmark for (2831ds/20260Mi) % 284.01/40.61 % (2697668)Instruction limit reached! % 284.01/40.61 % (2697668)------------------------------ % 284.01/40.61 % (2697668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.01/40.61 % (2697668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.01/40.61 % (2697668)CaDiCaL version: 2.1.3 % 284.01/40.61 % (2697668)Termination reason: Instruction limit % 284.01/40.61 % (2697668)Termination phase: Saturation % 284.01/40.61 % (2697668)Time elapsed: 9.149 s % 284.01/40.61 % (2697668)Peak memory usage: 167 MB % 284.01/40.61 % (2697668)Instructions burned: 17165 (million) % 284.01/40.61 % (2697919)Instruction limit reached! % 284.01/40.61 % (2697919)------------------------------ % 284.01/40.61 % (2697919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.01/40.61 % (2697919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.01/40.61 % (2697919)CaDiCaL version: 2.1.3 % 284.01/40.61 % (2697919)Termination reason: Instruction limit % 284.01/40.61 % (2697919)Termination phase: Saturation % 284.01/40.61 % (2697919)Time elapsedTerminated %------------------------------------------------------------------------------