%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC430_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n010.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:03:56 PM UTC 2026 % Result : Timeout 290.02s 41.70s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC430_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.12/0.24 % Computer : n010.cluster.edu % 0.12/0.24 % Model : x86_64 x86_64 % 0.12/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.24 % Memory : 8046.5625MB % 0.12/0.24 % OS : Linux 6.8.0-71-generic % 0.12/0.24 % CPULimit : 300 % 0.12/0.24 % WCLimit : 300 % 0.12/0.24 % DateTime : Mon Sep 28 09:37:32 UTC 2026 % 0.12/0.25 % CPUTime : % 0.12/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.27/0.30 Running first-order theorem proving % 0.27/0.30 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 % 5.85/1.71 % (1801349)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.85/1.71 % (1801357)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3582054316:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.85/1.71 % (1801360)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4241282247:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.85/1.71 % (1801357)Instruction limit reached! % 5.85/1.71 % (1801357)------------------------------ % 5.85/1.71 % (1801357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.71 % (1801357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.71 % (1801357)CaDiCaL version: 2.1.3 % 5.85/1.71 % (1801357)Termination reason: Instruction limit % 5.85/1.71 % (1801357)Termination phase: Saturation % 5.85/1.71 % (1801357)Time elapsed: 0.005 s % 5.85/1.71 % (1801357)Peak memory usage: 88 MB % 5.85/1.71 % (1801357)Instructions burned: 7 (million) % 5.85/1.71 % (1801356)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1822228557:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.85/1.71 % (1801359)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1210523832:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.85/1.71 % (1801358)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1975146421:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.85/1.71 % (1801355)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2122864244:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.85/1.71 % (1801354)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=989470127:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.85/1.71 % (1801360)Instruction limit reached! % 5.85/1.71 % (1801360)------------------------------ % 5.85/1.71 % (1801360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.71 % (1801360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.71 % (1801360)CaDiCaL version: 2.1.3 % 5.85/1.71 % (1801360)Termination reason: Instruction limit % 5.85/1.71 % (1801360)Termination phase: Saturation % 5.85/1.71 % (1801360)Time elapsed: 0.069 s % 5.85/1.71 % (1801360)Peak memory usage: 116 MB % 5.85/1.71 % (1801360)Instructions burned: 33 (million) % 5.85/1.71 % (1801358)Instruction limit reached! % 5.85/1.71 % (1801358)------------------------------ % 5.85/1.71 % (1801358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.71 % (1801358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.71 % (1801358)CaDiCaL version: 2.1.3 % 5.85/1.71 % (1801358)Termination reason: Instruction limit % 5.85/1.71 % (1801358)Termination phase: Saturation % 5.85/1.71 % (1801358)Time elapsed: 0.006 s % 5.85/1.71 % (1801358)Peak memory usage: 88 MB % 5.85/1.71 % (1801358)Instructions burned: 4 (million) % 5.85/1.71 % (1801354)Instruction limit reached! % 5.85/1.71 % (1801354)------------------------------ % 5.85/1.71 % (1801354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.71 % (1801354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.71 % (1801354)CaDiCaL version: 2.1.3 % 5.85/1.71 % (1801354)Termination reason: Instruction limit % 5.85/1.71 % (1801354)Termination phase: Saturation % 5.85/1.71 % (1801354)Time elapsed: 0.044 s % 5.85/1.71 % (1801354)Peak memory usage: 115 MB % 5.85/1.71 % (1801354)Instructions burned: 13 (million) % 5.85/1.71 % (1801359)Instruction limit reached! % 5.85/1.71 % (1801359)------------------------------ % 5.85/1.71 % (1801359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.85/1.71 % (1801359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.71 % (1801359)CaDiCaL version: 2.1.3 % 5.85/1.71 % (1801359)Termination reason: Instruction limit % 5.85/1.71 % (1801359)Termination phase: Saturation % 5.85/1.71 % (1801359)Time elapsed: 0.077 s % 5.85/1.71 % (1801359)Peak memory usage: 115 MB % 5.85/1.71 % (1801359)Instructions burned: 47 (million) % 5.85/1.71 % (1801363)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2957053346:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 5.85/1.71 % (1801363)Instruction limit reached! % 5.85/1.71 % (1801363)------------------------------ % 7.33/1.89 % (1801363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.33/1.89 % (1801363)CaDiCaL version: 2.1.3 % 7.33/1.89 % (1801363)Termination reason: Instruction limit % 7.33/1.89 % (1801363)Termination phase: Saturation % 7.33/1.89 % (1801363)Time elapsed: 0.009 s % 7.33/1.89 % (1801363)Peak memory usage: 88 MB % 7.33/1.89 % (1801363)Instructions burned: 15 (million) % 7.33/1.89 % (1801356)Instruction limit reached! % 7.33/1.89 % (1801356)------------------------------ % 7.33/1.89 % (1801356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.33/1.89 % (1801356)CaDiCaL version: 2.1.3 % 7.33/1.89 % (1801356)Termination reason: Instruction limit % 7.33/1.89 % (1801356)Termination phase: Saturation % 7.33/1.89 % (1801356)Time elapsed: 0.260 s % 7.33/1.89 % (1801356)Peak memory usage: 117 MB % 7.33/1.89 % (1801356)Instructions burned: 201 (million) % 7.33/1.89 % (1801371)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=911716288:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 7.33/1.89 % (1801370)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2305929801:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 7.33/1.89 % (1801369)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=268810565:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 7.33/1.89 % (1801371)Instruction limit reached! % 7.33/1.89 % (1801371)------------------------------ % 7.33/1.89 % (1801371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.33/1.89 % (1801371)CaDiCaL version: 2.1.3 % 7.33/1.89 % (1801371)Termination reason: Instruction limit % 7.33/1.89 % (1801371)Termination phase: Saturation % 7.33/1.89 % (1801371)Time elapsed: 0.018 s % 7.33/1.89 % (1801371)Peak memory usage: 89 MB % 7.33/1.89 % (1801371)Instructions burned: 25 (million) % 7.33/1.89 % (1801370)Instruction limit reached! % 7.33/1.89 % (1801370)------------------------------ % 7.33/1.89 % (1801370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.33/1.89 % (1801370)CaDiCaL version: 2.1.3 % 7.33/1.89 % (1801370)Termination reason: Instruction limit % 7.33/1.89 % (1801370)Termination phase: Saturation % 7.33/1.89 % (1801370)Time elapsed: 0.017 s % 7.33/1.89 % (1801370)Peak memory usage: 90 MB % 7.33/1.89 % (1801370)Instructions burned: 16 (million) % 7.33/1.89 % (1801369)Instruction limit reached! % 7.33/1.89 % (1801369)------------------------------ % 7.33/1.89 % (1801369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.33/1.89 % (1801369)CaDiCaL version: 2.1.3 % 7.33/1.89 % (1801369)Termination reason: Instruction limit % 7.33/1.89 % (1801369)Termination phase: Saturation % 7.33/1.89 % (1801369)Time elapsed: 0.035 s % 7.33/1.89 % (1801369)Peak memory usage: 89 MB % 7.33/1.89 % (1801369)Instructions burned: 29 (million) % 7.33/1.89 % (1801355)Instruction limit reached! % 7.33/1.89 % (1801355)------------------------------ % 7.33/1.89 % (1801355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.33/1.89 % (1801355)CaDiCaL version: 2.1.3 % 7.33/1.89 % (1801355)Termination reason: Instruction limit % 7.33/1.89 % (1801355)Termination phase: Saturation % 7.33/1.89 % (1801355)Time elapsed: 0.341 s % 7.33/1.89 % (1801355)Peak memory usage: 118 MB % 7.33/1.89 % (1801355)Instructions burned: 307 (million) % 7.33/1.89 % (1801372)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=3234108103:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 7.33/1.89 % (1801372)Instruction limit reached! % 7.33/1.89 % (1801372)------------------------------ % 7.33/1.89 % (1801372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.33/1.89 % (1801372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.15 % (1801372)CaDiCaL version: 2.1.3 % 9.82/2.15 % (1801372)Termination reason: Instruction limit % 9.82/2.15 % (1801372)Termination phase: Saturation % 9.82/2.15 % (1801372)Time elapsed: 0.029 s % 9.82/2.15 % (1801372)Peak memory usage: 89 MB % 9.82/2.15 % (1801372)Instructions burned: 27 (million) % 9.82/2.15 % (1801374)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2723022250:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 9.82/2.15 % (1801378)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2917547859:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 9.82/2.15 % (1801378)Instruction limit reached! % 9.82/2.15 % (1801378)------------------------------ % 9.82/2.15 % (1801378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.15 % (1801378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.15 % (1801378)CaDiCaL version: 2.1.3 % 9.82/2.15 % (1801378)Termination reason: Instruction limit % 9.82/2.15 % (1801378)Termination phase: Saturation % 9.82/2.15 % (1801378)Time elapsed: 0.004 s % 9.82/2.15 % (1801378)Peak memory usage: 88 MB % 9.82/2.15 % (1801378)Instructions burned: 2 (million) % 9.82/2.15 % (1801381)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1749959126:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 9.82/2.15 % (1801374)Instruction limit reached! % 9.82/2.15 % (1801374)------------------------------ % 9.82/2.15 % (1801374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.15 % (1801374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.15 % (1801374)CaDiCaL version: 2.1.3 % 9.82/2.15 % (1801374)Termination reason: Instruction limit % 9.82/2.15 % (1801374)Termination phase: Saturation % 9.82/2.15 % (1801374)Time elapsed: 0.083 s % 9.82/2.15 % (1801374)Peak memory usage: 89 MB % 9.82/2.15 % (1801374)Instructions burned: 85 (million) % 9.82/2.15 % (1801379)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=246032722:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.82/2.15 % (1801380)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1008003802:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.82/2.15 % (1801380)Instruction limit reached! % 9.82/2.15 % (1801380)------------------------------ % 9.82/2.15 % (1801380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.15 % (1801380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.15 % (1801380)CaDiCaL version: 2.1.3 % 9.82/2.15 % (1801380)Termination reason: Instruction limit % 9.82/2.15 % (1801380)Termination phase: Saturation % 9.82/2.15 % (1801380)Time elapsed: 0.005 s % 9.82/2.15 % (1801380)Peak memory usage: 88 MB % 9.82/2.15 % (1801380)Instructions burned: 4 (million) % 9.82/2.15 % (1801381)Instruction limit reached! % 9.82/2.15 % (1801381)------------------------------ % 9.82/2.15 % (1801381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.15 % (1801381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.15 % (1801381)CaDiCaL version: 2.1.3 % 9.82/2.15 % (1801381)Termination reason: Instruction limit % 9.82/2.15 % (1801381)Termination phase: Saturation % 9.82/2.15 % (1801381)Time elapsed: 0.074 s % 9.82/2.15 % (1801381)Peak memory usage: 135 MB % 9.82/2.15 % (1801381)Instructions burned: 68 (million) % 9.82/2.15 % (1801382)lrs+10_1_thi=all:si=on:fd=off:random_seed=2043899731:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 9.82/2.15 % (1801384)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=1522510441:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 9.82/2.15 % (1801384)Instruction limit reached! % 9.82/2.15 % (1801384)------------------------------ % 9.82/2.15 % (1801384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.82/2.15 % (1801384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.82/2.15 % (1801384)CaDiCaL version: 2.1.3 % 9.82/2.15 % (1801384)Termination reason: Instruction limit % 9.82/2.15 % (1801384)Termination phase: Saturation % 9.82/2.15 % (1801384)Time elapsed: 0.010 s % 9.82/2.15 % (1801384)Peak memory usage: 88 MB % 9.82/2.15 % (1801384)Instructions burned: 8 (million) % 9.82/2.15 % (1801382)Instruction limit reached! % 11.68/2.59 % (1801382)------------------------------ % 11.68/2.59 % (1801382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.68/2.59 % (1801382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.68/2.59 % (1801382)CaDiCaL version: 2.1.3 % 11.68/2.59 % (1801382)Termination reason: Instruction limit % 11.68/2.59 % (1801382)Termination phase: Saturation % 11.68/2.59 % (1801382)Time elapsed: 0.096 s % 11.68/2.59 % (1801382)Peak memory usage: 116 MB % 11.68/2.59 % (1801382)Instructions burned: 53 (million) % 11.68/2.59 % (1801387)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=350526582:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 11.68/2.59 % (1801387)Instruction limit reached! % 11.68/2.59 % (1801387)------------------------------ % 11.68/2.59 % (1801387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.68/2.59 % (1801387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.68/2.59 % (1801387)CaDiCaL version: 2.1.3 % 11.68/2.59 % (1801387)Termination reason: Instruction limit % 11.68/2.59 % (1801387)Termination phase: Saturation % 11.68/2.59 % (1801387)Time elapsed: 0.004 s % 11.68/2.59 % (1801387)Peak memory usage: 89 MB % 11.68/2.59 % (1801387)Instructions burned: 3 (million) % 11.68/2.59 % (1801392)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3987661896:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 11.68/2.59 % (1801379)Instruction limit reached! % 11.68/2.59 % (1801379)------------------------------ % 11.68/2.59 % (1801379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.68/2.59 % (1801379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.68/2.59 % (1801379)CaDiCaL version: 2.1.3 % 11.68/2.59 % (1801379)Termination reason: Instruction limit % 11.68/2.59 % (1801379)Termination phase: Saturation % 11.68/2.59 % (1801379)Time elapsed: 0.184 s % 11.68/2.59 % (1801379)Peak memory usage: 90 MB % 11.68/2.59 % (1801379)Instructions burned: 183 (million) % 11.68/2.59 % (1801389)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2324324657:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 11.68/2.59 % (1801389)Instruction limit reached! % 11.68/2.59 % (1801389)------------------------------ % 11.68/2.59 % (1801389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.68/2.59 % (1801389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.68/2.59 % (1801389)CaDiCaL version: 2.1.3 % 11.68/2.59 % (1801389)Termination reason: Instruction limit % 11.68/2.59 % (1801389)Termination phase: Saturation % 11.68/2.59 % (1801389)Time elapsed: 0.004 s % 11.68/2.59 % (1801389)Peak memory usage: 89 MB % 11.68/2.59 % (1801389)Instructions burned: 2 (million) % 11.68/2.59 % (1801393)dis+10_1_si=on:random_seed=3138164541:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 11.68/2.59 % (1801393)Instruction limit reached! % 11.68/2.59 % (1801393)------------------------------ % 11.68/2.59 % (1801393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.68/2.59 % (1801393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.68/2.59 % (1801393)CaDiCaL version: 2.1.3 % 11.68/2.59 % (1801393)Termination reason: Instruction limit % 11.68/2.59 % (1801393)Termination phase: Saturation % 11.68/2.59 % (1801393)Time elapsed: 0.007 s % 11.68/2.59 % (1801393)Peak memory usage: 88 MB % 11.68/2.59 % (1801393)Instructions burned: 11 (million) % 11.68/2.59 % (1801392)Instruction limit reached! % 11.68/2.59 % (1801392)------------------------------ % 11.68/2.59 % (1801392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.68/2.59 % (1801392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.68/2.59 % (1801392)CaDiCaL version: 2.1.3 % 11.68/2.59 % (1801392)Termination reason: Instruction limit % 11.68/2.59 % (1801392)Termination phase: Saturation % 11.68/2.59 % (1801392)Time elapsed: 0.158 s % 11.68/2.59 % (1801392)Peak memory usage: 116 MB % 11.68/2.59 % (1801392)Instructions burned: 127 (million) % 11.68/2.59 % (1801400)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=248310658:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 11.68/2.59 % (1801396)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1357176419:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 11.68/2.59 % (1801400)Instruction limit reached! % 11.68/2.59 % (1801400)------------------------------ % 11.68/2.59 % (1801400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.99 % (1801400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.99 % (1801400)CaDiCaL version: 2.1.3 % 13.98/2.99 % (1801400)Termination reason: Instruction limit % 13.98/2.99 % (1801400)Termination phase: Saturation % 13.98/2.99 % (1801400)Time elapsed: 0.003 s % 13.98/2.99 % (1801400)Peak memory usage: 89 MB % 13.98/2.99 % (1801400)Instructions burned: 2 (million) % 13.98/2.99 % (1801396)Refutation not found, incomplete strategy % 13.98/2.99 % (1801396)------------------------------ % 13.98/2.99 % (1801396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.99 % (1801396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.99 % (1801396)CaDiCaL version: 2.1.3 % 13.98/2.99 % (1801396)Termination reason: Refutation not found, incomplete strategy % 13.98/2.99 % (1801396)Time elapsed: 0.004 s % 13.98/2.99 % (1801396)Peak memory usage: 89 MB % 13.98/2.99 % (1801396)Instructions burned: 2 (million) % 13.98/2.99 % (1801401)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1958172488:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 13.98/2.99 % (1801399)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3372938161: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_2990 on theBenchmark for (2990ds/35Mi) % 13.98/2.99 % (1801401)Instruction limit reached! % 13.98/2.99 % (1801401)------------------------------ % 13.98/2.99 % (1801401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.99 % (1801401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.99 % (1801401)CaDiCaL version: 2.1.3 % 13.98/2.99 % (1801401)Termination reason: Instruction limit % 13.98/2.99 % (1801401)Termination phase: Saturation % 13.98/2.99 % (1801401)Time elapsed: 0.011 s % 13.98/2.99 % (1801401)Peak memory usage: 88 MB % 13.98/2.99 % (1801401)Instructions burned: 8 (million) % 13.98/2.99 % (1801405)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3254816411:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 13.98/2.99 % (1801403)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1246562218:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 13.98/2.99 % (1801405)Instruction limit reached! % 13.98/2.99 % (1801405)------------------------------ % 13.98/2.99 % (1801405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.99 % (1801405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.99 % (1801405)CaDiCaL version: 2.1.3 % 13.98/2.99 % (1801405)Termination reason: Instruction limit % 13.98/2.99 % (1801405)Termination phase: Saturation % 13.98/2.99 % (1801405)Time elapsed: 0.025 s % 13.98/2.99 % (1801405)Peak memory usage: 116 MB % 13.98/2.99 % (1801405)Instructions burned: 13 (million) % 13.98/2.99 % (1801399)Instruction limit reached! % 13.98/2.99 % (1801399)------------------------------ % 13.98/2.99 % (1801399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.99 % (1801399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.99 % (1801399)CaDiCaL version: 2.1.3 % 13.98/2.99 % (1801399)Termination reason: Instruction limit % 13.98/2.99 % (1801399)Termination phase: Saturation % 13.98/2.99 % (1801399)Time elapsed: 0.044 s % 13.98/2.99 % (1801399)Peak memory usage: 89 MB % 13.98/2.99 % (1801399)Instructions burned: 35 (million) % 13.98/2.99 % (1801409)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=737169660:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 13.98/2.99 % (1801409)Instruction limit reached! % 13.98/2.99 % (1801409)------------------------------ % 13.98/2.99 % (1801409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.98/2.99 % (1801409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.98/2.99 % (1801409)CaDiCaL version: 2.1.3 % 13.98/2.99 % (1801409)Termination reason: Instruction limit % 13.98/2.99 % (1801409)Termination phase: Saturation % 13.98/2.99 % (1801409)Time elapsed: 0.012 s % 13.98/2.99 % (1801409)Peak memory usage: 88 MB % 13.98/2.99 % (1801409)Instructions burned: 10 (million) % 13.98/2.99 % (1801408)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4112517075:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 18.34/3.41 % (1801408)Refutation not found, incomplete strategy % 18.34/3.41 % (1801408)------------------------------ % 18.34/3.41 % (1801408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.34/3.41 % (1801408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.34/3.41 % (1801408)CaDiCaL version: 2.1.3 % 18.34/3.41 % (1801408)Termination reason: Refutation not found, incomplete strategy % 18.34/3.41 % (1801408)Time elapsed: 0.041 s % 18.34/3.41 % (1801408)Peak memory usage: 115 MB % 18.34/3.41 % (1801408)Instructions burned: 7 (million) % 18.34/3.41 % (1801414)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=338626801:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 18.34/3.41 % (1801415)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=2251941515:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 18.34/3.41 % (1801396)------------------------------ % 18.34/3.41 % (1801396)------------------------------ % 18.34/3.41 % (1801416)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=2067565589:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 18.34/3.41 % (1801403)Instruction limit reached! % 18.34/3.41 % (1801403)------------------------------ % 18.34/3.41 % (1801403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.34/3.41 % (1801403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.34/3.41 % (1801403)CaDiCaL version: 2.1.3 % 18.34/3.41 % (1801403)Termination reason: Instruction limit % 18.34/3.41 % (1801403)Termination phase: Saturation % 18.34/3.41 % (1801403)Time elapsed: 0.315 s % 18.34/3.41 % (1801403)Peak memory usage: 91 MB % 18.34/3.41 % (1801403)Instructions burned: 370 (million) % 18.34/3.41 % (1801415)Instruction limit reached! % 18.34/3.41 % (1801415)------------------------------ % 18.34/3.41 % (1801415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.34/3.41 % (1801415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.34/3.41 % (1801415)CaDiCaL version: 2.1.3 % 18.34/3.41 % (1801415)Termination reason: Instruction limit % 18.34/3.41 % (1801415)Termination phase: Saturation % 18.34/3.41 % (1801415)Time elapsed: 0.073 s % 18.34/3.41 % (1801415)Peak memory usage: 90 MB % 18.34/3.41 % (1801415)Instructions burned: 76 (million) % 18.34/3.41 % (1801418)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1519928676:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 18.34/3.41 % (1801414)Instruction limit reached! % 18.34/3.41 % (1801414)------------------------------ % 18.34/3.41 % (1801414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.34/3.41 % (1801414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.34/3.41 % (1801414)CaDiCaL version: 2.1.3 % 18.34/3.41 % (1801414)Termination reason: Instruction limit % 18.34/3.41 % (1801414)Termination phase: Saturation % 18.34/3.41 % (1801414)Time elapsed: 0.133 s % 18.34/3.41 % (1801414)Peak memory usage: 134 MB % 18.34/3.41 % (1801414)Instructions burned: 71 (million) % 18.34/3.41 % (1801418)Instruction limit reached! % 18.34/3.41 % (1801418)------------------------------ % 18.34/3.41 % (1801418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.34/3.41 % (1801418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.34/3.41 % (1801418)CaDiCaL version: 2.1.3 % 18.34/3.41 % (1801418)Termination reason: Instruction limit % 18.34/3.41 % (1801418)Termination phase: Saturation % 18.34/3.41 % (1801418)Time elapsed: 0.079 s % 18.34/3.41 % (1801418)Peak memory usage: 116 MB % 18.34/3.41 % (1801418)Instructions burned: 130 (million) % 18.34/3.41 % (1801423)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3359438881:i=131:rtra=on_2984 on theBenchmark for (2984ds/131Mi) % 18.34/3.41 % (1801408)------------------------------ % 18.34/3.41 % (1801408)------------------------------ % 18.34/3.41 % (1801424)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2194475844:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 18.34/3.41 % (1801416)Instruction limit reached! % 18.34/3.41 % (1801416)------------------------------ % 18.34/3.41 % (1801416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (1801416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (1801416)CaDiCaL version: 2.1.3 % 19.93/3.85 % (1801416)Termination reason: Instruction limit % 19.93/3.85 % (1801416)Termination phase: Saturation % 19.93/3.85 % (1801416)Time elapsed: 0.294 s % 19.93/3.85 % (1801416)Peak memory usage: 90 MB % 19.93/3.85 % (1801416)Instructions burned: 294 (million) % 19.93/3.85 % (1801425)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3997727983:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 19.93/3.85 % (1801423)Instruction limit reached! % 19.93/3.85 % (1801423)------------------------------ % 19.93/3.85 % (1801423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (1801423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (1801423)CaDiCaL version: 2.1.3 % 19.93/3.85 % (1801423)Termination reason: Instruction limit % 19.93/3.85 % (1801423)Termination phase: Saturation % 19.93/3.85 % (1801423)Time elapsed: 0.122 s % 19.93/3.85 % (1801423)Peak memory usage: 133 MB % 19.93/3.85 % (1801423)Instructions burned: 131 (million) % 19.93/3.85 % (1801427)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=708531493:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 19.93/3.85 % (1801424)Instruction limit reached! % 19.93/3.85 % (1801424)------------------------------ % 19.93/3.85 % (1801424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (1801424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (1801424)CaDiCaL version: 2.1.3 % 19.93/3.85 % (1801424)Termination reason: Instruction limit % 19.93/3.85 % (1801424)Termination phase: Saturation % 19.93/3.85 % (1801424)Time elapsed: 0.108 s % 19.93/3.85 % (1801424)Peak memory usage: 134 MB % 19.93/3.85 % (1801424)Instructions burned: 40 (million) % 19.93/3.85 % (1801428)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1249945561:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 19.93/3.85 % (1801428)Instruction limit reached! % 19.93/3.85 % (1801428)------------------------------ % 19.93/3.85 % (1801428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (1801428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (1801428)CaDiCaL version: 2.1.3 % 19.93/3.85 % (1801428)Termination reason: Instruction limit % 19.93/3.85 % (1801428)Termination phase: Saturation % 19.93/3.85 % (1801428)Time elapsed: 0.089 s % 19.93/3.85 % (1801428)Peak memory usage: 118 MB % 19.93/3.85 % (1801428)Instructions burned: 132 (million) % 19.93/3.85 % (1801436)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=215438821:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 19.93/3.85 % (1801434)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=160494566:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2981 on theBenchmark for (2981ds/259Mi) % 19.93/3.85 % (1801435)dis+10_1_si=on:random_seed=2341356164:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 19.93/3.85 % (1801425)Instruction limit reached! % 19.93/3.85 % (1801425)------------------------------ % 19.93/3.85 % (1801425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (1801425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (1801425)CaDiCaL version: 2.1.3 % 19.93/3.85 % (1801425)Termination reason: Instruction limit % 19.93/3.85 % (1801425)Termination phase: Saturation % 19.93/3.85 % (1801425)Time elapsed: 0.267 s % 19.93/3.85 % (1801425)Peak memory usage: 91 MB % 19.93/3.85 % (1801425)Instructions burned: 308 (million) % 19.93/3.85 % (1801436)Instruction limit reached! % 19.93/3.85 % (1801436)------------------------------ % 19.93/3.85 % (1801436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (1801436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (1801436)CaDiCaL version: 2.1.3 % 19.93/3.85 % (1801436)Termination reason: Instruction limit % 19.93/3.85 % (1801436)Termination phase: Saturation % 19.93/3.85 % (1801436)Time elapsed: 0.185 s % 19.93/3.85 % (1801436)Peak memory usage: 95 MB % 19.93/3.85 % (1801436)Instructions burned: 384 (million) % 19.93/3.85 % (1801439)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3484633156:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 24.60/4.28 % (1801434)Instruction limit reached! % 24.60/4.28 % (1801434)------------------------------ % 24.60/4.28 % (1801434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.60/4.28 % (1801434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.60/4.28 % (1801434)CaDiCaL version: 2.1.3 % 24.60/4.28 % (1801434)Termination reason: Instruction limit % 24.60/4.28 % (1801434)Termination phase: Saturation % 24.60/4.28 % (1801434)Time elapsed: 0.249 s % 24.60/4.28 % (1801434)Peak memory usage: 116 MB % 24.60/4.28 % (1801434)Instructions burned: 259 (million) % 24.60/4.28 % (1801443)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1364565522:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 24.60/4.28 % (1801448)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1909501790:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 24.60/4.28 % (1801443)Refutation not found, incomplete strategy % 24.60/4.28 % (1801443)------------------------------ % 24.60/4.28 % (1801443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.60/4.28 % (1801443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.60/4.28 % (1801443)CaDiCaL version: 2.1.3 % 24.60/4.28 % (1801443)Termination reason: Refutation not found, incomplete strategy % 24.60/4.28 % (1801443)Time elapsed: 0.041 s % 24.60/4.28 % (1801443)Peak memory usage: 115 MB % 24.60/4.28 % (1801443)Instructions burned: 7 (million) % 24.60/4.28 % (1801439)Instruction limit reached! % 24.60/4.28 % (1801439)------------------------------ % 24.60/4.28 % (1801439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.60/4.28 % (1801439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.60/4.28 % (1801439)CaDiCaL version: 2.1.3 % 24.60/4.28 % (1801439)Termination reason: Instruction limit % 24.60/4.28 % (1801439)Termination phase: Saturation % 24.60/4.28 % (1801439)Time elapsed: 0.150 s % 24.60/4.28 % (1801439)Peak memory usage: 91 MB % 24.60/4.28 % (1801439)Instructions burned: 142 (million) % 24.60/4.28 % (1801448)Instruction limit reached! % 24.60/4.28 % (1801448)------------------------------ % 24.60/4.29 % (1801448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.60/4.29 % (1801448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.60/4.29 % (1801448)CaDiCaL version: 2.1.3 % 24.60/4.29 % (1801448)Termination reason: Instruction limit % 24.60/4.29 % (1801448)Termination phase: Saturation % 24.60/4.29 % (1801448)Time elapsed: 0.109 s % 24.60/4.29 % (1801448)Peak memory usage: 89 MB % 24.60/4.29 % (1801448)Instructions burned: 121 (million) % 24.60/4.29 % (1801450)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=2319408731:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 24.60/4.29 % (1801450)Instruction limit reached! % 24.60/4.29 % (1801450)------------------------------ % 24.60/4.29 % (1801450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.60/4.29 % (1801450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.60/4.29 % (1801450)CaDiCaL version: 2.1.3 % 24.60/4.29 % (1801450)Termination reason: Instruction limit % 24.60/4.29 % (1801450)Termination phase: Saturation % 24.60/4.29 % (1801450)Time elapsed: 0.097 s % 24.60/4.29 % (1801450)Peak memory usage: 117 MB % 24.60/4.29 % (1801450)Instructions burned: 128 (million) % 24.60/4.29 % (1801452)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=1497188354:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi) % 24.60/4.29 % (1801427)Instruction limit reached! % 24.60/4.29 % (1801427)------------------------------ % 24.60/4.29 % (1801427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.60/4.29 % (1801427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.60/4.29 % (1801427)CaDiCaL version: 2.1.3 % 24.60/4.29 % (1801427)Termination reason: Instruction limit % 24.60/4.29 % (1801427)Termination phase: Saturation % 24.60/4.29 % (1801427)Time elapsed: 0.713 s % 24.60/4.29 % (1801427)Peak memory usage: 137 MB % 24.60/4.29 % (1801427)Instructions burned: 598 (million) % 24.60/4.29 % (1801454)dis+1010_1_to=kbo:si=on:random_seed=2422156546:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 24.60/4.29 % (1801452)Instruction limit reached! % 27.23/4.83 % (1801452)------------------------------ % 27.23/4.83 % (1801452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.83 % (1801452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.83 % (1801452)CaDiCaL version: 2.1.3 % 27.23/4.83 % (1801452)Termination reason: Instruction limit % 27.23/4.83 % (1801452)Termination phase: Saturation % 27.23/4.83 % (1801452)Time elapsed: 0.073 s % 27.23/4.83 % (1801452)Peak memory usage: 115 MB % 27.23/4.83 % (1801452)Instructions burned: 39 (million) % 27.23/4.83 % (1801455)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3556802077:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 27.23/4.83 % (1801462)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=766846041:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 27.23/4.83 % (1801443)------------------------------ % 27.23/4.83 % (1801443)------------------------------ % 27.23/4.83 % (1801454)Instruction limit reached! % 27.23/4.83 % (1801454)------------------------------ % 27.23/4.83 % (1801454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.83 % (1801454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.83 % (1801454)CaDiCaL version: 2.1.3 % 27.23/4.83 % (1801454)Termination reason: Instruction limit % 27.23/4.83 % (1801454)Termination phase: Saturation % 27.23/4.83 % (1801454)Time elapsed: 0.186 s % 27.23/4.83 % (1801454)Peak memory usage: 91 MB % 27.23/4.83 % (1801454)Instructions burned: 175 (million) % 27.23/4.83 % (1801435)Instruction limit reached! % 27.23/4.83 % (1801435)------------------------------ % 27.23/4.83 % (1801435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.83 % (1801435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.83 % (1801435)CaDiCaL version: 2.1.3 % 27.23/4.83 % (1801435)Termination reason: Instruction limit % 27.23/4.83 % (1801435)Termination phase: Saturation % 27.23/4.83 % (1801435)Time elapsed: 0.853 s % 27.23/4.83 % (1801435)Peak memory usage: 94 MB % 27.23/4.83 % (1801435)Instructions burned: 1000 (million) % 27.23/4.83 % (1801470)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3227411788:thitd=on:i=215:nm=0:rtra=on:ev=force_2973 on theBenchmark for (2973ds/215Mi) % 27.23/4.83 % (1801474)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2381429905:i=349:rtra=on_2973 on theBenchmark for (2973ds/349Mi) % 27.23/4.83 % (1801462)Instruction limit reached! % 27.23/4.83 % (1801462)------------------------------ % 27.23/4.83 % (1801462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.83 % (1801462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.83 % (1801462)CaDiCaL version: 2.1.3 % 27.23/4.83 % (1801462)Termination reason: Instruction limit % 27.23/4.83 % (1801462)Termination phase: Saturation % 27.23/4.83 % (1801462)Time elapsed: 0.235 s % 27.23/4.83 % (1801462)Peak memory usage: 138 MB % 27.23/4.83 % (1801462)Instructions burned: 484 (million) % 27.23/4.83 % (1801474)Refutation not found, incomplete strategy % 27.23/4.83 % (1801474)------------------------------ % 27.23/4.83 % (1801474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.83 % (1801474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.83 % (1801474)CaDiCaL version: 2.1.3 % 27.23/4.83 % (1801474)Termination reason: Refutation not found, incomplete strategy % 27.23/4.83 % (1801474)Time elapsed: 0.042 s % 27.23/4.83 % (1801474)Peak memory usage: 116 MB % 27.23/4.83 % (1801474)Instructions burned: 7 (million) % 27.23/4.83 % (1801480)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1263997103:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 27.23/4.83 % (1801481)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3045392118:i=328:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/328Mi) % 27.23/4.83 % (1801455)Instruction limit reached! % 27.23/4.83 % (1801455)------------------------------ % 27.23/4.83 % (1801455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.23/4.83 % (1801455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.23/4.83 % (1801455)CaDiCaL version: 2.1.3 % 27.23/4.83 % (1801455)Termination reason: Instruction limit % 31.42/5.28 % (1801455)Termination phase: Saturation % 31.42/5.28 % (1801455)Time elapsed: 0.418 s % 31.42/5.28 % (1801455)Peak memory usage: 119 MB % 31.42/5.28 % (1801455)Instructions burned: 330 (million) % 31.42/5.28 % (1801485)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=4037887815:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi) % 31.42/5.28 % (1801487)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2302393736:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi) % 31.42/5.28 % (1801470)Instruction limit reached! % 31.42/5.28 % (1801470)------------------------------ % 31.42/5.28 % (1801470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.42/5.28 % (1801470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.42/5.28 % (1801470)CaDiCaL version: 2.1.3 % 31.42/5.28 % (1801470)Termination reason: Instruction limit % 31.42/5.28 % (1801470)Termination phase: Saturation % 31.42/5.28 % (1801470)Time elapsed: 0.275 s % 31.42/5.28 % (1801470)Peak memory usage: 136 MB % 31.42/5.28 % (1801470)Instructions burned: 216 (million) % 31.42/5.28 % (1801480)Instruction limit reached! % 31.42/5.28 % (1801480)------------------------------ % 31.42/5.28 % (1801480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.42/5.28 % (1801480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.42/5.28 % (1801480)CaDiCaL version: 2.1.3 % 31.42/5.28 % (1801480)Termination reason: Instruction limit % 31.42/5.28 % (1801480)Termination phase: Saturation % 31.42/5.28 % (1801480)Time elapsed: 0.271 s % 31.42/5.28 % (1801480)Peak memory usage: 90 MB % 31.42/5.28 % (1801480)Instructions burned: 295 (million) % 31.42/5.28 % (1801493)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3236646902:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi) % 31.42/5.28 % (1801474)------------------------------ % 31.42/5.28 % (1801474)------------------------------ % 31.42/5.28 % (1801481)Instruction limit reached! % 31.42/5.28 % (1801481)------------------------------ % 31.42/5.28 % (1801481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.42/5.28 % (1801481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.42/5.28 % (1801481)CaDiCaL version: 2.1.3 % 31.42/5.28 % (1801481)Termination reason: Instruction limit % 31.42/5.28 % (1801481)Termination phase: Saturation % 31.42/5.28 % (1801481)Time elapsed: 0.360 s % 31.42/5.28 % (1801481)Peak memory usage: 118 MB % 31.42/5.28 % (1801481)Instructions burned: 329 (million) % 31.42/5.28 % (1801493)Instruction limit reached! % 31.42/5.28 % (1801493)------------------------------ % 31.42/5.28 % (1801493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.42/5.28 % (1801493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.42/5.28 % (1801493)CaDiCaL version: 2.1.3 % 31.42/5.28 % (1801493)Termination reason: Instruction limit % 31.42/5.28 % (1801493)Termination phase: Saturation % 31.42/5.28 % (1801493)Time elapsed: 0.159 s % 31.42/5.28 % (1801493)Peak memory usage: 114 MB % 31.42/5.28 % (1801493)Instructions burned: 322 (million) % 31.42/5.28 % (1801497)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1754952319:i=416:rtra=on:gtg=position:ss=axioms_2967 on theBenchmark for (2967ds/416Mi) % 31.42/5.28 % (1801485)Instruction limit reached! % 31.42/5.28 % (1801485)------------------------------ % 31.42/5.28 % (1801485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.42/5.28 % (1801485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.42/5.28 % (1801485)CaDiCaL version: 2.1.3 % 31.42/5.28 % (1801485)Termination reason: Instruction limit % 31.42/5.28 % (1801485)Termination phase: Saturation % 31.42/5.28 % (1801485)Time elapsed: 0.310 s % 31.42/5.28 % (1801485)Peak memory usage: 119 MB % 31.42/5.28 % (1801485)Instructions burned: 282 (million) % 31.42/5.28 % (1801497)Refutation not found, incomplete strategy % 31.42/5.28 % (1801497)------------------------------ % 31.42/5.28 % (1801497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.42/5.28 % (1801497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.42/5.28 % (1801497)CaDiCaL version: 2.1.3 % 31.42/5.28 % (1801497)Termination reason: Refutation not found, incomplete strategy % 31.42/5.28 % (1801497)Time elapsed: 0.041 s % 31.42/5.28 % (1801497)Peak memory usage: 116 MB % 31.42/5.28 % (1801497)Instructions burned: 7 (million) % 31.42/5.28 % (1801500)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=846132451:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 33.29/5.93 % (1801502)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=1212368801:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 33.29/5.93 % (1801487)Instruction limit reached! % 33.29/5.93 % (1801487)------------------------------ % 33.29/5.93 % (1801487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.29/5.93 % (1801487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.29/5.93 % (1801487)CaDiCaL version: 2.1.3 % 33.29/5.93 % (1801487)Termination reason: Instruction limit % 33.29/5.93 % (1801487)Termination phase: Saturation % 33.29/5.93 % (1801487)Time elapsed: 0.472 s % 33.29/5.93 % (1801487)Peak memory usage: 92 MB % 33.29/5.93 % (1801487)Instructions burned: 485 (million) % 33.29/5.93 % (1801505)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2767153682:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/387Mi) % 33.29/5.93 % (1801503)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3588990006:i=375:kws=inv_arity_squared:rtra=on_2965 on theBenchmark for (2965ds/375Mi) % 33.29/5.93 % (1801507)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2433193795:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi) % 33.29/5.93 % (1801505)Instruction limit reached! % 33.29/5.93 % (1801505)------------------------------ % 33.29/5.93 % (1801505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.29/5.93 % (1801505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.29/5.93 % (1801505)CaDiCaL version: 2.1.3 % 33.29/5.93 % (1801505)Termination reason: Instruction limit % 33.29/5.93 % (1801505)Termination phase: Saturation % 33.29/5.93 % (1801505)Time elapsed: 0.170 s % 33.29/5.93 % (1801505)Peak memory usage: 119 MB % 33.29/5.93 % (1801505)Instructions burned: 389 (million) % 33.29/5.93 % (1801497)------------------------------ % 33.29/5.93 % (1801497)------------------------------ % 33.29/5.93 % (1801514)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=479159869:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi) % 33.29/5.93 % (1801502)Instruction limit reached! % 33.29/5.93 % (1801502)------------------------------ % 33.29/5.93 % (1801502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.29/5.93 % (1801502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.29/5.93 % (1801502)CaDiCaL version: 2.1.3 % 33.29/5.93 % (1801502)Termination reason: Instruction limit % 33.29/5.93 % (1801502)Termination phase: Saturation % 33.29/5.93 % (1801502)Time elapsed: 0.349 s % 33.29/5.93 % (1801502)Peak memory usage: 135 MB % 33.29/5.93 % (1801502)Instructions burned: 276 (million) % 33.29/5.93 % (1801500)Instruction limit reached! % 33.29/5.93 % (1801500)------------------------------ % 33.29/5.93 % (1801500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.29/5.93 % (1801500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.29/5.93 % (1801500)CaDiCaL version: 2.1.3 % 33.29/5.93 % (1801500)Termination reason: Instruction limit % 33.29/5.93 % (1801500)Termination phase: Saturation % 33.29/5.93 % (1801500)Time elapsed: 0.471 s % 33.29/5.93 % (1801500)Peak memory usage: 119 MB % 33.29/5.93 % (1801500)Instructions burned: 472 (million) % 33.29/5.93 % (1801519)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=362636251:i=359:rtra=on:gtg=exists_top:ss=axioms_2961 on theBenchmark for (2961ds/359Mi) % 33.29/5.93 % (1801519)Refutation not found, incomplete strategy % 33.29/5.93 % (1801519)------------------------------ % 33.29/5.93 % (1801519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.29/5.93 % (1801519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.29/5.93 % (1801519)CaDiCaL version: 2.1.3 % 33.29/5.93 % (1801519)Termination reason: Refutation not found, incomplete strategy % 33.29/5.93 % (1801519)Time elapsed: 0.003 s % 33.29/5.93 % (1801519)Peak memory usage: 89 MB % 33.29/5.93 % (1801519)Instructions burned: 2 (million) % 33.29/5.93 % (1801503)Instruction limit reached! % 33.29/5.93 % (1801503)------------------------------ % 40.14/6.58 % (1801503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.14/6.58 % (1801503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.14/6.58 % (1801503)CaDiCaL version: 2.1.3 % 40.14/6.58 % (1801503)Termination reason: Instruction limit % 40.14/6.58 % (1801503)Termination phase: Saturation % 40.14/6.58 % (1801503)Time elapsed: 0.393 s % 40.14/6.58 % (1801503)Peak memory usage: 118 MB % 40.14/6.58 % (1801503)Instructions burned: 376 (million) % 40.14/6.58 % (1801520)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3422979996:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 40.14/6.58 % (1801524)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=3201488966:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/235Mi) % 40.14/6.58 % (1801519)------------------------------ % 40.14/6.58 % (1801519)------------------------------ % 40.14/6.58 % (1801523)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2267107256:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 40.14/6.58 % (1801507)Instruction limit reached! % 40.14/6.58 % (1801507)------------------------------ % 40.14/6.58 % (1801507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.14/6.58 % (1801507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.14/6.58 % (1801507)CaDiCaL version: 2.1.3 % 40.14/6.58 % (1801507)Termination reason: Instruction limit % 40.14/6.58 % (1801507)Termination phase: Saturation % 40.14/6.58 % (1801507)Time elapsed: 0.518 s % 40.14/6.58 % (1801507)Peak memory usage: 93 MB % 40.14/6.58 % (1801507)Instructions burned: 514 (million) % 40.14/6.58 % (1801514)Instruction limit reached! % 40.14/6.58 % (1801514)------------------------------ % 40.14/6.58 % (1801514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.14/6.58 % (1801514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.14/6.58 % (1801514)CaDiCaL version: 2.1.3 % 40.14/6.58 % (1801514)Termination reason: Instruction limit % 40.14/6.58 % (1801514)Termination phase: Saturation % 40.14/6.58 % (1801514)Time elapsed: 0.344 s % 40.14/6.58 % (1801514)Peak memory usage: 133 MB % 40.14/6.58 % (1801514)Instructions burned: 335 (million) % 40.14/6.58 % (1801525)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3406230403:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 40.14/6.58 % (1801528)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=104080854:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi) % 40.14/6.58 % (1801524)Instruction limit reached! % 40.14/6.58 % (1801524)------------------------------ % 40.14/6.58 % (1801524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.14/6.58 % (1801524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.14/6.58 % (1801524)CaDiCaL version: 2.1.3 % 40.14/6.58 % (1801524)Termination reason: Instruction limit % 40.14/6.58 % (1801524)Termination phase: Saturation % 40.14/6.58 % (1801524)Time elapsed: 0.239 s % 40.14/6.58 % (1801524)Peak memory usage: 116 MB % 40.14/6.58 % (1801524)Instructions burned: 235 (million) % 40.14/6.58 % (1801528)Instruction limit reached! % 40.14/6.58 % (1801528)------------------------------ % 40.14/6.58 % (1801528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.14/6.58 % (1801528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.14/6.58 % (1801528)CaDiCaL version: 2.1.3 % 40.14/6.58 % (1801528)Termination reason: Instruction limit % 40.14/6.58 % (1801528)Termination phase: Saturation % 40.14/6.58 % (1801528)Time elapsed: 0.053 s % 40.14/6.58 % (1801528)Peak memory usage: 90 MB % 40.14/6.58 % (1801528)Instructions burned: 148 (million) % 40.14/6.58 % (1801523)Instruction limit reached! % 40.14/6.58 % (1801523)------------------------------ % 40.14/6.58 % (1801523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.14/6.58 % (1801523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.14/6.58 % (1801523)CaDiCaL version: 2.1.3 % 40.14/6.58 % (1801523)Termination reason: Instruction limit % 40.14/6.58 % (1801523)Termination phase: Saturation % 40.14/6.58 % (1801523)Time elapsed: 0.243 s % 40.14/6.58 % (1801523)Peak memory usage: 116 MB % 47.37/7.50 % (1801523)Instructions burned: 263 (million) % 47.37/7.50 % (1801530)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1185094109:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi) % 47.37/7.50 % (1801520)Instruction limit reached! % 47.37/7.50 % (1801520)------------------------------ % 47.37/7.50 % (1801520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.37/7.50 % (1801520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.37/7.50 % (1801520)CaDiCaL version: 2.1.3 % 47.37/7.50 % (1801520)Termination reason: Instruction limit % 47.37/7.50 % (1801520)Termination phase: Saturation % 47.37/7.50 % (1801520)Time elapsed: 0.358 s % 47.37/7.50 % (1801520)Peak memory usage: 121 MB % 47.37/7.50 % (1801520)Instructions burned: 341 (million) % 47.37/7.50 % (1801531)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=2158397740:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi) % 47.37/7.50 % (1801537)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=852344538:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2954 on theBenchmark for (2954ds/655Mi) % 47.37/7.50 % (1801525)Instruction limit reached! % 47.37/7.50 % (1801525)------------------------------ % 47.37/7.50 % (1801525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.37/7.50 % (1801525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.37/7.50 % (1801525)CaDiCaL version: 2.1.3 % 47.37/7.50 % (1801525)Termination reason: Instruction limit % 47.37/7.50 % (1801525)Termination phase: Saturation % 47.37/7.50 % (1801525)Time elapsed: 0.301 s % 47.37/7.50 % (1801525)Peak memory usage: 92 MB % 47.37/7.50 % (1801525)Instructions burned: 273 (million) % 47.37/7.50 % (1801535)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1650304264:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 47.37/7.50 % (1801539)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=33967594:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1054Mi) % 47.37/7.50 % (1801540)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=181164287:i=107:rtra=on_2954 on theBenchmark for (2954ds/107Mi) % 47.37/7.50 % (1801540)Refutation not found, incomplete strategy % 47.37/7.50 % (1801540)------------------------------ % 47.37/7.50 % (1801540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.37/7.50 % (1801540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.37/7.50 % (1801540)CaDiCaL version: 2.1.3 % 47.37/7.50 % (1801540)Termination reason: Refutation not found, incomplete strategy % 47.37/7.50 % (1801540)Time elapsed: 0.041 s % 47.37/7.50 % (1801540)Peak memory usage: 116 MB % 47.37/7.50 % (1801540)Instructions burned: 7 (million) % 47.37/7.50 % (1801543)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3802765048:s2a=on:i=450:doe=on:nm=32:rtra=on_2953 on theBenchmark for (2953ds/450Mi) % 47.37/7.50 % (1801531)Instruction limit reached! % 47.37/7.50 % (1801531)------------------------------ % 47.37/7.50 % (1801531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.37/7.50 % (1801531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.37/7.50 % (1801531)CaDiCaL version: 2.1.3 % 47.37/7.50 % (1801531)Termination reason: Instruction limit % 47.37/7.50 % (1801531)Termination phase: Saturation % 47.37/7.50 % (1801531)Time elapsed: 0.349 s % 47.37/7.50 % (1801531)Peak memory usage: 136 MB % 47.37/7.50 % (1801531)Instructions burned: 277 (million) % 47.37/7.50 % (1801537)Instruction limit reached! % 47.37/7.50 % (1801537)------------------------------ % 47.37/7.50 % (1801537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.37/7.50 % (1801537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.37/7.50 % (1801537)CaDiCaL version: 2.1.3 % 47.37/7.50 % (1801537)Termination reason: Instruction limit % 47.37/7.50 % (1801537)Termination phase: Saturation % 47.37/7.50 % (1801537)Time elapsed: 0.336 s % 47.37/7.50 % (1801537)Peak memory usage: 95 MB % 47.37/7.50 % (1801537)Instructions burned: 657 (million) % 47.37/7.50 % (1801550)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 % 50.05/7.96 % (1801550)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2327362689:i=1090:aac=none:nm=0:rtra=on:rawr=on_2950 on theBenchmark for (2950ds/1090Mi) % 50.05/7.96 % (1801540)------------------------------ % 50.05/7.96 % (1801540)------------------------------ % 50.05/7.96 % (1801551)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3749776503:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2950 on theBenchmark for (2950ds/130Mi) % 50.05/7.96 % (1801551)Instruction limit reached! % 50.05/7.96 % (1801551)------------------------------ % 50.05/7.96 % (1801551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.05/7.96 % (1801551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.05/7.96 % (1801551)CaDiCaL version: 2.1.3 % 50.05/7.96 % (1801551)Termination reason: Instruction limit % 50.05/7.96 % (1801551)Termination phase: Saturation % 50.05/7.96 % (1801551)Time elapsed: 0.143 s % 50.05/7.96 % (1801551)Peak memory usage: 116 MB % 50.05/7.96 % (1801551)Instructions burned: 130 (million) % 50.05/7.96 % (1801543)Instruction limit reached! % 50.05/7.96 % (1801543)------------------------------ % 50.05/7.96 % (1801543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.05/7.96 % (1801543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.05/7.96 % (1801543)CaDiCaL version: 2.1.3 % 50.05/7.96 % (1801543)Termination reason: Instruction limit % 50.05/7.96 % (1801543)Termination phase: Saturation % 50.05/7.96 % (1801543)Time elapsed: 0.510 s % 50.05/7.96 % (1801543)Peak memory usage: 137 MB % 50.05/7.96 % (1801543)Instructions burned: 450 (million) % 50.05/7.96 % (1801557)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2910262787:i=312:kws=inv_frequency:nm=20:rtra=on_2947 on theBenchmark for (2947ds/312Mi) % 50.05/7.96 % (1801535)Instruction limit reached! % 50.05/7.96 % (1801535)------------------------------ % 50.05/7.96 % (1801535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.05/7.96 % (1801535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.05/7.96 % (1801535)CaDiCaL version: 2.1.3 % 50.05/7.96 % (1801535)Termination reason: Instruction limit % 50.05/7.96 % (1801535)Termination phase: Saturation % 50.05/7.96 % (1801535)Time elapsed: 0.825 s % 50.05/7.96 % (1801535)Peak memory usage: 90 MB % 50.05/7.96 % (1801535)Instructions burned: 1053 (million) % 50.05/7.96 % (1801557)Instruction limit reached! % 50.05/7.96 % (1801557)------------------------------ % 50.05/7.96 % (1801557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.05/7.96 % (1801557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.05/7.96 % (1801557)CaDiCaL version: 2.1.3 % 50.05/7.96 % (1801557)Termination reason: Instruction limit % 50.05/7.96 % (1801557)Termination phase: Saturation % 50.05/7.96 % (1801557)Time elapsed: 0.186 s % 50.05/7.96 % (1801557)Peak memory usage: 118 MB % 50.05/7.96 % (1801557)Instructions burned: 313 (million) % 50.05/7.96 % (1801559)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2747684891:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 50.05/7.96 % (1801560)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=179294249:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 50.05/7.96 % (1801539)Instruction limit reached! % 50.05/7.96 % (1801539)------------------------------ % 50.05/7.96 % (1801539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.05/7.96 % (1801539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.05/7.96 % (1801539)CaDiCaL version: 2.1.3 % 50.05/7.96 % (1801539)Termination reason: Instruction limit % 50.05/7.96 % (1801539)Termination phase: Saturation % 50.05/7.96 % (1801539)Time elapsed: 0.953 s % 50.05/7.96 % (1801539)Peak memory usage: 93 MB % 50.05/7.96 % (1801539)Instructions burned: 1055 (million) % 50.05/7.96 % (1801562)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3029666892:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2944 on theBenchmark for (2944ds/307Mi) % 50.05/7.96 % (1801562)Refutation not found, incomplete strategy % 50.05/7.96 % (1801562)------------------------------ % 50.05/7.96 % (1801562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.05/7.96 % (1801562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.05/7.96 % (1801562)CaDiCaL version: 2.1.3 % 56.68/9.01 % (1801562)Termination reason: Refutation not found, incomplete strategy % 56.68/9.01 % (1801562)Time elapsed: 0.005 s % 56.68/9.01 % (1801562)Peak memory usage: 89 MB % 56.68/9.01 % (1801562)Instructions burned: 2 (million) % 56.68/9.01 % (1801550)Instruction limit reached! % 56.68/9.01 % (1801550)------------------------------ % 56.68/9.01 % (1801550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.68/9.01 % (1801550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.68/9.01 % (1801550)CaDiCaL version: 2.1.3 % 56.68/9.01 % (1801550)Termination reason: Instruction limit % 56.68/9.01 % (1801550)Termination phase: Saturation % 56.68/9.01 % (1801550)Time elapsed: 0.711 s % 56.68/9.01 % (1801550)Peak memory usage: 127 MB % 56.68/9.01 % (1801550)Instructions burned: 1091 (million) % 56.68/9.01 % (1801563)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2702216620:i=776:doe=on:rtra=on_2943 on theBenchmark for (2943ds/776Mi) % 56.68/9.01 % (1801566)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=354671058:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2942 on theBenchmark for (2942ds/646Mi) % 56.68/9.01 % (1801569)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=464597436:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2940 on theBenchmark for (2940ds/784Mi) % 56.68/9.01 % (1801559)Instruction limit reached! % 56.68/9.01 % (1801559)------------------------------ % 56.68/9.01 % (1801559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.68/9.01 % (1801559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.68/9.01 % (1801559)CaDiCaL version: 2.1.3 % 56.68/9.01 % (1801559)Termination reason: Instruction limit % 56.68/9.01 % (1801559)Termination phase: Saturation % 56.68/9.01 % (1801559)Time elapsed: 0.471 s % 56.68/9.01 % (1801559)Peak memory usage: 92 MB % 56.68/9.01 % (1801559)Instructions burned: 492 (million) % 56.68/9.01 % (1801562)------------------------------ % 56.68/9.01 % (1801562)------------------------------ % 56.68/9.01 % (1801563)Instruction limit reached! % 56.68/9.01 % (1801563)------------------------------ % 56.68/9.01 % (1801563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.68/9.01 % (1801563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.68/9.01 % (1801563)CaDiCaL version: 2.1.3 % 56.68/9.01 % (1801563)Termination reason: Instruction limit % 56.68/9.01 % (1801563)Termination phase: Saturation % 56.68/9.01 % (1801563)Time elapsed: 0.414 s % 56.68/9.01 % (1801563)Peak memory usage: 122 MB % 56.68/9.01 % (1801563)Instructions burned: 776 (million) % 56.68/9.01 % (1801572)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=2105239532:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi) % 56.68/9.01 % (1801560)Instruction limit reached! % 56.68/9.01 % (1801560)------------------------------ % 56.68/9.01 % (1801560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.68/9.01 % (1801560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.68/9.01 % (1801560)CaDiCaL version: 2.1.3 % 56.68/9.01 % (1801560)Termination reason: Instruction limit % 56.68/9.01 % (1801560)Termination phase: Saturation % 56.68/9.01 % (1801560)Time elapsed: 0.778 s % 56.68/9.01 % (1801560)Peak memory usage: 93 MB % 56.68/9.01 % (1801560)Instructions burned: 836 (million) % 56.68/9.01 % (1801573)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=2323668029:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi) % 56.68/9.01 % (1801574)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1213034626:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2936 on theBenchmark for (2936ds/775Mi) % 56.68/9.01 % (1801573)Instruction limit reached! % 56.68/9.01 % (1801573)------------------------------ % 56.68/9.01 % (1801573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.68/9.01 % (1801573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.68/9.01 % (1801573)CaDiCaL version: 2.1.3 % 56.68/9.01 % (1801573)Termination reason: Instruction limit % 56.68/9.01 % (1801573)Termination phase: Saturation % 56.68/9.01 % (1801573)Time elapsed: 0.240 s % 56.68/9.01 % (1801573)Peak memory usage: 116 MB % 70.84/10.87 % (1801573)Instructions burned: 246 (million) % 70.84/10.87 % (1801566)Instruction limit reached! % 70.84/10.87 % (1801566)------------------------------ % 70.84/10.87 % (1801566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.84/10.87 % (1801566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.84/10.87 % (1801566)CaDiCaL version: 2.1.3 % 70.84/10.87 % (1801566)Termination reason: Instruction limit % 70.84/10.87 % (1801566)Termination phase: Saturation % 70.84/10.87 % (1801566)Time elapsed: 0.753 s % 70.84/10.87 % (1801566)Peak memory usage: 138 MB % 70.84/10.87 % (1801566)Instructions burned: 646 (million) % 70.84/10.87 % (1801582)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=137879098:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2934 on theBenchmark for (2934ds/273Mi) % 70.84/10.87 % (1801569)Instruction limit reached! % 70.84/10.87 % (1801569)------------------------------ % 70.84/10.87 % (1801569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.84/10.87 % (1801569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.84/10.87 % (1801569)CaDiCaL version: 2.1.3 % 70.84/10.87 % (1801569)Termination reason: Instruction limit % 70.84/10.87 % (1801569)Termination phase: Saturation % 70.84/10.87 % (1801569)Time elapsed: 0.814 s % 70.84/10.87 % (1801569)Peak memory usage: 122 MB % 70.84/10.87 % (1801569)Instructions burned: 785 (million) % 70.84/10.87 % (1801574)Instruction limit reached! % 70.84/10.87 % (1801574)------------------------------ % 70.84/10.87 % (1801574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.84/10.87 % (1801574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.84/10.87 % (1801574)CaDiCaL version: 2.1.3 % 70.84/10.87 % (1801574)Termination reason: Instruction limit % 70.84/10.87 % (1801574)Termination phase: Saturation % 70.84/10.87 % (1801574)Time elapsed: 0.452 s % 70.84/10.87 % (1801574)Peak memory usage: 95 MB % 70.84/10.87 % (1801574)Instructions burned: 776 (million) % 70.84/10.87 % (1801583)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1129402209:i=102:nm=16:rtra=on_2932 on theBenchmark for (2932ds/102Mi) % 70.84/10.87 % (1801584)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=859581902:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2932 on theBenchmark for (2932ds/1094Mi) % 70.84/10.87 % (1801583)Instruction limit reached! % 70.84/10.87 % (1801583)------------------------------ % 70.84/10.87 % (1801583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.84/10.87 % (1801583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.84/10.87 % (1801583)CaDiCaL version: 2.1.3 % 70.84/10.87 % (1801583)Termination reason: Instruction limit % 70.84/10.87 % (1801583)Termination phase: Saturation % 70.84/10.87 % (1801583)Time elapsed: 0.091 s % 70.84/10.87 % (1801583)Peak memory usage: 89 MB % 70.84/10.87 % (1801583)Instructions burned: 102 (million) % 70.84/10.87 % (1801582)Instruction limit reached! % 70.84/10.87 % (1801582)------------------------------ % 70.84/10.87 % (1801582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.84/10.87 % (1801582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.84/10.87 % (1801582)CaDiCaL version: 2.1.3 % 70.84/10.87 % (1801582)Termination reason: Instruction limit % 70.84/10.87 % (1801582)Termination phase: Saturation % 70.84/10.87 % (1801582)Time elapsed: 0.303 s % 70.84/10.87 % (1801582)Peak memory usage: 92 MB % 70.84/10.87 % (1801582)Instructions burned: 276 (million) % 70.84/10.87 % (1801587)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=1611082749:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/868Mi) % 70.84/10.87 % (1801586)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=190969597:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 70.84/10.87 % (1801587)Refutation not found, incomplete strategy % 70.84/10.87 % (1801587)------------------------------ % 70.84/10.87 % (1801587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.84/10.87 % (1801587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.84/10.87 % (1801587)CaDiCaL version: 2.1.3 % 70.84/10.87 % (1801587)Termination reason: Refutation not found, incomplete strategy % 70.84/10.87 % (1801587)Time elapsed: 0.028 s % 70.84/10.87 % (1801587)Peak memory usage: 116 MB % 70.84/10.87 % (1801587)Instructions burned: 13 (million) % 87.31/13.12 % (1801590)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=392491380:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi) % 87.31/13.12 % (1801591)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2229716713:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2928 on theBenchmark for (2928ds/36816Mi) % 87.31/13.12 % (1801591)Refutation not found, incomplete strategy % 87.31/13.12 % (1801591)------------------------------ % 87.31/13.12 % (1801591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.31/13.12 % (1801591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.31/13.12 % (1801591)CaDiCaL version: 2.1.3 % 87.31/13.12 % (1801591)Termination reason: Refutation not found, incomplete strategy % 87.31/13.12 % (1801591)Time elapsed: 0.003 s % 87.31/13.12 % (1801591)Peak memory usage: 88 MB % 87.31/13.12 % (1801591)Instructions burned: 1 (million) % 87.31/13.12 % (1801587)------------------------------ % 87.31/13.12 % (1801587)------------------------------ % 87.31/13.12 % (1801572)Instruction limit reached! % 87.31/13.12 % (1801572)------------------------------ % 87.31/13.12 % (1801572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.31/13.12 % (1801572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.31/13.12 % (1801572)CaDiCaL version: 2.1.3 % 87.31/13.12 % (1801572)Termination reason: Instruction limit % 87.31/13.12 % (1801572)Termination phase: Saturation % 87.31/13.12 % (1801572)Time elapsed: 1.149 s % 87.31/13.12 % (1801572)Peak memory usage: 126 MB % 87.31/13.12 % (1801572)Instructions burned: 1132 (million) % 87.31/13.12 % (1801598)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=247232808:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2925 on theBenchmark for (2925ds/273Mi) % 87.31/13.12 % (1801591)------------------------------ % 87.31/13.12 % (1801591)------------------------------ % 87.31/13.12 % (1801598)Instruction limit reached! % 87.31/13.12 % (1801598)------------------------------ % 87.31/13.12 % (1801598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.31/13.12 % (1801598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.31/13.12 % (1801598)CaDiCaL version: 2.1.3 % 87.31/13.12 % (1801598)Termination reason: Instruction limit % 87.31/13.12 % (1801598)Termination phase: Saturation % 87.31/13.12 % (1801598)Time elapsed: 0.160 s % 87.31/13.12 % (1801598)Peak memory usage: 92 MB % 87.31/13.12 % (1801598)Instructions burned: 273 (million) % 87.31/13.12 % (1801599)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=68131623:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2923 on theBenchmark for (2923ds/863Mi) % 87.31/13.12 % (1801599)Refutation not found, incomplete strategy % 87.31/13.12 % (1801599)------------------------------ % 87.31/13.12 % (1801599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.31/13.12 % (1801599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.31/13.12 % (1801599)CaDiCaL version: 2.1.3 % 87.31/13.12 % (1801599)Termination reason: Refutation not found, incomplete strategy % 87.31/13.12 % (1801599)Time elapsed: 0.050 s % 87.31/13.12 % (1801599)Peak memory usage: 116 MB % 87.31/13.12 % (1801599)Instructions burned: 13 (million) % 87.31/13.12 % (1801584)Instruction limit reached! % 87.31/13.12 % (1801584)------------------------------ % 87.31/13.12 % (1801584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.31/13.12 % (1801584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.31/13.12 % (1801584)CaDiCaL version: 2.1.3 % 87.31/13.12 % (1801584)Termination reason: Instruction limit % 87.31/13.12 % (1801584)Termination phase: Saturation % 87.31/13.12 % (1801584)Time elapsed: 0.939 s % 87.31/13.12 % (1801584)Peak memory usage: 91 MB % 87.31/13.12 % (1801584)Instructions burned: 1095 (million) % 87.31/13.12 % (1801602)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=2269814230:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2921 on theBenchmark for (2921ds/2216Mi) % 87.31/13.12 % (1801601)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=559663087:i=5811:kws=precedence:nm=0:rtra=on_2921 on theBenchmark for (2921ds/5811Mi) % 87.31/13.12 % (1801605)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2524951082:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2919 on theBenchmark for (2919ds/801Mi) % 106.21/15.80 % (1801599)------------------------------ % 106.21/15.80 % (1801599)------------------------------ % 106.21/15.80 % (1801616)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3843043697:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2917 on theBenchmark for (2917ds/1026Mi) % 106.21/15.80 % (1801530)Instruction limit reached! % 106.21/15.80 % (1801530)------------------------------ % 106.21/15.80 % (1801530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.21/15.80 % (1801530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.21/15.80 % (1801530)CaDiCaL version: 2.1.3 % 106.21/15.80 % (1801530)Termination reason: Instruction limit % 106.21/15.80 % (1801530)Termination phase: Saturation % 106.21/15.80 % (1801530)Time elapsed: 4.087 s % 106.21/15.80 % (1801530)Peak memory usage: 110 MB % 106.21/15.80 % (1801530)Instructions burned: 4428 (million) % 106.21/15.80 % (1801605)Instruction limit reached! % 106.21/15.80 % (1801605)------------------------------ % 106.21/15.80 % (1801605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.21/15.80 % (1801605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.21/15.80 % (1801605)CaDiCaL version: 2.1.3 % 106.21/15.80 % (1801605)Termination reason: Instruction limit % 106.21/15.80 % (1801605)Termination phase: Saturation % 106.21/15.80 % (1801605)Time elapsed: 0.625 s % 106.21/15.80 % (1801605)Peak memory usage: 92 MB % 106.21/15.80 % (1801605)Instructions burned: 801 (million) % 106.21/15.80 % (1801618)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2397885619:i=3509:rtra=on_2913 on theBenchmark for (2913ds/3509Mi) % 106.21/15.80 % (1801602)Instruction limit reached! % 106.21/15.80 % (1801602)------------------------------ % 106.21/15.80 % (1801602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.21/15.80 % (1801602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.21/15.80 % (1801602)CaDiCaL version: 2.1.3 % 106.21/15.80 % (1801602)Termination reason: Instruction limit % 106.21/15.80 % (1801602)Termination phase: Saturation % 106.21/15.80 % (1801602)Time elapsed: 0.983 s % 106.21/15.80 % (1801602)Peak memory usage: 126 MB % 106.21/15.80 % (1801602)Instructions burned: 2218 (million) % 106.21/15.80 % (1801590)Instruction limit reached! % 106.21/15.80 % (1801590)------------------------------ % 106.21/15.80 % (1801590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.21/15.80 % (1801590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.21/15.80 % (1801590)CaDiCaL version: 2.1.3 % 106.21/15.80 % (1801590)Termination reason: Instruction limit % 106.21/15.80 % (1801590)Termination phase: Saturation % 106.21/15.80 % (1801590)Time elapsed: 1.716 s % 106.21/15.80 % (1801590)Peak memory usage: 97 MB % 106.21/15.80 % (1801590)Instructions burned: 1847 (million) % 106.21/15.80 % (1801619)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3664746679:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/2127Mi) % 106.21/15.80 % (1801621)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=443428305:i=1959:rtra=on:fsd=on:proc=on_2909 on theBenchmark for (2909ds/1959Mi) % 106.21/15.80 % (1801622)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1615005729:s2a=on:i=3553:nm=0:rtra=on_2909 on theBenchmark for (2909ds/3553Mi) % 106.21/15.80 % (1801616)Instruction limit reached! % 106.21/15.80 % (1801616)------------------------------ % 106.21/15.80 % (1801616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.21/15.80 % (1801616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.21/15.80 % (1801616)CaDiCaL version: 2.1.3 % 106.21/15.80 % (1801616)Termination reason: Instruction limit % 106.21/15.80 % (1801616)Termination phase: Saturation % 106.21/15.80 % (1801616)Time elapsed: 0.877 s % 106.21/15.80 % (1801616)Peak memory usage: 93 MB % 106.21/15.80 % (1801616)Instructions burned: 1026 (million) % 106.21/15.80 % (1801626)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4037106114:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2905 on theBenchmark for (2905ds/3201Mi) % 106.21/15.80 % (1801621)Instruction limit reached! % 106.21/15.80 % (1801621)------------------------------ % 106.21/15.80 % (1801621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.21/15.80 % (1801621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.91 % (1801621)CaDiCaL version: 2.1.3 % 157.24/22.91 % (1801621)Termination reason: Instruction limit % 157.24/22.91 % (1801621)Termination phase: Saturation % 157.24/22.91 % (1801621)Time elapsed: 0.856 s % 157.24/22.91 % (1801621)Peak memory usage: 119 MB % 157.24/22.91 % (1801621)Instructions burned: 1959 (million) % 157.24/22.91 % (1801628)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=1809128931:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2898 on theBenchmark for (2898ds/4093Mi) % 157.24/22.91 % (1801619)Instruction limit reached! % 157.24/22.91 % (1801619)------------------------------ % 157.24/22.91 % (1801619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.24/22.91 % (1801619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.91 % (1801619)CaDiCaL version: 2.1.3 % 157.24/22.91 % (1801619)Termination reason: Instruction limit % 157.24/22.91 % (1801619)Termination phase: Saturation % 157.24/22.91 % (1801619)Time elapsed: 1.785 s % 157.24/22.91 % (1801619)Peak memory usage: 101 MB % 157.24/22.91 % (1801619)Instructions burned: 2127 (million) % 157.24/22.91 % (1801630)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=599359993:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2890 on theBenchmark for (2890ds/21173Mi) % 157.24/22.91 % (1801626)Refutation not found, incomplete strategy % 157.24/22.91 % (1801626)------------------------------ % 157.24/22.91 % (1801626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.24/22.91 % (1801626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.91 % (1801626)CaDiCaL version: 2.1.3 % 157.24/22.91 % (1801626)Termination reason: Refutation not found, incomplete strategy % 157.24/22.91 % (1801626)Time elapsed: 1.682 s % 157.24/22.91 % (1801626)Peak memory usage: 95 MB % 157.24/22.91 % (1801626)Instructions burned: 2175 (million) % 157.24/22.91 % (1801618)Instruction limit reached! % 157.24/22.91 % (1801618)------------------------------ % 157.24/22.91 % (1801618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.24/22.91 % (1801618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.91 % (1801618)CaDiCaL version: 2.1.3 % 157.24/22.91 % (1801618)Termination reason: Instruction limit % 157.24/22.91 % (1801618)Termination phase: Saturation % 157.24/22.91 % (1801618)Time elapsed: 2.823 s % 157.24/22.91 % (1801618)Peak memory usage: 104 MB % 157.24/22.91 % (1801618)Instructions burned: 3510 (million) % 157.24/22.91 % (1801626)------------------------------ % 157.24/22.91 % (1801626)------------------------------ % 157.24/22.91 % (1801632)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3075285888:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2882 on theBenchmark for (2882ds/10544Mi) % 157.24/22.91 % (1801633)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4152139093:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2881 on theBenchmark for (2881ds/1262Mi) % 157.24/22.91 % (1801628)Instruction limit reached! % 157.24/22.91 % (1801628)------------------------------ % 157.24/22.91 % (1801628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.24/22.91 % (1801628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.91 % (1801628)CaDiCaL version: 2.1.3 % 157.24/22.91 % (1801628)Termination reason: Instruction limit % 157.24/22.91 % (1801628)Termination phase: Saturation % 157.24/22.91 % (1801628)Time elapsed: 1.755 s % 157.24/22.91 % (1801628)Peak memory usage: 145 MB % 157.24/22.91 % (1801628)Instructions burned: 4094 (million) % 157.24/22.91 % (1801633)Refutation not found, incomplete strategy % 157.24/22.91 % (1801633)------------------------------ % 157.24/22.91 % (1801633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.24/22.91 % (1801633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.24/22.91 % (1801633)CaDiCaL version: 2.1.3 % 157.24/22.91 % (1801633)Termination reason: Refutation not found, incomplete strategy % 157.24/22.91 % (1801633)Time elapsed: 0.041 s % 157.24/22.91 % (1801633)Peak memory usage: 116 MB % 157.24/22.91 % (1801633)Instructions burned: 7 (million) % 157.24/22.91 % (1801636)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3850606480:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2878 on theBenchmark for (2878ds/775Mi) % 183.09/26.53 % (1801633)------------------------------ % 183.09/26.53 % (1801633)------------------------------ % 183.09/26.53 % (1801622)Instruction limit reached! % 183.09/26.53 % (1801622)------------------------------ % 183.09/26.53 % (1801622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.09/26.53 % (1801622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.53 % (1801622)CaDiCaL version: 2.1.3 % 183.09/26.53 % (1801622)Termination reason: Instruction limit % 183.09/26.53 % (1801622)Termination phase: Saturation % 183.09/26.53 % (1801622)Time elapsed: 3.451 s % 183.09/26.53 % (1801622)Peak memory usage: 106 MB % 183.09/26.53 % (1801622)Instructions burned: 3553 (million) % 183.09/26.53 % (1801638)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2731403936:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2874 on theBenchmark for (2874ds/270Mi) % 183.09/26.53 % (1801636)Instruction limit reached! % 183.09/26.53 % (1801636)------------------------------ % 183.09/26.53 % (1801636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.09/26.53 % (1801636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.53 % (1801636)CaDiCaL version: 2.1.3 % 183.09/26.53 % (1801636)Termination reason: Instruction limit % 183.09/26.53 % (1801636)Termination phase: Saturation % 183.09/26.53 % (1801636)Time elapsed: 0.446 s % 183.09/26.53 % (1801636)Peak memory usage: 95 MB % 183.09/26.53 % (1801636)Instructions burned: 776 (million) % 183.09/26.53 % (1801586)Instruction limit reached! % 183.09/26.53 % (1801586)------------------------------ % 183.09/26.53 % (1801586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.09/26.53 % (1801586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.53 % (1801586)CaDiCaL version: 2.1.3 % 183.09/26.53 % (1801586)Termination reason: Instruction limit % 183.09/26.53 % (1801586)Termination phase: Saturation % 183.09/26.53 % (1801586)Time elapsed: 5.828 s % 183.09/26.53 % (1801586)Peak memory usage: 118 MB % 183.09/26.53 % (1801586)Instructions burned: 6400 (million) % 183.09/26.53 % (1801641)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1254242812:s2a=on:i=13094:s2at=-1:rtra=on_2871 on theBenchmark for (2871ds/13094Mi) % 183.09/26.53 % (1801639)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3644479640:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2872 on theBenchmark for (2872ds/17165Mi) % 183.09/26.53 % (1801638)Instruction limit reached! % 183.09/26.53 % (1801638)------------------------------ % 183.09/26.53 % (1801638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.09/26.53 % (1801638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.53 % (1801638)CaDiCaL version: 2.1.3 % 183.09/26.53 % (1801638)Termination reason: Instruction limit % 183.09/26.53 % (1801638)Termination phase: Saturation % 183.09/26.53 % (1801638)Time elapsed: 0.275 s % 183.09/26.53 % (1801638)Peak memory usage: 91 MB % 183.09/26.53 % (1801638)Instructions burned: 271 (million) % 183.09/26.53 % (1801601)Instruction limit reached! % 183.09/26.53 % (1801601)------------------------------ % 183.09/26.53 % (1801601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.09/26.53 % (1801601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.09/26.53 % (1801601)CaDiCaL version: 2.1.3 % 183.09/26.53 % (1801601)Termination reason: Instruction limit % 183.09/26.53 % (1801601)Termination phase: Saturation % 183.09/26.53 % (1801601)Time elapsed: 5.019 s % 183.09/26.53 % (1801601)Peak memory usage: 139 MB % 183.09/26.53 % (1801601)Instructions burned: 5811 (million) % 183.09/26.53 % (1801642)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1981473256:st=2:i=12633:rtra=on:ss=axioms_2869 on theBenchmark for (2869ds/12633Mi) % 183.09/26.53 % (1801645)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3300528009:i=1783:rtra=on:gtg=position_2869 on theBenchmark for (2869ds/1783Mi) % 183.09/26.53 % (1801646)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=300007937:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2868 on theBenchmark for (2868ds/5451Mi) % 183.09/26.53 % (1801645)Instruction limit reached! % 183.09/26.53 % (1801645)------------------------------ % 183.09/26.53 % (1801645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.09/26.53 % (1801645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.00/27.92 % (1801645)CaDiCaL version: 2.1.3 % 188.00/27.92 % (1801645)Termination reason: Instruction limit % 188.00/27.92 % (1801645)Termination phase: Saturation % 188.00/27.92 % (1801645)Time elapsed: 1.723 s % 188.00/27.92 % (1801645)Peak memory usage: 127 MB % 188.00/27.92 % (1801645)Instructions burned: 1783 (million) % 188.00/27.92 % (1801653)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=4289206225:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2849 on theBenchmark for (2849ds/4975Mi) % 188.00/27.92 % (1801653)Refutation not found, incomplete strategy % 188.00/27.92 % (1801653)------------------------------ % 188.00/27.92 % (1801653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.00/27.92 % (1801653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.00/27.92 % (1801653)CaDiCaL version: 2.1.3 % 188.00/27.92 % (1801653)Termination reason: Refutation not found, incomplete strategy % 188.00/27.92 % (1801653)Time elapsed: 0.047 s % 188.00/27.92 % (1801653)Peak memory usage: 116 MB % 188.00/27.92 % (1801653)Instructions burned: 13 (million) % 188.00/27.92 % (1801653)------------------------------ % 188.00/27.92 % (1801653)------------------------------ % 188.00/27.92 % (1801660)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=908085052:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2842 on theBenchmark for (2842ds/2076Mi) % 188.00/27.92 % (1801660)Instruction limit reached! % 188.00/27.92 % (1801660)------------------------------ % 188.00/27.92 % (1801660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.00/27.92 % (1801660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.00/27.92 % (1801660)CaDiCaL version: 2.1.3 % 188.00/27.92 % (1801660)Termination reason: Instruction limit % 188.00/27.92 % (1801660)Termination phase: Saturation % 188.00/27.92 % (1801660)Time elapsed: 1.841 s % 188.00/27.92 % (1801660)Peak memory usage: 124 MB % 188.00/27.92 % (1801660)Instructions burned: 2077 (million) % 188.00/27.92 % (1801664)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2878690919:i=5145:rtra=on_2820 on theBenchmark for (2820ds/5145Mi) % 188.00/27.92 % (1801646)Instruction limit reached! % 188.00/27.92 % (1801646)------------------------------ % 188.00/27.92 % (1801646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.00/27.92 % (1801646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.00/27.92 % (1801646)CaDiCaL version: 2.1.3 % 188.00/27.92 % (1801646)Termination reason: Instruction limit % 188.00/27.92 % (1801646)Termination phase: Saturation % 188.00/27.92 % (1801646)Time elapsed: 5.295 s % 188.00/27.92 % (1801646)Peak memory usage: 146 MB % 188.00/27.92 % (1801646)Instructions burned: 5451 (million) % 188.00/27.92 % (1801666)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3587120409:i=3509:rtra=on_2813 on theBenchmark for (2813ds/3509Mi) % 188.00/27.92 % (1801641)Instruction limit reached! % 188.00/27.92 % (1801641)------------------------------ % 188.00/27.92 % (1801641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.00/27.92 % (1801641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.00/27.92 % (1801641)CaDiCaL version: 2.1.3 % 188.00/27.92 % (1801641)Termination reason: Instruction limit % 188.00/27.92 % (1801641)Termination phase: Saturation % 188.00/27.92 % (1801641)Time elapsed: 6.433 s % 188.00/27.92 % (1801641)Peak memory usage: 129 MB % 188.00/27.92 % (1801641)Instructions burned: 13095 (million) % 188.00/27.92 % (1801668)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3695430731:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2805 on theBenchmark for (2805ds/13800Mi) % 188.00/27.92 % (1801666)Instruction limit reached! % 188.00/27.92 % (1801666)------------------------------ % 188.00/27.92 % (1801666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.00/27.92 % (1801666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.00/27.92 % (1801666)CaDiCaL version: 2.1.3 % 188.00/27.92 % (1801666)Termination reason: Instruction limit % 188.00/27.92 % (1801666)Termination phase: Saturation % 188.00/27.92 % (1801666)Time elapsed: 2.909 s % 188.00/27.92 % (1801666)Peak memory usage: 102 MB % 188.00/27.92 % (1801666)Instructions burned: 3510 (million) % 188.00/27.92 % (1801670)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=524699528:i=1412:rtra=on:fsd=on:proc=on_2781 on theBenchmark for (2781ds/1412Mi) % 227.12/32.80 % (1801664)Instruction limit reached! % 227.12/32.80 % (1801664)------------------------------ % 227.12/32.80 % (1801664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.12/32.80 % (1801664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.80 % (1801664)CaDiCaL version: 2.1.3 % 227.12/32.80 % (1801664)Termination reason: Instruction limit % 227.12/32.80 % (1801664)Termination phase: Saturation % 227.12/32.80 % (1801664)Time elapsed: 4.434 s % 227.12/32.80 % (1801664)Peak memory usage: 101 MB % 227.12/32.80 % (1801664)Instructions burned: 5145 (million) % 227.12/32.80 % (1801642)Instruction limit reached! % 227.12/32.80 % (1801642)------------------------------ % 227.12/32.80 % (1801642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.12/32.80 % (1801642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.80 % (1801642)CaDiCaL version: 2.1.3 % 227.12/32.80 % (1801642)Termination reason: Instruction limit % 227.12/32.80 % (1801642)Termination phase: Saturation % 227.12/32.80 % (1801642)Time elapsed: 9.462 s % 227.12/32.80 % (1801642)Peak memory usage: 144 MB % 227.12/32.80 % (1801642)Instructions burned: 12633 (million) % 227.12/32.80 % (1801676)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 % 227.12/32.80 % (1801676)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=54005970:i=11747:aac=none:nm=0:rtra=on:rawr=on_2773 on theBenchmark for (2773ds/11747Mi) % 227.12/32.80 % (1801677)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=790752199:s2a=on:i=3553:nm=0:rtra=on_2772 on theBenchmark for (2772ds/3553Mi) % 227.12/32.80 % (1801632)Instruction limit reached! % 227.12/32.80 % (1801632)------------------------------ % 227.12/32.80 % (1801632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.12/32.80 % (1801632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.80 % (1801632)CaDiCaL version: 2.1.3 % 227.12/32.80 % (1801632)Termination reason: Instruction limit % 227.12/32.80 % (1801632)Termination phase: Saturation % 227.12/32.80 % (1801632)Time elapsed: 11.206 s % 227.12/32.80 % (1801632)Peak memory usage: 200 MB % 227.12/32.80 % (1801632)Instructions burned: 10544 (million) % 227.12/32.80 % (1801670)Instruction limit reached! % 227.12/32.80 % (1801670)------------------------------ % 227.12/32.80 % (1801670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.12/32.80 % (1801670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.80 % (1801670)CaDiCaL version: 2.1.3 % 227.12/32.80 % (1801670)Termination reason: Instruction limit % 227.12/32.80 % (1801670)Termination phase: Saturation % 227.12/32.80 % (1801670)Time elapsed: 1.249 s % 227.12/32.80 % (1801670)Peak memory usage: 119 MB % 227.12/32.80 % (1801670)Instructions burned: 1412 (million) % 227.12/32.80 % (1801682)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=682714016:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/3201Mi) % 227.12/32.80 % (1801683)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=3993771179:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2765 on theBenchmark for (2765ds/4081Mi) % 227.12/32.80 % (1801682)Refutation not found, incomplete strategy % 227.12/32.80 % (1801682)------------------------------ % 227.12/32.80 % (1801682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.12/32.80 % (1801682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.80 % (1801682)CaDiCaL version: 2.1.3 % 227.12/32.80 % (1801682)Termination reason: Refutation not found, incomplete strategy % 227.12/32.80 % (1801682)Time elapsed: 2.019 s % 227.12/32.80 % (1801682)Peak memory usage: 94 MB % 227.12/32.80 % (1801682)Instructions burned: 2440 (million) % 227.12/32.80 % (1801668)Instruction limit reached! % 227.12/32.80 % (1801668)------------------------------ % 227.12/32.80 % (1801668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.12/32.80 % (1801668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.80 % (1801668)CaDiCaL version: 2.1.3 % 227.12/32.80 % (1801668)Termination reason: Instruction limit % 227.12/32.80 % (1801668)Termination phase: Saturation % 240.51/34.66 % (1801668)Time elapsed: 6.055 s % 240.51/34.66 % (1801668)Peak memory usage: 139 MB % 240.51/34.66 % (1801668)Instructions burned: 13802 (million) % 240.51/34.66 % (1801682)------------------------------ % 240.51/34.66 % (1801682)------------------------------ % 240.51/34.66 % (1801686)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=3607216536:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2742 on theBenchmark for (2742ds/20260Mi) % 240.51/34.66 % (1801689)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=967052240:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2740 on theBenchmark for (2740ds/58627Mi) % 240.51/34.66 % (1801689)Refutation not found, incomplete strategy % 240.51/34.66 % (1801689)------------------------------ % 240.51/34.66 % (1801689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.51/34.66 % (1801689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.51/34.66 % (1801689)CaDiCaL version: 2.1.3 % 240.51/34.66 % (1801689)Termination reason: Refutation not found, incomplete strategy % 240.51/34.66 % (1801689)Time elapsed: 0.003 s % 240.51/34.66 % (1801689)Peak memory usage: 88 MB % 240.51/34.66 % (1801689)Instructions burned: 1 (million) % 240.51/34.66 % (1801677)Instruction limit reached! % 240.51/34.66 % (1801677)------------------------------ % 240.51/34.66 % (1801677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.51/34.66 % (1801677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.51/34.66 % (1801677)CaDiCaL version: 2.1.3 % 240.51/34.66 % (1801677)Termination reason: Instruction limit % 240.51/34.66 % (1801677)Termination phase: Saturation % 240.51/34.66 % (1801677)Time elapsed: 3.353 s % 240.51/34.66 % (1801677)Peak memory usage: 106 MB % 240.51/34.66 % (1801677)Instructions burned: 3554 (million) % 240.51/34.66 % (1801639)Instruction limit reached! % 240.51/34.66 % (1801639)------------------------------ % 240.51/34.66 % (1801639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.51/34.66 % (1801639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.51/34.66 % (1801639)CaDiCaL version: 2.1.3 % 240.51/34.66 % (1801639)Termination reason: Instruction limit % 240.51/34.66 % (1801639)Termination phase: Saturation % 240.51/34.66 % (1801639)Time elapsed: 13.387 s % 240.51/34.66 % (1801639)Peak memory usage: 168 MB % 240.51/34.66 % (1801639)Instructions burned: 17165 (million) % 240.51/34.66 % (1801692)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2345211702:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/6258Mi) % 240.51/34.66 % (1801689)------------------------------ % 240.51/34.66 % (1801689)------------------------------ % 240.51/34.66 % (1801692)Refutation not found, incomplete strategy % 240.51/34.66 % (1801692)------------------------------ % 240.51/34.66 % (1801692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.51/34.66 % (1801692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.51/34.66 % (1801692)CaDiCaL version: 2.1.3 % 240.51/34.66 % (1801692)Termination reason: Refutation not found, incomplete strategy % 240.51/34.66 % (1801692)Time elapsed: 0.043 s % 240.51/34.66 % (1801692)Peak memory usage: 116 MB % 240.51/34.66 % (1801692)Instructions burned: 7 (million) % 240.51/34.66 % (1801693)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2225863385:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2735 on theBenchmark for (2735ds/34001Mi) % 240.51/34.66 % (1801695)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1133961366:s2a=on:i=71622:s2at=-1:rtra=on_2733 on theBenchmark for (2733ds/71622Mi) % 240.51/34.66 % (1801692)------------------------------ % 240.51/34.66 % (1801692)------------------------------ % 240.51/34.66 % (1801683)Instruction limit reached! % 240.51/34.66 % (1801683)------------------------------ % 240.51/34.66 % (1801683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.51/34.66 % (1801683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.51/34.66 % (1801683)CaDiCaL version: 2.1.3 % 240.51/34.66 % (1801683)Termination reason: Instruction limit % 240.51/34.66 % (1801683)Termination phase: Saturation % 240.51/34.66 % (1801683)Time elapsed: 3.421 s % 240.51/34.66 % (1801683)Peak memory usage: 142 MB % 240.51/34.66 % (1801683)Instructions burned: 4083 (million) % 240.51/34.66 % (1801699)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4242982152:i=24001:kws=precedence:nm=0:rtra=on_2730 on theBenchmark for (2730ds/24001Mi) % 266.58/38.30 % (1801700)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=387961038:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2728 on theBenchmark for (2728ds/2076Mi) % 266.58/38.30 % (1801630)Instruction limit reached! % 266.58/38.30 % (1801630)------------------------------ % 266.58/38.30 % (1801630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.58/38.30 % (1801630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.58/38.30 % (1801630)CaDiCaL version: 2.1.3 % 266.58/38.30 % (1801630)Termination reason: Instruction limit % 266.58/38.30 % (1801630)Termination phase: Saturation % 266.58/38.30 % (1801630)Time elapsed: 16.285 s % 266.58/38.30 % (1801630)Peak memory usage: 137 MB % 266.58/38.30 % (1801630)Instructions burned: 21174 (million) % 266.58/38.30 % (1801742)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3729651445:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2724 on theBenchmark for (2724ds/83971Mi) % 266.58/38.30 % (1801700)Instruction limit reached! % 266.58/38.30 % (1801700)------------------------------ % 266.58/38.30 % (1801700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.58/38.30 % (1801700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.58/38.30 % (1801700)CaDiCaL version: 2.1.3 % 266.58/38.30 % (1801700)Termination reason: Instruction limit % 266.58/38.30 % (1801700)Termination phase: Saturation % 266.58/38.30 % (1801700)Time elapsed: 1.129 s % 266.58/38.30 % (1801700)Peak memory usage: 124 MB % 266.58/38.30 % (1801700)Instructions burned: 2077 (million) % 266.58/38.30 % (1801771)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2369470321:i=83944:rtra=on_2715 on theBenchmark for (2715ds/83944Mi) % 266.58/38.30 % (1801771)Refutation not found, incomplete strategy % 266.58/38.30 % (1801771)------------------------------ % 266.58/38.30 % (1801771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.58/38.30 % (1801771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.58/38.30 % (1801771)CaDiCaL version: 2.1.3 % 266.58/38.30 % (1801771)Termination reason: Refutation not found, incomplete strategy % 266.58/38.30 % (1801771)Time elapsed: 0.029 s % 266.58/38.30 % (1801771)Peak memory usage: 116 MB % 266.58/38.30 % (1801771)Instructions burned: 8 (million) % 266.58/38.30 % (1801771)------------------------------ % 266.58/38.30 % (1801771)------------------------------ % 266.58/38.30 % (1801860)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=533118825:i=9201:rtra=on_2711 on theBenchmark for (2711ds/9201Mi) % 266.58/38.30 % (1801676)Instruction limit reached! % 266.58/38.30 % (1801676)------------------------------ % 266.58/38.30 % (1801676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.58/38.30 % (1801676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.58/38.30 % (1801676)CaDiCaL version: 2.1.3 % 266.58/38.30 % (1801676)Termination reason: Instruction limit % 266.58/38.30 % (1801676)Termination phase: Saturation % 266.58/38.30 % (1801676)Time elapsed: 7.717 s % 266.58/38.30 % (1801676)Peak memory usage: 185 MB % 266.58/38.30 % (1801676)Instructions burned: 11747 (million) % 266.58/38.30 % (1801862)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 % 266.58/38.30 % (1801862)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3414321922:i=6806:aac=none:nm=0:rtra=on:rawr=on_2693 on theBenchmark for (2693ds/6806Mi) % 266.58/38.30 % (1801686)Instruction limit reached! % 266.58/38.30 % (1801686)------------------------------ % 266.58/38.30 % (1801686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.58/38.30 % (1801686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.58/38.30 % (1801686)CaDiCaL version: 2.1.3 % 266.58/38.30 % (1801686)Termination reason: Instruction limit % 266.58/38.30 % (1801686)Termination phase: Saturation % 266.58/38.30 % (1801686)Time elapsed: 4.792 s % 266.58/38.30 % (1801686)Peak memory usage: 136 MB % 266.58/38.30 % (1801686)Instructions burned: 20261 (million) % 266.58/38.30 % (1801864)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4088021370:s2a=on:i=3553:nm=0:rtra=on_2691 on theBenchmark for (2691ds/3553Mi) % 266.58/38.30 % (1801864)Instruction limit reached! % 269.25/38.88 % (1801864)------------------------------ % 269.25/38.88 % (1801864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.25/38.88 % (1801864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.25/38.88 % (1801864)CaDiCaL version: 2.1.3 % 269.25/38.88 % (1801864)Termination reason: Instruction limit % 269.25/38.88 % (1801864)Termination phase: Saturation % 269.25/38.88 % (1801864)Time elapsed: 1.108 s % 269.25/38.88 % (1801864)Peak memory usage: 106 MB % 269.25/38.88 % (1801864)Instructions burned: 3556 (million) % 269.25/38.88 % (1801866)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=3726793872:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2679 on theBenchmark for (2679ds/2064Mi) % 269.25/38.88 % (1801866)Instruction limit reached! % 269.25/38.88 % (1801866)------------------------------ % 269.25/38.88 % (1801866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.25/38.88 % (1801866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.25/38.88 % (1801866)CaDiCaL version: 2.1.3 % 269.25/38.88 % (1801866)Termination reason: Instruction limit % 269.25/38.88 % (1801866)Termination phase: Saturation % 269.25/38.88 % (1801866)Time elapsed: 0.563 s % 269.25/38.88 % (1801866)Peak memory usage: 143 MB % 269.25/38.88 % (1801866)Instructions burned: 2069 (million) % 269.25/38.88 % (1801860)Instruction limit reached! % 269.25/38.88 % (1801860)------------------------------ % 269.25/38.88 % (1801860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.25/38.88 % (1801860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.25/38.88 % (1801860)CaDiCaL version: 2.1.3 % 269.25/38.88 % (1801860)Termination reason: Instruction limit % 269.25/38.88 % (1801860)Termination phase: Saturation % 269.25/38.88 % (1801860)Time elapsed: 3.810 s % 269.25/38.88 % (1801860)Peak memory usage: 127 MB % 269.25/38.88 % (1801860)Instructions burned: 9202 (million) % 269.25/38.88 % (1801868)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=239595654:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2672 on theBenchmark for (2672ds/20260Mi) % 269.25/38.88 % (1801869)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2790615012:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2671 on theBenchmark for (2671ds/1244Mi) % 269.25/38.88 % (1801869)Refutation not found, incomplete strategy % 269.25/38.88 % (1801869)------------------------------ % 269.25/38.88 % (1801869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.25/38.88 % (1801869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.25/38.88 % (1801869)CaDiCaL version: 2.1.3 % 269.25/38.88 % (1801869)Termination reason: Refutation not found, incomplete strategy % 269.25/38.88 % (1801869)Time elapsed: 0.029 s % 269.25/38.88 % (1801869)Peak memory usage: 116 MB % 269.25/38.88 % (1801869)Instructions burned: 7 (million) % 269.25/38.88 % (1801869)------------------------------ % 269.25/38.88 % (1801869)------------------------------ % 269.25/38.88 % (1801872)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=759430565:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2667 on theBenchmark for (2667ds/58261Mi) % 269.25/38.88 % (1801872)Refutation not found, incomplete strategy % 269.25/38.88 % (1801872)------------------------------ % 269.25/38.88 % (1801872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.25/38.88 % (1801872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.25/38.88 % (1801872)CaDiCaL version: 2.1.3 % 269.25/38.88 % (1801872)Termination reason: Refutation not found, incomplete strategy % 269.25/38.88 % (1801872)Time elapsed: 0.034 s % 269.25/38.88 % (1801872)Peak memory usage: 116 MB % 269.25/38.88 % (1801872)Instructions burned: 14 (million) % 269.25/38.88 % (1801872)------------------------------ % 269.25/38.88 % (1801872)------------------------------ % 269.25/38.88 % (1801874)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 % 269.25/38.88 % (1801874)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1122873524:i=6806:aac=none:nm=0:rtra=on:rawr=on_2662 on theBenchmark for (2662ds/6806Mi) % 272.58/39.20 % (1801862)Instruction limit reached! % 272.58/39.20 % (1801862)------------------------------ % 272.58/39.20 % (1801862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.58/39.20 % (1801862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.58/39.20 % (1801862)CaDiCaL version: 2.1.3 % 272.58/39.20 % (1801862)Termination reason: Instruction limit % 272.58/39.20 % (1801862)Termination phase: Saturation % 272.58/39.20 % (1801862)Time elapsed: 3.588 s % 272.58/39.20 % (1801862)Peak memory usage: 153 MB % 272.58/39.20 % (1801862)Instructions burned: 6806 (million) % 272.58/39.20 % (1801876)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=4071405037:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2655 on theBenchmark for (2655ds/4081Mi) % 272.58/39.20 % (1801876)Instruction limit reached! % 272.58/39.20 % (1801876)------------------------------ % 272.58/39.20 % (1801876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.58/39.20 % (1801876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.58/39.20 % (1801876)CaDiCaL version: 2.1.3 % 272.58/39.20 % (1801876)Termination reason: Instruction limit % 272.58/39.20 % (1801876)Termination phase: Saturation % 272.58/39.20 % (1801876)Time elapsed: 1.922 s % 272.58/39.20 % (1801876)Peak memory usage: 143 MB % 272.58/39.20 % (1801876)Instructions burned: 4083 (million) % 272.58/39.20 % (1801878)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2707253280:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2635 on theBenchmark for (2635ds/1701Mi) % 272.58/39.20 % (1801878)Refutation not found, incomplete strategy % 272.58/39.20 % (1801878)------------------------------ % 272.58/39.20 % (1801878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.58/39.20 % (1801878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.58/39.20 % (1801878)CaDiCaL version: 2.1.3 % 272.58/39.20 % (1801878)Termination reason: Refutation not found, incomplete strategy % 272.58/39.20 % (1801878)Time elapsed: 0.029 s % 272.58/39.20 % (1801878)Peak memory usage: 116 MB % 272.58/39.20 % (1801878)Instructions burned: 7 (million) % 272.58/39.20 % (1801878)------------------------------ % 272.58/39.20 % (1801878)------------------------------ % 272.58/39.20 % (1801880)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=1670399589:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2630 on theBenchmark for (2630ds/57001Mi) % 272.58/39.20 % (1801880)Refutation not found, incomplete strategy % 272.58/39.20 % (1801880)------------------------------ % 272.58/39.20 % (1801880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.58/39.20 % (1801880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.58/39.20 % (1801880)CaDiCaL version: 2.1.3 % 272.58/39.20 % (1801880)Termination reason: Refutation not found, incomplete strategy % 272.58/39.20 % (1801880)Time elapsed: 0.034 s % 272.58/39.20 % (1801880)Peak memory usage: 116 MB % 272.58/39.20 % (1801880)Instructions burned: 13 (million) % 272.58/39.20 % (1801880)------------------------------ % 272.58/39.20 % (1801880)------------------------------ % 272.58/39.20 % (1801874)Instruction limit reached! % 272.58/39.20 % (1801874)------------------------------ % 272.58/39.20 % (1801874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.58/39.20 % (1801874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.58/39.20 % (1801874)CaDiCaL version: 2.1.3 % 272.58/39.20 % (1801874)Termination reason: Instruction limit % 272.58/39.20 % (1801874)Termination phase: Saturation % 272.58/39.20 % (1801874)Time elapsed: 3.511 s % 272.58/39.20 % (1801874)Peak memory usage: 156 MB % 272.58/39.20 % (1801874)Instructions burned: 6806 (million) % 272.58/39.20 % (1801699)Instruction limit reached! % 272.58/39.20 % (1801699)------------------------------ % 272.58/39.20 % (1801699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.58/39.20 % (1801699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.58/39.20 % (1801699)CaDiCaL version: 2.1.3 % 272.58/39.20 % (1801699)Termination reason: Instruction limit % 272.58/39.20 % (1801699)Termination phase: Saturation % 272.58/39.20 % (1801699)Time elapsed: 10.288 s % 272.58/39.20 % (1801699)Peak memory usage: 173 MB % 272.58/39.20 % (1801699)Instructions burned: 24001 (million) % 272.58/39.20 % (1801882)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 % 275.60/39.61 % (1801882)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=769767582:i=8622:aac=none:nm=0:rtra=on:rawr=on_2626 on theBenchmark for (2626ds/8622Mi) % 275.60/39.61 % (1801883)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1700475082:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2625 on theBenchmark for (2625ds/24Mi) % 275.60/39.61 % (1801883)Instruction limit reached! % 275.60/39.61 % (1801883)------------------------------ % 275.60/39.61 % (1801883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/39.61 % (1801883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/39.61 % (1801883)CaDiCaL version: 2.1.3 % 275.60/39.61 % (1801883)Termination reason: Instruction limit % 275.60/39.61 % (1801883)Termination phase: Saturation % 275.60/39.61 % (1801883)Time elapsed: 0.038 s % 275.60/39.61 % (1801883)Peak memory usage: 115 MB % 275.60/39.61 % (1801883)Instructions burned: 25 (million) % 275.60/39.61 % (1801884)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=441984131:i=614:kws=precedence:nm=0:rtra=on_2625 on theBenchmark for (2625ds/614Mi) % 275.60/39.61 % (1801887)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4212299376:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2623 on theBenchmark for (2623ds/402Mi) % 275.60/39.61 % (1801868)Instruction limit reached! % 275.60/39.61 % (1801868)------------------------------ % 275.60/39.61 % (1801868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/39.61 % (1801868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/39.61 % (1801868)CaDiCaL version: 2.1.3 % 275.60/39.61 % (1801868)Termination reason: Instruction limit % 275.60/39.61 % (1801868)Termination phase: Saturation % 275.60/39.61 % (1801868)Time elapsed: 4.959 s % 275.60/39.61 % (1801868)Peak memory usage: 149 MB % 275.60/39.61 % (1801868)Instructions burned: 20262 (million) % 275.60/39.61 % (1801884)Instruction limit reached! % 275.60/39.61 % (1801884)------------------------------ % 275.60/39.61 % (1801884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/39.61 % (1801884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/39.61 % (1801884)CaDiCaL version: 2.1.3 % 275.60/39.61 % (1801884)Termination reason: Instruction limit % 275.60/39.61 % (1801884)Termination phase: Saturation % 275.60/39.61 % (1801884)Time elapsed: 0.347 s % 275.60/39.61 % (1801884)Peak memory usage: 120 MB % 275.60/39.61 % (1801884)Instructions burned: 616 (million) % 275.60/39.61 % (1801890)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2450321590:s2a=on:i=14:rtra=on:inst=on_2621 on theBenchmark for (2621ds/14Mi) % 275.60/39.61 % (1801890)Instruction limit reached! % 275.60/39.61 % (1801890)------------------------------ % 275.60/39.61 % (1801890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/39.61 % (1801890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/39.61 % (1801890)CaDiCaL version: 2.1.3 % 275.60/39.61 % (1801890)Termination reason: Instruction limit % 275.60/39.61 % (1801890)Termination phase: Saturation % 275.60/39.61 % (1801890)Time elapsed: 0.006 s % 275.60/39.61 % (1801890)Peak memory usage: 88 MB % 275.60/39.61 % (1801890)Instructions burned: 17 (million) % 275.60/39.61 % (1801887)Instruction limit reached! % 275.60/39.61 % (1801887)------------------------------ % 275.60/39.61 % (1801887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/39.61 % (1801887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/39.61 % (1801887)CaDiCaL version: 2.1.3 % 275.60/39.61 % (1801887)Termination reason: Instruction limit % 275.60/39.61 % (1801887)Termination phase: Saturation % 275.60/39.61 % (1801887)Time elapsed: 0.309 s % 275.60/39.61 % (1801887)Peak memory usage: 119 MB % 275.60/39.61 % (1801887)Instructions burned: 402 (million) % 275.60/39.61 % (1801893)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1458211027:i=92:rtra=on_2620 on theBenchmark for (2620ds/92Mi) % 275.60/39.61 % (1801891)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=69511999:i=8:rtra=on_2620 on theBenchmark for (2620ds/8Mi) % 275.60/39.61 % (1801891)Instruction limit reached! % 275.60/39.61 % (1801891)------------------------------ % 275.60/39.61 % (1801891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.84/39.93 % (1801891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.84/39.93 % (1801891)CaDiCaL version: 2.1.3 % 277.84/39.93 % (1801891)Termination reason: Instruction limit % 277.84/39.93 % (1801891)Termination phase: Saturation % 277.84/39.93 % (1801891)Time elapsed: 0.006 s % 277.84/39.93 % (1801891)Peak memory usage: 89 MB % 277.84/39.93 % (1801891)Instructions burned: 9 (million) % 277.84/39.93 % (1801893)Instruction limit reached! % 277.84/39.93 % (1801893)------------------------------ % 277.84/39.93 % (1801893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.84/39.93 % (1801893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.84/39.93 % (1801893)CaDiCaL version: 2.1.3 % 277.84/39.93 % (1801893)Termination reason: Instruction limit % 277.84/39.93 % (1801893)Termination phase: Saturation % 277.84/39.93 % (1801893)Time elapsed: 0.039 s % 277.84/39.93 % (1801893)Peak memory usage: 115 MB % 277.84/39.93 % (1801893)Instructions burned: 92 (million) % 277.84/39.93 % (1801894)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1365076199:i=66:rtra=on_2619 on theBenchmark for (2619ds/66Mi) % 277.84/39.93 % (1801898)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=1877759359:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2618 on theBenchmark for (2618ds/58Mi) % 277.84/39.93 % (1801897)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3023133069:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2618 on theBenchmark for (2618ds/28Mi) % 277.84/39.93 % (1801894)Instruction limit reached! % 277.84/39.93 % (1801894)------------------------------ % 277.84/39.93 % (1801894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.84/39.93 % (1801894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.84/39.93 % (1801894)CaDiCaL version: 2.1.3 % 277.84/39.93 % (1801894)Termination reason: Instruction limit % 277.84/39.93 % (1801894)Termination phase: Saturation % 277.84/39.93 % (1801894)Time elapsed: 0.069 s % 277.84/39.93 % (1801894)Peak memory usage: 117 MB % 277.84/39.93 % (1801894)Instructions burned: 66 (million) % 277.84/39.93 % (1801897)Instruction limit reached! % 277.84/39.93 % (1801897)------------------------------ % 277.84/39.93 % (1801897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.84/39.93 % (1801897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.84/39.93 % (1801897)CaDiCaL version: 2.1.3 % 277.84/39.93 % (1801897)Termination reason: Instruction limit % 277.84/39.93 % (1801897)Termination phase: Saturation % 277.84/39.93 % (1801897)Time elapsed: 0.017 s % 277.84/39.93 % (1801897)Peak memory usage: 88 MB % 277.84/39.93 % (1801897)Instructions burned: 29 (million) % 277.84/39.93 % (1801898)Instruction limit reached! % 277.84/39.93 % (1801898)------------------------------ % 277.84/39.93 % (1801898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.84/39.93 % (1801898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.84/39.93 % (1801898)CaDiCaL version: 2.1.3 % 277.84/39.93 % (1801898)Termination reason: Instruction limit % 277.84/39.93 % (1801898)Termination phase: Saturation % 277.84/39.93 % (1801898)Time elapsed: 0.022 s % 277.84/39.93 % (1801898)Peak memory usage: 89 MB % 277.84/39.93 % (1801898)Instructions burned: 61 (million) % 277.84/39.93 % (1801904)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=3744755577:i=54:canc=cautious:fsr=off:rtra=on_2616 on theBenchmark for (2616ds/54Mi) % 277.84/39.93 % (1801902)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1759448840:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2617 on theBenchmark for (2617ds/32Mi) % 277.84/39.93 % (1801904)Instruction limit reached! % 277.84/39.93 % (1801904)------------------------------ % 277.84/39.93 % (1801904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.84/39.93 % (1801904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.84/39.93 % (1801904)CaDiCaL version: 2.1.3 % 277.84/39.93 % (1801904)Termination reason: Instruction limit % 277.84/39.93 % (1801904)Termination phase: Saturation % 277.84/39.93 % (1801904)Time elapsed: 0.017 s % 277.84/39.93 % (1801904)Peak memory usage: 89 MB % 277.84/39.93 % (1801904)Instructions burned: 55 (million) % 277.84/39.93 % (1801902)Instruction limit reached! % 277.84/39.93 % (1801902)------------------------------ % 277.84/39.93 % (1801902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.74/40.33 % (1801902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.74/40.33 % (1801902)CaDiCaL version: 2.1.3 % 280.74/40.33 % (1801902)Termination reason: Instruction limit % 280.74/40.33 % (1801902)Termination phase: Saturation % 280.74/40.33 % (1801902)Time elapsed: 0.018 s % 280.74/40.33 % (1801902)Peak memory usage: 90 MB % 280.74/40.33 % (1801902)Instructions burned: 33 (million) % 280.74/40.33 % (1801903)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1924098733:i=48:canc=force:rtra=on_2616 on theBenchmark for (2616ds/48Mi) % 280.74/40.33 % (1801903)Instruction limit reached! % 280.74/40.33 % (1801903)------------------------------ % 280.74/40.33 % (1801903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.74/40.33 % (1801903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.74/40.33 % (1801903)CaDiCaL version: 2.1.3 % 280.74/40.33 % (1801903)Termination reason: Instruction limit % 280.74/40.33 % (1801903)Termination phase: Saturation % 280.74/40.33 % (1801903)Time elapsed: 0.034 s % 280.74/40.33 % (1801903)Peak memory usage: 89 MB % 280.74/40.33 % (1801903)Instructions burned: 48 (million) % 280.74/40.33 % (1801907)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2999622116:i=170:gtgl=4:rtra=on:gtg=exists_sym_2615 on theBenchmark for (2615ds/170Mi) % 280.74/40.33 % (1801908)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1321309459:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2615 on theBenchmark for (2615ds/4Mi) % 280.74/40.33 % (1801908)Instruction limit reached! % 280.74/40.33 % (1801908)------------------------------ % 280.74/40.33 % (1801908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.74/40.33 % (1801908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.74/40.33 % (1801908)CaDiCaL version: 2.1.3 % 280.74/40.33 % (1801908)Termination reason: Instruction limit % 280.74/40.33 % (1801908)Termination phase: Saturation % 280.74/40.33 % (1801908)Time elapsed: 0.004 s % 280.74/40.33 % (1801908)Peak memory usage: 89 MB % 280.74/40.33 % (1801908)Instructions burned: 5 (million) % 280.74/40.33 % (1801907)Instruction limit reached! % 280.74/40.33 % (1801907)------------------------------ % 280.74/40.33 % (1801907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.74/40.33 % (1801907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.74/40.33 % (1801907)CaDiCaL version: 2.1.3 % 280.74/40.33 % (1801907)Termination reason: Instruction limit % 280.74/40.33 % (1801907)Termination phase: Saturation % 280.74/40.33 % (1801907)Time elapsed: 0.053 s % 280.74/40.33 % (1801907)Peak memory usage: 90 MB % 280.74/40.33 % (1801907)Instructions burned: 174 (million) % 280.74/40.33 % (1801910)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3444159745:i=362:rtra=on:ss=axioms:ev=cautious_2615 on theBenchmark for (2615ds/362Mi) % 280.74/40.33 % (1801914)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=629970869:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2613 on theBenchmark for (2613ds/132Mi) % 280.74/40.33 % (1801913)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2546576465:i=8:ep=RST:ins=2:rtra=on_2614 on theBenchmark for (2614ds/8Mi) % 280.74/40.33 % (1801913)Instruction limit reached! % 280.74/40.33 % (1801913)------------------------------ % 280.74/40.33 % (1801913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.74/40.33 % (1801913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.74/40.33 % (1801913)CaDiCaL version: 2.1.3 % 280.74/40.33 % (1801913)Termination reason: Instruction limit % 280.74/40.33 % (1801913)Termination phase: Saturation % 280.74/40.33 % (1801913)Time elapsed: 0.006 s % 280.74/40.33 % (1801913)Peak memory usage: 89 MB % 280.74/40.33 % (1801913)Instructions burned: 8 (million) % 280.74/40.33 % (1801914)Instruction limit reached! % 280.74/40.33 % (1801914)------------------------------ % 280.74/40.33 % (1801914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.74/40.33 % (1801914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.74/40.33 % (1801914)CaDiCaL version: 2.1.3 % 280.74/40.33 % (1801914)Termination reason: Instruction limit % 280.74/40.33 % (1801914)Termination phase: Saturation % 280.74/40.33 % (1801914)Time elapsed: 0.074 s % 280.74/40.33 % (1801914)Peak memory usage: 136 MB % 280.74/40.33 % (1801914)Instructions burned: 136 (million) % 280.74/40.33 % (1801910)Instruction limit reached! % 280.74/40.33 % (1801910)------------------------------ % 280.74/40.33 % (1801910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.82/40.98 % (1801910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.82/40.98 % (1801910)CaDiCaL version: 2.1.3 % 284.82/40.98 % (1801910)Termination reason: Instruction limit % 284.82/40.98 % (1801910)Termination phase: Saturation % 284.82/40.98 % (1801910)Time elapsed: 0.222 s % 284.82/40.98 % (1801910)Peak memory usage: 92 MB % 284.82/40.98 % (1801910)Instructions burned: 362 (million) % 284.82/40.98 % (1801918)lrs+10_1_thi=all:si=on:fd=off:random_seed=2371420849:i=106:rtra=on:gtg=all_2612 on theBenchmark for (2612ds/106Mi) % 284.82/40.98 % (1801919)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=1411692208:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2611 on theBenchmark for (2611ds/16Mi) % 284.82/40.98 % (1801919)Instruction limit reached! % 284.82/40.98 % (1801919)------------------------------ % 284.82/40.98 % (1801919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.82/40.98 % (1801919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.82/40.98 % (1801919)CaDiCaL version: 2.1.3 % 284.82/40.98 % (1801919)Termination reason: Instruction limit % 284.82/40.98 % (1801919)Termination phase: Saturation % 284.82/40.98 % (1801919)Time elapsed: 0.006 s % 284.82/40.98 % (1801919)Peak memory usage: 88 MB % 284.82/40.98 % (1801919)Instructions burned: 16 (million) % 284.82/40.98 % (1801918)Instruction limit reached! % 284.82/40.98 % (1801918)------------------------------ % 284.82/40.98 % (1801918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.82/40.98 % (1801918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.82/40.98 % (1801918)CaDiCaL version: 2.1.3 % 284.82/40.98 % (1801918)Termination reason: Instruction limit % 284.82/40.98 % (1801918)Termination phase: Saturation % 284.82/40.98 % (1801918)Time elapsed: 0.096 s % 284.82/40.98 % (1801918)Peak memory usage: 117 MB % 284.82/40.98 % (1801918)Instructions burned: 107 (million) % 284.82/40.98 % (1801920)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=60230707:st=3:i=4:rtra=on:ss=axioms_2611 on theBenchmark for (2611ds/4Mi) % 284.82/40.98 % (1801920)Instruction limit reached! % 284.82/40.98 % (1801920)------------------------------ % 284.82/40.98 % (1801920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.82/40.98 % (1801920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.82/40.98 % (1801920)CaDiCaL version: 2.1.3 % 284.82/40.98 % (1801920)Termination reason: Instruction limit % 284.82/40.98 % (1801920)Termination phase: Saturation % 284.82/40.98 % (1801920)Time elapsed: 0.004 s % 284.82/40.98 % (1801920)Peak memory usage: 90 MB % 284.82/40.98 % (1801920)Instructions burned: 5 (million) % 284.82/40.98 % (1801923)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1347068295:i=4:doe=on:canc=force:asg=cautious:rtra=on_2610 on theBenchmark for (2610ds/4Mi) % 284.82/40.98 % (1801923)Instruction limit reached! % 284.82/40.98 % (1801923)------------------------------ % 284.82/40.98 % (1801923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.82/40.98 % (1801923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.82/40.98 % (1801923)CaDiCaL version: 2.1.3 % 284.82/40.98 % (1801923)Termination reason: Instruction limit % 284.82/40.98 % (1801923)Termination phase: Saturation % 284.82/40.98 % (1801923)Time elapsed: 0.003 s % 284.82/40.98 % (1801923)Peak memory usage: 89 MB % 284.82/40.98 % (1801923)Instructions burned: 6 (million) % 284.82/40.98 % (1801924)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=359156222:i=254:doe=on:rtra=on_2610 on theBenchmark for (2610ds/254Mi) % 284.82/40.98 % (1801926)dis+10_1_si=on:random_seed=1282451139:i=20:ep=R:rtra=on_2609 on theBenchmark for (2609ds/20Mi) % 284.82/40.98 % (1801928)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2144687811:i=52:canc=cautious:av=off:rtra=on_2609 on theBenchmark for (2609ds/52Mi) % 284.82/40.98 % (1801928)Refutation not found, incomplete strategy % 284.82/40.98 % (1801928)------------------------------ % 284.82/40.98 % (1801928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.82/40.98 % (1801928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.82/40.98 % (1801928)CaDiCaL version: 2.1.3 % 284.82/40.98 % (1801928)Termination reason: Refutation not found, incomplete strategy % 284.82/40.98 % (1801928)Time elapsed: 0.001 s % 284.82/40.98 % (1801928)Peak memory usage: 89 MB % 284.82/40.98 % (1801928)Instructions burned: 2 (million) % 284.82/40.98 % (1801926)Instruction limit reached! % 284.82/40.98 % (1801926)------------------------------ % 290.02/41.70 % (1801926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.02/41.70 % (1801926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.02/41.70 % (1801926)CaDiCaL version: 2.1.3 % 290.02/41.70 % (1801926)Termination reason: Instruction limit % 290.02/41.70 % (1801926)Termination phase: Saturation % 290.02/41.70 % (1801926)Time elapsed: 0.014 s % 290.02/41.70 % (1801926)Peak memory usage: 88 MB % 290.02/41.70 % (1801926)Instructions burned: 21 (million) % 290.02/41.70 % (1801924)Instruction limit reached! % 290.02/41.70 % (1801924)------------------------------ % 290.02/41.70 % (1801924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.02/41.70 % (1801924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.02/41.70 % (1801924)CaDiCaL version: 2.1.3 % 290.02/41.70 % (1801924)Termination reason: Instruction limit % 290.02/41.70 % (1801924)Termination phase: Saturation % 290.02/41.70 % (1801924)Time elapsed: 0.167 s % 290.02/41.70 % (1801924)Peak memory usage: 119 MB % 290.02/41.70 % (1801924)Instructions burned: 255 (million) % 290.02/41.70 % (1801928)------------------------------ % 290.02/41.70 % (1801928)------------------------------ % 290.02/41.70 % (1801932)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1935425920: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_2608 on theBenchmark for (2608ds/70Mi) % 290.02/41.70 % (1801932)Instruction limit reached! % 290.02/41.70 % (1801932)------------------------------ % 290.02/41.70 % (1801932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.02/41.70 % (1801932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.02/41.70 % (1801932)CaDiCaL version: 2.1.3 % 290.02/41.70 % (1801932)Termination reason: Instruction limit % 290.02/41.70 % (1801932)Termination phase: Saturation % 290.02/41.70 % (1801932)Time elapsed: 0.052 s % 290.02/41.70 % (1801932)Peak memory usage: 89 MB % 290.02/41.70 % (1801932)Instructions burned: 71 (million) % 290.02/41.70 % (1801934)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3415140475:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2606 on theBenchmark for (2606ds/16Mi) % 290.02/41.70 % (1801934)Instruction limit reached! % 290.02/41.70 % (1801934)------------------------------ % 290.02/41.70 % (1801934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.02/41.70 % (1801934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.02/41.70 % (1801934)CaDiCaL version: 2.1.3 % 290.02/41.70 % (1801934)Termination reason: Instruction limit % 290.02/41.70 % (1801934)Termination phase: Saturation % 290.02/41.70 % (1801934)Time elapsed: 0.007 s % 290.02/41.70 % (1801934)Peak memory usage: 89 MB % 290.02/41.70 % (1801934)Instructions burned: 17 (million) % 290.02/41.70 % (1801933)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3654038968:i=4:fsr=off:rtra=on:inst=on_2606 on theBenchmark for (2606ds/4Mi) % 290.02/41.70 % (1801933)Instruction limit reached! % 290.02/41.70 % (1801933)------------------------------ % 290.02/41.70 % (1801933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.02/41.70 % (1801933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.02/41.70 % (1801933)CaDiCaL version: 2.1.3 % 290.02/41.70 % (1801933)Termination reason: Instruction limit % 290.02/41.70 % (1801933)Termination phase: Saturation % 290.02/41.70 % (1801933)Time elapsed: 0.004 s % 290.02/41.70 % (1801933)Peak memory usage: 89 MB % 290.02/41.70 % (1801933)Instructions burned: 4 (million) % 290.02/41.70 % (1801938)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1796084138:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2605 on theBenchmark for (2605ds/26Mi) % 290.02/41.70 % (1801936)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1387929639:i=740:ep=RS:fsr=off:rtra=on_2605 on theBenchmark for (2605ds/740Mi) % 290.02/41.70 % (1801938)Instruction limit reached! % 290.02/41.70 % (1801938)------------------------------ % 290.02/41.70 % (1801938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.02/41.70 % (1801938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.02/41.70 % (1801938)CaDiCaL version: 2.1.3 % 290.02/41.70 % (1801938)Termination reason: Instruction limit % 290.02/41.70 % (1801938)Termination phase: Saturation % 290.02/41.70 % (1801938)Time elapsed: 0.026 s % 290.02/41.70 % (1801938)Peak memory usage: 116 MB % 290.02/41.70 % (1801938)Instructions burned: 28 (million) % 296.14/42.53 % (1801940)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=543108946:i=452:rtra=on:gtg=position:ss=axioms_2605 on theBenchmark for (2605ds/452Mi) % 296.14/42.53 % (1801940)Refutation not found, incomplete strategy % 296.14/42.53 % (1801940)------------------------------ % 296.14/42.53 % (1801940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.14/42.53 % (1801940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.14/42.53 % (1801940)CaDiCaL version: 2.1.3 % 296.14/42.53 % (1801940)Termination reason: Refutation not found, incomplete strategy % 296.14/42.53 % (1801940)Time elapsed: 0.029 s % 296.14/42.53 % (1801940)Peak memory usage: 115 MB % 296.14/42.53 % (1801940)Instructions burned: 7 (million) % 296.14/42.53 % (1801943)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1479103704:i=20:rtra=on_2604 on theBenchmark for (2604ds/20Mi) % 296.14/42.53 % (1801943)Instruction limit reached! % 296.14/42.53 % (1801943)------------------------------ % 296.14/42.53 % (1801943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.14/42.53 % (1801943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.14/42.53 % (1801943)CaDiCaL version: 2.1.3 % 296.14/42.53 % (1801943)Termination reason: Instruction limit % 296.14/42.53 % (1801943)Termination phase: Saturation % 296.14/42.53 % (1801943)Time elapsed: 0.007 s % 296.14/42.53 % (1801943)Peak memory usage: 88 MB % 296.14/42.53 % (1801943)Instructions burned: 21 (million) % 296.14/42.53 % (1801946)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=304624318:i=142:rtra=on:gtg=exists_top_2602 on theBenchmark for (2602ds/142Mi) % 296.14/42.53 % (1801940)------------------------------ % 296.14/42.53 % (1801940)------------------------------ % 296.14/42.53 % (1801946)Instruction limit reached! % 296.14/42.53 % (1801946)------------------------------ % 296.14/42.53 % (1801946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.14/42.53 % (1801946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.14/42.53 % (1801946)CaDiCaL version: 2.1.3 % 296.14/42.53 % (1801946)Termination reason: Instruction limit % 296.14/42.53 % (1801946)Termination phase: Saturation % 296.14/42.53 % (1801946)Time elapsed: 0.075 s % 296.14/42.53 % (1801946)Peak memory usage: 135 MB % 296.14/42.53 % (1801946)Instructions burned: 142 (million) % 296.14/42.53 % (1801936)Instruction limit reached! % 296.14/42.53 % (1801936)------------------------------ % 296.14/42.53 % (1801936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.14/42.53 % (1801936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.14/42.53 % (1801936)CaDiCaL version: 2.1.3 % 296.14/42.53 % (1801936)Termination reason: Instruction limit % 296.14/42.53 % (1801936)Termination phase: Saturation % 296.14/42.53 % (1801936)Time elapsed: 0.363 s % 296.14/42.53 % (1801936)Peak memory usage: 94 MB % 296.14/42.53 % (1801936)Instructions burned: 745 (million) % 296.14/42.53 % (1801949)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=1410898681:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2600 on theBenchmark for (2600ds/588Mi) % 296.14/42.53 % (1801948)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=758962222:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2601 on theBenchmark for (2601ds/150Mi) % 296.14/42.53 % (1801950)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2028871293:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2600 on theBenchmark for (2600ds/260Mi) % 296.14/42.53 % (1801948)Instruction limit reached! % 296.14/42.53 % (1801948)------------------------------ % 296.14/42.53 % (1801948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.14/42.53 % (1801948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.14/42.53 % (1801948)CaDiCaL version: 2.1.3 % 296.14/42.53 % (1801948)Termination reason: Instruction limit % 296.14/42.53 % (1801948)Termination phase: Saturation % 296.14/42.53 % (1801948)Time elapsed: 0.080 s % 296.14/42.53 % (1801948)Peak memory usage: 90 MB % 296.14/42.53 % (1801948)Instructions burned: 151 (million) % 296.14/42.53 % (1801949)Instruction limit reached! % 296.14/42.53 % (1801949)------------------------------ % 296.14/42.53 % (1801949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.14/42.53 % (1801949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.97/43.03 % (1801949)CaDiCaL version: 2.1.3 % 298.97/43.03 % (1801949)Termination reason: Instruction limit % 298.97/43.03 % (1801949)Termination phase: Saturation % 298.97/43.03 % (1801949)Time elapsed: 0.186 s % 298.97/43.03 % (1801949)Peak memory usage: 91 MB % 298.97/43.03 % (1801949)Instructions burned: 591 (million) % 298.97/43.03 % (1801950)Instruction limit reached! % 298.97/43.03 % (1801950)------------------------------ % 298.97/43.03 % (1801950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.97/43.03 % (1801950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.97/43.03 % (1801950)CaDiCaL version: 2.1.3 % 298.97/43.03 % (1801950)Termination reason: Instruction limit % 298.97/43.03 % (1801950)Termination phase: Saturation % 298.97/43.03 % (1801950)Time elapsed: 0.167 s % 298.97/43.03 % (1801950)Peak memory usage: 117 MB % 298.97/43.03 % (1801950)Instructions burned: 261 (million) % 298.97/43.03 % (1801954)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1114516968:i=262:rtra=on_2598 on theBenchmark for (2598ds/262Mi) % 298.97/43.03 % (1801955)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=608001856:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2597 on theBenchmark for (2597ds/80Mi) % 298.97/43.03 % (1801955)Instruction limit reached! % 298.97/43.03 % (1801955)------------------------------ % 298.97/43.03 % (1801955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.97/43.03 % (1801955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.97/43.03 % (1801955)CaDiCaL version: 2.1.3 % 298.97/43.03 % (1801955)Termination reason: Instruction limit % 298.97/43.03 % (1801955)Termination phase: Saturation % 298.97/43.03 % (1801955)Time elapsed: 0.055 s % 298.97/43.03 % (1801955)Peak memory usage: 135 MB % 298.97/43.03 % (1801955)Instructions burned: 80 (million) % 298.97/43.03 % (1801956)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2077681573:i=614:rtra=on:gtg=exists_top_2597 on theBenchmark for (2597ds/614Mi) % 298.97/43.03 % (1801954)Instruction limit reached! % 298.97/43.03 % (1801954)------------------------------ % 298.97/43.03 % (1801954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.97/43.03 % (1801954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.97/43.03 % (1801954)CaDiCaL version: 2.1.3 % 298.97/43.03 % (1801954)Termination reason: Instruction limit % 298.97/43.03 % (1801954)Termination phase: Saturation % 298.97/43.03 % (1801954)Time elapsed: 0.174 s % 298.97/43.03 % (1801954)Peak memory usage: 133 MB % 298.97/43.03 % (1801954)Instructions burned: 263 (million) % 298.97/43.03 % (1801959)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=756021993:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2596 on theBenchmark for (2596ds/1196Mi) % 298.97/43.03 % (1801961)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=930190216:i=262:canc=cautious:fsr=off:rtra=on_2595 on theBenchmark for (2595ds/262Mi) % 298.97/43.03 % (1801956)Instruction limit reached! % 298.97/43.03 % (1801956)------------------------------ % 298.97/43.03 % (1801956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.97/43.03 % (1801956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.97/43.03 % (1801956)CaDiCaL version: 2.1.3 % 298.97/43.03 % (1801956)Termination reason: Instruction limit % 298.97/43.03 % (1801956)Termination phase: Saturation % 298.97/43.03 % (1801956)Time elapsed: 0.270 s % 298.97/43.03 % (1801956)Peak memory usage: 91 MB % 298.97/43.03 % (1801956)Instructions burned: 616 (million) % 298.97/43.03 % (1801961)Instruction limit reached! % 298.97/43.03 % (1801961)------------------------------ % 298.97/43.03 % (1801961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.97/43.03 % (1801961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.97/43.03 % (1801961)CaDiCaL version: 2.1.3 % 298.97/43.03 % (1801961)Termination reason: Instruction limit % 298.97/43.03 % (1801961)Termination phase: Saturation % 298.97/43.03 % (1801961)Time elapsed: 0.189 s % 298.97/43.03 % (1801961)Peak memory usage: 119 MB % 298.97/43.03 % (1801961)Instructions burned: 263 (million) % 298.97/43.03 % (1801964)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=1744102803:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2593 on theBenchmark for (2593ds/518Mi) % 298.97/43.03 % (1801959)Instruction limit reached! % 298.97/43.03 % (1801959)------------------------------ % 298.97/43.03 % (1801959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801959)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801959)Termination reason: Instruction limit % 300.13/43.07 % (1801959)Termination phase: Saturation % 300.13/43.07 % (1801959)Time elapsed: 0.435 s % 300.13/43.07 % (1801959)Peak memory usage: 140 MB % 300.13/43.07 % (1801959)Instructions burned: 1198 (million) % 300.13/43.07 % (1801965)dis+10_1_si=on:random_seed=2335633030:s2a=on:i=2000:rtra=on:gtg=exists_all_2591 on theBenchmark for (2591ds/2000Mi) % 300.13/43.07 % (1801967)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=199447281:i=766:fsr=off:rtra=on:ev=force_2590 on theBenchmark for (2590ds/766Mi) % 300.13/43.07 % (1801964)Instruction limit reached! % 300.13/43.07 % (1801964)------------------------------ % 300.13/43.07 % (1801964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801964)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801964)Termination reason: Instruction limit % 300.13/43.07 % (1801964)Termination phase: Saturation % 300.13/43.07 % (1801964)Time elapsed: 0.268 s % 300.13/43.07 % (1801964)Peak memory usage: 118 MB % 300.13/43.07 % (1801964)Instructions burned: 518 (million) % 300.13/43.07 % (1801970)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3486200368:i=282:doe=on:rtra=on_2588 on theBenchmark for (2588ds/282Mi) % 300.13/43.07 % (1801967)Instruction limit reached! % 300.13/43.07 % (1801967)------------------------------ % 300.13/43.07 % (1801967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801967)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801967)Termination reason: Instruction limit % 300.13/43.07 % (1801967)Termination phase: Saturation % 300.13/43.07 % (1801967)Time elapsed: 0.193 s % 300.13/43.07 % (1801967)Peak memory usage: 98 MB % 300.13/43.07 % (1801967)Instructions burned: 767 (million) % 300.13/43.07 % (1801972)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1414552535:i=130:nm=16:rtra=on_2587 on theBenchmark for (2587ds/130Mi) % 300.13/43.07 % (1801972)Refutation not found, incomplete strategy % 300.13/43.07 % (1801972)------------------------------ % 300.13/43.07 % (1801972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801972)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801972)Termination reason: Refutation not found, incomplete strategy % 300.13/43.07 % (1801972)Time elapsed: 0.017 s % 300.13/43.07 % (1801972)Peak memory usage: 115 MB % 300.13/43.07 % (1801972)Instructions burned: 7 (million) % 300.13/43.07 % (1801970)Instruction limit reached! % 300.13/43.07 % (1801970)------------------------------ % 300.13/43.07 % (1801970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801970)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801970)Termination reason: Instruction limit % 300.13/43.07 % (1801970)Termination phase: Saturation % 300.13/43.07 % (1801970)Time elapsed: 0.183 s % 300.13/43.07 % (1801970)Peak memory usage: 92 MB % 300.13/43.07 % (1801970)Instructions burned: 283 (million) % 300.13/43.07 % (1801972)------------------------------ % 300.13/43.07 % (1801972)------------------------------ % 300.13/43.07 % (1801974)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=744908390:i=242:nm=16:rtra=on_2585 on theBenchmark for (2585ds/242Mi) % 300.13/43.07 % (1801975)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=1033092289:s2a=on:i=256:s2at=5:ins=3:rtra=on_2584 on theBenchmark for (2584ds/256Mi) % 300.13/43.07 % (1801974)Instruction limit reached! % 300.13/43.07 % (1801974)------------------------------ % 300.13/43.07 % (1801974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801974)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801974)Termination reason: Instruction limit % 300.13/43.07 % (1801974)Termination phase: Saturation % 300.13/43.07 % (1801974)Time elapsed: 0.125 s % 300.13/43.07 % (1801974)Peak memory usage: 89 MB % 300.13/43.07 % (1801974)Instructions burned: 244 (million) % 300.13/43.07 % (1801975)Instruction limit reached! % 300.13/43.07 % (1801975)------------------------------ % 300.13/43.07 % (1801975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801975)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801975)Termination reason: Instruction limit % 300.13/43.07 % (1801975)Termination phase: Saturation % 300.13/43.07 % (1801975)Time elapsed: 0.103 s % 300.13/43.07 % (1801975)Peak memory usage: 120 MB % 300.13/43.07 % (1801975)Instructions burned: 257 (million) % 300.13/43.07 % (1801978)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=72498962:i=78:ins=3:rtra=on_2582 on theBenchmark for (2582ds/78Mi) % 300.13/43.07 % (1801979)dis+1010_1_to=kbo:si=on:random_seed=1530697701:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2582 on theBenchmark for (2582ds/350Mi) % 300.13/43.07 % (1801978)Instruction limit reached! % 300.13/43.07 % (1801978)------------------------------ % 300.13/43.07 % (1801978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801978)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801978)Termination reason: Instruction limit % 300.13/43.07 % (1801978)Termination phase: Saturation % 300.13/43.07 % (1801978)Time elapsed: 0.071 s % 300.13/43.07 % (1801978)Peak memory usage: 116 MB % 300.13/43.07 % (1801978)Instructions burned: 78 (million) % 300.13/43.07 % (1801965)Instruction limit reached! % 300.13/43.07 % (1801965)------------------------------ % 300.13/43.07 % (1801965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801965)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801965)Termination reason: Instruction limit % 300.13/43.07 % (1801965)Termination phase: Saturation % 300.13/43.07 % (1801965)Time elapsed: 1.012 s % 300.13/43.07 % (1801965)Peak memory usage: 98 MB % 300.13/43.07 % (1801965)Instructions burned: 2000 (million) % 300.13/43.07 % (1801979)Instruction limit reached! % 300.13/43.07 % (1801979)------------------------------ % 300.13/43.07 % (1801979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801979)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801979)Termination reason: Instruction limit % 300.13/43.07 % (1801979)Termination phase: Saturation % 300.13/43.07 % (1801979)Time elapsed: 0.122 s % 300.13/43.07 % (1801979)Peak memory usage: 93 MB % 300.13/43.07 % (1801979)Instructions burned: 352 (million) % 300.13/43.07 % (1801882)Instruction limit reached! % 300.13/43.07 % (1801882)------------------------------ % 300.13/43.07 % (1801882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801882)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801882)Termination reason: Instruction limit % 300.13/43.07 % (1801882)Termination phase: Saturation % 300.13/43.07 % (1801882)Time elapsed: 4.509 s % 300.13/43.07 % (1801882)Peak memory usage: 177 MB % 300.13/43.07 % (1801882)Instructions burned: 8623 (million) % 300.13/43.07 % (1801982)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=705903700:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2580 on theBenchmark for (2580ds/658Mi) % 300.13/43.07 % (1801984)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1757762707:thitd=on:i=430:nm=0:rtra=on:ev=force_2579 on theBenchmark for (2579ds/430Mi) % 300.13/43.07 % (1801983)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=151408881:s2a=on:i=966:doe=on:nm=32:rtra=on_2580 on theBenchmark for (2580ds/966Mi) % 300.13/43.07 % (1801985)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=396583242:i=698:rtra=on_2579 on theBenchmark for (2579ds/698Mi) % 300.13/43.07 % (1801984)Instruction limit reached! % 300.13/43.07 % (1801984)------------------------------ % 300.13/43.07 % (1801984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.07 % (1801984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.07 % (1801984)CaDiCaL version: 2.1.3 % 300.13/43.07 % (1801984)Termination reason: Instruction limit % 300.13/43.07 % (1801984)Termination phase: Saturation % 300.13/43.07 % (1801984)Time ela % 300.13/43.07 Terminated %------------------------------------------------------------------------------