%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW671_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n019.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:31:06 PM UTC 2026 % Result : Timeout 300.61s 43.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW671_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.24/0.28 % Computer : n019.cluster.edu % 0.24/0.28 % Model : x86_64 x86_64 % 0.24/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.24/0.28 % Memory : 8046.5625MB % 0.24/0.28 % OS : Linux 6.8.0-71-generic % 0.24/0.28 % CPULimit : 300 % 0.24/0.28 % WCLimit : 300 % 0.24/0.29 % DateTime : Mon Sep 28 14:24:33 UTC 2026 % 0.24/0.29 % CPUTime : % 0.24/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.24/0.32 Running first-order theorem proving % 0.24/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.58/1.88 % (4033662)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.58/1.88 % (4033669)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3155032068:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.58/1.88 % (4033672)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1731579559:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.58/1.88 % (4033672)Instruction limit reached! % 5.58/1.88 % (4033672)------------------------------ % 5.58/1.88 % (4033672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.88 % (4033672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.88 % (4033672)CaDiCaL version: 2.1.3 % 5.58/1.88 % (4033672)Termination reason: Instruction limit % 5.58/1.88 % (4033672)Termination phase: Property scanning % 5.58/1.88 % (4033672)Time elapsed: 0.005 s % 5.58/1.88 % (4033672)Peak memory usage: 86 MB % 5.58/1.88 % (4033672)Instructions burned: 4 (million) % 5.58/1.88 % (4033670)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=333508893:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.58/1.88 % (4033668)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2067332112:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.58/1.88 % (4033671)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2066995035:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.58/1.88 % (4033673)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3912175529:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.58/1.88 % (4033671)Instruction limit reached! % 5.58/1.88 % (4033671)------------------------------ % 5.58/1.88 % (4033671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.88 % (4033671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.88 % (4033671)CaDiCaL version: 2.1.3 % 5.58/1.88 % (4033671)Termination reason: Instruction limit % 5.58/1.88 % (4033671)Termination phase: Saturation % 5.58/1.88 % (4033671)Time elapsed: 0.009 s % 5.58/1.88 % (4033671)Peak memory usage: 88 MB % 5.58/1.88 % (4033671)Instructions burned: 8 (million) % 5.58/1.88 % (4033674)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=484414784:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.58/1.88 % (4033668)Instruction limit reached! % 5.58/1.88 % (4033668)------------------------------ % 5.58/1.88 % (4033668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.88 % (4033668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.88 % (4033668)CaDiCaL version: 2.1.3 % 5.58/1.88 % (4033668)Termination reason: Instruction limit % 5.58/1.88 % (4033668)Termination phase: Saturation % 5.58/1.88 % (4033668)Time elapsed: 0.040 s % 5.58/1.88 % (4033668)Peak memory usage: 112 MB % 5.58/1.88 % (4033668)Instructions burned: 12 (million) % 5.58/1.88 % (4033674)Instruction limit reached! % 5.58/1.88 % (4033674)------------------------------ % 5.58/1.88 % (4033674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.88 % (4033674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.88 % (4033674)CaDiCaL version: 2.1.3 % 5.58/1.88 % (4033674)Termination reason: Instruction limit % 5.58/1.88 % (4033674)Termination phase: Saturation % 5.58/1.88 % (4033674)Time elapsed: 0.048 s % 5.58/1.88 % (4033674)Peak memory usage: 116 MB % 5.58/1.88 % (4033674)Instructions burned: 33 (million) % 5.58/1.88 % (4033673)Instruction limit reached! % 5.58/1.88 % (4033673)------------------------------ % 5.58/1.88 % (4033673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.88 % (4033673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.88 % (4033673)CaDiCaL version: 2.1.3 % 5.58/1.88 % (4033673)Termination reason: Instruction limit % 5.58/1.88 % (4033673)Termination phase: Saturation % 5.58/1.88 % (4033673)Time elapsed: 0.080 s % 5.58/1.88 % (4033673)Peak memory usage: 115 MB % 5.58/1.88 % (4033673)Instructions burned: 47 (million) % 5.58/1.88 % (4033669)Instruction limit reached! % 5.58/1.88 % (4033669)------------------------------ % 5.58/1.88 % (4033669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.88 % (4033669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.11 % (4033669)CaDiCaL version: 2.1.3 % 7.42/2.11 % (4033669)Termination reason: Instruction limit % 7.42/2.11 % (4033669)Termination phase: Saturation % 7.42/2.11 % (4033669)Time elapsed: 0.189 s % 7.42/2.11 % (4033669)Peak memory usage: 117 MB % 7.42/2.11 % (4033669)Instructions burned: 308 (million) % 7.42/2.11 % (4033678)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=516591204:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 7.42/2.11 % (4033678)Instruction limit reached! % 7.42/2.11 % (4033678)------------------------------ % 7.42/2.11 % (4033678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.11 % (4033678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.11 % (4033678)CaDiCaL version: 2.1.3 % 7.42/2.11 % (4033678)Termination reason: Instruction limit % 7.42/2.11 % (4033678)Termination phase: Saturation % 7.42/2.11 % (4033678)Time elapsed: 0.017 s % 7.42/2.11 % (4033678)Peak memory usage: 88 MB % 7.42/2.11 % (4033678)Instructions burned: 14 (million) % 7.42/2.11 % (4033670)Instruction limit reached! % 7.42/2.11 % (4033670)------------------------------ % 7.42/2.11 % (4033670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.11 % (4033670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.11 % (4033670)CaDiCaL version: 2.1.3 % 7.42/2.11 % (4033670)Termination reason: Instruction limit % 7.42/2.11 % (4033670)Termination phase: Saturation % 7.42/2.11 % (4033670)Time elapsed: 0.238 s % 7.42/2.11 % (4033670)Peak memory usage: 118 MB % 7.42/2.11 % (4033670)Instructions burned: 201 (million) % 7.42/2.11 % (4033683)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=52352149:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 7.42/2.11 % (4033687)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=568133786:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 7.42/2.11 % (4033685)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2117065382:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 7.42/2.11 % (4033687)Refutation not found, incomplete strategy % 7.42/2.11 % (4033687)------------------------------ % 7.42/2.11 % (4033687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.11 % (4033687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.11 % (4033687)CaDiCaL version: 2.1.3 % 7.42/2.11 % (4033687)Termination reason: Refutation not found, incomplete strategy % 7.42/2.11 % (4033687)Time elapsed: 0.006 s % 7.42/2.11 % (4033687)Peak memory usage: 89 MB % 7.42/2.11 % (4033687)Instructions burned: 9 (million) % 7.42/2.11 % (4033683)Instruction limit reached! % 7.42/2.11 % (4033683)------------------------------ % 7.42/2.11 % (4033683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.11 % (4033683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.11 % (4033683)CaDiCaL version: 2.1.3 % 7.42/2.11 % (4033683)Termination reason: Instruction limit % 7.42/2.11 % (4033683)Termination phase: Saturation % 7.42/2.11 % (4033683)Time elapsed: 0.030 s % 7.42/2.11 % (4033683)Peak memory usage: 89 MB % 7.42/2.11 % (4033683)Instructions burned: 30 (million) % 7.42/2.11 % (4033685)Instruction limit reached! % 7.42/2.11 % (4033685)------------------------------ % 7.42/2.11 % (4033685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.11 % (4033685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.11 % (4033685)CaDiCaL version: 2.1.3 % 7.42/2.11 % (4033685)Termination reason: Instruction limit % 7.42/2.11 % (4033685)Termination phase: Saturation % 7.42/2.11 % (4033685)Time elapsed: 0.017 s % 7.42/2.11 % (4033685)Peak memory usage: 89 MB % 7.42/2.11 % (4033685)Instructions burned: 16 (million) % 7.42/2.11 % (4033686)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1508972696:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 7.42/2.11 % (4033686)Instruction limit reached! % 7.42/2.11 % (4033686)------------------------------ % 7.42/2.11 % (4033686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.11 % (4033686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.39 % (4033686)CaDiCaL version: 2.1.3 % 9.65/2.39 % (4033686)Termination reason: Instruction limit % 9.65/2.39 % (4033686)Termination phase: Saturation % 9.65/2.39 % (4033686)Time elapsed: 0.029 s % 9.65/2.39 % (4033686)Peak memory usage: 89 MB % 9.65/2.39 % (4033686)Instructions burned: 24 (million) % 9.65/2.39 % (4033688)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4000470655:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 9.65/2.39 % (4033688)Instruction limit reached! % 9.65/2.39 % (4033688)------------------------------ % 9.65/2.39 % (4033688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.39 % (4033688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.39 % (4033688)CaDiCaL version: 2.1.3 % 9.65/2.39 % (4033688)Termination reason: Instruction limit % 9.65/2.39 % (4033688)Termination phase: Saturation % 9.65/2.39 % (4033688)Time elapsed: 0.080 s % 9.65/2.39 % (4033688)Peak memory usage: 89 MB % 9.65/2.39 % (4033688)Instructions burned: 85 (million) % 9.65/2.39 % (4033690)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1769316190:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 9.65/2.39 % (4033690)Instruction limit reached! % 9.65/2.39 % (4033690)------------------------------ % 9.65/2.39 % (4033690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.39 % (4033690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.39 % (4033690)CaDiCaL version: 2.1.3 % 9.65/2.39 % (4033690)Termination reason: Instruction limit % 9.65/2.39 % (4033690)Termination phase: Preprocessing 3 % 9.65/2.39 % (4033690)Time elapsed: 0.003 s % 9.65/2.39 % (4033690)Peak memory usage: 86 MB % 9.65/2.39 % (4033690)Instructions burned: 2 (million) % 9.65/2.39 % (4033691)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1268171497:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.65/2.39 % (4033687)------------------------------ % 9.65/2.39 % (4033687)------------------------------ % 9.65/2.39 % (4033696)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=699956430:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 9.65/2.39 % (4033695)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=766799856:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.65/2.39 % (4033695)Instruction limit reached! % 9.65/2.39 % (4033695)------------------------------ % 9.65/2.39 % (4033695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.39 % (4033695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.39 % (4033695)CaDiCaL version: 2.1.3 % 9.65/2.39 % (4033695)Termination reason: Instruction limit % 9.65/2.39 % (4033695)Termination phase: Property scanning % 9.65/2.39 % (4033695)Time elapsed: 0.005 s % 9.65/2.39 % (4033695)Peak memory usage: 86 MB % 9.65/2.39 % (4033695)Instructions burned: 4 (million) % 9.65/2.39 % (4033699)lrs+10_1_thi=all:si=on:fd=off:random_seed=3734824134:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 9.65/2.39 % (4033702)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=336389988:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 9.65/2.39 % (4033702)Instruction limit reached! % 9.65/2.39 % (4033702)------------------------------ % 9.65/2.39 % (4033702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.39 % (4033702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.39 % (4033702)CaDiCaL version: 2.1.3 % 9.65/2.39 % (4033702)Termination reason: Instruction limit % 9.65/2.39 % (4033702)Termination phase: Property scanning % 9.65/2.39 % (4033702)Time elapsed: 0.003 s % 9.65/2.39 % (4033702)Peak memory usage: 86 MB % 9.65/2.39 % (4033702)Instructions burned: 2 (million) % 9.65/2.39 % (4033696)Instruction limit reached! % 9.65/2.39 % (4033696)------------------------------ % 9.65/2.39 % (4033696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.39 % (4033696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.39 % (4033696)CaDiCaL version: 2.1.3 % 9.65/2.39 % (4033696)Termination reason: Instruction limit % 9.65/2.39 % (4033696)Termination phase: Saturation % 9.65/2.39 % (4033696)Time elapsed: 0.136 s % 9.65/2.39 % (4033696)Peak memory usage: 134 MB % 9.65/2.39 % (4033696)Instructions burned: 66 (million) % 12.17/2.80 % (4033700)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=975178066:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 12.17/2.80 % (4033691)Instruction limit reached! % 12.17/2.80 % (4033691)------------------------------ % 12.17/2.80 % (4033691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.17/2.80 % (4033691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.17/2.80 % (4033691)CaDiCaL version: 2.1.3 % 12.17/2.80 % (4033691)Termination reason: Instruction limit % 12.17/2.80 % (4033691)Termination phase: Saturation % 12.17/2.80 % (4033691)Time elapsed: 0.183 s % 12.17/2.80 % (4033691)Peak memory usage: 91 MB % 12.17/2.80 % (4033691)Instructions burned: 181 (million) % 12.17/2.80 % (4033700)Instruction limit reached! % 12.17/2.80 % (4033700)------------------------------ % 12.17/2.80 % (4033700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.17/2.80 % (4033700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.17/2.80 % (4033700)CaDiCaL version: 2.1.3 % 12.17/2.80 % (4033700)Termination reason: Instruction limit % 12.17/2.80 % (4033700)Termination phase: Property scanning % 12.17/2.80 % (4033700)Time elapsed: 0.008 s % 12.17/2.80 % (4033700)Peak memory usage: 87 MB % 12.17/2.80 % (4033700)Instructions burned: 8 (million) % 12.17/2.80 % (4033699)Instruction limit reached! % 12.17/2.80 % (4033699)------------------------------ % 12.17/2.80 % (4033699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.17/2.80 % (4033699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.17/2.80 % (4033699)CaDiCaL version: 2.1.3 % 12.17/2.80 % (4033699)Termination reason: Instruction limit % 12.17/2.80 % (4033699)Termination phase: Saturation % 12.17/2.80 % (4033699)Time elapsed: 0.094 s % 12.17/2.80 % (4033699)Peak memory usage: 118 MB % 12.17/2.80 % (4033699)Instructions burned: 53 (million) % 12.17/2.80 % (4033707)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1737083271:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 12.17/2.80 % (4033705)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3656775400:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi) % 12.17/2.80 % (4033705)Instruction limit reached! % 12.17/2.80 % (4033705)------------------------------ % 12.17/2.80 % (4033705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.17/2.80 % (4033705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.17/2.80 % (4033705)CaDiCaL version: 2.1.3 % 12.17/2.80 % (4033705)Termination reason: Instruction limit % 12.17/2.80 % (4033705)Termination phase: Preprocessing 3 % 12.17/2.80 % (4033705)Time elapsed: 0.003 s % 12.17/2.80 % (4033705)Peak memory usage: 86 MB % 12.17/2.80 % (4033705)Instructions burned: 2 (million) % 12.17/2.80 % (4033707)Instruction limit reached! % 12.17/2.80 % (4033707)------------------------------ % 12.17/2.80 % (4033707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.17/2.80 % (4033707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.17/2.80 % (4033707)CaDiCaL version: 2.1.3 % 12.17/2.80 % (4033707)Termination reason: Instruction limit % 12.17/2.80 % (4033707)Termination phase: Saturation % 12.17/2.80 % (4033707)Time elapsed: 0.096 s % 12.17/2.80 % (4033707)Peak memory usage: 117 MB % 12.17/2.80 % (4033707)Instructions burned: 128 (million) % 12.17/2.80 % (4033710)dis+10_1_si=on:random_seed=3949888211:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 12.17/2.80 % (4033714)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1745662995:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 12.17/2.80 % (4033714)Instruction limit reached! % 12.17/2.80 % (4033714)------------------------------ % 12.17/2.80 % (4033714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.17/2.80 % (4033714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.17/2.80 % (4033714)CaDiCaL version: 2.1.3 % 12.17/2.80 % (4033714)Termination reason: Instruction limit % 12.17/2.80 % (4033714)Termination phase: Preprocessing 3 % 12.17/2.80 % (4033714)Time elapsed: 0.003 s % 12.17/2.80 % (4033714)Peak memory usage: 86 MB % 12.17/2.80 % (4033714)Instructions burned: 2 (million) % 12.17/2.80 % (4033710)Instruction limit reached! % 12.17/2.80 % (4033710)------------------------------ % 12.17/2.80 % (4033710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.10/3.21 % (4033710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/3.21 % (4033710)CaDiCaL version: 2.1.3 % 16.10/3.21 % (4033710)Termination reason: Instruction limit % 16.10/3.21 % (4033710)Termination phase: Saturation % 16.10/3.21 % (4033710)Time elapsed: 0.012 s % 16.10/3.21 % (4033710)Peak memory usage: 88 MB % 16.10/3.21 % (4033710)Instructions burned: 11 (million) % 16.10/3.21 % (4033713)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2558730674:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 16.10/3.21 % (4033712)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=134748777:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 16.10/3.21 % (4033712)Refutation not found, incomplete strategy % 16.10/3.21 % (4033712)------------------------------ % 16.10/3.21 % (4033712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.10/3.21 % (4033712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/3.21 % (4033712)CaDiCaL version: 2.1.3 % 16.10/3.21 % (4033712)Termination reason: Refutation not found, incomplete strategy % 16.10/3.21 % (4033712)Time elapsed: 0.012 s % 16.10/3.21 % (4033712)Peak memory usage: 89 MB % 16.10/3.21 % (4033712)Instructions burned: 9 (million) % 16.10/3.21 % (4033713)Instruction limit reached! % 16.10/3.21 % (4033713)------------------------------ % 16.10/3.21 % (4033713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.10/3.21 % (4033713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/3.21 % (4033713)CaDiCaL version: 2.1.3 % 16.10/3.21 % (4033713)Termination reason: Instruction limit % 16.10/3.21 % (4033713)Termination phase: Saturation % 16.10/3.21 % (4033713)Time elapsed: 0.040 s % 16.10/3.21 % (4033713)Peak memory usage: 89 MB % 16.10/3.21 % (4033713)Instructions burned: 35 (million) % 16.10/3.21 % (4033715)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3520959371:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 16.10/3.21 % (4033715)Instruction limit reached! % 16.10/3.21 % (4033715)------------------------------ % 16.10/3.21 % (4033715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.10/3.21 % (4033715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/3.21 % (4033715)CaDiCaL version: 2.1.3 % 16.10/3.21 % (4033715)Termination reason: Instruction limit % 16.10/3.21 % (4033715)Termination phase: Saturation % 16.10/3.21 % (4033715)Time elapsed: 0.011 s % 16.10/3.21 % (4033715)Peak memory usage: 88 MB % 16.10/3.21 % (4033715)Instructions burned: 8 (million) % 16.10/3.21 % (4033718)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1629993273:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 16.10/3.21 % (4033719)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1772165827:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi) % 16.10/3.21 % (4033719)Instruction limit reached! % 16.10/3.21 % (4033719)------------------------------ % 16.10/3.21 % (4033719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.10/3.21 % (4033719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/3.21 % (4033719)CaDiCaL version: 2.1.3 % 16.10/3.21 % (4033719)Termination reason: Instruction limit % 16.10/3.21 % (4033719)Termination phase: Saturation % 16.10/3.21 % (4033719)Time elapsed: 0.025 s % 16.10/3.21 % (4033719)Peak memory usage: 112 MB % 16.10/3.21 % (4033719)Instructions burned: 13 (million) % 16.10/3.21 % (4033723)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2893800535:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 16.10/3.21 % (4033722)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1954139995:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 16.10/3.21 % (4033723)Instruction limit reached! % 16.10/3.21 % (4033723)------------------------------ % 16.10/3.21 % (4033723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.10/3.21 % (4033723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/3.21 % (4033723)CaDiCaL version: 2.1.3 % 16.10/3.21 % (4033723)Termination reason: Instruction limit % 17.89/3.57 % (4033723)Termination phase: Saturation % 17.89/3.57 % (4033723)Time elapsed: 0.013 s % 17.89/3.57 % (4033723)Peak memory usage: 88 MB % 17.89/3.57 % (4033723)Instructions burned: 10 (million) % 17.89/3.57 % (4033726)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2244414528:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 17.89/3.57 % (4033728)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=1522224636:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 17.89/3.57 % (4033731)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=40900235:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi) % 17.89/3.57 % (4033712)------------------------------ % 17.89/3.57 % (4033712)------------------------------ % 17.89/3.57 % (4033728)Instruction limit reached! % 17.89/3.57 % (4033728)------------------------------ % 17.89/3.57 % (4033728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.57 % (4033728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.57 % (4033728)CaDiCaL version: 2.1.3 % 17.89/3.57 % (4033728)Termination reason: Instruction limit % 17.89/3.57 % (4033728)Termination phase: Saturation % 17.89/3.57 % (4033728)Time elapsed: 0.077 s % 17.89/3.57 % (4033728)Peak memory usage: 89 MB % 17.89/3.57 % (4033728)Instructions burned: 75 (million) % 17.89/3.57 % (4033718)Instruction limit reached! % 17.89/3.57 % (4033718)------------------------------ % 17.89/3.57 % (4033718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.57 % (4033718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.57 % (4033718)CaDiCaL version: 2.1.3 % 17.89/3.57 % (4033718)Termination reason: Instruction limit % 17.89/3.57 % (4033718)Termination phase: Saturation % 17.89/3.57 % (4033718)Time elapsed: 0.322 s % 17.89/3.57 % (4033718)Peak memory usage: 91 MB % 17.89/3.57 % (4033718)Instructions burned: 370 (million) % 17.89/3.57 % (4033726)Instruction limit reached! % 17.89/3.57 % (4033726)------------------------------ % 17.89/3.57 % (4033726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.57 % (4033726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.57 % (4033726)CaDiCaL version: 2.1.3 % 17.89/3.57 % (4033726)Termination reason: Instruction limit % 17.89/3.57 % (4033726)Termination phase: Saturation % 17.89/3.57 % (4033726)Time elapsed: 0.136 s % 17.89/3.57 % (4033726)Peak memory usage: 133 MB % 17.89/3.57 % (4033726)Instructions burned: 71 (million) % 17.89/3.57 % (4033722)Instruction limit reached! % 17.89/3.57 % (4033722)------------------------------ % 17.89/3.57 % (4033722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.57 % (4033722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.57 % (4033722)CaDiCaL version: 2.1.3 % 17.89/3.57 % (4033722)Termination reason: Instruction limit % 17.89/3.57 % (4033722)Termination phase: Saturation % 17.89/3.57 % (4033722)Time elapsed: 0.232 s % 17.89/3.57 % (4033722)Peak memory usage: 116 MB % 17.89/3.57 % (4033722)Instructions burned: 227 (million) % 17.89/3.57 % (4033731)Instruction limit reached! % 17.89/3.57 % (4033731)------------------------------ % 17.89/3.57 % (4033731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.57 % (4033731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.57 % (4033731)CaDiCaL version: 2.1.3 % 17.89/3.57 % (4033731)Termination reason: Instruction limit % 17.89/3.57 % (4033731)Termination phase: Saturation % 17.89/3.57 % (4033731)Time elapsed: 0.146 s % 17.89/3.57 % (4033731)Peak memory usage: 90 MB % 17.89/3.57 % (4033731)Instructions burned: 296 (million) % 17.89/3.57 % (4033734)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=160391740:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi) % 17.89/3.57 % (4033743)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2511719564:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 17.89/3.57 % (4033739)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3369420507:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2983 on theBenchmark for (2983ds/40Mi) % 17.89/3.57 % (4033740)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2646295479:i=307:rtra=on:gtg=exists_top_2983 on theBenchmark for (2983ds/307Mi) % 20.53/4.10 % (4033742)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2875930270:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 20.53/4.10 % (4033738)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3250472483:i=131:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 20.53/4.10 % (4033734)Instruction limit reached! % 20.53/4.10 % (4033734)------------------------------ % 20.53/4.10 % (4033734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.53/4.10 % (4033734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/4.10 % (4033734)CaDiCaL version: 2.1.3 % 20.53/4.10 % (4033734)Termination reason: Instruction limit % 20.53/4.10 % (4033734)Termination phase: Saturation % 20.53/4.10 % (4033734)Time elapsed: 0.164 s % 20.53/4.10 % (4033734)Peak memory usage: 117 MB % 20.53/4.10 % (4033734)Instructions burned: 130 (million) % 20.53/4.10 % (4033745)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=3123594869:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 20.53/4.10 % (4033739)Instruction limit reached! % 20.53/4.10 % (4033739)------------------------------ % 20.53/4.10 % (4033739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.53/4.10 % (4033739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/4.10 % (4033739)CaDiCaL version: 2.1.3 % 20.53/4.10 % (4033739)Termination reason: Instruction limit % 20.53/4.10 % (4033739)Termination phase: Saturation % 20.53/4.10 % (4033739)Time elapsed: 0.095 s % 20.53/4.10 % (4033739)Peak memory usage: 133 MB % 20.53/4.10 % (4033739)Instructions burned: 40 (million) % 20.53/4.10 % (4033743)Instruction limit reached! % 20.53/4.10 % (4033743)------------------------------ % 20.53/4.10 % (4033743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.53/4.10 % (4033743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/4.10 % (4033743)CaDiCaL version: 2.1.3 % 20.53/4.10 % (4033743)Termination reason: Instruction limit % 20.53/4.10 % (4033743)Termination phase: Saturation % 20.53/4.10 % (4033743)Time elapsed: 0.136 s % 20.53/4.10 % (4033743)Peak memory usage: 118 MB % 20.53/4.10 % (4033743)Instructions burned: 131 (million) % 20.53/4.10 % (4033738)Instruction limit reached! % 20.53/4.10 % (4033738)------------------------------ % 20.53/4.10 % (4033738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.53/4.10 % (4033738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/4.10 % (4033738)CaDiCaL version: 2.1.3 % 20.53/4.10 % (4033738)Termination reason: Instruction limit % 20.53/4.10 % (4033738)Termination phase: Saturation % 20.53/4.10 % (4033738)Time elapsed: 0.198 s % 20.53/4.10 % (4033738)Peak memory usage: 134 MB % 20.53/4.10 % (4033738)Instructions burned: 131 (million) % 20.53/4.10 % (4033745)Instruction limit reached! % 20.53/4.10 % (4033745)------------------------------ % 20.53/4.10 % (4033745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.53/4.10 % (4033745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/4.10 % (4033745)CaDiCaL version: 2.1.3 % 20.53/4.10 % (4033745)Termination reason: Instruction limit % 20.53/4.10 % (4033745)Termination phase: Saturation % 20.53/4.10 % (4033745)Time elapsed: 0.165 s % 20.53/4.10 % (4033745)Peak memory usage: 117 MB % 20.53/4.10 % (4033745)Instructions burned: 260 (million) % 20.53/4.10 % (4033740)Instruction limit reached! % 20.53/4.10 % (4033740)------------------------------ % 20.53/4.10 % (4033740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.53/4.10 % (4033740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/4.10 % (4033740)CaDiCaL version: 2.1.3 % 20.53/4.10 % (4033740)Termination reason: Instruction limit % 20.53/4.10 % (4033740)Termination phase: Saturation % 20.53/4.10 % (4033740)Time elapsed: 0.290 s % 20.53/4.10 % (4033740)Peak memory usage: 92 MB % 20.53/4.10 % (4033740)Instructions burned: 307 (million) % 20.53/4.10 % (4033754)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1216358858:i=383:fsr=off:rtra=on:ev=force_2980 on theBenchmark for (2980ds/383Mi) % 20.53/4.10 % (4033752)dis+10_1_si=on:random_seed=940896107:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 20.53/4.10 % (4033755)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=749949062:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 24.30/4.66 % (4033756)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4167656275:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 24.30/4.66 % (4033754)Instruction limit reached! % 24.30/4.66 % (4033754)------------------------------ % 24.30/4.66 % (4033754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.30/4.66 % (4033754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.30/4.66 % (4033754)CaDiCaL version: 2.1.3 % 24.30/4.66 % (4033754)Termination reason: Instruction limit % 24.30/4.66 % (4033754)Termination phase: Saturation % 24.30/4.66 % (4033754)Time elapsed: 0.218 s % 24.30/4.66 % (4033754)Peak memory usage: 93 MB % 24.30/4.66 % (4033754)Instructions burned: 384 (million) % 24.30/4.66 % (4033757)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4030350230:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 24.30/4.66 % (4033756)Refutation not found, incomplete strategy % 24.30/4.66 % (4033756)------------------------------ % 24.30/4.66 % (4033756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.30/4.66 % (4033756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.30/4.66 % (4033756)CaDiCaL version: 2.1.3 % 24.30/4.66 % (4033756)Termination reason: Refutation not found, incomplete strategy % 24.30/4.66 % (4033756)Time elapsed: 0.060 s % 24.30/4.66 % (4033756)Peak memory usage: 116 MB % 24.30/4.66 % (4033756)Instructions burned: 25 (million) % 24.30/4.66 % (4033755)Instruction limit reached! % 24.30/4.66 % (4033755)------------------------------ % 24.30/4.66 % (4033755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.30/4.66 % (4033755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.30/4.66 % (4033755)CaDiCaL version: 2.1.3 % 24.30/4.66 % (4033755)Termination reason: Instruction limit % 24.30/4.66 % (4033755)Termination phase: Saturation % 24.30/4.66 % (4033755)Time elapsed: 0.153 s % 24.30/4.66 % (4033755)Peak memory usage: 90 MB % 24.30/4.66 % (4033755)Instructions burned: 141 (million) % 24.30/4.66 % (4033760)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=3356292042:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 24.30/4.66 % (4033757)Instruction limit reached! % 24.30/4.66 % (4033757)------------------------------ % 24.30/4.66 % (4033757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.30/4.66 % (4033757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.30/4.66 % (4033757)CaDiCaL version: 2.1.3 % 24.30/4.66 % (4033757)Termination reason: Instruction limit % 24.30/4.66 % (4033757)Termination phase: Saturation % 24.30/4.66 % (4033757)Time elapsed: 0.127 s % 24.30/4.66 % (4033757)Peak memory usage: 89 MB % 24.30/4.66 % (4033757)Instructions burned: 121 (million) % 24.30/4.66 % (4033742)Instruction limit reached! % 24.30/4.66 % (4033742)------------------------------ % 24.30/4.66 % (4033742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.30/4.66 % (4033742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.30/4.66 % (4033742)CaDiCaL version: 2.1.3 % 24.30/4.66 % (4033742)Termination reason: Instruction limit % 24.30/4.66 % (4033742)Termination phase: Saturation % 24.30/4.66 % (4033742)Time elapsed: 0.666 s % 24.30/4.66 % (4033742)Peak memory usage: 140 MB % 24.30/4.66 % (4033742)Instructions burned: 599 (million) % 24.30/4.66 % (4033763)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=3816026991:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi) % 24.30/4.66 % (4033760)Instruction limit reached! % 24.30/4.66 % (4033760)------------------------------ % 24.30/4.66 % (4033760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.30/4.66 % (4033760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.30/4.66 % (4033760)CaDiCaL version: 2.1.3 % 24.30/4.66 % (4033760)Termination reason: Instruction limit % 24.30/4.66 % (4033760)Termination phase: Saturation % 24.30/4.66 % (4033760)Time elapsed: 0.156 s % 24.30/4.66 % (4033760)Peak memory usage: 117 MB % 24.30/4.66 % (4033760)Instructions burned: 128 (million) % 24.30/4.66 % (4033763)Refutation not found, incomplete strategy % 24.30/4.66 % (4033763)------------------------------ % 24.30/4.66 % (4033763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/5.09 % (4033763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.00/5.09 % (4033763)CaDiCaL version: 2.1.3 % 27.00/5.09 % (4033763)Termination reason: Refutation not found, incomplete strategy % 27.00/5.09 % (4033763)Time elapsed: 0.057 s % 27.00/5.09 % (4033763)Peak memory usage: 116 MB % 27.00/5.09 % (4033763)Instructions burned: 20 (million) % 27.00/5.09 % (4033766)dis+1010_1_to=kbo:si=on:random_seed=1019831987:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 27.00/5.09 % (4033768)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4055604564:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 27.00/5.09 % (4033767)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3150619281:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/329Mi) % 27.00/5.09 % (4033766)Instruction limit reached! % 27.00/5.09 % (4033766)------------------------------ % 27.00/5.09 % (4033766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/5.09 % (4033766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.00/5.09 % (4033766)CaDiCaL version: 2.1.3 % 27.00/5.09 % (4033766)Termination reason: Instruction limit % 27.00/5.09 % (4033766)Termination phase: Saturation % 27.00/5.09 % (4033766)Time elapsed: 0.105 s % 27.00/5.09 % (4033766)Peak memory usage: 91 MB % 27.00/5.09 % (4033766)Instructions burned: 176 (million) % 27.00/5.09 % (4033756)------------------------------ % 27.00/5.09 % (4033756)------------------------------ % 27.00/5.09 % (4033770)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=190433103:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi) % 27.00/5.09 % (4033768)Instruction limit reached! % 27.00/5.09 % (4033768)------------------------------ % 27.00/5.09 % (4033768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/5.09 % (4033768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.00/5.09 % (4033768)CaDiCaL version: 2.1.3 % 27.00/5.09 % (4033768)Termination reason: Instruction limit % 27.00/5.09 % (4033768)Termination phase: Saturation % 27.00/5.09 % (4033768)Time elapsed: 0.269 s % 27.00/5.09 % (4033768)Peak memory usage: 134 MB % 27.00/5.09 % (4033768)Instructions burned: 483 (million) % 27.00/5.09 % (4033763)------------------------------ % 27.00/5.09 % (4033763)------------------------------ % 27.00/5.09 % (4033774)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=143268448:i=349:rtra=on_2972 on theBenchmark for (2972ds/349Mi) % 27.00/5.09 % (4033775)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=890997162:st=2:i=295:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/295Mi) % 27.00/5.09 % (4033767)Instruction limit reached! % 27.00/5.09 % (4033767)------------------------------ % 27.00/5.09 % (4033767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/5.09 % (4033767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.00/5.09 % (4033767)CaDiCaL version: 2.1.3 % 27.00/5.09 % (4033767)Termination reason: Instruction limit % 27.00/5.09 % (4033767)Termination phase: Saturation % 27.00/5.09 % (4033767)Time elapsed: 0.372 s % 27.00/5.09 % (4033767)Peak memory usage: 120 MB % 27.00/5.09 % (4033767)Instructions burned: 329 (million) % 27.00/5.09 % (4033777)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=586569021:i=328:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/328Mi) % 27.00/5.09 % (4033752)Instruction limit reached! % 27.00/5.09 % (4033752)------------------------------ % 27.00/5.09 % (4033752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/5.09 % (4033752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.00/5.09 % (4033752)CaDiCaL version: 2.1.3 % 27.00/5.09 % (4033752)Termination reason: Instruction limit % 27.00/5.09 % (4033752)Termination phase: Saturation % 27.00/5.09 % (4033752)Time elapsed: 0.978 s % 27.00/5.09 % (4033752)Peak memory usage: 93 MB % 27.00/5.09 % (4033752)Instructions burned: 1001 (million) % 27.00/5.09 % (4033770)Instruction limit reached! % 27.00/5.09 % (4033770)------------------------------ % 27.00/5.09 % (4033770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/5.09 % (4033770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.07/5.64 % (4033770)CaDiCaL version: 2.1.3 % 32.07/5.64 % (4033770)Termination reason: Instruction limit % 32.07/5.64 % (4033770)Termination phase: Saturation % 32.07/5.64 % (4033770)Time elapsed: 0.269 s % 32.07/5.64 % (4033770)Peak memory usage: 135 MB % 32.07/5.64 % (4033770)Instructions burned: 216 (million) % 32.07/5.64 % (4033777)Instruction limit reached! % 32.07/5.64 % (4033777)------------------------------ % 32.07/5.64 % (4033777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.07/5.64 % (4033777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.07/5.64 % (4033777)CaDiCaL version: 2.1.3 % 32.07/5.64 % (4033777)Termination reason: Instruction limit % 32.07/5.64 % (4033777)Termination phase: Saturation % 32.07/5.64 % (4033777)Time elapsed: 0.160 s % 32.07/5.64 % (4033777)Peak memory usage: 118 MB % 32.07/5.64 % (4033777)Instructions burned: 329 (million) % 32.07/5.64 % (4033774)Instruction limit reached! % 32.07/5.64 % (4033774)------------------------------ % 32.07/5.64 % (4033774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.07/5.64 % (4033774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.07/5.64 % (4033774)CaDiCaL version: 2.1.3 % 32.07/5.64 % (4033774)Termination reason: Instruction limit % 32.07/5.64 % (4033774)Termination phase: Saturation % 32.07/5.64 % (4033774)Time elapsed: 0.279 s % 32.07/5.64 % (4033774)Peak memory usage: 116 MB % 32.07/5.64 % (4033774)Instructions burned: 350 (million) % 32.07/5.64 % (4033780)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=4024572512:i=281:gtgl=2:rtra=on:gtg=all_2969 on theBenchmark for (2969ds/281Mi) % 32.07/5.64 % (4033775)Instruction limit reached! % 32.07/5.64 % (4033775)------------------------------ % 32.07/5.64 % (4033775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.07/5.64 % (4033775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.07/5.64 % (4033775)CaDiCaL version: 2.1.3 % 32.07/5.64 % (4033775)Termination reason: Instruction limit % 32.07/5.64 % (4033775)Termination phase: Saturation % 32.07/5.64 % (4033775)Time elapsed: 0.281 s % 32.07/5.64 % (4033775)Peak memory usage: 91 MB % 32.07/5.64 % (4033775)Instructions burned: 295 (million) % 32.07/5.64 % (4033783)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1138397670:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/484Mi) % 32.07/5.64 % (4033784)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2336192734:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi) % 32.07/5.64 % (4033785)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=882012483:i=416:rtra=on:gtg=position:ss=axioms_2968 on theBenchmark for (2968ds/416Mi) % 32.07/5.64 % (4033788)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=826717594:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 32.07/5.64 % (4033786)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=813284343:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 32.07/5.64 % (4033791)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1264278782:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 32.07/5.64 % (4033780)Instruction limit reached! % 32.07/5.64 % (4033780)------------------------------ % 32.07/5.64 % (4033780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.07/5.64 % (4033780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.07/5.64 % (4033780)CaDiCaL version: 2.1.3 % 32.07/5.64 % (4033780)Termination reason: Instruction limit % 32.07/5.64 % (4033780)Termination phase: Saturation % 32.07/5.64 % (4033780)Time elapsed: 0.314 s % 32.07/5.64 % (4033780)Peak memory usage: 117 MB % 32.07/5.64 % (4033780)Instructions burned: 281 (million) % 32.07/5.64 % (4033788)Instruction limit reached! % 32.07/5.64 % (4033788)------------------------------ % 32.07/5.64 % (4033788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.07/5.64 % (4033788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.07/5.64 % (4033788)CaDiCaL version: 2.1.3 % 32.07/5.64 % (4033788)Termination reason: Instruction limit % 32.07/5.64 % (4033788)Termination phase: Saturation % 37.86/6.28 % (4033788)Time elapsed: 0.195 s % 37.86/6.28 % (4033788)Peak memory usage: 134 MB % 37.86/6.28 % (4033788)Instructions burned: 279 (million) % 37.86/6.28 % (4033784)Instruction limit reached! % 37.86/6.28 % (4033784)------------------------------ % 37.86/6.28 % (4033784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.86/6.28 % (4033784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.86/6.28 % (4033784)CaDiCaL version: 2.1.3 % 37.86/6.28 % (4033784)Termination reason: Instruction limit % 37.86/6.28 % (4033784)Termination phase: Saturation % 37.86/6.28 % (4033784)Time elapsed: 0.350 s % 37.86/6.28 % (4033784)Peak memory usage: 115 MB % 37.86/6.28 % (4033784)Instructions burned: 321 (million) % 37.86/6.28 % (4033783)Instruction limit reached! % 37.86/6.28 % (4033783)------------------------------ % 37.86/6.28 % (4033783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.86/6.28 % (4033783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.86/6.28 % (4033783)CaDiCaL version: 2.1.3 % 37.86/6.28 % (4033783)Termination reason: Instruction limit % 37.86/6.28 % (4033783)Termination phase: Saturation % 37.86/6.28 % (4033783)Time elapsed: 0.404 s % 37.86/6.28 % (4033783)Peak memory usage: 90 MB % 37.86/6.28 % (4033783)Instructions burned: 484 (million) % 37.86/6.28 % (4033785)Refutation not found, incomplete strategy % 37.86/6.28 % (4033785)------------------------------ % 37.86/6.28 % (4033785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.86/6.28 % (4033785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.86/6.28 % (4033785)CaDiCaL version: 2.1.3 % 37.86/6.28 % (4033785)Termination reason: Refutation not found, incomplete strategy % 37.86/6.28 % (4033785)Time elapsed: 0.370 s % 37.86/6.28 % (4033785)Peak memory usage: 118 MB % 37.86/6.28 % (4033785)Instructions burned: 395 (million) % 37.86/6.28 % (4033797)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=913127231:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/387Mi) % 37.86/6.28 % (4033798)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3097888494:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2962 on theBenchmark for (2962ds/513Mi) % 37.86/6.28 % (4033799)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3911661670:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi) % 37.86/6.28 % (4033800)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=179305809:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 37.86/6.28 % (4033800)Refutation not found, incomplete strategy % 37.86/6.28 % (4033800)------------------------------ % 37.86/6.28 % (4033800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.86/6.28 % (4033800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.86/6.28 % (4033800)CaDiCaL version: 2.1.3 % 37.86/6.28 % (4033800)Termination reason: Refutation not found, incomplete strategy % 37.86/6.28 % (4033800)Time elapsed: 0.013 s % 37.86/6.28 % (4033800)Peak memory usage: 90 MB % 37.86/6.28 % (4033800)Instructions burned: 9 (million) % 37.86/6.28 % (4033786)Instruction limit reached! % 37.86/6.28 % (4033786)------------------------------ % 37.86/6.28 % (4033786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.86/6.28 % (4033786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.86/6.28 % (4033786)CaDiCaL version: 2.1.3 % 37.86/6.28 % (4033786)Termination reason: Instruction limit % 37.86/6.28 % (4033786)Termination phase: Saturation % 37.86/6.28 % (4033786)Time elapsed: 0.493 s % 37.86/6.28 % (4033786)Peak memory usage: 119 MB % 37.86/6.28 % (4033786)Instructions burned: 471 (million) % 37.86/6.28 % (4033791)Instruction limit reached! % 37.86/6.28 % (4033791)------------------------------ % 37.86/6.28 % (4033791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.86/6.28 % (4033791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.86/6.28 % (4033791)CaDiCaL version: 2.1.3 % 37.86/6.28 % (4033791)Termination reason: Instruction limit % 37.86/6.28 % (4033791)Termination phase: Saturation % 37.86/6.28 % (4033791)Time elapsed: 0.415 s % 37.86/6.28 % (4033791)Peak memory usage: 118 MB % 37.86/6.28 % (4033791)Instructions burned: 375 (million) % 37.86/6.28 % (4033799)Instruction limit reached! % 37.86/6.28 % (4033799)------------------------------ % 37.86/6.28 % (4033799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.31/6.89 % (4033799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.31/6.89 % (4033799)CaDiCaL version: 2.1.3 % 40.31/6.89 % (4033799)Termination reason: Instruction limit % 40.31/6.89 % (4033799)Termination phase: Saturation % 40.31/6.89 % (4033799)Time elapsed: 0.192 s % 40.31/6.89 % (4033799)Peak memory usage: 134 MB % 40.31/6.89 % (4033799)Instructions burned: 337 (million) % 40.31/6.89 % (4033785)------------------------------ % 40.31/6.89 % (4033785)------------------------------ % 40.31/6.89 % (4033805)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3804375697:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2959 on theBenchmark for (2959ds/341Mi) % 40.31/6.89 % (4033806)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3071373277:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 40.31/6.89 % (4033807)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=3382798360:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2958 on theBenchmark for (2958ds/235Mi) % 40.31/6.89 % (4033800)------------------------------ % 40.31/6.89 % (4033800)------------------------------ % 40.31/6.89 % (4033797)Instruction limit reached! % 40.31/6.89 % (4033797)------------------------------ % 40.31/6.89 % (4033797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.31/6.89 % (4033797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.31/6.89 % (4033797)CaDiCaL version: 2.1.3 % 40.31/6.89 % (4033797)Termination reason: Instruction limit % 40.31/6.89 % (4033797)Termination phase: Saturation % 40.31/6.89 % (4033797)Time elapsed: 0.466 s % 40.31/6.89 % (4033797)Peak memory usage: 119 MB % 40.31/6.89 % (4033797)Instructions burned: 387 (million) % 40.31/6.89 % (4033808)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3232760986:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 40.31/6.89 % (4033798)Instruction limit reached! % 40.31/6.89 % (4033798)------------------------------ % 40.31/6.89 % (4033798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.31/6.89 % (4033798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.31/6.89 % (4033798)CaDiCaL version: 2.1.3 % 40.31/6.89 % (4033798)Termination reason: Instruction limit % 40.31/6.89 % (4033798)Termination phase: Saturation % 40.31/6.89 % (4033798)Time elapsed: 0.531 s % 40.31/6.89 % (4033798)Peak memory usage: 92 MB % 40.31/6.89 % (4033798)Instructions burned: 513 (million) % 40.31/6.89 % (4033807)Instruction limit reached! % 40.31/6.89 % (4033807)------------------------------ % 40.31/6.89 % (4033807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.31/6.89 % (4033807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.31/6.89 % (4033807)CaDiCaL version: 2.1.3 % 40.31/6.89 % (4033807)Termination reason: Instruction limit % 40.31/6.89 % (4033807)Termination phase: Saturation % 40.31/6.89 % (4033807)Time elapsed: 0.148 s % 40.31/6.89 % (4033807)Peak memory usage: 117 MB % 40.31/6.89 % (4033807)Instructions burned: 236 (million) % 40.31/6.89 % (4033806)Instruction limit reached! % 40.31/6.89 % (4033806)------------------------------ % 40.31/6.89 % (4033806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.31/6.89 % (4033806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.31/6.89 % (4033806)CaDiCaL version: 2.1.3 % 40.31/6.89 % (4033806)Termination reason: Instruction limit % 40.31/6.89 % (4033806)Termination phase: Saturation % 40.31/6.89 % (4033806)Time elapsed: 0.297 s % 40.31/6.89 % (4033806)Peak memory usage: 117 MB % 40.31/6.89 % (4033806)Instructions burned: 261 (million) % 40.31/6.89 % (4033812)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3248019097:i=146:doe=on:rtra=on_2956 on theBenchmark for (2956ds/146Mi) % 40.31/6.89 % (4033813)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3321801455:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi) % 40.31/6.89 % (4033815)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=1890231266:avsq=on:i=276:avsqr=1,2:rtra=on_2955 on theBenchmark for (2955ds/276Mi) % 40.31/6.89 % (4033805)Instruction limit reached! % 47.14/7.80 % (4033805)------------------------------ % 47.14/7.80 % (4033805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.14/7.80 % (4033805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.14/7.80 % (4033805)CaDiCaL version: 2.1.3 % 47.14/7.80 % (4033805)Termination reason: Instruction limit % 47.14/7.80 % (4033805)Termination phase: Saturation % 47.14/7.80 % (4033805)Time elapsed: 0.399 s % 47.14/7.80 % (4033805)Peak memory usage: 119 MB % 47.14/7.80 % (4033805)Instructions burned: 341 (million) % 47.14/7.80 % (4033817)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=104381780:i=1052:rtra=on_2954 on theBenchmark for (2954ds/1052Mi) % 47.14/7.80 % (4033808)Instruction limit reached! % 47.14/7.80 % (4033808)------------------------------ % 47.14/7.80 % (4033808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.14/7.80 % (4033808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.14/7.80 % (4033808)CaDiCaL version: 2.1.3 % 47.14/7.80 % (4033808)Termination reason: Instruction limit % 47.14/7.80 % (4033808)Termination phase: Saturation % 47.14/7.80 % (4033808)Time elapsed: 0.292 s % 47.14/7.80 % (4033808)Peak memory usage: 91 MB % 47.14/7.80 % (4033808)Instructions burned: 274 (million) % 47.14/7.80 % (4033812)Instruction limit reached! % 47.14/7.80 % (4033812)------------------------------ % 47.14/7.80 % (4033812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.14/7.80 % (4033812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.14/7.80 % (4033812)CaDiCaL version: 2.1.3 % 47.14/7.80 % (4033812)Termination reason: Instruction limit % 47.14/7.80 % (4033812)Termination phase: Saturation % 47.14/7.80 % (4033812)Time elapsed: 0.153 s % 47.14/7.80 % (4033812)Peak memory usage: 90 MB % 47.14/7.80 % (4033812)Instructions burned: 146 (million) % 47.14/7.80 % (4033818)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=368758011:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/655Mi) % 47.14/7.80 % (4033822)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4022411338:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2952 on theBenchmark for (2952ds/1054Mi) % 47.14/7.80 % (4033825)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2768062532:i=107:rtra=on_2952 on theBenchmark for (2952ds/107Mi) % 47.14/7.80 % (4033826)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=628344104:s2a=on:i=450:doe=on:nm=32:rtra=on_2951 on theBenchmark for (2951ds/450Mi) % 47.14/7.80 % (4033825)Refutation not found, incomplete strategy % 47.14/7.80 % (4033825)------------------------------ % 47.14/7.80 % (4033825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.14/7.80 % (4033825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.14/7.80 % (4033825)CaDiCaL version: 2.1.3 % 47.14/7.80 % (4033825)Termination reason: Refutation not found, incomplete strategy % 47.14/7.80 % (4033825)Time elapsed: 0.050 s % 47.14/7.80 % (4033825)Peak memory usage: 115 MB % 47.14/7.80 % (4033825)Instructions burned: 16 (million) % 47.14/7.80 % (4033815)Instruction limit reached! % 47.14/7.80 % (4033815)------------------------------ % 47.14/7.80 % (4033815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.14/7.80 % (4033815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.14/7.80 % (4033815)CaDiCaL version: 2.1.3 % 47.14/7.80 % (4033815)Termination reason: Instruction limit % 47.14/7.80 % (4033815)Termination phase: Saturation % 47.14/7.80 % (4033815)Time elapsed: 0.361 s % 47.14/7.80 % (4033815)Peak memory usage: 135 MB % 47.14/7.80 % (4033815)Instructions burned: 277 (million) % 47.14/7.80 % (4033817)Instruction limit reached! % 47.14/7.80 % (4033817)------------------------------ % 47.14/7.80 % (4033817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.14/7.80 % (4033817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.14/7.80 % (4033817)CaDiCaL version: 2.1.3 % 47.14/7.80 % (4033817)Termination reason: Instruction limit % 47.14/7.80 % (4033817)Termination phase: Saturation % 47.14/7.80 % (4033817)Time elapsed: 0.470 s % 47.14/7.80 % (4033817)Peak memory usage: 92 MB % 47.14/7.80 % (4033817)Instructions burned: 1052 (million) % 47.14/7.80 % (4033831)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 % 53.03/8.45 % (4033831)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2233316312:i=1090:aac=none:nm=0:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/1090Mi) % 53.03/8.45 % (4033826)Instruction limit reached! % 53.03/8.45 % (4033826)------------------------------ % 53.03/8.45 % (4033826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.03/8.45 % (4033826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.03/8.45 % (4033826)CaDiCaL version: 2.1.3 % 53.03/8.45 % (4033826)Termination reason: Instruction limit % 53.03/8.45 % (4033826)Termination phase: Saturation % 53.03/8.45 % (4033826)Time elapsed: 0.386 s % 53.03/8.45 % (4033826)Peak memory usage: 133 MB % 53.03/8.45 % (4033826)Instructions burned: 450 (million) % 53.03/8.45 % (4033825)------------------------------ % 53.03/8.45 % (4033825)------------------------------ % 53.03/8.45 % (4033832)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1886784814:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2948 on theBenchmark for (2948ds/130Mi) % 53.03/8.45 % (4033818)Instruction limit reached! % 53.03/8.45 % (4033818)------------------------------ % 53.03/8.45 % (4033818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.03/8.45 % (4033818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.03/8.45 % (4033818)CaDiCaL version: 2.1.3 % 53.03/8.45 % (4033818)Termination reason: Instruction limit % 53.03/8.45 % (4033818)Termination phase: Saturation % 53.03/8.45 % (4033818)Time elapsed: 0.622 s % 53.03/8.45 % (4033818)Peak memory usage: 93 MB % 53.03/8.45 % (4033818)Instructions burned: 655 (million) % 53.03/8.45 % (4033835)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=722598525:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 53.03/8.45 % (4033835)Refutation not found, incomplete strategy % 53.03/8.45 % (4033835)------------------------------ % 53.03/8.45 % (4033835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.03/8.45 % (4033835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.03/8.45 % (4033835)CaDiCaL version: 2.1.3 % 53.03/8.45 % (4033835)Termination reason: Refutation not found, incomplete strategy % 53.03/8.45 % (4033835)Time elapsed: 0.008 s % 53.03/8.45 % (4033835)Peak memory usage: 89 MB % 53.03/8.45 % (4033835)Instructions burned: 9 (million) % 53.03/8.45 % (4033834)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3530080154:i=312:kws=inv_frequency:nm=20:rtra=on_2946 on theBenchmark for (2946ds/312Mi) % 53.03/8.45 % (4033832)Instruction limit reached! % 53.03/8.45 % (4033832)------------------------------ % 53.03/8.45 % (4033832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.03/8.45 % (4033832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.03/8.45 % (4033832)CaDiCaL version: 2.1.3 % 53.03/8.45 % (4033832)Termination reason: Instruction limit % 53.03/8.45 % (4033832)Termination phase: Saturation % 53.03/8.45 % (4033832)Time elapsed: 0.160 s % 53.03/8.45 % (4033832)Peak memory usage: 117 MB % 53.03/8.45 % (4033832)Instructions burned: 130 (million) % 53.03/8.45 % (4033837)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1219187217:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 53.03/8.45 % (4033835)------------------------------ % 53.03/8.45 % (4033835)------------------------------ % 53.03/8.45 % (4033831)Instruction limit reached! % 53.03/8.45 % (4033831)------------------------------ % 53.03/8.45 % (4033831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.03/8.45 % (4033831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.03/8.45 % (4033831)CaDiCaL version: 2.1.3 % 53.03/8.45 % (4033831)Termination reason: Instruction limit % 53.03/8.45 % (4033831)Termination phase: Saturation % 53.03/8.45 % (4033831)Time elapsed: 0.560 s % 53.03/8.45 % (4033831)Peak memory usage: 120 MB % 53.03/8.45 % (4033831)Instructions burned: 1091 (million) % 53.03/8.45 % (4033840)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=548579766:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2943 on theBenchmark for (2943ds/307Mi) % 53.03/8.45 % (4033840)Refutation not found, incomplete strategy % 53.03/8.45 % (4033840)------------------------------ % 53.03/8.45 % (4033840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.66/9.17 % (4033840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.66/9.17 % (4033840)CaDiCaL version: 2.1.3 % 55.66/9.17 % (4033840)Termination reason: Refutation not found, incomplete strategy % 55.66/9.17 % (4033840)Time elapsed: 0.018 s % 55.66/9.17 % (4033840)Peak memory usage: 89 MB % 55.66/9.17 % (4033840)Instructions burned: 15 (million) % 55.66/9.17 % (4033822)Instruction limit reached! % 55.66/9.17 % (4033822)------------------------------ % 55.66/9.17 % (4033822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.66/9.17 % (4033822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.66/9.17 % (4033822)CaDiCaL version: 2.1.3 % 55.66/9.17 % (4033822)Termination reason: Instruction limit % 55.66/9.17 % (4033822)Termination phase: Saturation % 55.66/9.17 % (4033822)Time elapsed: 1.0000 s % 55.66/9.17 % (4033822)Peak memory usage: 96 MB % 55.66/9.17 % (4033822)Instructions burned: 1054 (million) % 55.66/9.17 % (4033834)Instruction limit reached! % 55.66/9.17 % (4033834)------------------------------ % 55.66/9.17 % (4033834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.66/9.17 % (4033834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.66/9.17 % (4033834)CaDiCaL version: 2.1.3 % 55.66/9.17 % (4033834)Termination reason: Instruction limit % 55.66/9.17 % (4033834)Termination phase: Saturation % 55.66/9.17 % (4033834)Time elapsed: 0.361 s % 55.66/9.17 % (4033834)Peak memory usage: 118 MB % 55.66/9.17 % (4033834)Instructions burned: 313 (million) % 55.66/9.17 % (4033844)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4190030264:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 55.66/9.17 % (4033843)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3048628341:i=776:doe=on:rtra=on_2941 on theBenchmark for (2941ds/776Mi) % 55.66/9.17 % (4033846)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=3036485171:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2940 on theBenchmark for (2940ds/784Mi) % 55.66/9.17 % (4033847)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=1963415739:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2940 on theBenchmark for (2940ds/1131Mi) % 55.66/9.17 % (4033840)------------------------------ % 55.66/9.17 % (4033840)------------------------------ % 55.66/9.17 % (4033837)Instruction limit reached! % 55.66/9.17 % (4033837)------------------------------ % 55.66/9.17 % (4033837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.66/9.17 % (4033837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.66/9.17 % (4033837)CaDiCaL version: 2.1.3 % 55.66/9.17 % (4033837)Termination reason: Instruction limit % 55.66/9.17 % (4033837)Termination phase: Saturation % 55.66/9.17 % (4033837)Time elapsed: 0.669 s % 55.66/9.17 % (4033837)Peak memory usage: 94 MB % 55.66/9.17 % (4033837)Instructions burned: 835 (million) % 55.66/9.17 % (4033844)Instruction limit reached! % 55.66/9.17 % (4033844)------------------------------ % 55.66/9.17 % (4033844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.66/9.17 % (4033844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.66/9.17 % (4033844)CaDiCaL version: 2.1.3 % 55.66/9.17 % (4033844)Termination reason: Instruction limit % 55.66/9.17 % (4033844)Termination phase: Saturation % 55.66/9.17 % (4033844)Time elapsed: 0.371 s % 55.66/9.17 % (4033844)Peak memory usage: 140 MB % 55.66/9.17 % (4033844)Instructions burned: 648 (million) % 55.66/9.17 % (4033853)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=1921754351:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2936 on theBenchmark for (2936ds/246Mi) % 55.66/9.17 % (4033854)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1262122925:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/775Mi) % 55.66/9.17 % (4033855)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3023235123:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi) % 55.66/9.17 % (4033855)Instruction limit reached! % 55.66/9.17 % (4033855)------------------------------ % 55.66/9.17 % (4033855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.67/12.36 % (4033855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.67/12.36 % (4033855)CaDiCaL version: 2.1.3 % 80.67/12.36 % (4033855)Termination reason: Instruction limit % 80.67/12.36 % (4033855)Termination phase: Saturation % 80.67/12.36 % (4033855)Time elapsed: 0.147 s % 80.67/12.36 % (4033855)Peak memory usage: 92 MB % 80.67/12.36 % (4033855)Instructions burned: 274 (million) % 80.67/12.36 % (4033853)Instruction limit reached! % 80.67/12.36 % (4033853)------------------------------ % 80.67/12.36 % (4033853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.67/12.36 % (4033853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.67/12.36 % (4033853)CaDiCaL version: 2.1.3 % 80.67/12.36 % (4033853)Termination reason: Instruction limit % 80.67/12.36 % (4033853)Termination phase: Saturation % 80.67/12.36 % (4033853)Time elapsed: 0.283 s % 80.67/12.36 % (4033853)Peak memory usage: 117 MB % 80.67/12.36 % (4033853)Instructions burned: 246 (million) % 80.67/12.36 % (4033843)Instruction limit reached! % 80.67/12.36 % (4033843)------------------------------ % 80.67/12.36 % (4033843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.67/12.36 % (4033843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.67/12.36 % (4033843)CaDiCaL version: 2.1.3 % 80.67/12.36 % (4033843)Termination reason: Instruction limit % 80.67/12.36 % (4033843)Termination phase: Saturation % 80.67/12.36 % (4033843)Time elapsed: 0.782 s % 80.67/12.36 % (4033843)Peak memory usage: 123 MB % 80.67/12.36 % (4033843)Instructions burned: 776 (million) % 80.67/12.36 % (4033846)Instruction limit reached! % 80.67/12.36 % (4033846)------------------------------ % 80.67/12.36 % (4033846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.67/12.36 % (4033846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.67/12.36 % (4033846)CaDiCaL version: 2.1.3 % 80.67/12.36 % (4033846)Termination reason: Instruction limit % 80.67/12.36 % (4033846)Termination phase: Saturation % 80.67/12.36 % (4033846)Time elapsed: 0.796 s % 80.67/12.36 % (4033846)Peak memory usage: 122 MB % 80.67/12.36 % (4033846)Instructions burned: 784 (million) % 80.67/12.36 % (4033859)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=272869505:i=102:nm=16:rtra=on_2931 on theBenchmark for (2931ds/102Mi) % 80.67/12.36 % (4033861)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=487300006:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 80.67/12.36 % (4033859)Instruction limit reached! % 80.67/12.36 % (4033859)------------------------------ % 80.67/12.36 % (4033859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.67/12.36 % (4033859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.67/12.36 % (4033859)CaDiCaL version: 2.1.3 % 80.67/12.36 % (4033859)Termination reason: Instruction limit % 80.67/12.36 % (4033859)Termination phase: Saturation % 80.67/12.36 % (4033859)Time elapsed: 0.057 s % 80.67/12.36 % (4033859)Peak memory usage: 89 MB % 80.67/12.36 % (4033859)Instructions burned: 103 (million) % 80.67/12.36 % (4033860)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2968675765:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2930 on theBenchmark for (2930ds/1094Mi) % 80.67/12.36 % (4033862)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=2028654537:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/868Mi) % 80.67/12.36 % (4033865)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=8626781:i=1846:canc=cautious:fsr=off:rtra=on_2928 on theBenchmark for (2928ds/1846Mi) % 80.67/12.36 % (4033865)Refutation not found, incomplete strategy % 80.67/12.36 % (4033865)------------------------------ % 80.67/12.36 % (4033865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.67/12.36 % (4033865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.67/12.36 % (4033865)CaDiCaL version: 2.1.3 % 80.67/12.36 % (4033865)Termination reason: Refutation not found, incomplete strategy % 80.67/12.36 % (4033865)Time elapsed: 0.006 s % 80.67/12.36 % (4033865)Peak memory usage: 89 MB % 80.67/12.36 % (4033865)Instructions burned: 9 (million) % 80.67/12.36 % (4033854)Instruction limit reached! % 80.67/12.36 % (4033854)------------------------------ % 80.67/12.36 % (4033854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033847)Instruction limit reached! % 91.70/13.97 % (4033847)------------------------------ % 91.70/13.97 % (4033847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.70/13.97 % (4033847)CaDiCaL version: 2.1.3 % 91.70/13.97 % (4033854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.70/13.97 % (4033847)Termination reason: Instruction limit % 91.70/13.97 % (4033847)Termination phase: Saturation % 91.70/13.97 % (4033847)Time elapsed: 1.231 s % 91.70/13.97 % (4033854)CaDiCaL version: 2.1.3 % 91.70/13.97 % (4033847)Peak memory usage: 128 MB % 91.70/13.97 % (4033847)Instructions burned: 1131 (million) % 91.70/13.97 % (4033854)Termination reason: Instruction limit % 91.70/13.97 % (4033854)Termination phase: Saturation % 91.70/13.97 % (4033854)Time elapsed: 0.822 s % 91.70/13.97 % (4033854)Peak memory usage: 96 MB % 91.70/13.97 % (4033854)Instructions burned: 776 (million) % 91.70/13.97 % (4033865)------------------------------ % 91.70/13.97 % (4033865)------------------------------ % 91.70/13.97 % (4033871)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=2215631737:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2924 on theBenchmark for (2924ds/863Mi) % 91.70/13.97 % (4033869)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2670757979:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2924 on theBenchmark for (2924ds/36816Mi) % 91.70/13.97 % (4033870)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3705313985:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2924 on theBenchmark for (2924ds/273Mi) % 91.70/13.97 % (4033860)Instruction limit reached! % 91.70/13.97 % (4033860)------------------------------ % 91.70/13.97 % (4033860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.70/13.97 % (4033860)CaDiCaL version: 2.1.3 % 91.70/13.97 % (4033860)Termination reason: Instruction limit % 91.70/13.97 % (4033860)Termination phase: Saturation % 91.70/13.97 % (4033860)Time elapsed: 0.765 s % 91.70/13.97 % (4033860)Peak memory usage: 91 MB % 91.70/13.97 % (4033860)Instructions burned: 1094 (million) % 91.70/13.97 % (4033870)Instruction limit reached! % 91.70/13.97 % (4033870)------------------------------ % 91.70/13.97 % (4033870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.70/13.97 % (4033870)CaDiCaL version: 2.1.3 % 91.70/13.97 % (4033870)Termination reason: Instruction limit % 91.70/13.97 % (4033870)Termination phase: Saturation % 91.70/13.97 % (4033870)Time elapsed: 0.288 s % 91.70/13.97 % (4033870)Peak memory usage: 92 MB % 91.70/13.97 % (4033870)Instructions burned: 274 (million) % 91.70/13.97 % (4033862)Instruction limit reached! % 91.70/13.97 % (4033862)------------------------------ % 91.70/13.97 % (4033862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.70/13.97 % (4033862)CaDiCaL version: 2.1.3 % 91.70/13.97 % (4033862)Termination reason: Instruction limit % 91.70/13.97 % (4033862)Termination phase: Saturation % 91.70/13.97 % (4033862)Time elapsed: 0.821 s % 91.70/13.97 % (4033862)Peak memory usage: 119 MB % 91.70/13.97 % (4033862)Instructions burned: 870 (million) % 91.70/13.97 % (4033813)Instruction limit reached! % 91.70/13.97 % (4033813)------------------------------ % 91.70/13.97 % (4033813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.70/13.97 % (4033813)CaDiCaL version: 2.1.3 % 91.70/13.97 % (4033813)Termination reason: Instruction limit % 91.70/13.97 % (4033813)Termination phase: Saturation % 91.70/13.97 % (4033813)Time elapsed: 3.549 s % 91.70/13.97 % (4033813)Peak memory usage: 106 MB % 91.70/13.97 % (4033813)Instructions burned: 4429 (million) % 91.70/13.97 % (4033875)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2258194276:i=5811:kws=precedence:nm=0:rtra=on_2920 on theBenchmark for (2920ds/5811Mi) % 91.70/13.97 % (4033871)Instruction limit reached! % 91.70/13.97 % (4033871)------------------------------ % 91.70/13.97 % (4033871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.70/13.97 % (4033871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.27/18.32 % (4033871)CaDiCaL version: 2.1.3 % 123.27/18.32 % (4033871)Termination reason: Instruction limit % 123.27/18.32 % (4033871)Termination phase: Saturation % 123.27/18.32 % (4033871)Time elapsed: 0.463 s % 123.27/18.32 % (4033871)Peak memory usage: 119 MB % 123.27/18.32 % (4033871)Instructions burned: 864 (million) % 123.27/18.32 % (4033877)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=77744968:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2919 on theBenchmark for (2919ds/2216Mi) % 123.27/18.32 % (4033878)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=613227949:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2919 on theBenchmark for (2919ds/801Mi) % 123.27/18.32 % (4033881)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3312739308:i=3509:rtra=on_2917 on theBenchmark for (2917ds/3509Mi) % 123.27/18.32 % (4033879)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=836720649:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2917 on theBenchmark for (2917ds/1026Mi) % 123.27/18.32 % (4033878)Instruction limit reached! % 123.27/18.32 % (4033878)------------------------------ % 123.27/18.32 % (4033878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.27/18.32 % (4033878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.27/18.32 % (4033878)CaDiCaL version: 2.1.3 % 123.27/18.32 % (4033878)Termination reason: Instruction limit % 123.27/18.32 % (4033878)Termination phase: Saturation % 123.27/18.32 % (4033878)Time elapsed: 0.786 s % 123.27/18.32 % (4033878)Peak memory usage: 94 MB % 123.27/18.32 % (4033878)Instructions burned: 802 (million) % 123.27/18.32 % (4033877)Instruction limit reached! % 123.27/18.32 % (4033877)------------------------------ % 123.27/18.32 % (4033877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.27/18.32 % (4033877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.27/18.32 % (4033877)CaDiCaL version: 2.1.3 % 123.27/18.32 % (4033877)Termination reason: Instruction limit % 123.27/18.32 % (4033877)Termination phase: Saturation % 123.27/18.32 % (4033877)Time elapsed: 1.039 s % 123.27/18.32 % (4033877)Peak memory usage: 124 MB % 123.27/18.32 % (4033877)Instructions burned: 2217 (million) % 123.27/18.32 % (4033887)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1684461850:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2908 on theBenchmark for (2908ds/2127Mi) % 123.27/18.32 % (4033888)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3084798712:i=1959:rtra=on:fsd=on:proc=on_2906 on theBenchmark for (2906ds/1959Mi) % 123.27/18.32 % (4033879)Instruction limit reached! % 123.27/18.32 % (4033879)------------------------------ % 123.27/18.32 % (4033879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.27/18.32 % (4033879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.27/18.32 % (4033879)CaDiCaL version: 2.1.3 % 123.27/18.32 % (4033879)Termination reason: Instruction limit % 123.27/18.32 % (4033879)Termination phase: Saturation % 123.27/18.32 % (4033879)Time elapsed: 1.049 s % 123.27/18.32 % (4033879)Peak memory usage: 96 MB % 123.27/18.32 % (4033879)Instructions burned: 1026 (million) % 123.27/18.32 % (4033891)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=164494043:s2a=on:i=3553:nm=0:rtra=on_2904 on theBenchmark for (2904ds/3553Mi) % 123.27/18.32 % (4033888)Instruction limit reached! % 123.27/18.32 % (4033888)------------------------------ % 123.27/18.32 % (4033888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.27/18.32 % (4033888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.27/18.32 % (4033888)CaDiCaL version: 2.1.3 % 123.27/18.32 % (4033888)Termination reason: Instruction limit % 123.27/18.32 % (4033888)Termination phase: Saturation % 123.27/18.32 % (4033888)Time elapsed: 0.907 s % 123.27/18.32 % (4033888)Peak memory usage: 122 MB % 123.27/18.32 % (4033888)Instructions burned: 1960 (million) % 123.27/18.32 % (4033893)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2092955264:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2895 on theBenchmark for (2895ds/3201Mi) % 123.27/18.32 % (4033887)Instruction limit reached! % 123.27/18.32 % (4033887)------------------------------ % 123.27/18.32 % (4033887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.27/18.32 % (4033887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.07/20.70 % (4033887)CaDiCaL version: 2.1.3 % 140.07/20.70 % (4033887)Termination reason: Instruction limit % 140.07/20.70 % (4033887)Termination phase: Saturation % 140.07/20.70 % (4033887)Time elapsed: 1.970 s % 140.07/20.70 % (4033887)Peak memory usage: 108 MB % 140.07/20.70 % (4033887)Instructions burned: 2127 (million) % 140.07/20.70 % (4033881)Instruction limit reached! % 140.07/20.70 % (4033881)------------------------------ % 140.07/20.70 % (4033881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.07/20.70 % (4033881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.07/20.70 % (4033881)CaDiCaL version: 2.1.3 % 140.07/20.70 % (4033881)Termination reason: Instruction limit % 140.07/20.70 % (4033881)Termination phase: Saturation % 140.07/20.70 % (4033881)Time elapsed: 3.064 s % 140.07/20.70 % (4033881)Peak memory usage: 108 MB % 140.07/20.70 % (4033881)Instructions burned: 3509 (million) % 140.07/20.70 % (4033897)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=2205133493:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2885 on theBenchmark for (2885ds/4093Mi) % 140.07/20.70 % (4033898)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=3839860614:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2884 on theBenchmark for (2884ds/21173Mi) % 140.07/20.70 % (4033893)Instruction limit reached! % 140.07/20.70 % (4033893)------------------------------ % 140.07/20.70 % (4033893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.07/20.70 % (4033893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.07/20.70 % (4033893)CaDiCaL version: 2.1.3 % 140.07/20.70 % (4033893)Termination reason: Instruction limit % 140.07/20.70 % (4033893)Termination phase: Saturation % 140.07/20.70 % (4033893)Time elapsed: 1.247 s % 140.07/20.70 % (4033893)Peak memory usage: 98 MB % 140.07/20.70 % (4033893)Instructions burned: 3202 (million) % 140.07/20.70 % (4033903)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=429579927:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2880 on theBenchmark for (2880ds/10544Mi) % 140.07/20.70 % (4033861)Instruction limit reached! % 140.07/20.70 % (4033861)------------------------------ % 140.07/20.70 % (4033861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.07/20.70 % (4033861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.07/20.70 % (4033861)CaDiCaL version: 2.1.3 % 140.07/20.70 % (4033861)Termination reason: Instruction limit % 140.07/20.70 % (4033861)Termination phase: Saturation % 140.07/20.70 % (4033861)Time elapsed: 5.038 s % 140.07/20.70 % (4033861)Peak memory usage: 113 MB % 140.07/20.70 % (4033861)Instructions burned: 6400 (million) % 140.07/20.70 % (4033905)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=942004903:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/1262Mi) % 140.07/20.70 % (4033905)Instruction limit reached! % 140.07/20.70 % (4033905)------------------------------ % 140.07/20.70 % (4033905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.07/20.70 % (4033905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.07/20.70 % (4033905)CaDiCaL version: 2.1.3 % 140.07/20.70 % (4033905)Termination reason: Instruction limit % 140.07/20.70 % (4033905)Termination phase: Saturation % 140.07/20.70 % (4033905)Time elapsed: 0.374 s % 140.07/20.70 % (4033905)Peak memory usage: 120 MB % 140.07/20.70 % (4033905)Instructions burned: 1267 (million) % 140.07/20.70 % (4034020)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2253128016:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2873 on theBenchmark for (2873ds/775Mi) % 140.07/20.70 % (4033891)Instruction limit reached! % 140.07/20.70 % (4033891)------------------------------ % 140.07/20.70 % (4033891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.07/20.70 % (4033891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.07/20.70 % (4033891)CaDiCaL version: 2.1.3 % 140.07/20.70 % (4033891)Termination reason: Instruction limit % 140.07/20.70 % (4033891)Termination phase: Saturation % 140.07/20.70 % (4033891)Time elapsed: 3.129 s % 140.07/20.70 % (4033891)Peak memory usage: 104 MB % 140.07/20.70 % (4033891)Instructions burned: 3554 (million) % 140.07/20.70 % (4034020)Instruction limit reached! % 140.07/20.70 % (4034020)------------------------------ % 157.57/23.13 % (4034020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.57/23.13 % (4034020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.57/23.13 % (4034020)CaDiCaL version: 2.1.3 % 157.57/23.13 % (4034020)Termination reason: Instruction limit % 157.57/23.13 % (4034020)Termination phase: Saturation % 157.57/23.13 % (4034020)Time elapsed: 0.278 s % 157.57/23.13 % (4034020)Peak memory usage: 96 MB % 157.57/23.13 % (4034020)Instructions burned: 775 (million) % 157.57/23.13 % (4033875)Instruction limit reached! % 157.57/23.13 % (4033875)------------------------------ % 157.57/23.13 % (4033875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.57/23.13 % (4033875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.57/23.13 % (4033875)CaDiCaL version: 2.1.3 % 157.57/23.13 % (4033875)Termination reason: Instruction limit % 157.57/23.13 % (4033875)Termination phase: Saturation % 157.57/23.13 % (4033875)Time elapsed: 4.808 s % 157.57/23.13 % (4033875)Peak memory usage: 131 MB % 157.57/23.13 % (4033875)Instructions burned: 5811 (million) % 157.57/23.13 % (4034063)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1257442231:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2869 on theBenchmark for (2869ds/17165Mi) % 157.57/23.13 % (4034062)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=887564830:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2869 on theBenchmark for (2869ds/270Mi) % 157.57/23.13 % (4034064)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1107973140:s2a=on:i=13094:s2at=-1:rtra=on_2869 on theBenchmark for (2869ds/13094Mi) % 157.57/23.13 % (4034062)Instruction limit reached! % 157.57/23.13 % (4034062)------------------------------ % 157.57/23.13 % (4034062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.57/23.13 % (4034062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.57/23.13 % (4034062)CaDiCaL version: 2.1.3 % 157.57/23.13 % (4034062)Termination reason: Instruction limit % 157.57/23.13 % (4034062)Termination phase: Saturation % 157.57/23.13 % (4034062)Time elapsed: 0.167 s % 157.57/23.13 % (4034062)Peak memory usage: 91 MB % 157.57/23.13 % (4034062)Instructions burned: 270 (million) % 157.57/23.13 % (4034068)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1580519198:st=2:i=12633:rtra=on:ss=axioms_2866 on theBenchmark for (2866ds/12633Mi) % 157.57/23.13 % (4033897)Instruction limit reached! % 157.57/23.13 % (4033897)------------------------------ % 157.57/23.13 % (4033897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.57/23.13 % (4033897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.57/23.13 % (4033897)CaDiCaL version: 2.1.3 % 157.57/23.13 % (4033897)Termination reason: Instruction limit % 157.57/23.13 % (4033897)Termination phase: Saturation % 157.57/23.13 % (4033897)Time elapsed: 2.194 s % 157.57/23.13 % (4033897)Peak memory usage: 140 MB % 157.57/23.13 % (4033897)Instructions burned: 4093 (million) % 157.57/23.13 % (4034070)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1266928831:i=1783:rtra=on:gtg=position_2860 on theBenchmark for (2860ds/1783Mi) % 157.57/23.13 % (4034070)Instruction limit reached! % 157.57/23.13 % (4034070)------------------------------ % 157.57/23.13 % (4034070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.57/23.13 % (4034070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.57/23.13 % (4034070)CaDiCaL version: 2.1.3 % 157.57/23.13 % (4034070)Termination reason: Instruction limit % 157.57/23.13 % (4034070)Termination phase: Saturation % 157.57/23.13 % (4034070)Time elapsed: 1.062 s % 157.57/23.13 % (4034070)Peak memory usage: 123 MB % 157.57/23.13 % (4034070)Instructions burned: 1784 (million) % 157.57/23.13 % (4034072)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=1318172949:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2848 on theBenchmark for (2848ds/5451Mi) % 157.57/23.13 % (4034063)Instruction limit reached! % 157.57/23.13 % (4034063)------------------------------ % 157.57/23.13 % (4034063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.57/23.13 % (4034063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.57/23.13 % (4034063)CaDiCaL version: 2.1.3 % 157.57/23.13 % (4034063)Termination reason: Instruction limit % 157.57/23.13 % (4034063)Termination phase: Saturation % 187.57/27.48 % (4034063)Time elapsed: 4.231 s % 187.57/27.48 % (4034063)Peak memory usage: 159 MB % 187.57/27.48 % (4034063)Instructions burned: 17168 (million) % 187.57/27.48 % (4034074)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=2090420895:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2826 on theBenchmark for (2826ds/4975Mi) % 187.57/27.48 % (4034072)Instruction limit reached! % 187.57/27.48 % (4034072)------------------------------ % 187.57/27.48 % (4034072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.57/27.48 % (4034072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.57/27.48 % (4034072)CaDiCaL version: 2.1.3 % 187.57/27.48 % (4034072)Termination reason: Instruction limit % 187.57/27.48 % (4034072)Termination phase: Saturation % 187.57/27.48 % (4034072)Time elapsed: 2.870 s % 187.57/27.48 % (4034072)Peak memory usage: 129 MB % 187.57/27.48 % (4034072)Instructions burned: 5451 (million) % 187.57/27.48 % (4034076)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=2326286343:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2818 on theBenchmark for (2818ds/2076Mi) % 187.57/27.48 % (4033903)Instruction limit reached! % 187.57/27.48 % (4033903)------------------------------ % 187.57/27.48 % (4033903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.57/27.48 % (4033903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.57/27.48 % (4033903)CaDiCaL version: 2.1.3 % 187.57/27.48 % (4033903)Termination reason: Instruction limit % 187.57/27.48 % (4033903)Termination phase: Saturation % 187.57/27.48 % (4033903)Time elapsed: 6.854 s % 187.57/27.48 % (4033903)Peak memory usage: 187 MB % 187.57/27.48 % (4033903)Instructions burned: 10544 (million) % 187.57/27.48 % (4034074)Instruction limit reached! % 187.57/27.48 % (4034074)------------------------------ % 187.57/27.48 % (4034074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.57/27.48 % (4034074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.57/27.48 % (4034074)CaDiCaL version: 2.1.3 % 187.57/27.48 % (4034074)Termination reason: Instruction limit % 187.57/27.48 % (4034074)Termination phase: Saturation % 187.57/27.48 % (4034074)Time elapsed: 1.439 s % 187.57/27.48 % (4034074)Peak memory usage: 127 MB % 187.57/27.48 % (4034074)Instructions burned: 4976 (million) % 187.57/27.48 % (4034068)Instruction limit reached! % 187.57/27.48 % (4034068)------------------------------ % 187.57/27.48 % (4034068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.57/27.48 % (4034068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.57/27.48 % (4034068)CaDiCaL version: 2.1.3 % 187.57/27.48 % (4034068)Termination reason: Instruction limit % 187.57/27.48 % (4034068)Termination phase: Saturation % 187.57/27.48 % (4034068)Time elapsed: 5.532 s % 187.57/27.48 % (4034068)Peak memory usage: 129 MB % 187.57/27.48 % (4034068)Instructions burned: 12633 (million) % 187.57/27.48 % (4034079)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2860079528:i=3509:rtra=on_2810 on theBenchmark for (2810ds/3509Mi) % 187.57/27.48 % (4034078)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3654845426:i=5145:rtra=on_2810 on theBenchmark for (2810ds/5145Mi) % 187.57/27.48 % (4034080)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1189826246:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2809 on theBenchmark for (2809ds/13800Mi) % 187.57/27.48 % (4034076)Instruction limit reached! % 187.57/27.48 % (4034076)------------------------------ % 187.57/27.48 % (4034076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.57/27.48 % (4034076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.57/27.48 % (4034076)CaDiCaL version: 2.1.3 % 187.57/27.48 % (4034076)Termination reason: Instruction limit % 187.57/27.48 % (4034076)Termination phase: Saturation % 187.57/27.48 % (4034076)Time elapsed: 1.143 s % 187.57/27.48 % (4034076)Peak memory usage: 124 MB % 187.57/27.48 % (4034076)Instructions burned: 2076 (million) % 187.57/27.48 % (4034084)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3193901977:i=1412:rtra=on:fsd=on:proc=on_2804 on theBenchmark for (2804ds/1412Mi) % 187.57/27.48 % (4034064)Instruction limit reached! % 187.57/27.48 % (4034064)------------------------------ % 187.57/27.48 % (4034064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.57/27.48 % (4034064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.11/40.88 % (4034064)CaDiCaL version: 2.1.3 % 283.11/40.88 % (4034064)Termination reason: Instruction limit % 283.11/40.88 % (4034064)Termination phase: Saturation % 283.11/40.88 % (4034064)Time elapsed: 6.551 s % 283.11/40.88 % (4034064)Peak memory usage: 111 MB % 283.11/40.88 % (4034064)Instructions burned: 13096 (million) % 283.11/40.88 % (4034086)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 % 283.11/40.88 % (4034086)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4110024873:i=11747:aac=none:nm=0:rtra=on:rawr=on_2802 on theBenchmark for (2802ds/11747Mi) % 283.11/40.88 % (4034079)Instruction limit reached! % 283.11/40.88 % (4034079)------------------------------ % 283.11/40.88 % (4034079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.11/40.88 % (4034079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.11/40.88 % (4034079)CaDiCaL version: 2.1.3 % 283.11/40.88 % (4034079)Termination reason: Instruction limit % 283.11/40.88 % (4034079)Termination phase: Saturation % 283.11/40.88 % (4034079)Time elapsed: 1.057 s % 283.11/40.88 % (4034079)Peak memory usage: 106 MB % 283.11/40.88 % (4034079)Instructions burned: 3512 (million) % 283.11/40.88 % (4034088)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=657811242:s2a=on:i=3553:nm=0:rtra=on_2798 on theBenchmark for (2798ds/3553Mi) % 283.11/40.88 % (4034084)Instruction limit reached! % 283.11/40.88 % (4034084)------------------------------ % 283.11/40.88 % (4034084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.11/40.88 % (4034084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.11/40.88 % (4034084)CaDiCaL version: 2.1.3 % 283.11/40.88 % (4034084)Termination reason: Instruction limit % 283.11/40.88 % (4034084)Termination phase: Saturation % 283.11/40.88 % (4034084)Time elapsed: 0.821 s % 283.11/40.88 % (4034084)Peak memory usage: 121 MB % 283.11/40.88 % (4034084)Instructions burned: 1413 (million) % 283.11/40.88 % (4034090)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=264589562:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2794 on theBenchmark for (2794ds/3201Mi) % 283.11/40.88 % (4034088)Instruction limit reached! % 283.11/40.88 % (4034088)------------------------------ % 283.11/40.88 % (4034088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.11/40.88 % (4034088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.11/40.88 % (4034088)CaDiCaL version: 2.1.3 % 283.11/40.88 % (4034088)Termination reason: Instruction limit % 283.11/40.88 % (4034088)Termination phase: Saturation % 283.11/40.88 % (4034088)Time elapsed: 1.276 s % 283.11/40.88 % (4034088)Peak memory usage: 106 MB % 283.11/40.88 % (4034088)Instructions burned: 3554 (million) % 283.11/40.88 % (4034092)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=2296054649:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2784 on theBenchmark for (2784ds/4081Mi) % 283.11/40.88 % (4034078)Instruction limit reached! % 283.11/40.88 % (4034078)------------------------------ % 283.11/40.88 % (4034078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.11/40.88 % (4034078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.11/40.88 % (4034078)CaDiCaL version: 2.1.3 % 283.11/40.88 % (4034078)Termination reason: Instruction limit % 283.11/40.88 % (4034078)Termination phase: Saturation % 283.11/40.88 % (4034078)Time elapsed: 2.825 s % 283.11/40.88 % (4034078)Peak memory usage: 101 MB % 283.11/40.88 % (4034078)Instructions burned: 5146 (million) % 283.11/40.88 % (4034094)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=3013717161:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2781 on theBenchmark for (2781ds/20260Mi) % 283.11/40.88 % (4034090)Instruction limit reached! % 283.11/40.88 % (4034090)------------------------------ % 283.11/40.88 % (4034090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.11/40.88 % (4034090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.11/40.88 % (4034090)CaDiCaL version: 2.1.3 % 283.11/40.88 % (4034090)Termination reason: Instruction limit % 283.11/40.88 % (4034090)Termination phase: Saturation % 283.11/40.88 % Terminated %------------------------------------------------------------------------------