%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX104_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:53 PM UTC 2026 % Result : Timeout 300.41s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX104_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.27 % Computer : n014.cluster.edu % 0.10/0.27 % Model : x86_64 x86_64 % 0.10/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.27 % Memory : 8046.5625MB % 0.10/0.27 % OS : Linux 6.8.0-71-generic % 0.10/0.27 % CPULimit : 300 % 0.10/0.27 % WCLimit : 300 % 0.10/0.27 % DateTime : Mon Sep 28 15:01:16 UTC 2026 % 0.26/0.27 % CPUTime : % 0.26/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.26/0.32 Running first-order theorem proving % 0.26/0.33 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.64/1.63 % (1834111)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.64/1.63 % (1834133)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2363476686:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.64/1.63 % (1834135)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=8328327:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.64/1.63 % (1834133)Instruction limit reached! % 5.64/1.63 % (1834133)------------------------------ % 5.64/1.63 % (1834133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.63 % (1834133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.63 % (1834133)CaDiCaL version: 2.1.3 % 5.64/1.63 % (1834133)Termination reason: Instruction limit % 5.64/1.63 % (1834133)Termination phase: Saturation % 5.64/1.63 % (1834133)Time elapsed: 0.004 s % 5.64/1.63 % (1834133)Peak memory usage: 88 MB % 5.64/1.63 % (1834133)Instructions burned: 7 (million) % 5.64/1.63 % (1834135)Instruction limit reached! % 5.64/1.63 % (1834135)------------------------------ % 5.64/1.63 % (1834135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.63 % (1834135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.63 % (1834135)CaDiCaL version: 2.1.3 % 5.64/1.63 % (1834135)Termination reason: Instruction limit % 5.64/1.63 % (1834135)Termination phase: Saturation % 5.64/1.63 % (1834135)Time elapsed: 0.061 s % 5.64/1.63 % (1834135)Peak memory usage: 116 MB % 5.64/1.63 % (1834135)Instructions burned: 47 (million) % 5.64/1.63 % (1834132)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1941947652:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.64/1.63 % (1834131)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3900322293:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.64/1.63 % (1834130)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=756360576:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.64/1.63 % (1834136)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3670168276:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.64/1.63 % (1834134)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1563740961:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.64/1.63 % (1834134)Instruction limit reached! % 5.64/1.63 % (1834134)------------------------------ % 5.64/1.63 % (1834134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.63 % (1834134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.63 % (1834134)CaDiCaL version: 2.1.3 % 5.64/1.63 % (1834134)Termination reason: Instruction limit % 5.64/1.63 % (1834134)Termination phase: Property scanning % 5.64/1.63 % (1834134)Time elapsed: 0.005 s % 5.64/1.63 % (1834134)Peak memory usage: 86 MB % 5.64/1.63 % (1834134)Instructions burned: 4 (million) % 5.64/1.63 % (1834130)Instruction limit reached! % 5.64/1.63 % (1834130)------------------------------ % 5.64/1.63 % (1834130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.63 % (1834130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.63 % (1834130)CaDiCaL version: 2.1.3 % 5.64/1.63 % (1834130)Termination reason: Instruction limit % 5.64/1.63 % (1834130)Termination phase: Saturation % 5.64/1.63 % (1834130)Time elapsed: 0.042 s % 5.64/1.63 % (1834130)Peak memory usage: 114 MB % 5.64/1.63 % (1834130)Instructions burned: 12 (million) % 5.64/1.63 % (1834136)Instruction limit reached! % 5.64/1.63 % (1834136)------------------------------ % 5.64/1.63 % (1834136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.64/1.63 % (1834136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.64/1.63 % (1834136)CaDiCaL version: 2.1.3 % 5.64/1.63 % (1834136)Termination reason: Instruction limit % 5.64/1.63 % (1834136)Termination phase: Saturation % 5.64/1.63 % (1834136)Time elapsed: 0.067 s % 5.64/1.63 % (1834136)Peak memory usage: 116 MB % 5.64/1.63 % (1834136)Instructions burned: 33 (million) % 5.64/1.63 % (1834139)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1720205187:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 5.64/1.63 % (1834139)Instruction limit reached! % 5.64/1.63 % (1834139)------------------------------ % 7.11/1.88 % (1834139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.88 % (1834139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.88 % (1834139)CaDiCaL version: 2.1.3 % 7.11/1.88 % (1834139)Termination reason: Instruction limit % 7.11/1.88 % (1834139)Termination phase: Saturation % 7.11/1.88 % (1834139)Time elapsed: 0.010 s % 7.11/1.88 % (1834139)Peak memory usage: 89 MB % 7.11/1.88 % (1834139)Instructions burned: 15 (million) % 7.11/1.88 % (1834132)Instruction limit reached! % 7.11/1.88 % (1834132)------------------------------ % 7.11/1.88 % (1834132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.88 % (1834132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.88 % (1834132)CaDiCaL version: 2.1.3 % 7.11/1.88 % (1834132)Termination reason: Instruction limit % 7.11/1.88 % (1834132)Termination phase: Saturation % 7.11/1.88 % (1834132)Time elapsed: 0.194 s % 7.11/1.88 % (1834132)Peak memory usage: 114 MB % 7.11/1.88 % (1834132)Instructions burned: 201 (million) % 7.11/1.88 % (1834140)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=1349977314:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 7.11/1.88 % (1834146)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1507376921:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 7.11/1.88 % (1834146)Instruction limit reached! % 7.11/1.88 % (1834146)------------------------------ % 7.11/1.88 % (1834146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.88 % (1834146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.88 % (1834146)CaDiCaL version: 2.1.3 % 7.11/1.88 % (1834146)Termination reason: Instruction limit % 7.11/1.88 % (1834146)Termination phase: Saturation % 7.11/1.88 % (1834146)Time elapsed: 0.018 s % 7.11/1.88 % (1834146)Peak memory usage: 88 MB % 7.11/1.88 % (1834146)Instructions burned: 16 (million) % 7.11/1.88 % (1834140)Instruction limit reached! % 7.11/1.88 % (1834140)------------------------------ % 7.11/1.88 % (1834140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.88 % (1834140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.88 % (1834140)CaDiCaL version: 2.1.3 % 7.11/1.88 % (1834140)Termination reason: Instruction limit % 7.11/1.88 % (1834140)Termination phase: Saturation % 7.11/1.88 % (1834140)Time elapsed: 0.033 s % 7.11/1.88 % (1834140)Peak memory usage: 89 MB % 7.11/1.88 % (1834140)Instructions burned: 29 (million) % 7.11/1.88 % (1834147)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1227304047:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 7.11/1.88 % (1834150)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=817329108:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 7.11/1.88 % (1834148)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=3973243027:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 7.11/1.88 % (1834147)Instruction limit reached! % 7.11/1.88 % (1834147)------------------------------ % 7.11/1.88 % (1834147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.88 % (1834147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.88 % (1834147)CaDiCaL version: 2.1.3 % 7.11/1.88 % (1834147)Termination reason: Instruction limit % 7.11/1.88 % (1834147)Termination phase: Saturation % 7.11/1.88 % (1834147)Time elapsed: 0.031 s % 7.11/1.88 % (1834147)Peak memory usage: 89 MB % 7.11/1.88 % (1834147)Instructions burned: 24 (million) % 7.11/1.88 % (1834148)Instruction limit reached! % 7.11/1.88 % (1834148)------------------------------ % 7.11/1.88 % (1834148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.11/1.88 % (1834148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.11/1.88 % (1834148)CaDiCaL version: 2.1.3 % 7.11/1.88 % (1834148)Termination reason: Instruction limit % 7.11/1.88 % (1834148)Termination phase: Saturation % 7.11/1.88 % (1834148)Time elapsed: 0.029 s % 7.11/1.88 % (1834148)Peak memory usage: 90 MB % 7.11/1.88 % (1834148)Instructions burned: 28 (million) % 7.11/1.88 % (1834131)Instruction limit reached! % 7.11/1.88 % (1834131)------------------------------ % 7.11/1.88 % (1834131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.20 % (1834131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.20 % (1834131)CaDiCaL version: 2.1.3 % 10.29/2.20 % (1834131)Termination reason: Instruction limit % 10.29/2.20 % (1834131)Termination phase: Saturation % 10.29/2.20 % (1834131)Time elapsed: 0.359 s % 10.29/2.20 % (1834131)Peak memory usage: 118 MB % 10.29/2.20 % (1834131)Instructions burned: 307 (million) % 10.29/2.20 % (1834150)Instruction limit reached! % 10.29/2.20 % (1834150)------------------------------ % 10.29/2.20 % (1834150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.20 % (1834150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.20 % (1834150)CaDiCaL version: 2.1.3 % 10.29/2.20 % (1834150)Termination reason: Instruction limit % 10.29/2.20 % (1834150)Termination phase: Saturation % 10.29/2.20 % (1834150)Time elapsed: 0.043 s % 10.29/2.20 % (1834150)Peak memory usage: 89 MB % 10.29/2.20 % (1834150)Instructions burned: 87 (million) % 10.29/2.20 % (1834154)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4053232865:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 10.29/2.20 % (1834151)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4240540604:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 10.29/2.20 % (1834151)Instruction limit reached! % 10.29/2.20 % (1834151)------------------------------ % 10.29/2.20 % (1834151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.20 % (1834151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.20 % (1834151)CaDiCaL version: 2.1.3 % 10.29/2.20 % (1834151)Termination reason: Instruction limit % 10.29/2.20 % (1834151)Termination phase: Preprocessing 3 % 10.29/2.20 % (1834151)Time elapsed: 0.003 s % 10.29/2.20 % (1834151)Peak memory usage: 86 MB % 10.29/2.20 % (1834151)Instructions burned: 2 (million) % 10.29/2.20 % (1834155)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4155816795:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 10.29/2.20 % (1834155)Instruction limit reached! % 10.29/2.20 % (1834155)------------------------------ % 10.29/2.20 % (1834155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.20 % (1834155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.20 % (1834155)CaDiCaL version: 2.1.3 % 10.29/2.20 % (1834155)Termination reason: Instruction limit % 10.29/2.20 % (1834155)Termination phase: Property scanning % 10.29/2.20 % (1834155)Time elapsed: 0.005 s % 10.29/2.20 % (1834155)Peak memory usage: 87 MB % 10.29/2.20 % (1834155)Instructions burned: 4 (million) % 10.29/2.20 % (1834161)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=1447784763:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 10.29/2.20 % (1834161)Instruction limit reached! % 10.29/2.20 % (1834161)------------------------------ % 10.29/2.20 % (1834161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.20 % (1834161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.20 % (1834161)CaDiCaL version: 2.1.3 % 10.29/2.20 % (1834161)Termination reason: Instruction limit % 10.29/2.20 % (1834161)Termination phase: Saturation % 10.29/2.20 % (1834161)Time elapsed: 0.005 s % 10.29/2.20 % (1834161)Peak memory usage: 88 MB % 10.29/2.20 % (1834161)Instructions burned: 9 (million) % 10.29/2.20 % (1834154)Instruction limit reached! % 10.29/2.20 % (1834154)------------------------------ % 10.29/2.20 % (1834154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.20 % (1834154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.20 % (1834154)CaDiCaL version: 2.1.3 % 10.29/2.20 % (1834154)Termination reason: Instruction limit % 10.29/2.20 % (1834154)Termination phase: Saturation % 10.29/2.20 % (1834154)Time elapsed: 0.145 s % 10.29/2.20 % (1834154)Peak memory usage: 90 MB % 10.29/2.20 % (1834154)Instructions burned: 181 (million) % 10.29/2.20 % (1834159)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2982649555:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 10.29/2.20 % (1834160)lrs+10_1_thi=all:si=on:fd=off:random_seed=847433944:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 10.29/2.20 % (1834162)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2664359230:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 11.57/2.55 % (1834162)Instruction limit reached! % 11.57/2.55 % (1834162)------------------------------ % 11.57/2.55 % (1834162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.55 % (1834162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.55 % (1834162)CaDiCaL version: 2.1.3 % 11.57/2.55 % (1834162)Termination reason: Instruction limit % 11.57/2.55 % (1834162)Termination phase: Clausification % 11.57/2.55 % (1834162)Time elapsed: 0.004 s % 11.57/2.55 % (1834162)Peak memory usage: 86 MB % 11.57/2.55 % (1834162)Instructions burned: 3 (million) % 11.57/2.55 % (1834160)Instruction limit reached! % 11.57/2.55 % (1834160)------------------------------ % 11.57/2.55 % (1834160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.55 % (1834160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.55 % (1834160)CaDiCaL version: 2.1.3 % 11.57/2.55 % (1834160)Termination reason: Instruction limit % 11.57/2.55 % (1834160)Termination phase: Saturation % 11.57/2.55 % (1834160)Time elapsed: 0.092 s % 11.57/2.55 % (1834160)Peak memory usage: 117 MB % 11.57/2.55 % (1834160)Instructions burned: 53 (million) % 11.57/2.55 % (1834165)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1226918509:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 11.57/2.55 % (1834165)Instruction limit reached! % 11.57/2.55 % (1834165)------------------------------ % 11.57/2.55 % (1834165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.55 % (1834165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.55 % (1834165)CaDiCaL version: 2.1.3 % 11.57/2.55 % (1834165)Termination reason: Instruction limit % 11.57/2.55 % (1834165)Termination phase: Preprocessing 3 % 11.57/2.55 % (1834165)Time elapsed: 0.003 s % 11.57/2.55 % (1834165)Peak memory usage: 86 MB % 11.57/2.55 % (1834165)Instructions burned: 2 (million) % 11.57/2.55 % (1834159)Instruction limit reached! % 11.57/2.55 % (1834159)------------------------------ % 11.57/2.55 % (1834159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.55 % (1834159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.55 % (1834159)CaDiCaL version: 2.1.3 % 11.57/2.55 % (1834159)Termination reason: Instruction limit % 11.57/2.55 % (1834159)Termination phase: Saturation % 11.57/2.55 % (1834159)Time elapsed: 0.137 s % 11.57/2.55 % (1834159)Peak memory usage: 134 MB % 11.57/2.55 % (1834159)Instructions burned: 66 (million) % 11.57/2.55 % (1834169)dis+10_1_si=on:random_seed=3382206791:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 11.57/2.55 % (1834169)Instruction limit reached! % 11.57/2.55 % (1834169)------------------------------ % 11.57/2.55 % (1834169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.55 % (1834169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.55 % (1834169)CaDiCaL version: 2.1.3 % 11.57/2.55 % (1834169)Termination reason: Instruction limit % 11.57/2.55 % (1834169)Termination phase: Saturation % 11.57/2.55 % (1834169)Time elapsed: 0.007 s % 11.57/2.55 % (1834169)Peak memory usage: 88 MB % 11.57/2.55 % (1834169)Instructions burned: 11 (million) % 11.57/2.55 % (1834167)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2637656833:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 11.57/2.55 % (1834171)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1834580758:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 11.57/2.55 % (1834171)Refutation not found, incomplete strategy % 11.57/2.55 % (1834171)------------------------------ % 11.57/2.55 % (1834171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.55 % (1834171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.55 % (1834171)CaDiCaL version: 2.1.3 % 11.57/2.55 % (1834171)Termination reason: Refutation not found, incomplete strategy % 11.57/2.55 % (1834171)Time elapsed: 0.010 s % 11.57/2.55 % (1834171)Peak memory usage: 89 MB % 11.57/2.55 % (1834171)Instructions burned: 8 (million) % 11.57/2.55 % (1834174)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4035312436: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_2991 on theBenchmark for (2991ds/35Mi) % 13.16/2.89 % (1834178)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3732625154:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 13.16/2.89 % (1834177)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=58645311:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 13.16/2.89 % (1834176)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=149379857:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 13.16/2.89 % (1834174)Instruction limit reached! % 13.16/2.89 % (1834174)------------------------------ % 13.16/2.89 % (1834174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.89 % (1834174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.89 % (1834174)CaDiCaL version: 2.1.3 % 13.16/2.89 % (1834174)Termination reason: Instruction limit % 13.16/2.89 % (1834174)Termination phase: Saturation % 13.16/2.89 % (1834174)Time elapsed: 0.042 s % 13.16/2.89 % (1834174)Peak memory usage: 89 MB % 13.16/2.89 % (1834174)Instructions burned: 35 (million) % 13.16/2.89 % (1834176)Instruction limit reached! % 13.16/2.89 % (1834176)------------------------------ % 13.16/2.89 % (1834176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.89 % (1834176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.89 % (1834176)CaDiCaL version: 2.1.3 % 13.16/2.89 % (1834176)Termination reason: Instruction limit % 13.16/2.89 % (1834176)Termination phase: Preprocessing 3 % 13.16/2.89 % (1834176)Time elapsed: 0.003 s % 13.16/2.89 % (1834176)Peak memory usage: 86 MB % 13.16/2.89 % (1834176)Instructions burned: 2 (million) % 13.16/2.89 % (1834177)Instruction limit reached! % 13.16/2.89 % (1834177)------------------------------ % 13.16/2.89 % (1834177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.89 % (1834177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.89 % (1834177)CaDiCaL version: 2.1.3 % 13.16/2.89 % (1834177)Termination reason: Instruction limit % 13.16/2.89 % (1834177)Termination phase: Saturation % 13.16/2.89 % (1834177)Time elapsed: 0.009 s % 13.16/2.89 % (1834177)Peak memory usage: 88 MB % 13.16/2.89 % (1834177)Instructions burned: 8 (million) % 13.16/2.89 % (1834180)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2039324721:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 13.16/2.89 % (1834167)Instruction limit reached! % 13.16/2.89 % (1834167)------------------------------ % 13.16/2.89 % (1834167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.89 % (1834167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.89 % (1834167)CaDiCaL version: 2.1.3 % 13.16/2.89 % (1834167)Termination reason: Instruction limit % 13.16/2.89 % (1834167)Termination phase: Saturation % 13.16/2.89 % (1834167)Time elapsed: 0.177 s % 13.16/2.89 % (1834167)Peak memory usage: 117 MB % 13.16/2.89 % (1834167)Instructions burned: 127 (million) % 13.16/2.89 % (1834180)Instruction limit reached! % 13.16/2.89 % (1834180)------------------------------ % 13.16/2.89 % (1834180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.89 % (1834180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.16/2.89 % (1834180)CaDiCaL version: 2.1.3 % 13.16/2.89 % (1834180)Termination reason: Instruction limit % 13.16/2.89 % (1834180)Termination phase: Saturation % 13.16/2.89 % (1834180)Time elapsed: 0.024 s % 13.16/2.89 % (1834180)Peak memory usage: 112 MB % 13.16/2.89 % (1834180)Instructions burned: 14 (million) % 13.16/2.89 % (1834189)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2830405902:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 13.16/2.89 % (1834187)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=395933422:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 13.16/2.89 % (1834188)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1215834224:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 13.16/2.89 % (1834188)Instruction limit reached! % 13.16/2.89 % (1834188)------------------------------ % 13.16/2.89 % (1834188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.16/2.89 % (1834188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.33 % (1834188)CaDiCaL version: 2.1.3 % 17.90/3.33 % (1834188)Termination reason: Instruction limit % 17.90/3.33 % (1834188)Termination phase: Saturation % 17.90/3.33 % (1834188)Time elapsed: 0.012 s % 17.90/3.33 % (1834188)Peak memory usage: 88 MB % 17.90/3.33 % (1834188)Instructions burned: 10 (million) % 17.90/3.33 % (1834192)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=3076094237:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 17.90/3.33 % (1834171)------------------------------ % 17.90/3.33 % (1834171)------------------------------ % 17.90/3.33 % (1834178)Instruction limit reached! % 17.90/3.33 % (1834178)------------------------------ % 17.90/3.33 % (1834178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.33 % (1834178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.33 % (1834178)CaDiCaL version: 2.1.3 % 17.90/3.33 % (1834178)Termination reason: Instruction limit % 17.90/3.33 % (1834178)Termination phase: Saturation % 17.90/3.33 % (1834178)Time elapsed: 0.337 s % 17.90/3.33 % (1834178)Peak memory usage: 97 MB % 17.90/3.33 % (1834178)Instructions burned: 370 (million) % 17.90/3.33 % (1834191)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=483818778:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 17.90/3.33 % (1834189)Instruction limit reached! % 17.90/3.33 % (1834189)------------------------------ % 17.90/3.33 % (1834189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.33 % (1834189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.33 % (1834189)CaDiCaL version: 2.1.3 % 17.90/3.33 % (1834189)Termination reason: Instruction limit % 17.90/3.33 % (1834189)Termination phase: Saturation % 17.90/3.33 % (1834189)Time elapsed: 0.141 s % 17.90/3.33 % (1834189)Peak memory usage: 134 MB % 17.90/3.33 % (1834189)Instructions burned: 71 (million) % 17.90/3.33 % (1834191)Instruction limit reached! % 17.90/3.33 % (1834191)------------------------------ % 17.90/3.33 % (1834191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.33 % (1834191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.33 % (1834191)CaDiCaL version: 2.1.3 % 17.90/3.33 % (1834191)Termination reason: Instruction limit % 17.90/3.33 % (1834191)Termination phase: Saturation % 17.90/3.33 % (1834191)Time elapsed: 0.080 s % 17.90/3.33 % (1834191)Peak memory usage: 90 MB % 17.90/3.33 % (1834191)Instructions burned: 75 (million) % 17.90/3.33 % (1834192)Instruction limit reached! % 17.90/3.33 % (1834192)------------------------------ % 17.90/3.33 % (1834192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.33 % (1834192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.33 % (1834192)CaDiCaL version: 2.1.3 % 17.90/3.33 % (1834192)Termination reason: Instruction limit % 17.90/3.33 % (1834192)Termination phase: Saturation % 17.90/3.33 % (1834192)Time elapsed: 0.157 s % 17.90/3.33 % (1834192)Peak memory usage: 91 MB % 17.90/3.33 % (1834192)Instructions burned: 295 (million) % 17.90/3.33 % (1834197)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=519344352:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi) % 17.90/3.33 % (1834187)Instruction limit reached! % 17.90/3.33 % (1834187)------------------------------ % 17.90/3.33 % (1834187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.33 % (1834187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.33 % (1834187)CaDiCaL version: 2.1.3 % 17.90/3.33 % (1834187)Termination reason: Instruction limit % 17.90/3.33 % (1834187)Termination phase: Saturation % 17.90/3.33 % (1834187)Time elapsed: 0.264 s % 17.90/3.33 % (1834187)Peak memory usage: 119 MB % 17.90/3.33 % (1834187)Instructions burned: 226 (million) % 17.90/3.33 % (1834198)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3632515799:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 17.90/3.33 % (1834199)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3359043102:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 17.90/3.33 % (1834201)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2178579719:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 17.90/3.33 % (1834203)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=261282041:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 20.35/3.82 % (1834199)Instruction limit reached! % 20.35/3.82 % (1834199)------------------------------ % 20.35/3.82 % (1834199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.35/3.82 % (1834199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.35/3.82 % (1834199)CaDiCaL version: 2.1.3 % 20.35/3.82 % (1834199)Termination reason: Instruction limit % 20.35/3.82 % (1834199)Termination phase: Saturation % 20.35/3.82 % (1834199)Time elapsed: 0.098 s % 20.35/3.82 % (1834199)Peak memory usage: 134 MB % 20.35/3.82 % (1834199)Instructions burned: 40 (million) % 20.35/3.82 % (1834202)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1934487560:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 20.35/3.82 % (1834197)Instruction limit reached! % 20.35/3.82 % (1834197)------------------------------ % 20.35/3.82 % (1834197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.35/3.82 % (1834197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.35/3.82 % (1834197)CaDiCaL version: 2.1.3 % 20.35/3.82 % (1834197)Termination reason: Instruction limit % 20.35/3.82 % (1834197)Termination phase: Saturation % 20.35/3.82 % (1834197)Time elapsed: 0.178 s % 20.35/3.82 % (1834197)Peak memory usage: 119 MB % 20.35/3.82 % (1834197)Instructions burned: 130 (million) % 20.35/3.82 % (1834205)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=555488727:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 20.35/3.82 % (1834198)Instruction limit reached! % 20.35/3.82 % (1834198)------------------------------ % 20.35/3.82 % (1834198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.35/3.82 % (1834198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.35/3.82 % (1834198)CaDiCaL version: 2.1.3 % 20.35/3.82 % (1834198)Termination reason: Instruction limit % 20.35/3.82 % (1834198)Termination phase: Saturation % 20.35/3.82 % (1834198)Time elapsed: 0.201 s % 20.35/3.82 % (1834198)Peak memory usage: 135 MB % 20.35/3.82 % (1834198)Instructions burned: 131 (million) % 20.35/3.82 % (1834203)Instruction limit reached! % 20.35/3.82 % (1834203)------------------------------ % 20.35/3.82 % (1834203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.35/3.82 % (1834203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.35/3.82 % (1834203)CaDiCaL version: 2.1.3 % 20.35/3.82 % (1834203)Termination reason: Instruction limit % 20.35/3.82 % (1834203)Termination phase: Saturation % 20.35/3.82 % (1834203)Time elapsed: 0.154 s % 20.35/3.82 % (1834203)Peak memory usage: 118 MB % 20.35/3.82 % (1834203)Instructions burned: 131 (million) % 20.35/3.82 % (1834205)Instruction limit reached! % 20.35/3.82 % (1834205)------------------------------ % 20.35/3.82 % (1834205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.35/3.82 % (1834205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.35/3.82 % (1834205)CaDiCaL version: 2.1.3 % 20.35/3.82 % (1834205)Termination reason: Instruction limit % 20.35/3.82 % (1834205)Termination phase: Saturation % 20.35/3.82 % (1834205)Time elapsed: 0.159 s % 20.35/3.82 % (1834205)Peak memory usage: 119 MB % 20.35/3.82 % (1834205)Instructions burned: 260 (million) % 20.35/3.82 % (1834214)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3396679178:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 20.35/3.82 % (1834211)dis+10_1_si=on:random_seed=3307248227:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 20.35/3.82 % (1834201)Instruction limit reached! % 20.35/3.82 % (1834201)------------------------------ % 20.35/3.82 % (1834201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.35/3.82 % (1834201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.35/3.82 % (1834201)CaDiCaL version: 2.1.3 % 20.35/3.82 % (1834201)Termination reason: Instruction limit % 20.35/3.82 % (1834201)Termination phase: Saturation % 20.35/3.82 % (1834201)Time elapsed: 0.330 s % 20.35/3.82 % (1834201)Peak memory usage: 92 MB % 20.35/3.82 % (1834201)Instructions burned: 307 (million) % 20.35/3.82 % (1834212)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2354293237:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 24.90/4.32 % (1834214)Instruction limit reached! % 24.90/4.32 % (1834214)------------------------------ % 24.90/4.32 % (1834214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.90/4.32 % (1834214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/4.32 % (1834214)CaDiCaL version: 2.1.3 % 24.90/4.32 % (1834214)Termination reason: Instruction limit % 24.90/4.32 % (1834214)Termination phase: Saturation % 24.90/4.32 % (1834214)Time elapsed: 0.078 s % 24.90/4.32 % (1834214)Peak memory usage: 90 MB % 24.90/4.32 % (1834214)Instructions burned: 141 (million) % 24.90/4.32 % (1834215)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3092192524:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 24.90/4.32 % (1834216)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1364324559:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 24.90/4.32 % (1834215)Instruction limit reached! % 24.90/4.32 % (1834215)------------------------------ % 24.90/4.32 % (1834215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.90/4.32 % (1834215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/4.32 % (1834215)CaDiCaL version: 2.1.3 % 24.90/4.32 % (1834215)Termination reason: Instruction limit % 24.90/4.32 % (1834215)Termination phase: Saturation % 24.90/4.32 % (1834215)Time elapsed: 0.098 s % 24.90/4.32 % (1834215)Peak memory usage: 118 MB % 24.90/4.32 % (1834215)Instructions burned: 65 (million) % 24.90/4.32 % (1834219)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=3772178379:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 24.90/4.32 % (1834216)Instruction limit reached! % 24.90/4.32 % (1834216)------------------------------ % 24.90/4.32 % (1834216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.90/4.32 % (1834216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/4.32 % (1834216)CaDiCaL version: 2.1.3 % 24.90/4.32 % (1834216)Termination reason: Instruction limit % 24.90/4.32 % (1834216)Termination phase: Saturation % 24.90/4.32 % (1834216)Time elapsed: 0.132 s % 24.90/4.32 % (1834216)Peak memory usage: 89 MB % 24.90/4.32 % (1834216)Instructions burned: 121 (million) % 24.90/4.32 % (1834221)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=1727408770:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi) % 24.90/4.32 % (1834221)Instruction limit reached! % 24.90/4.32 % (1834221)------------------------------ % 24.90/4.32 % (1834221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.90/4.32 % (1834221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/4.32 % (1834221)CaDiCaL version: 2.1.3 % 24.90/4.32 % (1834221)Termination reason: Instruction limit % 24.90/4.32 % (1834221)Termination phase: Saturation % 24.90/4.32 % (1834221)Time elapsed: 0.040 s % 24.90/4.32 % (1834221)Peak memory usage: 116 MB % 24.90/4.32 % (1834221)Instructions burned: 40 (million) % 24.90/4.32 % (1834212)Instruction limit reached! % 24.90/4.32 % (1834212)------------------------------ % 24.90/4.32 % (1834212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.90/4.32 % (1834212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/4.32 % (1834212)CaDiCaL version: 2.1.3 % 24.90/4.32 % (1834212)Termination reason: Instruction limit % 24.90/4.32 % (1834212)Termination phase: Saturation % 24.90/4.32 % (1834212)Time elapsed: 0.330 s % 24.90/4.32 % (1834212)Peak memory usage: 91 MB % 24.90/4.32 % (1834212)Instructions burned: 383 (million) % 24.90/4.32 % (1834219)Instruction limit reached! % 24.90/4.32 % (1834219)------------------------------ % 24.90/4.32 % (1834219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.90/4.32 % (1834219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.90/4.32 % (1834219)CaDiCaL version: 2.1.3 % 24.90/4.32 % (1834219)Termination reason: Instruction limit % 24.90/4.32 % (1834219)Termination phase: Saturation % 24.90/4.32 % (1834219)Time elapsed: 0.169 s % 24.90/4.32 % (1834219)Peak memory usage: 119 MB % 24.90/4.32 % (1834219)Instructions burned: 128 (million) % 24.90/4.32 % (1834224)dis+1010_1_to=kbo:si=on:random_seed=915278620:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 24.90/4.32 % (1834202)Instruction limit reached! % 24.90/4.32 % (1834202)------------------------------ % 26.39/4.75 % (1834202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.39/4.75 % (1834202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.39/4.75 % (1834202)CaDiCaL version: 2.1.3 % 26.39/4.75 % (1834202)Termination reason: Instruction limit % 26.39/4.75 % (1834202)Termination phase: Saturation % 26.39/4.75 % (1834202)Time elapsed: 0.713 s % 26.39/4.75 % (1834202)Peak memory usage: 139 MB % 26.39/4.75 % (1834202)Instructions burned: 598 (million) % 26.39/4.75 % (1834228)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3486394454:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi) % 26.39/4.75 % (1834226)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3542626188:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi) % 26.39/4.75 % (1834229)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4017516074:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi) % 26.39/4.75 % (1834224)Instruction limit reached! % 26.39/4.75 % (1834224)------------------------------ % 26.39/4.75 % (1834224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.39/4.75 % (1834224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.39/4.75 % (1834224)CaDiCaL version: 2.1.3 % 26.39/4.75 % (1834224)Termination reason: Instruction limit % 26.39/4.75 % (1834224)Termination phase: Saturation % 26.39/4.75 % (1834224)Time elapsed: 0.132 s % 26.39/4.75 % (1834224)Peak memory usage: 91 MB % 26.39/4.75 % (1834224)Instructions burned: 175 (million) % 26.39/4.75 % (1834231)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3473511042:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi) % 26.39/4.75 % (1834232)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1544059144:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi) % 26.39/4.75 % (1834229)Instruction limit reached! % 26.39/4.75 % (1834229)------------------------------ % 26.39/4.75 % (1834229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.39/4.75 % (1834229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.39/4.75 % (1834229)CaDiCaL version: 2.1.3 % 26.39/4.75 % (1834229)Termination reason: Instruction limit % 26.39/4.75 % (1834229)Termination phase: Saturation % 26.39/4.75 % (1834229)Time elapsed: 0.242 s % 26.39/4.75 % (1834229)Peak memory usage: 135 MB % 26.39/4.75 % (1834229)Instructions burned: 215 (million) % 26.39/4.75 % (1834226)Instruction limit reached! % 26.39/4.75 % (1834226)------------------------------ % 26.39/4.75 % (1834226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.39/4.75 % (1834226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.39/4.75 % (1834226)CaDiCaL version: 2.1.3 % 26.39/4.75 % (1834226)Termination reason: Instruction limit % 26.39/4.75 % (1834226)Termination phase: Saturation % 26.39/4.75 % (1834226)Time elapsed: 0.286 s % 26.39/4.75 % (1834226)Peak memory usage: 114 MB % 26.39/4.75 % (1834226)Instructions burned: 329 (million) % 26.39/4.75 % (1834228)Instruction limit reached! % 26.39/4.75 % (1834228)------------------------------ % 26.39/4.75 % (1834228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.39/4.75 % (1834228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.39/4.75 % (1834228)CaDiCaL version: 2.1.3 % 26.39/4.75 % (1834228)Termination reason: Instruction limit % 26.39/4.75 % (1834228)Termination phase: Saturation % 26.39/4.75 % (1834228)Time elapsed: 0.302 s % 26.39/4.75 % (1834228)Peak memory usage: 136 MB % 26.39/4.75 % (1834228)Instructions burned: 483 (million) % 26.39/4.75 % (1834238)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1493792970:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi) % 26.39/4.75 % (1834211)Instruction limit reached! % 26.39/4.75 % (1834211)------------------------------ % 26.39/4.75 % (1834211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.39/4.75 % (1834211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.39/4.75 % (1834211)CaDiCaL version: 2.1.3 % 26.39/4.75 % (1834211)Termination reason: Instruction limit % 26.39/4.75 % (1834211)Termination phase: Saturation % 26.39/4.75 % (1834211)Time elapsed: 0.941 s % 26.39/4.75 % (1834211)Peak memory usage: 98 MB % 30.94/5.22 % (1834211)Instructions burned: 1000 (million) % 30.94/5.22 % (1834241)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=577482831:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi) % 30.94/5.22 % (1834243)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2458329249:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi) % 30.94/5.22 % (1834232)Instruction limit reached! % 30.94/5.22 % (1834232)------------------------------ % 30.94/5.22 % (1834232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.94/5.22 % (1834232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.94/5.22 % (1834232)CaDiCaL version: 2.1.3 % 30.94/5.22 % (1834232)Termination reason: Instruction limit % 30.94/5.22 % (1834232)Termination phase: Saturation % 30.94/5.22 % (1834232)Time elapsed: 0.279 s % 30.94/5.22 % (1834232)Peak memory usage: 91 MB % 30.94/5.22 % (1834232)Instructions burned: 296 (million) % 30.94/5.22 % (1834231)Instruction limit reached! % 30.94/5.22 % (1834231)------------------------------ % 30.94/5.22 % (1834231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.94/5.22 % (1834231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.94/5.22 % (1834231)CaDiCaL version: 2.1.3 % 30.94/5.22 % (1834231)Termination reason: Instruction limit % 30.94/5.22 % (1834231)Termination phase: Saturation % 30.94/5.22 % (1834231)Time elapsed: 0.356 s % 30.94/5.22 % (1834231)Peak memory usage: 117 MB % 30.94/5.22 % (1834231)Instructions burned: 350 (million) % 30.94/5.22 % (1834242)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1457602210:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi) % 30.94/5.22 % (1834245)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1984814562:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi) % 30.94/5.22 % (1834243)Instruction limit reached! % 30.94/5.22 % (1834243)------------------------------ % 30.94/5.22 % (1834243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.94/5.22 % (1834243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.94/5.22 % (1834243)CaDiCaL version: 2.1.3 % 30.94/5.22 % (1834243)Termination reason: Instruction limit % 30.94/5.22 % (1834243)Termination phase: Saturation % 30.94/5.22 % (1834243)Time elapsed: 0.166 s % 30.94/5.22 % (1834243)Peak memory usage: 116 MB % 30.94/5.22 % (1834243)Instructions burned: 321 (million) % 30.94/5.22 % (1834238)Instruction limit reached! % 30.94/5.22 % (1834238)------------------------------ % 30.94/5.22 % (1834238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.94/5.22 % (1834238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.94/5.22 % (1834238)CaDiCaL version: 2.1.3 % 30.94/5.22 % (1834238)Termination reason: Instruction limit % 30.94/5.22 % (1834238)Termination phase: Saturation % 30.94/5.22 % (1834238)Time elapsed: 0.354 s % 30.94/5.22 % (1834238)Peak memory usage: 119 MB % 30.94/5.22 % (1834238)Instructions burned: 328 (million) % 30.94/5.22 % (1834248)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1879364809:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi) % 30.94/5.22 % (1834241)Instruction limit reached! % 30.94/5.22 % (1834241)------------------------------ % 30.94/5.22 % (1834241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.94/5.22 % (1834241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.94/5.22 % (1834241)CaDiCaL version: 2.1.3 % 30.94/5.22 % (1834241)Termination reason: Instruction limit % 30.94/5.22 % (1834241)Termination phase: Saturation % 30.94/5.22 % (1834241)Time elapsed: 0.309 s % 30.94/5.22 % (1834241)Peak memory usage: 118 MB % 30.94/5.22 % (1834241)Instructions burned: 281 (million) % 30.94/5.22 % (1834249)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=2584017797:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi) % 30.94/5.22 % (1834252)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=228902259:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 30.94/5.22 % (1834253)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2830349066:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi) % 37.66/6.06 % (1834242)Instruction limit reached! % 37.66/6.06 % (1834242)------------------------------ % 37.66/6.06 % (1834242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834242)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834242)Termination reason: Instruction limit % 37.66/6.06 % (1834242)Termination phase: Saturation % 37.66/6.06 % (1834242)Time elapsed: 0.443 s % 37.66/6.06 % (1834242)Peak memory usage: 92 MB % 37.66/6.06 % (1834242)Instructions burned: 484 (million) % 37.66/6.06 % (1834255)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=811423939:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi) % 37.66/6.06 % (1834245)Instruction limit reached! % 37.66/6.06 % (1834245)------------------------------ % 37.66/6.06 % (1834245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834245)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834245)Termination reason: Instruction limit % 37.66/6.06 % (1834245)Termination phase: Saturation % 37.66/6.06 % (1834245)Time elapsed: 0.420 s % 37.66/6.06 % (1834245)Peak memory usage: 119 MB % 37.66/6.06 % (1834245)Instructions burned: 416 (million) % 37.66/6.06 % (1834249)Instruction limit reached! % 37.66/6.06 % (1834249)------------------------------ % 37.66/6.06 % (1834249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834249)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834249)Termination reason: Instruction limit % 37.66/6.06 % (1834249)Termination phase: Saturation % 37.66/6.06 % (1834249)Time elapsed: 0.337 s % 37.66/6.06 % (1834249)Peak memory usage: 137 MB % 37.66/6.06 % (1834249)Instructions burned: 276 (million) % 37.66/6.06 % (1834260)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1263066697:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi) % 37.66/6.06 % (1834248)Instruction limit reached! % 37.66/6.06 % (1834248)------------------------------ % 37.66/6.06 % (1834248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834248)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834248)Termination reason: Instruction limit % 37.66/6.06 % (1834248)Termination phase: Saturation % 37.66/6.06 % (1834248)Time elapsed: 0.517 s % 37.66/6.06 % (1834248)Peak memory usage: 122 MB % 37.66/6.06 % (1834248)Instructions burned: 471 (million) % 37.66/6.06 % (1834255)Instruction limit reached! % 37.66/6.06 % (1834255)------------------------------ % 37.66/6.06 % (1834255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834255)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834255)Termination reason: Instruction limit % 37.66/6.06 % (1834255)Termination phase: Saturation % 37.66/6.06 % (1834255)Time elapsed: 0.269 s % 37.66/6.06 % (1834255)Peak memory usage: 93 MB % 37.66/6.06 % (1834255)Instructions burned: 515 (million) % 37.66/6.06 % (1834261)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3416948117:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 37.66/6.06 % (1834253)Instruction limit reached! % 37.66/6.06 % (1834253)------------------------------ % 37.66/6.06 % (1834253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834253)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834253)Termination reason: Instruction limit % 37.66/6.06 % (1834253)Termination phase: Saturation % 37.66/6.06 % (1834253)Time elapsed: 0.415 s % 37.66/6.06 % (1834253)Peak memory usage: 120 MB % 37.66/6.06 % (1834253)Instructions burned: 387 (million) % 37.66/6.06 % (1834252)Instruction limit reached! % 37.66/6.06 % (1834252)------------------------------ % 37.66/6.06 % (1834252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.66/6.06 % (1834252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.66/6.06 % (1834252)CaDiCaL version: 2.1.3 % 37.66/6.06 % (1834252)Termination reason: Instruction limit % 41.28/6.93 % (1834252)Termination phase: Saturation % 41.28/6.93 % (1834252)Time elapsed: 0.428 s % 41.28/6.93 % (1834252)Peak memory usage: 119 MB % 41.28/6.93 % (1834252)Instructions burned: 376 (million) % 41.28/6.93 % (1834262)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=244529025:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2961 on theBenchmark for (2961ds/341Mi) % 41.28/6.93 % (1834261)Instruction limit reached! % 41.28/6.93 % (1834261)------------------------------ % 41.28/6.93 % (1834261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.28/6.93 % (1834261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.28/6.93 % (1834261)CaDiCaL version: 2.1.3 % 41.28/6.93 % (1834261)Termination reason: Instruction limit % 41.28/6.93 % (1834261)Termination phase: Saturation % 41.28/6.93 % (1834261)Time elapsed: 0.176 s % 41.28/6.93 % (1834261)Peak memory usage: 91 MB % 41.28/6.93 % (1834261)Instructions burned: 360 (million) % 41.28/6.93 % (1834265)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=3652754606:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/235Mi) % 41.28/6.93 % (1834264)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3532948145:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi) % 41.28/6.93 % (1834267)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1214501007:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi) % 41.28/6.93 % (1834268)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=291847077:i=146:doe=on:rtra=on_2960 on theBenchmark for (2960ds/146Mi) % 41.28/6.93 % (1834260)Instruction limit reached! % 41.28/6.93 % (1834260)------------------------------ % 41.28/6.93 % (1834260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.28/6.93 % (1834260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.28/6.93 % (1834260)CaDiCaL version: 2.1.3 % 41.28/6.93 % (1834260)Termination reason: Instruction limit % 41.28/6.93 % (1834260)Termination phase: Saturation % 41.28/6.93 % (1834260)Time elapsed: 0.379 s % 41.28/6.93 % (1834260)Peak memory usage: 137 MB % 41.28/6.93 % (1834260)Instructions burned: 334 (million) % 41.28/6.93 % (1834270)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1156970006:i=4428:doe=on:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/4428Mi) % 41.28/6.93 % (1834265)Instruction limit reached! % 41.28/6.93 % (1834265)------------------------------ % 41.28/6.93 % (1834265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.28/6.93 % (1834265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.28/6.93 % (1834265)CaDiCaL version: 2.1.3 % 41.28/6.93 % (1834265)Termination reason: Instruction limit % 41.28/6.93 % (1834265)Termination phase: Saturation % 41.28/6.93 % (1834265)Time elapsed: 0.284 s % 41.28/6.93 % (1834265)Peak memory usage: 119 MB % 41.28/6.93 % (1834265)Instructions burned: 235 (million) % 41.28/6.93 % (1834268)Instruction limit reached! % 41.28/6.93 % (1834268)------------------------------ % 41.28/6.93 % (1834268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.28/6.93 % (1834268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.28/6.93 % (1834268)CaDiCaL version: 2.1.3 % 41.28/6.93 % (1834268)Termination reason: Instruction limit % 41.28/6.93 % (1834268)Termination phase: Saturation % 41.28/6.93 % (1834268)Time elapsed: 0.150 s % 41.28/6.93 % (1834268)Peak memory usage: 90 MB % 41.28/6.93 % (1834268)Instructions burned: 147 (million) % 41.28/6.93 % (1834262)Instruction limit reached! % 41.28/6.93 % (1834262)------------------------------ % 41.28/6.93 % (1834262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.28/6.93 % (1834262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.28/6.93 % (1834262)CaDiCaL version: 2.1.3 % 41.28/6.93 % (1834262)Termination reason: Instruction limit % 41.28/6.93 % (1834262)Termination phase: Saturation % 41.28/6.93 % (1834262)Time elapsed: 0.357 s % 41.28/6.93 % (1834262)Peak memory usage: 119 MB % 41.28/6.93 % (1834262)Instructions burned: 342 (million) % 41.28/6.93 % (1834264)Instruction limit reached! % 41.28/6.93 % (1834264)------------------------------ % 41.28/6.93 % (1834264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.35/7.60 % (1834264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.35/7.60 % (1834264)CaDiCaL version: 2.1.3 % 47.35/7.60 % (1834264)Termination reason: Instruction limit % 47.35/7.60 % (1834264)Termination phase: Saturation % 47.35/7.60 % (1834264)Time elapsed: 0.299 s % 47.35/7.60 % (1834264)Peak memory usage: 119 MB % 47.35/7.60 % (1834264)Instructions burned: 262 (million) % 47.35/7.60 % (1834275)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=3215000:avsq=on:i=276:avsqr=1,2:rtra=on_2957 on theBenchmark for (2957ds/276Mi) % 47.35/7.60 % (1834267)Instruction limit reached! % 47.35/7.60 % (1834267)------------------------------ % 47.35/7.60 % (1834267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.35/7.60 % (1834267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.35/7.60 % (1834267)CaDiCaL version: 2.1.3 % 47.35/7.60 % (1834267)Termination reason: Instruction limit % 47.35/7.60 % (1834267)Termination phase: Saturation % 47.35/7.60 % (1834267)Time elapsed: 0.312 s % 47.35/7.60 % (1834267)Peak memory usage: 92 MB % 47.35/7.60 % (1834267)Instructions burned: 273 (million) % 47.35/7.60 % (1834280)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=184736352:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi) % 47.35/7.60 % (1834279)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1956733915:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi) % 47.35/7.60 % (1834277)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2061919826:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 47.35/7.60 % (1834278)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1161891375:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/655Mi) % 47.35/7.60 % (1834280)Refutation not found, incomplete strategy % 47.35/7.60 % (1834280)------------------------------ % 47.35/7.60 % (1834280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.35/7.60 % (1834280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.35/7.60 % (1834280)CaDiCaL version: 2.1.3 % 47.35/7.60 % (1834280)Termination reason: Refutation not found, incomplete strategy % 47.35/7.60 % (1834280)Time elapsed: 0.036 s % 47.35/7.60 % (1834280)Peak memory usage: 116 MB % 47.35/7.60 % (1834280)Instructions burned: 16 (million) % 47.35/7.60 % (1834282)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=950192794:s2a=on:i=450:doe=on:nm=32:rtra=on_2954 on theBenchmark for (2954ds/450Mi) % 47.35/7.60 % (1834275)Instruction limit reached! % 47.35/7.60 % (1834275)------------------------------ % 47.35/7.60 % (1834275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.35/7.60 % (1834275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.35/7.60 % (1834275)CaDiCaL version: 2.1.3 % 47.35/7.60 % (1834275)Termination reason: Instruction limit % 47.35/7.60 % (1834275)Termination phase: Saturation % 47.35/7.60 % (1834275)Time elapsed: 0.327 s % 47.35/7.60 % (1834275)Peak memory usage: 136 MB % 47.35/7.60 % (1834275)Instructions burned: 277 (million) % 47.35/7.60 % (1834280)------------------------------ % 47.35/7.60 % (1834280)------------------------------ % 47.35/7.60 % (1834288)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 % 47.35/7.60 % (1834288)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=570661819:i=1090:aac=none:nm=0:rtra=on:rawr=on_2951 on theBenchmark for (2951ds/1090Mi) % 47.35/7.60 % (1834289)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=964008916:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2950 on theBenchmark for (2950ds/130Mi) % 47.35/7.60 % (1834282)Instruction limit reached! % 47.35/7.60 % (1834282)------------------------------ % 47.35/7.60 % (1834282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.35/7.60 % (1834282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.35/7.60 % (1834282)CaDiCaL version: 2.1.3 % 47.35/7.60 % (1834282)Termination reason: Instruction limit % 51.77/8.12 % (1834282)Termination phase: Saturation % 51.77/8.12 % (1834282)Time elapsed: 0.508 s % 51.77/8.12 % (1834282)Peak memory usage: 137 MB % 51.77/8.12 % (1834282)Instructions burned: 450 (million) % 51.77/8.12 % (1834278)Instruction limit reached! % 51.77/8.12 % (1834278)------------------------------ % 51.77/8.12 % (1834278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.77/8.12 % (1834278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.77/8.12 % (1834278)CaDiCaL version: 2.1.3 % 51.77/8.12 % (1834278)Termination reason: Instruction limit % 51.77/8.12 % (1834278)Termination phase: Saturation % 51.77/8.12 % (1834278)Time elapsed: 0.723 s % 51.77/8.12 % (1834278)Peak memory usage: 95 MB % 51.77/8.12 % (1834278)Instructions burned: 656 (million) % 51.77/8.12 % (1834289)Instruction limit reached! % 51.77/8.12 % (1834289)------------------------------ % 51.77/8.12 % (1834289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.77/8.12 % (1834289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.77/8.12 % (1834289)CaDiCaL version: 2.1.3 % 51.77/8.12 % (1834289)Termination reason: Instruction limit % 51.77/8.12 % (1834289)Termination phase: Saturation % 51.77/8.12 % (1834289)Time elapsed: 0.175 s % 51.77/8.12 % (1834289)Peak memory usage: 118 MB % 51.77/8.12 % (1834289)Instructions burned: 131 (million) % 51.77/8.12 % (1834292)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=543025395:i=312:kws=inv_frequency:nm=20:rtra=on_2946 on theBenchmark for (2946ds/312Mi) % 51.77/8.12 % (1834293)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1574011493:i=491:doe=on:rtra=on:gtg=position_2946 on theBenchmark for (2946ds/491Mi) % 51.77/8.12 % (1834294)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=212977592:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 51.77/8.12 % (1834279)Instruction limit reached! % 51.77/8.12 % (1834279)------------------------------ % 51.77/8.12 % (1834279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.77/8.12 % (1834279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.77/8.12 % (1834279)CaDiCaL version: 2.1.3 % 51.77/8.12 % (1834279)Termination reason: Instruction limit % 51.77/8.12 % (1834279)Termination phase: Saturation % 51.77/8.12 % (1834279)Time elapsed: 1.019 s % 51.77/8.12 % (1834279)Peak memory usage: 93 MB % 51.77/8.12 % (1834279)Instructions burned: 1055 (million) % 51.77/8.12 % (1834277)Instruction limit reached! % 51.77/8.12 % (1834277)------------------------------ % 51.77/8.12 % (1834277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.77/8.12 % (1834277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.77/8.12 % (1834277)CaDiCaL version: 2.1.3 % 51.77/8.12 % (1834277)Termination reason: Instruction limit % 51.77/8.12 % (1834277)Termination phase: Saturation % 51.77/8.12 % (1834277)Time elapsed: 1.059 s % 51.77/8.12 % (1834277)Peak memory usage: 95 MB % 51.77/8.12 % (1834277)Instructions burned: 1052 (million) % 51.77/8.12 % (1834292)Instruction limit reached! % 51.77/8.12 % (1834292)------------------------------ % 51.77/8.12 % (1834292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.77/8.12 % (1834292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.77/8.12 % (1834292)CaDiCaL version: 2.1.3 % 51.77/8.12 % (1834292)Termination reason: Instruction limit % 51.77/8.12 % (1834292)Termination phase: Saturation % 51.77/8.12 % (1834292)Time elapsed: 0.343 s % 51.77/8.12 % (1834292)Peak memory usage: 118 MB % 51.77/8.12 % (1834292)Instructions burned: 312 (million) % 51.77/8.12 % (1834298)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=325956164:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2943 on theBenchmark for (2943ds/307Mi) % 51.77/8.12 % (1834299)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=292596901:i=776:doe=on:rtra=on_2942 on theBenchmark for (2942ds/776Mi) % 51.77/8.12 % (1834300)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1632151040:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 51.77/8.12 % (1834293)Instruction limit reached! % 51.77/8.12 % (1834293)------------------------------ % 51.77/8.12 % (1834293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.77/8.12 % (1834293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.77/8.12 % (1834293)CaDiCaL version: 2.1.3 % 61.66/9.51 % (1834293)Termination reason: Instruction limit % 61.66/9.51 % (1834293)Termination phase: Saturation % 61.66/9.51 % (1834293)Time elapsed: 0.505 s % 61.66/9.51 % (1834293)Peak memory usage: 95 MB % 61.66/9.51 % (1834293)Instructions burned: 491 (million) % 61.66/9.51 % (1834288)Instruction limit reached! % 61.66/9.51 % (1834288)------------------------------ % 61.66/9.51 % (1834288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.51 % (1834288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.51 % (1834288)CaDiCaL version: 2.1.3 % 61.66/9.51 % (1834288)Termination reason: Instruction limit % 61.66/9.51 % (1834288)Termination phase: Saturation % 61.66/9.51 % (1834288)Time elapsed: 1.045 s % 61.66/9.51 % (1834288)Peak memory usage: 125 MB % 61.66/9.51 % (1834288)Instructions burned: 1090 (million) % 61.66/9.51 % (1834298)Instruction limit reached! % 61.66/9.51 % (1834298)------------------------------ % 61.66/9.51 % (1834298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.51 % (1834298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.51 % (1834298)CaDiCaL version: 2.1.3 % 61.66/9.51 % (1834298)Termination reason: Instruction limit % 61.66/9.51 % (1834298)Termination phase: Saturation % 61.66/9.51 % (1834298)Time elapsed: 0.341 s % 61.66/9.51 % (1834298)Peak memory usage: 93 MB % 61.66/9.51 % (1834298)Instructions burned: 307 (million) % 61.66/9.51 % (1834270)Instruction limit reached! % 61.66/9.51 % (1834270)------------------------------ % 61.66/9.51 % (1834270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.51 % (1834270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.51 % (1834270)CaDiCaL version: 2.1.3 % 61.66/9.51 % (1834270)Termination reason: Instruction limit % 61.66/9.51 % (1834270)Termination phase: Saturation % 61.66/9.51 % (1834270)Time elapsed: 2.116 s % 61.66/9.51 % (1834270)Peak memory usage: 114 MB % 61.66/9.51 % (1834270)Instructions burned: 4430 (million) % 61.66/9.51 % (1834305)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=2850404175:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi) % 61.66/9.51 % (1834304)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=2806410850:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2938 on theBenchmark for (2938ds/784Mi) % 61.66/9.51 % (1834294)Instruction limit reached! % 61.66/9.51 % (1834294)------------------------------ % 61.66/9.51 % (1834294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.51 % (1834294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.51 % (1834294)CaDiCaL version: 2.1.3 % 61.66/9.51 % (1834294)Termination reason: Instruction limit % 61.66/9.51 % (1834294)Termination phase: Saturation % 61.66/9.51 % (1834294)Time elapsed: 0.861 s % 61.66/9.51 % (1834294)Peak memory usage: 94 MB % 61.66/9.51 % (1834294)Instructions burned: 835 (million) % 61.66/9.51 % (1834306)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=2531265951:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2936 on theBenchmark for (2936ds/246Mi) % 61.66/9.51 % (1834307)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1352534756:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/775Mi) % 61.66/9.51 % (1834299)Instruction limit reached! % 61.66/9.51 % (1834299)------------------------------ % 61.66/9.51 % (1834299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.51 % (1834299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.51 % (1834299)CaDiCaL version: 2.1.3 % 61.66/9.51 % (1834299)Termination reason: Instruction limit % 61.66/9.51 % (1834299)Termination phase: Saturation % 61.66/9.51 % (1834299)Time elapsed: 0.691 s % 61.66/9.51 % (1834299)Peak memory usage: 119 MB % 61.66/9.51 % (1834299)Instructions burned: 776 (million) % 61.66/9.51 % (1834310)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3241995213:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2934 on theBenchmark for (2934ds/273Mi) % 61.66/9.51 % (1834300)Instruction limit reached! % 61.66/9.51 % (1834300)------------------------------ % 61.66/9.51 % (1834300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.31/12.26 % (1834300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.31/12.26 % (1834300)CaDiCaL version: 2.1.3 % 81.31/12.26 % (1834300)Termination reason: Instruction limit % 81.31/12.26 % (1834300)Termination phase: Saturation % 81.31/12.26 % (1834300)Time elapsed: 0.691 s % 81.31/12.26 % (1834300)Peak memory usage: 140 MB % 81.31/12.26 % (1834300)Instructions burned: 647 (million) % 81.31/12.26 % (1834306)Instruction limit reached! % 81.31/12.26 % (1834306)------------------------------ % 81.31/12.26 % (1834306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.31/12.26 % (1834306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.31/12.26 % (1834306)CaDiCaL version: 2.1.3 % 81.31/12.26 % (1834306)Termination reason: Instruction limit % 81.31/12.26 % (1834306)Termination phase: Saturation % 81.31/12.26 % (1834306)Time elapsed: 0.287 s % 81.31/12.26 % (1834306)Peak memory usage: 119 MB % 81.31/12.26 % (1834306)Instructions burned: 248 (million) % 81.31/12.26 % (1834313)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1988279450:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi) % 81.31/12.26 % (1834307)Instruction limit reached! % 81.31/12.26 % (1834307)------------------------------ % 81.31/12.26 % (1834307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.31/12.26 % (1834307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.31/12.26 % (1834307)CaDiCaL version: 2.1.3 % 81.31/12.26 % (1834307)Termination reason: Instruction limit % 81.31/12.26 % (1834307)Termination phase: Saturation % 81.31/12.26 % (1834307)Time elapsed: 0.409 s % 81.31/12.26 % (1834307)Peak memory usage: 95 MB % 81.31/12.26 % (1834307)Instructions burned: 775 (million) % 81.31/12.26 % (1834310)Instruction limit reached! % 81.31/12.26 % (1834310)------------------------------ % 81.31/12.26 % (1834310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.31/12.26 % (1834310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.31/12.26 % (1834310)CaDiCaL version: 2.1.3 % 81.31/12.26 % (1834310)Termination reason: Instruction limit % 81.31/12.26 % (1834310)Termination phase: Saturation % 81.31/12.26 % (1834310)Time elapsed: 0.295 s % 81.31/12.26 % (1834310)Peak memory usage: 92 MB % 81.31/12.26 % (1834310)Instructions burned: 273 (million) % 81.31/12.26 % (1834313)Instruction limit reached! % 81.31/12.26 % (1834313)------------------------------ % 81.31/12.26 % (1834313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.31/12.26 % (1834313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.31/12.26 % (1834313)CaDiCaL version: 2.1.3 % 81.31/12.26 % (1834313)Termination reason: Instruction limit % 81.31/12.26 % (1834313)Termination phase: Saturation % 81.31/12.26 % (1834313)Time elapsed: 0.104 s % 81.31/12.26 % (1834313)Peak memory usage: 89 MB % 81.31/12.26 % (1834313)Instructions burned: 102 (million) % 81.31/12.26 % (1834316)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2872718360:i=6400:doe=on:fsr=off:rtra=on_2931 on theBenchmark for (2931ds/6400Mi) % 81.31/12.26 % (1834315)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=603659697:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 81.31/12.26 % (1834319)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=363954908:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi) % 81.31/12.26 % (1834318)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=4156319523:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/868Mi) % 81.31/12.26 % (1834304)Instruction limit reached! % 81.31/12.26 % (1834304)------------------------------ % 81.31/12.26 % (1834304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.31/12.26 % (1834304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.31/12.26 % (1834304)CaDiCaL version: 2.1.3 % 81.31/12.26 % (1834304)Termination reason: Instruction limit % 81.31/12.26 % (1834304)Termination phase: Saturation % 81.31/12.26 % (1834304)Time elapsed: 0.890 s % 81.31/12.26 % (1834304)Peak memory usage: 124 MB % 81.31/12.26 % (1834304)Instructions burned: 784 (million) % 81.31/12.26 % (1834320)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1231089765:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2929 on theBenchmark for (2929ds/36816Mi) % 99.46/15.05 % (1834325)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1829537690:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2926 on theBenchmark for (2926ds/273Mi) % 99.46/15.05 % (1834305)Instruction limit reached! % 99.46/15.05 % (1834305)------------------------------ % 99.46/15.05 % (1834305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.46/15.05 % (1834305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.46/15.05 % (1834305)CaDiCaL version: 2.1.3 % 99.46/15.05 % (1834305)Termination reason: Instruction limit % 99.46/15.05 % (1834305)Termination phase: Saturation % 99.46/15.05 % (1834305)Time elapsed: 1.203 s % 99.46/15.05 % (1834305)Peak memory usage: 123 MB % 99.46/15.05 % (1834305)Instructions burned: 1131 (million) % 99.46/15.05 % (1834328)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=138578478:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2923 on theBenchmark for (2923ds/863Mi) % 99.46/15.05 % (1834325)Instruction limit reached! % 99.46/15.05 % (1834325)------------------------------ % 99.46/15.05 % (1834325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.46/15.05 % (1834325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.46/15.05 % (1834325)CaDiCaL version: 2.1.3 % 99.46/15.05 % (1834325)Termination reason: Instruction limit % 99.46/15.05 % (1834325)Termination phase: Saturation % 99.46/15.05 % (1834325)Time elapsed: 0.296 s % 99.46/15.05 % (1834325)Peak memory usage: 92 MB % 99.46/15.05 % (1834325)Instructions burned: 273 (million) % 99.46/15.05 % (1834319)Instruction limit reached! % 99.46/15.05 % (1834319)------------------------------ % 99.46/15.05 % (1834319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.46/15.05 % (1834319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.46/15.05 % (1834319)CaDiCaL version: 2.1.3 % 99.46/15.05 % (1834319)Termination reason: Instruction limit % 99.46/15.05 % (1834319)Termination phase: Saturation % 99.46/15.05 % (1834319)Time elapsed: 0.872 s % 99.46/15.05 % (1834319)Peak memory usage: 101 MB % 99.46/15.05 % (1834319)Instructions burned: 1847 (million) % 99.46/15.05 % (1834318)Instruction limit reached! % 99.46/15.05 % (1834318)------------------------------ % 99.46/15.05 % (1834318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.46/15.05 % (1834318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.46/15.05 % (1834318)CaDiCaL version: 2.1.3 % 99.46/15.05 % (1834318)Termination reason: Instruction limit % 99.46/15.05 % (1834318)Termination phase: Saturation % 99.46/15.05 % (1834318)Time elapsed: 0.885 s % 99.46/15.05 % (1834318)Peak memory usage: 122 MB % 99.46/15.05 % (1834318)Instructions burned: 868 (million) % 99.46/15.05 % (1834330)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3448645123:i=5811:kws=precedence:nm=0:rtra=on_2920 on theBenchmark for (2920ds/5811Mi) % 99.46/15.05 % (1834315)Instruction limit reached! % 99.46/15.05 % (1834315)------------------------------ % 99.46/15.05 % (1834315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.46/15.05 % (1834315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.46/15.05 % (1834315)CaDiCaL version: 2.1.3 % 99.46/15.05 % (1834315)Termination reason: Instruction limit % 99.46/15.05 % (1834315)Termination phase: Saturation % 99.46/15.05 % (1834315)Time elapsed: 1.105 s % 99.46/15.05 % (1834315)Peak memory usage: 96 MB % 99.46/15.05 % (1834315)Instructions burned: 1094 (million) % 99.46/15.05 % (1834331)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=4177392705:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2918 on theBenchmark for (2918ds/2216Mi) % 99.46/15.05 % (1834332)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1650261212:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2918 on theBenchmark for (2918ds/801Mi) % 99.46/15.05 % (1834334)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1379872250:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2917 on theBenchmark for (2917ds/1026Mi) % 99.46/15.05 % (1834328)Instruction limit reached! % 99.46/15.05 % (1834328)------------------------------ % 99.46/15.05 % (1834328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.46/15.05 % (1834328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.08/21.63 % (1834328)CaDiCaL version: 2.1.3 % 148.08/21.63 % (1834328)Termination reason: Instruction limit % 148.08/21.63 % (1834328)Termination phase: Saturation % 148.08/21.63 % (1834328)Time elapsed: 0.816 s % 148.08/21.63 % (1834328)Peak memory usage: 119 MB % 148.08/21.63 % (1834328)Instructions burned: 864 (million) % 148.08/21.63 % (1834332)Instruction limit reached! % 148.08/21.63 % (1834332)------------------------------ % 148.08/21.63 % (1834332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.08/21.63 % (1834332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.08/21.63 % (1834332)CaDiCaL version: 2.1.3 % 148.08/21.63 % (1834332)Termination reason: Instruction limit % 148.08/21.63 % (1834332)Termination phase: Saturation % 148.08/21.63 % (1834332)Time elapsed: 0.453 s % 148.08/21.63 % (1834332)Peak memory usage: 96 MB % 148.08/21.63 % (1834332)Instructions burned: 802 (million) % 148.08/21.63 % (1834339)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4083430644:i=3509:rtra=on_2912 on theBenchmark for (2912ds/3509Mi) % 148.08/21.63 % (1834341)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2277428709:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/2127Mi) % 148.08/21.63 % (1834334)Instruction limit reached! % 148.08/21.63 % (1834334)------------------------------ % 148.08/21.63 % (1834334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.08/21.63 % (1834334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.08/21.63 % (1834334)CaDiCaL version: 2.1.3 % 148.08/21.63 % (1834334)Termination reason: Instruction limit % 148.08/21.63 % (1834334)Termination phase: Saturation % 148.08/21.63 % (1834334)Time elapsed: 0.957 s % 148.08/21.63 % (1834334)Peak memory usage: 94 MB % 148.08/21.63 % (1834334)Instructions burned: 1027 (million) % 148.08/21.63 % (1834350)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3636385913:i=1959:rtra=on:fsd=on:proc=on_2905 on theBenchmark for (2905ds/1959Mi) % 148.08/21.63 % (1834331)Instruction limit reached! % 148.08/21.63 % (1834331)------------------------------ % 148.08/21.63 % (1834331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.08/21.63 % (1834331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.08/21.63 % (1834331)CaDiCaL version: 2.1.3 % 148.08/21.63 % (1834331)Termination reason: Instruction limit % 148.08/21.63 % (1834331)Termination phase: Saturation % 148.08/21.63 % (1834331)Time elapsed: 1.898 s % 148.08/21.63 % (1834331)Peak memory usage: 121 MB % 148.08/21.63 % (1834331)Instructions burned: 2217 (million) % 148.08/21.63 % (1834358)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2323727673:s2a=on:i=3553:nm=0:rtra=on_2897 on theBenchmark for (2897ds/3553Mi) % 148.08/21.63 % (1834339)Instruction limit reached! % 148.08/21.63 % (1834339)------------------------------ % 148.08/21.63 % (1834339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.08/21.63 % (1834339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.08/21.63 % (1834339)CaDiCaL version: 2.1.3 % 148.08/21.63 % (1834339)Termination reason: Instruction limit % 148.08/21.63 % (1834339)Termination phase: Saturation % 148.08/21.63 % (1834339)Time elapsed: 1.689 s % 148.08/21.63 % (1834339)Peak memory usage: 109 MB % 148.08/21.63 % (1834339)Instructions burned: 3509 (million) % 148.08/21.63 % (1834360)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1184897721:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/3201Mi) % 148.08/21.63 % (1834341)Instruction limit reached! % 148.08/21.63 % (1834341)------------------------------ % 148.08/21.63 % (1834341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.08/21.63 % (1834341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.08/21.63 % (1834341)CaDiCaL version: 2.1.3 % 148.08/21.63 % (1834341)Termination reason: Instruction limit % 148.08/21.63 % (1834341)Termination phase: Saturation % 148.08/21.63 % (1834341)Time elapsed: 1.866 s % 148.08/21.63 % (1834341)Peak memory usage: 92 MB % 148.08/21.63 % (1834341)Instructions burned: 2127 (million) % 148.08/21.63 % (1834362)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=2323620499:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2890 on theBenchmark for (2890ds/4093Mi) % 148.08/21.63 % (1834350)Instruction limit reached! % 148.08/21.63 % (1834350)------------------------------ % 188.48/27.38 % (1834350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.48/27.38 % (1834350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.48/27.38 % (1834350)CaDiCaL version: 2.1.3 % 188.48/27.38 % (1834350)Termination reason: Instruction limit % 188.48/27.38 % (1834350)Termination phase: Saturation % 188.48/27.38 % (1834350)Time elapsed: 1.719 s % 188.48/27.38 % (1834350)Peak memory usage: 121 MB % 188.48/27.38 % (1834350)Instructions burned: 1959 (million) % 188.48/27.38 % (1834366)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=3232100254:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2884 on theBenchmark for (2884ds/21173Mi) % 188.48/27.38 % (1834360)Instruction limit reached! % 188.48/27.38 % (1834360)------------------------------ % 188.48/27.38 % (1834360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.48/27.38 % (1834360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.48/27.38 % (1834360)CaDiCaL version: 2.1.3 % 188.48/27.38 % (1834360)Termination reason: Instruction limit % 188.48/27.38 % (1834360)Termination phase: Saturation % 188.48/27.38 % (1834360)Time elapsed: 1.400 s % 188.48/27.38 % (1834360)Peak memory usage: 93 MB % 188.48/27.38 % (1834360)Instructions burned: 3201 (million) % 188.48/27.38 % (1834370)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2031752061:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2876 on theBenchmark for (2876ds/10544Mi) % 188.48/27.38 % (1834316)Instruction limit reached! % 188.48/27.38 % (1834316)------------------------------ % 188.48/27.38 % (1834316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.48/27.38 % (1834316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.48/27.38 % (1834316)CaDiCaL version: 2.1.3 % 188.48/27.38 % (1834316)Termination reason: Instruction limit % 188.48/27.38 % (1834316)Termination phase: Saturation % 188.48/27.38 % (1834316)Time elapsed: 5.898 s % 188.48/27.38 % (1834316)Peak memory usage: 118 MB % 188.48/27.38 % (1834316)Instructions burned: 6400 (million) % 188.48/27.38 % (1834376)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1436131745:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/1262Mi) % 188.48/27.38 % (1834330)Instruction limit reached! % 188.48/27.38 % (1834330)------------------------------ % 188.48/27.38 % (1834330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.48/27.38 % (1834330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.48/27.38 % (1834330)CaDiCaL version: 2.1.3 % 188.48/27.38 % (1834330)Termination reason: Instruction limit % 188.48/27.38 % (1834330)Termination phase: Saturation % 188.48/27.38 % (1834330)Time elapsed: 5.223 s % 188.48/27.38 % (1834330)Peak memory usage: 135 MB % 188.48/27.38 % (1834330)Instructions burned: 5811 (million) % 188.48/27.38 % (1834378)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4109216562:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2865 on theBenchmark for (2865ds/775Mi) % 188.48/27.38 % (1834358)Instruction limit reached! % 188.48/27.38 % (1834358)------------------------------ % 188.48/27.38 % (1834358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.48/27.38 % (1834358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.48/27.38 % (1834358)CaDiCaL version: 2.1.3 % 188.48/27.38 % (1834358)Termination reason: Instruction limit % 188.48/27.38 % (1834358)Termination phase: Saturation % 188.48/27.38 % (1834358)Time elapsed: 3.234 s % 188.48/27.38 % (1834358)Peak memory usage: 103 MB % 188.48/27.38 % (1834358)Instructions burned: 3553 (million) % 188.48/27.38 % (1834380)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1759037701:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2862 on theBenchmark for (2862ds/270Mi) % 188.48/27.38 % (1834380)Instruction limit reached! % 188.48/27.38 % (1834380)------------------------------ % 188.48/27.38 % (1834380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.48/27.38 % (1834380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.48/27.38 % (1834380)CaDiCaL version: 2.1.3 % 188.48/27.38 % (1834380)Termination reason: Instruction limit % 188.48/27.38 % (1834380)Termination phase: Saturation % 188.48/27.38 % (1834380)Time elapsed: 0.279 s % 188.48/27.38 % (1834380)Peak memory usage: 92 MB % 188.48/27.38 % (1834380)Instructions burned: 271 (million) % 210.16/30.43 % (1834376)Instruction limit reached! % 210.16/30.43 % (1834376)------------------------------ % 210.16/30.43 % (1834376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.16/30.43 % (1834376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.16/30.43 % (1834376)CaDiCaL version: 2.1.3 % 210.16/30.43 % (1834376)Termination reason: Instruction limit % 210.16/30.43 % (1834376)Termination phase: Saturation % 210.16/30.43 % (1834376)Time elapsed: 1.106 s % 210.16/30.43 % (1834376)Peak memory usage: 121 MB % 210.16/30.43 % (1834376)Instructions burned: 1262 (million) % 210.16/30.43 % (1834378)Instruction limit reached! % 210.16/30.43 % (1834378)------------------------------ % 210.16/30.43 % (1834378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.16/30.43 % (1834378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.16/30.43 % (1834378)CaDiCaL version: 2.1.3 % 210.16/30.43 % (1834378)Termination reason: Instruction limit % 210.16/30.43 % (1834378)Termination phase: Saturation % 210.16/30.43 % (1834378)Time elapsed: 0.764 s % 210.16/30.43 % (1834378)Peak memory usage: 95 MB % 210.16/30.43 % (1834378)Instructions burned: 775 (million) % 210.16/30.43 % (1834387)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2673057574:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2857 on theBenchmark for (2857ds/17165Mi) % 210.16/30.43 % (1834389)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=4240340264:s2a=on:i=13094:s2at=-1:rtra=on_2855 on theBenchmark for (2855ds/13094Mi) % 210.16/30.43 % (1834390)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3389189771:st=2:i=12633:rtra=on:ss=axioms_2855 on theBenchmark for (2855ds/12633Mi) % 210.16/30.43 % (1834362)Instruction limit reached! % 210.16/30.43 % (1834362)------------------------------ % 210.16/30.43 % (1834362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.16/30.43 % (1834362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.16/30.43 % (1834362)CaDiCaL version: 2.1.3 % 210.16/30.43 % (1834362)Termination reason: Instruction limit % 210.16/30.43 % (1834362)Termination phase: Saturation % 210.16/30.43 % (1834362)Time elapsed: 4.168 s % 210.16/30.43 % (1834362)Peak memory usage: 147 MB % 210.16/30.43 % (1834362)Instructions burned: 4093 (million) % 210.16/30.43 % (1834394)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1389136595:i=1783:rtra=on:gtg=position_2846 on theBenchmark for (2846ds/1783Mi) % 210.16/30.43 % (1834394)Instruction limit reached! % 210.16/30.43 % (1834394)------------------------------ % 210.16/30.43 % (1834394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.16/30.43 % (1834394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.16/30.43 % (1834394)CaDiCaL version: 2.1.3 % 210.16/30.43 % (1834394)Termination reason: Instruction limit % 210.16/30.43 % (1834394)Termination phase: Saturation % 210.16/30.43 % (1834394)Time elapsed: 1.748 s % 210.16/30.43 % (1834394)Peak memory usage: 123 MB % 210.16/30.43 % (1834394)Instructions burned: 1783 (million) % 210.16/30.43 % (1834407)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=1521899184:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2825 on theBenchmark for (2825ds/5451Mi) % 210.16/30.43 % (1834370)Instruction limit reached! % 210.16/30.43 % (1834370)------------------------------ % 210.16/30.43 % (1834370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.16/30.43 % (1834370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.16/30.43 % (1834370)CaDiCaL version: 2.1.3 % 210.16/30.43 % (1834370)Termination reason: Instruction limit % 210.16/30.43 % (1834370)Termination phase: Saturation % 210.16/30.43 % (1834370)Time elapsed: 5.908 s % 210.16/30.43 % (1834370)Peak memory usage: 191 MB % 210.16/30.43 % (1834370)Instructions burned: 10545 (million) % 210.16/30.43 % (1834409)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=2853639067:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2815 on theBenchmark for (2815ds/4975Mi) % 210.16/30.43 % (1834409)Instruction limit reached! % 210.16/30.43 % (1834409)------------------------------ % 210.16/30.43 % (1834409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.16/30.43 % (1834409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.16/30.43 % (1834409)CaDiCaL version: 2.1.3 % 244.30/35.15 % (1834409)Termination reason: Instruction limit % 244.30/35.15 % (1834409)Termination phase: Saturation % 244.30/35.15 % (1834409)Time elapsed: 2.131 s % 244.30/35.15 % (1834409)Peak memory usage: 127 MB % 244.30/35.15 % (1834409)Instructions burned: 4977 (million) % 244.30/35.15 % (1834423)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=712192704:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2791 on theBenchmark for (2791ds/2076Mi) % 244.30/35.15 % (1834423)Instruction limit reached! % 244.30/35.15 % (1834423)------------------------------ % 244.30/35.15 % (1834423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.30/35.15 % (1834423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.30/35.15 % (1834423)CaDiCaL version: 2.1.3 % 244.30/35.15 % (1834423)Termination reason: Instruction limit % 244.30/35.15 % (1834423)Termination phase: Saturation % 244.30/35.15 % (1834423)Time elapsed: 0.979 s % 244.30/35.15 % (1834423)Peak memory usage: 121 MB % 244.30/35.15 % (1834423)Instructions burned: 2076 (million) % 244.30/35.15 % (1834425)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4155481605:i=5145:rtra=on_2779 on theBenchmark for (2779ds/5145Mi) % 244.30/35.15 % (1834407)Instruction limit reached! % 244.30/35.15 % (1834407)------------------------------ % 244.30/35.15 % (1834407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.30/35.15 % (1834407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.30/35.15 % (1834407)CaDiCaL version: 2.1.3 % 244.30/35.15 % (1834407)Termination reason: Instruction limit % 244.30/35.15 % (1834407)Termination phase: Saturation % 244.30/35.15 % (1834407)Time elapsed: 5.077 s % 244.30/35.15 % (1834407)Peak memory usage: 132 MB % 244.30/35.15 % (1834407)Instructions burned: 5451 (million) % 244.30/35.15 % (1834427)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1631495965:i=3509:rtra=on_2772 on theBenchmark for (2772ds/3509Mi) % 244.30/35.15 % (1834425)Instruction limit reached! % 244.30/35.15 % (1834425)------------------------------ % 244.30/35.15 % (1834425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.30/35.15 % (1834425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.30/35.15 % (1834425)CaDiCaL version: 2.1.3 % 244.30/35.15 % (1834425)Termination reason: Instruction limit % 244.30/35.15 % (1834425)Termination phase: Saturation % 244.30/35.15 % (1834425)Time elapsed: 2.687 s % 244.30/35.15 % (1834425)Peak memory usage: 113 MB % 244.30/35.15 % (1834425)Instructions burned: 5147 (million) % 244.30/35.15 % (1834431)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=141386358:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2750 on theBenchmark for (2750ds/13800Mi) % 244.30/35.15 % (1834390)Instruction limit reached! % 244.30/35.15 % (1834390)------------------------------ % 244.30/35.15 % (1834390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.30/35.15 % (1834390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.30/35.15 % (1834390)CaDiCaL version: 2.1.3 % 244.30/35.15 % (1834390)Termination reason: Instruction limit % 244.30/35.15 % (1834390)Termination phase: Saturation % 244.30/35.15 % (1834390)Time elapsed: 11.434 s % 244.30/35.15 % (1834390)Peak memory usage: 138 MB % 244.30/35.15 % (1834390)Instructions burned: 12633 (million) % 244.30/35.15 % (1834427)Instruction limit reached! % 244.30/35.15 % (1834427)------------------------------ % 244.30/35.15 % (1834427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.30/35.15 % (1834427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.30/35.15 % (1834427)CaDiCaL version: 2.1.3 % 244.30/35.15 % (1834427)Termination reason: Instruction limit % 244.30/35.15 % (1834427)Termination phase: Saturation % 244.30/35.15 % (1834427)Time elapsed: 3.260 s % 244.30/35.15 % (1834427)Peak memory usage: 108 MB % 244.30/35.15 % (1834427)Instructions burned: 3509 (million) % 244.30/35.15 % (1834434)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2813946339:i=1412:rtra=on:fsd=on:proc=on_2738 on theBenchmark for (2738ds/1412Mi) % 244.30/35.15 % (1834436)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 % 244.30/35.15 % (1834436)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1572699603:i=11747:aTerminated %------------------------------------------------------------------------------