%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX128_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:56 PM UTC 2026 % Result : Timeout 288.27s 41.30s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX128_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.18 % Computer : n002.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 15:05:22 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.22 Running first-order theorem proving % 0.07/0.22 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.46/1.19 % (423428)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.46/1.19 % (423439)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1405878871:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.46/1.19 % (423439)Instruction limit reached! % 3.46/1.19 % (423439)------------------------------ % 3.46/1.19 % (423439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.19 % (423439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.19 % (423439)CaDiCaL version: 2.1.3 % 3.46/1.19 % (423439)Termination reason: Instruction limit % 3.46/1.19 % (423439)Termination phase: Saturation % 3.46/1.19 % (423439)Time elapsed: 0.007 s % 3.46/1.19 % (423439)Peak memory usage: 88 MB % 3.46/1.19 % (423439)Instructions burned: 35 (million) % 3.46/1.19 % (423433)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2577601641:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.46/1.19 % (423438)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3468206505:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.46/1.19 % (423435)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=143266087:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.46/1.19 % (423437)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1866675475:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.46/1.19 % (423434)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=85288943:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.46/1.19 % (423436)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1650352379:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.46/1.19 % (423437)Instruction limit reached! % 3.46/1.19 % (423437)------------------------------ % 3.46/1.19 % (423437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.19 % (423437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.19 % (423437)CaDiCaL version: 2.1.3 % 3.46/1.19 % (423437)Termination reason: Instruction limit % 3.46/1.19 % (423437)Termination phase: Property scanning % 3.46/1.19 % (423437)Time elapsed: 0.003 s % 3.46/1.19 % (423437)Peak memory usage: 85 MB % 3.46/1.19 % (423437)Instructions burned: 7 (million) % 3.46/1.19 % (423436)Instruction limit reached! % 3.46/1.19 % (423436)------------------------------ % 3.46/1.19 % (423436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.19 % (423436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.19 % (423436)CaDiCaL version: 2.1.3 % 3.46/1.19 % (423436)Termination reason: Instruction limit % 3.46/1.19 % (423436)Termination phase: Property scanning % 3.46/1.19 % (423436)Time elapsed: 0.003 s % 3.46/1.19 % (423436)Peak memory usage: 85 MB % 3.46/1.19 % (423436)Instructions burned: 7 (million) % 3.46/1.19 % (423433)Instruction limit reached! % 3.46/1.19 % (423433)------------------------------ % 3.46/1.19 % (423433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.19 % (423433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.19 % (423433)CaDiCaL version: 2.1.3 % 3.46/1.19 % (423433)Termination reason: Instruction limit % 3.46/1.19 % (423433)Termination phase: Property scanning % 3.46/1.19 % (423433)Time elapsed: 0.006 s % 3.46/1.19 % (423433)Peak memory usage: 85 MB % 3.46/1.19 % (423433)Instructions burned: 13 (million) % 3.46/1.19 % (423438)Instruction limit reached! % 3.46/1.19 % (423438)------------------------------ % 3.46/1.19 % (423438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.46/1.19 % (423438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.46/1.19 % (423438)CaDiCaL version: 2.1.3 % 3.46/1.19 % (423438)Termination reason: Instruction limit % 3.46/1.19 % (423438)Termination phase: Saturation % 3.46/1.19 % (423438)Time elapsed: 0.041 s % 3.46/1.19 % (423438)Peak memory usage: 111 MB % 3.46/1.19 % (423438)Instructions burned: 47 (million) % 3.46/1.19 % (423441)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2293847061:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.46/1.19 % (423441)Refutation not found, incomplete strategy % 3.46/1.19 % (423441)------------------------------ % 3.46/1.19 % (423441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423441)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423441)Termination reason: Refutation not found, incomplete strategy % 4.32/1.33 % (423441)Time elapsed: 0.004 s % 4.32/1.33 % (423441)Peak memory usage: 88 MB % 4.32/1.33 % (423441)Instructions burned: 18 (million) % 4.32/1.33 % (423435)Instruction limit reached! % 4.32/1.33 % (423435)------------------------------ % 4.32/1.33 % (423435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423435)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423435)Termination reason: Instruction limit % 4.32/1.33 % (423435)Termination phase: Saturation % 4.32/1.33 % (423435)Time elapsed: 0.109 s % 4.32/1.33 % (423435)Peak memory usage: 117 MB % 4.32/1.33 % (423435)Instructions burned: 202 (million) % 4.32/1.33 % (423449)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2585934056:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.32/1.33 % (423450)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1956964431:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.32/1.33 % (423448)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=1775647529:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.32/1.33 % (423449)Instruction limit reached! % 4.32/1.33 % (423449)------------------------------ % 4.32/1.33 % (423449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423449)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423449)Termination reason: Instruction limit % 4.32/1.33 % (423449)Termination phase: Property scanning % 4.32/1.33 % (423449)Time elapsed: 0.007 s % 4.32/1.33 % (423449)Peak memory usage: 86 MB % 4.32/1.33 % (423449)Instructions burned: 18 (million) % 4.32/1.33 % (423434)Instruction limit reached! % 4.32/1.33 % (423434)------------------------------ % 4.32/1.33 % (423434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423434)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423434)Termination reason: Instruction limit % 4.32/1.33 % (423434)Termination phase: Saturation % 4.32/1.33 % (423434)Time elapsed: 0.153 s % 4.32/1.33 % (423434)Peak memory usage: 117 MB % 4.32/1.33 % (423434)Instructions burned: 310 (million) % 4.32/1.33 % (423450)Instruction limit reached! % 4.32/1.33 % (423450)------------------------------ % 4.32/1.33 % (423450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423450)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423450)Termination reason: Instruction limit % 4.32/1.33 % (423450)Termination phase: Property scanning % 4.32/1.33 % (423450)Time elapsed: 0.011 s % 4.32/1.33 % (423450)Peak memory usage: 86 MB % 4.32/1.33 % (423450)Instructions burned: 27 (million) % 4.32/1.33 % (423448)Instruction limit reached! % 4.32/1.33 % (423448)------------------------------ % 4.32/1.33 % (423448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423448)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423448)Termination reason: Instruction limit % 4.32/1.33 % (423448)Termination phase: Saturation % 4.32/1.33 % (423448)Time elapsed: 0.012 s % 4.32/1.33 % (423448)Peak memory usage: 87 MB % 4.32/1.33 % (423448)Instructions burned: 30 (million) % 4.32/1.33 % (423451)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=2897600998:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.32/1.33 % (423451)Instruction limit reached! % 4.32/1.33 % (423451)------------------------------ % 4.32/1.33 % (423451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.32/1.33 % (423451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/1.33 % (423451)CaDiCaL version: 2.1.3 % 4.32/1.33 % (423451)Termination reason: Instruction limit % 5.25/1.48 % (423451)Termination phase: Saturation % 5.25/1.48 % (423451)Time elapsed: 0.011 s % 5.25/1.48 % (423451)Peak memory usage: 88 MB % 5.25/1.48 % (423451)Instructions burned: 29 (million) % 5.25/1.48 % (423441)------------------------------ % 5.25/1.48 % (423441)------------------------------ % 5.25/1.48 % (423453)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2097437487:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.25/1.48 % (423457)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3305796002:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.25/1.48 % (423457)Instruction limit reached! % 5.25/1.48 % (423457)------------------------------ % 5.25/1.48 % (423457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.25/1.48 % (423457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.25/1.48 % (423457)CaDiCaL version: 2.1.3 % 5.25/1.48 % (423457)Termination reason: Instruction limit % 5.25/1.48 % (423457)Termination phase: Property scanning % 5.25/1.48 % (423457)Time elapsed: 0.002 s % 5.25/1.48 % (423457)Peak memory usage: 85 MB % 5.25/1.48 % (423457)Instructions burned: 3 (million) % 5.25/1.48 % (423453)Instruction limit reached! % 5.25/1.48 % (423453)------------------------------ % 5.25/1.48 % (423453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.25/1.48 % (423453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.25/1.48 % (423453)CaDiCaL version: 2.1.3 % 5.25/1.48 % (423453)Termination reason: Instruction limit % 5.25/1.48 % (423453)Termination phase: Saturation % 5.25/1.48 % (423453)Time elapsed: 0.038 s % 5.25/1.48 % (423453)Peak memory usage: 89 MB % 5.25/1.48 % (423453)Instructions burned: 86 (million) % 5.25/1.48 % (423458)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=169407898:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.25/1.48 % (423460)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1269037413:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 5.25/1.48 % (423459)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2581100595:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.25/1.48 % (423459)Instruction limit reached! % 5.25/1.48 % (423459)------------------------------ % 5.25/1.48 % (423459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.25/1.48 % (423459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.25/1.48 % (423459)CaDiCaL version: 2.1.3 % 5.25/1.48 % (423459)Termination reason: Instruction limit % 5.25/1.48 % (423459)Termination phase: Property scanning % 5.25/1.48 % (423459)Time elapsed: 0.003 s % 5.25/1.48 % (423459)Peak memory usage: 85 MB % 5.25/1.48 % (423459)Instructions burned: 7 (million) % 5.25/1.48 % (423458)Refutation not found, incomplete strategy % 5.25/1.48 % (423458)------------------------------ % 5.25/1.48 % (423458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.25/1.48 % (423458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.25/1.48 % (423458)CaDiCaL version: 2.1.3 % 5.25/1.48 % (423458)Termination reason: Refutation not found, incomplete strategy % 5.25/1.48 % (423458)Time elapsed: 0.007 s % 5.25/1.48 % (423458)Peak memory usage: 87 MB % 5.25/1.48 % (423458)Instructions burned: 17 (million) % 5.25/1.48 % (423463)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=4046875442:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 5.25/1.48 % (423463)Instruction limit reached! % 5.25/1.48 % (423463)------------------------------ % 5.25/1.48 % (423463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.25/1.48 % (423463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.25/1.48 % (423463)CaDiCaL version: 2.1.3 % 5.25/1.48 % (423463)Termination reason: Instruction limit % 5.25/1.48 % (423463)Termination phase: Property scanning % 5.25/1.48 % (423463)Time elapsed: 0.002 s % 5.25/1.48 % (423463)Peak memory usage: 85 MB % 5.25/1.48 % (423463)Instructions burned: 9 (million) % 5.25/1.48 % (423462)lrs+10_1_thi=all:si=on:fd=off:random_seed=2260891111:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.25/1.48 % (423460)Instruction limit reached! % 5.25/1.48 % (423460)------------------------------ % 5.25/1.48 % (423460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.62 % (423460)CaDiCaL version: 2.1.3 % 5.90/1.62 % (423460)Termination reason: Instruction limit % 5.90/1.62 % (423460)Termination phase: Saturation % 5.90/1.62 % (423460)Time elapsed: 0.069 s % 5.90/1.62 % (423460)Peak memory usage: 128 MB % 5.90/1.62 % (423460)Instructions burned: 67 (million) % 5.90/1.62 % (423462)Instruction limit reached! % 5.90/1.62 % (423462)------------------------------ % 5.90/1.62 % (423462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.62 % (423462)CaDiCaL version: 2.1.3 % 5.90/1.62 % (423462)Termination reason: Instruction limit % 5.90/1.62 % (423462)Termination phase: Saturation % 5.90/1.62 % (423462)Time elapsed: 0.039 s % 5.90/1.62 % (423462)Peak memory usage: 105 MB % 5.90/1.62 % (423462)Instructions burned: 53 (million) % 5.90/1.62 % (423473)dis+10_1_si=on:random_seed=3410124888:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi) % 5.90/1.62 % (423473)Instruction limit reached! % 5.90/1.62 % (423473)------------------------------ % 5.90/1.62 % (423473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.62 % (423473)CaDiCaL version: 2.1.3 % 5.90/1.62 % (423473)Termination reason: Instruction limit % 5.90/1.62 % (423473)Termination phase: Property scanning % 5.90/1.62 % (423473)Time elapsed: 0.003 s % 5.90/1.62 % (423473)Peak memory usage: 85 MB % 5.90/1.62 % (423473)Instructions burned: 14 (million) % 5.90/1.62 % (423470)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3159960351:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 5.90/1.62 % (423466)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=625081073:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 5.90/1.62 % (423470)Instruction limit reached! % 5.90/1.62 % (423470)------------------------------ % 5.90/1.62 % (423470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.62 % (423470)CaDiCaL version: 2.1.3 % 5.90/1.62 % (423470)Termination reason: Instruction limit % 5.90/1.62 % (423470)Termination phase: Property scanning % 5.90/1.62 % (423470)Time elapsed: 0.002 s % 5.90/1.62 % (423470)Peak memory usage: 85 MB % 5.90/1.62 % (423470)Instructions burned: 4 (million) % 5.90/1.62 % (423466)Instruction limit reached! % 5.90/1.62 % (423466)------------------------------ % 5.90/1.62 % (423466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.62 % (423466)CaDiCaL version: 2.1.3 % 5.90/1.62 % (423466)Termination reason: Instruction limit % 5.90/1.62 % (423466)Termination phase: Property scanning % 5.90/1.62 % (423466)Time elapsed: 0.002 s % 5.90/1.62 % (423466)Peak memory usage: 85 MB % 5.90/1.62 % (423466)Instructions burned: 4 (million) % 5.90/1.62 % (423471)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1410124609:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 5.90/1.62 % (423478)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3417777704:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 5.90/1.62 % (423478)Instruction limit reached! % 5.90/1.62 % (423478)------------------------------ % 5.90/1.62 % (423478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.62 % (423478)CaDiCaL version: 2.1.3 % 5.90/1.62 % (423478)Termination reason: Instruction limit % 5.90/1.62 % (423478)Termination phase: Property scanning % 5.90/1.62 % (423478)Time elapsed: 0.001 s % 5.90/1.62 % (423478)Peak memory usage: 85 MB % 5.90/1.62 % (423478)Instructions burned: 3 (million) % 5.90/1.62 % (423475)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2921389243:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 5.90/1.62 % (423471)Instruction limit reached! % 5.90/1.62 % (423471)------------------------------ % 5.90/1.62 % (423471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.90/1.62 % (423471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.85 % (423471)CaDiCaL version: 2.1.3 % 7.45/1.85 % (423471)Termination reason: Instruction limit % 7.45/1.85 % (423471)Termination phase: Saturation % 7.45/1.85 % (423471)Time elapsed: 0.074 s % 7.45/1.85 % (423471)Peak memory usage: 113 MB % 7.45/1.85 % (423471)Instructions burned: 128 (million) % 7.45/1.85 % (423476)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1420105569:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi) % 7.45/1.85 % (423475)Instruction limit reached! % 7.45/1.85 % (423475)------------------------------ % 7.45/1.85 % (423475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.45/1.85 % (423475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.85 % (423475)CaDiCaL version: 2.1.3 % 7.45/1.85 % (423475)Termination reason: Instruction limit % 7.45/1.85 % (423475)Termination phase: Property scanning % 7.45/1.85 % (423475)Time elapsed: 0.011 s % 7.45/1.85 % (423475)Peak memory usage: 86 MB % 7.45/1.85 % (423475)Instructions burned: 27 (million) % 7.45/1.85 % (423476)Instruction limit reached! % 7.45/1.85 % (423476)------------------------------ % 7.45/1.85 % (423476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.45/1.85 % (423476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.85 % (423476)CaDiCaL version: 2.1.3 % 7.45/1.85 % (423476)Termination reason: Instruction limit % 7.45/1.85 % (423476)Termination phase: Saturation % 7.45/1.85 % (423476)Time elapsed: 0.014 s % 7.45/1.85 % (423476)Peak memory usage: 86 MB % 7.45/1.85 % (423476)Instructions burned: 36 (million) % 7.45/1.85 % (423481)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2755970351:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.45/1.85 % (423482)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=159319438:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 7.45/1.85 % (423458)------------------------------ % 7.45/1.85 % (423458)------------------------------ % 7.45/1.85 % (423481)Instruction limit reached! % 7.45/1.85 % (423481)------------------------------ % 7.45/1.85 % (423481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.45/1.85 % (423481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.85 % (423481)CaDiCaL version: 2.1.3 % 7.45/1.85 % (423481)Termination reason: Instruction limit % 7.45/1.85 % (423481)Termination phase: Property scanning % 7.45/1.85 % (423481)Time elapsed: 0.004 s % 7.45/1.85 % (423481)Peak memory usage: 85 MB % 7.45/1.85 % (423481)Instructions burned: 9 (million) % 7.45/1.85 % (423485)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2833489564:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.45/1.85 % (423485)Instruction limit reached! % 7.45/1.85 % (423485)------------------------------ % 7.45/1.85 % (423485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.45/1.85 % (423485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.85 % (423485)CaDiCaL version: 2.1.3 % 7.45/1.85 % (423485)Termination reason: Instruction limit % 7.45/1.85 % (423485)Termination phase: shuffling % 7.45/1.85 % (423485)Time elapsed: 0.003 s % 7.45/1.85 % (423485)Peak memory usage: 85 MB % 7.45/1.85 % (423485)Instructions burned: 15 (million) % 7.45/1.85 % (423482)Refutation not found, incomplete strategy % 7.45/1.85 % (423482)------------------------------ % 7.45/1.85 % (423482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.45/1.85 % (423482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.45/1.85 % (423482)CaDiCaL version: 2.1.3 % 7.45/1.85 % (423482)Termination reason: Refutation not found, incomplete strategy % 7.45/1.85 % (423482)Time elapsed: 0.020 s % 7.45/1.85 % (423482)Peak memory usage: 89 MB % 7.45/1.85 % (423482)Instructions burned: 49 (million) % 7.45/1.85 % (423488)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1790466185:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.45/1.85 % (423489)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3258118977:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 7.45/1.85 % (423489)Instruction limit reached! % 9.94/2.10 % (423489)------------------------------ % 9.94/2.10 % (423489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.10 % (423489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.10 % (423489)CaDiCaL version: 2.1.3 % 9.94/2.10 % (423489)Termination reason: Instruction limit % 9.94/2.10 % (423489)Termination phase: Property scanning % 9.94/2.10 % (423489)Time elapsed: 0.005 s % 9.94/2.10 % (423489)Peak memory usage: 85 MB % 9.94/2.10 % (423489)Instructions burned: 12 (million) % 9.94/2.10 % (423496)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2707957936:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 9.94/2.10 % (423490)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3465574217:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 9.94/2.10 % (423488)Refutation not found, incomplete strategy % 9.94/2.10 % (423488)------------------------------ % 9.94/2.10 % (423488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.10 % (423488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.10 % (423488)CaDiCaL version: 2.1.3 % 9.94/2.10 % (423488)Termination reason: Refutation not found, incomplete strategy % 9.94/2.10 % (423488)Time elapsed: 0.035 s % 9.94/2.10 % (423488)Peak memory usage: 111 MB % 9.94/2.10 % (423488)Instructions burned: 29 (million) % 9.94/2.10 % (423495)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=3572430126:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 9.94/2.10 % (423493)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=3684336821:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi) % 9.94/2.10 % (423496)Instruction limit reached! % 9.94/2.10 % (423496)------------------------------ % 9.94/2.10 % (423496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.10 % (423496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.10 % (423496)CaDiCaL version: 2.1.3 % 9.94/2.10 % (423496)Termination reason: Instruction limit % 9.94/2.10 % (423496)Termination phase: Saturation % 9.94/2.10 % (423496)Time elapsed: 0.040 s % 9.94/2.10 % (423496)Peak memory usage: 113 MB % 9.94/2.10 % (423496)Instructions burned: 130 (million) % 9.94/2.10 % (423493)Instruction limit reached! % 9.94/2.10 % (423493)------------------------------ % 9.94/2.10 % (423493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.10 % (423493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.10 % (423493)CaDiCaL version: 2.1.3 % 9.94/2.10 % (423493)Termination reason: Instruction limit % 9.94/2.10 % (423493)Termination phase: Saturation % 9.94/2.10 % (423493)Time elapsed: 0.031 s % 9.94/2.10 % (423493)Peak memory usage: 89 MB % 9.94/2.10 % (423493)Instructions burned: 77 (million) % 9.94/2.10 % (423490)Instruction limit reached! % 9.94/2.10 % (423490)------------------------------ % 9.94/2.10 % (423490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.10 % (423490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.11 % (423490)CaDiCaL version: 2.1.3 % 9.94/2.11 % (423490)Termination reason: Instruction limit % 9.94/2.11 % (423490)Termination phase: Saturation % 9.94/2.11 % (423490)Time elapsed: 0.070 s % 9.94/2.11 % (423490)Peak memory usage: 129 MB % 9.94/2.11 % (423490)Instructions burned: 71 (million) % 9.94/2.11 % (423504)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3491416443:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 9.94/2.11 % (423500)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2524343482:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 9.94/2.11 % (423504)Instruction limit reached! % 9.94/2.11 % (423504)------------------------------ % 9.94/2.11 % (423504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.11 % (423504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.11 % (423504)CaDiCaL version: 2.1.3 % 9.94/2.11 % (423504)Termination reason: Instruction limit % 9.94/2.11 % (423504)Termination phase: Property scanning % 9.94/2.11 % (423504)Time elapsed: 0.008 s % 11.14/2.36 % (423504)Peak memory usage: 86 MB % 11.14/2.36 % (423504)Instructions burned: 43 (million) % 11.14/2.36 % (423495)Instruction limit reached! % 11.14/2.36 % (423495)------------------------------ % 11.14/2.36 % (423495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.14/2.36 % (423495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/2.36 % (423495)CaDiCaL version: 2.1.3 % 11.14/2.36 % (423495)Termination reason: Instruction limit % 11.14/2.36 % (423495)Termination phase: Saturation % 11.14/2.36 % (423495)Time elapsed: 0.119 s % 11.14/2.36 % (423495)Peak memory usage: 90 MB % 11.14/2.36 % (423495)Instructions burned: 295 (million) % 11.14/2.36 % (423482)------------------------------ % 11.14/2.36 % (423482)------------------------------ % 11.14/2.36 % (423505)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=444056079:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 11.14/2.36 % (423505)Refutation not found, incomplete strategy % 11.14/2.36 % (423505)------------------------------ % 11.14/2.36 % (423505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.14/2.36 % (423505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/2.36 % (423505)CaDiCaL version: 2.1.3 % 11.14/2.36 % (423505)Termination reason: Refutation not found, incomplete strategy % 11.14/2.36 % (423505)Time elapsed: 0.028 s % 11.14/2.36 % (423505)Peak memory usage: 89 MB % 11.14/2.36 % (423505)Instructions burned: 67 (million) % 11.14/2.36 % (423506)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3372755571:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 11.14/2.36 % (423509)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2148994301:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.14/2.36 % (423500)Instruction limit reached! % 11.14/2.36 % (423500)------------------------------ % 11.14/2.36 % (423500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.14/2.36 % (423500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/2.36 % (423500)CaDiCaL version: 2.1.3 % 11.14/2.36 % (423500)Termination reason: Instruction limit % 11.14/2.36 % (423500)Termination phase: Saturation % 11.14/2.36 % (423500)Time elapsed: 0.097 s % 11.14/2.36 % (423500)Peak memory usage: 129 MB % 11.14/2.36 % (423500)Instructions burned: 132 (million) % 11.14/2.36 % (423488)------------------------------ % 11.14/2.36 % (423488)------------------------------ % 11.14/2.36 % (423509)Instruction limit reached! % 11.14/2.36 % (423509)------------------------------ % 11.14/2.36 % (423509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.14/2.36 % (423509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/2.36 % (423509)CaDiCaL version: 2.1.3 % 11.14/2.36 % (423509)Termination reason: Instruction limit % 11.14/2.36 % (423509)Termination phase: Saturation % 11.14/2.36 % (423509)Time elapsed: 0.041 s % 11.14/2.36 % (423509)Peak memory usage: 112 MB % 11.14/2.36 % (423509)Instructions burned: 134 (million) % 11.14/2.36 % (423510)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=2926172151:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 11.14/2.36 % (423510)Refutation not found, incomplete strategy % 11.14/2.36 % (423510)------------------------------ % 11.14/2.36 % (423510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.14/2.36 % (423510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/2.36 % (423510)CaDiCaL version: 2.1.3 % 11.14/2.36 % (423510)Termination reason: Refutation not found, incomplete strategy % 11.14/2.36 % (423510)Time elapsed: 0.036 s % 11.14/2.36 % (423510)Peak memory usage: 111 MB % 11.14/2.36 % (423510)Instructions burned: 31 (million) % 11.14/2.36 % (423511)dis+10_1_si=on:random_seed=1537233029:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.14/2.36 % (423518)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1849293340:i=65:nm=16:rtra=on_2989 on theBenchmark for (2989ds/65Mi) % 11.14/2.36 % (423515)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3808113777:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 11.14/2.36 % (423518)Instruction limit reached! % 11.14/2.36 % (423518)------------------------------ % 12.52/2.55 % (423518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.52/2.55 % (423518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.52/2.55 % (423518)CaDiCaL version: 2.1.3 % 12.52/2.55 % (423518)Termination reason: Instruction limit % 12.52/2.55 % (423518)Termination phase: Saturation % 12.52/2.55 % (423518)Time elapsed: 0.019 s % 12.52/2.55 % (423518)Peak memory usage: 96 MB % 12.52/2.55 % (423518)Instructions burned: 65 (million) % 12.52/2.55 % (423516)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=809145086:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi) % 12.52/2.55 % (423505)------------------------------ % 12.52/2.55 % (423505)------------------------------ % 12.52/2.55 % (423516)Instruction limit reached! % 12.52/2.55 % (423516)------------------------------ % 12.52/2.55 % (423516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.52/2.55 % (423516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.52/2.55 % (423516)CaDiCaL version: 2.1.3 % 12.52/2.55 % (423516)Termination reason: Instruction limit % 12.52/2.55 % (423516)Termination phase: Saturation % 12.52/2.55 % (423516)Time elapsed: 0.056 s % 12.52/2.55 % (423516)Peak memory usage: 89 MB % 12.52/2.55 % (423516)Instructions burned: 142 (million) % 12.52/2.55 % (423522)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3626791184:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 12.52/2.55 % (423522)Instruction limit reached! % 12.52/2.55 % (423522)------------------------------ % 12.52/2.55 % (423522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.52/2.55 % (423522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.52/2.55 % (423522)CaDiCaL version: 2.1.3 % 12.52/2.55 % (423522)Termination reason: Instruction limit % 12.52/2.55 % (423522)Termination phase: Saturation % 12.52/2.55 % (423522)Time elapsed: 0.027 s % 12.52/2.55 % (423522)Peak memory usage: 90 MB % 12.52/2.55 % (423522)Instructions burned: 123 (million) % 12.52/2.55 % (423515)Instruction limit reached! % 12.52/2.55 % (423515)------------------------------ % 12.52/2.55 % (423515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.52/2.55 % (423515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.52/2.55 % (423515)CaDiCaL version: 2.1.3 % 12.52/2.55 % (423515)Termination reason: Instruction limit % 12.52/2.55 % (423515)Termination phase: Saturation % 12.52/2.55 % (423515)Time elapsed: 0.157 s % 12.52/2.55 % (423515)Peak memory usage: 90 MB % 12.52/2.55 % (423515)Instructions burned: 392 (million) % 12.52/2.55 % (423506)Instruction limit reached! % 12.52/2.55 % (423506)------------------------------ % 12.52/2.55 % (423506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.52/2.55 % (423506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.52/2.55 % (423506)CaDiCaL version: 2.1.3 % 12.52/2.55 % (423506)Termination reason: Instruction limit % 12.52/2.55 % (423506)Termination phase: Saturation % 12.52/2.55 % (423506)Time elapsed: 0.307 s % 12.52/2.55 % (423506)Peak memory usage: 136 MB % 12.52/2.55 % (423506)Instructions burned: 599 (million) % 12.52/2.55 % (423510)------------------------------ % 12.52/2.55 % (423510)------------------------------ % 12.52/2.55 % (423527)dis+1010_1_to=kbo:si=on:random_seed=371968737:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 12.52/2.55 % (423525)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=1443576152:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 12.52/2.55 % (423526)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=103558433:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi) % 12.52/2.55 % (423526)Instruction limit reached! % 12.52/2.55 % (423526)------------------------------ % 12.52/2.55 % (423526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.52/2.55 % (423526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.52/2.55 % (423526)CaDiCaL version: 2.1.3 % 12.52/2.55 % (423526)Termination reason: Instruction limit % 12.52/2.55 % (423526)Termination phase: Saturation % 12.52/2.55 % (423526)Time elapsed: 0.016 s % 12.52/2.55 % (423526)Peak memory usage: 88 MB % 12.52/2.55 % (423526)Instructions burned: 41 (million) % 12.52/2.55 % (423527)Instruction limit reached! % 12.52/2.55 % (423527)------------------------------ % 12.52/2.55 % (423527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.51/2.81 % (423527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.51/2.81 % (423527)CaDiCaL version: 2.1.3 % 14.51/2.81 % (423527)Termination reason: Instruction limit % 14.51/2.81 % (423527)Termination phase: Saturation % 14.51/2.81 % (423527)Time elapsed: 0.039 s % 14.51/2.81 % (423527)Peak memory usage: 90 MB % 14.51/2.81 % (423527)Instructions burned: 176 (million) % 14.51/2.81 % (423528)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3301394170:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 14.51/2.81 % (423525)Refutation not found, incomplete strategy % 14.51/2.81 % (423525)------------------------------ % 14.51/2.81 % (423525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.51/2.81 % (423525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.51/2.81 % (423525)CaDiCaL version: 2.1.3 % 14.51/2.81 % (423525)Termination reason: Refutation not found, incomplete strategy % 14.51/2.81 % (423525)Time elapsed: 0.061 s % 14.51/2.81 % (423525)Peak memory usage: 114 MB % 14.51/2.81 % (423525)Instructions burned: 86 (million) % 14.51/2.81 % (423529)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=522070376:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi) % 14.51/2.81 % (423530)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=340349211:thitd=on:i=215:nm=0:rtra=on:ev=force_2986 on theBenchmark for (2986ds/215Mi) % 14.51/2.81 % (423511)Instruction limit reached! % 14.51/2.81 % (423511)------------------------------ % 14.51/2.81 % (423511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.51/2.81 % (423511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.51/2.81 % (423511)CaDiCaL version: 2.1.3 % 14.51/2.81 % (423511)Termination reason: Instruction limit % 14.51/2.81 % (423511)Termination phase: Saturation % 14.51/2.81 % (423511)Time elapsed: 0.388 s % 14.51/2.81 % (423511)Peak memory usage: 90 MB % 14.51/2.81 % (423511)Instructions burned: 1001 (million) % 14.51/2.81 % (423535)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3399578137:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi) % 14.51/2.81 % (423535)Refutation not found, incomplete strategy % 14.51/2.81 % (423535)------------------------------ % 14.51/2.81 % (423535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.51/2.81 % (423535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.51/2.81 % (423535)CaDiCaL version: 2.1.3 % 14.51/2.81 % (423535)Termination reason: Refutation not found, incomplete strategy % 14.51/2.81 % (423535)Time elapsed: 0.005 s % 14.51/2.81 % (423535)Peak memory usage: 88 MB % 14.51/2.81 % (423535)Instructions burned: 26 (million) % 14.51/2.81 % (423534)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=180081497:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 14.51/2.81 % (423528)Instruction limit reached! % 14.51/2.81 % (423528)------------------------------ % 14.51/2.81 % (423528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.51/2.81 % (423528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.51/2.81 % (423528)CaDiCaL version: 2.1.3 % 14.51/2.81 % (423528)Termination reason: Instruction limit % 14.51/2.81 % (423528)Termination phase: Saturation % 14.51/2.81 % (423528)Time elapsed: 0.156 s % 14.51/2.81 % (423528)Peak memory usage: 117 MB % 14.51/2.81 % (423528)Instructions burned: 330 (million) % 14.51/2.81 % (423530)Instruction limit reached! % 14.51/2.81 % (423530)------------------------------ % 14.51/2.81 % (423530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.51/2.81 % (423530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.51/2.81 % (423530)CaDiCaL version: 2.1.3 % 14.51/2.81 % (423530)Termination reason: Instruction limit % 14.51/2.81 % (423530)Termination phase: Saturation % 14.51/2.81 % (423530)Time elapsed: 0.130 s % 14.51/2.81 % (423530)Peak memory usage: 133 MB % 14.51/2.81 % (423530)Instructions burned: 216 (million) % 14.51/2.81 % (423539)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=702657407:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi) % 14.51/2.81 % (423535)------------------------------ % 17.01/3.04 % (423535)------------------------------ % 17.01/3.04 % (423525)------------------------------ % 17.01/3.04 % (423525)------------------------------ % 17.01/3.04 % (423529)Instruction limit reached! % 17.01/3.04 % (423529)------------------------------ % 17.01/3.04 % (423529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.04 % (423529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.04 % (423529)CaDiCaL version: 2.1.3 % 17.01/3.04 % (423529)Termination reason: Instruction limit % 17.01/3.04 % (423529)Termination phase: Saturation % 17.01/3.04 % (423529)Time elapsed: 0.243 s % 17.01/3.04 % (423529)Peak memory usage: 135 MB % 17.01/3.04 % (423529)Instructions burned: 485 (million) % 17.01/3.04 % (423534)Instruction limit reached! % 17.01/3.04 % (423534)------------------------------ % 17.01/3.04 % (423534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.04 % (423534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.04 % (423534)CaDiCaL version: 2.1.3 % 17.01/3.04 % (423534)Termination reason: Instruction limit % 17.01/3.04 % (423534)Termination phase: Saturation % 17.01/3.04 % (423534)Time elapsed: 0.169 s % 17.01/3.04 % (423534)Peak memory usage: 118 MB % 17.01/3.04 % (423534)Instructions burned: 353 (million) % 17.01/3.04 % (423543)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=605227487:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi) % 17.01/3.04 % (423542)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1721967290:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 17.01/3.04 % (423543)Refutation not found, incomplete strategy % 17.01/3.04 % (423543)------------------------------ % 17.01/3.04 % (423543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.04 % (423543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.04 % (423543)CaDiCaL version: 2.1.3 % 17.01/3.04 % (423543)Termination reason: Refutation not found, incomplete strategy % 17.01/3.04 % (423543)Time elapsed: 0.010 s % 17.01/3.04 % (423543)Peak memory usage: 87 MB % 17.01/3.04 % (423543)Instructions burned: 25 (million) % 17.01/3.04 % (423545)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=795795183:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.01/3.04 % (423545)Refutation not found, incomplete strategy % 17.01/3.04 % (423545)------------------------------ % 17.01/3.04 % (423545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.04 % (423545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.04 % (423545)CaDiCaL version: 2.1.3 % 17.01/3.04 % (423545)Termination reason: Refutation not found, incomplete strategy % 17.01/3.04 % (423545)Time elapsed: 0.021 s % 17.01/3.04 % (423545)Peak memory usage: 112 MB % 17.01/3.04 % (423545)Instructions burned: 30 (million) % 17.01/3.04 % (423539)Instruction limit reached! % 17.01/3.04 % (423539)------------------------------ % 17.01/3.04 % (423539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.04 % (423539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.04 % (423539)CaDiCaL version: 2.1.3 % 17.01/3.04 % (423539)Termination reason: Instruction limit % 17.01/3.04 % (423539)Termination phase: Saturation % 17.01/3.04 % (423539)Time elapsed: 0.163 s % 17.01/3.04 % (423539)Peak memory usage: 117 MB % 17.01/3.04 % (423539)Instructions burned: 329 (million) % 17.01/3.04 % (423546)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2734667322:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 17.01/3.04 % (423547)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=341821879:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi) % 17.01/3.04 % (423548)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=181515685:avsq=on:i=276:avsqr=1,2:rtra=on_2982 on theBenchmark for (2982ds/276Mi) % 17.01/3.04 % (423546)Refutation not found, incomplete strategy % 17.01/3.04 % (423546)------------------------------ % 17.01/3.04 % (423546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.04 % (423546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.04 % (423546)CaDiCaL version: 2.1.3 % 17.01/3.04 % (423546)Termination reason: Refutation not found, incomplete strategy % 17.85/3.37 % (423546)Time elapsed: 0.035 s % 17.85/3.37 % (423546)Peak memory usage: 111 MB % 17.85/3.37 % (423546)Instructions burned: 29 (million) % 17.85/3.37 % (423542)Instruction limit reached! % 17.85/3.37 % (423542)------------------------------ % 17.85/3.37 % (423542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.85/3.37 % (423542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/3.37 % (423542)CaDiCaL version: 2.1.3 % 17.85/3.37 % (423542)Termination reason: Instruction limit % 17.85/3.37 % (423542)Termination phase: Saturation % 17.85/3.37 % (423542)Time elapsed: 0.146 s % 17.85/3.37 % (423542)Peak memory usage: 118 MB % 17.85/3.37 % (423542)Instructions burned: 281 (million) % 17.85/3.37 % (423545)------------------------------ % 17.85/3.37 % (423545)------------------------------ % 17.85/3.37 % (423552)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=463955210:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi) % 17.85/3.37 % (423543)------------------------------ % 17.85/3.37 % (423543)------------------------------ % 17.85/3.37 % (423556)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=236870056:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 17.85/3.37 % (423548)Instruction limit reached! % 17.85/3.37 % (423548)------------------------------ % 17.85/3.37 % (423548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.85/3.37 % (423548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/3.37 % (423548)CaDiCaL version: 2.1.3 % 17.85/3.37 % (423548)Termination reason: Instruction limit % 17.85/3.37 % (423548)Termination phase: Saturation % 17.85/3.37 % (423548)Time elapsed: 0.161 s % 17.85/3.37 % (423548)Peak memory usage: 134 MB % 17.85/3.37 % (423548)Instructions burned: 276 (million) % 17.85/3.37 % (423558)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3477223008:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2980 on theBenchmark for (2980ds/513Mi) % 17.85/3.37 % (423556)Refutation not found, incomplete strategy % 17.85/3.37 % (423556)------------------------------ % 17.85/3.37 % (423556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.85/3.37 % (423556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/3.37 % (423556)CaDiCaL version: 2.1.3 % 17.85/3.37 % (423556)Termination reason: Refutation not found, incomplete strategy % 17.85/3.37 % (423556)Time elapsed: 0.036 s % 17.85/3.37 % (423556)Peak memory usage: 111 MB % 17.85/3.37 % (423556)Instructions burned: 31 (million) % 17.85/3.37 % (423547)Instruction limit reached! % 17.85/3.37 % (423547)------------------------------ % 17.85/3.37 % (423547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.85/3.37 % (423547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/3.37 % (423547)CaDiCaL version: 2.1.3 % 17.85/3.37 % (423547)Termination reason: Instruction limit % 17.85/3.37 % (423547)Termination phase: Saturation % 17.85/3.37 % (423547)Time elapsed: 0.210 s % 17.85/3.37 % (423547)Peak memory usage: 112 MB % 17.85/3.37 % (423547)Instructions burned: 471 (million) % 17.85/3.37 % (423546)------------------------------ % 17.85/3.37 % (423546)------------------------------ % 17.85/3.37 % (423552)Instruction limit reached! % 17.85/3.37 % (423552)------------------------------ % 17.85/3.37 % (423552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.85/3.37 % (423552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/3.37 % (423552)CaDiCaL version: 2.1.3 % 17.85/3.37 % (423552)Termination reason: Instruction limit % 17.85/3.37 % (423552)Termination phase: Saturation % 17.85/3.37 % (423552)Time elapsed: 0.176 s % 17.85/3.37 % (423552)Peak memory usage: 117 MB % 17.85/3.37 % (423552)Instructions burned: 377 (million) % 17.85/3.37 % (423559)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1031336279:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi) % 17.85/3.37 % (423558)Instruction limit reached! % 17.85/3.37 % (423558)------------------------------ % 17.85/3.37 % (423558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.85/3.37 % (423558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.85/3.37 % (423558)CaDiCaL version: 2.1.3 % 17.85/3.37 % (423558)Termination reason: Instruction limit % 17.85/3.37 % (423558)Termination phase: Saturation % 21.06/3.72 % (423558)Time elapsed: 0.104 s % 21.06/3.72 % (423558)Peak memory usage: 89 MB % 21.06/3.72 % (423558)Instructions burned: 514 (million) % 21.06/3.72 % (423562)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=354867798:i=359:rtra=on:gtg=exists_top:ss=axioms_2979 on theBenchmark for (2979ds/359Mi) % 21.06/3.72 % (423562)Refutation not found, incomplete strategy % 21.06/3.72 % (423562)------------------------------ % 21.06/3.72 % (423562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.06/3.72 % (423562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.72 % (423562)CaDiCaL version: 2.1.3 % 21.06/3.72 % (423562)Termination reason: Refutation not found, incomplete strategy % 21.06/3.72 % (423562)Time elapsed: 0.013 s % 21.06/3.72 % (423562)Peak memory usage: 88 MB % 21.06/3.72 % (423562)Instructions burned: 32 (million) % 21.06/3.72 % (423563)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=784043325:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2979 on theBenchmark for (2979ds/341Mi) % 21.06/3.72 % (423567)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=598446659:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2978 on theBenchmark for (2978ds/273Mi) % 21.06/3.72 % (423564)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2691451978:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi) % 21.06/3.72 % (423566)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=1645245228:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2978 on theBenchmark for (2978ds/235Mi) % 21.06/3.72 % (423564)Refutation not found, incomplete strategy % 21.06/3.72 % (423564)------------------------------ % 21.06/3.72 % (423564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.06/3.72 % (423564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.72 % (423564)CaDiCaL version: 2.1.3 % 21.06/3.72 % (423564)Termination reason: Refutation not found, incomplete strategy % 21.06/3.72 % (423564)Time elapsed: 0.032 s % 21.06/3.72 % (423564)Peak memory usage: 111 MB % 21.06/3.72 % (423564)Instructions burned: 25 (million) % 21.06/3.72 % (423567)Instruction limit reached! % 21.06/3.72 % (423567)------------------------------ % 21.06/3.72 % (423567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.06/3.72 % (423567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.72 % (423567)CaDiCaL version: 2.1.3 % 21.06/3.72 % (423567)Termination reason: Instruction limit % 21.06/3.72 % (423567)Termination phase: Saturation % 21.06/3.72 % (423567)Time elapsed: 0.059 s % 21.06/3.72 % (423567)Peak memory usage: 91 MB % 21.06/3.72 % (423567)Instructions burned: 275 (million) % 21.06/3.72 % (423566)Refutation not found, incomplete strategy % 21.06/3.72 % (423566)------------------------------ % 21.06/3.72 % (423566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.06/3.72 % (423566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.72 % (423566)CaDiCaL version: 2.1.3 % 21.06/3.72 % (423566)Termination reason: Refutation not found, incomplete strategy % 21.06/3.72 % (423566)Time elapsed: 0.035 s % 21.06/3.72 % (423566)Peak memory usage: 111 MB % 21.06/3.72 % (423566)Instructions burned: 31 (million) % 21.06/3.72 % (423556)------------------------------ % 21.06/3.72 % (423556)------------------------------ % 21.06/3.72 % (423559)Instruction limit reached! % 21.06/3.72 % (423559)------------------------------ % 21.06/3.72 % (423559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.06/3.72 % (423559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.72 % (423559)CaDiCaL version: 2.1.3 % 21.06/3.72 % (423559)Termination reason: Instruction limit % 21.06/3.72 % (423559)Termination phase: Saturation % 21.06/3.72 % (423559)Time elapsed: 0.196 s % 21.06/3.72 % (423559)Peak memory usage: 135 MB % 21.06/3.72 % (423559)Instructions burned: 342 (million) % 21.06/3.72 % (423563)Instruction limit reached! % 21.06/3.72 % (423563)------------------------------ % 21.06/3.72 % (423563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.06/3.72 % (423563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.72 % (423563)CaDiCaL version: 2.1.3 % 24.20/4.14 % (423563)Termination reason: Instruction limit % 24.20/4.14 % (423563)Termination phase: Saturation % 24.20/4.14 % (423563)Time elapsed: 0.161 s % 24.20/4.14 % (423563)Peak memory usage: 117 MB % 24.20/4.14 % (423563)Instructions burned: 343 (million) % 24.20/4.14 % (423573)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2145741679:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi) % 24.20/4.14 % (423573)Instruction limit reached! % 24.20/4.14 % (423573)------------------------------ % 24.20/4.14 % (423573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.20/4.14 % (423573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.20/4.14 % (423573)CaDiCaL version: 2.1.3 % 24.20/4.14 % (423573)Termination reason: Instruction limit % 24.20/4.14 % (423573)Termination phase: Saturation % 24.20/4.14 % (423573)Time elapsed: 0.030 s % 24.20/4.14 % (423573)Peak memory usage: 89 MB % 24.20/4.14 % (423573)Instructions burned: 147 (million) % 24.20/4.14 % (423562)------------------------------ % 24.20/4.14 % (423562)------------------------------ % 24.20/4.14 % (423574)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1063517663:i=4428:doe=on:fsr=off:rtra=on_2976 on theBenchmark for (2976ds/4428Mi) % 24.20/4.14 % (423575)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=553209236:avsq=on:i=276:avsqr=1,2:rtra=on_2976 on theBenchmark for (2976ds/276Mi) % 24.20/4.14 % (423578)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2613386679:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2975 on theBenchmark for (2975ds/655Mi) % 24.20/4.14 % (423577)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=28146527:i=1052:rtra=on_2976 on theBenchmark for (2976ds/1052Mi) % 24.20/4.14 % (423564)------------------------------ % 24.20/4.14 % (423564)------------------------------ % 24.20/4.14 % (423566)------------------------------ % 24.20/4.14 % (423566)------------------------------ % 24.20/4.14 % (423579)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=871339449:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/1054Mi) % 24.20/4.14 % (423579)Refutation not found, incomplete strategy % 24.20/4.14 % (423579)------------------------------ % 24.20/4.14 % (423579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.20/4.14 % (423579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.20/4.14 % (423579)CaDiCaL version: 2.1.3 % 24.20/4.14 % (423579)Termination reason: Refutation not found, incomplete strategy % 24.20/4.14 % (423579)Time elapsed: 0.007 s % 24.20/4.14 % (423579)Peak memory usage: 87 MB % 24.20/4.14 % (423579)Instructions burned: 18 (million) % 24.20/4.14 % (423575)Instruction limit reached! % 24.20/4.14 % (423575)------------------------------ % 24.20/4.14 % (423575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.20/4.14 % (423575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.20/4.14 % (423575)CaDiCaL version: 2.1.3 % 24.20/4.14 % (423575)Termination reason: Instruction limit % 24.20/4.14 % (423575)Termination phase: Saturation % 24.20/4.14 % (423575)Time elapsed: 0.162 s % 24.20/4.14 % (423575)Peak memory usage: 135 MB % 24.20/4.14 % (423575)Instructions burned: 278 (million) % 24.20/4.14 % (423584)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3847655397:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi) % 24.20/4.14 % (423585)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2406499167:s2a=on:i=450:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/450Mi) % 24.20/4.14 % (423578)Refutation not found, incomplete strategy % 24.20/4.14 % (423578)------------------------------ % 24.20/4.14 % (423578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.20/4.14 % (423578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.20/4.14 % (423578)CaDiCaL version: 2.1.3 % 24.20/4.14 % (423578)Termination reason: Refutation not found, incomplete strategy % 24.20/4.14 % (423578)Time elapsed: 0.182 s % 24.20/4.14 % (423578)Peak memory usage: 97 MB % 24.20/4.14 % (423578)Instructions burned: 533 (million) % 24.20/4.14 % (423584)Refutation not found, incomplete strategy % 24.20/4.14 % (423584)------------------------------ % 24.20/4.14 % (423584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.00/4.42 % (423584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.00/4.42 % (423584)CaDiCaL version: 2.1.3 % 26.00/4.42 % (423584)Termination reason: Refutation not found, incomplete strategy % 26.00/4.42 % (423584)Time elapsed: 0.056 s % 26.00/4.42 % (423584)Peak memory usage: 113 MB % 26.00/4.42 % (423584)Instructions burned: 77 (million) % 26.00/4.42 % (423587)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.00/4.42 % (423587)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1482327166:i=1090:aac=none:nm=0:rtra=on:rawr=on_2973 on theBenchmark for (2973ds/1090Mi) % 26.00/4.42 % (423579)------------------------------ % 26.00/4.42 % (423579)------------------------------ % 26.00/4.42 % (423578)------------------------------ % 26.00/4.42 % (423578)------------------------------ % 26.00/4.42 % (423577)Instruction limit reached! % 26.00/4.42 % (423577)------------------------------ % 26.00/4.42 % (423577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.00/4.42 % (423577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.00/4.42 % (423577)CaDiCaL version: 2.1.3 % 26.00/4.42 % (423577)Termination reason: Instruction limit % 26.00/4.42 % (423577)Termination phase: Saturation % 26.00/4.42 % (423577)Time elapsed: 0.397 s % 26.00/4.42 % (423577)Peak memory usage: 90 MB % 26.00/4.42 % (423577)Instructions burned: 1052 (million) % 26.00/4.42 % (423585)Instruction limit reached! % 26.00/4.42 % (423585)------------------------------ % 26.00/4.42 % (423585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.00/4.42 % (423585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.00/4.42 % (423585)CaDiCaL version: 2.1.3 % 26.00/4.42 % (423585)Termination reason: Instruction limit % 26.00/4.42 % (423585)Termination phase: Saturation % 26.00/4.42 % (423585)Time elapsed: 0.230 s % 26.00/4.42 % (423585)Peak memory usage: 135 MB % 26.00/4.42 % (423585)Instructions burned: 451 (million) % 26.00/4.42 % (423592)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1547678144:i=312:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/312Mi) % 26.00/4.42 % (423591)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1925815861:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2971 on theBenchmark for (2971ds/130Mi) % 26.00/4.42 % (423584)------------------------------ % 26.00/4.42 % (423584)------------------------------ % 26.00/4.42 % (423591)Instruction limit reached! % 26.00/4.42 % (423591)------------------------------ % 26.00/4.42 % (423591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.00/4.42 % (423591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.00/4.42 % (423591)CaDiCaL version: 2.1.3 % 26.00/4.42 % (423591)Termination reason: Instruction limit % 26.00/4.42 % (423591)Termination phase: Saturation % 26.00/4.42 % (423591)Time elapsed: 0.072 s % 26.00/4.42 % (423591)Peak memory usage: 113 MB % 26.00/4.42 % (423591)Instructions burned: 131 (million) % 26.00/4.42 % (423592)Instruction limit reached! % 26.00/4.42 % (423592)------------------------------ % 26.00/4.42 % (423592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.00/4.42 % (423592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.00/4.42 % (423592)CaDiCaL version: 2.1.3 % 26.00/4.42 % (423592)Termination reason: Instruction limit % 26.00/4.42 % (423592)Termination phase: Saturation % 26.00/4.42 % (423592)Time elapsed: 0.084 s % 26.00/4.42 % (423592)Peak memory usage: 117 MB % 26.00/4.42 % (423592)Instructions burned: 316 (million) % 26.00/4.42 % (423593)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2447021832:i=491:doe=on:rtra=on:gtg=position_2970 on theBenchmark for (2970ds/491Mi) % 26.00/4.42 % (423594)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1506160820:s2a=on:i=835:s2at=2:rtra=on_2970 on theBenchmark for (2970ds/835Mi) % 26.00/4.42 % (423593)Refutation not found, incomplete strategy % 26.00/4.42 % (423593)------------------------------ % 26.00/4.42 % (423593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.00/4.42 % (423593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.00/4.42 % (423593)CaDiCaL version: 2.1.3 % 26.00/4.42 % (423593)Termination reason: Refutation not found, incomplete strategy % 27.78/4.87 % (423593)Time elapsed: 0.036 s % 27.78/4.87 % (423593)Peak memory usage: 90 MB % 27.78/4.87 % (423593)Instructions burned: 85 (million) % 27.78/4.87 % (423597)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2333528671:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2970 on theBenchmark for (2970ds/307Mi) % 27.78/4.87 % (423599)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1879213357:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2969 on theBenchmark for (2969ds/646Mi) % 27.78/4.87 % (423597)Refutation not found, incomplete strategy % 27.78/4.87 % (423597)------------------------------ % 27.78/4.87 % (423597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.78/4.87 % (423597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.78/4.87 % (423597)CaDiCaL version: 2.1.3 % 27.78/4.87 % (423597)Termination reason: Refutation not found, incomplete strategy % 27.78/4.87 % (423597)Time elapsed: 0.042 s % 27.78/4.87 % (423597)Peak memory usage: 91 MB % 27.78/4.87 % (423597)Instructions burned: 99 (million) % 27.78/4.87 % (423598)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=905952266:i=776:doe=on:rtra=on_2969 on theBenchmark for (2969ds/776Mi) % 27.78/4.87 % (423587)Instruction limit reached! % 27.78/4.87 % (423587)------------------------------ % 27.78/4.87 % (423587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.78/4.87 % (423587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.78/4.87 % (423587)CaDiCaL version: 2.1.3 % 27.78/4.87 % (423587)Termination reason: Instruction limit % 27.78/4.87 % (423587)Termination phase: Saturation % 27.78/4.87 % (423587)Time elapsed: 0.455 s % 27.78/4.87 % (423587)Peak memory usage: 118 MB % 27.78/4.87 % (423587)Instructions burned: 1091 (million) % 27.78/4.87 % (423599)Instruction limit reached! % 27.78/4.87 % (423599)------------------------------ % 27.78/4.87 % (423599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.78/4.87 % (423599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.78/4.87 % (423599)CaDiCaL version: 2.1.3 % 27.78/4.87 % (423599)Termination reason: Instruction limit % 27.78/4.87 % (423599)Termination phase: Saturation % 27.78/4.87 % (423599)Time elapsed: 0.167 s % 27.78/4.87 % (423599)Peak memory usage: 136 MB % 27.78/4.87 % (423599)Instructions burned: 649 (million) % 27.78/4.87 % (423593)------------------------------ % 27.78/4.87 % (423593)------------------------------ % 27.78/4.87 % (423605)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=3711654096:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2967 on theBenchmark for (2967ds/784Mi) % 27.78/4.87 % (423606)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=1293262781:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2967 on theBenchmark for (2967ds/1131Mi) % 27.78/4.87 % (423597)------------------------------ % 27.78/4.87 % (423597)------------------------------ % 27.78/4.87 % (423594)Instruction limit reached! % 27.78/4.87 % (423594)------------------------------ % 27.78/4.87 % (423594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.78/4.87 % (423594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.78/4.87 % (423594)CaDiCaL version: 2.1.3 % 27.78/4.87 % (423594)Termination reason: Instruction limit % 27.78/4.87 % (423594)Termination phase: Saturation % 27.78/4.87 % (423594)Time elapsed: 0.324 s % 27.78/4.87 % (423594)Peak memory usage: 89 MB % 27.78/4.87 % (423594)Instructions burned: 836 (million) % 27.78/4.87 % (423607)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=3797404283:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2966 on theBenchmark for (2966ds/246Mi) % 27.78/4.87 % (423598)Instruction limit reached! % 27.78/4.87 % (423598)------------------------------ % 27.78/4.87 % (423598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.78/4.87 % (423598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.78/4.87 % (423598)CaDiCaL version: 2.1.3 % 27.78/4.87 % (423598)Termination reason: Instruction limit % 27.78/4.87 % (423598)Termination phase: Saturation % 27.78/4.87 % (423598)Time elapsed: 0.317 s % 27.78/4.87 % (423598)Peak memory usage: 114 MB % 27.78/4.87 % (423598)Instructions burned: 778 (million) % 27.78/4.87 % (423607)Refutation not found, incomplete strategy % 35.69/5.73 % (423607)------------------------------ % 35.69/5.73 % (423607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.69/5.73 % (423607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.73 % (423607)CaDiCaL version: 2.1.3 % 35.69/5.73 % (423607)Termination reason: Refutation not found, incomplete strategy % 35.69/5.73 % (423607)Time elapsed: 0.036 s % 35.69/5.73 % (423607)Peak memory usage: 111 MB % 35.69/5.73 % (423607)Instructions burned: 31 (million) % 35.69/5.73 % (423611)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=283152884:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2966 on theBenchmark for (2966ds/273Mi) % 35.69/5.73 % (423610)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1145735784:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2966 on theBenchmark for (2966ds/775Mi) % 35.69/5.73 % (423610)Refutation not found, incomplete strategy % 35.69/5.73 % (423610)------------------------------ % 35.69/5.73 % (423610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.69/5.73 % (423610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.73 % (423610)CaDiCaL version: 2.1.3 % 35.69/5.73 % (423610)Termination reason: Refutation not found, incomplete strategy % 35.69/5.73 % (423610)Time elapsed: 0.011 s % 35.69/5.73 % (423610)Peak memory usage: 88 MB % 35.69/5.73 % (423610)Instructions burned: 27 (million) % 35.69/5.73 % (423613)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2098451032:i=102:nm=16:rtra=on_2965 on theBenchmark for (2965ds/102Mi) % 35.69/5.73 % (423606)Instruction limit reached! % 35.69/5.73 % (423606)------------------------------ % 35.69/5.73 % (423606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.69/5.73 % (423606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.73 % (423606)CaDiCaL version: 2.1.3 % 35.69/5.73 % (423606)Termination reason: Instruction limit % 35.69/5.73 % (423606)Termination phase: Saturation % 35.69/5.73 % (423606)Time elapsed: 0.247 s % 35.69/5.73 % (423606)Peak memory usage: 114 MB % 35.69/5.73 % (423606)Instructions burned: 1131 (million) % 35.69/5.73 % (423611)Instruction limit reached! % 35.69/5.73 % (423611)------------------------------ % 35.69/5.73 % (423611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.69/5.73 % (423611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.73 % (423611)CaDiCaL version: 2.1.3 % 35.69/5.73 % (423611)Termination reason: Instruction limit % 35.69/5.73 % (423611)Termination phase: Saturation % 35.69/5.73 % (423611)Time elapsed: 0.113 s % 35.69/5.73 % (423611)Peak memory usage: 90 MB % 35.69/5.73 % (423611)Instructions burned: 281 (million) % 35.69/5.73 % (423613)Instruction limit reached! % 35.69/5.73 % (423613)------------------------------ % 35.69/5.73 % (423613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.69/5.73 % (423613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.73 % (423613)CaDiCaL version: 2.1.3 % 35.69/5.73 % (423613)Termination reason: Instruction limit % 35.69/5.73 % (423613)Termination phase: Saturation % 35.69/5.73 % (423613)Time elapsed: 0.044 s % 35.69/5.73 % (423613)Peak memory usage: 90 MB % 35.69/5.73 % (423613)Instructions burned: 102 (million) % 35.69/5.73 % (423605)Instruction limit reached! % 35.69/5.73 % (423605)------------------------------ % 35.69/5.73 % (423605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.69/5.73 % (423605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.73 % (423605)CaDiCaL version: 2.1.3 % 35.69/5.73 % (423605)Termination reason: Instruction limit % 35.69/5.73 % (423605)Termination phase: Saturation % 35.69/5.73 % (423605)Time elapsed: 0.322 s % 35.69/5.73 % (423605)Peak memory usage: 113 MB % 35.69/5.73 % (423605)Instructions burned: 787 (million) % 35.69/5.73 % (423617)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=837468233:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2963 on theBenchmark for (2963ds/1094Mi) % 35.69/5.73 % (423607)------------------------------ % 35.69/5.73 % (423607)------------------------------ % 35.69/5.73 % (423618)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1533801987:i=6400:doe=on:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/6400Mi) % 35.69/5.73 % (423610)------------------------------ % 35.69/5.73 % (423610)------------------------------ % 43.25/6.92 % (423619)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=3305384048:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2963 on theBenchmark for (2963ds/868Mi) % 43.25/6.92 % (423620)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=992828818:i=1846:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/1846Mi) % 43.25/6.92 % (423620)Refutation not found, incomplete strategy % 43.25/6.92 % (423620)------------------------------ % 43.25/6.92 % (423620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.25/6.92 % (423620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.25/6.92 % (423620)CaDiCaL version: 2.1.3 % 43.25/6.92 % (423620)Termination reason: Refutation not found, incomplete strategy % 43.25/6.92 % (423620)Time elapsed: 0.022 s % 43.25/6.92 % (423620)Peak memory usage: 89 MB % 43.25/6.92 % (423620)Instructions burned: 54 (million) % 43.25/6.92 % (423623)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1983140110:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2962 on theBenchmark for (2962ds/36816Mi) % 43.25/6.92 % (423625)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3619923296:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 43.25/6.92 % (423617)Instruction limit reached! % 43.25/6.92 % (423617)------------------------------ % 43.25/6.92 % (423617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.25/6.92 % (423617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.25/6.92 % (423617)CaDiCaL version: 2.1.3 % 43.25/6.92 % (423617)Termination reason: Instruction limit % 43.25/6.92 % (423617)Termination phase: Saturation % 43.25/6.92 % (423617)Time elapsed: 0.219 s % 43.25/6.92 % (423617)Peak memory usage: 91 MB % 43.25/6.92 % (423617)Instructions burned: 1100 (million) % 43.25/6.92 % (423629)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=1848657400:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/863Mi) % 43.25/6.93 % (423625)Instruction limit reached! % 43.25/6.93 % (423625)------------------------------ % 43.25/6.93 % (423625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.25/6.93 % (423625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.25/6.93 % (423625)CaDiCaL version: 2.1.3 % 43.25/6.93 % (423625)Termination reason: Instruction limit % 43.25/6.93 % (423625)Termination phase: Saturation % 43.25/6.93 % (423625)Time elapsed: 0.114 s % 43.25/6.93 % (423625)Peak memory usage: 91 MB % 43.25/6.93 % (423625)Instructions burned: 276 (million) % 43.25/6.93 % (423620)------------------------------ % 43.25/6.93 % (423620)------------------------------ % 43.25/6.93 % (423631)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1064903118:i=5811:kws=precedence:nm=0:rtra=on_2959 on theBenchmark for (2959ds/5811Mi) % 43.25/6.93 % (423574)Instruction limit reached! % 43.25/6.93 % (423574)------------------------------ % 43.25/6.93 % (423574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.25/6.93 % (423574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.25/6.93 % (423574)CaDiCaL version: 2.1.3 % 43.25/6.93 % (423574)Termination reason: Instruction limit % 43.25/6.93 % (423574)Termination phase: Saturation % 43.25/6.93 % (423574)Time elapsed: 1.731 s % 43.25/6.93 % (423574)Peak memory usage: 91 MB % 43.25/6.93 % (423574)Instructions burned: 4430 (million) % 43.25/6.93 % (423619)Instruction limit reached! % 43.25/6.93 % (423619)------------------------------ % 43.25/6.93 % (423619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.25/6.93 % (423619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.25/6.93 % (423619)CaDiCaL version: 2.1.3 % 43.25/6.93 % (423619)Termination reason: Instruction limit % 43.25/6.93 % (423619)Termination phase: Saturation % 43.25/6.93 % (423619)Time elapsed: 0.408 s % 43.25/6.93 % (423619)Peak memory usage: 129 MB % 43.25/6.93 % (423619)Instructions burned: 868 (million) % 43.25/6.93 % (423632)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=3573069773:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2959 on theBenchmark for (2959ds/2216Mi) % 47.18/7.45 % (423629)Instruction limit reached! % 47.18/7.45 % (423629)------------------------------ % 47.18/7.45 % (423629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.18/7.45 % (423629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.45 % (423629)CaDiCaL version: 2.1.3 % 47.18/7.45 % (423629)Termination reason: Instruction limit % 47.18/7.45 % (423629)Termination phase: Saturation % 47.18/7.45 % (423629)Time elapsed: 0.221 s % 47.18/7.45 % (423629)Peak memory usage: 129 MB % 47.18/7.45 % (423629)Instructions burned: 864 (million) % 47.18/7.45 % (423634)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=176324718:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/801Mi) % 47.18/7.45 % (423637)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4017274800:i=3509:rtra=on_2957 on theBenchmark for (2957ds/3509Mi) % 47.18/7.45 % (423635)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=62561475:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2958 on theBenchmark for (2958ds/1026Mi) % 47.18/7.45 % (423635)Refutation not found, incomplete strategy % 47.18/7.45 % (423635)------------------------------ % 47.18/7.45 % (423635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.18/7.45 % (423635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.45 % (423635)CaDiCaL version: 2.1.3 % 47.18/7.45 % (423635)Termination reason: Refutation not found, incomplete strategy % 47.18/7.45 % (423635)Time elapsed: 0.007 s % 47.18/7.45 % (423635)Peak memory usage: 87 MB % 47.18/7.45 % (423635)Instructions burned: 18 (million) % 47.18/7.45 % (423635)------------------------------ % 47.18/7.45 % (423635)------------------------------ % 47.18/7.45 % (423634)Refutation not found, incomplete strategy % 47.18/7.45 % (423634)------------------------------ % 47.18/7.45 % (423634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.18/7.45 % (423634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.45 % (423634)CaDiCaL version: 2.1.3 % 47.18/7.45 % (423634)Termination reason: Refutation not found, incomplete strategy % 47.18/7.45 % (423634)Time elapsed: 0.350 s % 47.18/7.45 % (423634)Peak memory usage: 97 MB % 47.18/7.45 % (423634)Instructions burned: 564 (million) % 47.18/7.45 % (423641)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2182316948:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2954 on theBenchmark for (2954ds/2127Mi) % 47.18/7.45 % (423641)Refutation not found, incomplete strategy % 47.18/7.45 % (423641)------------------------------ % 47.18/7.45 % (423641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.18/7.45 % (423641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.45 % (423641)CaDiCaL version: 2.1.3 % 47.18/7.45 % (423641)Termination reason: Refutation not found, incomplete strategy % 47.18/7.45 % (423641)Time elapsed: 0.010 s % 47.18/7.45 % (423641)Peak memory usage: 88 MB % 47.18/7.45 % (423641)Instructions burned: 26 (million) % 47.18/7.45 % (423634)------------------------------ % 47.18/7.45 % (423634)------------------------------ % 47.18/7.45 % (423641)------------------------------ % 47.18/7.45 % (423641)------------------------------ % 47.18/7.45 % (423637)Instruction limit reached! % 47.18/7.45 % (423637)------------------------------ % 47.18/7.45 % (423637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.18/7.45 % (423637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.45 % (423637)CaDiCaL version: 2.1.3 % 47.18/7.45 % (423637)Termination reason: Instruction limit % 47.18/7.45 % (423637)Termination phase: Saturation % 47.18/7.45 % (423637)Time elapsed: 0.706 s % 47.18/7.45 % (423637)Peak memory usage: 90 MB % 47.18/7.45 % (423637)Instructions burned: 3511 (million) % 47.18/7.45 % (423643)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3378094479:i=1959:rtra=on:fsd=on:proc=on_2951 on theBenchmark for (2951ds/1959Mi) % 47.18/7.45 % (423632)Instruction limit reached! % 47.18/7.45 % (423632)------------------------------ % 47.18/7.45 % (423632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.18/7.45 % (423632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.45 % (423632)CaDiCaL version: 2.1.3 % 47.18/7.45 % (423632)Termination reason: Instruction limit % 47.18/7.45 % (423632)Termination phase: Saturation % 64.87/10.00 % (423632)Time elapsed: 0.854 s % 64.87/10.00 % (423632)Peak memory usage: 119 MB % 64.87/10.00 % (423632)Instructions burned: 2216 (million) % 64.87/10.00 % (423644)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=936471048:s2a=on:i=3553:nm=0:rtra=on_2950 on theBenchmark for (2950ds/3553Mi) % 64.87/10.00 % (423645)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=30854874:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/3201Mi) % 64.87/10.00 % (423645)Refutation not found, incomplete strategy % 64.87/10.00 % (423645)------------------------------ % 64.87/10.00 % (423645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.87/10.00 % (423645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/10.00 % (423645)CaDiCaL version: 2.1.3 % 64.87/10.00 % (423645)Termination reason: Refutation not found, incomplete strategy % 64.87/10.00 % (423645)Time elapsed: 0.066 s % 64.87/10.00 % (423645)Peak memory usage: 92 MB % 64.87/10.00 % (423645)Instructions burned: 312 (million) % 64.87/10.00 % (423648)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=79445906:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2949 on theBenchmark for (2949ds/4093Mi) % 64.87/10.00 % (423645)------------------------------ % 64.87/10.00 % (423645)------------------------------ % 64.87/10.00 % (423651)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=1177608314:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2946 on theBenchmark for (2946ds/21173Mi) % 64.87/10.00 % (423651)Refutation not found, incomplete strategy % 64.87/10.00 % (423651)------------------------------ % 64.87/10.00 % (423651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.87/10.00 % (423651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/10.00 % (423651)CaDiCaL version: 2.1.3 % 64.87/10.00 % (423651)Termination reason: Refutation not found, incomplete strategy % 64.87/10.00 % (423651)Time elapsed: 0.018 s % 64.87/10.00 % (423651)Peak memory usage: 112 MB % 64.87/10.00 % (423651)Instructions burned: 15 (million) % 64.87/10.00 % (423651)------------------------------ % 64.87/10.00 % (423651)------------------------------ % 64.87/10.00 % (423653)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4285046322:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2944 on theBenchmark for (2944ds/10544Mi) % 64.87/10.00 % (423643)Instruction limit reached! % 64.87/10.00 % (423643)------------------------------ % 64.87/10.00 % (423643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.87/10.00 % (423643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/10.00 % (423643)CaDiCaL version: 2.1.3 % 64.87/10.00 % (423643)Termination reason: Instruction limit % 64.87/10.00 % (423643)Termination phase: Saturation % 64.87/10.00 % (423643)Time elapsed: 0.793 s % 64.87/10.00 % (423643)Peak memory usage: 119 MB % 64.87/10.00 % (423643)Instructions burned: 1961 (million) % 64.87/10.00 % (423655)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=859467397:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2941 on theBenchmark for (2941ds/1262Mi) % 64.87/10.00 % (423618)Instruction limit reached! % 64.87/10.00 % (423618)------------------------------ % 64.87/10.00 % (423618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.87/10.00 % (423618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/10.00 % (423618)CaDiCaL version: 2.1.3 % 64.87/10.00 % (423618)Termination reason: Instruction limit % 64.87/10.00 % (423618)Termination phase: Saturation % 64.87/10.00 % (423618)Time elapsed: 2.396 s % 64.87/10.00 % (423618)Peak memory usage: 92 MB % 64.87/10.00 % (423618)Instructions burned: 6402 (million) % 64.87/10.00 % (423657)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3588292832:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2938 on theBenchmark for (2938ds/775Mi) % 64.87/10.00 % (423657)Refutation not found, incomplete strategy % 64.87/10.00 % (423657)------------------------------ % 64.87/10.00 % (423657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.87/10.00 % (423657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.87/10.00 % (423657)CaDiCaL version: 2.1.3 % 74.41/11.15 % (423657)Termination reason: Refutation not found, incomplete strategy % 74.41/11.15 % (423657)Time elapsed: 0.011 s % 74.41/11.15 % (423657)Peak memory usage: 88 MB % 74.41/11.15 % (423657)Instructions burned: 27 (million) % 74.41/11.15 % (423644)Instruction limit reached! % 74.41/11.15 % (423644)------------------------------ % 74.41/11.15 % (423644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.15 % (423644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.15 % (423644)CaDiCaL version: 2.1.3 % 74.41/11.15 % (423644)Termination reason: Instruction limit % 74.41/11.15 % (423644)Termination phase: Saturation % 74.41/11.15 % (423644)Time elapsed: 1.313 s % 74.41/11.15 % (423644)Peak memory usage: 92 MB % 74.41/11.15 % (423644)Instructions burned: 3555 (million) % 74.41/11.15 % (423655)Instruction limit reached! % 74.41/11.15 % (423655)------------------------------ % 74.41/11.15 % (423655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.15 % (423655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.15 % (423655)CaDiCaL version: 2.1.3 % 74.41/11.15 % (423655)Termination reason: Instruction limit % 74.41/11.15 % (423655)Termination phase: Saturation % 74.41/11.15 % (423655)Time elapsed: 0.496 s % 74.41/11.15 % (423655)Peak memory usage: 118 MB % 74.41/11.15 % (423655)Instructions burned: 1263 (million) % 74.41/11.15 % (423631)Instruction limit reached! % 74.41/11.15 % (423631)------------------------------ % 74.41/11.15 % (423631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.15 % (423631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.15 % (423631)CaDiCaL version: 2.1.3 % 74.41/11.15 % (423631)Termination reason: Instruction limit % 74.41/11.15 % (423631)Termination phase: Saturation % 74.41/11.15 % (423631)Time elapsed: 2.352 s % 74.41/11.15 % (423631)Peak memory usage: 119 MB % 74.41/11.15 % (423631)Instructions burned: 5813 (million) % 74.41/11.15 % (423657)------------------------------ % 74.41/11.15 % (423657)------------------------------ % 74.41/11.15 % (423659)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3421229169:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2936 on theBenchmark for (2936ds/270Mi) % 74.41/11.15 % (423660)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=4075841381:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2935 on theBenchmark for (2935ds/17165Mi) % 74.41/11.15 % (423662)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=4167796299:st=2:i=12633:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/12633Mi) % 74.41/11.15 % (423661)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2354574703:s2a=on:i=13094:s2at=-1:rtra=on_2934 on theBenchmark for (2934ds/13094Mi) % 74.41/11.15 % (423662)Refutation not found, incomplete strategy % 74.41/11.15 % (423662)------------------------------ % 74.41/11.15 % (423662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.15 % (423659)Instruction limit reached! % 74.41/11.15 % (423659)------------------------------ % 74.41/11.15 % (423659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.15 % (423662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.15 % (423659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.15 % (423662)CaDiCaL version: 2.1.3 % 74.41/11.15 % (423662)Termination reason: Refutation not found, incomplete strategy % 74.41/11.15 % (423662)Time elapsed: 0.008 s % 74.41/11.15 % (423659)CaDiCaL version: 2.1.3 % 74.41/11.15 % (423662)Peak memory usage: 88 MB % 74.41/11.15 % (423659)Termination reason: Instruction limit % 74.41/11.15 % (423659)Termination phase: Saturation % 74.41/11.15 % (423659)Time elapsed: 0.111 s % 74.41/11.15 % (423662)Instructions burned: 18 (million) % 74.41/11.15 % (423659)Peak memory usage: 91 MB % 74.41/11.15 % (423659)Instructions burned: 271 (million) % 74.41/11.15 % (423667)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1395514010:i=1783:rtra=on:gtg=position_2933 on theBenchmark for (2933ds/1783Mi) % 74.41/11.15 % (423648)Instruction limit reached! % 74.41/11.15 % (423648)------------------------------ % 74.41/11.15 % (423648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.41/11.15 % (423648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.41/11.15 % (423648)CaDiCaL version: 2.1.3 % 92.62/13.75 % (423648)Termination reason: Instruction limit % 92.62/13.75 % (423648)Termination phase: Saturation % 92.62/13.75 % (423648)Time elapsed: 1.586 s % 92.62/13.75 % (423648)Peak memory usage: 136 MB % 92.62/13.75 % (423648)Instructions burned: 4096 (million) % 92.62/13.75 % (423662)------------------------------ % 92.62/13.75 % (423662)------------------------------ % 92.62/13.75 % (423669)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=944227589:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2931 on theBenchmark for (2931ds/5451Mi) % 92.62/13.75 % (423670)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=1543998014:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2931 on theBenchmark for (2931ds/4975Mi) % 92.62/13.75 % (423667)Instruction limit reached! % 92.62/13.75 % (423667)------------------------------ % 92.62/13.75 % (423667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.62/13.75 % (423667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.62/13.75 % (423667)CaDiCaL version: 2.1.3 % 92.62/13.75 % (423667)Termination reason: Instruction limit % 92.62/13.75 % (423667)Termination phase: Saturation % 92.62/13.75 % (423667)Time elapsed: 0.726 s % 92.62/13.75 % (423667)Peak memory usage: 120 MB % 92.62/13.75 % (423667)Instructions burned: 1784 (million) % 92.62/13.75 % (423673)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=238748010:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2924 on theBenchmark for (2924ds/2076Mi) % 92.62/13.75 % (423653)Instruction limit reached! % 92.62/13.75 % (423653)------------------------------ % 92.62/13.75 % (423653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.62/13.75 % (423653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.62/13.75 % (423653)CaDiCaL version: 2.1.3 % 92.62/13.75 % (423653)Termination reason: Instruction limit % 92.62/13.75 % (423653)Termination phase: Saturation % 92.62/13.75 % (423653)Time elapsed: 2.601 s % 92.62/13.75 % (423653)Peak memory usage: 168 MB % 92.62/13.75 % (423653)Instructions burned: 10547 (million) % 92.62/13.75 % (423675)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2551762522:i=5145:rtra=on_2917 on theBenchmark for (2917ds/5145Mi) % 92.62/13.75 % (423673)Instruction limit reached! % 92.62/13.75 % (423673)------------------------------ % 92.62/13.75 % (423673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.62/13.75 % (423673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.62/13.75 % (423673)CaDiCaL version: 2.1.3 % 92.62/13.75 % (423673)Termination reason: Instruction limit % 92.62/13.75 % (423673)Termination phase: Saturation % 92.62/13.75 % (423673)Time elapsed: 0.791 s % 92.62/13.75 % (423673)Peak memory usage: 119 MB % 92.62/13.75 % (423673)Instructions burned: 2078 (million) % 92.62/13.75 % (423677)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2571923659:i=3509:rtra=on_2915 on theBenchmark for (2915ds/3509Mi) % 92.62/13.75 % (423669)Instruction limit reached! % 92.62/13.75 % (423669)------------------------------ % 92.62/13.75 % (423669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.62/13.75 % (423669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.62/13.75 % (423669)CaDiCaL version: 2.1.3 % 92.62/13.75 % (423669)Termination reason: Instruction limit % 92.62/13.75 % (423669)Termination phase: Saturation % 92.62/13.75 % (423669)Time elapsed: 2.225 s % 92.62/13.75 % (423669)Peak memory usage: 122 MB % 92.62/13.75 % (423669)Instructions burned: 5451 (million) % 92.62/13.75 % (423679)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=338628587:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2908 on theBenchmark for (2908ds/13800Mi) % 92.62/13.75 % (423679)Refutation not found, incomplete strategy % 92.62/13.75 % (423679)------------------------------ % 92.62/13.75 % (423679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.62/13.75 % (423679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.62/13.75 % (423679)CaDiCaL version: 2.1.3 % 92.62/13.75 % (423679)Termination reason: Refutation not found, incomplete strategy % 92.62/13.75 % (423679)Time elapsed: 0.010 s % 92.62/13.75 % (423679)Peak memory usage: 88 MB % 92.62/13.75 % (423679)Instructions burned: 26 (million) % 92.62/13.75 % (423670)Instruction limit reached! % 92.62/13.75 % (423670)------------------------------ % 92.62/13.75 % (423670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.68/20.66 % (423670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.68/20.66 % (423670)CaDiCaL version: 2.1.3 % 141.68/20.66 % (423670)Termination reason: Instruction limit % 141.68/20.66 % (423670)Termination phase: Saturation % 141.68/20.66 % (423670)Time elapsed: 2.323 s % 141.68/20.66 % (423670)Peak memory usage: 134 MB % 141.68/20.66 % (423670)Instructions burned: 4978 (million) % 141.68/20.66 % (423675)Instruction limit reached! % 141.68/20.66 % (423675)------------------------------ % 141.68/20.66 % (423675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.68/20.66 % (423675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.68/20.66 % (423675)CaDiCaL version: 2.1.3 % 141.68/20.66 % (423675)Termination reason: Instruction limit % 141.68/20.66 % (423675)Termination phase: Saturation % 141.68/20.66 % (423675)Time elapsed: 1.070 s % 141.68/20.66 % (423675)Peak memory usage: 97 MB % 141.68/20.66 % (423675)Instructions burned: 5151 (million) % 141.68/20.66 % (423681)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2816326466:i=1412:rtra=on:fsd=on:proc=on_2906 on theBenchmark for (2906ds/1412Mi) % 141.68/20.66 % (423682)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 % 141.68/20.66 % (423682)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2766283750:i=11747:aac=none:nm=0:rtra=on:rawr=on_2905 on theBenchmark for (2905ds/11747Mi) % 141.68/20.66 % (423679)------------------------------ % 141.68/20.66 % (423679)------------------------------ % 141.68/20.66 % (423685)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=40620075:s2a=on:i=3553:nm=0:rtra=on_2904 on theBenchmark for (2904ds/3553Mi) % 141.68/20.66 % (423677)Instruction limit reached! % 141.68/20.66 % (423677)------------------------------ % 141.68/20.66 % (423677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.68/20.66 % (423677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.68/20.66 % (423677)CaDiCaL version: 2.1.3 % 141.68/20.66 % (423677)Termination reason: Instruction limit % 141.68/20.66 % (423677)Termination phase: Saturation % 141.68/20.66 % (423677)Time elapsed: 1.313 s % 141.68/20.66 % (423677)Peak memory usage: 91 MB % 141.68/20.66 % (423677)Instructions burned: 3512 (million) % 141.68/20.66 % (423687)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=620622183:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2901 on theBenchmark for (2901ds/3201Mi) % 141.68/20.66 % (423681)Instruction limit reached! % 141.68/20.66 % (423681)------------------------------ % 141.68/20.66 % (423681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.68/20.66 % (423681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.68/20.66 % (423681)CaDiCaL version: 2.1.3 % 141.68/20.66 % (423681)Termination reason: Instruction limit % 141.68/20.66 % (423681)Termination phase: Saturation % 141.68/20.66 % (423681)Time elapsed: 0.556 s % 141.68/20.66 % (423681)Peak memory usage: 119 MB % 141.68/20.66 % (423681)Instructions burned: 1414 (million) % 141.68/20.66 % (423687)Refutation not found, incomplete strategy % 141.68/20.66 % (423687)------------------------------ % 141.68/20.66 % (423687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.68/20.66 % (423687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.68/20.66 % (423687)CaDiCaL version: 2.1.3 % 141.68/20.66 % (423687)Termination reason: Refutation not found, incomplete strategy % 141.68/20.66 % (423687)Time elapsed: 0.124 s % 141.68/20.66 % (423687)Peak memory usage: 92 MB % 141.68/20.66 % (423687)Instructions burned: 312 (million) % 141.68/20.66 % (423689)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=4006779548:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2899 on theBenchmark for (2899ds/4081Mi) % 141.68/20.66 % (423687)------------------------------ % 141.68/20.66 % (423687)------------------------------ % 141.68/20.66 % (423691)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=1650677374:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2896 on theBenchmark for (2896ds/20260Mi) % 158.93/23.06 % (423691)Refutation not found, incomplete strategy % 158.93/23.06 % (423691)------------------------------ % 158.93/23.06 % (423691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.93/23.06 % (423691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.93/23.06 % (423691)CaDiCaL version: 2.1.3 % 158.93/23.06 % (423691)Termination reason: Refutation not found, incomplete strategy % 158.93/23.06 % (423691)Time elapsed: 0.030 s % 158.93/23.06 % (423691)Peak memory usage: 113 MB % 158.93/23.06 % (423691)Instructions burned: 15 (million) % 158.93/23.06 % (423691)------------------------------ % 158.93/23.06 % (423691)------------------------------ % 158.93/23.06 % (423693)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3555173892:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2892 on theBenchmark for (2892ds/58627Mi) % 158.93/23.06 % (423685)Instruction limit reached! % 158.93/23.06 % (423685)------------------------------ % 158.93/23.06 % (423685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.93/23.06 % (423685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.93/23.06 % (423685)CaDiCaL version: 2.1.3 % 158.93/23.06 % (423685)Termination reason: Instruction limit % 158.93/23.06 % (423685)Termination phase: Saturation % 158.93/23.06 % (423685)Time elapsed: 1.311 s % 158.93/23.06 % (423685)Peak memory usage: 91 MB % 158.93/23.06 % (423685)Instructions burned: 3554 (million) % 158.93/23.06 % (423695)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=433990425:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2890 on theBenchmark for (2890ds/6258Mi) % 158.93/23.06 % (423661)Instruction limit reached! % 158.93/23.06 % (423661)------------------------------ % 158.93/23.06 % (423661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.93/23.06 % (423661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.93/23.06 % (423661)CaDiCaL version: 2.1.3 % 158.93/23.06 % (423661)Termination reason: Instruction limit % 158.93/23.06 % (423661)Termination phase: Saturation % 158.93/23.06 % (423661)Time elapsed: 4.836 s % 158.93/23.06 % (423661)Peak memory usage: 107 MB % 158.93/23.06 % (423661)Instructions burned: 13097 (million) % 158.93/23.06 % (423697)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1144882152:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2885 on theBenchmark for (2885ds/34001Mi) % 158.93/23.06 % (423689)Instruction limit reached! % 158.93/23.06 % (423689)------------------------------ % 158.93/23.06 % (423689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.93/23.06 % (423689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.93/23.06 % (423689)CaDiCaL version: 2.1.3 % 158.93/23.06 % (423689)Termination reason: Instruction limit % 158.93/23.06 % (423689)Termination phase: Saturation % 158.93/23.06 % (423689)Time elapsed: 1.544 s % 158.93/23.06 % (423689)Peak memory usage: 136 MB % 158.93/23.06 % (423689)Instructions burned: 4082 (million) % 158.93/23.06 % (423699)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2544408686:s2a=on:i=71622:s2at=-1:rtra=on_2882 on theBenchmark for (2882ds/71622Mi) % 158.93/23.06 % (423682)Instruction limit reached! % 158.93/23.06 % (423682)------------------------------ % 158.93/23.06 % (423682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.93/23.06 % (423682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.93/23.06 % (423682)CaDiCaL version: 2.1.3 % 158.93/23.06 % (423682)Termination reason: Instruction limit % 158.93/23.06 % (423682)Termination phase: Saturation % 158.93/23.06 % (423682)Time elapsed: 2.501 s % 158.93/23.06 % (423682)Peak memory usage: 120 MB % 158.93/23.06 % (423682)Instructions burned: 11750 (million) % 158.93/23.06 % (423701)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=626486121:i=24001:kws=precedence:nm=0:rtra=on_2879 on theBenchmark for (2879ds/24001Mi) % 158.93/23.06 % (423660)Instruction limit reached! % 158.93/23.06 % (423660)------------------------------ % 158.93/23.06 % (423660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.93/23.06 % (423660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.93/23.06 % (423660)CaDiCaL version: 2.1.3 % 158.93/23.06 % (423660)Termination reason: Instruction limit % 158.93/23.06 % (423660)Termination phase: Saturation % 158.93/23.06 % (423660)Time elapsed: 6.370 s % 158.93/23.06 % (423660)Peak memory usage: 95 MB % 158.93/23.06 % (423660)Instructions burned: 17166 (million) % 158.93/23.06 % (423712)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=776789095:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2870 on theBenchmark for (2870ds/2076Mi) % 199.86/28.88 % (423695)Instruction limit reached! % 199.86/28.88 % (423695)------------------------------ % 199.86/28.88 % (423695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.88 % (423695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.88 % (423695)CaDiCaL version: 2.1.3 % 199.86/28.88 % (423695)Termination reason: Instruction limit % 199.86/28.88 % (423695)Termination phase: Saturation % 199.86/28.88 % (423695)Time elapsed: 2.436 s % 199.86/28.88 % (423695)Peak memory usage: 121 MB % 199.86/28.88 % (423695)Instructions burned: 6259 (million) % 199.86/28.88 % (423912)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=649139542:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2864 on theBenchmark for (2864ds/83971Mi) % 199.86/28.88 % (423712)Instruction limit reached! % 199.86/28.88 % (423712)------------------------------ % 199.86/28.88 % (423712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.89 % (423712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.89 % (423712)CaDiCaL version: 2.1.3 % 199.86/28.89 % (423712)Termination reason: Instruction limit % 199.86/28.89 % (423712)Termination phase: Saturation % 199.86/28.89 % (423712)Time elapsed: 0.786 s % 199.86/28.89 % (423712)Peak memory usage: 119 MB % 199.86/28.89 % (423712)Instructions burned: 2078 (million) % 199.86/28.89 % (424004)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3107371545:i=83944:rtra=on_2861 on theBenchmark for (2861ds/83944Mi) % 199.86/28.89 % (423701)Instruction limit reached! % 199.86/28.89 % (423701)------------------------------ % 199.86/28.89 % (423701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.89 % (423701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.89 % (423701)CaDiCaL version: 2.1.3 % 199.86/28.89 % (423701)Termination reason: Instruction limit % 199.86/28.89 % (423701)Termination phase: Saturation % 199.86/28.89 % (423701)Time elapsed: 5.241 s % 199.86/28.89 % (423701)Peak memory usage: 121 MB % 199.86/28.89 % (423701)Instructions burned: 24002 (million) % 199.86/28.89 % (424068)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3117390633:i=9201:rtra=on_2826 on theBenchmark for (2826ds/9201Mi) % 199.86/28.89 % (423623)Instruction limit reached! % 199.86/28.89 % (423623)------------------------------ % 199.86/28.89 % (423623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.89 % (423623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.89 % (423623)CaDiCaL version: 2.1.3 % 199.86/28.89 % (423623)Termination reason: Instruction limit % 199.86/28.89 % (423623)Termination phase: Saturation % 199.86/28.89 % (423623)Time elapsed: 13.639 s % 199.86/28.89 % (423623)Peak memory usage: 108 MB % 199.86/28.89 % (423623)Instructions burned: 36818 (million) % 199.86/28.89 % (424070)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 % 199.86/28.89 % (424070)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4074954662:i=6806:aac=none:nm=0:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/6806Mi) % 199.86/28.89 % (424068)Instruction limit reached! % 199.86/28.89 % (424068)------------------------------ % 199.86/28.89 % (424068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.89 % (424068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.89 % (424068)CaDiCaL version: 2.1.3 % 199.86/28.89 % (424068)Termination reason: Instruction limit % 199.86/28.89 % (424068)Termination phase: Saturation % 199.86/28.89 % (424068)Time elapsed: 1.811 s % 199.86/28.89 % (424068)Peak memory usage: 93 MB % 199.86/28.89 % (424068)Instructions burned: 9202 (million) % 199.86/28.89 % (424072)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2796474172:s2a=on:i=3553:nm=0:rtra=on_2807 on theBenchmark for (2807ds/3553Mi) % 199.86/28.89 % (424072)Instruction limit reached! % 199.86/28.89 % (424072)------------------------------ % 199.86/28.89 % (424072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.89 % (424072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.79/30.26 % (424072)CaDiCaL version: 2.1.3 % 209.79/30.26 % (424072)Termination reason: Instruction limit % 209.79/30.26 % (424072)Termination phase: Saturation % 209.79/30.26 % (424072)Time elapsed: 0.697 s % 209.79/30.26 % (424072)Peak memory usage: 92 MB % 209.79/30.26 % (424072)Instructions burned: 3557 (million) % 209.79/30.26 % (424074)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=3414374054:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2799 on theBenchmark for (2799ds/2064Mi) % 209.79/30.26 % (424070)Instruction limit reached! % 209.79/30.26 % (424070)------------------------------ % 209.79/30.26 % (424070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.79/30.26 % (424070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.79/30.26 % (424070)CaDiCaL version: 2.1.3 % 209.79/30.26 % (424070)Termination reason: Instruction limit % 209.79/30.26 % (424070)Termination phase: Saturation % 209.79/30.26 % (424070)Time elapsed: 2.745 s % 209.79/30.26 % (424070)Peak memory usage: 119 MB % 209.79/30.26 % (424070)Instructions burned: 6807 (million) % 209.79/30.26 % (424074)Instruction limit reached! % 209.79/30.26 % (424074)------------------------------ % 209.79/30.26 % (424074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.79/30.26 % (424074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.79/30.26 % (424074)CaDiCaL version: 2.1.3 % 209.79/30.26 % (424074)Termination reason: Instruction limit % 209.79/30.26 % (424074)Termination phase: Saturation % 209.79/30.26 % (424074)Time elapsed: 0.439 s % 209.79/30.26 % (424074)Peak memory usage: 131 MB % 209.79/30.26 % (424074)Instructions burned: 2068 (million) % 209.79/30.26 % (424076)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=3498437474:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2796 on theBenchmark for (2796ds/20260Mi) % 209.79/30.26 % (424076)Refutation not found, incomplete strategy % 209.79/30.26 % (424076)------------------------------ % 209.79/30.26 % (424076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.79/30.26 % (424076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.79/30.26 % (424076)CaDiCaL version: 2.1.3 % 209.79/30.26 % (424076)Termination reason: Refutation not found, incomplete strategy % 209.79/30.26 % (424076)Time elapsed: 0.030 s % 209.79/30.26 % (424076)Peak memory usage: 112 MB % 209.79/30.26 % (424076)Instructions burned: 15 (million) % 209.79/30.26 % (424078)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3839202773:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2794 on theBenchmark for (2794ds/1244Mi) % 209.79/30.26 % (424076)------------------------------ % 209.79/30.26 % (424076)------------------------------ % 209.79/30.26 % (424078)Instruction limit reached! % 209.79/30.26 % (424078)------------------------------ % 209.79/30.26 % (424078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.79/30.26 % (424078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.79/30.26 % (424078)CaDiCaL version: 2.1.3 % 209.79/30.26 % (424078)Termination reason: Instruction limit % 209.79/30.26 % (424078)Termination phase: Saturation % 209.79/30.26 % (424078)Time elapsed: 0.261 s % 209.79/30.26 % (424078)Peak memory usage: 118 MB % 209.79/30.26 % (424078)Instructions burned: 1247 (million) % 209.79/30.26 % (424080)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=3358812651:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2791 on theBenchmark for (2791ds/58261Mi) % 209.79/30.26 % (424081)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 % 209.79/30.26 % (424081)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1061442412:i=6806:aac=none:nm=0:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/6806Mi) % 209.79/30.26 % (424081)Instruction limit reached! % 209.79/30.26 % (424081)------------------------------ % 209.79/30.26 % (424081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.79/30.26 % (424081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.79/30.26 % (424081)CaDiCaL version: 2.1.3 % 209.79/30.26 % (424081)Termination reason: Instruction limit % 223.68/32.16 % (424081)Termination phase: Saturation % 223.68/32.16 % (424081)Time elapsed: 1.447 s % 223.68/32.16 % (424081)Peak memory usage: 120 MB % 223.68/32.16 % (424081)Instructions burned: 6810 (million) % 223.68/32.16 % (424084)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=1491487419:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2775 on theBenchmark for (2775ds/4081Mi) % 223.68/32.16 % (424084)Instruction limit reached! % 223.68/32.16 % (424084)------------------------------ % 223.68/32.16 % (424084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.68/32.16 % (424084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.68/32.16 % (424084)CaDiCaL version: 2.1.3 % 223.68/32.16 % (424084)Termination reason: Instruction limit % 223.68/32.16 % (424084)Termination phase: Saturation % 223.68/32.16 % (424084)Time elapsed: 0.846 s % 223.68/32.16 % (424084)Peak memory usage: 132 MB % 223.68/32.16 % (424084)Instructions burned: 4084 (million) % 223.68/32.16 % (424086)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1425181388:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2766 on theBenchmark for (2766ds/1701Mi) % 223.68/32.16 % (424086)Instruction limit reached! % 223.68/32.16 % (424086)------------------------------ % 223.68/32.16 % (424086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.68/32.16 % (424086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.68/32.16 % (424086)CaDiCaL version: 2.1.3 % 223.68/32.16 % (424086)Termination reason: Instruction limit % 223.68/32.16 % (424086)Termination phase: Saturation % 223.68/32.16 % (424086)Time elapsed: 0.353 s % 223.68/32.16 % (424086)Peak memory usage: 119 MB % 223.68/32.16 % (424086)Instructions burned: 1706 (million) % 223.68/32.16 % (424088)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=1408037406:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2762 on theBenchmark for (2762ds/57001Mi) % 223.68/32.16 % (423697)Instruction limit reached! % 223.68/32.16 % (423697)------------------------------ % 223.68/32.16 % (423697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.68/32.16 % (423697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.68/32.16 % (423697)CaDiCaL version: 2.1.3 % 223.68/32.16 % (423697)Termination reason: Instruction limit % 223.68/32.16 % (423697)Termination phase: Saturation % 223.68/32.16 % (423697)Time elapsed: 12.709 s % 223.68/32.16 % (423697)Peak memory usage: 101 MB % 223.68/32.16 % (423697)Instructions burned: 34001 (million) % 223.68/32.16 % (424090)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 % 223.68/32.16 % (424090)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3679990572:i=8622:aac=none:nm=0:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/8622Mi) % 223.68/32.16 % (424090)Instruction limit reached! % 223.68/32.16 % (424090)------------------------------ % 223.68/32.16 % (424090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.68/32.16 % (424090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.68/32.16 % (424090)CaDiCaL version: 2.1.3 % 223.68/32.16 % (424090)Termination reason: Instruction limit % 223.68/32.16 % (424090)Termination phase: Saturation % 223.68/32.16 % (424090)Time elapsed: 3.521 s % 223.68/32.16 % (424090)Peak memory usage: 119 MB % 223.68/32.16 % (424090)Instructions burned: 8624 (million) % 223.68/32.16 % (424110)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1497654850:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2720 on theBenchmark for (2720ds/24Mi) % 223.68/32.16 % (424110)Instruction limit reached! % 223.68/32.16 % (424110)------------------------------ % 223.68/32.16 % (424110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.68/32.16 % (424110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.68/32.16 % (424110)CaDiCaL version: 2.1.3 % 223.68/32.16 % (424110)Termination reason: Instruction limit % 223.68/32.16 % (424110)Termination phase: SInE selection % 223.68/32.16 % (424110)Time elapsed: 0.010 s % 223.68/32.16 % (424110)Peak memory usage: 86 MB % 223.68/32.16 % (424110)Instructions burned: 24 (million) % 223.68/32.16 % (424158)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=987793622:i=614:kws=precedence:nm=0:rtra=on_2718 on theBenchmark for (2718ds/614Mi) % 237.14/34.07 % (424158)Instruction limit reached! % 237.14/34.07 % (424158)------------------------------ % 237.14/34.07 % (424158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.14/34.07 % (424158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.14/34.07 % (424158)CaDiCaL version: 2.1.3 % 237.14/34.07 % (424158)Termination reason: Instruction limit % 237.14/34.07 % (424158)Termination phase: Saturation % 237.14/34.07 % (424158)Time elapsed: 0.255 s % 237.14/34.07 % (424158)Peak memory usage: 118 MB % 237.14/34.07 % (424158)Instructions burned: 615 (million) % 237.14/34.07 % (424228)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2339237532:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2715 on theBenchmark for (2715ds/402Mi) % 237.14/34.07 % (424228)Instruction limit reached! % 237.14/34.07 % (424228)------------------------------ % 237.14/34.07 % (424228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.14/34.07 % (424228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.14/34.07 % (424228)CaDiCaL version: 2.1.3 % 237.14/34.07 % (424228)Termination reason: Instruction limit % 237.14/34.07 % (424228)Termination phase: Saturation % 237.14/34.07 % (424228)Time elapsed: 0.182 s % 237.14/34.07 % (424228)Peak memory usage: 117 MB % 237.14/34.07 % (424228)Instructions burned: 403 (million) % 237.14/34.07 % (424272)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1468714767:s2a=on:i=14:rtra=on:inst=on_2711 on theBenchmark for (2711ds/14Mi) % 237.14/34.07 % (424272)Instruction limit reached! % 237.14/34.07 % (424272)------------------------------ % 237.14/34.07 % (424272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.14/34.07 % (424272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.14/34.07 % (424272)CaDiCaL version: 2.1.3 % 237.14/34.07 % (424272)Termination reason: Instruction limit % 237.14/34.07 % (424272)Termination phase: Property scanning % 237.14/34.07 % (424272)Time elapsed: 0.012 s % 237.14/34.07 % (424272)Peak memory usage: 85 MB % 237.14/34.07 % (424272)Instructions burned: 14 (million) % 237.14/34.07 % (424315)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4104705181:i=8:rtra=on_2710 on theBenchmark for (2710ds/8Mi) % 237.14/34.07 % (424315)Instruction limit reached! % 237.14/34.07 % (424315)------------------------------ % 237.14/34.07 % (424315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.14/34.07 % (424315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.14/34.07 % (424315)CaDiCaL version: 2.1.3 % 237.14/34.07 % (424315)Termination reason: Instruction limit % 237.14/34.07 % (424315)Termination phase: Property scanning % 237.14/34.07 % (424315)Time elapsed: 0.005 s % 237.14/34.07 % (424315)Peak memory usage: 85 MB % 237.14/34.07 % (424315)Instructions burned: 9 (million) % 237.14/34.07 % (424351)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1175622598:i=92:rtra=on_2708 on theBenchmark for (2708ds/92Mi) % 237.14/34.07 % (424351)Instruction limit reached! % 237.14/34.07 % (424351)------------------------------ % 237.14/34.07 % (424351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.14/34.07 % (424351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.14/34.07 % (424351)CaDiCaL version: 2.1.3 % 237.14/34.07 % (424351)Termination reason: Instruction limit % 237.14/34.07 % (424351)Termination phase: Saturation % 237.14/34.07 % (424351)Time elapsed: 0.059 s % 237.14/34.07 % (424351)Peak memory usage: 113 MB % 237.14/34.07 % (424351)Instructions burned: 93 (million) % 237.14/34.07 % (424366)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2499944648:i=66:rtra=on_2706 on theBenchmark for (2706ds/66Mi) % 237.14/34.07 % (424366)Instruction limit reached! % 237.14/34.07 % (424366)------------------------------ % 237.14/34.07 % (424366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.14/34.07 % (424366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.14/34.07 % (424366)CaDiCaL version: 2.1.3 % 237.14/34.07 % (424366)Termination reason: Instruction limit % 237.14/34.07 % (424366)Termination phase: Saturation % 237.14/34.07 % (424366)Time elapsed: 0.048 s % 237.14/34.07 % (424366)Peak memory usage: 113 MB % 237.14/34.07 % (424366)Instructions burned: 67 (million) % 237.14/34.07 % (424368)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1780503703:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2705 on theBenchmark for (2705ds/28Mi) % 245.70/35.33 % (424368)Refutation not found, incomplete strategy % 245.70/35.33 % (424368)------------------------------ % 245.70/35.33 % (424368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.70/35.33 % (424368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.70/35.33 % (424368)CaDiCaL version: 2.1.3 % 245.70/35.33 % (424368)Termination reason: Refutation not found, incomplete strategy % 245.70/35.33 % (424368)Time elapsed: 0.007 s % 245.70/35.33 % (424368)Peak memory usage: 88 MB % 245.70/35.33 % (424368)Instructions burned: 18 (million) % 245.70/35.33 % (424368)------------------------------ % 245.70/35.33 % (424368)------------------------------ % 245.70/35.33 % (424378)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=3744737028:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2701 on theBenchmark for (2701ds/58Mi) % 245.70/35.33 % (424378)Instruction limit reached! % 245.70/35.33 % (424378)------------------------------ % 245.70/35.33 % (424378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.70/35.33 % (424378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.70/35.33 % (424378)CaDiCaL version: 2.1.3 % 245.70/35.33 % (424378)Termination reason: Instruction limit % 245.70/35.33 % (424378)Termination phase: Saturation % 245.70/35.33 % (424378)Time elapsed: 0.042 s % 245.70/35.33 % (424378)Peak memory usage: 89 MB % 245.70/35.33 % (424378)Instructions burned: 58 (million) % 245.70/35.33 % (424391)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2341809204:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2698 on theBenchmark for (2698ds/32Mi) % 245.70/35.33 % (424391)Instruction limit reached! % 245.70/35.33 % (424391)------------------------------ % 245.70/35.33 % (424391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.70/35.33 % (424391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.70/35.33 % (424391)CaDiCaL version: 2.1.3 % 245.70/35.33 % (424391)Termination reason: Instruction limit % 245.70/35.33 % (424391)Termination phase: Saturation % 245.70/35.33 % (424391)Time elapsed: 0.023 s % 245.70/35.33 % (424391)Peak memory usage: 89 MB % 245.70/35.33 % (424391)Instructions burned: 33 (million) % 245.70/35.33 % (424405)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=35513388:i=48:canc=force:rtra=on_2696 on theBenchmark for (2696ds/48Mi) % 245.70/35.33 % (424405)Instruction limit reached! % 245.70/35.33 % (424405)------------------------------ % 245.70/35.33 % (424405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.70/35.33 % (424405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.70/35.33 % (424405)CaDiCaL version: 2.1.3 % 245.70/35.33 % (424405)Termination reason: Instruction limit % 245.70/35.33 % (424405)Termination phase: Saturation % 245.70/35.33 % (424405)Time elapsed: 0.034 s % 245.70/35.33 % (424405)Peak memory usage: 88 MB % 245.70/35.33 % (424405)Instructions burned: 48 (million) % 245.70/35.33 % (424421)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=218534914:i=54:canc=cautious:fsr=off:rtra=on_2693 on theBenchmark for (2693ds/54Mi) % 245.70/35.33 % (424421)Refutation not found, incomplete strategy % 245.70/35.33 % (424421)------------------------------ % 245.70/35.33 % (424421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.70/35.33 % (424421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.70/35.33 % (424421)CaDiCaL version: 2.1.3 % 245.70/35.33 % (424421)Termination reason: Refutation not found, incomplete strategy % 245.70/35.33 % (424421)Time elapsed: 0.025 s % 245.70/35.33 % (424421)Peak memory usage: 89 MB % 245.70/35.33 % (424421)Instructions burned: 54 (million) % 245.70/35.33 % (424421)------------------------------ % 245.70/35.33 % (424421)------------------------------ % 245.70/35.33 % (424448)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3835036729:i=170:gtgl=4:rtra=on:gtg=exists_sym_2688 on theBenchmark for (2688ds/170Mi) % 245.70/35.33 % (424448)Instruction limit reached! % 245.70/35.33 % (424448)------------------------------ % 245.70/35.33 % (424448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.70/35.33 % (424448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.70/35.33 % (424448)CaDiCaL version: 2.1.3 % 245.70/35.33 % (424448)Termination reason: Instruction limit % 245.70/35.33 % (424448)Termination phase: Saturation % 245.70/35.33 % (424448)Time elapsed: 0.126 s % 251.13/36.12 % (424448)Peak memory usage: 90 MB % 251.13/36.12 % (424448)Instructions burned: 171 (million) % 251.13/36.12 % (424462)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1368515400:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2684 on theBenchmark for (2684ds/4Mi) % 251.13/36.12 % (424462)Instruction limit reached! % 251.13/36.12 % (424462)------------------------------ % 251.13/36.12 % (424462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.13/36.12 % (424462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.13/36.12 % (424462)CaDiCaL version: 2.1.3 % 251.13/36.12 % (424462)Termination reason: Instruction limit % 251.13/36.12 % (424462)Termination phase: Property scanning % 251.13/36.12 % (424462)Time elapsed: 0.004 s % 251.13/36.12 % (424462)Peak memory usage: 85 MB % 251.13/36.12 % (424462)Instructions burned: 4 (million) % 251.13/36.12 % (424470)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1695406525:i=362:rtra=on:ss=axioms:ev=cautious_2682 on theBenchmark for (2682ds/362Mi) % 251.13/36.12 % (424470)Refutation not found, incomplete strategy % 251.13/36.12 % (424470)------------------------------ % 251.13/36.12 % (424470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.13/36.12 % (424470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.13/36.12 % (424470)CaDiCaL version: 2.1.3 % 251.13/36.12 % (424470)Termination reason: Refutation not found, incomplete strategy % 251.13/36.12 % (424470)Time elapsed: 0.011 s % 251.13/36.12 % (424470)Peak memory usage: 88 MB % 251.13/36.12 % (424470)Instructions burned: 17 (million) % 251.13/36.12 % (424470)------------------------------ % 251.13/36.12 % (424470)------------------------------ % 251.13/36.12 % (424489)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=23928867:i=8:ep=RST:ins=2:rtra=on_2677 on theBenchmark for (2677ds/8Mi) % 251.13/36.12 % (424489)Instruction limit reached! % 251.13/36.12 % (424489)------------------------------ % 251.13/36.12 % (424489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.13/36.12 % (424489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.13/36.12 % (424489)CaDiCaL version: 2.1.3 % 251.13/36.12 % (424489)Termination reason: Instruction limit % 251.13/36.12 % (424489)Termination phase: Property scanning % 251.13/36.12 % (424489)Time elapsed: 0.007 s % 251.13/36.12 % (424489)Peak memory usage: 85 MB % 251.13/36.12 % (424489)Instructions burned: 9 (million) % 251.13/36.12 % (424497)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1228671922:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2675 on theBenchmark for (2675ds/132Mi) % 251.13/36.12 % (424497)Instruction limit reached! % 251.13/36.12 % (424497)------------------------------ % 251.13/36.12 % (424497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.13/36.12 % (424497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.13/36.12 % (424497)CaDiCaL version: 2.1.3 % 251.13/36.12 % (424497)Termination reason: Instruction limit % 251.13/36.12 % (424497)Termination phase: Saturation % 251.13/36.12 % (424497)Time elapsed: 0.139 s % 251.13/36.12 % (424497)Peak memory usage: 130 MB % 251.13/36.12 % (424497)Instructions burned: 132 (million) % 251.13/36.12 % (424512)lrs+10_1_thi=all:si=on:fd=off:random_seed=2015290634:i=106:rtra=on:gtg=all_2671 on theBenchmark for (2671ds/106Mi) % 251.13/36.12 % (424512)Instruction limit reached! % 251.13/36.12 % (424512)------------------------------ % 251.13/36.12 % (424512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.13/36.12 % (424512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.13/36.12 % (424512)CaDiCaL version: 2.1.3 % 251.13/36.12 % (424512)Termination reason: Instruction limit % 251.13/36.12 % (424512)Termination phase: Saturation % 251.13/36.12 % (424512)Time elapsed: 0.110 s % 251.13/36.12 % (424512)Peak memory usage: 117 MB % 251.13/36.12 % (424512)Instructions burned: 108 (million) % 251.13/36.12 % (424518)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=459209469:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2668 on theBenchmark for (2668ds/16Mi) % 251.13/36.12 % (424518)Instruction limit reached! % 251.13/36.12 % (424518)------------------------------ % 251.13/36.12 % (424518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.13/36.12 % (424518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.13/36.12 % (424518)CaDiCaL version: 2.1.3 % 261.73/37.67 % (424518)Termination reason: Instruction limit % 261.73/37.67 % (424518)Termination phase: Property scanning % 261.73/37.67 % (424518)Time elapsed: 0.012 s % 261.73/37.67 % (424518)Peak memory usage: 85 MB % 261.73/37.67 % (424518)Instructions burned: 19 (million) % 261.73/37.67 % (424527)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4264783910:st=3:i=4:rtra=on:ss=axioms_2665 on theBenchmark for (2665ds/4Mi) % 261.73/37.67 % (424527)Instruction limit reached! % 261.73/37.67 % (424527)------------------------------ % 261.73/37.67 % (424527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.73/37.67 % (424527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.73/37.67 % (424527)CaDiCaL version: 2.1.3 % 261.73/37.67 % (424527)Termination reason: Instruction limit % 261.73/37.67 % (424527)Termination phase: Property scanning % 261.73/37.67 % (424527)Time elapsed: 0.004 s % 261.73/37.67 % (424527)Peak memory usage: 85 MB % 261.73/37.67 % (424527)Instructions burned: 4 (million) % 261.73/37.67 % (424535)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=530006558:i=4:doe=on:canc=force:asg=cautious:rtra=on_2663 on theBenchmark for (2663ds/4Mi) % 261.73/37.67 % (424535)Instruction limit reached! % 261.73/37.67 % (424535)------------------------------ % 261.73/37.67 % (424535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.73/37.67 % (424535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.73/37.67 % (424535)CaDiCaL version: 2.1.3 % 261.73/37.67 % (424535)Termination reason: Instruction limit % 261.73/37.67 % (424535)Termination phase: Property scanning % 261.73/37.67 % (424535)Time elapsed: 0.004 s % 261.73/37.67 % (424535)Peak memory usage: 85 MB % 261.73/37.67 % (424535)Instructions burned: 4 (million) % 261.73/37.67 % (424542)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1405844060:i=254:doe=on:rtra=on_2661 on theBenchmark for (2661ds/254Mi) % 261.73/37.67 % (423693)Instruction limit reached! % 261.73/37.67 % (423693)------------------------------ % 261.73/37.67 % (423693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.73/37.67 % (423693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.73/37.67 % (423693)CaDiCaL version: 2.1.3 % 261.73/37.67 % (423693)Termination reason: Instruction limit % 261.73/37.67 % (423693)Termination phase: Saturation % 261.73/37.67 % (423693)Time elapsed: 23.338 s % 261.73/37.67 % (423693)Peak memory usage: 124 MB % 261.73/37.67 % (423693)Instructions burned: 58628 (million) % 261.73/37.67 % (424542)Instruction limit reached! % 261.73/37.67 % (424542)------------------------------ % 261.73/37.67 % (424542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.73/37.67 % (424542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.73/37.67 % (424542)CaDiCaL version: 2.1.3 % 261.73/37.67 % (424542)Termination reason: Instruction limit % 261.73/37.67 % (424542)Termination phase: Saturation % 261.73/37.67 % (424542)Time elapsed: 0.208 s % 261.73/37.67 % (424542)Peak memory usage: 113 MB % 261.73/37.67 % (424542)Instructions burned: 255 (million) % 261.73/37.67 % (424553)dis+10_1_si=on:random_seed=2209103496:i=20:ep=R:rtra=on_2657 on theBenchmark for (2657ds/20Mi) % 261.73/37.67 % (424553)Instruction limit reached! % 261.73/37.67 % (424553)------------------------------ % 261.73/37.67 % (424553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.73/37.67 % (424553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.73/37.67 % (424553)CaDiCaL version: 2.1.3 % 261.73/37.67 % (424553)Termination reason: Instruction limit % 261.73/37.67 % (424553)Termination phase: Property scanning % 261.73/37.67 % (424553)Time elapsed: 0.016 s % 261.73/37.67 % (424553)Peak memory usage: 86 MB % 261.73/37.67 % (424553)Instructions burned: 20 (million) % 261.73/37.67 % (424555)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2125308882:i=52:canc=cautious:av=off:rtra=on_2657 on theBenchmark for (2657ds/52Mi) % 261.73/37.67 % (424555)Instruction limit reached! % 261.73/37.67 % (424555)------------------------------ % 261.73/37.67 % (424555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.73/37.67 % (424555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.73/37.67 % (424555)CaDiCaL version: 2.1.3 % 261.73/37.67 % (424555)Termination reason: Instruction limit % 261.73/37.67 % (424555)Termination phase: Saturation % 261.73/37.67 % (424555)Time elapsed: 0.041 s % 261.73/37.67 % (424555)Peak memory usage: 88 MB % 261.73/37.67 % (424555)Instructions burned: 52 (million) % 261.73/37.67 % (424560)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=924352190: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_2655 on theBenchmark for (2655ds/70Mi) % 274.85/39.46 % (424560)Instruction limit reached! % 274.85/39.46 % (424560)------------------------------ % 274.85/39.46 % (424560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.85/39.46 % (424560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.85/39.46 % (424560)CaDiCaL version: 2.1.3 % 274.85/39.46 % (424560)Termination reason: Instruction limit % 274.85/39.46 % (424560)Termination phase: Saturation % 274.85/39.46 % (424560)Time elapsed: 0.043 s % 274.85/39.46 % (424560)Peak memory usage: 89 MB % 274.85/39.46 % (424560)Instructions burned: 71 (million) % 274.85/39.46 % (424562)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3343694021:i=4:fsr=off:rtra=on:inst=on_2654 on theBenchmark for (2654ds/4Mi) % 274.85/39.46 % (424562)Instruction limit reached! % 274.85/39.46 % (424562)------------------------------ % 274.85/39.46 % (424562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.85/39.46 % (424562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.85/39.46 % (424562)CaDiCaL version: 2.1.3 % 274.85/39.46 % (424562)Termination reason: Instruction limit % 274.85/39.46 % (424562)Termination phase: Property scanning % 274.85/39.46 % (424562)Time elapsed: 0.004 s % 274.85/39.46 % (424562)Peak memory usage: 85 MB % 274.85/39.46 % (424562)Instructions burned: 5 (million) % 274.85/39.46 % (424568)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4069066530:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2652 on theBenchmark for (2652ds/16Mi) % 274.85/39.46 % (424568)Instruction limit reached! % 274.85/39.46 % (424568)------------------------------ % 274.85/39.46 % (424568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.85/39.46 % (424568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.85/39.46 % (424568)CaDiCaL version: 2.1.3 % 274.85/39.46 % (424568)Termination reason: Instruction limit % 274.85/39.46 % (424568)Termination phase: SInE selection % 274.85/39.46 % (424568)Time elapsed: 0.012 s % 274.85/39.46 % (424568)Peak memory usage: 85 MB % 274.85/39.46 % (424568)Instructions burned: 16 (million) % 274.85/39.46 % (424571)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2456749024:i=740:ep=RS:fsr=off:rtra=on_2652 on theBenchmark for (2652ds/740Mi) % 274.85/39.46 % (424571)Refutation not found, incomplete strategy % 274.85/39.46 % (424571)------------------------------ % 274.85/39.46 % (424571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.85/39.46 % (424571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.85/39.46 % (424571)CaDiCaL version: 2.1.3 % 274.85/39.46 % (424571)Termination reason: Refutation not found, incomplete strategy % 274.85/39.46 % (424571)Time elapsed: 0.032 s % 274.85/39.46 % (424571)Peak memory usage: 89 MB % 274.85/39.46 % (424571)Instructions burned: 49 (million) % 274.85/39.46 % (424577)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1160284483:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2650 on theBenchmark for (2650ds/26Mi) % 274.85/39.46 % (424577)Instruction limit reached! % 274.85/39.46 % (424577)------------------------------ % 274.85/39.46 % (424577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.85/39.46 % (424577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.85/39.46 % (424577)CaDiCaL version: 2.1.3 % 274.85/39.46 % (424577)Termination reason: Instruction limit % 274.85/39.46 % (424577)Termination phase: Property scanning % 274.85/39.46 % (424577)Time elapsed: 0.022 s % 274.85/39.46 % (424577)Peak memory usage: 85 MB % 274.85/39.46 % (424577)Instructions burned: 27 (million) % 274.85/39.46 % (424571)------------------------------ % 274.85/39.46 % (424571)------------------------------ % 274.85/39.46 % (424584)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=627625103:i=452:rtra=on:gtg=position:ss=axioms_2648 on theBenchmark for (2648ds/452Mi) % 274.85/39.46 % (424584)Refutation not found, incomplete strategy % 274.85/39.46 % (424584)------------------------------ % 274.85/39.46 % (424584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.85/39.46 % (424584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.85/39.46 % (424584)CaDiCaL version: 2.1.3 % 274.85/39.46 % (424584)Termination reason: Refutation not found, incomplete strategy % 288.27/41.30 % (424584)Time elapsed: 0.054 s % 288.27/41.30 % (424584)Peak memory usage: 111 MB % 288.27/41.30 % (424584)Instructions burned: 29 (million) % 288.27/41.30 % (424586)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2338233342:i=20:rtra=on_2645 on theBenchmark for (2645ds/20Mi) % 288.27/41.30 % (424586)Instruction limit reached! % 288.27/41.30 % (424586)------------------------------ % 288.27/41.30 % (424586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.27/41.30 % (424586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.27/41.30 % (424586)CaDiCaL version: 2.1.3 % 288.27/41.30 % (424586)Termination reason: Instruction limit % 288.27/41.30 % (424586)Termination phase: Saturation % 288.27/41.30 % (424586)Time elapsed: 0.015 s % 288.27/41.30 % (424586)Peak memory usage: 86 MB % 288.27/41.30 % (424586)Instructions burned: 20 (million) % 288.27/41.30 % (424584)------------------------------ % 288.27/41.30 % (424584)------------------------------ % 288.27/41.30 % (424596)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2657887380:i=142:rtra=on:gtg=exists_top_2643 on theBenchmark for (2643ds/142Mi) % 288.27/41.30 % (424596)Instruction limit reached! % 288.27/41.30 % (424596)------------------------------ % 288.27/41.30 % (424596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.27/41.30 % (424596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.27/41.30 % (424596)CaDiCaL version: 2.1.3 % 288.27/41.30 % (424596)Termination reason: Instruction limit % 288.27/41.30 % (424596)Termination phase: Saturation % 288.27/41.30 % (424596)Time elapsed: 0.156 s % 288.27/41.30 % (424596)Peak memory usage: 130 MB % 288.27/41.30 % (424596)Instructions burned: 143 (million) % 288.27/41.30 % (424600)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=3629323829:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2641 on theBenchmark for (2641ds/150Mi) % 288.27/41.30 % (424600)Instruction limit reached! % 288.27/41.30 % (424600)------------------------------ % 288.27/41.30 % (424600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.27/41.30 % (424600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.27/41.30 % (424600)CaDiCaL version: 2.1.3 % 288.27/41.30 % (424600)Termination reason: Instruction limit % 288.27/41.30 % (424600)Termination phase: Saturation % 288.27/41.30 % (424600)Time elapsed: 0.113 s % 288.27/41.30 % (424600)Peak memory usage: 91 MB % 288.27/41.30 % (424600)Instructions burned: 150 (million) % 288.27/41.30 % (424606)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=4058069569:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2639 on theBenchmark for (2639ds/588Mi) % 288.27/41.30 % (424610)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3910840214:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2638 on theBenchmark for (2638ds/260Mi) % 288.27/41.30 % (424610)Instruction limit reached! % 288.27/41.30 % (424610)------------------------------ % 288.27/41.30 % (424610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.27/41.30 % (424610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.27/41.30 % (424610)CaDiCaL version: 2.1.3 % 288.27/41.30 % (424610)Termination reason: Instruction limit % 288.27/41.30 % (424610)Termination phase: Saturation % 288.27/41.30 % (424610)Time elapsed: 0.244 s % 288.27/41.30 % (424610)Peak memory usage: 119 MB % 288.27/41.30 % (424610)Instructions burned: 260 (million) % 288.27/41.30 % (424606)Instruction limit reached! % 288.27/41.30 % (424606)------------------------------ % 288.27/41.30 % (424606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.27/41.30 % (424606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.27/41.30 % (424606)CaDiCaL version: 2.1.3 % 288.27/41.30 % (424606)Termination reason: Instruction limit % 288.27/41.30 % (424606)Termination phase: Saturation % 288.27/41.30 % (424606)Time elapsed: 0.430 s % 288.27/41.30 % (424606)Peak memory usage: 91 MB % 288.27/41.30 % (424606)Instructions burned: 588 (million) % 288.27/41.30 % (424624)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3111434790:i=262:rtra=on_2633 on theBenchmark for (2633ds/262Mi) % 288.27/41.30 % (424626)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2169431958:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2633 on theBenchmark for (2633ds/80Mi) % 288.27/41.30 % (424626)Instruction limit reached! % 296.19/42.50 % (424626)------------------------------ % 296.19/42.50 % (424626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.19/42.50 % (424626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.19/42.50 % (424626)CaDiCaL version: 2.1.3 % 296.19/42.50 % (424626)Termination reason: Instruction limit % 296.19/42.50 % (424626)Termination phase: Saturation % 296.19/42.50 % (424626)Time elapsed: 0.117 s % 296.19/42.50 % (424626)Peak memory usage: 129 MB % 296.19/42.50 % (424626)Instructions burned: 81 (million) % 296.19/42.50 % (424624)Instruction limit reached! % 296.19/42.50 % (424624)------------------------------ % 296.19/42.50 % (424624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.19/42.50 % (424624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.19/42.50 % (424624)CaDiCaL version: 2.1.3 % 296.19/42.50 % (424624)Termination reason: Instruction limit % 296.19/42.50 % (424624)Termination phase: Saturation % 296.19/42.50 % (424624)Time elapsed: 0.267 s % 296.19/42.50 % (424624)Peak memory usage: 134 MB % 296.19/42.50 % (424624)Instructions burned: 262 (million) % 296.19/42.50 % (424633)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3623170843:i=614:rtra=on:gtg=exists_top_2629 on theBenchmark for (2629ds/614Mi) % 296.19/42.50 % (424633)Refutation not found, incomplete strategy % 296.19/42.50 % (424633)------------------------------ % 296.19/42.50 % (424633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.19/42.50 % (424633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.19/42.50 % (424633)CaDiCaL version: 2.1.3 % 296.19/42.50 % (424633)Termination reason: Refutation not found, incomplete strategy % 296.19/42.50 % (424633)Time elapsed: 0.028 s % 296.19/42.50 % (424633)Peak memory usage: 89 MB % 296.19/42.50 % (424633)Instructions burned: 67 (million) % 296.19/42.50 % (424635)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1358638093:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2628 on theBenchmark for (2628ds/1196Mi) % 296.19/42.50 % (424633)------------------------------ % 296.19/42.50 % (424633)------------------------------ % 296.19/42.50 % (424641)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3013767143:i=262:canc=cautious:fsr=off:rtra=on_2625 on theBenchmark for (2625ds/262Mi) % 296.19/42.50 % (424641)Instruction limit reached! % 296.19/42.50 % (424641)------------------------------ % 296.19/42.50 % (424641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.19/42.50 % (424641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.19/42.50 % (424641)CaDiCaL version: 2.1.3 % 296.19/42.50 % (424641)Termination reason: Instruction limit % 296.19/42.50 % (424641)Termination phase: Saturation % 296.19/42.50 % (424641)Time elapsed: 0.213 s % 296.19/42.50 % (424641)Peak memory usage: 113 MB % 296.19/42.50 % (424641)Instructions burned: 262 (million) % 296.19/42.50 % (424647)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=1304364657:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2620 on theBenchmark for (2620ds/518Mi) % 296.19/42.50 % (424647)Refutation not found, incomplete strategy % 296.19/42.50 % (424647)------------------------------ % 296.19/42.50 % (424647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.19/42.50 % (424647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.19/42.50 % (424647)CaDiCaL version: 2.1.3 % 296.19/42.50 % (424647)Termination reason: Refutation not found, incomplete strategy % 296.19/42.50 % (424647)Time elapsed: 0.055 s % 296.19/42.50 % (424647)Peak memory usage: 112 MB % 296.19/42.50 % (424647)Instructions burned: 31 (million) % 296.19/42.50 % (424635)Instruction limit reached! % 296.19/42.50 % (424635)------------------------------ % 296.19/42.50 % (424635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.19/42.50 % (424635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.19/42.50 % (424635)CaDiCaL version: 2.1.3 % 296.19/42.50 % (424635)Termination reason: Instruction limit % 296.19/42.50 % (424635)Termination phase: Saturation % 296.19/42.50 % (424635)Time elapsed: 0.961 s % 296.19/42.50 % (424635)Peak memory usage: 136 MB % 296.19/42.50 % (424635)Instructions burned: 1196 (million) % 296.19/42.50 % (424650)dis+10_1_si=on:random_seed=2792259921:s2a=on:i=2000:rtra=on:gtg=exists_all_2616 on theBenchmark for (2616ds/2000Mi) % 296.19/42.50 % (424647)------------------------------ % 296.19/42.50 % (424647)------------------------------ % 296.19/42.50 % (424653)dis+1010_1_to=lpo:sil=1280Terminated %------------------------------------------------------------------------------