%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW582_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:51 PM UTC 2026 % Result : Timeout 289.78s 41.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW582_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.20 % Computer : n020.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:20:35 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.24 Running first-order theorem proving % 0.08/0.24 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.26/1.16 % (194441)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.26/1.16 % (194448)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=225981870:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.26/1.16 % (194446)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4004459729:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.26/1.16 % (194446)Instruction limit reached! % 3.26/1.16 % (194446)------------------------------ % 3.26/1.16 % (194446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.26/1.16 % (194446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.26/1.16 % (194446)CaDiCaL version: 2.1.3 % 3.26/1.16 % (194446)Termination reason: Instruction limit % 3.26/1.16 % (194446)Termination phase: Property scanning % 3.26/1.16 % (194446)Time elapsed: 0.007 s % 3.26/1.16 % (194446)Peak memory usage: 87 MB % 3.26/1.16 % (194446)Instructions burned: 14 (million) % 3.26/1.16 % (194450)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1029017288:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.26/1.16 % (194447)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1631274130:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.26/1.16 % (194450)Instruction limit reached! % 3.26/1.16 % (194450)------------------------------ % 3.26/1.16 % (194450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.26/1.16 % (194450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.26/1.16 % (194450)CaDiCaL version: 2.1.3 % 3.26/1.16 % (194450)Termination reason: Instruction limit % 3.26/1.16 % (194450)Termination phase: Preprocessing 3 % 3.26/1.16 % (194450)Time elapsed: 0.003 s % 3.26/1.16 % (194450)Peak memory usage: 86 MB % 3.26/1.16 % (194450)Instructions burned: 5 (million) % 3.26/1.16 % (194452)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1337141380:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.26/1.16 % (194451)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4159737169:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.26/1.16 % (194449)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1795882612:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.26/1.16 % (194449)Instruction limit reached! % 3.26/1.16 % (194449)------------------------------ % 3.26/1.16 % (194449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.26/1.16 % (194449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.26/1.16 % (194449)CaDiCaL version: 2.1.3 % 3.26/1.16 % (194449)Termination reason: Instruction limit % 3.26/1.16 % (194449)Termination phase: Property scanning % 3.26/1.16 % (194449)Time elapsed: 0.005 s % 3.26/1.16 % (194449)Peak memory usage: 86 MB % 3.26/1.16 % (194449)Instructions burned: 9 (million) % 3.26/1.16 % (194452)Instruction limit reached! % 3.26/1.16 % (194452)------------------------------ % 3.26/1.16 % (194452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.26/1.16 % (194452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.26/1.16 % (194452)CaDiCaL version: 2.1.3 % 3.26/1.16 % (194452)Termination reason: Instruction limit % 3.26/1.16 % (194452)Termination phase: Saturation % 3.26/1.16 % (194452)Time elapsed: 0.042 s % 3.26/1.16 % (194452)Peak memory usage: 116 MB % 3.26/1.16 % (194452)Instructions burned: 34 (million) % 3.26/1.16 % (194451)Instruction limit reached! % 3.26/1.16 % (194451)------------------------------ % 3.26/1.16 % (194451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.26/1.16 % (194451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.26/1.16 % (194451)CaDiCaL version: 2.1.3 % 3.26/1.16 % (194451)Termination reason: Instruction limit % 3.26/1.16 % (194451)Termination phase: Saturation % 3.26/1.16 % (194451)Time elapsed: 0.052 s % 3.26/1.16 % (194451)Peak memory usage: 116 MB % 3.26/1.16 % (194451)Instructions burned: 46 (million) % 3.26/1.16 % (194448)Instruction limit reached! % 3.26/1.16 % (194448)------------------------------ % 3.26/1.16 % (194448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.26/1.16 % (194448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.26/1.16 % (194448)CaDiCaL version: 2.1.3 % 3.82/1.29 % (194448)Termination reason: Instruction limit % 3.82/1.29 % (194448)Termination phase: Saturation % 3.82/1.29 % (194448)Time elapsed: 0.093 s % 3.82/1.29 % (194448)Peak memory usage: 119 MB % 3.82/1.29 % (194448)Instructions burned: 201 (million) % 3.82/1.29 % (194457)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3354346464:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.82/1.29 % (194457)Instruction limit reached! % 3.82/1.29 % (194457)------------------------------ % 3.82/1.29 % (194457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.29 % (194457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.29 % (194457)CaDiCaL version: 2.1.3 % 3.82/1.29 % (194457)Termination reason: Instruction limit % 3.82/1.29 % (194457)Termination phase: Saturation % 3.82/1.29 % (194457)Time elapsed: 0.009 s % 3.82/1.29 % (194457)Peak memory usage: 88 MB % 3.82/1.29 % (194457)Instructions burned: 15 (million) % 3.82/1.29 % (194462)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3167469711:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 3.82/1.29 % (194461)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=541326761:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 3.82/1.29 % (194462)Instruction limit reached! % 3.82/1.29 % (194462)------------------------------ % 3.82/1.29 % (194462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.29 % (194462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.29 % (194462)CaDiCaL version: 2.1.3 % 3.82/1.29 % (194462)Termination reason: Instruction limit % 3.82/1.29 % (194462)Termination phase: Saturation % 3.82/1.29 % (194462)Time elapsed: 0.008 s % 3.82/1.29 % (194462)Peak memory usage: 88 MB % 3.82/1.29 % (194462)Instructions burned: 16 (million) % 3.82/1.29 % (194465)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=832634311:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 3.82/1.29 % (194447)Instruction limit reached! % 3.82/1.29 % (194447)------------------------------ % 3.82/1.29 % (194447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.29 % (194447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.29 % (194447)CaDiCaL version: 2.1.3 % 3.82/1.29 % (194447)Termination reason: Instruction limit % 3.82/1.29 % (194447)Termination phase: Property scanning % 3.82/1.29 % (194447)Time elapsed: 0.157 s % 3.82/1.29 % (194447)Peak memory usage: 118 MB % 3.82/1.29 % (194447)Instructions burned: 308 (million) % 3.82/1.29 % (194461)Instruction limit reached! % 3.82/1.29 % (194461)------------------------------ % 3.82/1.29 % (194461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.29 % (194461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.29 % (194461)CaDiCaL version: 2.1.3 % 3.82/1.29 % (194461)Termination reason: Instruction limit % 3.82/1.29 % (194461)Termination phase: Clausification % 3.82/1.29 % (194461)Time elapsed: 0.023 s % 3.82/1.29 % (194461)Peak memory usage: 94 MB % 3.82/1.29 % (194461)Instructions burned: 29 (million) % 3.82/1.29 % (194465)Instruction limit reached! % 3.82/1.29 % (194465)------------------------------ % 3.82/1.29 % (194465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.29 % (194465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.82/1.29 % (194465)CaDiCaL version: 2.1.3 % 3.82/1.29 % (194465)Termination reason: Instruction limit % 3.82/1.29 % (194465)Termination phase: Saturation % 3.82/1.29 % (194465)Time elapsed: 0.024 s % 3.82/1.29 % (194465)Peak memory usage: 89 MB % 3.82/1.29 % (194465)Instructions burned: 87 (million) % 3.82/1.29 % (194464)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=1982711326:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 3.82/1.29 % (194463)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1915968743:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 3.82/1.29 % (194464)Instruction limit reached! % 3.82/1.29 % (194464)------------------------------ % 3.82/1.29 % (194464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.82/1.29 % (194464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.83/1.46 % (194464)CaDiCaL version: 2.1.3 % 4.83/1.46 % (194464)Termination reason: Instruction limit % 4.83/1.46 % (194464)Termination phase: Saturation % 4.83/1.46 % (194464)Time elapsed: 0.016 s % 4.83/1.46 % (194464)Peak memory usage: 90 MB % 4.83/1.46 % (194464)Instructions burned: 28 (million) % 4.83/1.46 % (194463)Instruction limit reached! % 4.83/1.46 % (194463)------------------------------ % 4.83/1.46 % (194463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.83/1.46 % (194463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.83/1.46 % (194463)CaDiCaL version: 2.1.3 % 4.83/1.46 % (194463)Termination reason: Instruction limit % 4.83/1.46 % (194463)Termination phase: Saturation % 4.83/1.46 % (194463)Time elapsed: 0.017 s % 4.83/1.46 % (194463)Peak memory usage: 89 MB % 4.83/1.46 % (194463)Instructions burned: 25 (million) % 4.83/1.46 % (194474)lrs+10_1_thi=all:si=on:fd=off:random_seed=4156436593:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 4.83/1.46 % (194469)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2134600741:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi) % 4.83/1.46 % (194469)Instruction limit reached! % 4.83/1.46 % (194469)------------------------------ % 4.83/1.46 % (194469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.83/1.46 % (194469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.83/1.46 % (194469)CaDiCaL version: 2.1.3 % 4.83/1.46 % (194469)Termination reason: Instruction limit % 4.83/1.46 % (194469)Termination phase: Unused predicate definition removal % 4.83/1.46 % (194469)Time elapsed: 0.002 s % 4.83/1.46 % (194469)Peak memory usage: 85 MB % 4.83/1.46 % (194469)Instructions burned: 3 (million) % 4.83/1.46 % (194471)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2457692904:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi) % 4.83/1.46 % (194474)Instruction limit reached! % 4.83/1.46 % (194474)------------------------------ % 4.83/1.46 % (194474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.83/1.46 % (194474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.83/1.46 % (194474)CaDiCaL version: 2.1.3 % 4.83/1.46 % (194474)Termination reason: Instruction limit % 4.83/1.46 % (194474)Termination phase: Saturation % 4.83/1.46 % (194474)Time elapsed: 0.034 s % 4.83/1.46 % (194474)Peak memory usage: 116 MB % 4.83/1.46 % (194474)Instructions burned: 55 (million) % 4.83/1.46 % (194472)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2631834637:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 4.83/1.46 % (194473)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=70447275:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 4.83/1.46 % (194472)Instruction limit reached! % 4.83/1.46 % (194472)------------------------------ % 4.83/1.46 % (194472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.83/1.46 % (194472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.83/1.46 % (194472)CaDiCaL version: 2.1.3 % 4.83/1.46 % (194472)Termination reason: Instruction limit % 4.83/1.46 % (194472)Termination phase: Preprocessing 3 % 4.83/1.46 % (194472)Time elapsed: 0.003 s % 4.83/1.46 % (194472)Peak memory usage: 86 MB % 4.83/1.46 % (194472)Instructions burned: 5 (million) % 4.83/1.46 % (194478)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=371249255:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 4.83/1.46 % (194478)Instruction limit reached! % 4.83/1.46 % (194478)------------------------------ % 4.83/1.46 % (194478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.83/1.46 % (194478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.83/1.46 % (194478)CaDiCaL version: 2.1.3 % 4.83/1.46 % (194478)Termination reason: Instruction limit % 4.83/1.46 % (194478)Termination phase: Naming % 4.83/1.46 % (194478)Time elapsed: 0.002 s % 4.83/1.46 % (194478)Peak memory usage: 86 MB % 4.83/1.46 % (194478)Instructions burned: 3 (million) % 4.83/1.46 % (194477)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=1161388001:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 4.83/1.46 % (194477)Instruction limit reached! % 6.28/1.67 % (194477)------------------------------ % 6.28/1.67 % (194477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194477)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194477)Termination reason: Instruction limit % 6.28/1.67 % (194477)Termination phase: Preprocessing 3 % 6.28/1.67 % (194477)Time elapsed: 0.004 s % 6.28/1.67 % (194477)Peak memory usage: 86 MB % 6.28/1.67 % (194477)Instructions burned: 8 (million) % 6.28/1.67 % (194481)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=499541275:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.28/1.67 % (194481)Instruction limit reached! % 6.28/1.67 % (194481)------------------------------ % 6.28/1.67 % (194481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194481)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194481)Termination reason: Instruction limit % 6.28/1.67 % (194481)Termination phase: shuffling % 6.28/1.67 % (194481)Time elapsed: 0.002 s % 6.28/1.67 % (194481)Peak memory usage: 85 MB % 6.28/1.67 % (194481)Instructions burned: 3 (million) % 6.28/1.67 % (194483)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3192551935:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.28/1.67 % (194471)Instruction limit reached! % 6.28/1.67 % (194471)------------------------------ % 6.28/1.67 % (194471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194471)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194471)Termination reason: Instruction limit % 6.28/1.67 % (194471)Termination phase: Saturation % 6.28/1.67 % (194471)Time elapsed: 0.122 s % 6.28/1.67 % (194471)Peak memory usage: 91 MB % 6.28/1.67 % (194471)Instructions burned: 182 (million) % 6.28/1.67 % (194473)Instruction limit reached! % 6.28/1.67 % (194473)------------------------------ % 6.28/1.67 % (194473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194473)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194473)Termination reason: Instruction limit % 6.28/1.67 % (194473)Termination phase: Saturation % 6.28/1.67 % (194473)Time elapsed: 0.089 s % 6.28/1.67 % (194473)Peak memory usage: 134 MB % 6.28/1.67 % (194473)Instructions burned: 66 (million) % 6.28/1.67 % (194486)dis+10_1_si=on:random_seed=2273296330:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi) % 6.28/1.67 % (194486)Instruction limit reached! % 6.28/1.67 % (194486)------------------------------ % 6.28/1.67 % (194486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194486)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194486)Termination reason: Instruction limit % 6.28/1.67 % (194486)Termination phase: Equality proxy % 6.28/1.67 % (194486)Time elapsed: 0.006 s % 6.28/1.67 % (194486)Peak memory usage: 86 MB % 6.28/1.67 % (194486)Instructions burned: 12 (million) % 6.28/1.67 % (194483)Instruction limit reached! % 6.28/1.67 % (194483)------------------------------ % 6.28/1.67 % (194483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194483)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194483)Termination reason: Instruction limit % 6.28/1.67 % (194483)Termination phase: Saturation % 6.28/1.67 % (194483)Time elapsed: 0.063 s % 6.28/1.67 % (194483)Peak memory usage: 118 MB % 6.28/1.67 % (194483)Instructions burned: 127 (million) % 6.28/1.67 % (194489)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=203540722:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi) % 6.28/1.67 % (194489)Refutation not found, incomplete strategy % 6.28/1.67 % (194489)------------------------------ % 6.28/1.67 % (194489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.28/1.67 % (194489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.28/1.67 % (194489)CaDiCaL version: 2.1.3 % 6.28/1.67 % (194489)Termination reason: Refutation not found, incomplete strategy % 6.28/1.67 % (194489)Time elapsed: 0.012 s % 6.28/1.67 % (194489)Peak memory usage: 89 MB % 6.28/1.67 % (194489)Instructions burned: 20 (million) % 7.98/1.92 % (194490)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=338626714: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_2995 on theBenchmark for (2995ds/35Mi) % 7.98/1.92 % (194490)Instruction limit reached! % 7.98/1.92 % (194490)------------------------------ % 7.98/1.92 % (194490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.92 % (194490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.92 % (194490)CaDiCaL version: 2.1.3 % 7.98/1.92 % (194490)Termination reason: Instruction limit % 7.98/1.92 % (194490)Termination phase: Saturation % 7.98/1.92 % (194490)Time elapsed: 0.017 s % 7.98/1.92 % (194490)Peak memory usage: 89 MB % 7.98/1.92 % (194490)Instructions burned: 35 (million) % 7.98/1.92 % (194494)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=899587300:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.98/1.92 % (194493)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1687285719:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.98/1.93 % (194493)Instruction limit reached! % 7.98/1.93 % (194493)------------------------------ % 7.98/1.93 % (194493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.93 % (194493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.93 % (194493)CaDiCaL version: 2.1.3 % 7.98/1.93 % (194493)Termination reason: Instruction limit % 7.98/1.93 % (194493)Termination phase: Preprocessing 2 % 7.98/1.93 % (194493)Time elapsed: 0.002 s % 7.98/1.93 % (194493)Peak memory usage: 85 MB % 7.98/1.93 % (194493)Instructions burned: 3 (million) % 7.98/1.93 % (194494)Instruction limit reached! % 7.98/1.93 % (194494)------------------------------ % 7.98/1.93 % (194494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.93 % (194494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.93 % (194494)CaDiCaL version: 2.1.3 % 7.98/1.93 % (194494)Termination reason: Instruction limit % 7.98/1.93 % (194494)Termination phase: Function definition elimination % 7.98/1.93 % (194494)Time elapsed: 0.005 s % 7.98/1.93 % (194494)Peak memory usage: 86 MB % 7.98/1.93 % (194494)Instructions burned: 9 (million) % 7.98/1.93 % (194495)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2340956586:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 7.98/1.93 % (194499)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1649265129:i=226:rtra=on:gtg=position:ss=axioms_2994 on theBenchmark for (2994ds/226Mi) % 7.98/1.93 % (194497)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2544567534:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi) % 7.98/1.93 % (194497)Instruction limit reached! % 7.98/1.93 % (194497)------------------------------ % 7.98/1.93 % (194497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.93 % (194497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.93 % (194497)CaDiCaL version: 2.1.3 % 7.98/1.93 % (194497)Termination reason: Instruction limit % 7.98/1.93 % (194497)Termination phase: Saturation % 7.98/1.93 % (194497)Time elapsed: 0.007 s % 7.98/1.93 % (194497)Peak memory usage: 88 MB % 7.98/1.93 % (194497)Instructions burned: 14 (million) % 7.98/1.93 % (194504)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1817381165:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 7.98/1.93 % (194501)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4245184381:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 7.98/1.93 % (194505)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=904165943:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 7.98/1.93 % (194499)Instruction limit reached! % 7.98/1.93 % (194499)------------------------------ % 7.98/1.93 % (194499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.93 % (194499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.93 % (194499)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194499)Termination reason: Instruction limit % 9.93/2.10 % (194499)Termination phase: Saturation % 9.93/2.10 % (194499)Time elapsed: 0.088 s % 9.93/2.10 % (194499)Peak memory usage: 117 MB % 9.93/2.10 % (194499)Instructions burned: 227 (million) % 9.93/2.10 % (194501)Instruction limit reached! % 9.93/2.10 % (194501)------------------------------ % 9.93/2.10 % (194501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.93/2.10 % (194501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/2.10 % (194501)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194501)Termination reason: Instruction limit % 9.93/2.10 % (194501)Termination phase: Property scanning % 9.93/2.10 % (194501)Time elapsed: 0.005 s % 9.93/2.10 % (194501)Peak memory usage: 86 MB % 9.93/2.10 % (194501)Instructions burned: 10 (million) % 9.93/2.10 % (194505)Instruction limit reached! % 9.93/2.10 % (194505)------------------------------ % 9.93/2.10 % (194505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.93/2.10 % (194505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/2.10 % (194505)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194505)Termination reason: Instruction limit % 9.93/2.10 % (194505)Termination phase: Saturation % 9.93/2.10 % (194505)Time elapsed: 0.043 s % 9.93/2.10 % (194505)Peak memory usage: 90 MB % 9.93/2.10 % (194505)Instructions burned: 75 (million) % 9.93/2.10 % (194509)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=2416071865:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 9.93/2.10 % (194489)------------------------------ % 9.93/2.10 % (194489)------------------------------ % 9.93/2.10 % (194504)Instruction limit reached! % 9.93/2.10 % (194504)------------------------------ % 9.93/2.10 % (194504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.93/2.10 % (194504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/2.10 % (194504)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194504)Termination reason: Instruction limit % 9.93/2.10 % (194504)Termination phase: Saturation % 9.93/2.10 % (194504)Time elapsed: 0.088 s % 9.93/2.10 % (194504)Peak memory usage: 133 MB % 9.93/2.10 % (194504)Instructions burned: 72 (million) % 9.93/2.10 % (194495)Instruction limit reached! % 9.93/2.10 % (194495)------------------------------ % 9.93/2.10 % (194495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.93/2.10 % (194495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/2.10 % (194495)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194495)Termination reason: Instruction limit % 9.93/2.10 % (194495)Termination phase: Saturation % 9.93/2.10 % (194495)Time elapsed: 0.203 s % 9.93/2.10 % (194495)Peak memory usage: 91 MB % 9.93/2.10 % (194495)Instructions burned: 371 (million) % 9.93/2.10 % (194513)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3876713695:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 9.93/2.10 % (194514)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3074275751:i=131:rtra=on_2992 on theBenchmark for (2992ds/131Mi) % 9.93/2.10 % (194513)Instruction limit reached! % 9.93/2.10 % (194513)------------------------------ % 9.93/2.10 % (194513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.93/2.10 % (194513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/2.10 % (194513)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194513)Termination reason: Instruction limit % 9.93/2.10 % (194513)Termination phase: Property scanning % 9.93/2.10 % (194513)Time elapsed: 0.053 s % 9.93/2.10 % (194513)Peak memory usage: 118 MB % 9.93/2.10 % (194513)Instructions burned: 133 (million) % 9.93/2.10 % (194515)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1497441719:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 9.93/2.10 % (194509)Instruction limit reached! % 9.93/2.10 % (194509)------------------------------ % 9.93/2.10 % (194509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.93/2.10 % (194509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.93/2.10 % (194509)CaDiCaL version: 2.1.3 % 9.93/2.10 % (194509)Termination reason: Instruction limit % 9.93/2.10 % (194509)Termination phase: Property scanning % 9.93/2.10 % (194509)Time elapsed: 0.146 s % 9.93/2.10 % (194509)Peak memory usage: 118 MB % 9.93/2.10 % (194509)Instructions burned: 295 (million) % 11.37/2.43 % (194517)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3174843956:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 11.37/2.43 % (194518)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3736034701:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi) % 11.37/2.43 % (194520)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2456408369:i=131:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 11.37/2.43 % (194515)Instruction limit reached! % 11.37/2.43 % (194515)------------------------------ % 11.37/2.43 % (194515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.43 % (194515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.43 % (194515)CaDiCaL version: 2.1.3 % 11.37/2.43 % (194515)Termination reason: Instruction limit % 11.37/2.43 % (194515)Termination phase: Saturation % 11.37/2.43 % (194515)Time elapsed: 0.066 s % 11.37/2.43 % (194515)Peak memory usage: 133 MB % 11.37/2.43 % (194515)Instructions burned: 40 (million) % 11.37/2.43 % (194522)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=1282811118:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 11.37/2.43 % (194514)Instruction limit reached! % 11.37/2.43 % (194514)------------------------------ % 11.37/2.43 % (194514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.43 % (194514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.43 % (194514)CaDiCaL version: 2.1.3 % 11.37/2.43 % (194514)Termination reason: Instruction limit % 11.37/2.43 % (194514)Termination phase: Saturation % 11.37/2.43 % (194514)Time elapsed: 0.134 s % 11.37/2.43 % (194514)Peak memory usage: 134 MB % 11.37/2.43 % (194514)Instructions burned: 131 (million) % 11.37/2.43 % (194526)dis+10_1_si=on:random_seed=2768596084:s2a=on:i=1000:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/1000Mi) % 11.37/2.43 % (194520)Instruction limit reached! % 11.37/2.43 % (194520)------------------------------ % 11.37/2.43 % (194520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.43 % (194520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.43 % (194520)CaDiCaL version: 2.1.3 % 11.37/2.43 % (194520)Termination reason: Instruction limit % 11.37/2.43 % (194520)Termination phase: Saturation % 11.37/2.43 % (194520)Time elapsed: 0.108 s % 11.37/2.43 % (194520)Peak memory usage: 118 MB % 11.37/2.43 % (194520)Instructions burned: 131 (million) % 11.37/2.43 % (194522)Instruction limit reached! % 11.37/2.43 % (194522)------------------------------ % 11.37/2.43 % (194522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.43 % (194522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.43 % (194522)CaDiCaL version: 2.1.3 % 11.37/2.43 % (194522)Termination reason: Instruction limit % 11.37/2.43 % (194522)Termination phase: Saturation % 11.37/2.43 % (194522)Time elapsed: 0.107 s % 11.37/2.43 % (194522)Peak memory usage: 117 MB % 11.37/2.43 % (194522)Instructions burned: 261 (million) % 11.37/2.43 % (194529)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3006452378:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 11.37/2.43 % (194517)Instruction limit reached! % 11.37/2.43 % (194517)------------------------------ % 11.37/2.43 % (194517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.43 % (194517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.43 % (194517)CaDiCaL version: 2.1.3 % 11.37/2.43 % (194517)Termination reason: Instruction limit % 11.37/2.43 % (194517)Termination phase: Saturation % 11.37/2.43 % (194517)Time elapsed: 0.178 s % 11.37/2.43 % (194517)Peak memory usage: 91 MB % 11.37/2.43 % (194517)Instructions burned: 309 (million) % 11.37/2.43 % (194530)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1562475890:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi) % 11.37/2.43 % (194533)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=517997416:i=121:nm=16:rtra=on_2988 on theBenchmark for (2988ds/121Mi) % 11.37/2.43 % (194532)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1842941838:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.04/2.71 % (194530)Instruction limit reached! % 13.04/2.71 % (194530)------------------------------ % 13.04/2.71 % (194530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194530)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194530)Termination reason: Instruction limit % 13.04/2.71 % (194530)Termination phase: Saturation % 13.04/2.71 % (194530)Time elapsed: 0.094 s % 13.04/2.71 % (194530)Peak memory usage: 90 MB % 13.04/2.71 % (194530)Instructions burned: 142 (million) % 13.04/2.71 % (194533)Instruction limit reached! % 13.04/2.71 % (194533)------------------------------ % 13.04/2.71 % (194533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194533)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194533)Termination reason: Instruction limit % 13.04/2.71 % (194533)Termination phase: Saturation % 13.04/2.71 % (194533)Time elapsed: 0.037 s % 13.04/2.71 % (194533)Peak memory usage: 89 MB % 13.04/2.71 % (194533)Instructions burned: 122 (million) % 13.04/2.71 % (194532)Refutation not found, incomplete strategy % 13.04/2.71 % (194532)------------------------------ % 13.04/2.71 % (194532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194532)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194532)Termination reason: Refutation not found, incomplete strategy % 13.04/2.71 % (194532)Time elapsed: 0.046 s % 13.04/2.71 % (194532)Peak memory usage: 116 MB % 13.04/2.71 % (194532)Instructions burned: 38 (million) % 13.04/2.71 % (194536)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=2676509883:s2a=on:i=128:s2at=5:ins=3:rtra=on_2988 on theBenchmark for (2988ds/128Mi) % 13.04/2.71 % (194540)dis+1010_1_to=kbo:si=on:random_seed=1051032793:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2987 on theBenchmark for (2987ds/175Mi) % 13.04/2.71 % (194518)Instruction limit reached! % 13.04/2.71 % (194518)------------------------------ % 13.04/2.71 % (194518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194518)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194518)Termination reason: Instruction limit % 13.04/2.71 % (194518)Termination phase: Saturation % 13.04/2.71 % (194518)Time elapsed: 0.378 s % 13.04/2.71 % (194518)Peak memory usage: 139 MB % 13.04/2.71 % (194518)Instructions burned: 599 (million) % 13.04/2.71 % (194529)Instruction limit reached! % 13.04/2.71 % (194529)------------------------------ % 13.04/2.71 % (194529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194529)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194529)Termination reason: Instruction limit % 13.04/2.71 % (194529)Termination phase: Saturation % 13.04/2.71 % (194529)Time elapsed: 0.225 s % 13.04/2.71 % (194529)Peak memory usage: 94 MB % 13.04/2.71 % (194529)Instructions burned: 384 (million) % 13.04/2.71 % (194539)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=975364692:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi) % 13.04/2.71 % (194536)Instruction limit reached! % 13.04/2.71 % (194536)------------------------------ % 13.04/2.71 % (194536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194536)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194536)Termination reason: Instruction limit % 13.04/2.71 % (194536)Termination phase: Saturation % 13.04/2.71 % (194536)Time elapsed: 0.106 s % 13.04/2.71 % (194536)Peak memory usage: 118 MB % 13.04/2.71 % (194536)Instructions burned: 129 (million) % 13.04/2.71 % (194540)Instruction limit reached! % 13.04/2.71 % (194540)------------------------------ % 13.04/2.71 % (194540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.71 % (194540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.71 % (194540)CaDiCaL version: 2.1.3 % 13.04/2.71 % (194540)Termination reason: Instruction limit % 13.04/2.71 % (194540)Termination phase: Property scanning % 13.04/2.71 % (194540)Time elapsed: 0.059 s % 13.04/2.71 % (194540)Peak memory usage: 118 MB % 13.04/2.71 % (194540)Instructions burned: 177 (million) % 15.18/3.01 % (194539)Instruction limit reached! % 15.18/3.01 % (194539)------------------------------ % 15.18/3.01 % (194539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.18/3.01 % (194539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.18/3.01 % (194539)CaDiCaL version: 2.1.3 % 15.18/3.01 % (194539)Termination reason: Instruction limit % 15.18/3.01 % (194539)Termination phase: Saturation % 15.18/3.01 % (194539)Time elapsed: 0.048 s % 15.18/3.01 % (194539)Peak memory usage: 116 MB % 15.18/3.01 % (194539)Instructions burned: 39 (million) % 15.18/3.01 % (194544)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3036539479:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi) % 15.18/3.01 % (194543)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2868757775:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 15.18/3.01 % (194547)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3030655340:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.18/3.01 % (194532)------------------------------ % 15.18/3.01 % (194532)------------------------------ % 15.18/3.01 % (194546)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1196686332:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.18/3.01 % (194548)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1454581522:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 15.18/3.01 % (194547)Instruction limit reached! % 15.18/3.01 % (194547)------------------------------ % 15.18/3.01 % (194547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.18/3.01 % (194547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.18/3.01 % (194547)CaDiCaL version: 2.1.3 % 15.18/3.01 % (194547)Termination reason: Instruction limit % 15.18/3.01 % (194547)Termination phase: Saturation % 15.18/3.01 % (194547)Time elapsed: 0.112 s % 15.18/3.01 % (194547)Peak memory usage: 118 MB % 15.18/3.01 % (194547)Instructions burned: 352 (million) % 15.18/3.01 % (194553)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1241645614:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi) % 15.18/3.01 % (194546)Instruction limit reached! % 15.18/3.01 % (194546)------------------------------ % 15.18/3.01 % (194546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.18/3.01 % (194546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.18/3.01 % (194546)CaDiCaL version: 2.1.3 % 15.18/3.01 % (194546)Termination reason: Instruction limit % 15.18/3.01 % (194546)Termination phase: Property scanning % 15.18/3.01 % (194546)Time elapsed: 0.120 s % 15.18/3.01 % (194546)Peak memory usage: 118 MB % 15.18/3.01 % (194546)Instructions burned: 216 (million) % 15.18/3.01 % (194555)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1512715146:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 15.18/3.01 % (194526)Instruction limit reached! % 15.18/3.01 % (194526)------------------------------ % 15.18/3.01 % (194526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.18/3.01 % (194526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.18/3.01 % (194526)CaDiCaL version: 2.1.3 % 15.18/3.01 % (194526)Termination reason: Instruction limit % 15.18/3.01 % (194526)Termination phase: Saturation % 15.18/3.01 % (194526)Time elapsed: 0.605 s % 15.18/3.01 % (194526)Peak memory usage: 94 MB % 15.18/3.01 % (194526)Instructions burned: 1001 (million) % 15.18/3.01 % (194548)Instruction limit reached! % 15.18/3.01 % (194548)------------------------------ % 15.18/3.01 % (194548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.18/3.01 % (194548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.18/3.01 % (194548)CaDiCaL version: 2.1.3 % 15.18/3.01 % (194548)Termination reason: Instruction limit % 15.18/3.01 % (194548)Termination phase: Saturation % 15.18/3.01 % (194548)Time elapsed: 0.167 s % 15.18/3.01 % (194548)Peak memory usage: 91 MB % 15.18/3.01 % (194548)Instructions burned: 296 (million) % 15.18/3.01 % (194543)Instruction limit reached! % 15.18/3.01 % (194543)------------------------------ % 15.18/3.01 % (194543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.18/3.01 % (194543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.54/3.25 % (194543)CaDiCaL version: 2.1.3 % 17.54/3.25 % (194543)Termination reason: Instruction limit % 17.54/3.25 % (194543)Termination phase: Saturation % 17.54/3.25 % (194543)Time elapsed: 0.253 s % 17.54/3.25 % (194543)Peak memory usage: 120 MB % 17.54/3.25 % (194543)Instructions burned: 329 (million) % 17.54/3.25 % (194544)Instruction limit reached! % 17.54/3.25 % (194544)------------------------------ % 17.54/3.25 % (194544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.54/3.25 % (194544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.54/3.25 % (194544)CaDiCaL version: 2.1.3 % 17.54/3.25 % (194544)Termination reason: Instruction limit % 17.54/3.25 % (194544)Termination phase: Saturation % 17.54/3.25 % (194544)Time elapsed: 0.276 s % 17.54/3.25 % (194544)Peak memory usage: 133 MB % 17.54/3.25 % (194544)Instructions burned: 484 (million) % 17.54/3.25 % (194557)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3434078129:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi) % 17.54/3.25 % (194555)Instruction limit reached! % 17.54/3.25 % (194555)------------------------------ % 17.54/3.25 % (194555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.54/3.25 % (194555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.54/3.25 % (194555)CaDiCaL version: 2.1.3 % 17.54/3.25 % (194555)Termination reason: Instruction limit % 17.54/3.25 % (194555)Termination phase: Saturation % 17.54/3.25 % (194555)Time elapsed: 0.113 s % 17.54/3.25 % (194555)Peak memory usage: 117 MB % 17.54/3.25 % (194555)Instructions burned: 284 (million) % 17.54/3.25 % (194559)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2842819882:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.54/3.25 % (194560)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1446640576:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 17.54/3.25 % (194561)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4102260482:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi) % 17.54/3.25 % (194553)Instruction limit reached! % 17.54/3.25 % (194553)------------------------------ % 17.54/3.25 % (194553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.54/3.25 % (194553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.54/3.25 % (194553)CaDiCaL version: 2.1.3 % 17.54/3.25 % (194553)Termination reason: Instruction limit % 17.54/3.25 % (194553)Termination phase: Saturation % 17.54/3.25 % (194553)Time elapsed: 0.229 s % 17.54/3.25 % (194553)Peak memory usage: 118 MB % 17.54/3.25 % (194553)Instructions burned: 328 (million) % 17.54/3.25 % (194564)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3731323747:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi) % 17.54/3.25 % (194562)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=2714204056:avsq=on:i=276:avsqr=1,2:rtra=on_2982 on theBenchmark for (2982ds/276Mi) % 17.54/3.25 % (194559)Instruction limit reached! % 17.54/3.25 % (194559)------------------------------ % 17.54/3.25 % (194559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.54/3.25 % (194559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.54/3.25 % (194559)CaDiCaL version: 2.1.3 % 17.54/3.25 % (194559)Termination reason: Instruction limit % 17.54/3.25 % (194559)Termination phase: Saturation % 17.54/3.25 % (194559)Time elapsed: 0.170 s % 17.54/3.25 % (194559)Peak memory usage: 114 MB % 17.54/3.25 % (194559)Instructions burned: 321 (million) % 17.54/3.25 % (194557)Instruction limit reached! % 17.54/3.25 % (194557)------------------------------ % 17.54/3.25 % (194557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.54/3.25 % (194557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.54/3.25 % (194557)CaDiCaL version: 2.1.3 % 17.54/3.25 % (194557)Termination reason: Instruction limit % 17.54/3.25 % (194557)Termination phase: Property scanning % 17.54/3.25 % (194557)Time elapsed: 0.215 s % 17.54/3.25 % (194557)Peak memory usage: 118 MB % 17.54/3.25 % (194557)Instructions burned: 485 (million) % 17.54/3.25 % (194568)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2870876346:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/387Mi) % 18.84/3.66 % (194564)Instruction limit reached! % 18.84/3.66 % (194564)------------------------------ % 18.84/3.66 % (194564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.66 % (194564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.66 % (194564)CaDiCaL version: 2.1.3 % 18.84/3.66 % (194564)Termination reason: Instruction limit % 18.84/3.66 % (194564)Termination phase: Saturation % 18.84/3.66 % (194564)Time elapsed: 0.137 s % 18.84/3.66 % (194564)Peak memory usage: 119 MB % 18.84/3.66 % (194564)Instructions burned: 376 (million) % 18.84/3.66 % (194560)Instruction limit reached! % 18.84/3.66 % (194560)------------------------------ % 18.84/3.66 % (194560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.66 % (194560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.66 % (194560)CaDiCaL version: 2.1.3 % 18.84/3.66 % (194560)Termination reason: Instruction limit % 18.84/3.66 % (194560)Termination phase: Saturation % 18.84/3.66 % (194560)Time elapsed: 0.280 s % 18.84/3.66 % (194560)Peak memory usage: 119 MB % 18.84/3.66 % (194560)Instructions burned: 417 (million) % 18.84/3.66 % (194574)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1690036080:i=359:rtra=on:gtg=exists_top:ss=axioms_2979 on theBenchmark for (2979ds/359Mi) % 18.84/3.66 % (194562)Instruction limit reached! % 18.84/3.66 % (194562)------------------------------ % 18.84/3.66 % (194562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.66 % (194562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.66 % (194562)CaDiCaL version: 2.1.3 % 18.84/3.66 % (194562)Termination reason: Instruction limit % 18.84/3.66 % (194562)Termination phase: Saturation % 18.84/3.66 % (194562)Time elapsed: 0.228 s % 18.84/3.66 % (194562)Peak memory usage: 134 MB % 18.84/3.66 % (194562)Instructions burned: 276 (million) % 18.84/3.66 % (194574)Refutation not found, incomplete strategy % 18.84/3.66 % (194574)------------------------------ % 18.84/3.66 % (194574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.66 % (194574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.66 % (194574)CaDiCaL version: 2.1.3 % 18.84/3.66 % (194574)Termination reason: Refutation not found, incomplete strategy % 18.84/3.66 % (194574)Time elapsed: 0.008 s % 18.84/3.66 % (194574)Peak memory usage: 90 MB % 18.84/3.66 % (194574)Instructions burned: 25 (million) % 18.84/3.66 % (194571)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=195592238:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 18.84/3.66 % (194572)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3514049456:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 18.84/3.66 % (194561)Instruction limit reached! % 18.84/3.66 % (194561)------------------------------ % 18.84/3.66 % (194561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.66 % (194561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.66 % (194561)CaDiCaL version: 2.1.3 % 18.84/3.66 % (194561)Termination reason: Instruction limit % 18.84/3.66 % (194561)Termination phase: Saturation % 18.84/3.66 % (194561)Time elapsed: 0.323 s % 18.84/3.66 % (194561)Peak memory usage: 119 MB % 18.84/3.66 % (194561)Instructions burned: 471 (million) % 18.84/3.66 % (194576)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2111542797:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 18.84/3.66 % (194579)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2375125920:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi) % 18.84/3.66 % (194574)------------------------------ % 18.84/3.66 % (194574)------------------------------ % 18.84/3.66 % (194568)Instruction limit reached! % 18.84/3.66 % (194568)------------------------------ % 18.84/3.66 % (194568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.66 % (194568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.66 % (194568)CaDiCaL version: 2.1.3 % 18.84/3.66 % (194568)Termination reason: Instruction limit % 18.84/3.66 % (194568)Termination phase: Saturation % 24.03/4.07 % (194568)Time elapsed: 0.291 s % 24.03/4.07 % (194568)Peak memory usage: 119 MB % 24.03/4.07 % (194568)Instructions burned: 387 (million) % 24.03/4.07 % (194580)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=2571811444:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi) % 24.03/4.07 % (194572)Instruction limit reached! % 24.03/4.07 % (194572)------------------------------ % 24.03/4.07 % (194572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.03/4.07 % (194572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.03/4.07 % (194572)CaDiCaL version: 2.1.3 % 24.03/4.07 % (194572)Termination reason: Instruction limit % 24.03/4.07 % (194572)Termination phase: Saturation % 24.03/4.07 % (194572)Time elapsed: 0.231 s % 24.03/4.07 % (194572)Peak memory usage: 134 MB % 24.03/4.07 % (194572)Instructions burned: 334 (million) % 24.03/4.07 % (194583)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=347006183:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2976 on theBenchmark for (2976ds/273Mi) % 24.03/4.07 % (194584)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2258877308:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 24.03/4.07 % (194571)Instruction limit reached! % 24.03/4.07 % (194571)------------------------------ % 24.03/4.07 % (194571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.03/4.07 % (194571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.03/4.07 % (194571)CaDiCaL version: 2.1.3 % 24.03/4.07 % (194571)Termination reason: Instruction limit % 24.03/4.07 % (194571)Termination phase: Saturation % 24.03/4.07 % (194571)Time elapsed: 0.323 s % 24.03/4.07 % (194571)Peak memory usage: 93 MB % 24.03/4.07 % (194571)Instructions burned: 513 (million) % 24.03/4.07 % (194579)Instruction limit reached! % 24.03/4.07 % (194579)------------------------------ % 24.03/4.07 % (194579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.03/4.07 % (194579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.03/4.07 % (194579)CaDiCaL version: 2.1.3 % 24.03/4.07 % (194579)Termination reason: Instruction limit % 24.03/4.07 % (194579)Termination phase: Saturation % 24.03/4.07 % (194579)Time elapsed: 0.203 s % 24.03/4.07 % (194579)Peak memory usage: 118 MB % 24.03/4.07 % (194579)Instructions burned: 261 (million) % 24.03/4.07 % (194583)Instruction limit reached! % 24.03/4.07 % (194583)------------------------------ % 24.03/4.07 % (194583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.03/4.07 % (194583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.03/4.07 % (194583)CaDiCaL version: 2.1.3 % 24.03/4.07 % (194583)Termination reason: Instruction limit % 24.03/4.07 % (194583)Termination phase: Saturation % 24.03/4.07 % (194583)Time elapsed: 0.107 s % 24.03/4.07 % (194583)Peak memory usage: 92 MB % 24.03/4.07 % (194583)Instructions burned: 273 (million) % 24.03/4.07 % (194576)Instruction limit reached! % 24.03/4.07 % (194576)------------------------------ % 24.03/4.07 % (194576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.03/4.07 % (194576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.03/4.07 % (194576)CaDiCaL version: 2.1.3 % 24.03/4.07 % (194576)Termination reason: Instruction limit % 24.03/4.07 % (194576)Termination phase: Saturation % 24.03/4.07 % (194576)Time elapsed: 0.245 s % 24.03/4.07 % (194576)Peak memory usage: 121 MB % 24.03/4.07 % (194576)Instructions burned: 342 (million) % 24.03/4.07 % (194580)Instruction limit reached! % 24.03/4.07 % (194580)------------------------------ % 24.03/4.07 % (194580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.03/4.07 % (194580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.03/4.07 % (194580)CaDiCaL version: 2.1.3 % 24.03/4.07 % (194580)Termination reason: Instruction limit % 24.03/4.07 % (194580)Termination phase: Saturation % 24.03/4.07 % (194580)Time elapsed: 0.183 s % 24.03/4.07 % (194580)Peak memory usage: 117 MB % 24.03/4.07 % (194580)Instructions burned: 236 (million) % 24.03/4.07 % (194587)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1729292412:i=4428:doe=on:fsr=off:rtra=on_2976 on theBenchmark for (2976ds/4428Mi) % 24.03/4.07 % (194584)Instruction limit reached! % 24.03/4.07 % (194584)------------------------------ % 24.03/4.07 % (194584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.89/4.64 % (194584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.64 % (194584)CaDiCaL version: 2.1.3 % 26.89/4.64 % (194584)Termination reason: Instruction limit % 26.89/4.64 % (194584)Termination phase: Saturation % 26.89/4.64 % (194584)Time elapsed: 0.098 s % 26.89/4.64 % (194584)Peak memory usage: 91 MB % 26.89/4.64 % (194584)Instructions burned: 147 (million) % 26.89/4.64 % (194591)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2762031989:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2975 on theBenchmark for (2975ds/655Mi) % 26.89/4.64 % (194589)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=1695685068:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi) % 26.89/4.64 % (194590)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3201797472:i=1052:rtra=on_2975 on theBenchmark for (2975ds/1052Mi) % 26.89/4.64 % (194593)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=974261106:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi) % 26.89/4.64 % (194594)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3707135547:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 26.89/4.64 % (194594)Refutation not found, incomplete strategy % 26.89/4.64 % (194594)------------------------------ % 26.89/4.64 % (194594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.89/4.64 % (194594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.64 % (194594)CaDiCaL version: 2.1.3 % 26.89/4.64 % (194594)Termination reason: Refutation not found, incomplete strategy % 26.89/4.64 % (194594)Time elapsed: 0.040 s % 26.89/4.64 % (194594)Peak memory usage: 116 MB % 26.89/4.64 % (194594)Instructions burned: 29 (million) % 26.89/4.64 % (194595)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3167709938:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi) % 26.89/4.64 % (194591)Instruction limit reached! % 26.89/4.64 % (194591)------------------------------ % 26.89/4.64 % (194591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.89/4.64 % (194591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.64 % (194591)CaDiCaL version: 2.1.3 % 26.89/4.64 % (194591)Termination reason: Instruction limit % 26.89/4.64 % (194591)Termination phase: Saturation % 26.89/4.64 % (194591)Time elapsed: 0.216 s % 26.89/4.64 % (194591)Peak memory usage: 94 MB % 26.89/4.64 % (194591)Instructions burned: 655 (million) % 26.89/4.64 % (194589)Instruction limit reached! % 26.89/4.64 % (194589)------------------------------ % 26.89/4.64 % (194589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.89/4.64 % (194589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.64 % (194589)CaDiCaL version: 2.1.3 % 26.89/4.64 % (194589)Termination reason: Instruction limit % 26.89/4.64 % (194589)Termination phase: Saturation % 26.89/4.64 % (194589)Time elapsed: 0.226 s % 26.89/4.64 % (194589)Peak memory usage: 135 MB % 26.89/4.64 % (194589)Instructions burned: 276 (million) % 26.89/4.64 % (194602)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 % 26.89/4.64 % (194602)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2563455849:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi) % 26.89/4.64 % (194594)------------------------------ % 26.89/4.64 % (194594)------------------------------ % 26.89/4.64 % (194595)Instruction limit reached! % 26.89/4.64 % (194595)------------------------------ % 26.89/4.64 % (194595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.89/4.64 % (194595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.89/4.64 % (194595)CaDiCaL version: 2.1.3 % 26.89/4.64 % (194595)Termination reason: Instruction limit % 26.89/4.64 % (194595)Termination phase: Saturation % 26.89/4.64 % (194595)Time elapsed: 0.253 s % 26.89/4.64 % (194595)Peak memory usage: 133 MB % 26.89/4.64 % (194595)Instructions burned: 451 (million) % 26.89/4.64 % (194603)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3298178610:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2971 on theBenchmark for (2971ds/130Mi) % 31.15/5.03 % (194605)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3686363838:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi) % 31.15/5.03 % (194603)Instruction limit reached! % 31.15/5.03 % (194603)------------------------------ % 31.15/5.03 % (194603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.15/5.03 % (194603)CaDiCaL version: 2.1.3 % 31.15/5.03 % (194603)Termination reason: Instruction limit % 31.15/5.03 % (194603)Termination phase: Property scanning % 31.15/5.03 % (194603)Time elapsed: 0.087 s % 31.15/5.03 % (194603)Peak memory usage: 118 MB % 31.15/5.03 % (194603)Instructions burned: 131 (million) % 31.15/5.03 % (194606)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3185409105:i=491:doe=on:rtra=on:gtg=position_2970 on theBenchmark for (2970ds/491Mi) % 31.15/5.03 % (194602)Instruction limit reached! % 31.15/5.03 % (194602)------------------------------ % 31.15/5.03 % (194602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.15/5.03 % (194602)CaDiCaL version: 2.1.3 % 31.15/5.03 % (194602)Termination reason: Instruction limit % 31.15/5.03 % (194602)Termination phase: Property scanning % 31.15/5.03 % (194602)Time elapsed: 0.226 s % 31.15/5.03 % (194602)Peak memory usage: 118 MB % 31.15/5.03 % (194602)Instructions burned: 1094 (million) % 31.15/5.03 % (194609)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1608465542:s2a=on:i=835:s2at=2:rtra=on_2969 on theBenchmark for (2969ds/835Mi) % 31.15/5.03 % (194611)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2345545155:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2968 on theBenchmark for (2968ds/307Mi) % 31.15/5.03 % (194605)Instruction limit reached! % 31.15/5.03 % (194605)------------------------------ % 31.15/5.03 % (194605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.15/5.03 % (194605)CaDiCaL version: 2.1.3 % 31.15/5.03 % (194605)Termination reason: Instruction limit % 31.15/5.03 % (194605)Termination phase: Saturation % 31.15/5.03 % (194605)Time elapsed: 0.216 s % 31.15/5.03 % (194605)Peak memory usage: 117 MB % 31.15/5.03 % (194605)Instructions burned: 313 (million) % 31.15/5.03 % (194593)Instruction limit reached! % 31.15/5.03 % (194593)------------------------------ % 31.15/5.03 % (194593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.15/5.03 % (194593)CaDiCaL version: 2.1.3 % 31.15/5.03 % (194593)Termination reason: Instruction limit % 31.15/5.03 % (194593)Termination phase: Saturation % 31.15/5.03 % (194593)Time elapsed: 0.635 s % 31.15/5.03 % (194593)Peak memory usage: 95 MB % 31.15/5.03 % (194593)Instructions burned: 1054 (million) % 31.15/5.03 % (194590)Instruction limit reached! % 31.15/5.03 % (194590)------------------------------ % 31.15/5.03 % (194590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.15/5.03 % (194590)CaDiCaL version: 2.1.3 % 31.15/5.03 % (194590)Termination reason: Instruction limit % 31.15/5.03 % (194590)Termination phase: Saturation % 31.15/5.03 % (194590)Time elapsed: 0.664 s % 31.15/5.03 % (194590)Peak memory usage: 94 MB % 31.15/5.03 % (194590)Instructions burned: 1053 (million) % 31.15/5.03 % (194606)Instruction limit reached! % 31.15/5.03 % (194606)------------------------------ % 31.15/5.03 % (194606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.15/5.03 % (194606)CaDiCaL version: 2.1.3 % 31.15/5.03 % (194606)Termination reason: Instruction limit % 31.15/5.03 % (194606)Termination phase: Saturation % 31.15/5.03 % (194606)Time elapsed: 0.294 s % 31.15/5.03 % (194606)Peak memory usage: 92 MB % 31.15/5.03 % (194606)Instructions burned: 491 (million) % 31.15/5.03 % (194611)Instruction limit reached! % 31.15/5.03 % (194611)------------------------------ % 31.15/5.03 % (194611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.15/5.03 % (194611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.96 % (194611)CaDiCaL version: 2.1.3 % 34.95/5.96 % (194611)Termination reason: Instruction limit % 34.95/5.96 % (194611)Termination phase: Saturation % 34.95/5.96 % (194611)Time elapsed: 0.149 s % 34.95/5.96 % (194611)Peak memory usage: 92 MB % 34.95/5.96 % (194611)Instructions burned: 308 (million) % 34.95/5.96 % (194615)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=454230562:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2967 on theBenchmark for (2967ds/646Mi) % 34.95/5.96 % (194614)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1639094697:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 34.95/5.96 % (194616)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=897212889:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2967 on theBenchmark for (2967ds/784Mi) % 34.95/5.96 % (194618)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=1128868348:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2966 on theBenchmark for (2966ds/246Mi) % 34.95/5.96 % (194617)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=552502353: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.95/5.96 % (194618)Instruction limit reached! % 34.95/5.96 % (194618)------------------------------ % 34.95/5.96 % (194618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.96 % (194618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.96 % (194618)CaDiCaL version: 2.1.3 % 34.95/5.96 % (194618)Termination reason: Instruction limit % 34.95/5.96 % (194618)Termination phase: Saturation % 34.95/5.96 % (194618)Time elapsed: 0.100 s % 34.95/5.96 % (194618)Peak memory usage: 117 MB % 34.95/5.96 % (194618)Instructions burned: 248 (million) % 34.95/5.96 % (194609)Instruction limit reached! % 34.95/5.96 % (194609)------------------------------ % 34.95/5.96 % (194609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.96 % (194609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.96 % (194609)CaDiCaL version: 2.1.3 % 34.95/5.96 % (194609)Termination reason: Instruction limit % 34.95/5.96 % (194609)Termination phase: Saturation % 34.95/5.96 % (194609)Time elapsed: 0.433 s % 34.95/5.96 % (194609)Peak memory usage: 94 MB % 34.95/5.96 % (194609)Instructions burned: 836 (million) % 34.95/5.96 % (194624)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4215691784:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/775Mi) % 34.95/5.96 % (194625)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3043373934:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2963 on theBenchmark for (2963ds/273Mi) % 34.95/5.96 % (194615)Instruction limit reached! % 34.95/5.96 % (194615)------------------------------ % 34.95/5.96 % (194615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.96 % (194615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.96 % (194615)CaDiCaL version: 2.1.3 % 34.95/5.96 % (194615)Termination reason: Instruction limit % 34.95/5.96 % (194615)Termination phase: Saturation % 34.95/5.96 % (194615)Time elapsed: 0.391 s % 34.95/5.96 % (194615)Peak memory usage: 139 MB % 34.95/5.96 % (194615)Instructions burned: 647 (million) % 34.95/5.96 % (194614)Instruction limit reached! % 34.95/5.96 % (194614)------------------------------ % 34.95/5.96 % (194614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.96 % (194614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.96 % (194614)CaDiCaL version: 2.1.3 % 34.95/5.96 % (194614)Termination reason: Instruction limit % 34.95/5.96 % (194614)Termination phase: Saturation % 34.95/5.96 % (194614)Time elapsed: 0.503 s % 34.95/5.96 % (194614)Peak memory usage: 122 MB % 34.95/5.96 % (194614)Instructions burned: 777 (million) % 34.95/5.96 % (194628)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=9425042:i=102:nm=16:rtra=on_2962 on theBenchmark for (2962ds/102Mi) % 34.95/5.96 % (194625)Instruction limit reached! % 34.95/5.96 % (194625)------------------------------ % 34.95/5.96 % (194625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.14/7.59 % (194625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.14/7.59 % (194625)CaDiCaL version: 2.1.3 % 48.14/7.59 % (194625)Termination reason: Instruction limit % 48.14/7.59 % (194625)Termination phase: Saturation % 48.14/7.59 % (194625)Time elapsed: 0.197 s % 48.14/7.59 % (194625)Peak memory usage: 91 MB % 48.14/7.59 % (194625)Instructions burned: 274 (million) % 48.14/7.59 % (194624)Instruction limit reached! % 48.14/7.59 % (194624)------------------------------ % 48.14/7.59 % (194624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.14/7.59 % (194624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.14/7.59 % (194624)CaDiCaL version: 2.1.3 % 48.14/7.59 % (194624)Termination reason: Instruction limit % 48.14/7.59 % (194624)Termination phase: Saturation % 48.14/7.59 % (194624)Time elapsed: 0.288 s % 48.14/7.59 % (194624)Peak memory usage: 96 MB % 48.14/7.59 % (194624)Instructions burned: 777 (million) % 48.14/7.59 % (194616)Instruction limit reached! % 48.14/7.59 % (194616)------------------------------ % 48.14/7.59 % (194616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.14/7.59 % (194616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.14/7.59 % (194616)CaDiCaL version: 2.1.3 % 48.14/7.59 % (194616)Termination reason: Instruction limit % 48.14/7.59 % (194616)Termination phase: Saturation % 48.14/7.59 % (194616)Time elapsed: 0.570 s % 48.14/7.59 % (194616)Peak memory usage: 122 MB % 48.14/7.59 % (194616)Instructions burned: 784 (million) % 48.14/7.59 % (194628)Instruction limit reached! % 48.14/7.59 % (194628)------------------------------ % 48.14/7.59 % (194628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.14/7.59 % (194628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.14/7.59 % (194628)CaDiCaL version: 2.1.3 % 48.14/7.59 % (194628)Termination reason: Instruction limit % 48.14/7.59 % (194628)Termination phase: Saturation % 48.14/7.59 % (194628)Time elapsed: 0.060 s % 48.14/7.59 % (194628)Peak memory usage: 89 MB % 48.14/7.59 % (194628)Instructions burned: 104 (million) % 48.14/7.59 % (194629)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=4210469830:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2960 on theBenchmark for (2960ds/1094Mi) % 48.14/7.59 % (194632)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=920293773:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi) % 48.14/7.59 % (194631)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3964790449:i=6400:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/6400Mi) % 48.14/7.59 % (194633)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=1646422214:i=1846:canc=cautious:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/1846Mi) % 48.14/7.59 % (194634)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4072983068:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2960 on theBenchmark for (2960ds/36816Mi) % 48.14/7.59 % (194617)Instruction limit reached! % 48.14/7.59 % (194617)------------------------------ % 48.14/7.59 % (194617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.14/7.59 % (194617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.14/7.59 % (194617)CaDiCaL version: 2.1.3 % 48.14/7.59 % (194617)Termination reason: Instruction limit % 48.14/7.59 % (194617)Termination phase: Saturation % 48.14/7.59 % (194617)Time elapsed: 0.732 s % 48.14/7.59 % (194617)Peak memory usage: 122 MB % 48.14/7.59 % (194617)Instructions burned: 1132 (million) % 48.14/7.59 % (194632)Instruction limit reached! % 48.14/7.59 % (194632)------------------------------ % 48.14/7.59 % (194632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.14/7.59 % (194632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.14/7.59 % (194632)CaDiCaL version: 2.1.3 % 48.14/7.59 % (194632)Termination reason: Instruction limit % 48.14/7.59 % (194632)Termination phase: Property scanning % 48.14/7.59 % (194632)Time elapsed: 0.187 s % 48.14/7.59 % (194632)Peak memory usage: 118 MB % 48.14/7.59 % (194632)Instructions burned: 870 (million) % 48.14/7.59 % (194641)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=2916553475:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/863Mi) % 59.54/9.04 % (194640)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2685995241:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 59.54/9.04 % (194641)Instruction limit reached! % 59.54/9.04 % (194641)------------------------------ % 59.54/9.04 % (194641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.54/9.04 % (194641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.54/9.04 % (194641)CaDiCaL version: 2.1.3 % 59.54/9.04 % (194641)Termination reason: Instruction limit % 59.54/9.04 % (194641)Termination phase: Property scanning % 59.54/9.04 % (194641)Time elapsed: 0.182 s % 59.54/9.04 % (194641)Peak memory usage: 118 MB % 59.54/9.04 % (194641)Instructions burned: 868 (million) % 59.54/9.04 % (194640)Instruction limit reached! % 59.54/9.04 % (194640)------------------------------ % 59.54/9.04 % (194640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.54/9.04 % (194640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.54/9.04 % (194640)CaDiCaL version: 2.1.3 % 59.54/9.04 % (194640)Termination reason: Instruction limit % 59.54/9.04 % (194640)Termination phase: Saturation % 59.54/9.04 % (194640)Time elapsed: 0.190 s % 59.54/9.04 % (194640)Peak memory usage: 91 MB % 59.54/9.04 % (194640)Instructions burned: 273 (million) % 59.54/9.04 % (194644)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1568398365:i=5811:kws=precedence:nm=0:rtra=on_2954 on theBenchmark for (2954ds/5811Mi) % 59.54/9.04 % (194629)Instruction limit reached! % 59.54/9.04 % (194629)------------------------------ % 59.54/9.04 % (194629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.54/9.04 % (194629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.54/9.04 % (194629)CaDiCaL version: 2.1.3 % 59.54/9.04 % (194629)Termination reason: Instruction limit % 59.54/9.04 % (194629)Termination phase: Saturation % 59.54/9.04 % (194629)Time elapsed: 0.603 s % 59.54/9.04 % (194629)Peak memory usage: 93 MB % 59.54/9.04 % (194629)Instructions burned: 1094 (million) % 59.54/9.04 % (194645)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=636079705:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2954 on theBenchmark for (2954ds/2216Mi) % 59.54/9.04 % (194647)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2296402315:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/801Mi) % 59.54/9.04 % (194633)Instruction limit reached! % 59.54/9.04 % (194633)------------------------------ % 59.54/9.04 % (194633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.54/9.04 % (194633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.54/9.04 % (194633)CaDiCaL version: 2.1.3 % 59.54/9.04 % (194633)Termination reason: Instruction limit % 59.54/9.04 % (194633)Termination phase: Saturation % 59.54/9.04 % (194633)Time elapsed: 0.743 s % 59.54/9.04 % (194633)Peak memory usage: 92 MB % 59.54/9.04 % (194633)Instructions burned: 1848 (million) % 59.54/9.04 % (194650)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=615422922:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2951 on theBenchmark for (2951ds/1026Mi) % 59.54/9.05 % (194587)Instruction limit reached! % 59.54/9.05 % (194587)------------------------------ % 59.54/9.05 % (194587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.54/9.05 % (194587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.54/9.05 % (194587)CaDiCaL version: 2.1.3 % 59.54/9.05 % (194587)Termination reason: Instruction limit % 59.54/9.05 % (194587)Termination phase: Saturation % 59.54/9.05 % (194587)Time elapsed: 2.530 s % 59.54/9.05 % (194587)Peak memory usage: 112 MB % 59.54/9.05 % (194587)Instructions burned: 4428 (million) % 59.54/9.05 % (194652)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3215652431:i=3509:rtra=on_2949 on theBenchmark for (2949ds/3509Mi) % 59.54/9.05 % (194647)Instruction limit reached! % 59.54/9.05 % (194647)------------------------------ % 59.54/9.05 % (194647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.54/9.05 % (194647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.54/9.05 % (194647)CaDiCaL version: 2.1.3 % 59.54/9.05 % (194647)Termination reason: Instruction limit % 91.28/13.57 % (194647)Termination phase: Saturation % 91.28/13.57 % (194647)Time elapsed: 0.497 s % 91.28/13.57 % (194647)Peak memory usage: 95 MB % 91.28/13.57 % (194647)Instructions burned: 802 (million) % 91.28/13.57 % (194654)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1988559708:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2947 on theBenchmark for (2947ds/2127Mi) % 91.28/13.57 % (194650)Instruction limit reached! % 91.28/13.57 % (194650)------------------------------ % 91.28/13.57 % (194650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.28/13.57 % (194650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.28/13.57 % (194650)CaDiCaL version: 2.1.3 % 91.28/13.57 % (194650)Termination reason: Instruction limit % 91.28/13.57 % (194650)Termination phase: Saturation % 91.28/13.57 % (194650)Time elapsed: 0.608 s % 91.28/13.57 % (194650)Peak memory usage: 96 MB % 91.28/13.57 % (194650)Instructions burned: 1028 (million) % 91.28/13.57 % (194644)Instruction limit reached! % 91.28/13.57 % (194644)------------------------------ % 91.28/13.57 % (194644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.28/13.57 % (194644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.28/13.57 % (194644)CaDiCaL version: 2.1.3 % 91.28/13.57 % (194644)Termination reason: Instruction limit % 91.28/13.57 % (194644)Termination phase: Property scanning % 91.28/13.57 % (194644)Time elapsed: 1.077 s % 91.28/13.57 % (194644)Peak memory usage: 118 MB % 91.28/13.57 % (194644)Instructions burned: 5816 (million) % 91.28/13.57 % (194656)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2535822326:i=1959:rtra=on:fsd=on:proc=on_2943 on theBenchmark for (2943ds/1959Mi) % 91.28/13.57 % (194657)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4044421101:s2a=on:i=3553:nm=0:rtra=on_2942 on theBenchmark for (2942ds/3553Mi) % 91.28/13.57 % (194645)Instruction limit reached! % 91.28/13.57 % (194645)------------------------------ % 91.28/13.57 % (194645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.28/13.57 % (194645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.28/13.57 % (194645)CaDiCaL version: 2.1.3 % 91.28/13.57 % (194645)Termination reason: Instruction limit % 91.28/13.57 % (194645)Termination phase: Saturation % 91.28/13.57 % (194645)Time elapsed: 1.246 s % 91.28/13.57 % (194645)Peak memory usage: 129 MB % 91.28/13.57 % (194645)Instructions burned: 2217 (million) % 91.28/13.57 % (194660)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1969340349:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2940 on theBenchmark for (2940ds/3201Mi) % 91.28/13.57 % (194654)Instruction limit reached! % 91.28/13.57 % (194654)------------------------------ % 91.28/13.57 % (194654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.28/13.57 % (194654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.28/13.57 % (194654)CaDiCaL version: 2.1.3 % 91.28/13.57 % (194654)Termination reason: Instruction limit % 91.28/13.57 % (194654)Termination phase: Saturation % 91.28/13.57 % (194654)Time elapsed: 1.020 s % 91.28/13.57 % (194654)Peak memory usage: 103 MB % 91.28/13.57 % (194654)Instructions burned: 2129 (million) % 91.28/13.57 % (194662)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=921705909:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2935 on theBenchmark for (2935ds/4093Mi) % 91.28/13.57 % (194657)Instruction limit reached! % 91.28/13.57 % (194657)------------------------------ % 91.28/13.57 % (194657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.28/13.57 % (194657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.28/13.57 % (194657)CaDiCaL version: 2.1.3 % 91.28/13.57 % (194657)Termination reason: Instruction limit % 91.28/13.57 % (194657)Termination phase: NewCNF % 91.28/13.57 % (194657)Time elapsed: 0.835 s % 91.28/13.57 % (194657)Peak memory usage: 190 MB % 91.28/13.57 % (194657)Instructions burned: 3554 (million) % 91.28/13.57 % (194664)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=2534700261:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2933 on theBenchmark for (2933ds/21173Mi) % 91.28/13.57 % (194656)Instruction limit reached! % 91.28/13.57 % (194656)------------------------------ % 91.28/13.57 % (194656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.45/16.99 % (194656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.45/16.99 % (194656)CaDiCaL version: 2.1.3 % 115.45/16.99 % (194656)Termination reason: Instruction limit % 115.45/16.99 % (194656)Termination phase: Saturation % 115.45/16.99 % (194656)Time elapsed: 1.177 s % 115.45/16.99 % (194656)Peak memory usage: 125 MB % 115.45/16.99 % (194656)Instructions burned: 1960 (million) % 115.45/16.99 % (194666)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=157844229:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2930 on theBenchmark for (2930ds/10544Mi) % 115.45/16.99 % (194652)Instruction limit reached! % 115.45/16.99 % (194652)------------------------------ % 115.45/16.99 % (194652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.45/16.99 % (194652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.45/16.99 % (194652)CaDiCaL version: 2.1.3 % 115.45/16.99 % (194652)Termination reason: Instruction limit % 115.45/16.99 % (194652)Termination phase: Saturation % 115.45/16.99 % (194652)Time elapsed: 2.393 s % 115.45/16.99 % (194652)Peak memory usage: 107 MB % 115.45/16.99 % (194652)Instructions burned: 3509 (million) % 115.45/16.99 % (194660)Instruction limit reached! % 115.45/16.99 % (194660)------------------------------ % 115.45/16.99 % (194660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.45/16.99 % (194660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.45/16.99 % (194660)CaDiCaL version: 2.1.3 % 115.45/16.99 % (194660)Termination reason: Instruction limit % 115.45/16.99 % (194660)Termination phase: Saturation % 115.45/16.99 % (194660)Time elapsed: 1.505 s % 115.45/16.99 % (194660)Peak memory usage: 98 MB % 115.45/16.99 % (194660)Instructions burned: 3203 (million) % 115.45/16.99 % (194631)Instruction limit reached! % 115.45/16.99 % (194631)------------------------------ % 115.45/16.99 % (194631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.45/16.99 % (194631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.45/16.99 % (194631)CaDiCaL version: 2.1.3 % 115.45/16.99 % (194631)Termination reason: Instruction limit % 115.45/16.99 % (194631)Termination phase: Saturation % 115.45/16.99 % (194631)Time elapsed: 3.589 s % 115.45/16.99 % (194631)Peak memory usage: 119 MB % 115.45/16.99 % (194631)Instructions burned: 6401 (million) % 115.45/16.99 % (194669)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1791503970:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2924 on theBenchmark for (2924ds/775Mi) % 115.45/16.99 % (194668)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3388854169:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2924 on theBenchmark for (2924ds/1262Mi) % 115.45/16.99 % (194670)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3623059461:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/270Mi) % 115.45/16.99 % (194670)Instruction limit reached! % 115.45/16.99 % (194670)------------------------------ % 115.45/16.99 % (194670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.45/16.99 % (194670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.45/16.99 % (194670)CaDiCaL version: 2.1.3 % 115.45/16.99 % (194670)Termination reason: Instruction limit % 115.45/16.99 % (194670)Termination phase: Saturation % 115.45/16.99 % (194670)Time elapsed: 0.186 s % 115.45/16.99 % (194670)Peak memory usage: 92 MB % 115.45/16.99 % (194670)Instructions burned: 270 (million) % 115.45/16.99 % (194674)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2422915316:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2919 on theBenchmark for (2919ds/17165Mi) % 115.45/16.99 % (194669)Instruction limit reached! % 115.45/16.99 % (194669)------------------------------ % 115.45/16.99 % (194669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.45/16.99 % (194669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.45/16.99 % (194669)CaDiCaL version: 2.1.3 % 115.45/16.99 % (194669)Termination reason: Instruction limit % 115.45/16.99 % (194669)Termination phase: Saturation % 115.45/16.99 % (194669)Time elapsed: 0.525 s % 115.45/16.99 % (194669)Peak memory usage: 96 MB % 115.45/16.99 % (194669)Instructions burned: 776 (million) % 115.45/16.99 % (194676)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2546152778:s2a=on:i=13094:s2at=-1:rtra=on_2917 on theBenchmark for (2917ds/13094Mi) % 127.41/18.63 % (194668)Instruction limit reached! % 127.41/18.63 % (194668)------------------------------ % 127.41/18.63 % (194668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.41/18.63 % (194668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.41/18.63 % (194668)CaDiCaL version: 2.1.3 % 127.41/18.63 % (194668)Termination reason: Instruction limit % 127.41/18.63 % (194668)Termination phase: Saturation % 127.41/18.63 % (194668)Time elapsed: 0.664 s % 127.41/18.63 % (194668)Peak memory usage: 119 MB % 127.41/18.63 % (194668)Instructions burned: 1264 (million) % 127.41/18.63 % (194678)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1860656555:st=2:i=12633:rtra=on:ss=axioms_2916 on theBenchmark for (2916ds/12633Mi) % 127.41/18.63 % (194662)Instruction limit reached! % 127.41/18.63 % (194662)------------------------------ % 127.41/18.63 % (194662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.41/18.63 % (194662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.41/18.63 % (194662)CaDiCaL version: 2.1.3 % 127.41/18.63 % (194662)Termination reason: Instruction limit % 127.41/18.63 % (194662)Termination phase: Saturation % 127.41/18.63 % (194662)Time elapsed: 2.470 s % 127.41/18.63 % (194662)Peak memory usage: 147 MB % 127.41/18.63 % (194662)Instructions burned: 4095 (million) % 127.41/18.63 % (194680)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2466775831:i=1783:rtra=on:gtg=position_2909 on theBenchmark for (2909ds/1783Mi) % 127.41/18.63 % (194680)Instruction limit reached! % 127.41/18.63 % (194680)------------------------------ % 127.41/18.63 % (194680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.41/18.63 % (194680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.41/18.63 % (194680)CaDiCaL version: 2.1.3 % 127.41/18.63 % (194680)Termination reason: Instruction limit % 127.41/18.63 % (194680)Termination phase: Saturation % 127.41/18.63 % (194680)Time elapsed: 1.115 s % 127.41/18.63 % (194680)Peak memory usage: 126 MB % 127.41/18.63 % (194680)Instructions burned: 1784 (million) % 127.41/18.63 % (194682)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=1289212691:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2897 on theBenchmark for (2897ds/5451Mi) % 127.41/18.63 % (194664)Instruction limit reached! % 127.41/18.63 % (194664)------------------------------ % 127.41/18.63 % (194664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.41/18.63 % (194664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.41/18.63 % (194664)CaDiCaL version: 2.1.3 % 127.41/18.63 % (194664)Termination reason: Instruction limit % 127.41/18.63 % (194664)Termination phase: Saturation % 127.41/18.63 % (194664)Time elapsed: 5.131 s % 127.41/18.63 % (194664)Peak memory usage: 132 MB % 127.41/18.63 % (194664)Instructions burned: 21174 (million) % 127.41/18.63 % (194684)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=2463977563:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2881 on theBenchmark for (2881ds/4975Mi) % 127.41/18.63 % (194682)Instruction limit reached! % 127.41/18.63 % (194682)------------------------------ % 127.41/18.63 % (194682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.41/18.63 % (194682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.41/18.63 % (194682)CaDiCaL version: 2.1.3 % 127.41/18.63 % (194682)Termination reason: Instruction limit % 127.41/18.63 % (194682)Termination phase: Property scanning % 127.41/18.63 % (194682)Time elapsed: 1.907 s % 127.41/18.63 % (194682)Peak memory usage: 118 MB % 127.41/18.63 % (194682)Instructions burned: 5452 (million) % 127.41/18.63 % (194686)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=229392402:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2876 on theBenchmark for (2876ds/2076Mi) % 127.41/18.63 % (194684)Instruction limit reached! % 127.41/18.63 % (194684)------------------------------ % 127.41/18.63 % (194684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 127.41/18.63 % (194684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.41/18.63 % (194684)CaDiCaL version: 2.1.3 % 127.41/18.63 % (194684)Termination reason: Instruction limit % 127.41/18.63 % (194684)Termination phase: Property scanning % 127.41/18.63 % (194684)Time elapsed: 0.924 s % 127.41/18.63 % (194684)Peak memory usage: 118 MB % 127.41/18.63 % (194684)Instructions burned: 4976 (million) % 189.97/27.50 % (194718)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1023864242:i=5145:rtra=on_2871 on theBenchmark for (2871ds/5145Mi) % 189.97/27.50 % (194686)Instruction limit reached! % 189.97/27.50 % (194686)------------------------------ % 189.97/27.50 % (194686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.97/27.50 % (194686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.97/27.50 % (194686)CaDiCaL version: 2.1.3 % 189.97/27.50 % (194686)Termination reason: Instruction limit % 189.97/27.50 % (194686)Termination phase: Saturation % 189.97/27.50 % (194686)Time elapsed: 1.192 s % 189.97/27.50 % (194686)Peak memory usage: 128 MB % 189.97/27.50 % (194686)Instructions burned: 2076 (million) % 189.97/27.50 % (194842)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2957175048:i=3509:rtra=on_2863 on theBenchmark for (2863ds/3509Mi) % 189.97/27.50 % (194666)Instruction limit reached! % 189.97/27.50 % (194666)------------------------------ % 189.97/27.50 % (194666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.97/27.50 % (194666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.97/27.50 % (194666)CaDiCaL version: 2.1.3 % 189.97/27.50 % (194666)Termination reason: Instruction limit % 189.97/27.50 % (194666)Termination phase: Saturation % 189.97/27.50 % (194666)Time elapsed: 6.849 s % 189.97/27.50 % (194666)Peak memory usage: 193 MB % 189.97/27.50 % (194666)Instructions burned: 10544 (million) % 189.97/27.50 % (194921)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=570793933:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2860 on theBenchmark for (2860ds/13800Mi) % 189.97/27.50 % (194676)Instruction limit reached! % 189.97/27.50 % (194676)------------------------------ % 189.97/27.50 % (194676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.97/27.50 % (194676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.97/27.50 % (194676)CaDiCaL version: 2.1.3 % 189.97/27.50 % (194676)Termination reason: Instruction limit % 189.97/27.50 % (194676)Termination phase: Saturation % 189.97/27.50 % (194676)Time elapsed: 5.787 s % 189.97/27.50 % (194676)Peak memory usage: 94 MB % 189.97/27.50 % (194676)Instructions burned: 13094 (million) % 189.97/27.50 % (194957)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2798215822:i=1412:rtra=on:fsd=on:proc=on_2858 on theBenchmark for (2858ds/1412Mi) % 189.97/27.50 % (194718)Instruction limit reached! % 189.97/27.50 % (194718)------------------------------ % 189.97/27.50 % (194718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.97/27.50 % (194718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.97/27.50 % (194718)CaDiCaL version: 2.1.3 % 189.97/27.50 % (194718)Termination reason: Instruction limit % 189.97/27.50 % (194718)Termination phase: Saturation % 189.97/27.50 % (194718)Time elapsed: 1.668 s % 189.97/27.50 % (194718)Peak memory usage: 102 MB % 189.97/27.50 % (194718)Instructions burned: 5147 (million) % 189.97/27.50 % (194959)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 % 189.97/27.50 % (194959)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1275052096:i=11747:aac=none:nm=0:rtra=on:rawr=on_2853 on theBenchmark for (2853ds/11747Mi) % 189.97/27.50 % (194957)Instruction limit reached! % 189.97/27.50 % (194957)------------------------------ % 189.97/27.50 % (194957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.97/27.50 % (194957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.97/27.50 % (194957)CaDiCaL version: 2.1.3 % 189.97/27.50 % (194957)Termination reason: Instruction limit % 189.97/27.50 % (194957)Termination phase: Saturation % 189.97/27.50 % (194957)Time elapsed: 0.707 s % 189.97/27.50 % (194957)Peak memory usage: 118 MB % 189.97/27.50 % (194957)Instructions burned: 1413 (million) % 189.97/27.50 % (194971)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=965439179:s2a=on:i=3553:nm=0:rtra=on_2849 on theBenchmark for (2849ds/3553Mi) % 189.97/27.50 % (194842)Instruction limit reached! % 189.97/27.50 % (194842)------------------------------ % 189.97/27.50 % (194842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.97/27.50 % (194842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.97/27.50 % (194842)CaDiCaL version: 2.1.3 % 234.22/33.75 % (194842)Termination reason: Instruction limit % 234.22/33.75 % (194842)Termination phase: Saturation % 234.22/33.75 % (194842)Time elapsed: 2.540 s % 234.22/33.75 % (194842)Peak memory usage: 110 MB % 234.22/33.75 % (194842)Instructions burned: 3509 (million) % 234.22/33.75 % (195137)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1461677892:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/3201Mi) % 234.22/33.75 % (194674)Instruction limit reached! % 234.22/33.75 % (194674)------------------------------ % 234.22/33.75 % (194674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.22/33.75 % (194674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.22/33.75 % (194674)CaDiCaL version: 2.1.3 % 234.22/33.75 % (194674)Termination reason: Instruction limit % 234.22/33.75 % (194674)Termination phase: Saturation % 234.22/33.75 % (194674)Time elapsed: 8.445 s % 234.22/33.75 % (194674)Peak memory usage: 328 MB % 234.22/33.75 % (194674)Instructions burned: 17166 (million) % 234.22/33.75 % (195140)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=564309735:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2833 on theBenchmark for (2833ds/4081Mi) % 234.22/33.75 % (194971)Instruction limit reached! % 234.22/33.75 % (194971)------------------------------ % 234.22/33.75 % (194971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.22/33.75 % (194971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.22/33.75 % (194971)CaDiCaL version: 2.1.3 % 234.22/33.75 % (194971)Termination reason: Instruction limit % 234.22/33.75 % (194971)Termination phase: NewCNF % 234.22/33.75 % (194971)Time elapsed: 1.611 s % 234.22/33.75 % (194971)Peak memory usage: 190 MB % 234.22/33.75 % (194971)Instructions burned: 3554 (million) % 234.22/33.75 % (195142)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=288684682:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2831 on theBenchmark for (2831ds/20260Mi) % 234.22/33.75 % (194959)Instruction limit reached! % 234.22/33.75 % (194959)------------------------------ % 234.22/33.75 % (194959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.22/33.75 % (194959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.22/33.75 % (194959)CaDiCaL version: 2.1.3 % 234.22/33.75 % (194959)Termination reason: Instruction limit % 234.22/33.75 % (194959)Termination phase: Property scanning % 234.22/33.75 % (194959)Time elapsed: 2.392 s % 234.22/33.75 % (194959)Peak memory usage: 118 MB % 234.22/33.75 % (194959)Instructions burned: 11752 (million) % 234.22/33.75 % (195144)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=546763582:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2828 on theBenchmark for (2828ds/58627Mi) % 234.22/33.75 % (194678)Instruction limit reached! % 234.22/33.75 % (194678)------------------------------ % 234.22/33.75 % (194678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.22/33.75 % (194678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.22/33.75 % (194678)CaDiCaL version: 2.1.3 % 234.22/33.75 % (194678)Termination reason: Instruction limit % 234.22/33.75 % (194678)Termination phase: Saturation % 234.22/33.75 % (194678)Time elapsed: 8.752 s % 234.22/33.75 % (194678)Peak memory usage: 118 MB % 234.22/33.75 % (194678)Instructions burned: 12633 (million) % 234.22/33.75 % (195146)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=362003897:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/6258Mi) % 234.22/33.75 % (195137)Instruction limit reached! % 234.22/33.75 % (195137)------------------------------ % 234.22/33.75 % (195137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.22/33.75 % (195137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.22/33.75 % (195137)CaDiCaL version: 2.1.3 % 234.22/33.75 % (195137)Termination reason: Instruction limit % 234.22/33.75 % (195137)Termination phase: Saturation % 234.22/33.75 % (195137)Time elapsed: 1.366 s % 234.22/33.75 % (195137)Peak memory usage: 95 MB % 234.22/33.75 % (195137)Instructions burned: 3202 (million) % 234.22/33.75 % (195148)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=90860714:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2821 on theBenchmark for (2821ds/34001Mi) % 254.14/36.58 % (195140)Instruction limit reached! % 254.14/36.58 % (195140)------------------------------ % 254.14/36.58 % (195140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.14/36.58 % (195140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.14/36.58 % (195140)CaDiCaL version: 2.1.3 % 254.14/36.58 % (195140)Termination reason: Instruction limit % 254.14/36.58 % (195140)Termination phase: Saturation % 254.14/36.58 % (195140)Time elapsed: 2.356 s % 254.14/36.58 % (195140)Peak memory usage: 142 MB % 254.14/36.58 % (195140)Instructions burned: 4081 (million) % 254.14/36.58 % (195150)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3645652914:s2a=on:i=71622:s2at=-1:rtra=on_2808 on theBenchmark for (2808ds/71622Mi) % 254.14/36.58 % (195146)Instruction limit reached! % 254.14/36.58 % (195146)------------------------------ % 254.14/36.58 % (195146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.14/36.58 % (195146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.14/36.58 % (195146)CaDiCaL version: 2.1.3 % 254.14/36.58 % (195146)Termination reason: Instruction limit % 254.14/36.58 % (195146)Termination phase: Saturation % 254.14/36.58 % (195146)Time elapsed: 2.964 s % 254.14/36.58 % (195146)Peak memory usage: 124 MB % 254.14/36.58 % (195146)Instructions burned: 6259 (million) % 254.14/36.58 % (195152)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2193406472:i=24001:kws=precedence:nm=0:rtra=on_2796 on theBenchmark for (2796ds/24001Mi) % 254.14/36.58 % (194921)Instruction limit reached! % 254.14/36.58 % (194921)------------------------------ % 254.14/36.58 % (194921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.14/36.58 % (194921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.14/36.58 % (194921)CaDiCaL version: 2.1.3 % 254.14/36.58 % (194921)Termination reason: Instruction limit % 254.14/36.58 % (194921)Termination phase: Saturation % 254.14/36.58 % (194921)Time elapsed: 6.834 s % 254.14/36.58 % (194921)Peak memory usage: 157 MB % 254.14/36.58 % (194921)Instructions burned: 13802 (million) % 254.14/36.58 % (195154)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=1799078170:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2791 on theBenchmark for (2791ds/2076Mi) % 254.14/36.58 % (195154)Instruction limit reached! % 254.14/36.58 % (195154)------------------------------ % 254.14/36.58 % (195154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.14/36.58 % (195154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.14/36.58 % (195154)CaDiCaL version: 2.1.3 % 254.14/36.58 % (195154)Termination reason: Instruction limit % 254.14/36.58 % (195154)Termination phase: Saturation % 254.14/36.58 % (195154)Time elapsed: 1.188 s % 254.14/36.58 % (195154)Peak memory usage: 128 MB % 254.14/36.58 % (195154)Instructions burned: 2077 (million) % 254.14/36.58 % (195156)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=898513178:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2777 on theBenchmark for (2777ds/83971Mi) % 254.14/36.58 % (194634)Instruction limit reached! % 254.14/36.58 % (194634)------------------------------ % 254.14/36.58 % (194634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.14/36.58 % (194634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.14/36.58 % (194634)CaDiCaL version: 2.1.3 % 254.14/36.58 % (194634)Termination reason: Instruction limit % 254.14/36.58 % (194634)Termination phase: Saturation % 254.14/36.58 % (194634)Time elapsed: 21.182 s % 254.14/36.58 % (194634)Peak memory usage: 205 MB % 254.14/36.58 % (194634)Instructions burned: 36817 (million) % 254.14/36.58 % (195158)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3892201381:i=83944:rtra=on_2746 on theBenchmark for (2746ds/83944Mi) % 254.14/36.58 % (195142)Instruction limit reached! % 254.14/36.58 % (195142)------------------------------ % 254.14/36.58 % (195142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.14/36.58 % (195142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.14/36.58 % (195142)CaDiCaL version: 2.1.3 % 254.14/36.58 % (195142)Termination reason: Instruction limit % 254.14/36.58 % (195142)Termination phase: Saturation % 254.14/36.58 % (195142)Time elapsed: 9.712 s % 254.14/36.58 % (195142)Peak memory usage: 128 MB % 254.14/36.58 % (195142)Instructions burned: 20262 (million) % 254.14/36.58 % (195160)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4283419198:i=9201:rtra=on_2733 on theBenchmark for (2733ds/9201Mi) % 267.69/38.44 % (195152)Instruction limit reached! % 267.69/38.44 % (195152)------------------------------ % 267.69/38.44 % (195152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.69/38.44 % (195152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.69/38.44 % (195152)CaDiCaL version: 2.1.3 % 267.69/38.44 % (195152)Termination reason: Instruction limit % 267.69/38.44 % (195152)Termination phase: Function definition elimination % 267.69/38.44 % (195152)Time elapsed: 8.152 s % 267.69/38.44 % (195152)Peak memory usage: 118 MB % 267.69/38.44 % (195152)Instructions burned: 24001 (million) % 267.69/38.44 % (195430)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 % 267.69/38.44 % (195430)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1938684553:i=6806:aac=none:nm=0:rtra=on:rawr=on_2713 on theBenchmark for (2713ds/6806Mi) % 267.69/38.44 % (195158)Refutation not found, incomplete strategy % 267.69/38.44 % (195158)------------------------------ % 267.69/38.44 % (195158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.69/38.44 % (195158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.69/38.44 % (195158)CaDiCaL version: 2.1.3 % 267.69/38.44 % (195158)Termination reason: Refutation not found, incomplete strategy % 267.69/38.44 % (195158)Time elapsed: 4.840 s % 267.69/38.44 % (195158)Peak memory usage: 134 MB % 267.69/38.44 % (195158)Instructions burned: 9295 (million) % 267.69/38.44 % (195158)------------------------------ % 267.69/38.44 % (195158)------------------------------ % 267.69/38.44 % (195523)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=72536860:s2a=on:i=3553:nm=0:rtra=on_2694 on theBenchmark for (2694ds/3553Mi) % 267.69/38.44 % (195430)Instruction limit reached! % 267.69/38.44 % (195430)------------------------------ % 267.69/38.44 % (195430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.69/38.44 % (195430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.69/38.44 % (195430)CaDiCaL version: 2.1.3 % 267.69/38.44 % (195430)Termination reason: Instruction limit % 267.69/38.44 % (195430)Termination phase: Property scanning % 267.69/38.44 % (195430)Time elapsed: 2.365 s % 267.69/38.44 % (195430)Peak memory usage: 118 MB % 267.69/38.44 % (195430)Instructions burned: 6807 (million) % 267.69/38.44 % (195525)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=1146884451:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2688 on theBenchmark for (2688ds/2064Mi) % 267.69/38.44 % (195523)Instruction limit reached! % 267.69/38.44 % (195523)------------------------------ % 267.69/38.44 % (195523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.69/38.44 % (195523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.69/38.44 % (195523)CaDiCaL version: 2.1.3 % 267.69/38.44 % (195523)Termination reason: Instruction limit % 267.69/38.44 % (195523)Termination phase: NewCNF % 267.69/38.44 % (195523)Time elapsed: 1.539 s % 267.69/38.44 % (195523)Peak memory usage: 191 MB % 267.69/38.44 % (195523)Instructions burned: 3555 (million) % 267.69/38.44 % (195527)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=2945014152:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2677 on theBenchmark for (2677ds/20260Mi) % 267.69/38.44 % (195525)Instruction limit reached! % 267.69/38.44 % (195525)------------------------------ % 267.69/38.44 % (195525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.69/38.44 % (195525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.69/38.44 % (195525)CaDiCaL version: 2.1.3 % 267.69/38.44 % (195525)Termination reason: Instruction limit % 267.69/38.44 % (195525)Termination phase: Saturation % 267.69/38.44 % (195525)Time elapsed: 1.247 s % 267.69/38.44 % (195525)Peak memory usage: 140 MB % 267.69/38.44 % (195525)Instructions burned: 2065 (million) % 267.69/38.44 % (195529)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1900878671:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2674 on theBenchmark for (2674ds/1244Mi) % 267.69/38.44 % (195160)Instruction limit reached! % 267.69/38.44 % (195160)------------------------------ % 270.76/38.83 % (195160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.76/38.83 % (195160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.76/38.83 % (195160)CaDiCaL version: 2.1.3 % 270.76/38.83 % (195160)Termination reason: Instruction limit % 270.76/38.83 % (195160)Termination phase: Saturation % 270.76/38.83 % (195160)Time elapsed: 6.257 s % 270.76/38.83 % (195160)Peak memory usage: 116 MB % 270.76/38.83 % (195160)Instructions burned: 9202 (million) % 270.76/38.83 % (195531)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=3783126911:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2669 on theBenchmark for (2669ds/58261Mi) % 270.76/38.83 % (195529)Instruction limit reached! % 270.76/38.83 % (195529)------------------------------ % 270.76/38.83 % (195529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.76/38.83 % (195529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.76/38.83 % (195529)CaDiCaL version: 2.1.3 % 270.76/38.83 % (195529)Termination reason: Instruction limit % 270.76/38.83 % (195529)Termination phase: Saturation % 270.76/38.83 % (195529)Time elapsed: 0.643 s % 270.76/38.83 % (195529)Peak memory usage: 119 MB % 270.76/38.83 % (195529)Instructions burned: 1244 (million) % 270.76/38.83 % (195533)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 % 270.76/38.83 % (195533)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=677893458:i=6806:aac=none:nm=0:rtra=on:rawr=on_2667 on theBenchmark for (2667ds/6806Mi) % 270.76/38.83 % (195148)Instruction limit reached! % 270.76/38.83 % (195148)------------------------------ % 270.76/38.83 % (195148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.76/38.83 % (195148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.76/38.83 % (195148)CaDiCaL version: 2.1.3 % 270.76/38.83 % (195148)Termination reason: Instruction limit % 270.76/38.83 % (195148)Termination phase: Saturation % 270.76/38.83 % (195148)Time elapsed: 16.323 s % 270.76/38.83 % (195148)Peak memory usage: 540 MB % 270.76/38.83 % (195148)Instructions burned: 34002 (million) % 270.76/38.83 % (195535)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=1067106102:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2656 on theBenchmark for (2656ds/4081Mi) % 270.76/38.83 % (195144)Instruction limit reached! % 270.76/38.83 % (195144)------------------------------ % 270.76/38.83 % (195144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.76/38.83 % (195144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.76/38.83 % (195144)CaDiCaL version: 2.1.3 % 270.76/38.83 % (195144)Termination reason: Instruction limit % 270.76/38.83 % (195144)Termination phase: Saturation % 270.76/38.83 % (195144)Time elapsed: 18.127 s % 270.76/38.83 % (195144)Peak memory usage: 245 MB % 270.76/38.83 % (195144)Instructions burned: 58627 (million) % 270.76/38.83 % (195537)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3614264511:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2646 on theBenchmark for (2646ds/1701Mi) % 270.76/38.83 % (195533)Instruction limit reached! % 270.76/38.83 % (195533)------------------------------ % 270.76/38.83 % (195533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.76/38.83 % (195533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.76/38.83 % (195533)CaDiCaL version: 2.1.3 % 270.76/38.83 % (195533)Termination reason: Instruction limit % 270.76/38.83 % (195533)Termination phase: Property scanning % 270.76/38.83 % (195533)Time elapsed: 2.364 s % 270.76/38.83 % (195533)Peak memory usage: 118 MB % 270.76/38.83 % (195533)Instructions burned: 6808 (million) % 270.76/38.83 % (195537)Instruction limit reached! % 270.76/38.83 % (195537)------------------------------ % 270.76/38.83 % (195537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.76/38.83 % (195537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.76/38.83 % (195537)CaDiCaL version: 2.1.3 % 270.76/38.83 % (195537)Termination reason: Instruction limit % 270.76/38.83 % (195537)Termination phase: Saturation % 270.76/38.83 % (195537)Time elapsed: 0.445 s % 270.76/38.83 % (195537)Peak memory usage: 119 MB % 270.76/38.83 % (195537)Instructions burned: 1702 (million) % 273.55/39.27 % (195539)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=111955016:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2641 on theBenchmark for (2641ds/57001Mi) % 273.55/39.27 % (195540)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 % 273.55/39.27 % (195540)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4212893641:i=8622:aac=none:nm=0:rtra=on:rawr=on_2640 on theBenchmark for (2640ds/8622Mi) % 273.55/39.27 % (195535)Instruction limit reached! % 273.55/39.27 % (195535)------------------------------ % 273.55/39.27 % (195535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.55/39.27 % (195535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.55/39.27 % (195535)CaDiCaL version: 2.1.3 % 273.55/39.27 % (195535)Termination reason: Instruction limit % 273.55/39.27 % (195535)Termination phase: Saturation % 273.55/39.27 % (195535)Time elapsed: 2.348 s % 273.55/39.27 % (195535)Peak memory usage: 144 MB % 273.55/39.27 % (195535)Instructions burned: 4082 (million) % 273.55/39.27 % (195543)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1030387678:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2631 on theBenchmark for (2631ds/24Mi) % 273.55/39.27 % (195543)Instruction limit reached! % 273.55/39.27 % (195543)------------------------------ % 273.55/39.27 % (195543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.55/39.27 % (195543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.55/39.27 % (195543)CaDiCaL version: 2.1.3 % 273.55/39.27 % (195543)Termination reason: Instruction limit % 273.55/39.27 % (195543)Termination phase: Saturation % 273.55/39.27 % (195543)Time elapsed: 0.033 s % 273.55/39.27 % (195543)Peak memory usage: 113 MB % 273.55/39.27 % (195543)Instructions burned: 24 (million) % 273.55/39.27 % (195545)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3132605806:i=614:kws=precedence:nm=0:rtra=on_2630 on theBenchmark for (2630ds/614Mi) % 273.55/39.27 % (195545)Instruction limit reached! % 273.55/39.27 % (195545)------------------------------ % 273.55/39.27 % (195545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.55/39.27 % (195545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.55/39.27 % (195545)CaDiCaL version: 2.1.3 % 273.55/39.27 % (195545)Termination reason: Instruction limit % 273.55/39.27 % (195545)Termination phase: Property scanning % 273.55/39.27 % (195545)Time elapsed: 0.253 s % 273.55/39.27 % (195545)Peak memory usage: 118 MB % 273.55/39.27 % (195545)Instructions burned: 616 (million) % 273.55/39.27 % (195547)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3338638648:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2626 on theBenchmark for (2626ds/402Mi) % 273.55/39.27 % (195540)Instruction limit reached! % 273.55/39.27 % (195540)------------------------------ % 273.55/39.27 % (195540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.55/39.27 % (195540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.55/39.27 % (195540)CaDiCaL version: 2.1.3 % 273.55/39.27 % (195540)Termination reason: Instruction limit % 273.55/39.27 % (195540)Termination phase: Property scanning % 273.55/39.27 % (195540)Time elapsed: 1.575 s % 273.55/39.27 % (195540)Peak memory usage: 118 MB % 273.55/39.27 % (195540)Instructions burned: 8625 (million) % 273.55/39.27 % (195549)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=47347780:s2a=on:i=14:rtra=on:inst=on_2624 on theBenchmark for (2624ds/14Mi) % 273.55/39.27 % (195549)Instruction limit reached! % 273.55/39.27 % (195549)------------------------------ % 273.55/39.27 % (195549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.55/39.27 % (195549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.55/39.27 % (195549)CaDiCaL version: 2.1.3 % 273.55/39.27 % (195549)Termination reason: Instruction limit % 273.55/39.27 % (195549)Termination phase: Saturation % 273.55/39.27 % (195549)Time elapsed: 0.004 s % 273.55/39.27 % (195549)Peak memory usage: 88 MB % 273.55/39.27 % (195549)Instructions burned: 14 (million) % 273.55/39.27 % (195551)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1721809509:i=8:rtra=on_2623 on theBenchmark for (2623ds/8Mi) % 277.09/39.76 % (195551)Instruction limit reached! % 277.09/39.76 % (195551)------------------------------ % 277.09/39.76 % (195551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.09/39.76 % (195551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.09/39.76 % (195551)CaDiCaL version: 2.1.3 % 277.09/39.76 % (195551)Termination reason: Instruction limit % 277.09/39.76 % (195551)Termination phase: Saturation % 277.09/39.76 % (195551)Time elapsed: 0.003 s % 277.09/39.76 % (195551)Peak memory usage: 87 MB % 277.09/39.76 % (195551)Instructions burned: 12 (million) % 277.09/39.76 % (195547)Instruction limit reached! % 277.09/39.76 % (195547)------------------------------ % 277.09/39.76 % (195547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.09/39.76 % (195547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.09/39.76 % (195547)CaDiCaL version: 2.1.3 % 277.09/39.76 % (195547)Termination reason: Instruction limit % 277.09/39.76 % (195547)Termination phase: Saturation % 277.09/39.76 % (195547)Time elapsed: 0.300 s % 277.09/39.76 % (195547)Peak memory usage: 120 MB % 277.09/39.76 % (195547)Instructions burned: 402 (million) % 277.09/39.76 % (195553)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3446194506:i=92:rtra=on_2622 on theBenchmark for (2622ds/92Mi) % 277.09/39.76 % (195553)Instruction limit reached! % 277.09/39.76 % (195553)------------------------------ % 277.09/39.76 % (195553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.09/39.76 % (195553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.09/39.76 % (195553)CaDiCaL version: 2.1.3 % 277.09/39.76 % (195553)Termination reason: Instruction limit % 277.09/39.76 % (195553)Termination phase: Saturation % 277.09/39.76 % (195553)Time elapsed: 0.047 s % 277.09/39.76 % (195553)Peak memory usage: 117 MB % 277.09/39.76 % (195553)Instructions burned: 93 (million) % 277.09/39.76 % (195554)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3935581013:i=66:rtra=on_2622 on theBenchmark for (2622ds/66Mi) % 277.09/39.76 % (195554)Instruction limit reached! % 277.09/39.76 % (195554)------------------------------ % 277.09/39.76 % (195554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.09/39.76 % (195554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.09/39.76 % (195554)CaDiCaL version: 2.1.3 % 277.09/39.76 % (195554)Termination reason: Instruction limit % 277.09/39.76 % (195554)Termination phase: Saturation % 277.09/39.76 % (195554)Time elapsed: 0.067 s % 277.09/39.76 % (195554)Peak memory usage: 117 MB % 277.09/39.76 % (195554)Instructions burned: 67 (million) % 277.09/39.76 % (195557)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2751514028:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2620 on theBenchmark for (2620ds/28Mi) % 277.09/39.76 % (195557)Instruction limit reached! % 277.09/39.76 % (195557)------------------------------ % 277.09/39.76 % (195557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.09/39.76 % (195557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.09/39.76 % (195557)CaDiCaL version: 2.1.3 % 277.09/39.76 % (195557)Termination reason: Instruction limit % 277.09/39.76 % (195557)Termination phase: Saturation % 277.09/39.76 % (195557)Time elapsed: 0.010 s % 277.09/39.76 % (195557)Peak memory usage: 89 MB % 277.09/39.76 % (195557)Instructions burned: 28 (million) % 277.09/39.76 % (195560)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3579489633:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2619 on theBenchmark for (2619ds/32Mi) % 277.09/39.76 % (195560)Instruction limit reached! % 277.09/39.76 % (195560)------------------------------ % 277.09/39.76 % (195560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.09/39.76 % (195560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.09/39.76 % (195560)CaDiCaL version: 2.1.3 % 277.09/39.76 % (195560)Termination reason: Instruction limit % 277.09/39.76 % (195560)Termination phase: Saturation % 277.09/39.76 % (195560)Time elapsed: 0.009 s % 277.09/39.76 % (195560)Peak memory usage: 89 MB % 277.09/39.76 % (195560)Instructions burned: 35 (million) % 277.09/39.76 % (195558)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=3429882411:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2620 on theBenchmark for (2620ds/58Mi) % 277.09/39.76 % (195558)Instruction limit reached! % 277.09/39.76 % (195558)------------------------------ % 277.09/39.76 % (195558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.26/40.19 % (195558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/40.19 % (195558)CaDiCaL version: 2.1.3 % 280.26/40.19 % (195558)Termination reason: Instruction limit % 280.26/40.19 % (195558)Termination phase: Clausification % 280.26/40.19 % (195558)Time elapsed: 0.047 s % 280.26/40.19 % (195558)Peak memory usage: 104 MB % 280.26/40.19 % (195558)Instructions burned: 59 (million) % 280.26/40.19 % (195563)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=577084691:i=48:canc=force:rtra=on_2619 on theBenchmark for (2619ds/48Mi) % 280.26/40.19 % (195563)Instruction limit reached! % 280.26/40.19 % (195563)------------------------------ % 280.26/40.19 % (195563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.26/40.19 % (195563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/40.19 % (195563)CaDiCaL version: 2.1.3 % 280.26/40.19 % (195563)Termination reason: Instruction limit % 280.26/40.19 % (195563)Termination phase: Saturation % 280.26/40.19 % (195563)Time elapsed: 0.018 s % 280.26/40.19 % (195563)Peak memory usage: 90 MB % 280.26/40.19 % (195563)Instructions burned: 51 (million) % 280.26/40.19 % (195564)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=2991836244:i=54:canc=cautious:fsr=off:rtra=on_2618 on theBenchmark for (2618ds/54Mi) % 280.26/40.19 % (195566)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2494452247:i=170:gtgl=4:rtra=on:gtg=exists_sym_2617 on theBenchmark for (2617ds/170Mi) % 280.26/40.19 % (195564)Instruction limit reached! % 280.26/40.19 % (195564)------------------------------ % 280.26/40.19 % (195564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.26/40.19 % (195564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/40.19 % (195564)CaDiCaL version: 2.1.3 % 280.26/40.19 % (195564)Termination reason: Instruction limit % 280.26/40.19 % (195564)Termination phase: Saturation % 280.26/40.19 % (195564)Time elapsed: 0.037 s % 280.26/40.19 % (195564)Peak memory usage: 90 MB % 280.26/40.19 % (195564)Instructions burned: 60 (million) % 280.26/40.19 % (195566)Instruction limit reached! % 280.26/40.19 % (195566)------------------------------ % 280.26/40.19 % (195566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.26/40.19 % (195566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/40.19 % (195566)CaDiCaL version: 2.1.3 % 280.26/40.19 % (195566)Termination reason: Instruction limit % 280.26/40.19 % (195566)Termination phase: Saturation % 280.26/40.19 % (195566)Time elapsed: 0.045 s % 280.26/40.19 % (195566)Peak memory usage: 89 MB % 280.26/40.19 % (195566)Instructions burned: 174 (million) % 280.26/40.19 % (195570)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1329259077:i=362:rtra=on:ss=axioms:ev=cautious_2616 on theBenchmark for (2616ds/362Mi) % 280.26/40.19 % (195569)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1309916956:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2616 on theBenchmark for (2616ds/4Mi) % 280.26/40.19 % (195569)Instruction limit reached! % 280.26/40.19 % (195569)------------------------------ % 280.26/40.19 % (195569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.26/40.19 % (195569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/40.19 % (195569)CaDiCaL version: 2.1.3 % 280.26/40.19 % (195569)Termination reason: Instruction limit % 280.26/40.19 % (195569)Termination phase: Preprocessing 3 % 280.26/40.19 % (195569)Time elapsed: 0.004 s % 280.26/40.19 % (195569)Peak memory usage: 86 MB % 280.26/40.19 % (195569)Instructions burned: 7 (million) % 280.26/40.19 % (195570)Instruction limit reached! % 280.26/40.19 % (195570)------------------------------ % 280.26/40.19 % (195570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.26/40.19 % (195570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/40.19 % (195570)CaDiCaL version: 2.1.3 % 280.26/40.19 % (195570)Termination reason: Instruction limit % 280.26/40.19 % (195570)Termination phase: Saturation % 280.26/40.19 % (195570)Time elapsed: 0.119 s % 280.26/40.19 % (195570)Peak memory usage: 92 MB % 280.26/40.19 % (195570)Instructions burned: 364 (million) % 280.26/40.19 % (195573)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3403544395:i=8:ep=RST:ins=2:rtra=on_2615 on theBenchmark for (2615ds/8Mi) % 280.26/40.19 % (195573)Instruction limit reached! % 280.26/40.19 % (195573)------------------------------ % 280.26/40.19 % (195573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.83/40.82 % (195573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.83/40.82 % (195573)CaDiCaL version: 2.1.3 % 284.83/40.82 % (195573)Termination reason: Instruction limit % 284.83/40.82 % (195573)Termination phase: Function definition elimination % 284.83/40.82 % (195573)Time elapsed: 0.005 s % 284.83/40.82 % (195573)Peak memory usage: 86 MB % 284.83/40.82 % (195573)Instructions burned: 9 (million) % 284.83/40.82 % (195574)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3058014476:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2614 on theBenchmark for (2614ds/132Mi) % 284.83/40.82 % (195574)Instruction limit reached! % 284.83/40.82 % (195574)------------------------------ % 284.83/40.82 % (195574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.83/40.82 % (195574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.83/40.82 % (195574)CaDiCaL version: 2.1.3 % 284.83/40.82 % (195574)Termination reason: Instruction limit % 284.83/40.82 % (195574)Termination phase: Saturation % 284.83/40.82 % (195574)Time elapsed: 0.076 s % 284.83/40.82 % (195574)Peak memory usage: 135 MB % 284.83/40.82 % (195574)Instructions burned: 132 (million) % 284.83/40.82 % (195576)lrs+10_1_thi=all:si=on:fd=off:random_seed=1764915524:i=106:rtra=on:gtg=all_2614 on theBenchmark for (2614ds/106Mi) % 284.83/40.82 % (195579)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=1607049067:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2612 on theBenchmark for (2612ds/16Mi) % 284.83/40.82 % (195579)Instruction limit reached! % 284.83/40.82 % (195579)------------------------------ % 284.83/40.82 % (195579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.83/40.82 % (195579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.83/40.82 % (195579)CaDiCaL version: 2.1.3 % 284.83/40.82 % (195579)Termination reason: Instruction limit % 284.83/40.82 % (195579)Termination phase: Property scanning % 284.83/40.82 % (195579)Time elapsed: 0.004 s % 284.83/40.82 % (195579)Peak memory usage: 87 MB % 284.83/40.82 % (195579)Instructions burned: 17 (million) % 284.83/40.82 % (195576)Instruction limit reached! % 284.83/40.82 % (195576)------------------------------ % 284.83/40.82 % (195576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.83/40.82 % (195576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.83/40.82 % (195576)CaDiCaL version: 2.1.3 % 284.83/40.82 % (195576)Termination reason: Instruction limit % 284.83/40.82 % (195576)Termination phase: Saturation % 284.83/40.82 % (195576)Time elapsed: 0.100 s % 284.83/40.82 % (195576)Peak memory usage: 117 MB % 284.83/40.82 % (195576)Instructions burned: 106 (million) % 284.83/40.82 % (195581)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=903413380:st=3:i=4:rtra=on:ss=axioms_2611 on theBenchmark for (2611ds/4Mi) % 284.83/40.82 % (195581)Instruction limit reached! % 284.83/40.82 % (195581)------------------------------ % 284.83/40.82 % (195581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.83/40.82 % (195581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.83/40.82 % (195581)CaDiCaL version: 2.1.3 % 284.83/40.82 % (195581)Termination reason: Instruction limit % 284.83/40.82 % (195581)Termination phase: Property scanning % 284.83/40.82 % (195581)Time elapsed: 0.002 s % 284.83/40.82 % (195581)Peak memory usage: 86 MB % 284.83/40.82 % (195581)Instructions burned: 6 (million) % 284.83/40.82 % (195582)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3741712408:i=4:doe=on:canc=force:asg=cautious:rtra=on_2611 on theBenchmark for (2611ds/4Mi) % 284.83/40.82 % (195582)Instruction limit reached! % 284.83/40.82 % (195582)------------------------------ % 284.83/40.82 % (195582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.83/40.82 % (195582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.83/40.82 % (195582)CaDiCaL version: 2.1.3 % 284.83/40.82 % (195582)Termination reason: Instruction limit % 284.83/40.82 % (195582)Termination phase: Preprocessing 3 % 284.83/40.82 % (195582)Time elapsed: 0.003 s % 284.83/40.82 % (195582)Peak memory usage: 86 MB % 284.83/40.82 % (195582)Instructions burned: 5 (million) % 284.83/40.82 % (195584)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=292885853:i=254:doe=on:rtra=on_2611 on theBenchmark for (2611ds/254Mi) % 284.83/40.82 % (195586)dis+10_1_si=on:random_seed=3069678527:i=20:ep=R:rtra=on_2610 on theBenchmark for (2610ds/20Mi) % 284.83/40.82 % (195584)Instruction limit reached! % 289.78/41.58 % (195584)------------------------------ % 289.78/41.58 % (195584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.78/41.58 % (195584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.78/41.58 % (195584)CaDiCaL version: 2.1.3 % 289.78/41.58 % (195584)Termination reason: Instruction limit % 289.78/41.58 % (195584)Termination phase: Saturation % 289.78/41.58 % (195584)Time elapsed: 0.104 s % 289.78/41.58 % (195584)Peak memory usage: 119 MB % 289.78/41.58 % (195584)Instructions burned: 257 (million) % 289.78/41.58 % (195586)Instruction limit reached! % 289.78/41.58 % (195586)------------------------------ % 289.78/41.58 % (195586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.78/41.58 % (195586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.78/41.58 % (195586)CaDiCaL version: 2.1.3 % 289.78/41.58 % (195586)Termination reason: Instruction limit % 289.78/41.58 % (195586)Termination phase: Saturation % 289.78/41.58 % (195586)Time elapsed: 0.012 s % 289.78/41.58 % (195586)Peak memory usage: 89 MB % 289.78/41.58 % (195586)Instructions burned: 22 (million) % 289.78/41.58 % (195589)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1201565610:i=52:canc=cautious:av=off:rtra=on_2609 on theBenchmark for (2609ds/52Mi) % 289.78/41.58 % (195589)Refutation not found, incomplete strategy % 289.78/41.58 % (195589)------------------------------ % 289.78/41.58 % (195589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.78/41.58 % (195589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.78/41.58 % (195589)CaDiCaL version: 2.1.3 % 289.78/41.58 % (195589)Termination reason: Refutation not found, incomplete strategy % 289.78/41.58 % (195589)Time elapsed: 0.006 s % 289.78/41.58 % (195589)Peak memory usage: 89 MB % 289.78/41.58 % (195589)Instructions burned: 19 (million) % 289.78/41.58 % (195590)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=588061850:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2609 on theBenchmark for (2609ds/70Mi) % 289.78/41.58 % (195590)Instruction limit reached! % 289.78/41.58 % (195590)------------------------------ % 289.78/41.58 % (195590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.78/41.58 % (195590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.78/41.58 % (195590)CaDiCaL version: 2.1.3 % 289.78/41.58 % (195590)Termination reason: Instruction limit % 289.78/41.58 % (195590)Termination phase: Saturation % 289.78/41.58 % (195590)Time elapsed: 0.042 s % 289.78/41.58 % (195590)Peak memory usage: 89 MB % 289.78/41.58 % (195590)Instructions burned: 71 (million) % 289.78/41.58 % (195589)------------------------------ % 289.78/41.58 % (195589)------------------------------ % 289.78/41.58 % (195593)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1126735518:i=4:fsr=off:rtra=on:inst=on_2607 on theBenchmark for (2607ds/4Mi) % 289.78/41.58 % (195593)Instruction limit reached! % 289.78/41.58 % (195593)------------------------------ % 289.78/41.58 % (195593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.78/41.58 % (195593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.78/41.58 % (195593)CaDiCaL version: 2.1.3 % 289.78/41.58 % (195593)Termination reason: Instruction limit % 289.78/41.58 % (195593)Termination phase: Preprocessing 3 % 289.78/41.58 % (195593)Time elapsed: 0.003 s % 289.78/41.58 % (195593)Peak memory usage: 86 MB % 289.78/41.58 % (195593)Instructions burned: 5 (million) % 289.78/41.58 % (195594)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1480936567:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2606 on theBenchmark for (2606ds/16Mi) % 289.78/41.58 % (195594)Instruction limit reached! % 289.78/41.58 % (195594)------------------------------ % 289.78/41.58 % (195594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.78/41.58 % (195594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.78/41.58 % (195594)CaDiCaL version: 2.1.3 % 289.78/41.58 % (195594)Termination reason: Instruction limit % 289.78/41.58 % (195594)Termination phase: Saturation % 289.78/41.58 % (195594)Time elapsed: 0.005 s % 289.78/41.58 % (195594)Peak memory usage: 89 MB % 289.78/41.58 % (195594)Instructions burned: 17 (million) % 289.78/41.58 % (195598)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=702466114:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2605 on theBenchmark for (2605ds/26Mi) % 289.78/41.58 % (195598)Instruction limit reached! % 299.13/42.86 % (195598)------------------------------ % 299.13/42.86 % (195598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.13/42.86 % (195598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.13/42.86 % (195598)CaDiCaL version: 2.1.3 % 299.13/42.86 % (195598)Termination reason: Instruction limit % 299.13/42.86 % (195598)Termination phase: Saturation % 299.13/42.86 % (195598)Time elapsed: 0.021 s % 299.13/42.86 % (195598)Peak memory usage: 113 MB % 299.13/42.86 % (195598)Instructions burned: 28 (million) % 299.13/42.86 % (195596)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=751166741:i=740:ep=RS:fsr=off:rtra=on_2606 on theBenchmark for (2606ds/740Mi) % 299.13/42.86 % (195600)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2099133536:i=452:rtra=on:gtg=position:ss=axioms_2604 on theBenchmark for (2604ds/452Mi) % 299.13/42.86 % (195600)Instruction limit reached! % 299.13/42.86 % (195600)------------------------------ % 299.13/42.86 % (195600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.13/42.86 % (195600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.13/42.86 % (195600)CaDiCaL version: 2.1.3 % 299.13/42.86 % (195600)Termination reason: Instruction limit % 299.13/42.86 % (195600)Termination phase: Saturation % 299.13/42.86 % (195600)Time elapsed: 0.158 s % 299.13/42.86 % (195600)Peak memory usage: 119 MB % 299.13/42.86 % (195600)Instructions burned: 452 (million) % 299.13/42.86 % (195603)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=271809604:i=20:rtra=on_2602 on theBenchmark for (2602ds/20Mi) % 299.13/42.86 % (195603)Instruction limit reached! % 299.13/42.86 % (195603)------------------------------ % 299.13/42.86 % (195603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.13/42.86 % (195603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.13/42.86 % (195603)CaDiCaL version: 2.1.3 % 299.13/42.86 % (195603)Termination reason: Instruction limit % 299.13/42.86 % (195603)Termination phase: Saturation % 299.13/42.86 % (195603)Time elapsed: 0.007 s % 299.13/42.86 % (195603)Peak memory usage: 89 MB % 299.13/42.86 % (195603)Instructions burned: 22 (million) % 299.13/42.86 % (195596)Instruction limit reached! % 299.13/42.86 % (195596)------------------------------ % 299.13/42.86 % (195596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.13/42.86 % (195596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.13/42.86 % (195596)CaDiCaL version: 2.1.3 % 299.13/42.86 % (195596)Termination reason: Instruction limit % 299.13/42.86 % (195596)Termination phase: Saturation % 299.13/42.86 % (195596)Time elapsed: 0.395 s % 299.13/42.86 % (195596)Peak memory usage: 92 MB % 299.13/42.86 % (195596)Instructions burned: 741 (million) % 299.13/42.86 % (195605)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3026055220:i=142:rtra=on:gtg=exists_top_2601 on theBenchmark for (2601ds/142Mi) % 299.13/42.86 % (195605)Instruction limit reached! % 299.13/42.86 % (195605)------------------------------ % 299.13/42.86 % (195605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.13/42.86 % (195605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.13/42.86 % (195605)CaDiCaL version: 2.1.3 % 299.13/42.86 % (195605)Termination reason: Instruction limit % 299.13/42.86 % (195605)Termination phase: Saturation % 299.13/42.86 % (195605)Time elapsed: 0.068 s % 299.13/42.86 % (195605)Peak memory usage: 133 MB % 299.13/42.86 % (195605)Instructions burned: 144 (million) % 299.13/42.86 % (195606)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=4101803470:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2600 on theBenchmark for (2600ds/150Mi) % 299.13/42.86 % (195608)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=1915280324:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2599 on theBenchmark for (2599ds/588Mi) % 299.13/42.86 % (195606)Instruction limit reached! % 299.13/42.86 % (195606)------------------------------ % 299.13/42.86 % (195606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.13/42.86 % (195606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.13/42.86 % (195606)CaDiCaL version: 2.1.3 % 299.13/42.86 % (195606)Termination reason: Instruction limit % 299.13/42.86 % (195606)Termination phase: Saturation % 299.13/42.86 % (195606)Time elapsed: 0.076 s % 299.13/42.86 % (195606)Peak memory usage: 90 MB % 300.89/43.06 % (195606)Instructions burned: 153 (million) % 300.89/43.06 % (195608)Instruction limit reached! % 300.89/43.06 % (195608)------------------------------ % 300.89/43.06 % (195608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.89/43.06 % (195608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.89/43.06 % (195608)CaDiCaL version: 2.1.3 % 300.89/43.06 % (195608)Termination reason: Instruction limit % 300.89/43.06 % (195608)Termination phase: Property scanning % 300.89/43.06 % (195608)Time elapsed: 0.134 s % 300.89/43.06 % (195608)Peak memory usage: 118 MB % 300.89/43.06 % (195608)Instructions burned: 592 (million) % 300.89/43.06 % (195611)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3863123047:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2598 on theBenchmark for (2598ds/260Mi) % 300.89/43.06 % (195612)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3413211660:i=262:rtra=on_2597 on theBenchmark for (2597ds/262Mi) % 300.89/43.06 % (195611)Instruction limit reached! % 300.89/43.06 % (195611)------------------------------ % 300.89/43.06 % (195611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.89/43.06 % (195611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.89/43.06 % (195611)CaDiCaL version: 2.1.3 % 300.89/43.06 % (195611)Termination reason: Instruction limit % 300.89/43.06 % (195611)Termination phase: Property scanning % 300.89/43.06 % (195611)Time elapsed: 0.137 s % 300.89/43.06 % (195611)Peak memory usage: 118 MB % 300.89/43.06 % (195611)Instructions burned: 262 (million) % 300.89/43.06 % (195612)Instruction limit reached! % 300.89/43.06 % (195612)------------------------------ % 300.89/43.06 % (195612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.89/43.06 % (195612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.89/43.06 % (195612)CaDiCaL version: 2.1.3 % 300.89/43.06 % (195612)Termination reason: Instruction limit % 300.89/43.06 % (195612)Termination phase: Saturation % 300.89/43.06 % (195612)Time elapsed: 0.107 s % 300.89/43.06 % (195612)Peak memory usage: 134 MB % 300.89/43.06 % (195612)Instructions burned: 263 (million) % 300.89/43.06 % (195615)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2466062754:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2595 on theBenchmark for (2595ds/80Mi) % 300.89/43.06 % (195616)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2404799786:i=614:rtra=on:gtg=exists_top_2595 on theBenchmark for (2595ds/614Mi) % 300.89/43.06 % (195615)Instruction limit reached! % 300.89/43.06 % (195615)------------------------------ % 300.89/43.06 % (195615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.89/43.06 % (195615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.89/43.06 % (195615)CaDiCaL version: 2.1.3 % 300.89/43.06 % (195615)Termination reason: Instruction limit % 300.89/43.06 % (195615)Termination phase: Saturation % 300.89/43.06 % (195615)Time elapsed: 0.091 s % 300.89/43.06 % (195615)Peak memory usage: 134 MB % 300.89/43.06 % (195615)Instructions burned: 81 (million) % 300.89/43.06 % (195616)Instruction limit reached! % 300.89/43.06 % (195616)------------------------------ % 300.89/43.06 % (195616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.89/43.06 % (195616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.89/43.06 % (195616)CaDiCaL version: 2.1.3 % 300.89/43.06 % (195616)Termination reason: Instruction limit % 300.89/43.06 % (195616)Termination phase: Saturation % 300.89/43.06 % (195616)Time elapsed: 0.160 s % 300.89/43.06 % (195616)Peak memory usage: 96 MB % 300.89/43.06 % (195616)Instructions burned: 618 (million) % 300.89/43.06 % (195619)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4226853563:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2593 on theBenchmark for (2593ds/1196Mi) % 300.89/43.06 % (195620)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=239696914:i=262:canc=cautious:fsr=off:rtra=on_2592 on theBenchmark for (2592ds/262Mi) % 300.89/43.06 % (195620)Instruction limit reached! % 300.89/43.06 % (195620)------------------------------ % 300.89/43.06 % (195620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.89/43.06 % (195620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.89/43.06 % (195620)CaDiCaL version: 2.1.3 % 300.89/43.06 % (195620)Termination reason: Instruction limit % 300.89/43.06 % (195620)Termination phase: Saturation % 300.89/43.06 % (195620)Time elapsed: 0.108 s % 300.89/43.06 % (195620)P % 300.89/43.07 Terminated %------------------------------------------------------------------------------