%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC453_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n007.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:58 PM UTC 2026 % Result : Timeout 288.89s 41.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC453_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.20 % Computer : n007.cluster.edu % 0.07/0.20 % Model : x86_64 x86_64 % 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.20 % Memory : 8046.5625MB % 0.07/0.20 % OS : Linux 6.8.0-71-generic % 0.07/0.20 % CPULimit : 300 % 0.07/0.20 % WCLimit : 300 % 0.07/0.20 % DateTime : Mon Sep 28 09:36:34 UTC 2026 % 0.07/0.21 % CPUTime : % 0.07/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.24 Running first-order theorem proving % 0.07/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.66/1.66 % (2270370)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.66/1.66 % (2270475)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=824465158:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.66/1.66 % (2270474)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=209704063:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.66/1.66 % (2270473)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=544805570:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.66/1.66 % (2270479)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2484713450:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.66/1.66 % (2270478)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3768153565:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.66/1.66 % (2270476)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1505548984:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.66/1.66 % (2270477)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2258183486:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.66/1.66 % (2270476)Instruction limit reached! % 5.66/1.66 % (2270476)------------------------------ % 5.66/1.66 % (2270476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.66/1.66 % (2270476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.66/1.66 % (2270476)CaDiCaL version: 2.1.3 % 5.66/1.66 % (2270476)Termination reason: Instruction limit % 5.66/1.66 % (2270476)Termination phase: Saturation % 5.66/1.66 % (2270476)Time elapsed: 0.008 s % 5.66/1.66 % (2270476)Peak memory usage: 88 MB % 5.66/1.66 % (2270476)Instructions burned: 7 (million) % 5.66/1.66 % (2270477)Instruction limit reached! % 5.66/1.66 % (2270477)------------------------------ % 5.66/1.66 % (2270477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.66/1.66 % (2270477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.66/1.66 % (2270477)CaDiCaL version: 2.1.3 % 5.66/1.66 % (2270477)Termination reason: Instruction limit % 5.66/1.66 % (2270477)Termination phase: Saturation % 5.66/1.66 % (2270477)Time elapsed: 0.005 s % 5.66/1.66 % (2270477)Peak memory usage: 89 MB % 5.66/1.66 % (2270477)Instructions burned: 4 (million) % 5.66/1.66 % (2270473)Instruction limit reached! % 5.66/1.66 % (2270473)------------------------------ % 5.66/1.66 % (2270473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.66/1.66 % (2270473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.66/1.66 % (2270473)CaDiCaL version: 2.1.3 % 5.66/1.66 % (2270473)Termination reason: Instruction limit % 5.66/1.66 % (2270473)Termination phase: Saturation % 5.66/1.66 % (2270473)Time elapsed: 0.039 s % 5.66/1.66 % (2270473)Peak memory usage: 116 MB % 5.66/1.66 % (2270473)Instructions burned: 12 (million) % 5.66/1.66 % (2270474)Refutation not found, incomplete strategy % 5.66/1.66 % (2270474)------------------------------ % 5.66/1.66 % (2270474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.66/1.66 % (2270474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.66/1.66 % (2270474)CaDiCaL version: 2.1.3 % 5.66/1.66 % (2270474)Termination reason: Refutation not found, incomplete strategy % 5.66/1.66 % (2270474)Time elapsed: 0.059 s % 5.66/1.66 % (2270474)Peak memory usage: 116 MB % 5.66/1.66 % (2270474)Instructions burned: 28 (million) % 5.66/1.66 % (2270478)Refutation not found, incomplete strategy % 5.66/1.66 % (2270478)------------------------------ % 5.66/1.66 % (2270478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.66/1.66 % (2270478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.66/1.66 % (2270478)CaDiCaL version: 2.1.3 % 5.66/1.66 % (2270478)Termination reason: Refutation not found, incomplete strategy % 5.66/1.66 % (2270478)Time elapsed: 0.042 s % 5.66/1.66 % (2270478)Peak memory usage: 115 MB % 5.66/1.66 % (2270478)Instructions burned: 7 (million) % 5.66/1.66 % (2270479)Instruction limit reached! % 5.66/1.66 % (2270479)------------------------------ % 5.66/1.66 % (2270479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.66/1.66 % (2270479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.92 % (2270479)CaDiCaL version: 2.1.3 % 7.08/1.92 % (2270479)Termination reason: Instruction limit % 7.08/1.92 % (2270479)Termination phase: Saturation % 7.08/1.92 % (2270479)Time elapsed: 0.068 s % 7.08/1.92 % (2270479)Peak memory usage: 116 MB % 7.08/1.92 % (2270479)Instructions burned: 34 (million) % 7.08/1.92 % (2270475)Instruction limit reached! % 7.08/1.92 % (2270475)------------------------------ % 7.08/1.92 % (2270475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.08/1.92 % (2270475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.92 % (2270475)CaDiCaL version: 2.1.3 % 7.08/1.92 % (2270475)Termination reason: Instruction limit % 7.08/1.92 % (2270475)Termination phase: Saturation % 7.08/1.92 % (2270475)Time elapsed: 0.124 s % 7.08/1.92 % (2270475)Peak memory usage: 117 MB % 7.08/1.92 % (2270475)Instructions burned: 201 (million) % 7.08/1.92 % (2270522)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=823715965:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 7.08/1.92 % (2270522)Refutation not found, incomplete strategy % 7.08/1.92 % (2270522)------------------------------ % 7.08/1.92 % (2270522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.08/1.92 % (2270522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.92 % (2270522)CaDiCaL version: 2.1.3 % 7.08/1.92 % (2270522)Termination reason: Refutation not found, incomplete strategy % 7.08/1.92 % (2270522)Time elapsed: 0.003 s % 7.08/1.92 % (2270522)Peak memory usage: 89 MB % 7.08/1.92 % (2270523)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=1125826201:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 7.08/1.92 % (2270530)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1544169172:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 7.08/1.92 % (2270530)Refutation not found, incomplete strategy % 7.08/1.92 % (2270530)------------------------------ % 7.08/1.92 % (2270530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.08/1.92 % (2270530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.92 % (2270530)CaDiCaL version: 2.1.3 % 7.08/1.92 % (2270530)Termination reason: Refutation not found, incomplete strategy % 7.08/1.92 % (2270530)Time elapsed: 0.006 s % 7.08/1.92 % (2270530)Peak memory usage: 90 MB % 7.08/1.92 % (2270530)Instructions burned: 3 (million) % 7.08/1.92 % (2270535)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=2838070269:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 7.08/1.92 % (2270523)Instruction limit reached! % 7.08/1.92 % (2270523)------------------------------ % 7.08/1.92 % (2270523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.08/1.92 % (2270523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.92 % (2270523)CaDiCaL version: 2.1.3 % 7.08/1.92 % (2270523)Termination reason: Instruction limit % 7.08/1.92 % (2270523)Termination phase: Saturation % 7.08/1.92 % (2270523)Time elapsed: 0.030 s % 7.08/1.92 % (2270523)Peak memory usage: 88 MB % 7.08/1.93 % (2270523)Instructions burned: 29 (million) % 7.08/1.93 % (2270535)Instruction limit reached! % 7.08/1.93 % (2270535)------------------------------ % 7.08/1.93 % (2270535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.08/1.93 % (2270535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.08/1.93 % (2270535)CaDiCaL version: 2.1.3 % 7.08/1.93 % (2270535)Termination reason: Instruction limit % 7.08/1.93 % (2270535)Termination phase: Saturation % 7.08/1.93 % (2270535)Time elapsed: 0.014 s % 7.08/1.93 % (2270535)Peak memory usage: 89 MB % 7.08/1.93 % (2270535)Instructions burned: 29 (million) % 7.08/1.93 % (2270534)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4220341857:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 7.08/1.93 % (2270474)------------------------------ % 7.08/1.93 % (2270474)------------------------------ % 7.08/1.93 % (2270534)Instruction limit reached! % 7.08/1.93 % (2270534)------------------------------ % 7.08/1.93 % (2270534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.08/1.93 % (2270534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.18/2.18 % (2270534)CaDiCaL version: 2.1.3 % 10.18/2.18 % (2270534)Termination reason: Instruction limit % 10.18/2.18 % (2270534)Termination phase: Saturation % 10.18/2.18 % (2270534)Time elapsed: 0.030 s % 10.18/2.18 % (2270534)Peak memory usage: 89 MB % 10.18/2.18 % (2270534)Instructions burned: 25 (million) % 10.18/2.18 % (2270478)------------------------------ % 10.18/2.18 % (2270478)------------------------------ % 10.18/2.18 % (2270554)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=27209749:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 10.18/2.18 % (2270556)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1160875699:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 10.18/2.18 % (2270556)Instruction limit reached! % 10.18/2.18 % (2270556)------------------------------ % 10.18/2.18 % (2270556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.18/2.18 % (2270556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.18/2.18 % (2270556)CaDiCaL version: 2.1.3 % 10.18/2.18 % (2270556)Termination reason: Instruction limit % 10.18/2.18 % (2270556)Termination phase: Saturation % 10.18/2.18 % (2270556)Time elapsed: 0.004 s % 10.18/2.18 % (2270556)Peak memory usage: 89 MB % 10.18/2.18 % (2270556)Instructions burned: 2 (million) % 10.18/2.18 % (2270554)Instruction limit reached! % 10.18/2.18 % (2270554)------------------------------ % 10.18/2.18 % (2270554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.18/2.18 % (2270554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.18/2.18 % (2270554)CaDiCaL version: 2.1.3 % 10.18/2.18 % (2270554)Termination reason: Instruction limit % 10.18/2.18 % (2270554)Termination phase: Saturation % 10.18/2.18 % (2270554)Time elapsed: 0.053 s % 10.18/2.18 % (2270554)Peak memory usage: 89 MB % 10.18/2.18 % (2270554)Instructions burned: 85 (million) % 10.18/2.18 % (2270561)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1012222735:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 10.18/2.18 % (2270561)Instruction limit reached! % 10.18/2.18 % (2270561)------------------------------ % 10.18/2.18 % (2270561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.18/2.18 % (2270561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.18/2.18 % (2270561)CaDiCaL version: 2.1.3 % 10.18/2.18 % (2270561)Termination reason: Instruction limit % 10.18/2.18 % (2270561)Termination phase: Saturation % 10.18/2.18 % (2270561)Time elapsed: 0.006 s % 10.18/2.18 % (2270561)Peak memory usage: 89 MB % 10.18/2.18 % (2270561)Instructions burned: 4 (million) % 10.18/2.18 % (2270560)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=989526687:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 10.18/2.18 % (2270522)------------------------------ % 10.18/2.18 % (2270522)------------------------------ % 10.18/2.18 % (2270560)Refutation not found, incomplete strategy % 10.18/2.18 % (2270560)------------------------------ % 10.18/2.18 % (2270560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.18/2.18 % (2270560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.18/2.18 % (2270560)CaDiCaL version: 2.1.3 % 10.18/2.18 % (2270560)Termination reason: Refutation not found, incomplete strategy % 10.18/2.18 % (2270560)Time elapsed: 0.004 s % 10.18/2.18 % (2270560)Peak memory usage: 89 MB % 10.18/2.18 % (2270560)Instructions burned: 2 (million) % 10.18/2.18 % (2270530)------------------------------ % 10.18/2.18 % (2270530)------------------------------ % 10.18/2.18 % (2270562)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1260596015:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 10.18/2.18 % (2270568)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=1431599157:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 10.18/2.18 % (2270565)lrs+10_1_thi=all:si=on:fd=off:random_seed=843562772:i=53:rtra=on:gtg=all_2992 on theBenchmark for (2992ds/53Mi) % 10.18/2.18 % (2270568)Instruction limit reached! % 10.18/2.18 % (2270568)------------------------------ % 10.18/2.18 % (2270568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.18/2.18 % (2270568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.18/2.18 % (2270568)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270568)Termination reason: Instruction limit % 11.75/2.60 % (2270568)Termination phase: Saturation % 11.75/2.60 % (2270568)Time elapsed: 0.006 s % 11.75/2.60 % (2270568)Peak memory usage: 88 MB % 11.75/2.60 % (2270568)Instructions burned: 10 (million) % 11.75/2.60 % (2270562)Instruction limit reached! % 11.75/2.60 % (2270562)------------------------------ % 11.75/2.60 % (2270562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.75/2.60 % (2270562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.75/2.60 % (2270562)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270562)Termination reason: Instruction limit % 11.75/2.60 % (2270562)Termination phase: Saturation % 11.75/2.60 % (2270562)Time elapsed: 0.136 s % 11.75/2.60 % (2270562)Peak memory usage: 134 MB % 11.75/2.60 % (2270562)Instructions burned: 66 (million) % 11.75/2.60 % (2270565)Instruction limit reached! % 11.75/2.60 % (2270565)------------------------------ % 11.75/2.60 % (2270565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.75/2.60 % (2270565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.75/2.60 % (2270565)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270565)Termination reason: Instruction limit % 11.75/2.60 % (2270565)Termination phase: Saturation % 11.75/2.60 % (2270565)Time elapsed: 0.064 s % 11.75/2.60 % (2270565)Peak memory usage: 116 MB % 11.75/2.60 % (2270565)Instructions burned: 54 (million) % 11.75/2.60 % (2270569)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=656019995:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 11.75/2.60 % (2270569)Instruction limit reached! % 11.75/2.60 % (2270569)------------------------------ % 11.75/2.60 % (2270569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.75/2.60 % (2270569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.75/2.60 % (2270569)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270569)Termination reason: Instruction limit % 11.75/2.60 % (2270569)Termination phase: Saturation % 11.75/2.60 % (2270569)Time elapsed: 0.004 s % 11.75/2.60 % (2270569)Peak memory usage: 90 MB % 11.75/2.60 % (2270569)Instructions burned: 2 (million) % 11.75/2.60 % (2270573)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1056274203:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi) % 11.75/2.60 % (2270576)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=598325992:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 11.75/2.60 % (2270573)Instruction limit reached! % 11.75/2.60 % (2270573)------------------------------ % 11.75/2.60 % (2270573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.75/2.60 % (2270573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.75/2.60 % (2270573)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270573)Termination reason: Instruction limit % 11.75/2.60 % (2270573)Termination phase: Saturation % 11.75/2.60 % (2270573)Time elapsed: 0.004 s % 11.75/2.60 % (2270573)Peak memory usage: 89 MB % 11.75/2.60 % (2270573)Instructions burned: 2 (million) % 11.75/2.60 % (2270560)------------------------------ % 11.75/2.60 % (2270560)------------------------------ % 11.75/2.60 % (2270585)dis+10_1_si=on:random_seed=3899778990:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 11.75/2.60 % (2270585)Instruction limit reached! % 11.75/2.60 % (2270585)------------------------------ % 11.75/2.60 % (2270585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.75/2.60 % (2270585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.75/2.60 % (2270585)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270585)Termination reason: Instruction limit % 11.75/2.60 % (2270585)Termination phase: Saturation % 11.75/2.60 % (2270585)Time elapsed: 0.012 s % 11.75/2.60 % (2270585)Peak memory usage: 88 MB % 11.75/2.60 % (2270585)Instructions burned: 10 (million) % 11.75/2.60 % (2270587)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2655079327: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_2989 on theBenchmark for (2989ds/35Mi) % 11.75/2.60 % (2270576)Instruction limit reached! % 11.75/2.60 % (2270576)------------------------------ % 11.75/2.60 % (2270576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.75/2.60 % (2270576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.75/2.60 % (2270576)CaDiCaL version: 2.1.3 % 11.75/2.60 % (2270576)Termination reason: Instruction limit % 14.52/3.07 % (2270576)Termination phase: Saturation % 14.52/3.07 % (2270576)Time elapsed: 0.156 s % 14.52/3.07 % (2270576)Peak memory usage: 117 MB % 14.52/3.07 % (2270576)Instructions burned: 127 (million) % 14.52/3.07 % (2270587)Instruction limit reached! % 14.52/3.07 % (2270587)------------------------------ % 14.52/3.07 % (2270587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.52/3.07 % (2270587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.52/3.07 % (2270587)CaDiCaL version: 2.1.3 % 14.52/3.07 % (2270587)Termination reason: Instruction limit % 14.52/3.07 % (2270587)Termination phase: Saturation % 14.52/3.07 % (2270587)Time elapsed: 0.023 s % 14.52/3.07 % (2270587)Peak memory usage: 89 MB % 14.52/3.07 % (2270587)Instructions burned: 35 (million) % 14.52/3.07 % (2270589)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=470272567:i=2:fsr=off:rtra=on:inst=on_2989 on theBenchmark for (2989ds/2Mi) % 14.52/3.07 % (2270586)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2968745289:i=26:canc=cautious:av=off:rtra=on_2989 on theBenchmark for (2989ds/26Mi) % 14.52/3.07 % (2270589)Instruction limit reached! % 14.52/3.07 % (2270589)------------------------------ % 14.52/3.07 % (2270589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.52/3.07 % (2270589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.52/3.07 % (2270589)CaDiCaL version: 2.1.3 % 14.52/3.07 % (2270589)Termination reason: Instruction limit % 14.52/3.07 % (2270589)Termination phase: Saturation % 14.52/3.07 % (2270589)Time elapsed: 0.004 s % 14.52/3.07 % (2270589)Peak memory usage: 88 MB % 14.52/3.07 % (2270589)Instructions burned: 2 (million) % 14.52/3.07 % (2270586)Refutation not found, incomplete strategy % 14.52/3.07 % (2270586)------------------------------ % 14.52/3.07 % (2270586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.52/3.07 % (2270586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.52/3.07 % (2270586)CaDiCaL version: 2.1.3 % 14.52/3.07 % (2270586)Termination reason: Refutation not found, incomplete strategy % 14.52/3.07 % (2270586)Time elapsed: 0.004 s % 14.52/3.07 % (2270586)Peak memory usage: 88 MB % 14.52/3.07 % (2270586)Instructions burned: 2 (million) % 14.52/3.07 % (2270592)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3883041026:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 14.52/3.07 % (2270592)Instruction limit reached! % 14.52/3.07 % (2270592)------------------------------ % 14.52/3.07 % (2270592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.52/3.07 % (2270592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.52/3.07 % (2270592)CaDiCaL version: 2.1.3 % 14.52/3.07 % (2270592)Termination reason: Instruction limit % 14.52/3.07 % (2270592)Termination phase: Saturation % 14.52/3.07 % (2270592)Time elapsed: 0.011 s % 14.52/3.07 % (2270592)Peak memory usage: 89 MB % 14.52/3.07 % (2270592)Instructions burned: 8 (million) % 14.52/3.07 % (2270603)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2965067070:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi) % 14.52/3.07 % (2270602)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2481675966:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/13Mi) % 14.52/3.07 % (2270603)Refutation not found, incomplete strategy % 14.52/3.07 % (2270603)------------------------------ % 14.52/3.07 % (2270603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.52/3.07 % (2270603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.52/3.07 % (2270603)CaDiCaL version: 2.1.3 % 14.52/3.07 % (2270603)Termination reason: Refutation not found, incomplete strategy % 14.52/3.07 % (2270603)Time elapsed: 0.025 s % 14.52/3.07 % (2270603)Peak memory usage: 116 MB % 14.52/3.07 % (2270603)Instructions burned: 7 (million) % 14.52/3.07 % (2270601)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3164340036:i=370:ep=RS:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/370Mi) % 14.52/3.07 % (2270602)Instruction limit reached! % 14.52/3.07 % (2270602)------------------------------ % 14.52/3.07 % (2270602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.52/3.07 % (2270602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.52/3.07 % (2270602)CaDiCaL version: 2.1.3 % 19.65/3.54 % (2270602)Termination reason: Instruction limit % 19.65/3.54 % (2270602)Termination phase: Saturation % 19.65/3.54 % (2270602)Time elapsed: 0.046 s % 19.65/3.54 % (2270602)Peak memory usage: 116 MB % 19.65/3.54 % (2270602)Instructions burned: 13 (million) % 19.65/3.54 % (2270604)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1035258015:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 19.65/3.54 % (2270604)Refutation not found, incomplete strategy % 19.65/3.54 % (2270604)------------------------------ % 19.65/3.54 % (2270604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.54 % (2270604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.54 % (2270604)CaDiCaL version: 2.1.3 % 19.65/3.54 % (2270604)Termination reason: Refutation not found, incomplete strategy % 19.65/3.54 % (2270604)Time elapsed: 0.002 s % 19.65/3.54 % (2270604)Peak memory usage: 88 MB % 19.65/3.54 % (2270586)------------------------------ % 19.65/3.54 % (2270586)------------------------------ % 19.65/3.54 % (2270614)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=1353017386:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2986 on theBenchmark for (2986ds/75Mi) % 19.65/3.54 % (2270607)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=827846478:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 19.65/3.54 % (2270614)Instruction limit reached! % 19.65/3.54 % (2270614)------------------------------ % 19.65/3.54 % (2270614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.54 % (2270614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.54 % (2270614)CaDiCaL version: 2.1.3 % 19.65/3.54 % (2270614)Termination reason: Instruction limit % 19.65/3.54 % (2270614)Termination phase: Saturation % 19.65/3.54 % (2270614)Time elapsed: 0.063 s % 19.65/3.54 % (2270614)Peak memory usage: 89 MB % 19.65/3.54 % (2270614)Instructions burned: 76 (million) % 19.65/3.54 % (2270607)Refutation not found, incomplete strategy % 19.65/3.54 % (2270607)------------------------------ % 19.65/3.54 % (2270607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.54 % (2270607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.54 % (2270607)CaDiCaL version: 2.1.3 % 19.65/3.54 % (2270607)Termination reason: Refutation not found, incomplete strategy % 19.65/3.54 % (2270607)Time elapsed: 0.078 s % 19.65/3.54 % (2270607)Peak memory usage: 132 MB % 19.65/3.54 % (2270607)Instructions burned: 12 (million) % 19.65/3.54 % (2270603)------------------------------ % 19.65/3.54 % (2270603)------------------------------ % 19.65/3.54 % (2270621)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=405364387:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/130Mi) % 19.65/3.54 % (2270619)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=152564872:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2985 on theBenchmark for (2985ds/294Mi) % 19.65/3.54 % (2270601)Instruction limit reached! % 19.65/3.54 % (2270601)------------------------------ % 19.65/3.54 % (2270601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.54 % (2270601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.54 % (2270601)CaDiCaL version: 2.1.3 % 19.65/3.54 % (2270601)Termination reason: Instruction limit % 19.65/3.54 % (2270601)Termination phase: Saturation % 19.65/3.54 % (2270601)Time elapsed: 0.296 s % 19.65/3.54 % (2270601)Peak memory usage: 89 MB % 19.65/3.54 % (2270601)Instructions burned: 370 (million) % 19.65/3.54 % (2270621)Refutation not found, incomplete strategy % 19.65/3.54 % (2270621)------------------------------ % 19.65/3.54 % (2270621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.65/3.54 % (2270621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.65/3.54 % (2270621)CaDiCaL version: 2.1.3 % 19.65/3.54 % (2270621)Termination reason: Refutation not found, incomplete strategy % 19.65/3.54 % (2270621)Time elapsed: 0.039 s % 19.65/3.54 % (2270621)Peak memory usage: 116 MB % 19.65/3.54 % (2270621)Instructions burned: 18 (million) % 19.65/3.54 % (2270604)------------------------------ % 19.65/3.54 % (2270604)------------------------------ % 19.65/3.54 % (2270624)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2127397119:i=131:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 20.59/3.89 % (2270619)Instruction limit reached! % 20.59/3.89 % (2270619)------------------------------ % 20.59/3.89 % (2270619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.59/3.89 % (2270619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.89 % (2270619)CaDiCaL version: 2.1.3 % 20.59/3.89 % (2270619)Termination reason: Instruction limit % 20.59/3.89 % (2270619)Termination phase: Saturation % 20.59/3.89 % (2270619)Time elapsed: 0.193 s % 20.59/3.89 % (2270619)Peak memory usage: 88 MB % 20.59/3.89 % (2270619)Instructions burned: 295 (million) % 20.59/3.89 % (2270624)Refutation not found, incomplete strategy % 20.59/3.89 % (2270624)------------------------------ % 20.59/3.89 % (2270624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.59/3.89 % (2270624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.89 % (2270624)CaDiCaL version: 2.1.3 % 20.59/3.89 % (2270624)Termination reason: Refutation not found, incomplete strategy % 20.59/3.89 % (2270624)Time elapsed: 0.075 s % 20.59/3.89 % (2270624)Peak memory usage: 132 MB % 20.59/3.89 % (2270624)Instructions burned: 12 (million) % 20.59/3.89 % (2270625)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=516752804:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2983 on theBenchmark for (2983ds/40Mi) % 20.59/3.89 % (2270621)------------------------------ % 20.59/3.89 % (2270621)------------------------------ % 20.59/3.89 % (2270628)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=849787640:i=307:rtra=on:gtg=exists_top_2982 on theBenchmark for (2982ds/307Mi) % 20.59/3.89 % (2270607)------------------------------ % 20.59/3.89 % (2270607)------------------------------ % 20.59/3.89 % (2270625)Instruction limit reached! % 20.59/3.89 % (2270625)------------------------------ % 20.59/3.89 % (2270625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.59/3.89 % (2270625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.89 % (2270625)CaDiCaL version: 2.1.3 % 20.59/3.89 % (2270625)Termination reason: Instruction limit % 20.59/3.89 % (2270625)Termination phase: Saturation % 20.59/3.89 % (2270625)Time elapsed: 0.102 s % 20.59/3.89 % (2270625)Peak memory usage: 133 MB % 20.59/3.89 % (2270625)Instructions burned: 40 (million) % 20.59/3.89 % (2270630)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1354759599:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2980 on theBenchmark for (2980ds/598Mi) % 20.59/3.89 % (2270631)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2453164898:i=131:canc=cautious:fsr=off:rtra=on_2980 on theBenchmark for (2980ds/131Mi) % 20.59/3.89 % (2270635)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=3115494381:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2979 on theBenchmark for (2979ds/259Mi) % 20.59/3.89 % (2270630)Refutation not found, incomplete strategy % 20.59/3.89 % (2270630)------------------------------ % 20.59/3.89 % (2270630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.59/3.89 % (2270630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.89 % (2270630)CaDiCaL version: 2.1.3 % 20.59/3.89 % (2270630)Termination reason: Refutation not found, incomplete strategy % 20.59/3.89 % (2270630)Time elapsed: 0.081 s % 20.59/3.89 % (2270630)Peak memory usage: 133 MB % 20.59/3.89 % (2270630)Instructions burned: 13 (million) % 20.59/3.89 % (2270628)Instruction limit reached! % 20.59/3.89 % (2270628)------------------------------ % 20.59/3.89 % (2270628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.59/3.89 % (2270628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.59/3.89 % (2270628)CaDiCaL version: 2.1.3 % 20.59/3.89 % (2270628)Termination reason: Instruction limit % 20.59/3.89 % (2270628)Termination phase: Saturation % 20.59/3.89 % (2270628)Time elapsed: 0.255 s % 20.59/3.89 % (2270628)Peak memory usage: 91 MB % 20.59/3.89 % (2270628)Instructions burned: 307 (million) % 20.59/3.89 % (2270637)dis+10_1_si=on:random_seed=2727859923:s2a=on:i=1000:rtra=on:gtg=exists_all_2979 on theBenchmark for (2979ds/1000Mi) % 20.59/3.89 % (2270624)------------------------------ % 20.59/3.89 % (2270624)------------------------------ % 20.59/3.89 % (2270638)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=767883011:i=383:fsr=off:rtra=on:ev=force_2979 on theBenchmark for (2979ds/383Mi) % 26.07/4.55 % (2270638)Refutation not found, incomplete strategy % 26.07/4.55 % (2270638)------------------------------ % 26.07/4.55 % (2270638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.07/4.55 % (2270638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.07/4.55 % (2270638)CaDiCaL version: 2.1.3 % 26.07/4.55 % (2270638)Termination reason: Refutation not found, incomplete strategy % 26.07/4.55 % (2270638)Time elapsed: 0.005 s % 26.07/4.55 % (2270638)Peak memory usage: 89 MB % 26.07/4.55 % (2270638)Instructions burned: 3 (million) % 26.07/4.55 % (2270635)Instruction limit reached! % 26.07/4.55 % (2270635)------------------------------ % 26.07/4.55 % (2270635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.07/4.55 % (2270635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.07/4.55 % (2270635)CaDiCaL version: 2.1.3 % 26.07/4.55 % (2270635)Termination reason: Instruction limit % 26.07/4.55 % (2270635)Termination phase: Saturation % 26.07/4.55 % (2270635)Time elapsed: 0.141 s % 26.07/4.55 % (2270635)Peak memory usage: 116 MB % 26.07/4.55 % (2270635)Instructions burned: 259 (million) % 26.07/4.55 % (2270631)Instruction limit reached! % 26.07/4.55 % (2270631)------------------------------ % 26.07/4.55 % (2270631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.07/4.55 % (2270631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.07/4.55 % (2270631)CaDiCaL version: 2.1.3 % 26.07/4.55 % (2270631)Termination reason: Instruction limit % 26.07/4.55 % (2270631)Termination phase: Saturation % 26.07/4.55 % (2270631)Time elapsed: 0.163 s % 26.07/4.55 % (2270631)Peak memory usage: 118 MB % 26.07/4.55 % (2270631)Instructions burned: 132 (million) % 26.07/4.55 % (2270644)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2387291914:i=141:doe=on:rtra=on_2977 on theBenchmark for (2977ds/141Mi) % 26.07/4.55 % (2270648)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3540871894:i=121:nm=16:rtra=on_2976 on theBenchmark for (2976ds/121Mi) % 26.07/4.55 % (2270647)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2072234297:i=65:nm=16:rtra=on_2976 on theBenchmark for (2976ds/65Mi) % 26.07/4.55 % (2270648)Instruction limit reached! % 26.07/4.55 % (2270648)------------------------------ % 26.07/4.55 % (2270648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.07/4.55 % (2270648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.07/4.55 % (2270648)CaDiCaL version: 2.1.3 % 26.07/4.55 % (2270648)Termination reason: Instruction limit % 26.07/4.55 % (2270648)Termination phase: Saturation % 26.07/4.55 % (2270648)Time elapsed: 0.047 s % 26.07/4.55 % (2270648)Peak memory usage: 88 MB % 26.07/4.55 % (2270648)Instructions burned: 123 (million) % 26.07/4.55 % (2270630)------------------------------ % 26.07/4.55 % (2270630)------------------------------ % 26.07/4.55 % (2270647)Refutation not found, incomplete strategy % 26.07/4.55 % (2270647)------------------------------ % 26.07/4.55 % (2270647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.07/4.55 % (2270647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.07/4.55 % (2270647)CaDiCaL version: 2.1.3 % 26.07/4.55 % (2270647)Termination reason: Refutation not found, incomplete strategy % 26.07/4.55 % (2270647)Time elapsed: 0.041 s % 26.07/4.55 % (2270647)Peak memory usage: 115 MB % 26.07/4.55 % (2270647)Instructions burned: 6 (million) % 26.07/4.55 % (2270649)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=4097361941:s2a=on:i=128:s2at=5:ins=3:rtra=on_2976 on theBenchmark for (2976ds/128Mi) % 26.07/4.55 % (2270644)Instruction limit reached! % 26.07/4.55 % (2270644)------------------------------ % 26.07/4.55 % (2270644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.07/4.55 % (2270644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.07/4.55 % (2270644)CaDiCaL version: 2.1.3 % 26.07/4.55 % (2270644)Termination reason: Instruction limit % 26.07/4.55 % (2270644)Termination phase: Saturation % 26.07/4.55 % (2270644)Time elapsed: 0.148 s % 26.07/4.55 % (2270644)Peak memory usage: 90 MB % 26.07/4.55 % (2270644)Instructions burned: 141 (million) % 26.07/4.55 % (2270638)------------------------------ % 26.07/4.55 % (2270638)------------------------------ % 26.07/4.55 % (2270649)Instruction limit reached! % 26.07/4.55 % (2270649)------------------------------ % 26.94/4.91 % (2270649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.91 % (2270649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.91 % (2270649)CaDiCaL version: 2.1.3 % 26.94/4.91 % (2270649)Termination reason: Instruction limit % 26.94/4.91 % (2270649)Termination phase: Saturation % 26.94/4.91 % (2270649)Time elapsed: 0.168 s % 26.94/4.91 % (2270649)Peak memory usage: 117 MB % 26.94/4.91 % (2270649)Instructions burned: 128 (million) % 26.94/4.91 % (2270653)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=566506108:i=39:ins=3:rtra=on_2973 on theBenchmark for (2973ds/39Mi) % 26.94/4.91 % (2270653)Instruction limit reached! % 26.94/4.91 % (2270653)------------------------------ % 26.94/4.91 % (2270653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.91 % (2270653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.91 % (2270653)CaDiCaL version: 2.1.3 % 26.94/4.91 % (2270653)Termination reason: Instruction limit % 26.94/4.91 % (2270653)Termination phase: Saturation % 26.94/4.91 % (2270653)Time elapsed: 0.042 s % 26.94/4.91 % (2270653)Peak memory usage: 116 MB % 26.94/4.91 % (2270653)Instructions burned: 39 (million) % 26.94/4.91 % (2270654)dis+1010_1_to=kbo:si=on:random_seed=263313002:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2973 on theBenchmark for (2973ds/175Mi) % 26.94/4.91 % (2270656)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=459460766:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2972 on theBenchmark for (2972ds/329Mi) % 26.94/4.91 % (2270657)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=488780164:s2a=on:i=483:doe=on:nm=32:rtra=on_2972 on theBenchmark for (2972ds/483Mi) % 26.94/4.91 % (2270647)------------------------------ % 26.94/4.91 % (2270647)------------------------------ % 26.94/4.91 % (2270659)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1649498345:thitd=on:i=215:nm=0:rtra=on:ev=force_2971 on theBenchmark for (2971ds/215Mi) % 26.94/4.91 % (2270660)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=45135007:i=349:rtra=on_2971 on theBenchmark for (2971ds/349Mi) % 26.94/4.91 % (2270657)Refutation not found, incomplete strategy % 26.94/4.91 % (2270657)------------------------------ % 26.94/4.91 % (2270657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.91 % (2270657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.91 % (2270657)CaDiCaL version: 2.1.3 % 26.94/4.91 % (2270657)Termination reason: Refutation not found, incomplete strategy % 26.94/4.91 % (2270657)Time elapsed: 0.077 s % 26.94/4.91 % (2270657)Peak memory usage: 132 MB % 26.94/4.91 % (2270657)Instructions burned: 12 (million) % 26.94/4.91 % (2270654)Instruction limit reached! % 26.94/4.91 % (2270654)------------------------------ % 26.94/4.91 % (2270654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.91 % (2270654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.91 % (2270654)CaDiCaL version: 2.1.3 % 26.94/4.91 % (2270654)Termination reason: Instruction limit % 26.94/4.91 % (2270654)Termination phase: Saturation % 26.94/4.91 % (2270654)Time elapsed: 0.200 s % 26.94/4.91 % (2270654)Peak memory usage: 90 MB % 26.94/4.91 % (2270654)Instructions burned: 175 (million) % 26.94/4.91 % (2270660)Refutation not found, incomplete strategy % 26.94/4.91 % (2270660)------------------------------ % 26.94/4.91 % (2270660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.91 % (2270660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.91 % (2270660)CaDiCaL version: 2.1.3 % 26.94/4.91 % (2270660)Termination reason: Refutation not found, incomplete strategy % 26.94/4.91 % (2270660)Time elapsed: 0.025 s % 26.94/4.91 % (2270660)Peak memory usage: 116 MB % 26.94/4.91 % (2270660)Instructions burned: 7 (million) % 26.94/4.91 % (2270659)Refutation not found, incomplete strategy % 26.94/4.91 % (2270659)------------------------------ % 26.94/4.91 % (2270659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.91 % (2270659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.91 % (2270659)CaDiCaL version: 2.1.3 % 26.94/4.91 % (2270659)Termination reason: Refutation not found, incomplete strategy % 26.94/4.91 % (2270659)Time elapsed: 0.099 s % 33.15/5.44 % (2270659)Peak memory usage: 134 MB % 33.15/5.44 % (2270659)Instructions burned: 31 (million) % 33.15/5.44 % (2270637)Instruction limit reached! % 33.15/5.44 % (2270637)------------------------------ % 33.15/5.44 % (2270637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.15/5.44 % (2270637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.15/5.44 % (2270637)CaDiCaL version: 2.1.3 % 33.15/5.44 % (2270637)Termination reason: Instruction limit % 33.15/5.44 % (2270637)Termination phase: Saturation % 33.15/5.44 % (2270637)Time elapsed: 1.021 s % 33.15/5.44 % (2270637)Peak memory usage: 95 MB % 33.15/5.44 % (2270637)Instructions burned: 1000 (million) % 33.15/5.44 % (2270664)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1910664665:st=2:i=295:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/295Mi) % 33.15/5.44 % (2270660)------------------------------ % 33.15/5.44 % (2270660)------------------------------ % 33.15/5.44 % (2270656)Instruction limit reached! % 33.15/5.44 % (2270656)------------------------------ % 33.15/5.44 % (2270656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.15/5.44 % (2270656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.15/5.44 % (2270656)CaDiCaL version: 2.1.3 % 33.15/5.44 % (2270656)Termination reason: Instruction limit % 33.15/5.44 % (2270656)Termination phase: Saturation % 33.15/5.44 % (2270656)Time elapsed: 0.413 s % 33.15/5.44 % (2270656)Peak memory usage: 118 MB % 33.15/5.44 % (2270656)Instructions burned: 329 (million) % 33.15/5.44 % (2270667)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2094884834:i=328:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/328Mi) % 33.15/5.44 % (2270657)------------------------------ % 33.15/5.44 % (2270657)------------------------------ % 33.15/5.44 % (2270659)------------------------------ % 33.15/5.44 % (2270659)------------------------------ % 33.15/5.44 % (2270670)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1243510232:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2966 on theBenchmark for (2966ds/484Mi) % 33.15/5.44 % (2270664)Instruction limit reached! % 33.15/5.44 % (2270664)------------------------------ % 33.15/5.44 % (2270664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.15/5.44 % (2270664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.15/5.44 % (2270664)CaDiCaL version: 2.1.3 % 33.15/5.44 % (2270664)Termination reason: Instruction limit % 33.15/5.44 % (2270664)Termination phase: Saturation % 33.15/5.44 % (2270664)Time elapsed: 0.274 s % 33.15/5.44 % (2270664)Peak memory usage: 90 MB % 33.15/5.44 % (2270664)Instructions burned: 296 (million) % 33.15/5.44 % (2270669)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2961259753:i=281:gtgl=2:rtra=on:gtg=all_2966 on theBenchmark for (2966ds/281Mi) % 33.15/5.44 % (2270672)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3291101364:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2965 on theBenchmark for (2965ds/321Mi) % 33.15/5.44 % (2270667)Instruction limit reached! % 33.15/5.44 % (2270667)------------------------------ % 33.15/5.44 % (2270667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.15/5.44 % (2270667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.15/5.44 % (2270667)CaDiCaL version: 2.1.3 % 33.15/5.44 % (2270667)Termination reason: Instruction limit % 33.15/5.44 % (2270667)Termination phase: Saturation % 33.15/5.44 % (2270667)Time elapsed: 0.383 s % 33.15/5.44 % (2270667)Peak memory usage: 119 MB % 33.15/5.44 % (2270667)Instructions burned: 328 (million) % 33.15/5.44 % (2270673)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=168583422:i=416:rtra=on:gtg=position:ss=axioms_2964 on theBenchmark for (2964ds/416Mi) % 33.15/5.44 % (2270670)Instruction limit reached! % 33.15/5.44 % (2270670)------------------------------ % 33.15/5.44 % (2270670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.15/5.44 % (2270673)Refutation not found, incomplete strategy % 33.15/5.44 % (2270673)------------------------------ % 33.15/5.44 % (2270673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.15/5.44 % (2270673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.15/5.44 % (2270673)CaDiCaL version: 2.1.3 % 33.15/5.44 % (2270673)Termination reason: Refutation not found, incomplete strategy % 33.15/5.44 % (2270673)Time elapsed: 0.059 s % 33.15/5.44 % (2270673)Peak memory usage: 116 MB % 34.95/5.93 % (2270673)Instructions burned: 7 (million) % 34.95/5.93 % (2270670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.93 % (2270670)CaDiCaL version: 2.1.3 % 34.95/5.93 % (2270670)Termination reason: Instruction limit % 34.95/5.93 % (2270670)Termination phase: Saturation % 34.95/5.93 % (2270670)Time elapsed: 0.252 s % 34.95/5.93 % (2270670)Peak memory usage: 91 MB % 34.95/5.93 % (2270670)Instructions burned: 517 (million) % 34.95/5.93 % (2270675)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1143102878:i=471:thf=on:kws=precedence:rtra=on_2964 on theBenchmark for (2964ds/471Mi) % 34.95/5.93 % (2270677)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=2337167799:avsq=on:i=276:avsqr=1,2:rtra=on_2963 on theBenchmark for (2963ds/276Mi) % 34.95/5.93 % (2270675)Refutation not found, incomplete strategy % 34.95/5.93 % (2270675)------------------------------ % 34.95/5.93 % (2270675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.93 % (2270675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.93 % (2270675)CaDiCaL version: 2.1.3 % 34.95/5.93 % (2270675)Termination reason: Refutation not found, incomplete strategy % 34.95/5.93 % (2270675)Time elapsed: 0.042 s % 34.95/5.93 % (2270675)Peak memory usage: 116 MB % 34.95/5.93 % (2270675)Instructions burned: 7 (million) % 34.95/5.93 % (2270669)Instruction limit reached! % 34.95/5.93 % (2270669)------------------------------ % 34.95/5.93 % (2270669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.93 % (2270669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.93 % (2270669)CaDiCaL version: 2.1.3 % 34.95/5.93 % (2270669)Termination reason: Instruction limit % 34.95/5.93 % (2270669)Termination phase: Saturation % 34.95/5.93 % (2270669)Time elapsed: 0.331 s % 34.95/5.93 % (2270669)Peak memory usage: 117 MB % 34.95/5.93 % (2270669)Instructions burned: 281 (million) % 34.95/5.93 % (2270672)Instruction limit reached! % 34.95/5.93 % (2270672)------------------------------ % 34.95/5.93 % (2270672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.93 % (2270672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.93 % (2270672)CaDiCaL version: 2.1.3 % 34.95/5.93 % (2270672)Termination reason: Instruction limit % 34.95/5.93 % (2270672)Termination phase: Saturation % 34.95/5.93 % (2270672)Time elapsed: 0.322 s % 34.95/5.93 % (2270672)Peak memory usage: 114 MB % 34.95/5.93 % (2270672)Instructions burned: 322 (million) % 34.95/5.93 % (2270680)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3673417163:i=375:kws=inv_arity_squared:rtra=on_2962 on theBenchmark for (2962ds/375Mi) % 34.95/5.93 % (2270681)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=627308930:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/387Mi) % 34.95/5.93 % (2270680)Refutation not found, incomplete strategy % 34.95/5.93 % (2270680)------------------------------ % 34.95/5.93 % (2270680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.93 % (2270680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.93 % (2270680)CaDiCaL version: 2.1.3 % 34.95/5.93 % (2270680)Termination reason: Refutation not found, incomplete strategy % 34.95/5.93 % (2270680)Time elapsed: 0.041 s % 34.95/5.93 % (2270680)Peak memory usage: 115 MB % 34.95/5.93 % (2270680)Instructions burned: 7 (million) % 34.95/5.93 % (2270684)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1508112146:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2960 on theBenchmark for (2960ds/513Mi) % 34.95/5.93 % (2270673)------------------------------ % 34.95/5.93 % (2270673)------------------------------ % 34.95/5.93 % (2270677)Instruction limit reached! % 34.95/5.93 % (2270677)------------------------------ % 34.95/5.93 % (2270677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.95/5.93 % (2270677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.95/5.93 % (2270677)CaDiCaL version: 2.1.3 % 34.95/5.93 % (2270677)Termination reason: Instruction limit % 34.95/5.93 % (2270677)Termination phase: Saturation % 34.95/5.93 % (2270677)Time elapsed: 0.319 s % 34.95/5.93 % (2270677)Peak memory usage: 133 MB % 34.95/5.93 % (2270677)Instructions burned: 277 (million) % 40.51/6.50 % (2270675)------------------------------ % 40.51/6.50 % (2270675)------------------------------ % 40.51/6.50 % (2270685)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1828521266:i=334:rtra=on_2959 on theBenchmark for (2959ds/334Mi) % 40.51/6.50 % (2270681)Instruction limit reached! % 40.51/6.50 % (2270681)------------------------------ % 40.51/6.50 % (2270681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.51/6.50 % (2270681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.51/6.50 % (2270681)CaDiCaL version: 2.1.3 % 40.51/6.50 % (2270681)Termination reason: Instruction limit % 40.51/6.50 % (2270681)Termination phase: Saturation % 40.51/6.50 % (2270681)Time elapsed: 0.264 s % 40.51/6.50 % (2270681)Peak memory usage: 119 MB % 40.51/6.50 % (2270681)Instructions burned: 387 (million) % 40.51/6.50 % (2270693)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1904911291:i=359:rtra=on:gtg=exists_top:ss=axioms_2957 on theBenchmark for (2957ds/359Mi) % 40.51/6.50 % (2270693)Refutation not found, incomplete strategy % 40.51/6.50 % (2270693)------------------------------ % 40.51/6.50 % (2270693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.51/6.50 % (2270693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.51/6.50 % (2270693)CaDiCaL version: 2.1.3 % 40.51/6.50 % (2270693)Termination reason: Refutation not found, incomplete strategy % 40.51/6.50 % (2270693)Time elapsed: 0.003 s % 40.51/6.50 % (2270693)Peak memory usage: 89 MB % 40.51/6.50 % (2270693)Instructions burned: 2 (million) % 40.51/6.50 % (2270685)Refutation not found, incomplete strategy % 40.51/6.50 % (2270685)------------------------------ % 40.51/6.50 % (2270685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.51/6.50 % (2270685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.51/6.50 % (2270685)CaDiCaL version: 2.1.3 % 40.51/6.50 % (2270685)Termination reason: Refutation not found, incomplete strategy % 40.51/6.50 % (2270685)Time elapsed: 0.075 s % 40.51/6.50 % (2270685)Peak memory usage: 133 MB % 40.51/6.50 % (2270685)Instructions burned: 12 (million) % 40.51/6.50 % (2270680)------------------------------ % 40.51/6.50 % (2270680)------------------------------ % 40.51/6.50 % (2270694)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2382947525:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2957 on theBenchmark for (2957ds/341Mi) % 40.51/6.50 % (2270694)Refutation not found, incomplete strategy % 40.51/6.50 % (2270694)------------------------------ % 40.51/6.50 % (2270694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.51/6.50 % (2270694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.51/6.50 % (2270694)CaDiCaL version: 2.1.3 % 40.51/6.50 % (2270694)Termination reason: Refutation not found, incomplete strategy % 40.51/6.50 % (2270694)Time elapsed: 0.024 s % 40.51/6.50 % (2270694)Peak memory usage: 113 MB % 40.51/6.50 % (2270694)Instructions burned: 6 (million) % 40.51/6.50 % (2270697)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2636182330:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2956 on theBenchmark for (2956ds/261Mi) % 40.51/6.50 % (2270698)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=3673557062:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2956 on theBenchmark for (2956ds/235Mi) % 40.51/6.50 % (2270697)Refutation not found, incomplete strategy % 40.51/6.50 % (2270697)------------------------------ % 40.51/6.50 % (2270697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.51/6.50 % (2270697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.51/6.50 % (2270697)CaDiCaL version: 2.1.3 % 40.51/6.50 % (2270697)Termination reason: Refutation not found, incomplete strategy % 40.51/6.50 % (2270697)Time elapsed: 0.048 s % 40.51/6.50 % (2270697)Peak memory usage: 116 MB % 40.51/6.50 % (2270697)Instructions burned: 12 (million) % 40.51/6.50 % (2270684)Instruction limit reached! % 40.51/6.50 % (2270684)------------------------------ % 40.51/6.50 % (2270684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.51/6.50 % (2270684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.51/6.50 % (2270684)CaDiCaL version: 2.1.3 % 40.51/6.50 % (2270684)Termination reason: Instruction limit % 40.51/6.50 % (2270684)Termination phase: Saturation % 42.50/7.16 % (2270684)Time elapsed: 0.544 s % 42.50/7.16 % (2270684)Peak memory usage: 92 MB % 42.50/7.16 % (2270684)Instructions burned: 514 (million) % 42.50/7.16 % (2270694)------------------------------ % 42.50/7.16 % (2270694)------------------------------ % 42.50/7.16 % (2270693)------------------------------ % 42.50/7.16 % (2270693)------------------------------ % 42.50/7.16 % (2270702)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=841000541:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi) % 42.50/7.16 % (2270685)------------------------------ % 42.50/7.16 % (2270685)------------------------------ % 42.50/7.16 % (2270698)Instruction limit reached! % 42.50/7.16 % (2270698)------------------------------ % 42.50/7.16 % (2270698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.50/7.16 % (2270698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.50/7.16 % (2270698)CaDiCaL version: 2.1.3 % 42.50/7.16 % (2270698)Termination reason: Instruction limit % 42.50/7.16 % (2270698)Termination phase: Saturation % 42.50/7.16 % (2270698)Time elapsed: 0.235 s % 42.50/7.16 % (2270698)Peak memory usage: 117 MB % 42.50/7.16 % (2270698)Instructions burned: 235 (million) % 42.50/7.16 % (2270705)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3285368817:i=146:doe=on:rtra=on_2952 on theBenchmark for (2952ds/146Mi) % 42.50/7.16 % (2270706)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=389761566:i=4428:doe=on:fsr=off:rtra=on_2952 on theBenchmark for (2952ds/4428Mi) % 42.50/7.16 % (2270705)Instruction limit reached! % 42.50/7.16 % (2270705)------------------------------ % 42.50/7.16 % (2270705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.50/7.16 % (2270705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.50/7.16 % (2270705)CaDiCaL version: 2.1.3 % 42.50/7.16 % (2270705)Termination reason: Instruction limit % 42.50/7.16 % (2270705)Termination phase: Saturation % 42.50/7.16 % (2270705)Time elapsed: 0.082 s % 42.50/7.16 % (2270705)Peak memory usage: 90 MB % 42.50/7.16 % (2270705)Instructions burned: 148 (million) % 42.50/7.16 % (2270709)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3885316094:i=1052:rtra=on_2951 on theBenchmark for (2951ds/1052Mi) % 42.50/7.16 % (2270707)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=3982918028:avsq=on:i=276:avsqr=1,2:rtra=on_2952 on theBenchmark for (2952ds/276Mi) % 42.50/7.16 % (2270697)------------------------------ % 42.50/7.16 % (2270697)------------------------------ % 42.50/7.16 % (2270702)Instruction limit reached! % 42.50/7.16 % (2270702)------------------------------ % 42.50/7.16 % (2270702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.50/7.16 % (2270702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.50/7.16 % (2270702)CaDiCaL version: 2.1.3 % 42.50/7.16 % (2270702)Termination reason: Instruction limit % 42.50/7.16 % (2270702)Termination phase: Saturation % 42.50/7.16 % (2270702)Time elapsed: 0.298 s % 42.50/7.16 % (2270702)Peak memory usage: 92 MB % 42.50/7.16 % (2270702)Instructions burned: 273 (million) % 42.50/7.16 % (2270710)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2654559524:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2951 on theBenchmark for (2951ds/655Mi) % 42.50/7.16 % (2270710)Refutation not found, incomplete strategy % 42.50/7.16 % (2270710)------------------------------ % 42.50/7.16 % (2270710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.50/7.16 % (2270710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.50/7.16 % (2270710)CaDiCaL version: 2.1.3 % 42.50/7.16 % (2270710)Termination reason: Refutation not found, incomplete strategy % 42.50/7.16 % (2270710)Time elapsed: 0.005 s % 42.50/7.16 % (2270710)Peak memory usage: 89 MB % 42.50/7.16 % (2270710)Instructions burned: 3 (million) % 42.50/7.16 % (2270713)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1448709287:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2949 on theBenchmark for (2949ds/1054Mi) % 42.50/7.16 % (2270713)Refutation not found, incomplete strategy % 42.50/7.16 % (2270713)------------------------------ % 42.50/7.16 % (2270713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.12/7.85 % (2270713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.12/7.85 % (2270713)CaDiCaL version: 2.1.3 % 48.12/7.85 % (2270713)Termination reason: Refutation not found, incomplete strategy % 48.12/7.85 % (2270713)Time elapsed: 0.002 s % 48.12/7.85 % (2270713)Peak memory usage: 89 MB % 48.12/7.85 % (2270713)Instructions burned: 2 (million) % 48.12/7.85 % (2270707)Instruction limit reached! % 48.12/7.85 % (2270707)------------------------------ % 48.12/7.85 % (2270707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.12/7.85 % (2270707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.12/7.85 % (2270707)CaDiCaL version: 2.1.3 % 48.12/7.85 % (2270707)Termination reason: Instruction limit % 48.12/7.85 % (2270707)Termination phase: Saturation % 48.12/7.85 % (2270707)Time elapsed: 0.248 s % 48.12/7.85 % (2270707)Peak memory usage: 133 MB % 48.12/7.85 % (2270707)Instructions burned: 277 (million) % 48.12/7.85 % (2270716)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1872946996:i=107:rtra=on_2949 on theBenchmark for (2949ds/107Mi) % 48.12/7.85 % (2270716)Refutation not found, incomplete strategy % 48.12/7.85 % (2270716)------------------------------ % 48.12/7.85 % (2270716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.12/7.85 % (2270716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.12/7.85 % (2270716)CaDiCaL version: 2.1.3 % 48.12/7.85 % (2270716)Termination reason: Refutation not found, incomplete strategy % 48.12/7.85 % (2270716)Time elapsed: 0.042 s % 48.12/7.85 % (2270716)Peak memory usage: 116 MB % 48.12/7.85 % (2270716)Instructions burned: 7 (million) % 48.12/7.85 % (2270717)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=286292627:s2a=on:i=450:doe=on:nm=32:rtra=on_2949 on theBenchmark for (2949ds/450Mi) % 48.12/7.85 % (2270717)Refutation not found, incomplete strategy % 48.12/7.85 % (2270717)------------------------------ % 48.12/7.85 % (2270717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.12/7.85 % (2270717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.12/7.85 % (2270717)CaDiCaL version: 2.1.3 % 48.12/7.85 % (2270717)Termination reason: Refutation not found, incomplete strategy % 48.12/7.85 % (2270717)Time elapsed: 0.076 s % 48.12/7.85 % (2270717)Peak memory usage: 132 MB % 48.12/7.85 % (2270717)Instructions burned: 12 (million) % 48.12/7.85 % (2270713)------------------------------ % 48.12/7.85 % (2270713)------------------------------ % 48.12/7.85 % (2270710)------------------------------ % 48.12/7.85 % (2270710)------------------------------ % 48.12/7.85 % (2270720)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 % 48.12/7.85 % (2270720)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1250703958:i=1090:aac=none:nm=0:rtra=on:rawr=on_2947 on theBenchmark for (2947ds/1090Mi) % 48.12/7.85 % (2270720)Refutation not found, incomplete strategy % 48.12/7.85 % (2270720)------------------------------ % 48.12/7.85 % (2270720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.12/7.85 % (2270720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.12/7.85 % (2270720)CaDiCaL version: 2.1.3 % 48.12/7.85 % (2270720)Termination reason: Refutation not found, incomplete strategy % 48.12/7.85 % (2270720)Time elapsed: 0.042 s % 48.12/7.85 % (2270720)Peak memory usage: 115 MB % 48.12/7.85 % (2270720)Instructions burned: 7 (million) % 48.12/7.85 % (2270733)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=797513740:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2945 on theBenchmark for (2945ds/130Mi) % 48.12/7.85 % (2270733)Refutation not found, incomplete strategy % 48.12/7.85 % (2270733)------------------------------ % 48.12/7.85 % (2270733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.12/7.85 % (2270733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.12/7.85 % (2270733)CaDiCaL version: 2.1.3 % 48.12/7.85 % (2270733)Termination reason: Refutation not found, incomplete strategy % 48.12/7.85 % (2270733)Time elapsed: 0.033 s % 48.12/7.85 % (2270733)Peak memory usage: 116 MB % 48.12/7.85 % (2270733)Instructions burned: 19 (million) % 48.12/7.85 % (2270716)------------------------------ % 48.12/7.85 % (2270716)------------------------------ % 48.12/7.85 % (2270709)Instruction limit reached! % 55.53/8.77 % (2270709)------------------------------ % 55.53/8.77 % (2270709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.53/8.77 % (2270709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.53/8.77 % (2270709)CaDiCaL version: 2.1.3 % 55.53/8.77 % (2270709)Termination reason: Instruction limit % 55.53/8.77 % (2270709)Termination phase: Saturation % 55.53/8.77 % (2270709)Time elapsed: 0.768 s % 55.53/8.77 % (2270709)Peak memory usage: 89 MB % 55.53/8.77 % (2270709)Instructions burned: 1053 (million) % 55.53/8.77 % (2270734)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1044326656:i=312:kws=inv_frequency:nm=20:rtra=on_2944 on theBenchmark for (2944ds/312Mi) % 55.53/8.77 % (2270717)------------------------------ % 55.53/8.77 % (2270717)------------------------------ % 55.53/8.77 % (2270733)------------------------------ % 55.53/8.77 % (2270733)------------------------------ % 55.53/8.77 % (2270737)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=386049919:i=491:doe=on:rtra=on:gtg=position_2942 on theBenchmark for (2942ds/491Mi) % 55.53/8.77 % (2270720)------------------------------ % 55.53/8.77 % (2270720)------------------------------ % 55.53/8.77 % (2270738)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3753099000:s2a=on:i=835:s2at=2:rtra=on_2941 on theBenchmark for (2941ds/835Mi) % 55.53/8.77 % (2270740)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2438140525:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2941 on theBenchmark for (2941ds/307Mi) % 55.53/8.77 % (2270741)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4141631502:i=776:doe=on:rtra=on_2940 on theBenchmark for (2940ds/776Mi) % 55.53/8.77 % (2270734)Instruction limit reached! % 55.53/8.77 % (2270734)------------------------------ % 55.53/8.77 % (2270734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.53/8.77 % (2270734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.53/8.77 % (2270734)CaDiCaL version: 2.1.3 % 55.53/8.77 % (2270734)Termination reason: Instruction limit % 55.53/8.77 % (2270734)Termination phase: Saturation % 55.53/8.77 % (2270734)Time elapsed: 0.356 s % 55.53/8.77 % (2270734)Peak memory usage: 118 MB % 55.53/8.77 % (2270734)Instructions burned: 312 (million) % 55.53/8.77 % (2270743)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=331300495:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 55.53/8.77 % (2270743)Refutation not found, incomplete strategy % 55.53/8.77 % (2270743)------------------------------ % 55.53/8.77 % (2270743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.53/8.77 % (2270743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.53/8.77 % (2270743)CaDiCaL version: 2.1.3 % 55.53/8.77 % (2270743)Termination reason: Refutation not found, incomplete strategy % 55.53/8.77 % (2270743)Time elapsed: 0.076 s % 55.53/8.77 % (2270743)Peak memory usage: 133 MB % 55.53/8.77 % (2270743)Instructions burned: 13 (million) % 55.53/8.77 % (2270740)Instruction limit reached! % 55.53/8.77 % (2270740)------------------------------ % 55.53/8.77 % (2270740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.53/8.77 % (2270740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.53/8.77 % (2270740)CaDiCaL version: 2.1.3 % 55.53/8.77 % (2270740)Termination reason: Instruction limit % 55.53/8.77 % (2270740)Termination phase: Saturation % 55.53/8.77 % (2270740)Time elapsed: 0.278 s % 55.53/8.77 % (2270740)Peak memory usage: 92 MB % 55.53/8.77 % (2270740)Instructions burned: 307 (million) % 55.53/8.77 % (2270737)Instruction limit reached! % 55.53/8.77 % (2270737)------------------------------ % 55.53/8.77 % (2270737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.53/8.77 % (2270737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.53/8.77 % (2270737)CaDiCaL version: 2.1.3 % 55.53/8.77 % (2270737)Termination reason: Instruction limit % 55.53/8.77 % (2270737)Termination phase: Saturation % 55.53/8.77 % (2270737)Time elapsed: 0.436 s % 55.53/8.77 % (2270737)Peak memory usage: 90 MB % 55.53/8.77 % (2270737)Instructions burned: 491 (million) % 55.53/8.77 % (2270747)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=893214862:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2938 on theBenchmark for (2938ds/784Mi) % 60.26/9.52 % (2270741)Instruction limit reached! % 60.26/9.52 % (2270741)------------------------------ % 60.26/9.52 % (2270741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.26/9.52 % (2270741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.26/9.52 % (2270741)CaDiCaL version: 2.1.3 % 60.26/9.52 % (2270741)Termination reason: Instruction limit % 60.26/9.52 % (2270741)Termination phase: Saturation % 60.26/9.52 % (2270741)Time elapsed: 0.361 s % 60.26/9.52 % (2270741)Peak memory usage: 119 MB % 60.26/9.52 % (2270741)Instructions burned: 778 (million) % 60.26/9.52 % (2270752)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=4130556901:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2935 on theBenchmark for (2935ds/246Mi) % 60.26/9.52 % (2270751)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=535362108:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2935 on theBenchmark for (2935ds/1131Mi) % 60.26/9.52 % (2270743)------------------------------ % 60.26/9.52 % (2270743)------------------------------ % 60.26/9.52 % (2270754)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2523463014:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/775Mi) % 60.26/9.52 % (2270752)Instruction limit reached! % 60.26/9.52 % (2270752)------------------------------ % 60.26/9.52 % (2270752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.26/9.52 % (2270752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.26/9.52 % (2270752)CaDiCaL version: 2.1.3 % 60.26/9.52 % (2270752)Termination reason: Instruction limit % 60.26/9.52 % (2270752)Termination phase: Saturation % 60.26/9.52 % (2270752)Time elapsed: 0.228 s % 60.26/9.52 % (2270752)Peak memory usage: 116 MB % 60.26/9.52 % (2270752)Instructions burned: 247 (million) % 60.26/9.52 % (2270738)Instruction limit reached! % 60.26/9.52 % (2270738)------------------------------ % 60.26/9.52 % (2270738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.26/9.52 % (2270738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.26/9.52 % (2270738)CaDiCaL version: 2.1.3 % 60.26/9.52 % (2270738)Termination reason: Instruction limit % 60.26/9.52 % (2270738)Termination phase: Saturation % 60.26/9.52 % (2270738)Time elapsed: 0.789 s % 60.26/9.52 % (2270738)Peak memory usage: 93 MB % 60.26/9.52 % (2270738)Instructions burned: 835 (million) % 60.26/9.52 % (2270747)Instruction limit reached! % 60.26/9.52 % (2270747)------------------------------ % 60.26/9.52 % (2270747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.26/9.52 % (2270747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.26/9.52 % (2270747)CaDiCaL version: 2.1.3 % 60.26/9.52 % (2270747)Termination reason: Instruction limit % 60.26/9.52 % (2270747)Termination phase: Saturation % 60.26/9.52 % (2270747)Time elapsed: 0.493 s % 60.26/9.52 % (2270747)Peak memory usage: 121 MB % 60.26/9.52 % (2270747)Instructions burned: 784 (million) % 60.26/9.52 % (2270757)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2963432446:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2932 on theBenchmark for (2932ds/273Mi) % 60.26/9.52 % (2270760)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2395720800:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 60.26/9.52 % (2270759)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1906995101:i=102:nm=16:rtra=on_2931 on theBenchmark for (2931ds/102Mi) % 60.26/9.52 % (2270760)Refutation not found, incomplete strategy % 60.26/9.52 % (2270760)------------------------------ % 60.26/9.52 % (2270760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.26/9.52 % (2270760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.26/9.52 % (2270760)CaDiCaL version: 2.1.3 % 60.26/9.52 % (2270760)Termination reason: Refutation not found, incomplete strategy % 60.26/9.52 % (2270760)Time elapsed: 0.002 s % 60.26/9.52 % (2270760)Peak memory usage: 89 MB % 60.26/9.52 % (2270757)Instruction limit reached! % 60.26/9.52 % (2270757)------------------------------ % 60.26/9.52 % (2270757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.26/9.52 % (2270757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.23/10.79 % (2270757)CaDiCaL version: 2.1.3 % 70.23/10.79 % (2270757)Termination reason: Instruction limit % 70.23/10.79 % (2270757)Termination phase: Saturation % 70.23/10.79 % (2270757)Time elapsed: 0.201 s % 70.23/10.79 % (2270757)Peak memory usage: 91 MB % 70.23/10.79 % (2270757)Instructions burned: 273 (million) % 70.23/10.79 % (2270762)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3092657507:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 70.23/10.79 % (2270759)Instruction limit reached! % 70.23/10.79 % (2270759)------------------------------ % 70.23/10.79 % (2270759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.23/10.79 % (2270759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.23/10.79 % (2270759)CaDiCaL version: 2.1.3 % 70.23/10.79 % (2270759)Termination reason: Instruction limit % 70.23/10.79 % (2270759)Termination phase: Saturation % 70.23/10.79 % (2270759)Time elapsed: 0.074 s % 70.23/10.79 % (2270759)Peak memory usage: 88 MB % 70.23/10.79 % (2270759)Instructions burned: 103 (million) % 70.23/10.79 % (2270765)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=298312939:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2928 on theBenchmark for (2928ds/868Mi) % 70.23/10.79 % (2270765)Refutation not found, incomplete strategy % 70.23/10.79 % (2270765)------------------------------ % 70.23/10.79 % (2270765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.23/10.79 % (2270765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.23/10.79 % (2270765)CaDiCaL version: 2.1.3 % 70.23/10.79 % (2270765)Termination reason: Refutation not found, incomplete strategy % 70.23/10.79 % (2270765)Time elapsed: 0.043 s % 70.23/10.79 % (2270765)Peak memory usage: 116 MB % 70.23/10.79 % (2270765)Instructions burned: 22 (million) % 70.23/10.79 % (2270767)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=922648602:i=1846:canc=cautious:fsr=off:rtra=on_2927 on theBenchmark for (2927ds/1846Mi) % 70.23/10.79 % (2270760)------------------------------ % 70.23/10.79 % (2270760)------------------------------ % 70.23/10.79 % (2270754)Instruction limit reached! % 70.23/10.79 % (2270754)------------------------------ % 70.23/10.79 % (2270754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.23/10.79 % (2270754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.23/10.79 % (2270754)CaDiCaL version: 2.1.3 % 70.23/10.79 % (2270754)Termination reason: Instruction limit % 70.23/10.79 % (2270754)Termination phase: Saturation % 70.23/10.79 % (2270754)Time elapsed: 0.837 s % 70.23/10.79 % (2270754)Peak memory usage: 96 MB % 70.23/10.79 % (2270754)Instructions burned: 776 (million) % 70.23/10.79 % (2270765)------------------------------ % 70.23/10.79 % (2270765)------------------------------ % 70.23/10.79 % (2270770)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3084677636:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2924 on theBenchmark for (2924ds/36816Mi) % 70.23/10.79 % (2270770)Refutation not found, incomplete strategy % 70.23/10.79 % (2270770)------------------------------ % 70.23/10.79 % (2270770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.23/10.79 % (2270770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.23/10.79 % (2270770)CaDiCaL version: 2.1.3 % 70.23/10.79 % (2270770)Termination reason: Refutation not found, incomplete strategy % 70.23/10.79 % (2270770)Time elapsed: 0.002 s % 70.23/10.79 % (2270770)Peak memory usage: 88 MB % 70.23/10.79 % (2270751)Instruction limit reached! % 70.23/10.79 % (2270751)------------------------------ % 70.23/10.79 % (2270751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.23/10.79 % (2270751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.23/10.79 % (2270751)CaDiCaL version: 2.1.3 % 70.23/10.79 % (2270751)Termination reason: Instruction limit % 70.23/10.79 % (2270751)Termination phase: Saturation % 70.23/10.79 % (2270751)Time elapsed: 1.199 s % 70.23/10.79 % (2270751)Peak memory usage: 125 MB % 70.23/10.79 % (2270751)Instructions burned: 1131 (million) % 70.23/10.79 % (2270771)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3535973504:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2923 on theBenchmark for (2923ds/273Mi) % 70.23/10.79 % (2270772)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=603956997:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2922 on theBenchmark for (2922ds/863Mi) % 79.52/12.12 % (2270772)Refutation not found, incomplete strategy % 79.52/12.12 % (2270772)------------------------------ % 79.52/12.12 % (2270772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.52/12.12 % (2270772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.52/12.12 % (2270772)CaDiCaL version: 2.1.3 % 79.52/12.12 % (2270772)Termination reason: Refutation not found, incomplete strategy % 79.52/12.12 % (2270772)Time elapsed: 0.064 s % 79.52/12.12 % (2270772)Peak memory usage: 116 MB % 79.52/12.12 % (2270772)Instructions burned: 26 (million) % 79.52/12.12 % (2270775)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1485658674:i=5811:kws=precedence:nm=0:rtra=on_2921 on theBenchmark for (2921ds/5811Mi) % 79.52/12.12 % (2270771)Instruction limit reached! % 79.52/12.12 % (2270771)------------------------------ % 79.52/12.12 % (2270771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.52/12.12 % (2270771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.52/12.12 % (2270771)CaDiCaL version: 2.1.3 % 79.52/12.12 % (2270771)Termination reason: Instruction limit % 79.52/12.12 % (2270771)Termination phase: Saturation % 79.52/12.12 % (2270771)Time elapsed: 0.298 s % 79.52/12.12 % (2270771)Peak memory usage: 92 MB % 79.52/12.12 % (2270771)Instructions burned: 273 (million) % 79.52/12.12 % (2270770)------------------------------ % 79.52/12.12 % (2270770)------------------------------ % 79.52/12.12 % (2270775)Refutation not found, incomplete strategy % 79.52/12.12 % (2270775)------------------------------ % 79.52/12.12 % (2270775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.52/12.12 % (2270775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.52/12.12 % (2270775)CaDiCaL version: 2.1.3 % 79.52/12.12 % (2270775)Termination reason: Refutation not found, incomplete strategy % 79.52/12.12 % (2270775)Time elapsed: 0.068 s % 79.52/12.12 % (2270775)Peak memory usage: 116 MB % 79.52/12.12 % (2270775)Instructions burned: 30 (million) % 79.52/12.12 % (2270778)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=3549528750:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2918 on theBenchmark for (2918ds/2216Mi) % 79.52/12.12 % (2270779)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3228740592:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2917 on theBenchmark for (2917ds/801Mi) % 79.52/12.12 % (2270779)Refutation not found, incomplete strategy % 79.52/12.12 % (2270779)------------------------------ % 79.52/12.12 % (2270779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.52/12.12 % (2270779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.52/12.12 % (2270779)CaDiCaL version: 2.1.3 % 79.52/12.12 % (2270779)Termination reason: Refutation not found, incomplete strategy % 79.52/12.12 % (2270779)Time elapsed: 0.006 s % 79.52/12.12 % (2270779)Peak memory usage: 89 MB % 79.52/12.12 % (2270779)Instructions burned: 3 (million) % 79.52/12.12 % (2270772)------------------------------ % 79.52/12.12 % (2270772)------------------------------ % 79.52/12.12 % (2270775)------------------------------ % 79.52/12.12 % (2270775)------------------------------ % 79.52/12.12 % (2270767)Instruction limit reached! % 79.52/12.12 % (2270767)------------------------------ % 79.52/12.12 % (2270767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.52/12.12 % (2270767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.52/12.12 % (2270767)CaDiCaL version: 2.1.3 % 79.52/12.12 % (2270767)Termination reason: Instruction limit % 79.52/12.12 % (2270767)Termination phase: Saturation % 79.52/12.12 % (2270767)Time elapsed: 1.283 s % 79.52/12.12 % (2270767)Peak memory usage: 99 MB % 79.52/12.12 % (2270767)Instructions burned: 1846 (million) % 79.52/12.12 % (2270784)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3726269550:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2914 on theBenchmark for (2914ds/1026Mi) % 79.52/12.12 % (2270784)Refutation not found, incomplete strategy % 79.52/12.12 % (2270784)------------------------------ % 79.52/12.12 % (2270784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.52/12.12 % (2270784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/15.68 % (2270784)CaDiCaL version: 2.1.3 % 105.16/15.68 % (2270784)Termination reason: Refutation not found, incomplete strategy % 105.16/15.68 % (2270784)Time elapsed: 0.004 s % 105.16/15.68 % (2270784)Peak memory usage: 89 MB % 105.16/15.68 % (2270784)Instructions burned: 2 (million) % 105.16/15.68 % (2270779)------------------------------ % 105.16/15.68 % (2270779)------------------------------ % 105.16/15.68 % (2270785)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1622734784:i=3509:rtra=on_2913 on theBenchmark for (2913ds/3509Mi) % 105.16/15.68 % (2270706)Instruction limit reached! % 105.16/15.68 % (2270706)------------------------------ % 105.16/15.68 % (2270706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/15.68 % (2270706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/15.68 % (2270706)CaDiCaL version: 2.1.3 % 105.16/15.68 % (2270706)Termination reason: Instruction limit % 105.16/15.68 % (2270706)Termination phase: Saturation % 105.16/15.68 % (2270706)Time elapsed: 3.917 s % 105.16/15.68 % (2270706)Peak memory usage: 105 MB % 105.16/15.68 % (2270706)Instructions burned: 4429 (million) % 105.16/15.68 % (2270786)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2298538058:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/2127Mi) % 105.16/15.68 % (2270789)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3420948277:i=1959:rtra=on:fsd=on:proc=on_2910 on theBenchmark for (2910ds/1959Mi) % 105.16/15.68 % (2270784)------------------------------ % 105.16/15.68 % (2270784)------------------------------ % 105.16/15.68 % (2270790)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1775547032:s2a=on:i=3553:nm=0:rtra=on_2910 on theBenchmark for (2910ds/3553Mi) % 105.16/15.68 % (2270789)Refutation not found, incomplete strategy % 105.16/15.68 % (2270789)------------------------------ % 105.16/15.68 % (2270789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/15.68 % (2270789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/15.68 % (2270789)CaDiCaL version: 2.1.3 % 105.16/15.68 % (2270789)Termination reason: Refutation not found, incomplete strategy % 105.16/15.68 % (2270789)Time elapsed: 0.042 s % 105.16/15.68 % (2270789)Peak memory usage: 116 MB % 105.16/15.68 % (2270789)Instructions burned: 7 (million) % 105.16/15.68 % (2270794)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3313269202:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2907 on theBenchmark for (2907ds/3201Mi) % 105.16/15.68 % (2270794)Refutation not found, incomplete strategy % 105.16/15.68 % (2270794)------------------------------ % 105.16/15.68 % (2270794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/15.68 % (2270794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/15.68 % (2270794)CaDiCaL version: 2.1.3 % 105.16/15.68 % (2270794)Termination reason: Refutation not found, incomplete strategy % 105.16/15.68 % (2270794)Time elapsed: 0.007 s % 105.16/15.68 % (2270794)Peak memory usage: 90 MB % 105.16/15.68 % (2270794)Instructions burned: 3 (million) % 105.16/15.68 % (2270789)------------------------------ % 105.16/15.68 % (2270789)------------------------------ % 105.16/15.68 % (2270794)------------------------------ % 105.16/15.68 % (2270794)------------------------------ % 105.16/15.68 % (2270796)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=682582891:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2903 on theBenchmark for (2903ds/4093Mi) % 105.16/15.68 % (2270786)Instruction limit reached! % 105.16/15.68 % (2270786)------------------------------ % 105.16/15.68 % (2270786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/15.68 % (2270786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/15.68 % (2270786)CaDiCaL version: 2.1.3 % 105.16/15.68 % (2270786)Termination reason: Instruction limit % 105.16/15.68 % (2270786)Termination phase: Saturation % 105.16/15.68 % (2270786)Time elapsed: 0.944 s % 105.16/15.68 % (2270786)Peak memory usage: 101 MB % 105.16/15.68 % (2270786)Instructions burned: 2128 (million) % 105.16/15.68 % (2270799)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=2794698118:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2901 on theBenchmark for (2901ds/21173Mi) % 105.16/15.68 % (2270799)Refutation not found, incomplete strategy % 105.16/15.68 % (2270799)------------------------------ % 132.19/19.45 % (2270799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.19/19.45 % (2270799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.19/19.45 % (2270799)CaDiCaL version: 2.1.3 % 132.19/19.45 % (2270799)Termination reason: Refutation not found, incomplete strategy % 132.19/19.45 % (2270799)Time elapsed: 0.031 s % 132.19/19.45 % (2270799)Peak memory usage: 114 MB % 132.19/19.45 % (2270799)Instructions burned: 7 (million) % 132.19/19.45 % (2270801)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3252394009:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2900 on theBenchmark for (2900ds/10544Mi) % 132.19/19.45 % (2270778)Instruction limit reached! % 132.19/19.45 % (2270778)------------------------------ % 132.19/19.45 % (2270778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.19/19.45 % (2270778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.19/19.45 % (2270778)CaDiCaL version: 2.1.3 % 132.19/19.45 % (2270778)Termination reason: Instruction limit % 132.19/19.45 % (2270778)Termination phase: Saturation % 132.19/19.45 % (2270778)Time elapsed: 1.870 s % 132.19/19.45 % (2270778)Peak memory usage: 127 MB % 132.19/19.45 % (2270778)Instructions burned: 2217 (million) % 132.19/19.45 % (2270799)------------------------------ % 132.19/19.45 % (2270799)------------------------------ % 132.19/19.45 % (2270804)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1234189904:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2896 on theBenchmark for (2896ds/1262Mi) % 132.19/19.45 % (2270804)Refutation not found, incomplete strategy % 132.19/19.45 % (2270804)------------------------------ % 132.19/19.45 % (2270804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.19/19.45 % (2270804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.19/19.45 % (2270804)CaDiCaL version: 2.1.3 % 132.19/19.45 % (2270804)Termination reason: Refutation not found, incomplete strategy % 132.19/19.45 % (2270804)Time elapsed: 0.026 s % 132.19/19.45 % (2270804)Peak memory usage: 116 MB % 132.19/19.45 % (2270804)Instructions burned: 7 (million) % 132.19/19.45 % (2270805)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1390354715:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2896 on theBenchmark for (2896ds/775Mi) % 132.19/19.45 % (2270804)------------------------------ % 132.19/19.45 % (2270804)------------------------------ % 132.19/19.45 % (2270808)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3547244140:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2891 on theBenchmark for (2891ds/270Mi) % 132.19/19.45 % (2270762)Instruction limit reached! % 132.19/19.45 % (2270762)------------------------------ % 132.19/19.45 % (2270762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.19/19.45 % (2270762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.19/19.45 % (2270762)CaDiCaL version: 2.1.3 % 132.19/19.45 % (2270762)Termination reason: Instruction limit % 132.19/19.45 % (2270762)Termination phase: Saturation % 132.19/19.45 % (2270762)Time elapsed: 3.861 s % 132.19/19.45 % (2270762)Peak memory usage: 111 MB % 132.19/19.45 % (2270762)Instructions burned: 6401 (million) % 132.19/19.45 % (2270808)Instruction limit reached! % 132.19/19.45 % (2270808)------------------------------ % 132.19/19.45 % (2270808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.19/19.45 % (2270808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.19/19.45 % (2270808)CaDiCaL version: 2.1.3 % 132.19/19.45 % (2270808)Termination reason: Instruction limit % 132.19/19.45 % (2270808)Termination phase: Saturation % 132.19/19.45 % (2270808)Time elapsed: 0.156 s % 132.19/19.45 % (2270808)Peak memory usage: 91 MB % 132.19/19.45 % (2270808)Instructions burned: 271 (million) % 132.19/19.45 % (2270810)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2748757385:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2889 on theBenchmark for (2889ds/17165Mi) % 132.19/19.45 % (2270811)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3989326222:s2a=on:i=13094:s2at=-1:rtra=on_2888 on theBenchmark for (2888ds/13094Mi) % 132.19/19.45 % (2270805)Instruction limit reached! % 132.19/19.45 % (2270805)------------------------------ % 132.19/19.45 % (2270805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.19/19.45 % (2270805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.61/21.78 % (2270805)CaDiCaL version: 2.1.3 % 148.61/21.78 % (2270805)Termination reason: Instruction limit % 148.61/21.78 % (2270805)Termination phase: Saturation % 148.61/21.78 % (2270805)Time elapsed: 0.804 s % 148.61/21.78 % (2270805)Peak memory usage: 96 MB % 148.61/21.78 % (2270805)Instructions burned: 775 (million) % 148.61/21.78 % (2270814)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3711799725:st=2:i=12633:rtra=on:ss=axioms_2885 on theBenchmark for (2885ds/12633Mi) % 148.61/21.78 % (2270785)Instruction limit reached! % 148.61/21.78 % (2270785)------------------------------ % 148.61/21.78 % (2270785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.61/21.78 % (2270785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.61/21.78 % (2270785)CaDiCaL version: 2.1.3 % 148.61/21.78 % (2270785)Termination reason: Instruction limit % 148.61/21.78 % (2270785)Termination phase: Saturation % 148.61/21.78 % (2270785)Time elapsed: 3.698 s % 148.61/21.78 % (2270785)Peak memory usage: 107 MB % 148.61/21.78 % (2270785)Instructions burned: 3509 (million) % 148.61/21.78 % (2270816)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3396597832:i=1783:rtra=on:gtg=position_2873 on theBenchmark for (2873ds/1783Mi) % 148.61/21.78 % (2270790)Instruction limit reached! % 148.61/21.78 % (2270790)------------------------------ % 148.61/21.78 % (2270790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.61/21.78 % (2270790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.61/21.78 % (2270790)CaDiCaL version: 2.1.3 % 148.61/21.78 % (2270790)Termination reason: Instruction limit % 148.61/21.78 % (2270790)Termination phase: Saturation % 148.61/21.78 % (2270790)Time elapsed: 4.053 s % 148.61/21.78 % (2270790)Peak memory usage: 104 MB % 148.61/21.78 % (2270790)Instructions burned: 3553 (million) % 148.61/21.78 % (2270818)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=368509899:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2867 on theBenchmark for (2867ds/5451Mi) % 148.61/21.78 % (2270796)Instruction limit reached! % 148.61/21.78 % (2270796)------------------------------ % 148.61/21.78 % (2270796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.61/21.78 % (2270796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.61/21.78 % (2270796)CaDiCaL version: 2.1.3 % 148.61/21.78 % (2270796)Termination reason: Instruction limit % 148.61/21.78 % (2270796)Termination phase: Saturation % 148.61/21.78 % (2270796)Time elapsed: 4.153 s % 148.61/21.78 % (2270796)Peak memory usage: 154 MB % 148.61/21.78 % (2270796)Instructions burned: 4093 (million) % 148.61/21.78 % (2270820)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=675837774:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2858 on theBenchmark for (2858ds/4975Mi) % 148.61/21.78 % (2270820)Refutation not found, incomplete strategy % 148.61/21.78 % (2270820)------------------------------ % 148.61/21.78 % (2270820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.61/21.78 % (2270820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.61/21.78 % (2270820)CaDiCaL version: 2.1.3 % 148.61/21.78 % (2270820)Termination reason: Refutation not found, incomplete strategy % 148.61/21.78 % (2270820)Time elapsed: 0.042 s % 148.61/21.78 % (2270820)Peak memory usage: 116 MB % 148.61/21.78 % (2270820)Instructions burned: 24 (million) % 148.61/21.78 % (2270816)Instruction limit reached! % 148.61/21.78 % (2270816)------------------------------ % 148.61/21.78 % (2270816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.61/21.78 % (2270816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.61/21.78 % (2270816)CaDiCaL version: 2.1.3 % 148.61/21.78 % (2270816)Termination reason: Instruction limit % 148.61/21.78 % (2270816)Termination phase: Saturation % 148.61/21.78 % (2270816)Time elapsed: 1.798 s % 148.61/21.78 % (2270816)Peak memory usage: 121 MB % 148.61/21.78 % (2270816)Instructions burned: 1783 (million) % 148.61/21.78 % (2270820)------------------------------ % 148.61/21.78 % (2270820)------------------------------ % 148.61/21.78 % (2270826)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=1884118333:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2853 on theBenchmark for (2853ds/2076Mi) % 148.61/21.78 % (2270827)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2647714274:i=5145:rtra=on_2852 on theBenchmark for (2852ds/5145Mi) % 171.70/25.07 % (2270811)Instruction limit reached! % 171.70/25.07 % (2270811)------------------------------ % 171.70/25.07 % (2270811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.70/25.07 % (2270811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.70/25.07 % (2270811)CaDiCaL version: 2.1.3 % 171.70/25.07 % (2270811)Termination reason: Instruction limit % 171.70/25.07 % (2270811)Termination phase: Saturation % 171.70/25.07 % (2270811)Time elapsed: 4.396 s % 171.70/25.07 % (2270811)Peak memory usage: 91 MB % 171.70/25.07 % (2270811)Instructions burned: 13095 (million) % 171.70/25.07 % (2270830)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2874239813:i=3509:rtra=on_2842 on theBenchmark for (2842ds/3509Mi) % 171.70/25.07 % (2270826)Instruction limit reached! % 171.70/25.07 % (2270826)------------------------------ % 171.70/25.07 % (2270826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.70/25.07 % (2270826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.70/25.07 % (2270826)CaDiCaL version: 2.1.3 % 171.70/25.07 % (2270826)Termination reason: Instruction limit % 171.70/25.07 % (2270826)Termination phase: Saturation % 171.70/25.07 % (2270826)Time elapsed: 1.883 s % 171.70/25.07 % (2270826)Peak memory usage: 125 MB % 171.70/25.07 % (2270826)Instructions burned: 2076 (million) % 171.70/25.07 % (2270834)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2244215111:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2831 on theBenchmark for (2831ds/13800Mi) % 171.70/25.07 % (2270830)Instruction limit reached! % 171.70/25.07 % (2270830)------------------------------ % 171.70/25.07 % (2270830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.70/25.07 % (2270830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.70/25.07 % (2270830)CaDiCaL version: 2.1.3 % 171.70/25.07 % (2270830)Termination reason: Instruction limit % 171.70/25.07 % (2270830)Termination phase: Saturation % 171.70/25.07 % (2270830)Time elapsed: 2.092 s % 171.70/25.07 % (2270830)Peak memory usage: 106 MB % 171.70/25.07 % (2270830)Instructions burned: 3511 (million) % 171.70/25.07 % (2270836)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3372978419:i=1412:rtra=on:fsd=on:proc=on_2818 on theBenchmark for (2818ds/1412Mi) % 171.70/25.07 % (2270836)Refutation not found, incomplete strategy % 171.70/25.07 % (2270836)------------------------------ % 171.70/25.07 % (2270836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.70/25.07 % (2270836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.70/25.07 % (2270836)CaDiCaL version: 2.1.3 % 171.70/25.07 % (2270836)Termination reason: Refutation not found, incomplete strategy % 171.70/25.07 % (2270836)Time elapsed: 0.031 s % 171.70/25.07 % (2270836)Peak memory usage: 116 MB % 171.70/25.07 % (2270836)Instructions burned: 7 (million) % 171.70/25.07 % (2270827)Instruction limit reached! % 171.70/25.07 % (2270827)------------------------------ % 171.70/25.07 % (2270827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.70/25.07 % (2270827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.70/25.07 % (2270827)CaDiCaL version: 2.1.3 % 171.70/25.07 % (2270827)Termination reason: Instruction limit % 171.70/25.07 % (2270827)Termination phase: Saturation % 171.70/25.07 % (2270827)Time elapsed: 3.489 s % 171.70/25.07 % (2270827)Peak memory usage: 90 MB % 171.70/25.07 % (2270827)Instructions burned: 5146 (million) % 171.70/25.07 % (2270836)------------------------------ % 171.70/25.07 % (2270836)------------------------------ % 171.70/25.07 % (2270838)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 % 171.70/25.07 % (2270838)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2822411046:i=11747:aac=none:nm=0:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/11747Mi) % 171.70/25.07 % (2270818)Instruction limit reached! % 171.70/25.07 % (2270818)------------------------------ % 171.70/25.07 % (2270818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.70/25.07 % (2270818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.70/25.07 % (2270818)CaDiCaL version: 2.1.3 % 171.70/25.07 % (2270818)Termination reason: Instruction limit % 171.70/25.07 % (2270818)Termination phase: Saturation % 196.91/28.54 % (2270818)Time elapsed: 5.179 s % 196.91/28.54 % (2270818)Peak memory usage: 133 MB % 196.91/28.54 % (2270818)Instructions burned: 5451 (million) % 196.91/28.54 % (2270838)Refutation not found, incomplete strategy % 196.91/28.54 % (2270838)------------------------------ % 196.91/28.54 % (2270838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.91/28.54 % (2270838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.91/28.54 % (2270838)CaDiCaL version: 2.1.3 % 196.91/28.54 % (2270838)Termination reason: Refutation not found, incomplete strategy % 196.91/28.54 % (2270838)Time elapsed: 0.042 s % 196.91/28.54 % (2270838)Peak memory usage: 115 MB % 196.91/28.54 % (2270838)Instructions burned: 7 (million) % 196.91/28.54 % (2270839)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1831786868:s2a=on:i=3553:nm=0:rtra=on_2813 on theBenchmark for (2813ds/3553Mi) % 196.91/28.54 % (2270841)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2196728769:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/3201Mi) % 196.91/28.54 % (2270841)Refutation not found, incomplete strategy % 196.91/28.54 % (2270841)------------------------------ % 196.91/28.54 % (2270841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.91/28.54 % (2270841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.91/28.54 % (2270841)CaDiCaL version: 2.1.3 % 196.91/28.54 % (2270841)Termination reason: Refutation not found, incomplete strategy % 196.91/28.54 % (2270841)Time elapsed: 0.006 s % 196.91/28.54 % (2270841)Peak memory usage: 90 MB % 196.91/28.54 % (2270841)Instructions burned: 3 (million) % 196.91/28.54 % (2270838)------------------------------ % 196.91/28.54 % (2270838)------------------------------ % 196.91/28.54 % (2270844)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=4115168930:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2808 on theBenchmark for (2808ds/4081Mi) % 196.91/28.54 % (2270841)------------------------------ % 196.91/28.54 % (2270841)------------------------------ % 196.91/28.54 % (2270846)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=3647171609:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2805 on theBenchmark for (2805ds/20260Mi) % 196.91/28.54 % (2270846)Refutation not found, incomplete strategy % 196.91/28.54 % (2270846)------------------------------ % 196.91/28.54 % (2270846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.91/28.54 % (2270846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.91/28.54 % (2270846)CaDiCaL version: 2.1.3 % 196.91/28.54 % (2270846)Termination reason: Refutation not found, incomplete strategy % 196.91/28.54 % (2270846)Time elapsed: 0.041 s % 196.91/28.54 % (2270846)Peak memory usage: 115 MB % 196.91/28.54 % (2270846)Instructions burned: 7 (million) % 196.91/28.54 % (2270846)------------------------------ % 196.91/28.54 % (2270846)------------------------------ % 196.91/28.54 % (2270848)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2126540115:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2798 on theBenchmark for (2798ds/58627Mi) % 196.91/28.54 % (2270848)Refutation not found, incomplete strategy % 196.91/28.54 % (2270848)------------------------------ % 196.91/28.54 % (2270848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.91/28.54 % (2270848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.91/28.54 % (2270848)CaDiCaL version: 2.1.3 % 196.91/28.54 % (2270848)Termination reason: Refutation not found, incomplete strategy % 196.91/28.54 % (2270848)Time elapsed: 0.002 s % 196.91/28.54 % (2270848)Peak memory usage: 88 MB % 196.91/28.54 % (2270848)------------------------------ % 196.91/28.54 % (2270848)------------------------------ % 196.91/28.54 % (2270839)Instruction limit reached! % 196.91/28.54 % (2270839)------------------------------ % 196.91/28.54 % (2270839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.91/28.54 % (2270839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.91/28.54 % (2270839)CaDiCaL version: 2.1.3 % 196.91/28.54 % (2270839)Termination reason: Instruction limit % 196.91/28.54 % (2270839)Termination phase: Saturation % 196.91/28.54 % (2270839)Time elapsed: 2.204 s % 196.91/28.54 % (2270839)Peak memory usage: 104 MB % 196.91/28.54 % (2270839)Instructions burned: 3555 (million) % 196.91/28.54 % (2270850)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1600035853:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/6258Mi) % 202.03/29.35 % (2270850)Refutation not found, incomplete strategy % 202.03/29.35 % (2270850)------------------------------ % 202.03/29.35 % (2270850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.03/29.35 % (2270850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.03/29.35 % (2270850)CaDiCaL version: 2.1.3 % 202.03/29.35 % (2270850)Termination reason: Refutation not found, incomplete strategy % 202.03/29.35 % (2270850)Time elapsed: 0.038 s % 202.03/29.35 % (2270850)Peak memory usage: 116 MB % 202.03/29.35 % (2270850)Instructions burned: 7 (million) % 202.03/29.35 % (2270851)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2143782193:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2789 on theBenchmark for (2789ds/34001Mi) % 202.03/29.35 % (2270850)------------------------------ % 202.03/29.35 % (2270850)------------------------------ % 202.03/29.35 % (2270801)Instruction limit reached! % 202.03/29.35 % (2270801)------------------------------ % 202.03/29.35 % (2270801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.03/29.35 % (2270801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.03/29.35 % (2270801)CaDiCaL version: 2.1.3 % 202.03/29.35 % (2270801)Termination reason: Instruction limit % 202.03/29.35 % (2270801)Termination phase: Saturation % 202.03/29.35 % (2270801)Time elapsed: 11.253 s % 202.03/29.35 % (2270801)Peak memory usage: 194 MB % 202.03/29.35 % (2270801)Instructions burned: 10545 (million) % 202.03/29.35 % (2270855)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3055156306:i=24001:kws=precedence:nm=0:rtra=on_2784 on theBenchmark for (2784ds/24001Mi) % 202.03/29.35 % (2270854)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2885678870:s2a=on:i=71622:s2at=-1:rtra=on_2784 on theBenchmark for (2784ds/71622Mi) % 202.03/29.35 % (2270855)Refutation not found, incomplete strategy % 202.03/29.35 % (2270855)------------------------------ % 202.03/29.35 % (2270855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.03/29.35 % (2270855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.03/29.35 % (2270855)CaDiCaL version: 2.1.3 % 202.03/29.35 % (2270855)Termination reason: Refutation not found, incomplete strategy % 202.03/29.35 % (2270855)Time elapsed: 0.064 s % 202.03/29.35 % (2270855)Peak memory usage: 115 MB % 202.03/29.35 % (2270855)Instructions burned: 27 (million) % 202.03/29.35 % (2270855)------------------------------ % 202.03/29.35 % (2270855)------------------------------ % 202.03/29.35 % (2270858)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=503919119:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2777 on theBenchmark for (2777ds/2076Mi) % 202.03/29.35 % (2270844)Instruction limit reached! % 202.03/29.35 % (2270844)------------------------------ % 202.03/29.35 % (2270844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.03/29.35 % (2270844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.03/29.35 % (2270844)CaDiCaL version: 2.1.3 % 202.03/29.35 % (2270844)Termination reason: Instruction limit % 202.03/29.35 % (2270844)Termination phase: Saturation % 202.03/29.35 % (2270844)Time elapsed: 4.416 s % 202.03/29.35 % (2270844)Peak memory usage: 159 MB % 202.03/29.35 % (2270844)Instructions burned: 4081 (million) % 202.03/29.35 % (2270860)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3973190680:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2761 on theBenchmark for (2761ds/83971Mi) % 202.03/29.35 % (2270860)Refutation not found, incomplete strategy % 202.03/29.35 % (2270860)------------------------------ % 202.03/29.35 % (2270860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.03/29.35 % (2270860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.03/29.35 % (2270860)CaDiCaL version: 2.1.3 % 202.03/29.35 % (2270860)Termination reason: Refutation not found, incomplete strategy % 202.03/29.35 % (2270860)Time elapsed: 0.005 s % 202.03/29.35 % (2270860)Peak memory usage: 90 MB % 202.03/29.35 % (2270860)Instructions burned: 2 (million) % 202.03/29.35 % (2270858)Instruction limit reached! % 202.03/29.35 % (2270858)------------------------------ % 202.03/29.35 % (2270858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.87/30.52 % (2270858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.87/30.52 % (2270858)CaDiCaL version: 2.1.3 % 209.87/30.52 % (2270858)Termination reason: Instruction limit % 209.87/30.52 % (2270858)Termination phase: Saturation % 209.87/30.52 % (2270858)Time elapsed: 1.814 s % 209.87/30.52 % (2270858)Peak memory usage: 129 MB % 209.87/30.52 % (2270858)Instructions burned: 2077 (million) % 209.87/30.52 % (2270860)------------------------------ % 209.87/30.52 % (2270860)------------------------------ % 209.87/30.52 % (2270862)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2422850390:i=83944:rtra=on_2756 on theBenchmark for (2756ds/83944Mi) % 209.87/30.52 % (2270862)Refutation not found, incomplete strategy % 209.87/30.52 % (2270862)------------------------------ % 209.87/30.52 % (2270862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.87/30.52 % (2270862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.87/30.52 % (2270862)CaDiCaL version: 2.1.3 % 209.87/30.52 % (2270862)Termination reason: Refutation not found, incomplete strategy % 209.87/30.52 % (2270862)Time elapsed: 0.044 s % 209.87/30.52 % (2270862)Peak memory usage: 116 MB % 209.87/30.52 % (2270862)Instructions burned: 8 (million) % 209.87/30.52 % (2270814)Instruction limit reached! % 209.87/30.52 % (2270814)------------------------------ % 209.87/30.52 % (2270814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.87/30.52 % (2270814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.87/30.52 % (2270814)CaDiCaL version: 2.1.3 % 209.87/30.52 % (2270814)Termination reason: Instruction limit % 209.87/30.52 % (2270814)Termination phase: Saturation % 209.87/30.52 % (2270814)Time elapsed: 13.035 s % 209.87/30.52 % (2270814)Peak memory usage: 137 MB % 209.87/30.52 % (2270814)Instructions burned: 12634 (million) % 209.87/30.52 % (2270863)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2051416233:i=9201:rtra=on_2754 on theBenchmark for (2754ds/9201Mi) % 209.87/30.52 % (2270865)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 209.87/30.52 % (2270865)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=913683128:i=6806:aac=none:nm=0:rtra=on:rawr=on_2752 on theBenchmark for (2752ds/6806Mi) % 209.87/30.52 % (2270865)Refutation not found, incomplete strategy % 209.87/30.52 % (2270865)------------------------------ % 209.87/30.52 % (2270865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.87/30.52 % (2270865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.87/30.52 % (2270865)CaDiCaL version: 2.1.3 % 209.87/30.52 % (2270865)Termination reason: Refutation not found, incomplete strategy % 209.87/30.52 % (2270865)Time elapsed: 0.041 s % 209.87/30.52 % (2270865)Peak memory usage: 116 MB % 209.87/30.52 % (2270865)Instructions burned: 7 (million) % 209.87/30.52 % (2270862)------------------------------ % 209.87/30.52 % (2270862)------------------------------ % 209.87/30.52 % (2270868)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3788559363:s2a=on:i=3553:nm=0:rtra=on_2748 on theBenchmark for (2748ds/3553Mi) % 209.87/30.52 % (2270865)------------------------------ % 209.87/30.52 % (2270865)------------------------------ % 209.87/30.52 % (2270870)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=1201505681:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2744 on theBenchmark for (2744ds/2064Mi) % 209.87/30.52 % (2270834)Instruction limit reached! % 209.87/30.52 % (2270834)------------------------------ % 209.87/30.52 % (2270834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.87/30.52 % (2270834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.87/30.52 % (2270834)CaDiCaL version: 2.1.3 % 209.87/30.52 % (2270834)Termination reason: Instruction limit % 209.87/30.52 % (2270834)Termination phase: Saturation % 209.87/30.52 % (2270834)Time elapsed: 10.451 s % 209.87/30.52 % (2270834)Peak memory usage: 121 MB % 209.87/30.52 % (2270834)Instructions burned: 13801 (million) % 209.87/30.52 % (2270870)Instruction limit reached! % 209.87/30.52 % (2270870)------------------------------ % 209.87/30.52 % (2270870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.87/30.52 % (2270870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.77/31.56 % (2270870)CaDiCaL version: 2.1.3 % 217.77/31.56 % (2270870)Termination reason: Instruction limit % 217.77/31.56 % (2270870)Termination phase: Saturation % 217.77/31.56 % (2270870)Time elapsed: 2.096 s % 217.77/31.56 % (2270870)Peak memory usage: 143 MB % 217.77/31.56 % (2270870)Instructions burned: 2065 (million) % 217.77/31.56 % (2270878)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=3672058190:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2724 on theBenchmark for (2724ds/20260Mi) % 217.77/31.56 % (2270878)Refutation not found, incomplete strategy % 217.77/31.56 % (2270878)------------------------------ % 217.77/31.56 % (2270878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.77/31.56 % (2270878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.77/31.56 % (2270878)CaDiCaL version: 2.1.3 % 217.77/31.56 % (2270878)Termination reason: Refutation not found, incomplete strategy % 217.77/31.56 % (2270878)Time elapsed: 0.041 s % 217.77/31.56 % (2270878)Peak memory usage: 114 MB % 217.77/31.56 % (2270878)Instructions burned: 7 (million) % 217.77/31.56 % (2270810)Instruction limit reached! % 217.77/31.56 % (2270810)------------------------------ % 217.77/31.56 % (2270810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.77/31.56 % (2270810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.77/31.56 % (2270810)CaDiCaL version: 2.1.3 % 217.77/31.56 % (2270810)Termination reason: Instruction limit % 217.77/31.56 % (2270810)Termination phase: Saturation % 217.77/31.56 % (2270810)Time elapsed: 16.616 s % 217.77/31.56 % (2270810)Peak memory usage: 333 MB % 217.77/31.56 % (2270810)Instructions burned: 17165 (million) % 217.77/31.56 % (2270880)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=912260886:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2721 on theBenchmark for (2721ds/1244Mi) % 217.77/31.56 % (2270880)Refutation not found, incomplete strategy % 217.77/31.56 % (2270880)------------------------------ % 217.77/31.56 % (2270880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.77/31.56 % (2270880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.77/31.56 % (2270880)CaDiCaL version: 2.1.3 % 217.77/31.56 % (2270880)Termination reason: Refutation not found, incomplete strategy % 217.77/31.56 % (2270880)Time elapsed: 0.042 s % 217.77/31.56 % (2270880)Peak memory usage: 116 MB % 217.77/31.56 % (2270880)Instructions burned: 7 (million) % 217.77/31.56 % (2270878)------------------------------ % 217.77/31.56 % (2270878)------------------------------ % 217.77/31.56 % (2270881)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=3840992925:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2720 on theBenchmark for (2720ds/58261Mi) % 217.77/31.56 % (2270881)Refutation not found, incomplete strategy % 217.77/31.56 % (2270881)------------------------------ % 217.77/31.56 % (2270881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.77/31.56 % (2270881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.77/31.56 % (2270881)CaDiCaL version: 2.1.3 % 217.77/31.56 % (2270881)Termination reason: Refutation not found, incomplete strategy % 217.77/31.56 % (2270881)Time elapsed: 0.060 s % 217.77/31.56 % (2270881)Peak memory usage: 116 MB % 217.77/31.56 % (2270881)Instructions burned: 24 (million) % 217.77/31.56 % (2270880)------------------------------ % 217.77/31.56 % (2270880)------------------------------ % 217.77/31.56 % (2270884)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 % 217.77/31.56 % (2270884)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3958322825:i=6806:aac=none:nm=0:rtra=on:rawr=on_2717 on theBenchmark for (2717ds/6806Mi) % 217.77/31.56 % (2270884)Refutation not found, incomplete strategy % 217.77/31.56 % (2270884)------------------------------ % 217.77/31.56 % (2270884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.77/31.56 % (2270884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.77/31.56 % (2270884)CaDiCaL version: 2.1.3 % 217.77/31.56 % (2270884)Termination reason: Refutation not found, incomplete strategy % 217.77/31.56 % (2270884)Time elapsed: 0.042 s % 217.77/31.56 % (2270884)Peak memory usage: 116 MB % 217.77/31.56 % (2270884)Instructions burned: 7 (million) % 224.44/32.40 % (2270881)------------------------------ % 224.44/32.40 % (2270881)------------------------------ % 224.44/32.40 % (2270885)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=1196920198:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2714 on theBenchmark for (2714ds/4081Mi) % 224.44/32.40 % (2270887)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1195898565:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2712 on theBenchmark for (2712ds/1701Mi) % 224.44/32.40 % (2270884)------------------------------ % 224.44/32.40 % (2270884)------------------------------ % 224.44/32.40 % (2270887)Refutation not found, incomplete strategy % 224.44/32.40 % (2270887)------------------------------ % 224.44/32.40 % (2270887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.44/32.40 % (2270887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.44/32.40 % (2270887)CaDiCaL version: 2.1.3 % 224.44/32.40 % (2270887)Termination reason: Refutation not found, incomplete strategy % 224.44/32.40 % (2270887)Time elapsed: 0.041 s % 224.44/32.40 % (2270887)Peak memory usage: 116 MB % 224.44/32.40 % (2270887)Instructions burned: 7 (million) % 224.44/32.40 % (2270890)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=2743494198:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2709 on theBenchmark for (2709ds/57001Mi) % 224.44/32.40 % (2270890)Refutation not found, incomplete strategy % 224.44/32.40 % (2270890)------------------------------ % 224.44/32.40 % (2270890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.44/32.40 % (2270890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.44/32.40 % (2270890)CaDiCaL version: 2.1.3 % 224.44/32.40 % (2270890)Termination reason: Refutation not found, incomplete strategy % 224.44/32.40 % (2270890)Time elapsed: 0.058 s % 224.44/32.40 % (2270890)Peak memory usage: 116 MB % 224.44/32.40 % (2270890)Instructions burned: 23 (million) % 224.44/32.40 % (2270868)Instruction limit reached! % 224.44/32.40 % (2270868)------------------------------ % 224.44/32.40 % (2270868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.44/32.40 % (2270868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.44/32.40 % (2270868)CaDiCaL version: 2.1.3 % 224.44/32.40 % (2270868)Termination reason: Instruction limit % 224.44/32.40 % (2270868)Termination phase: Saturation % 224.44/32.40 % (2270868)Time elapsed: 4.047 s % 224.44/32.40 % (2270868)Peak memory usage: 107 MB % 224.44/32.40 % (2270868)Instructions burned: 3553 (million) % 224.44/32.40 % (2270887)------------------------------ % 224.44/32.40 % (2270887)------------------------------ % 224.44/32.40 % (2270896)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 % 224.44/32.40 % (2270896)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1368569375:i=8622:aac=none:nm=0:rtra=on:rawr=on_2705 on theBenchmark for (2705ds/8622Mi) % 224.44/32.40 % (2270896)Refutation not found, incomplete strategy % 224.44/32.40 % (2270896)------------------------------ % 224.44/32.40 % (2270896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.44/32.40 % (2270896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.44/32.40 % (2270896)CaDiCaL version: 2.1.3 % 224.44/32.40 % (2270896)Termination reason: Refutation not found, incomplete strategy % 224.44/32.40 % (2270896)Time elapsed: 0.041 s % 224.44/32.40 % (2270896)Peak memory usage: 115 MB % 224.44/32.40 % (2270896)Instructions burned: 7 (million) % 224.44/32.40 % (2270897)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=439949467:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2705 on theBenchmark for (2705ds/24Mi) % 224.44/32.40 % (2270890)------------------------------ % 224.44/32.40 % (2270890)------------------------------ % 224.44/32.40 % (2270897)Instruction limit reached! % 224.44/32.40 % (2270897)------------------------------ % 224.44/32.40 % (2270897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.44/32.40 % (2270897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.44/32.40 % (2270897)CaDiCaL version: 2.1.3 % 224.44/32.40 % (2270897)Termination reason: Instruction limit % 224.44/32.40 % (2270897)Termination phase: Saturation % 227.75/33.14 % (2270897)Time elapsed: 0.053 s % 227.75/33.14 % (2270897)Peak memory usage: 116 MB % 227.75/33.14 % (2270897)Instructions burned: 24 (million) % 227.75/33.14 % (2270900)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1149936501:i=614:kws=precedence:nm=0:rtra=on_2701 on theBenchmark for (2701ds/614Mi) % 227.75/33.14 % (2270901)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1429049605:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2701 on theBenchmark for (2701ds/402Mi) % 227.75/33.14 % (2270900)Refutation not found, incomplete strategy % 227.75/33.14 % (2270900)------------------------------ % 227.75/33.14 % (2270900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.75/33.14 % (2270900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.75/33.14 % (2270900)CaDiCaL version: 2.1.3 % 227.75/33.14 % (2270900)Termination reason: Refutation not found, incomplete strategy % 227.75/33.14 % (2270900)Time elapsed: 0.063 s % 227.75/33.14 % (2270900)Peak memory usage: 116 MB % 227.75/33.14 % (2270900)Instructions burned: 26 (million) % 227.75/33.14 % (2270896)------------------------------ % 227.75/33.14 % (2270896)------------------------------ % 227.75/33.14 % (2270900)------------------------------ % 227.75/33.14 % (2270900)------------------------------ % 227.75/33.14 % (2270905)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1421486145:s2a=on:i=14:rtra=on:inst=on_2698 on theBenchmark for (2698ds/14Mi) % 227.75/33.14 % (2270905)Instruction limit reached! % 227.75/33.14 % (2270905)------------------------------ % 227.75/33.14 % (2270905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.75/33.14 % (2270905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.75/33.14 % (2270905)CaDiCaL version: 2.1.3 % 227.75/33.14 % (2270905)Termination reason: Instruction limit % 227.75/33.14 % (2270905)Termination phase: Saturation % 227.75/33.14 % (2270905)Time elapsed: 0.014 s % 227.75/33.14 % (2270905)Peak memory usage: 88 MB % 227.75/33.14 % (2270905)Instructions burned: 14 (million) % 227.75/33.14 % (2270901)Instruction limit reached! % 227.75/33.14 % (2270901)------------------------------ % 227.75/33.14 % (2270901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.75/33.14 % (2270901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.75/33.14 % (2270901)CaDiCaL version: 2.1.3 % 227.75/33.14 % (2270901)Termination reason: Instruction limit % 227.75/33.14 % (2270901)Termination phase: Saturation % 227.75/33.14 % (2270901)Time elapsed: 0.472 s % 227.75/33.14 % (2270901)Peak memory usage: 120 MB % 227.75/33.14 % (2270901)Instructions burned: 402 (million) % 227.75/33.14 % (2270920)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4161566290:i=8:rtra=on_2695 on theBenchmark for (2695ds/8Mi) % 227.75/33.14 % (2270920)Instruction limit reached! % 227.75/33.14 % (2270920)------------------------------ % 227.75/33.14 % (2270920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.75/33.14 % (2270920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.75/33.14 % (2270920)CaDiCaL version: 2.1.3 % 227.75/33.14 % (2270920)Termination reason: Instruction limit % 227.75/33.14 % (2270920)Termination phase: Saturation % 227.75/33.14 % (2270920)Time elapsed: 0.009 s % 227.75/33.14 % (2270920)Peak memory usage: 89 MB % 227.75/33.14 % (2270920)Instructions burned: 8 (million) % 227.75/33.14 % (2270921)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2416014436:i=92:rtra=on_2695 on theBenchmark for (2695ds/92Mi) % 227.75/33.14 % (2270921)Refutation not found, incomplete strategy % 227.75/33.14 % (2270921)------------------------------ % 227.75/33.14 % (2270921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.75/33.14 % (2270921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.75/33.14 % (2270921)CaDiCaL version: 2.1.3 % 227.75/33.14 % (2270921)Termination reason: Refutation not found, incomplete strategy % 227.75/33.14 % (2270921)Time elapsed: 0.041 s % 227.75/33.14 % (2270921)Peak memory usage: 116 MB % 227.75/33.14 % (2270921)Instructions burned: 7 (million) % 227.75/33.14 % (2270922)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=508184366:i=66:rtra=on_2694 on theBenchmark for (2694ds/66Mi) % 227.75/33.14 % (2270922)Instruction limit reached! % 227.75/33.14 % (2270922)------------------------------ % 227.75/33.14 % (2270922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.75/33.14 % (2270922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.25/33.83 % (2270922)CaDiCaL version: 2.1.3 % 234.25/33.83 % (2270922)Termination reason: Instruction limit % 234.25/33.83 % (2270922)Termination phase: Saturation % 234.25/33.83 % (2270922)Time elapsed: 0.059 s % 234.25/33.83 % (2270922)Peak memory usage: 116 MB % 234.25/33.83 % (2270922)Instructions burned: 66 (million) % 234.25/33.83 % (2270924)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=598483789:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2692 on theBenchmark for (2692ds/28Mi) % 234.25/33.83 % (2270924)Refutation not found, incomplete strategy % 234.25/33.83 % (2270924)------------------------------ % 234.25/33.83 % (2270924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.25/33.83 % (2270924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.25/33.83 % (2270924)CaDiCaL version: 2.1.3 % 234.25/33.83 % (2270924)Termination reason: Refutation not found, incomplete strategy % 234.25/33.83 % (2270924)Time elapsed: 0.002 s % 234.25/33.83 % (2270924)Peak memory usage: 89 MB % 234.25/33.83 % (2270927)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=1341916339:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2691 on theBenchmark for (2691ds/58Mi) % 234.25/33.83 % (2270927)Instruction limit reached! % 234.25/33.83 % (2270927)------------------------------ % 234.25/33.83 % (2270927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.25/33.83 % (2270927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.25/33.83 % (2270927)CaDiCaL version: 2.1.3 % 234.25/33.83 % (2270927)Termination reason: Instruction limit % 234.25/33.83 % (2270927)Termination phase: Saturation % 234.25/33.83 % (2270927)Time elapsed: 0.024 s % 234.25/33.83 % (2270927)Peak memory usage: 88 MB % 234.25/33.83 % (2270927)Instructions burned: 60 (million) % 234.25/33.83 % (2270921)------------------------------ % 234.25/33.83 % (2270921)------------------------------ % 234.25/33.83 % (2270924)------------------------------ % 234.25/33.83 % (2270924)------------------------------ % 234.25/33.83 % (2270930)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4082996881:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2688 on theBenchmark for (2688ds/32Mi) % 234.25/33.83 % (2270930)Refutation not found, incomplete strategy % 234.25/33.83 % (2270930)------------------------------ % 234.25/33.83 % (2270930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.25/33.83 % (2270930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.25/33.83 % (2270930)CaDiCaL version: 2.1.3 % 234.25/33.83 % (2270930)Termination reason: Refutation not found, incomplete strategy % 234.25/33.83 % (2270930)Time elapsed: 0.006 s % 234.25/33.83 % (2270930)Peak memory usage: 90 MB % 234.25/33.83 % (2270930)Instructions burned: 3 (million) % 234.25/33.83 % (2270931)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2111942972:i=48:canc=force:rtra=on_2688 on theBenchmark for (2688ds/48Mi) % 234.25/33.83 % (2270931)Instruction limit reached! % 234.25/33.83 % (2270931)------------------------------ % 234.25/33.83 % (2270931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.25/33.83 % (2270931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.25/33.83 % (2270931)CaDiCaL version: 2.1.3 % 234.25/33.83 % (2270931)Termination reason: Instruction limit % 234.25/33.83 % (2270931)Termination phase: Saturation % 234.25/33.83 % (2270931)Time elapsed: 0.028 s % 234.25/33.83 % (2270931)Peak memory usage: 89 MB % 234.25/33.83 % (2270931)Instructions burned: 48 (million) % 234.25/33.83 % (2270933)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=3203246891:i=54:canc=cautious:fsr=off:rtra=on_2686 on theBenchmark for (2686ds/54Mi) % 234.25/33.83 % (2270935)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1424146902:i=170:gtgl=4:rtra=on:gtg=exists_sym_2685 on theBenchmark for (2685ds/170Mi) % 234.25/33.83 % (2270933)Instruction limit reached! % 234.25/33.83 % (2270933)------------------------------ % 234.25/33.83 % (2270933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.25/33.83 % (2270933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.25/33.83 % (2270933)CaDiCaL version: 2.1.3 % 234.25/33.83 % (2270933)Termination reason: Instruction limit % 234.25/33.83 % (2270933)Termination phase: Saturation % 234.25/33.83 % (2270933)Time elapsed: 0.047 s % 234.25/33.83 % (2270933)Peak memory usage: 90 MB % 234.25/33.83 % (2270933)Instructions burned: 55 (million) % 238.04/34.34 % (2270930)------------------------------ % 238.04/34.34 % (2270930)------------------------------ % 238.04/34.34 % (2270935)Instruction limit reached! % 238.04/34.34 % (2270935)------------------------------ % 238.04/34.34 % (2270935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.04/34.34 % (2270935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.04/34.34 % (2270935)CaDiCaL version: 2.1.3 % 238.04/34.34 % (2270935)Termination reason: Instruction limit % 238.04/34.34 % (2270935)Termination phase: Saturation % 238.04/34.34 % (2270935)Time elapsed: 0.099 s % 238.04/34.34 % (2270935)Peak memory usage: 90 MB % 238.04/34.34 % (2270935)Instructions burned: 171 (million) % 238.04/34.34 % (2270938)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2966690454:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2682 on theBenchmark for (2682ds/4Mi) % 238.04/34.34 % (2270938)Instruction limit reached! % 238.04/34.34 % (2270938)------------------------------ % 238.04/34.34 % (2270938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.04/34.34 % (2270938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.04/34.34 % (2270938)CaDiCaL version: 2.1.3 % 238.04/34.34 % (2270938)Termination reason: Instruction limit % 238.04/34.34 % (2270938)Termination phase: Saturation % 238.04/34.34 % (2270938)Time elapsed: 0.003 s % 238.04/34.34 % (2270938)Peak memory usage: 88 MB % 238.04/34.34 % (2270938)Instructions burned: 4 (million) % 238.04/34.34 % (2270940)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4077977349:i=8:ep=RST:ins=2:rtra=on_2682 on theBenchmark for (2682ds/8Mi) % 238.04/34.34 % (2270940)Instruction limit reached! % 238.04/34.34 % (2270940)------------------------------ % 238.04/34.34 % (2270940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.04/34.34 % (2270940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.04/34.34 % (2270940)CaDiCaL version: 2.1.3 % 238.04/34.34 % (2270940)Termination reason: Instruction limit % 238.04/34.34 % (2270940)Termination phase: Saturation % 238.04/34.34 % (2270940)Time elapsed: 0.007 s % 238.04/34.34 % (2270940)Peak memory usage: 89 MB % 238.04/34.34 % (2270940)Instructions burned: 8 (million) % 238.04/34.34 % (2270939)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4092403098:i=362:rtra=on:ss=axioms:ev=cautious_2682 on theBenchmark for (2682ds/362Mi) % 238.04/34.34 % (2270939)Refutation not found, incomplete strategy % 238.04/34.34 % (2270939)------------------------------ % 238.04/34.34 % (2270939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.04/34.34 % (2270939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.04/34.34 % (2270939)CaDiCaL version: 2.1.3 % 238.04/34.34 % (2270939)Termination reason: Refutation not found, incomplete strategy % 238.04/34.34 % (2270939)Time elapsed: 0.004 s % 238.04/34.34 % (2270939)Peak memory usage: 89 MB % 238.04/34.34 % (2270939)Instructions burned: 2 (million) % 238.04/34.34 % (2270942)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=897185964:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2680 on theBenchmark for (2680ds/132Mi) % 238.04/34.34 % (2270944)lrs+10_1_thi=all:si=on:fd=off:random_seed=3872108358:i=106:rtra=on:gtg=all_2680 on theBenchmark for (2680ds/106Mi) % 238.04/34.34 % (2270944)Instruction limit reached! % 238.04/34.34 % (2270944)------------------------------ % 238.04/34.34 % (2270944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.04/34.34 % (2270944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.04/34.34 % (2270944)CaDiCaL version: 2.1.3 % 238.04/34.34 % (2270944)Termination reason: Instruction limit % 238.04/34.34 % (2270944)Termination phase: Saturation % 238.04/34.34 % (2270944)Time elapsed: 0.082 s % 238.04/34.34 % (2270944)Peak memory usage: 117 MB % 238.04/34.34 % (2270944)Instructions burned: 106 (million) % 238.04/34.34 % (2270942)Instruction limit reached! % 238.04/34.34 % (2270942)------------------------------ % 238.04/34.34 % (2270942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.04/34.34 % (2270942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.04/34.34 % (2270942)CaDiCaL version: 2.1.3 % 238.04/34.34 % (2270942)Termination reason: Instruction limit % 238.04/34.34 % (2270942)Termination phase: Saturation % 238.04/34.34 % (2270942)Time elapsed: 0.203 s % 238.04/34.34 % (2270942)Peak memory usage: 135 MB % 238.04/34.34 % (2270942)Instructions burned: 132 (million) % 238.04/34.34 % (2270939)------------------------------ % 241.49/35.03 % (2270939)------------------------------ % 241.49/35.03 % (2270948)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=206293819:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2676 on theBenchmark for (2676ds/16Mi) % 241.49/35.03 % (2270948)Instruction limit reached! % 241.49/35.03 % (2270948)------------------------------ % 241.49/35.03 % (2270948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.49/35.03 % (2270948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.49/35.03 % (2270948)CaDiCaL version: 2.1.3 % 241.49/35.03 % (2270948)Termination reason: Instruction limit % 241.49/35.03 % (2270948)Termination phase: Saturation % 241.49/35.03 % (2270948)Time elapsed: 0.011 s % 241.49/35.03 % (2270948)Peak memory usage: 89 MB % 241.49/35.03 % (2270948)Instructions burned: 18 (million) % 241.49/35.03 % (2270949)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=935744418:st=3:i=4:rtra=on:ss=axioms_2675 on theBenchmark for (2675ds/4Mi) % 241.49/35.03 % (2270949)Refutation not found, incomplete strategy % 241.49/35.03 % (2270949)------------------------------ % 241.49/35.03 % (2270949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.49/35.03 % (2270949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.49/35.03 % (2270949)CaDiCaL version: 2.1.3 % 241.49/35.03 % (2270949)Termination reason: Refutation not found, incomplete strategy % 241.49/35.03 % (2270949)Time elapsed: 0.006 s % 241.49/35.03 % (2270949)Peak memory usage: 90 MB % 241.49/35.03 % (2270949)Instructions burned: 3 (million) % 241.49/35.03 % (2270950)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=778206470:i=4:doe=on:canc=force:asg=cautious:rtra=on_2675 on theBenchmark for (2675ds/4Mi) % 241.49/35.03 % (2270950)Instruction limit reached! % 241.49/35.03 % (2270950)------------------------------ % 241.49/35.03 % (2270950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.49/35.03 % (2270950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.49/35.03 % (2270950)CaDiCaL version: 2.1.3 % 241.49/35.03 % (2270950)Termination reason: Instruction limit % 241.49/35.03 % (2270950)Termination phase: Saturation % 241.49/35.03 % (2270950)Time elapsed: 0.007 s % 241.49/35.03 % (2270950)Peak memory usage: 89 MB % 241.49/35.03 % (2270950)Instructions burned: 4 (million) % 241.49/35.03 % (2270952)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3041684404:i=254:doe=on:rtra=on_2674 on theBenchmark for (2674ds/254Mi) % 241.49/35.03 % (2270952)Instruction limit reached! % 241.49/35.03 % (2270952)------------------------------ % 241.49/35.03 % (2270952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.49/35.03 % (2270952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.49/35.03 % (2270952)CaDiCaL version: 2.1.3 % 241.49/35.03 % (2270952)Termination reason: Instruction limit % 241.49/35.03 % (2270952)Termination phase: Saturation % 241.49/35.03 % (2270952)Time elapsed: 0.142 s % 241.49/35.03 % (2270952)Peak memory usage: 118 MB % 241.49/35.03 % (2270952)Instructions burned: 255 (million) % 241.49/35.03 % (2270955)dis+10_1_si=on:random_seed=2562199264:i=20:ep=R:rtra=on_2672 on theBenchmark for (2672ds/20Mi) % 241.49/35.03 % (2270885)Instruction limit reached! % 241.49/35.03 % (2270885)------------------------------ % 241.49/35.03 % (2270885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.49/35.03 % (2270885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.49/35.03 % (2270885)CaDiCaL version: 2.1.3 % 241.49/35.03 % (2270885)Termination reason: Instruction limit % 241.49/35.03 % (2270885)Termination phase: Saturation % 241.49/35.03 % (2270885)Time elapsed: 4.115 s % 241.49/35.03 % (2270885)Peak memory usage: 149 MB % 241.49/35.03 % (2270885)Instructions burned: 4082 (million) % 241.49/35.03 % (2270955)Instruction limit reached! % 241.49/35.03 % (2270955)------------------------------ % 241.49/35.03 % (2270955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.49/35.03 % (2270955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.49/35.03 % (2270955)CaDiCaL version: 2.1.3 % 241.49/35.03 % (2270955)Termination reason: Instruction limit % 241.49/35.03 % (2270955)Termination phase: Saturation % 241.49/35.03 % (2270955)Time elapsed: 0.020 s % 241.49/35.03 % (2270955)Peak memory usage: 88 MB % 241.49/35.03 % (2270955)Instructions burned: 20 (million) % 241.49/35.03 % (2270949)------------------------------ % 241.49/35.03 % (2270949)------------------------------ % 241.49/35.03 % (2270957)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4165971112:i=52:canc=cautious:av=off:rtra=on_2670 on theBenchmark for (2670ds/52Mi) % 247.36/35.81 % (2270957)Refutation not found, incomplete strategy % 247.36/35.81 % (2270957)------------------------------ % 247.36/35.81 % (2270957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.36/35.81 % (2270957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.36/35.81 % (2270957)CaDiCaL version: 2.1.3 % 247.36/35.81 % (2270957)Termination reason: Refutation not found, incomplete strategy % 247.36/35.81 % (2270957)Time elapsed: 0.002 s % 247.36/35.81 % (2270957)Peak memory usage: 89 MB % 247.36/35.81 % (2270957)Instructions burned: 2 (million) % 247.36/35.81 % (2270959)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2988932147: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_2669 on theBenchmark for (2669ds/70Mi) % 247.36/35.81 % (2270959)Instruction limit reached! % 247.36/35.81 % (2270959)------------------------------ % 247.36/35.81 % (2270959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.36/35.81 % (2270959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.36/35.81 % (2270959)CaDiCaL version: 2.1.3 % 247.36/35.81 % (2270959)Termination reason: Instruction limit % 247.36/35.81 % (2270959)Termination phase: Saturation % 247.36/35.81 % (2270959)Time elapsed: 0.082 s % 247.36/35.81 % (2270959)Peak memory usage: 89 MB % 247.36/35.81 % (2270959)Instructions burned: 70 (million) % 247.36/35.81 % (2270960)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=696553531:i=4:fsr=off:rtra=on:inst=on_2669 on theBenchmark for (2669ds/4Mi) % 247.36/35.81 % (2270960)Instruction limit reached! % 247.36/35.81 % (2270960)------------------------------ % 247.36/35.81 % (2270960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.36/35.81 % (2270960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.36/35.81 % (2270960)CaDiCaL version: 2.1.3 % 247.36/35.81 % (2270960)Termination reason: Instruction limit % 247.36/35.81 % (2270960)Termination phase: Saturation % 247.36/35.81 % (2270960)Time elapsed: 0.006 s % 247.36/35.81 % (2270960)Peak memory usage: 89 MB % 247.36/35.81 % (2270960)Instructions burned: 5 (million) % 247.36/35.81 % (2270957)------------------------------ % 247.36/35.81 % (2270957)------------------------------ % 247.36/35.81 % (2270961)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1528436567:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2669 on theBenchmark for (2669ds/16Mi) % 247.36/35.81 % (2270961)Instruction limit reached! % 247.36/35.81 % (2270961)------------------------------ % 247.36/35.81 % (2270961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.36/35.81 % (2270961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.36/35.81 % (2270961)CaDiCaL version: 2.1.3 % 247.36/35.81 % (2270961)Termination reason: Instruction limit % 247.36/35.81 % (2270961)Termination phase: Saturation % 247.36/35.81 % (2270961)Time elapsed: 0.018 s % 247.36/35.81 % (2270961)Peak memory usage: 89 MB % 247.36/35.81 % (2270961)Instructions burned: 16 (million) % 247.36/35.81 % (2270964)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=973293627:i=740:ep=RS:fsr=off:rtra=on_2667 on theBenchmark for (2667ds/740Mi) % 247.36/35.81 % (2270968)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=779359329:i=452:rtra=on:gtg=position:ss=axioms_2666 on theBenchmark for (2666ds/452Mi) % 247.36/35.81 % (2270966)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3627225531:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2666 on theBenchmark for (2666ds/26Mi) % 247.36/35.81 % (2270968)Refutation not found, incomplete strategy % 247.36/35.81 % (2270968)------------------------------ % 247.36/35.81 % (2270968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.36/35.81 % (2270968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.36/35.81 % (2270968)CaDiCaL version: 2.1.3 % 247.36/35.81 % (2270968)Termination reason: Refutation not found, incomplete strategy % 247.36/35.81 % (2270968)Time elapsed: 0.025 s % 247.36/35.81 % (2270968)Peak memory usage: 116 MB % 247.36/35.81 % (2270968)Instructions burned: 7 (million) % 247.36/35.81 % (2270966)Instruction limit reached! % 247.36/35.81 % (2270966)------------------------------ % 247.36/35.81 % (2270966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.68/36.40 % (2270966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.68/36.40 % (2270966)CaDiCaL version: 2.1.3 % 252.68/36.40 % (2270966)Termination reason: Instruction limit % 252.68/36.40 % (2270966)Termination phase: Saturation % 252.68/36.40 % (2270966)Time elapsed: 0.063 s % 252.68/36.40 % (2270966)Peak memory usage: 116 MB % 252.68/36.40 % (2270966)Instructions burned: 26 (million) % 252.68/36.40 % (2270969)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1501469950:i=20:rtra=on_2666 on theBenchmark for (2666ds/20Mi) % 252.68/36.40 % (2270969)Refutation not found, incomplete strategy % 252.68/36.40 % (2270969)------------------------------ % 252.68/36.40 % (2270969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.68/36.40 % (2270969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.68/36.40 % (2270969)CaDiCaL version: 2.1.3 % 252.68/36.40 % (2270969)Termination reason: Refutation not found, incomplete strategy % 252.68/36.40 % (2270969)Time elapsed: 0.002 s % 252.68/36.40 % (2270969)Peak memory usage: 88 MB % 252.68/36.40 % (2270968)------------------------------ % 252.68/36.40 % (2270968)------------------------------ % 252.68/36.40 % (2270863)Instruction limit reached! % 252.68/36.40 % (2270863)------------------------------ % 252.68/36.40 % (2270863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.68/36.40 % (2270863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.68/36.40 % (2270863)CaDiCaL version: 2.1.3 % 252.68/36.40 % (2270863)Termination reason: Instruction limit % 252.68/36.40 % (2270863)Termination phase: Saturation % 252.68/36.40 % (2270863)Time elapsed: 9.081 s % 252.68/36.40 % (2270863)Peak memory usage: 124 MB % 252.68/36.40 % (2270863)Instructions burned: 9201 (million) % 252.68/36.40 % (2270973)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1128145713:i=142:rtra=on:gtg=exists_top_2663 on theBenchmark for (2663ds/142Mi) % 252.68/36.40 % (2270973)Refutation not found, incomplete strategy % 252.68/36.40 % (2270973)------------------------------ % 252.68/36.40 % (2270973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.68/36.40 % (2270973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.68/36.40 % (2270973)CaDiCaL version: 2.1.3 % 252.68/36.40 % (2270973)Termination reason: Refutation not found, incomplete strategy % 252.68/36.40 % (2270973)Time elapsed: 0.075 s % 252.68/36.40 % (2270973)Peak memory usage: 133 MB % 252.68/36.40 % (2270973)Instructions burned: 12 (million) % 252.68/36.40 % (2270969)------------------------------ % 252.68/36.40 % (2270969)------------------------------ % 252.68/36.40 % (2270975)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=114217225:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2661 on theBenchmark for (2661ds/150Mi) % 252.68/36.40 % (2270964)Instruction limit reached! % 252.68/36.40 % (2270964)------------------------------ % 252.68/36.40 % (2270964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.68/36.40 % (2270964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.68/36.40 % (2270964)CaDiCaL version: 2.1.3 % 252.68/36.40 % (2270964)Termination reason: Instruction limit % 252.68/36.40 % (2270964)Termination phase: Saturation % 252.68/36.40 % (2270964)Time elapsed: 0.588 s % 252.68/36.40 % (2270964)Peak memory usage: 90 MB % 252.68/36.40 % (2270964)Instructions burned: 740 (million) % 252.68/36.40 % (2270977)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=1918430068:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2660 on theBenchmark for (2660ds/588Mi) % 252.68/36.40 % (2270975)Instruction limit reached! % 252.68/36.40 % (2270975)------------------------------ % 252.68/36.40 % (2270975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.68/36.40 % (2270975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.68/36.40 % (2270975)CaDiCaL version: 2.1.3 % 252.68/36.40 % (2270975)Termination reason: Instruction limit % 252.68/36.40 % (2270975)Termination phase: Saturation % 252.68/36.40 % (2270975)Time elapsed: 0.108 s % 252.68/36.40 % (2270975)Peak memory usage: 89 MB % 252.68/36.40 % (2270975)Instructions burned: 150 (million) % 252.68/36.40 % (2270979)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=359591650:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2659 on theBenchmark for (2659ds/260Mi) % 252.68/36.40 % (2270980)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3579700974:i=262:rtra=on_2658 on theBenchmark for (2658ds/262Mi) % 256.11/37.09 % (2270977)Instruction limit reached! % 256.11/37.09 % (2270977)------------------------------ % 256.11/37.09 % (2270977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.11/37.09 % (2270977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.11/37.09 % (2270977)CaDiCaL version: 2.1.3 % 256.11/37.09 % (2270977)Termination reason: Instruction limit % 256.11/37.09 % (2270977)Termination phase: Saturation % 256.11/37.09 % (2270977)Time elapsed: 0.212 s % 256.11/37.09 % (2270977)Peak memory usage: 89 MB % 256.11/37.09 % (2270977)Instructions burned: 590 (million) % 256.11/37.09 % (2270979)Refutation not found, incomplete strategy % 256.11/37.09 % (2270979)------------------------------ % 256.11/37.09 % (2270979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.11/37.09 % (2270973)------------------------------ % 256.11/37.09 % (2270973)------------------------------ % 256.11/37.09 % (2270979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.11/37.09 % (2270979)CaDiCaL version: 2.1.3 % 256.11/37.09 % (2270979)Termination reason: Refutation not found, incomplete strategy % 256.11/37.09 % (2270979)Time elapsed: 0.057 s % 256.11/37.09 % (2270979)Peak memory usage: 116 MB % 256.11/37.09 % (2270979)Instructions burned: 20 (million) % 256.11/37.09 % (2270980)Refutation not found, incomplete strategy % 256.11/37.09 % (2270980)------------------------------ % 256.11/37.09 % (2270980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.11/37.09 % (2270980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.11/37.09 % (2270980)CaDiCaL version: 2.1.3 % 256.11/37.09 % (2270980)Termination reason: Refutation not found, incomplete strategy % 256.11/37.09 % (2270980)Time elapsed: 0.074 s % 256.11/37.09 % (2270980)Peak memory usage: 133 MB % 256.11/37.09 % (2270980)Instructions burned: 12 (million) % 256.11/37.09 % (2270982)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3676986714:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2658 on theBenchmark for (2658ds/80Mi) % 256.11/37.09 % (2270982)Instruction limit reached! % 256.11/37.09 % (2270982)------------------------------ % 256.11/37.09 % (2270982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.11/37.09 % (2270982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.11/37.09 % (2270982)CaDiCaL version: 2.1.3 % 256.11/37.09 % (2270982)Termination reason: Instruction limit % 256.11/37.09 % (2270982)Termination phase: Saturation % 256.11/37.09 % (2270982)Time elapsed: 0.149 s % 256.11/37.09 % (2270982)Peak memory usage: 134 MB % 256.11/37.09 % (2270982)Instructions burned: 81 (million) % 256.11/37.09 % (2270986)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=631469580:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2656 on theBenchmark for (2656ds/1196Mi) % 256.11/37.09 % (2270985)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1065559683:i=614:rtra=on:gtg=exists_top_2656 on theBenchmark for (2656ds/614Mi) % 256.11/37.09 % (2270986)Refutation not found, incomplete strategy % 256.11/37.09 % (2270986)------------------------------ % 256.11/37.09 % (2270986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.11/37.09 % (2270986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.11/37.10 % (2270986)CaDiCaL version: 2.1.3 % 256.11/37.10 % (2270986)Termination reason: Refutation not found, incomplete strategy % 256.11/37.10 % (2270986)Time elapsed: 0.046 s % 256.11/37.10 % (2270986)Peak memory usage: 133 MB % 256.11/37.10 % (2270986)Instructions burned: 13 (million) % 256.11/37.10 % (2270979)------------------------------ % 256.11/37.10 % (2270979)------------------------------ % 256.11/37.10 % (2270980)------------------------------ % 256.11/37.10 % (2270980)------------------------------ % 256.11/37.10 % (2270988)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1828517211:i=262:canc=cautious:fsr=off:rtra=on_2653 on theBenchmark for (2653ds/262Mi) % 256.11/37.10 % (2270986)------------------------------ % 256.11/37.10 % (2270986)------------------------------ % 256.11/37.10 % (2270991)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=797317718:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2652 on theBenchmark for (2652ds/518Mi) % 256.11/37.10 % (2270992)dis+10_1_si=on:random_seed=1332204197:s2a=on:i=2000:rtra=on:gtg=exists_all_2651 on theBenchmark for (2651ds/2000Mi) % 256.11/37.10 % (2270988)Instruction limit reached! % 266.29/38.32 % (2270988)------------------------------ % 266.29/38.32 % (2270988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2270988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.29/38.32 % (2270988)CaDiCaL version: 2.1.3 % 266.29/38.32 % (2270988)Termination reason: Instruction limit % 266.29/38.32 % (2270988)Termination phase: Saturation % 266.29/38.32 % (2270988)Time elapsed: 0.271 s % 266.29/38.32 % (2270988)Peak memory usage: 118 MB % 266.29/38.32 % (2270988)Instructions burned: 262 (million) % 266.29/38.32 % (2270994)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1139186469:i=766:fsr=off:rtra=on:ev=force_2650 on theBenchmark for (2650ds/766Mi) % 266.29/38.32 % (2270994)Refutation not found, incomplete strategy % 266.29/38.32 % (2270994)------------------------------ % 266.29/38.32 % (2270994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2270994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.29/38.32 % (2270994)CaDiCaL version: 2.1.3 % 266.29/38.32 % (2270994)Termination reason: Refutation not found, incomplete strategy % 266.29/38.32 % (2270994)Time elapsed: 0.003 s % 266.29/38.32 % (2270994)Peak memory usage: 89 MB % 266.29/38.32 % (2270994)Instructions burned: 3 (million) % 266.29/38.32 % (2270985)Instruction limit reached! % 266.29/38.32 % (2270985)------------------------------ % 266.29/38.32 % (2270985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2270985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.29/38.32 % (2270985)CaDiCaL version: 2.1.3 % 266.29/38.32 % (2270985)Termination reason: Instruction limit % 266.29/38.32 % (2270985)Termination phase: Saturation % 266.29/38.32 % (2270985)Time elapsed: 0.519 s % 266.29/38.32 % (2270985)Peak memory usage: 92 MB % 266.29/38.32 % (2270985)Instructions burned: 614 (million) % 266.29/38.32 % (2270994)------------------------------ % 266.29/38.32 % (2270994)------------------------------ % 266.29/38.32 % (2270997)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3821688365:i=282:doe=on:rtra=on_2648 on theBenchmark for (2648ds/282Mi) % 266.29/38.32 % (2270999)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1431718292:i=130:nm=16:rtra=on_2648 on theBenchmark for (2648ds/130Mi) % 266.29/38.32 % (2270999)Refutation not found, incomplete strategy % 266.29/38.32 % (2270999)------------------------------ % 266.29/38.32 % (2270999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2270999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.29/38.32 % (2270999)CaDiCaL version: 2.1.3 % 266.29/38.32 % (2270999)Termination reason: Refutation not found, incomplete strategy % 266.29/38.32 % (2270999)Time elapsed: 0.041 s % 266.29/38.32 % (2270999)Peak memory usage: 115 MB % 266.29/38.32 % (2270999)Instructions burned: 6 (million) % 266.29/38.32 % (2270991)Instruction limit reached! % 266.29/38.32 % (2270991)------------------------------ % 266.29/38.32 % (2270991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2270991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.29/38.32 % (2270991)CaDiCaL version: 2.1.3 % 266.29/38.32 % (2270991)Termination reason: Instruction limit % 266.29/38.32 % (2270991)Termination phase: Saturation % 266.29/38.32 % (2270991)Time elapsed: 0.491 s % 266.29/38.32 % (2270991)Peak memory usage: 117 MB % 266.29/38.32 % (2270991)Instructions burned: 518 (million) % 266.29/38.32 % (2271000)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1682431573:i=242:nm=16:rtra=on_2646 on theBenchmark for (2646ds/242Mi) % 266.29/38.32 % (2270997)Instruction limit reached! % 266.29/38.32 % (2270997)------------------------------ % 266.29/38.32 % (2270997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2270997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.29/38.32 % (2270997)CaDiCaL version: 2.1.3 % 266.29/38.32 % (2270997)Termination reason: Instruction limit % 266.29/38.32 % (2270997)Termination phase: Saturation % 266.29/38.32 % (2270997)Time elapsed: 0.282 s % 266.29/38.32 % (2270997)Peak memory usage: 91 MB % 266.29/38.32 % (2270997)Instructions burned: 282 (million) % 266.29/38.32 % (2271000)Instruction limit reached! % 266.29/38.32 % (2271000)------------------------------ % 266.29/38.32 % (2271000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.29/38.32 % (2271000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.14/38.95 % (2271000)CaDiCaL version: 2.1.3 % 269.14/38.95 % (2271000)Termination reason: Instruction limit % 269.14/38.95 % (2271000)Termination phase: Saturation % 269.14/38.95 % (2271000)Time elapsed: 0.088 s % 269.14/38.95 % (2271000)Peak memory usage: 88 MB % 269.14/38.95 % (2271000)Instructions burned: 245 (million) % 269.14/38.95 % (2271003)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=329339191:s2a=on:i=256:s2at=5:ins=3:rtra=on_2644 on theBenchmark for (2644ds/256Mi) % 269.14/38.95 % (2270999)------------------------------ % 269.14/38.95 % (2270999)------------------------------ % 269.14/38.95 % (2271006)dis+1010_1_to=kbo:si=on:random_seed=3167684448:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2642 on theBenchmark for (2642ds/350Mi) % 269.14/38.95 % (2271005)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=3840324707:i=78:ins=3:rtra=on_2643 on theBenchmark for (2643ds/78Mi) % 269.14/38.95 % (2271005)Instruction limit reached! % 269.14/38.95 % (2271005)------------------------------ % 269.14/38.95 % (2271005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.14/38.95 % (2271005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.14/38.95 % (2271005)CaDiCaL version: 2.1.3 % 269.14/38.95 % (2271005)Termination reason: Instruction limit % 269.14/38.95 % (2271005)Termination phase: Saturation % 269.14/38.95 % (2271005)Time elapsed: 0.110 s % 269.14/38.95 % (2271005)Peak memory usage: 116 MB % 269.14/38.95 % (2271005)Instructions burned: 78 (million) % 269.14/38.95 % (2271003)Instruction limit reached! % 269.14/38.95 % (2271003)------------------------------ % 269.14/38.95 % (2271003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.14/38.95 % (2271003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.14/38.95 % (2271003)CaDiCaL version: 2.1.3 % 269.14/38.95 % (2271003)Termination reason: Instruction limit % 269.14/38.95 % (2271003)Termination phase: Saturation % 269.14/38.95 % (2271003)Time elapsed: 0.292 s % 269.14/38.95 % (2271003)Peak memory usage: 118 MB % 269.14/38.95 % (2271003)Instructions burned: 256 (million) % 269.14/38.95 % (2271008)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2040579171:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2641 on theBenchmark for (2641ds/658Mi) % 269.14/38.95 % (2271006)Instruction limit reached! % 269.14/38.95 % (2271006)------------------------------ % 269.14/38.95 % (2271006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.14/38.95 % (2271006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.14/38.95 % (2271006)CaDiCaL version: 2.1.3 % 269.14/38.95 % (2271006)Termination reason: Instruction limit % 269.14/38.95 % (2271006)Termination phase: Saturation % 269.14/38.95 % (2271006)Time elapsed: 0.204 s % 269.14/38.95 % (2271006)Peak memory usage: 92 MB % 269.14/38.95 % (2271006)Instructions burned: 352 (million) % 269.14/38.95 % (2271011)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2376689884:s2a=on:i=966:doe=on:nm=32:rtra=on_2639 on theBenchmark for (2639ds/966Mi) % 269.14/38.95 % (2271012)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4249622426:thitd=on:i=430:nm=0:rtra=on:ev=force_2638 on theBenchmark for (2638ds/430Mi) % 269.14/38.95 % (2271011)Refutation not found, incomplete strategy % 269.14/38.95 % (2271011)------------------------------ % 269.14/38.95 % (2271011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.14/38.95 % (2271011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.14/38.95 % (2271011)CaDiCaL version: 2.1.3 % 269.14/38.95 % (2271011)Termination reason: Refutation not found, incomplete strategy % 269.14/38.95 % (2271011)Time elapsed: 0.076 s % 269.14/38.95 % (2271011)Peak memory usage: 132 MB % 269.14/38.95 % (2271011)Instructions burned: 12 (million) % 269.14/38.95 % (2271012)Refutation not found, incomplete strategy % 269.14/38.95 % (2271012)------------------------------ % 269.14/38.95 % (2271012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.14/38.95 % (2271012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.14/38.95 % (2271012)CaDiCaL version: 2.1.3 % 269.14/38.95 % (2271012)Termination reason: Refutation not found, incomplete strategy % 269.14/38.95 % (2271012)Time elapsed: 0.059 s % 269.14/38.95 % (2271012)Peak memory usage: 134 MB % 269.14/38.95 % (2271012)Instructions burned: 33 (million) % 269.14/38.95 % (2271014)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=695327220:i=698:rtra=on_2638 on theBenchmark for (2638ds/698Mi) % 275.24/39.82 % (2271014)Refutation not found, incomplete strategy % 275.24/39.82 % (2271014)------------------------------ % 275.24/39.82 % (2271014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.24/39.82 % (2271014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.82 % (2271014)CaDiCaL version: 2.1.3 % 275.24/39.82 % (2271014)Termination reason: Refutation not found, incomplete strategy % 275.24/39.82 % (2271014)Time elapsed: 0.041 s % 275.24/39.82 % (2271014)Peak memory usage: 116 MB % 275.24/39.82 % (2271014)Instructions burned: 7 (million) % 275.24/39.82 % (2271012)------------------------------ % 275.24/39.82 % (2271012)------------------------------ % 275.24/39.82 % (2271011)------------------------------ % 275.24/39.82 % (2271011)------------------------------ % 275.24/39.82 % (2271014)------------------------------ % 275.24/39.82 % (2271014)------------------------------ % 275.24/39.82 % (2271018)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=616693216:st=2:i=590:rtra=on:ss=axioms_2633 on theBenchmark for (2633ds/590Mi) % 275.24/39.82 % (2271008)Instruction limit reached! % 275.24/39.82 % (2271008)------------------------------ % 275.24/39.82 % (2271008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.24/39.82 % (2271008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.82 % (2271008)CaDiCaL version: 2.1.3 % 275.24/39.82 % (2271008)Termination reason: Instruction limit % 275.24/39.82 % (2271008)Termination phase: Saturation % 275.24/39.82 % (2271008)Time elapsed: 0.735 s % 275.24/39.82 % (2271008)Peak memory usage: 121 MB % 275.24/39.82 % (2271008)Instructions burned: 659 (million) % 275.24/39.82 % (2270992)Instruction limit reached! % 275.24/39.82 % (2270992)------------------------------ % 275.24/39.82 % (2270992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.24/39.82 % (2270992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.82 % (2270992)CaDiCaL version: 2.1.3 % 275.24/39.82 % (2270992)Termination reason: Instruction limit % 275.24/39.82 % (2270992)Termination phase: Saturation % 275.24/39.82 % (2270992)Time elapsed: 1.946 s % 275.24/39.82 % (2270992)Peak memory usage: 101 MB % 275.24/39.82 % (2270992)Instructions burned: 2000 (million) % 275.24/39.82 % (2271019)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1714729658:i=656:kws=inv_frequency:nm=20:rtra=on_2632 on theBenchmark for (2632ds/656Mi) % 275.24/39.82 % (2271020)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2986927290:i=562:gtgl=2:rtra=on:gtg=all_2631 on theBenchmark for (2631ds/562Mi) % 275.24/39.82 % (2271018)Instruction limit reached! % 275.24/39.82 % (2271018)------------------------------ % 275.24/39.82 % (2271018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.24/39.82 % (2271018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.82 % (2271018)CaDiCaL version: 2.1.3 % 275.24/39.82 % (2271018)Termination reason: Instruction limit % 275.24/39.82 % (2271018)Termination phase: Saturation % 275.24/39.82 % (2271018)Time elapsed: 0.295 s % 275.24/39.82 % (2271018)Peak memory usage: 92 MB % 275.24/39.82 % (2271018)Instructions burned: 591 (million) % 275.24/39.82 % (2271022)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2093130452:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2631 on theBenchmark for (2631ds/968Mi) % 275.24/39.82 % (2271024)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2430261953:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2629 on theBenchmark for (2629ds/642Mi) % 275.24/39.82 % (2271027)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=53458227:i=832:rtra=on:gtg=position:ss=axioms_2628 on theBenchmark for (2628ds/832Mi) % 275.24/39.82 % (2271027)Refutation not found, incomplete strategy % 275.24/39.82 % (2271027)------------------------------ % 275.24/39.82 % (2271027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.24/39.82 % (2271027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.82 % (2271027)CaDiCaL version: 2.1.3 % 275.24/39.82 % (2271027)Termination reason: Refutation not found, incomplete strategy % 275.24/39.82 % (2271027)Time elapsed: 0.025 s % 275.24/39.82 % (2271027)Peak memory usage: 115 MB % 275.24/39.82 % (2271027)Instructions burned: 7 (million) % 275.24/39.82 % (2271027)------------------------------ % 275.24/39.82 % (2271027)------------------------------ % 281.96/40.62 % (2271020)Instruction limit reached! % 281.96/40.62 % (2271020)------------------------------ % 281.96/40.62 % (2271020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.96/40.62 % (2271020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.96/40.62 % (2271020)CaDiCaL version: 2.1.3 % 281.96/40.62 % (2271020)Termination reason: Instruction limit % 281.96/40.62 % (2271020)Termination phase: Saturation % 281.96/40.62 % (2271020)Time elapsed: 0.608 s % 281.96/40.62 % (2271020)Peak memory usage: 120 MB % 281.96/40.62 % (2271020)Instructions burned: 562 (million) % 281.96/40.62 % (2271019)Instruction limit reached! % 281.96/40.62 % (2271019)------------------------------ % 281.96/40.62 % (2271019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.96/40.62 % (2271019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.96/40.62 % (2271019)CaDiCaL version: 2.1.3 % 281.96/40.62 % (2271019)Termination reason: Instruction limit % 281.96/40.62 % (2271019)Termination phase: Saturation % 281.96/40.62 % (2271019)Time elapsed: 0.691 s % 281.96/40.62 % (2271019)Peak memory usage: 120 MB % 281.96/40.62 % (2271019)Instructions burned: 656 (million) % 281.96/40.62 % (2271030)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1639571741:i=942:thf=on:kws=precedence:rtra=on_2623 on theBenchmark for (2623ds/942Mi) % 281.96/40.62 % (2271030)Refutation not found, incomplete strategy % 281.96/40.62 % (2271030)------------------------------ % 281.96/40.62 % (2271030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.96/40.62 % (2271030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.96/40.62 % (2271030)CaDiCaL version: 2.1.3 % 281.96/40.62 % (2271030)Termination reason: Refutation not found, incomplete strategy % 281.96/40.62 % (2271030)Time elapsed: 0.025 s % 281.96/40.62 % (2271030)Peak memory usage: 115 MB % 281.96/40.62 % (2271030)Instructions burned: 7 (million) % 281.96/40.62 % (2271024)Instruction limit reached! % 281.96/40.62 % (2271024)------------------------------ % 281.96/40.62 % (2271024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.96/40.62 % (2271024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.96/40.62 % (2271024)CaDiCaL version: 2.1.3 % 281.96/40.62 % (2271024)Termination reason: Instruction limit % 281.96/40.62 % (2271024)Termination phase: Saturation % 281.96/40.62 % (2271024)Time elapsed: 0.614 s % 281.96/40.62 % (2271024)Peak memory usage: 116 MB % 281.96/40.62 % (2271024)Instructions burned: 642 (million) % 281.96/40.62 % (2271022)Instruction limit reached! % 281.96/40.62 % (2271022)------------------------------ % 281.96/40.62 % (2271022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.96/40.62 % (2271022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.96/40.62 % (2271022)CaDiCaL version: 2.1.3 % 281.96/40.62 % (2271022)Termination reason: Instruction limit % 281.96/40.62 % (2271022)Termination phase: Saturation % 281.96/40.62 % (2271022)Time elapsed: 0.834 s % 281.96/40.62 % (2271022)Peak memory usage: 92 MB % 281.96/40.62 % (2271022)Instructions burned: 968 (million) % 281.96/40.62 % (2271032)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=531233490:i=750:kws=inv_arity_squared:rtra=on_2622 on theBenchmark for (2622ds/750Mi) % 281.96/40.62 % (2271031)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=2457066800:avsq=on:i=552:avsqr=1,2:rtra=on_2622 on theBenchmark for (2622ds/552Mi) % 281.96/40.62 % (2271032)Refutation not found, incomplete strategy % 281.96/40.62 % (2271032)------------------------------ % 281.96/40.62 % (2271032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.96/40.62 % (2271032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.96/40.62 % (2271032)CaDiCaL version: 2.1.3 % 281.96/40.62 % (2271032)Termination reason: Refutation not found, incomplete strategy % 281.96/40.62 % (2271032)Time elapsed: 0.041 s % 281.96/40.62 % (2271032)Peak memory usage: 115 MB % 281.96/40.62 % (2271032)Instructions burned: 7 (million) % 281.96/40.62 % (2271030)------------------------------ % 281.96/40.62 % (2271030)------------------------------ % 281.96/40.62 % (2271034)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=614145785:i=774:bd=preordered:rtra=on:ss=axioms:sgt=8_2620 on theBenchmark for (2620ds/774Mi) % 281.96/40.62 % (2271035)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3435685643:i=1026:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2620 on theBenchmark for (2620ds/1026Mi) % 288.89/41.69 % (2271038)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3342286508:i=668:rtra=on_2618 on theBenchmark for (2618ds/668Mi) % 288.89/41.69 % (2271038)Refutation not found, incomplete strategy % 288.89/41.69 % (2271038)------------------------------ % 288.89/41.69 % (2271038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.89/41.69 % (2271038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.89/41.69 % (2271038)CaDiCaL version: 2.1.3 % 288.89/41.69 % (2271038)Termination reason: Refutation not found, incomplete strategy % 288.89/41.69 % (2271038)Time elapsed: 0.044 s % 288.89/41.69 % (2271038)Peak memory usage: 132 MB % 288.89/41.69 % (2271038)Instructions burned: 12 (million) % 288.89/41.69 % (2271032)------------------------------ % 288.89/41.69 % (2271032)------------------------------ % 288.89/41.69 % (2271031)Instruction limit reached! % 288.89/41.69 % (2271031)------------------------------ % 288.89/41.69 % (2271031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.89/41.69 % (2271031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.89/41.69 % (2271031)CaDiCaL version: 2.1.3 % 288.89/41.69 % (2271031)Termination reason: Instruction limit % 288.89/41.69 % (2271031)Termination phase: Saturation % 288.89/41.69 % (2271031)Time elapsed: 0.515 s % 288.89/41.69 % (2271031)Peak memory usage: 134 MB % 288.89/41.69 % (2271031)Instructions burned: 553 (million) % 288.89/41.69 % (2271038)------------------------------ % 288.89/41.69 % (2271038)------------------------------ % 288.89/41.69 % (2271042)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=182314141:i=718:rtra=on:gtg=exists_top:ss=axioms_2615 on theBenchmark for (2615ds/718Mi) % 288.89/41.69 % (2271042)Refutation not found, incomplete strategy % 288.89/41.69 % (2271042)------------------------------ % 288.89/41.69 % (2271042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.89/41.69 % (2271042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.89/41.69 % (2271042)CaDiCaL version: 2.1.3 % 288.89/41.69 % (2271042)Termination reason: Refutation not found, incomplete strategy % 288.89/41.69 % (2271042)Time elapsed: 0.004 s % 288.89/41.69 % (2271042)Peak memory usage: 89 MB % 288.89/41.69 % (2271042)Instructions burned: 2 (million) % 288.89/41.69 % (2271045)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2912671097:i=682:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2614 on theBenchmark for (2614ds/682Mi) % 288.89/41.69 % (2271046)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3729460940:st=1.5:i=522:sd=1:kws=precedence:rtra=on:ss=axioms_2613 on theBenchmark for (2613ds/522Mi) % 288.89/41.69 % (2271045)Refutation not found, incomplete strategy % 288.89/41.69 % (2271045)------------------------------ % 288.89/41.69 % (2271045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.89/41.69 % (2271045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.89/41.69 % (2271045)CaDiCaL version: 2.1.3 % 288.89/41.69 % (2271045)Termination reason: Refutation not found, incomplete strategy % 288.89/41.69 % (2271045)Time elapsed: 0.039 s % 288.89/41.69 % (2271045)Peak memory usage: 113 MB % 288.89/41.69 % (2271045)Instructions burned: 6 (million) % 288.89/41.69 % (2271046)Refutation not found, incomplete strategy % 288.89/41.69 % (2271046)------------------------------ % 288.89/41.69 % (2271046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.89/41.69 % (2271046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.89/41.69 % (2271046)CaDiCaL version: 2.1.3 % 288.89/41.69 % (2271046)Termination reason: Refutation not found, incomplete strategy % 288.89/41.69 % (2271046)Time elapsed: 0.028 s % 288.89/41.69 % (2271046)Peak memory usage: 116 MB % 288.89/41.69 % (2271046)Instructions burned: 11 (million) % 288.89/41.69 % (2271046)------------------------------ % 288.89/41.69 % (2271046)------------------------------ % 288.89/41.69 % (2271042)------------------------------ % 288.89/41.69 % (2271042)------------------------------ % 288.89/41.69 % (2271034)Instruction limit reached! % 288.89/41.69 % (2271034)------------------------------ % 288.89/41.69 % (2271034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.89/41.69 % (2271034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.89/41.69 % (2271034)CaDiCaL version: 2.1.3 % 297.71/43.05 % (2271034)Termination reason: Instruction limit % 297.71/43.05 % (2271034)Termination phase: Saturation % 297.71/43.05 % (2271034)Time elapsed: 0.905 s % 297.71/43.05 % (2271034)Peak memory usage: 122 MB % 297.71/43.05 % (2271034)Instructions burned: 774 (million) % 297.71/43.05 % (2271045)------------------------------ % 297.71/43.05 % (2271045)------------------------------ % 297.71/43.05 % (2271035)Instruction limit reached! % 297.71/43.05 % (2271035)------------------------------ % 297.71/43.05 % (2271035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.71/43.05 % (2271035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/43.05 % (2271035)CaDiCaL version: 2.1.3 % 297.71/43.05 % (2271035)Termination reason: Instruction limit % 297.71/43.05 % (2271035)Termination phase: Saturation % 297.71/43.05 % (2271035)Time elapsed: 0.998 s % 297.71/43.05 % (2271035)Peak memory usage: 95 MB % 297.71/43.05 % (2271035)Instructions burned: 1027 (million) % 297.71/43.05 % (2271050)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=992114676:s2pl=no:i=470:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2608 on theBenchmark for (2608ds/470Mi) % 297.71/43.06 % (2271051)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=427028872:i=546:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2608 on theBenchmark for (2608ds/546Mi) % 297.71/43.06 % (2271052)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2513028125:i=292:doe=on:rtra=on_2608 on theBenchmark for (2608ds/292Mi) % 297.71/43.06 % (2271053)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1409024520:i=8856:doe=on:fsr=off:rtra=on_2607 on theBenchmark for (2607ds/8856Mi) % 297.71/43.06 % (2271054)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=3453145674:avsq=on:i=552:avsqr=1,2:rtra=on_2607 on theBenchmark for (2607ds/552Mi) % 297.71/43.06 % (2271051)Instruction limit reached! % 297.71/43.06 % (2271051)------------------------------ % 297.71/43.06 % (2271051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.71/43.06 % (2271051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/43.06 % (2271051)CaDiCaL version: 2.1.3 % 297.71/43.06 % (2271051)Termination reason: Instruction limit % 297.71/43.06 % (2271051)Termination phase: Saturation % 297.71/43.06 % (2271051)Time elapsed: 0.310 s % 297.71/43.06 % (2271051)Peak memory usage: 95 MB % 297.71/43.06 % (2271051)Instructions burned: 547 (million) % 297.71/43.06 % (2271052)Instruction limit reached! % 297.71/43.06 % (2271052)------------------------------ % 297.71/43.06 % (2271052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.71/43.06 % (2271052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/43.06 % (2271052)CaDiCaL version: 2.1.3 % 297.71/43.06 % (2271052)Termination reason: Instruction limit % 297.71/43.06 % (2271052)Termination phase: Saturation % 297.71/43.06 % (2271052)Time elapsed: 0.286 s % 297.71/43.06 % (2271052)Peak memory usage: 92 MB % 297.71/43.06 % (2271052)Instructions burned: 292 (million) % 297.71/43.06 % (2271050)Instruction limit reached! % 297.71/43.06 % (2271050)------------------------------ % 297.71/43.06 % (2271050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.71/43.06 % (2271050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/43.06 % (2271050)CaDiCaL version: 2.1.3 % 297.71/43.06 % (2271050)Termination reason: Instruction limit % 297.71/43.06 % (2271050)Termination phase: Saturation % 297.71/43.06 % (2271050)Time elapsed: 0.424 s % 297.71/43.06 % (2271050)Peak memory usage: 117 MB % 297.71/43.06 % (2271050)Instructions burned: 470 (million) % 297.71/43.06 % (2271060)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1123630323:i=2104:rtra=on_2603 on theBenchmark for (2603ds/2104Mi) % 297.71/43.06 % (2271062)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2789046683:st=5:i=2108:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2602 on theBenchmark for (2602ds/2108Mi) % 297.71/43.06 % (2271062)Refutation not found, incomplete strategy % 297.71/43.06 % (2271062)------------------------------ % 297.71/43.06 % (2271062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.71/43.06 % (2271062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/43.06 % (2271062)CaDTerminated %------------------------------------------------------------------------------