%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX111_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:54 PM UTC 2026 % Result : Timeout 300.39s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX111_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.17 % Computer : n026.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 15:04:27 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.06/0.21 Running first-order theorem proving % 0.06/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.47/1.18 % (3917239)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.47/1.18 % (3917248)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2323311982:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.47/1.18 % (3917248)Instruction limit reached! % 3.47/1.18 % (3917248)------------------------------ % 3.47/1.18 % (3917248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.47/1.18 % (3917248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.47/1.18 % (3917248)CaDiCaL version: 2.1.3 % 3.47/1.18 % (3917248)Termination reason: Instruction limit % 3.47/1.18 % (3917248)Termination phase: Saturation % 3.47/1.18 % (3917248)Time elapsed: 0.003 s % 3.47/1.18 % (3917248)Peak memory usage: 89 MB % 3.47/1.18 % (3917248)Instructions burned: 6 (million) % 3.47/1.18 % (3917245)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2460230145:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.47/1.18 % (3917246)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1548887418:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.47/1.18 % (3917247)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=989309788:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.47/1.18 % (3917244)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2908655678:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.47/1.18 % (3917247)Instruction limit reached! % 3.47/1.18 % (3917247)------------------------------ % 3.47/1.18 % (3917247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.47/1.18 % (3917247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.47/1.18 % (3917247)CaDiCaL version: 2.1.3 % 3.47/1.18 % (3917247)Termination reason: Instruction limit % 3.47/1.18 % (3917247)Termination phase: Saturation % 3.47/1.18 % (3917247)Time elapsed: 0.006 s % 3.47/1.18 % (3917247)Peak memory usage: 88 MB % 3.47/1.18 % (3917247)Instructions burned: 8 (million) % 3.47/1.18 % (3917249)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1053558320:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.47/1.18 % (3917250)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=159662190:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.47/1.18 % (3917244)Instruction limit reached! % 3.47/1.18 % (3917244)------------------------------ % 3.47/1.18 % (3917244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.47/1.18 % (3917244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.47/1.18 % (3917244)CaDiCaL version: 2.1.3 % 3.47/1.18 % (3917244)Termination reason: Instruction limit % 3.47/1.18 % (3917244)Termination phase: Saturation % 3.47/1.18 % (3917244)Time elapsed: 0.032 s % 3.47/1.18 % (3917244)Peak memory usage: 115 MB % 3.47/1.18 % (3917244)Instructions burned: 13 (million) % 3.47/1.18 % (3917250)Instruction limit reached! % 3.47/1.18 % (3917250)------------------------------ % 3.47/1.18 % (3917250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.47/1.18 % (3917250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.47/1.18 % (3917250)CaDiCaL version: 2.1.3 % 3.47/1.18 % (3917250)Termination reason: Instruction limit % 3.47/1.18 % (3917250)Termination phase: Saturation % 3.47/1.18 % (3917250)Time elapsed: 0.046 s % 3.47/1.18 % (3917250)Peak memory usage: 116 MB % 3.47/1.18 % (3917250)Instructions burned: 33 (million) % 3.47/1.18 % (3917249)Instruction limit reached! % 3.47/1.18 % (3917249)------------------------------ % 3.47/1.18 % (3917249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.47/1.18 % (3917249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.47/1.18 % (3917249)CaDiCaL version: 2.1.3 % 3.47/1.18 % (3917249)Termination reason: Instruction limit % 3.47/1.18 % (3917249)Termination phase: Saturation % 3.47/1.18 % (3917249)Time elapsed: 0.054 s % 3.47/1.18 % (3917249)Peak memory usage: 115 MB % 3.47/1.18 % (3917249)Instructions burned: 47 (million) % 3.47/1.18 % (3917252)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1685619959:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.47/1.18 % (3917252)Instruction limit reached! % 3.47/1.18 % (3917252)------------------------------ % 4.31/1.31 % (3917252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.31/1.31 % (3917252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.31/1.31 % (3917252)CaDiCaL version: 2.1.3 % 4.31/1.31 % (3917252)Termination reason: Instruction limit % 4.31/1.31 % (3917252)Termination phase: Saturation % 4.31/1.31 % (3917252)Time elapsed: 0.006 s % 4.31/1.31 % (3917252)Peak memory usage: 88 MB % 4.31/1.31 % (3917252)Instructions burned: 16 (million) % 4.31/1.31 % (3917259)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=3201979526:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.31/1.31 % (3917264)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3586868137:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.31/1.31 % (3917259)Instruction limit reached! % 4.31/1.31 % (3917259)------------------------------ % 4.31/1.31 % (3917259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.31/1.31 % (3917259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.31/1.31 % (3917259)CaDiCaL version: 2.1.3 % 4.31/1.31 % (3917259)Termination reason: Instruction limit % 4.31/1.31 % (3917259)Termination phase: Saturation % 4.31/1.31 % (3917259)Time elapsed: 0.024 s % 4.31/1.31 % (3917259)Peak memory usage: 89 MB % 4.31/1.31 % (3917259)Instructions burned: 29 (million) % 4.31/1.31 % (3917246)Instruction limit reached! % 4.31/1.31 % (3917246)------------------------------ % 4.31/1.31 % (3917246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.31/1.31 % (3917246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.31/1.31 % (3917246)CaDiCaL version: 2.1.3 % 4.31/1.31 % (3917246)Termination reason: Instruction limit % 4.31/1.31 % (3917246)Termination phase: Saturation % 4.31/1.31 % (3917246)Time elapsed: 0.170 s % 4.31/1.31 % (3917246)Peak memory usage: 117 MB % 4.31/1.31 % (3917246)Instructions burned: 202 (million) % 4.31/1.31 % (3917260)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4208875652:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.31/1.31 % (3917261)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3663100590:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.31/1.31 % (3917264)Instruction limit reached! % 4.31/1.31 % (3917264)------------------------------ % 4.31/1.31 % (3917264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.31/1.31 % (3917264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.31/1.31 % (3917264)CaDiCaL version: 2.1.3 % 4.31/1.31 % (3917264)Termination reason: Instruction limit % 4.31/1.31 % (3917264)Termination phase: Saturation % 4.31/1.31 % (3917264)Time elapsed: 0.022 s % 4.31/1.31 % (3917264)Peak memory usage: 88 MB % 4.31/1.31 % (3917264)Instructions burned: 88 (million) % 4.31/1.31 % (3917260)Instruction limit reached! % 4.31/1.31 % (3917260)------------------------------ % 4.31/1.31 % (3917260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.31/1.31 % (3917260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.31/1.31 % (3917260)CaDiCaL version: 2.1.3 % 4.31/1.31 % (3917260)Termination reason: Instruction limit % 4.31/1.31 % (3917260)Termination phase: Saturation % 4.31/1.31 % (3917260)Time elapsed: 0.012 s % 4.31/1.31 % (3917260)Peak memory usage: 90 MB % 4.31/1.31 % (3917260)Instructions burned: 17 (million) % 4.31/1.31 % (3917261)Instruction limit reached! % 4.31/1.31 % (3917261)------------------------------ % 4.31/1.31 % (3917261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.31/1.31 % (3917261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.31/1.31 % (3917261)CaDiCaL version: 2.1.3 % 4.31/1.31 % (3917261)Termination reason: Instruction limit % 4.31/1.31 % (3917261)Termination phase: Saturation % 4.31/1.31 % (3917261)Time elapsed: 0.020 s % 4.31/1.31 % (3917261)Peak memory usage: 89 MB % 4.31/1.31 % (3917261)Instructions burned: 25 (million) % 4.31/1.31 % (3917263)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=1815852499:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.31/1.31 % (3917263)Instruction limit reached! % 4.31/1.31 % (3917263)------------------------------ % 4.31/1.31 % (3917263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.47 % (3917263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.47 % (3917263)CaDiCaL version: 2.1.3 % 4.99/1.47 % (3917263)Termination reason: Instruction limit % 4.99/1.47 % (3917263)Termination phase: Saturation % 4.99/1.47 % (3917263)Time elapsed: 0.017 s % 4.99/1.47 % (3917263)Peak memory usage: 89 MB % 4.99/1.47 % (3917263)Instructions burned: 28 (million) % 4.99/1.47 % (3917245)Instruction limit reached! % 4.99/1.47 % (3917245)------------------------------ % 4.99/1.47 % (3917245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.47 % (3917245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.47 % (3917245)CaDiCaL version: 2.1.3 % 4.99/1.47 % (3917245)Termination reason: Instruction limit % 4.99/1.47 % (3917245)Termination phase: Saturation % 4.99/1.47 % (3917245)Time elapsed: 0.231 s % 4.99/1.47 % (3917245)Peak memory usage: 118 MB % 4.99/1.47 % (3917245)Instructions burned: 308 (million) % 4.99/1.47 % (3917271)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2562988675:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 4.99/1.47 % (3917271)Instruction limit reached! % 4.99/1.47 % (3917271)------------------------------ % 4.99/1.47 % (3917271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.47 % (3917271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.47 % (3917271)CaDiCaL version: 2.1.3 % 4.99/1.47 % (3917271)Termination reason: Instruction limit % 4.99/1.47 % (3917271)Termination phase: Saturation % 4.99/1.47 % (3917271)Time elapsed: 0.003 s % 4.99/1.47 % (3917271)Peak memory usage: 88 MB % 4.99/1.47 % (3917271)Instructions burned: 6 (million) % 4.99/1.47 % (3917269)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=138436772:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 4.99/1.47 % (3917268)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3691097139:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 4.99/1.47 % (3917268)Instruction limit reached! % 4.99/1.47 % (3917268)------------------------------ % 4.99/1.47 % (3917268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.47 % (3917268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.47 % (3917268)CaDiCaL version: 2.1.3 % 4.99/1.47 % (3917268)Termination reason: Instruction limit % 4.99/1.47 % (3917268)Termination phase: Saturation % 4.99/1.47 % (3917268)Time elapsed: 0.003 s % 4.99/1.47 % (3917268)Peak memory usage: 88 MB % 4.99/1.47 % (3917268)Instructions burned: 3 (million) % 4.99/1.47 % (3917272)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=304998937:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 4.99/1.47 % (3917274)lrs+10_1_thi=all:si=on:fd=off:random_seed=1297551063:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 4.99/1.47 % (3917275)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=1019089522:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 4.99/1.47 % (3917275)Instruction limit reached! % 4.99/1.47 % (3917275)------------------------------ % 4.99/1.47 % (3917275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.47 % (3917275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.47 % (3917275)CaDiCaL version: 2.1.3 % 4.99/1.47 % (3917275)Termination reason: Instruction limit % 4.99/1.47 % (3917275)Termination phase: Saturation % 4.99/1.47 % (3917275)Time elapsed: 0.007 s % 4.99/1.47 % (3917275)Peak memory usage: 88 MB % 4.99/1.47 % (3917275)Instructions burned: 9 (million) % 4.99/1.47 % (3917276)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1548420125:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi) % 4.99/1.47 % (3917269)Instruction limit reached! % 4.99/1.47 % (3917269)------------------------------ % 4.99/1.47 % (3917269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.47 % (3917269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.47 % (3917269)CaDiCaL version: 2.1.3 % 4.99/1.47 % (3917269)Termination reason: Instruction limit % 4.99/1.47 % (3917269)Termination phase: Saturation % 6.92/1.71 % (3917269)Time elapsed: 0.079 s % 6.92/1.71 % (3917269)Peak memory usage: 89 MB % 6.92/1.71 % (3917269)Instructions burned: 182 (million) % 6.92/1.71 % (3917276)Instruction limit reached! % 6.92/1.71 % (3917276)------------------------------ % 6.92/1.71 % (3917276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.71 % (3917276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.71 % (3917276)CaDiCaL version: 2.1.3 % 6.92/1.71 % (3917276)Termination reason: Instruction limit % 6.92/1.71 % (3917276)Termination phase: Saturation % 6.92/1.71 % (3917276)Time elapsed: 0.003 s % 6.92/1.71 % (3917276)Peak memory usage: 89 MB % 6.92/1.71 % (3917276)Instructions burned: 3 (million) % 6.92/1.71 % (3917278)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4100108405:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.92/1.71 % (3917278)Instruction limit reached! % 6.92/1.71 % (3917278)------------------------------ % 6.92/1.71 % (3917278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.71 % (3917278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.71 % (3917278)CaDiCaL version: 2.1.3 % 6.92/1.71 % (3917278)Termination reason: Instruction limit % 6.92/1.71 % (3917278)Termination phase: Saturation % 6.92/1.71 % (3917278)Time elapsed: 0.002 s % 6.92/1.71 % (3917278)Peak memory usage: 89 MB % 6.92/1.71 % (3917278)Instructions burned: 3 (million) % 6.92/1.71 % (3917274)Instruction limit reached! % 6.92/1.71 % (3917274)------------------------------ % 6.92/1.71 % (3917274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.71 % (3917274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.71 % (3917274)CaDiCaL version: 2.1.3 % 6.92/1.71 % (3917274)Termination reason: Instruction limit % 6.92/1.71 % (3917274)Termination phase: Saturation % 6.92/1.71 % (3917274)Time elapsed: 0.065 s % 6.92/1.71 % (3917274)Peak memory usage: 116 MB % 6.92/1.71 % (3917274)Instructions burned: 54 (million) % 6.92/1.71 % (3917272)Instruction limit reached! % 6.92/1.71 % (3917272)------------------------------ % 6.92/1.71 % (3917272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.71 % (3917272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.71 % (3917272)CaDiCaL version: 2.1.3 % 6.92/1.71 % (3917272)Termination reason: Instruction limit % 6.92/1.71 % (3917272)Termination phase: Saturation % 6.92/1.71 % (3917272)Time elapsed: 0.100 s % 6.92/1.71 % (3917272)Peak memory usage: 134 MB % 6.92/1.71 % (3917272)Instructions burned: 67 (million) % 6.92/1.71 % (3917281)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3691387123:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi) % 6.92/1.71 % (3917290)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3498068109:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 6.92/1.71 % (3917290)Instruction limit reached! % 6.92/1.71 % (3917290)------------------------------ % 6.92/1.71 % (3917290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.71 % (3917290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.71 % (3917290)CaDiCaL version: 2.1.3 % 6.92/1.71 % (3917290)Termination reason: Instruction limit % 6.92/1.71 % (3917290)Termination phase: Saturation % 6.92/1.71 % (3917290)Time elapsed: 0.002 s % 6.92/1.71 % (3917290)Peak memory usage: 88 MB % 6.92/1.71 % (3917290)Instructions burned: 3 (million) % 6.92/1.71 % (3917285)dis+10_1_si=on:random_seed=2064184285:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.92/1.71 % (3917287)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1420833679:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.92/1.71 % (3917287)Refutation not found, incomplete strategy % 6.92/1.71 % (3917287)------------------------------ % 6.92/1.71 % (3917287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.92/1.71 % (3917287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.92/1.71 % (3917287)CaDiCaL version: 2.1.3 % 6.92/1.71 % (3917287)Termination reason: Refutation not found, incomplete strategy % 6.92/1.71 % (3917287)Time elapsed: 0.003 s % 6.92/1.71 % (3917287)Peak memory usage: 89 MB % 6.92/1.71 % (3917287)Instructions burned: 2 (million) % 6.92/1.71 % (3917285)Instruction limit reached! % 6.92/1.71 % (3917285)------------------------------ % 6.92/1.71 % (3917285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.42/1.93 % (3917285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.42/1.93 % (3917285)CaDiCaL version: 2.1.3 % 8.42/1.93 % (3917285)Termination reason: Instruction limit % 8.42/1.93 % (3917285)Termination phase: Saturation % 8.42/1.93 % (3917285)Time elapsed: 0.009 s % 8.42/1.93 % (3917285)Peak memory usage: 88 MB % 8.42/1.93 % (3917285)Instructions burned: 11 (million) % 8.42/1.93 % (3917288)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1766936735:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi) % 8.42/1.93 % (3917291)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1639708036:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 8.42/1.93 % (3917291)Instruction limit reached! % 8.42/1.93 % (3917291)------------------------------ % 8.42/1.93 % (3917291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.42/1.93 % (3917291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.42/1.93 % (3917291)CaDiCaL version: 2.1.3 % 8.42/1.93 % (3917291)Termination reason: Instruction limit % 8.42/1.93 % (3917291)Termination phase: Saturation % 8.42/1.93 % (3917291)Time elapsed: 0.007 s % 8.42/1.93 % (3917291)Peak memory usage: 88 MB % 8.42/1.93 % (3917291)Instructions burned: 8 (million) % 8.42/1.93 % (3917281)Instruction limit reached! % 8.42/1.93 % (3917281)------------------------------ % 8.42/1.93 % (3917281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.42/1.93 % (3917281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.42/1.93 % (3917281)CaDiCaL version: 2.1.3 % 8.42/1.93 % (3917281)Termination reason: Instruction limit % 8.42/1.93 % (3917281)Termination phase: Saturation % 8.42/1.93 % (3917281)Time elapsed: 0.097 s % 8.42/1.93 % (3917281)Peak memory usage: 116 MB % 8.42/1.93 % (3917281)Instructions burned: 129 (million) % 8.42/1.93 % (3917288)Instruction limit reached! % 8.42/1.93 % (3917288)------------------------------ % 8.42/1.93 % (3917288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.42/1.93 % (3917288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.42/1.93 % (3917288)CaDiCaL version: 2.1.3 % 8.42/1.93 % (3917288)Termination reason: Instruction limit % 8.42/1.93 % (3917288)Termination phase: Saturation % 8.42/1.93 % (3917288)Time elapsed: 0.031 s % 8.42/1.93 % (3917288)Peak memory usage: 89 MB % 8.42/1.93 % (3917288)Instructions burned: 36 (million) % 8.42/1.93 % (3917293)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2995399691:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 8.42/1.93 % (3917295)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1529812552:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 8.42/1.93 % (3917295)Instruction limit reached! % 8.42/1.93 % (3917295)------------------------------ % 8.42/1.93 % (3917295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.42/1.93 % (3917295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.42/1.93 % (3917295)CaDiCaL version: 2.1.3 % 8.42/1.93 % (3917295)Termination reason: Instruction limit % 8.42/1.93 % (3917295)Termination phase: Saturation % 8.42/1.93 % (3917295)Time elapsed: 0.021 s % 8.42/1.93 % (3917295)Peak memory usage: 116 MB % 8.42/1.93 % (3917295)Instructions burned: 14 (million) % 8.42/1.93 % (3917300)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2917595833:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 8.42/1.93 % (3917302)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2826216039:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 8.42/1.93 % (3917301)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3227386230:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 8.42/1.93 % (3917301)Instruction limit reached! % 8.42/1.93 % (3917301)------------------------------ % 8.42/1.93 % (3917301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.42/1.93 % (3917301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.42/1.93 % (3917301)CaDiCaL version: 2.1.3 % 10.63/2.19 % (3917301)Termination reason: Instruction limit % 10.63/2.19 % (3917301)Termination phase: Saturation % 10.63/2.19 % (3917301)Time elapsed: 0.008 s % 10.63/2.19 % (3917301)Peak memory usage: 88 MB % 10.63/2.19 % (3917301)Instructions burned: 10 (million) % 10.63/2.19 % (3917303)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=2338614152:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 10.63/2.19 % (3917306)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=1528538412:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 10.63/2.19 % (3917303)Instruction limit reached! % 10.63/2.19 % (3917303)------------------------------ % 10.63/2.19 % (3917303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.63/2.19 % (3917303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.63/2.19 % (3917303)CaDiCaL version: 2.1.3 % 10.63/2.19 % (3917303)Termination reason: Instruction limit % 10.63/2.19 % (3917303)Termination phase: Saturation % 10.63/2.19 % (3917303)Time elapsed: 0.054 s % 10.63/2.19 % (3917303)Peak memory usage: 90 MB % 10.63/2.19 % (3917303)Instructions burned: 75 (million) % 10.63/2.19 % (3917302)Instruction limit reached! % 10.63/2.19 % (3917302)------------------------------ % 10.63/2.19 % (3917302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.63/2.19 % (3917302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.63/2.19 % (3917302)CaDiCaL version: 2.1.3 % 10.63/2.19 % (3917302)Termination reason: Instruction limit % 10.63/2.19 % (3917302)Termination phase: Saturation % 10.63/2.19 % (3917302)Time elapsed: 0.095 s % 10.63/2.19 % (3917302)Peak memory usage: 133 MB % 10.63/2.19 % (3917302)Instructions burned: 71 (million) % 10.63/2.19 % (3917287)------------------------------ % 10.63/2.19 % (3917287)------------------------------ % 10.63/2.19 % (3917293)Instruction limit reached! % 10.63/2.19 % (3917293)------------------------------ % 10.63/2.19 % (3917293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.63/2.19 % (3917293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.63/2.19 % (3917293)CaDiCaL version: 2.1.3 % 10.63/2.19 % (3917293)Termination reason: Instruction limit % 10.63/2.19 % (3917293)Termination phase: Saturation % 10.63/2.19 % (3917293)Time elapsed: 0.216 s % 10.63/2.19 % (3917293)Peak memory usage: 97 MB % 10.63/2.19 % (3917293)Instructions burned: 371 (million) % 10.63/2.19 % (3917300)Instruction limit reached! % 10.63/2.19 % (3917300)------------------------------ % 10.63/2.19 % (3917300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.63/2.19 % (3917300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.63/2.19 % (3917300)CaDiCaL version: 2.1.3 % 10.63/2.19 % (3917300)Termination reason: Instruction limit % 10.63/2.19 % (3917300)Termination phase: Saturation % 10.63/2.19 % (3917300)Time elapsed: 0.150 s % 10.63/2.19 % (3917300)Peak memory usage: 116 MB % 10.63/2.19 % (3917300)Instructions burned: 226 (million) % 10.63/2.19 % (3917310)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3457300283:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi) % 10.63/2.19 % (3917306)Instruction limit reached! % 10.63/2.19 % (3917306)------------------------------ % 10.63/2.19 % (3917306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.63/2.19 % (3917306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.63/2.19 % (3917306)CaDiCaL version: 2.1.3 % 10.63/2.19 % (3917306)Termination reason: Instruction limit % 10.63/2.19 % (3917306)Termination phase: Saturation % 10.63/2.19 % (3917306)Time elapsed: 0.109 s % 10.63/2.19 % (3917306)Peak memory usage: 90 MB % 10.63/2.19 % (3917306)Instructions burned: 297 (million) % 10.63/2.19 % (3917314)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3669173740:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 10.63/2.19 % (3917313)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3373204122:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 10.63/2.19 % (3917315)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=144348820:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi) % 10.63/2.19 % (3917319)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=3356665510:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 11.71/2.52 % (3917310)Instruction limit reached! % 11.71/2.52 % (3917310)------------------------------ % 11.71/2.52 % (3917310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.71/2.52 % (3917310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.52 % (3917310)CaDiCaL version: 2.1.3 % 11.71/2.52 % (3917310)Termination reason: Instruction limit % 11.71/2.52 % (3917310)Termination phase: Saturation % 11.71/2.52 % (3917310)Time elapsed: 0.115 s % 11.71/2.52 % (3917310)Peak memory usage: 116 MB % 11.71/2.52 % (3917310)Instructions burned: 130 (million) % 11.71/2.52 % (3917316)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2897420252:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi) % 11.71/2.52 % (3917318)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4120673883:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.71/2.52 % (3917314)Instruction limit reached! % 11.71/2.52 % (3917314)------------------------------ % 11.71/2.52 % (3917314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.71/2.52 % (3917314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.52 % (3917314)CaDiCaL version: 2.1.3 % 11.71/2.52 % (3917314)Termination reason: Instruction limit % 11.71/2.52 % (3917314)Termination phase: Saturation % 11.71/2.52 % (3917314)Time elapsed: 0.068 s % 11.71/2.52 % (3917314)Peak memory usage: 133 MB % 11.71/2.52 % (3917314)Instructions burned: 40 (million) % 11.71/2.52 % (3917319)Instruction limit reached! % 11.71/2.52 % (3917319)------------------------------ % 11.71/2.52 % (3917319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.71/2.52 % (3917319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.52 % (3917319)CaDiCaL version: 2.1.3 % 11.71/2.52 % (3917319)Termination reason: Instruction limit % 11.71/2.52 % (3917319)Termination phase: Saturation % 11.71/2.52 % (3917319)Time elapsed: 0.098 s % 11.71/2.52 % (3917319)Peak memory usage: 116 MB % 11.71/2.52 % (3917319)Instructions burned: 260 (million) % 11.71/2.52 % (3917313)Instruction limit reached! % 11.71/2.52 % (3917313)------------------------------ % 11.71/2.52 % (3917313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.71/2.52 % (3917313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.52 % (3917313)CaDiCaL version: 2.1.3 % 11.71/2.52 % (3917313)Termination reason: Instruction limit % 11.71/2.52 % (3917313)Termination phase: Saturation % 11.71/2.52 % (3917313)Time elapsed: 0.137 s % 11.71/2.52 % (3917313)Peak memory usage: 133 MB % 11.71/2.52 % (3917313)Instructions burned: 131 (million) % 11.71/2.52 % (3917318)Instruction limit reached! % 11.71/2.52 % (3917318)------------------------------ % 11.71/2.52 % (3917318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.71/2.52 % (3917318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.52 % (3917318)CaDiCaL version: 2.1.3 % 11.71/2.52 % (3917318)Termination reason: Instruction limit % 11.71/2.52 % (3917318)Termination phase: Saturation % 11.71/2.52 % (3917318)Time elapsed: 0.098 s % 11.71/2.52 % (3917318)Peak memory usage: 117 MB % 11.71/2.52 % (3917318)Instructions burned: 131 (million) % 11.71/2.52 % (3917325)dis+10_1_si=on:random_seed=2790241696:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.71/2.52 % (3917315)Instruction limit reached! % 11.71/2.52 % (3917315)------------------------------ % 11.71/2.52 % (3917315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.71/2.52 % (3917315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.52 % (3917315)CaDiCaL version: 2.1.3 % 11.71/2.52 % (3917315)Termination reason: Instruction limit % 11.71/2.52 % (3917315)Termination phase: Saturation % 11.71/2.52 % (3917315)Time elapsed: 0.190 s % 11.71/2.52 % (3917315)Peak memory usage: 91 MB % 11.71/2.52 % (3917315)Instructions burned: 307 (million) % 11.71/2.52 % (3917327)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3373812199:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 11.71/2.52 % (3917328)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3376210651:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.92/2.80 % (3917329)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1629860134:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 13.92/2.80 % (3917331)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1907157903:i=121:nm=16:rtra=on_2988 on theBenchmark for (2988ds/121Mi) % 13.92/2.80 % (3917329)Refutation not found, incomplete strategy % 13.92/2.80 % (3917329)------------------------------ % 13.92/2.80 % (3917329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.92/2.80 % (3917329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.80 % (3917329)CaDiCaL version: 2.1.3 % 13.92/2.80 % (3917329)Termination reason: Refutation not found, incomplete strategy % 13.92/2.80 % (3917329)Time elapsed: 0.028 s % 13.92/2.80 % (3917329)Peak memory usage: 115 MB % 13.92/2.80 % (3917329)Instructions burned: 7 (million) % 13.92/2.80 % (3917332)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=1029527240:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 13.92/2.80 % (3917328)Instruction limit reached! % 13.92/2.80 % (3917328)------------------------------ % 13.92/2.80 % (3917328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.92/2.80 % (3917328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.80 % (3917328)CaDiCaL version: 2.1.3 % 13.92/2.80 % (3917328)Termination reason: Instruction limit % 13.92/2.80 % (3917328)Termination phase: Saturation % 13.92/2.80 % (3917328)Time elapsed: 0.083 s % 13.92/2.80 % (3917328)Peak memory usage: 90 MB % 13.92/2.80 % (3917328)Instructions burned: 142 (million) % 13.92/2.80 % (3917331)Instruction limit reached! % 13.92/2.80 % (3917331)------------------------------ % 13.92/2.80 % (3917331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.92/2.80 % (3917331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.80 % (3917331)CaDiCaL version: 2.1.3 % 13.92/2.80 % (3917331)Termination reason: Instruction limit % 13.92/2.80 % (3917331)Termination phase: Saturation % 13.92/2.80 % (3917331)Time elapsed: 0.065 s % 13.92/2.80 % (3917331)Peak memory usage: 89 MB % 13.92/2.80 % (3917331)Instructions burned: 123 (million) % 13.92/2.80 % (3917327)Instruction limit reached! % 13.92/2.80 % (3917327)------------------------------ % 13.92/2.80 % (3917327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.92/2.80 % (3917327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.80 % (3917327)CaDiCaL version: 2.1.3 % 13.92/2.80 % (3917327)Termination reason: Instruction limit % 13.92/2.80 % (3917327)Termination phase: Saturation % 13.92/2.80 % (3917327)Time elapsed: 0.228 s % 13.92/2.80 % (3917327)Peak memory usage: 91 MB % 13.92/2.80 % (3917327)Instructions burned: 383 (million) % 13.92/2.80 % (3917338)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=3530306554:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi) % 13.92/2.80 % (3917332)Instruction limit reached! % 13.92/2.80 % (3917332)------------------------------ % 13.92/2.80 % (3917332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.92/2.80 % (3917332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.80 % (3917332)CaDiCaL version: 2.1.3 % 13.92/2.80 % (3917332)Termination reason: Instruction limit % 13.92/2.80 % (3917332)Termination phase: Saturation % 13.92/2.80 % (3917332)Time elapsed: 0.111 s % 13.92/2.80 % (3917332)Peak memory usage: 117 MB % 13.92/2.80 % (3917332)Instructions burned: 129 (million) % 13.92/2.80 % (3917338)Instruction limit reached! % 13.92/2.80 % (3917338)------------------------------ % 13.92/2.80 % (3917338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.92/2.80 % (3917338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.92/2.80 % (3917338)CaDiCaL version: 2.1.3 % 13.92/2.80 % (3917338)Termination reason: Instruction limit % 13.92/2.80 % (3917338)Termination phase: Saturation % 13.92/2.80 % (3917338)Time elapsed: 0.028 s % 13.92/2.80 % (3917338)Peak memory usage: 116 MB % 13.92/2.80 % (3917338)Instructions burned: 41 (million) % 13.92/2.80 % (3917339)dis+1010_1_to=kbo:si=on:random_seed=559261078:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 13.92/2.80 % (3917316)Instruction limit reached! % 13.92/2.80 % (3917316)------------------------------ % 13.92/2.80 % (3917316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.18/3.10 % (3917316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.18/3.10 % (3917316)CaDiCaL version: 2.1.3 % 17.18/3.10 % (3917316)Termination reason: Instruction limit % 17.18/3.10 % (3917316)Termination phase: Saturation % 17.18/3.10 % (3917316)Time elapsed: 0.461 s % 17.18/3.10 % (3917316)Peak memory usage: 138 MB % 17.18/3.10 % (3917316)Instructions burned: 599 (million) % 17.18/3.10 % (3917329)------------------------------ % 17.18/3.10 % (3917329)------------------------------ % 17.18/3.10 % (3917340)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3556554339:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi) % 17.18/3.10 % (3917343)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1534165634:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 17.18/3.10 % (3917342)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3471572721:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 17.18/3.10 % (3917339)Instruction limit reached! % 17.18/3.10 % (3917339)------------------------------ % 17.18/3.10 % (3917339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.18/3.10 % (3917339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.18/3.10 % (3917339)CaDiCaL version: 2.1.3 % 17.18/3.10 % (3917339)Termination reason: Instruction limit % 17.18/3.10 % (3917339)Termination phase: Saturation % 17.18/3.10 % (3917339)Time elapsed: 0.125 s % 17.18/3.10 % (3917339)Peak memory usage: 91 MB % 17.18/3.10 % (3917339)Instructions burned: 175 (million) % 17.18/3.10 % (3917345)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=130870151:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi) % 17.18/3.10 % (3917343)Instruction limit reached! % 17.18/3.10 % (3917343)------------------------------ % 17.18/3.10 % (3917343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.18/3.10 % (3917343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.18/3.10 % (3917343)CaDiCaL version: 2.1.3 % 17.18/3.10 % (3917343)Termination reason: Instruction limit % 17.18/3.10 % (3917343)Termination phase: Saturation % 17.18/3.10 % (3917343)Time elapsed: 0.096 s % 17.18/3.10 % (3917343)Peak memory usage: 135 MB % 17.18/3.10 % (3917343)Instructions burned: 217 (million) % 17.18/3.10 % (3917346)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=347673124:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi) % 17.18/3.10 % (3917325)Instruction limit reached! % 17.18/3.10 % (3917325)------------------------------ % 17.18/3.10 % (3917325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.18/3.10 % (3917325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.18/3.10 % (3917325)CaDiCaL version: 2.1.3 % 17.18/3.10 % (3917325)Termination reason: Instruction limit % 17.18/3.10 % (3917325)Termination phase: Saturation % 17.18/3.10 % (3917325)Time elapsed: 0.561 s % 17.18/3.10 % (3917325)Peak memory usage: 95 MB % 17.18/3.10 % (3917325)Instructions burned: 1001 (million) % 17.18/3.10 % (3917350)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3765865581:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi) % 17.18/3.10 % (3917352)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3151357388:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi) % 17.18/3.10 % (3917340)Instruction limit reached! % 17.18/3.10 % (3917340)------------------------------ % 17.18/3.10 % (3917340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.18/3.10 % (3917340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.18/3.10 % (3917340)CaDiCaL version: 2.1.3 % 17.18/3.10 % (3917340)Termination reason: Instruction limit % 17.18/3.10 % (3917340)Termination phase: Saturation % 17.18/3.10 % (3917340)Time elapsed: 0.266 s % 17.18/3.10 % (3917340)Peak memory usage: 118 MB % 17.18/3.10 % (3917340)Instructions burned: 330 (million) % 17.18/3.10 % (3917346)Instruction limit reached! % 17.18/3.10 % (3917346)------------------------------ % 17.18/3.10 % (3917346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.18/3.10 % (3917346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.33 % (3917346)CaDiCaL version: 2.1.3 % 18.12/3.33 % (3917346)Termination reason: Instruction limit % 18.12/3.33 % (3917346)Termination phase: Saturation % 18.12/3.33 % (3917346)Time elapsed: 0.160 s % 18.12/3.33 % (3917346)Peak memory usage: 90 MB % 18.12/3.33 % (3917346)Instructions burned: 296 (million) % 18.12/3.33 % (3917354)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3388554867:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 18.12/3.33 % (3917345)Instruction limit reached! % 18.12/3.33 % (3917345)------------------------------ % 18.12/3.33 % (3917345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.33 % (3917345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.33 % (3917345)CaDiCaL version: 2.1.3 % 18.12/3.33 % (3917345)Termination reason: Instruction limit % 18.12/3.33 % (3917345)Termination phase: Saturation % 18.12/3.33 % (3917345)Time elapsed: 0.226 s % 18.12/3.33 % (3917345)Peak memory usage: 116 MB % 18.12/3.33 % (3917345)Instructions burned: 350 (million) % 18.12/3.33 % (3917352)Instruction limit reached! % 18.12/3.33 % (3917352)------------------------------ % 18.12/3.33 % (3917352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.33 % (3917352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.33 % (3917352)CaDiCaL version: 2.1.3 % 18.12/3.33 % (3917352)Termination reason: Instruction limit % 18.12/3.33 % (3917352)Termination phase: Saturation % 18.12/3.33 % (3917352)Time elapsed: 0.113 s % 18.12/3.33 % (3917352)Peak memory usage: 118 MB % 18.12/3.33 % (3917352)Instructions burned: 281 (million) % 18.12/3.33 % (3917357)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2148464521:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi) % 18.12/3.33 % (3917342)Instruction limit reached! % 18.12/3.33 % (3917342)------------------------------ % 18.12/3.33 % (3917342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.33 % (3917342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.33 % (3917342)CaDiCaL version: 2.1.3 % 18.12/3.33 % (3917342)Termination reason: Instruction limit % 18.12/3.33 % (3917342)Termination phase: Saturation % 18.12/3.33 % (3917342)Time elapsed: 0.390 s % 18.12/3.33 % (3917342)Peak memory usage: 135 MB % 18.12/3.33 % (3917342)Instructions burned: 483 (million) % 18.12/3.33 % (3917358)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2962653913:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi) % 18.12/3.33 % (3917350)Instruction limit reached! % 18.12/3.33 % (3917350)------------------------------ % 18.12/3.33 % (3917350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.33 % (3917350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.33 % (3917350)CaDiCaL version: 2.1.3 % 18.12/3.33 % (3917350)Termination reason: Instruction limit % 18.12/3.33 % (3917350)Termination phase: Saturation % 18.12/3.33 % (3917350)Time elapsed: 0.230 s % 18.12/3.33 % (3917350)Peak memory usage: 119 MB % 18.12/3.33 % (3917350)Instructions burned: 329 (million) % 18.12/3.33 % (3917361)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=3680326041:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi) % 18.12/3.33 % (3917360)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3431640698:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi) % 18.12/3.33 % (3917364)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2963794048:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi) % 18.12/3.33 % (3917361)Instruction limit reached! % 18.12/3.33 % (3917361)------------------------------ % 18.12/3.33 % (3917361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.12/3.33 % (3917361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.12/3.33 % (3917361)CaDiCaL version: 2.1.3 % 18.12/3.33 % (3917361)Termination reason: Instruction limit % 18.12/3.33 % (3917361)Termination phase: Saturation % 18.12/3.33 % (3917361)Time elapsed: 0.136 s % 18.12/3.33 % (3917361)Peak memory usage: 134 MB % 18.12/3.33 % (3917361)Instructions burned: 279 (million) % 18.12/3.33 % (3917366)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=847175712:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi) % 19.44/3.75 % (3917357)Instruction limit reached! % 19.44/3.75 % (3917357)------------------------------ % 19.44/3.75 % (3917357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.44/3.75 % (3917357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.44/3.75 % (3917357)CaDiCaL version: 2.1.3 % 19.44/3.75 % (3917357)Termination reason: Instruction limit % 19.44/3.75 % (3917357)Termination phase: Saturation % 19.44/3.75 % (3917357)Time elapsed: 0.198 s % 19.44/3.75 % (3917357)Peak memory usage: 114 MB % 19.44/3.75 % (3917357)Instructions burned: 323 (million) % 19.44/3.75 % (3917354)Instruction limit reached! % 19.44/3.75 % (3917354)------------------------------ % 19.44/3.75 % (3917354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.44/3.75 % (3917354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.44/3.75 % (3917354)CaDiCaL version: 2.1.3 % 19.44/3.75 % (3917354)Termination reason: Instruction limit % 19.44/3.75 % (3917354)Termination phase: Saturation % 19.44/3.75 % (3917354)Time elapsed: 0.297 s % 19.44/3.75 % (3917354)Peak memory usage: 93 MB % 19.44/3.75 % (3917354)Instructions burned: 485 (million) % 19.44/3.75 % (3917358)Instruction limit reached! % 19.44/3.75 % (3917358)------------------------------ % 19.44/3.75 % (3917358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.44/3.75 % (3917358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.44/3.75 % (3917358)CaDiCaL version: 2.1.3 % 19.44/3.75 % (3917370)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=952975040:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2978 on theBenchmark for (2978ds/513Mi) % 19.44/3.75 % (3917358)Termination reason: Instruction limit % 19.44/3.75 % (3917358)Termination phase: Saturation % 19.44/3.75 % (3917358)Time elapsed: 0.242 s % 19.44/3.75 % (3917358)Peak memory usage: 117 MB % 19.44/3.75 % (3917358)Instructions burned: 417 (million) % 19.44/3.75 % (3917372)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3243305831:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 19.44/3.75 % (3917371)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1434486926:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi) % 19.44/3.75 % (3917360)Instruction limit reached! % 19.44/3.75 % (3917360)------------------------------ % 19.44/3.75 % (3917360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.44/3.75 % (3917360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.44/3.75 % (3917360)CaDiCaL version: 2.1.3 % 19.44/3.75 % (3917360)Termination reason: Instruction limit % 19.44/3.75 % (3917360)Termination phase: Saturation % 19.44/3.75 % (3917360)Time elapsed: 0.332 s % 19.44/3.75 % (3917360)Peak memory usage: 120 MB % 19.44/3.75 % (3917360)Instructions burned: 472 (million) % 19.44/3.75 % (3917374)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3325289765:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2977 on theBenchmark for (2977ds/341Mi) % 19.44/3.75 % (3917364)Instruction limit reached! % 19.44/3.75 % (3917364)------------------------------ % 19.44/3.75 % (3917364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.44/3.75 % (3917364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.44/3.75 % (3917364)CaDiCaL version: 2.1.3 % 19.44/3.75 % (3917364)Termination reason: Instruction limit % 19.44/3.75 % (3917364)Termination phase: Saturation % 19.44/3.75 % (3917364)Time elapsed: 0.276 s % 19.44/3.75 % (3917364)Peak memory usage: 119 MB % 19.44/3.75 % (3917364)Instructions burned: 376 (million) % 19.44/3.75 % (3917370)Instruction limit reached! % 19.44/3.75 % (3917370)------------------------------ % 19.44/3.75 % (3917370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.44/3.75 % (3917370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.44/3.75 % (3917370)CaDiCaL version: 2.1.3 % 19.44/3.75 % (3917370)Termination reason: Instruction limit % 19.44/3.75 % (3917370)Termination phase: Saturation % 19.44/3.75 % (3917370)Time elapsed: 0.160 s % 19.44/3.75 % (3917370)Peak memory usage: 92 MB % 19.44/3.75 % (3917370)Instructions burned: 516 (million) % 19.44/3.75 % (3917366)Instruction limit reached! % 19.44/3.75 % (3917366)------------------------------ % 19.44/3.75 % (3917366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.39/4.20 % (3917366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.39/4.20 % (3917366)CaDiCaL version: 2.1.3 % 25.39/4.20 % (3917366)Termination reason: Instruction limit % 25.39/4.20 % (3917366)Termination phase: Saturation % 25.39/4.20 % (3917366)Time elapsed: 0.299 s % 25.39/4.20 % (3917366)Peak memory usage: 119 MB % 25.39/4.20 % (3917366)Instructions burned: 388 (million) % 25.39/4.20 % (3917372)Instruction limit reached! % 25.39/4.20 % (3917372)------------------------------ % 25.39/4.20 % (3917372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.39/4.20 % (3917372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.39/4.20 % (3917372)CaDiCaL version: 2.1.3 % 25.39/4.20 % (3917372)Termination reason: Instruction limit % 25.39/4.20 % (3917372)Termination phase: Saturation % 25.39/4.20 % (3917372)Time elapsed: 0.138 s % 25.39/4.20 % (3917372)Peak memory usage: 89 MB % 25.39/4.20 % (3917372)Instructions burned: 361 (million) % 25.39/4.20 % (3917379)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3040741598:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi) % 25.39/4.20 % (3917382)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3248334460:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi) % 25.39/4.20 % (3917379)Refutation not found, incomplete strategy % 25.39/4.20 % (3917379)------------------------------ % 25.39/4.20 % (3917379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.39/4.20 % (3917379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.39/4.20 % (3917379)CaDiCaL version: 2.1.3 % 25.39/4.20 % (3917379)Termination reason: Refutation not found, incomplete strategy % 25.39/4.20 % (3917379)Time elapsed: 0.028 s % 25.39/4.20 % (3917379)Peak memory usage: 115 MB % 25.39/4.20 % (3917379)Instructions burned: 6 (million) % 25.39/4.20 % (3917381)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=4145801734:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi) % 25.39/4.20 % (3917384)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1571580182:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi) % 25.39/4.20 % (3917383)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=400893485:i=146:doe=on:rtra=on_2975 on theBenchmark for (2975ds/146Mi) % 25.39/4.20 % (3917371)Instruction limit reached! % 25.39/4.20 % (3917371)------------------------------ % 25.39/4.20 % (3917371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.39/4.20 % (3917371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.39/4.20 % (3917371)CaDiCaL version: 2.1.3 % 25.39/4.20 % (3917371)Termination reason: Instruction limit % 25.39/4.20 % (3917371)Termination phase: Saturation % 25.39/4.20 % (3917371)Time elapsed: 0.273 s % 25.39/4.20 % (3917371)Peak memory usage: 134 MB % 25.39/4.20 % (3917371)Instructions burned: 335 (million) % 25.39/4.20 % (3917382)Instruction limit reached! % 25.39/4.20 % (3917382)------------------------------ % 25.39/4.20 % (3917382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.39/4.20 % (3917382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.39/4.20 % (3917382)CaDiCaL version: 2.1.3 % 25.39/4.20 % (3917382)Termination reason: Instruction limit % 25.39/4.20 % (3917382)Termination phase: Saturation % 25.39/4.20 % (3917382)Time elapsed: 0.103 s % 25.39/4.20 % (3917382)Peak memory usage: 92 MB % 25.39/4.20 % (3917382)Instructions burned: 275 (million) % 25.39/4.20 % (3917374)Instruction limit reached! % 25.39/4.20 % (3917374)------------------------------ % 25.39/4.20 % (3917374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.39/4.20 % (3917374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.39/4.20 % (3917374)CaDiCaL version: 2.1.3 % 25.39/4.20 % (3917374)Termination reason: Instruction limit % 25.39/4.20 % (3917374)Termination phase: Saturation % 25.39/4.20 % (3917374)Time elapsed: 0.246 s % 25.39/4.20 % (3917374)Peak memory usage: 118 MB % 25.39/4.20 % (3917374)Instructions burned: 342 (million) % 25.39/4.20 % (3917383)Instruction limit reached! % 25.39/4.20 % (3917383)------------------------------ % 25.39/4.20 % (3917383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.71/4.60 % (3917383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.71/4.60 % (3917383)CaDiCaL version: 2.1.3 % 26.71/4.60 % (3917383)Termination reason: Instruction limit % 26.71/4.60 % (3917383)Termination phase: Saturation % 26.71/4.60 % (3917383)Time elapsed: 0.097 s % 26.71/4.60 % (3917383)Peak memory usage: 90 MB % 26.71/4.60 % (3917383)Instructions burned: 147 (million) % 26.71/4.60 % (3917391)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2289993040:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 26.71/4.60 % (3917381)Instruction limit reached! % 26.71/4.60 % (3917381)------------------------------ % 26.71/4.60 % (3917381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.71/4.60 % (3917381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.71/4.60 % (3917381)CaDiCaL version: 2.1.3 % 26.71/4.60 % (3917381)Termination reason: Instruction limit % 26.71/4.60 % (3917381)Termination phase: Saturation % 26.71/4.60 % (3917381)Time elapsed: 0.175 s % 26.71/4.60 % (3917381)Peak memory usage: 116 MB % 26.71/4.60 % (3917381)Instructions burned: 236 (million) % 26.71/4.60 % (3917390)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=2131848381:avsq=on:i=276:avsqr=1,2:rtra=on_2974 on theBenchmark for (2974ds/276Mi) % 26.71/4.60 % (3917392)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1625795281:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2973 on theBenchmark for (2973ds/655Mi) % 26.71/4.60 % (3917379)------------------------------ % 26.71/4.60 % (3917379)------------------------------ % 26.71/4.60 % (3917393)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1450687196:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2973 on theBenchmark for (2973ds/1054Mi) % 26.71/4.60 % (3917395)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1733530016:i=107:rtra=on_2972 on theBenchmark for (2972ds/107Mi) % 26.71/4.60 % (3917395)Refutation not found, incomplete strategy % 26.71/4.60 % (3917395)------------------------------ % 26.71/4.60 % (3917395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.71/4.60 % (3917395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.71/4.60 % (3917395)CaDiCaL version: 2.1.3 % 26.71/4.60 % (3917395)Termination reason: Refutation not found, incomplete strategy % 26.71/4.60 % (3917395)Time elapsed: 0.029 s % 26.71/4.60 % (3917395)Peak memory usage: 115 MB % 26.71/4.60 % (3917395)Instructions burned: 8 (million) % 26.71/4.60 % (3917398)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3408642508:s2a=on:i=450:doe=on:nm=32:rtra=on_2972 on theBenchmark for (2972ds/450Mi) % 26.71/4.60 % (3917390)Instruction limit reached! % 26.71/4.60 % (3917390)------------------------------ % 26.71/4.60 % (3917390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.71/4.60 % (3917390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.71/4.60 % (3917390)CaDiCaL version: 2.1.3 % 26.71/4.60 % (3917390)Termination reason: Instruction limit % 26.71/4.60 % (3917390)Termination phase: Saturation % 26.71/4.60 % (3917390)Time elapsed: 0.245 s % 26.71/4.60 % (3917390)Peak memory usage: 134 MB % 26.71/4.60 % (3917390)Instructions burned: 276 (million) % 26.71/4.60 % (3917391)Instruction limit reached! % 26.71/4.60 % (3917391)------------------------------ % 26.71/4.60 % (3917391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.71/4.60 % (3917391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.71/4.60 % (3917391)CaDiCaL version: 2.1.3 % 26.71/4.60 % (3917391)Termination reason: Instruction limit % 26.71/4.60 % (3917391)Termination phase: Saturation % 26.71/4.60 % (3917391)Time elapsed: 0.356 s % 26.71/4.60 % (3917391)Peak memory usage: 92 MB % 26.71/4.60 % (3917391)Instructions burned: 1053 (million) % 26.71/4.60 % (3917395)------------------------------ % 26.71/4.60 % (3917395)------------------------------ % 26.71/4.60 % (3917402)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 26.71/4.60 % (3917402)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1770782166:i=1090:aac=none:nm=0:rtra=on:rawr=on_2970 on theBenchmark for (2970ds/1090Mi) % 28.58/5.03 % (3917403)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=616107377:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi) % 28.58/5.03 % (3917392)Instruction limit reached! % 28.58/5.03 % (3917392)------------------------------ % 28.58/5.03 % (3917392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.58/5.03 % (3917392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.58/5.03 % (3917392)CaDiCaL version: 2.1.3 % 28.58/5.03 % (3917392)Termination reason: Instruction limit % 28.58/5.03 % (3917392)Termination phase: Saturation % 28.58/5.03 % (3917392)Time elapsed: 0.393 s % 28.58/5.03 % (3917392)Peak memory usage: 91 MB % 28.58/5.03 % (3917392)Instructions burned: 656 (million) % 28.58/5.03 % (3917403)Instruction limit reached! % 28.58/5.03 % (3917403)------------------------------ % 28.58/5.03 % (3917403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.58/5.03 % (3917403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.58/5.03 % (3917403)CaDiCaL version: 2.1.3 % 28.58/5.03 % (3917403)Termination reason: Instruction limit % 28.58/5.03 % (3917403)Termination phase: Saturation % 28.58/5.03 % (3917403)Time elapsed: 0.062 s % 28.58/5.03 % (3917403)Peak memory usage: 116 MB % 28.58/5.03 % (3917403)Instructions burned: 132 (million) % 28.58/5.03 % (3917393)Instruction limit reached! % 28.58/5.03 % (3917393)------------------------------ % 28.58/5.03 % (3917393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.58/5.03 % (3917393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.58/5.03 % (3917393)CaDiCaL version: 2.1.3 % 28.58/5.03 % (3917393)Termination reason: Instruction limit % 28.58/5.03 % (3917393)Termination phase: Saturation % 28.58/5.03 % (3917393)Time elapsed: 0.407 s % 28.58/5.03 % (3917393)Peak memory usage: 90 MB % 28.58/5.03 % (3917393)Instructions burned: 1056 (million) % 28.58/5.03 % (3917398)Instruction limit reached! % 28.58/5.03 % (3917398)------------------------------ % 28.58/5.03 % (3917398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.58/5.03 % (3917398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.58/5.03 % (3917398)CaDiCaL version: 2.1.3 % 28.58/5.03 % (3917398)Termination reason: Instruction limit % 28.58/5.03 % (3917398)Termination phase: Saturation % 28.58/5.03 % (3917398)Time elapsed: 0.351 s % 28.58/5.03 % (3917398)Peak memory usage: 135 MB % 28.58/5.03 % (3917398)Instructions burned: 450 (million) % 28.58/5.03 % (3917405)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=334255753:i=312:kws=inv_frequency:nm=20:rtra=on_2969 on theBenchmark for (2969ds/312Mi) % 28.58/5.03 % (3917407)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=220107171:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi) % 28.58/5.03 % (3917408)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1462241467:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 28.58/5.03 % (3917409)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2134704177:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 28.58/5.03 % (3917411)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2178872912:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 28.58/5.03 % (3917405)Instruction limit reached! % 28.58/5.03 % (3917405)------------------------------ % 28.58/5.03 % (3917405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.58/5.03 % (3917405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.58/5.03 % (3917405)CaDiCaL version: 2.1.3 % 28.58/5.03 % (3917405)Termination reason: Instruction limit % 28.58/5.03 % (3917405)Termination phase: Saturation % 28.58/5.03 % (3917405)Time elapsed: 0.216 s % 28.58/5.03 % (3917405)Peak memory usage: 118 MB % 28.58/5.03 % (3917405)Instructions burned: 312 (million) % 28.58/5.03 % (3917408)Instruction limit reached! % 28.58/5.03 % (3917408)------------------------------ % 28.58/5.03 % (3917408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.58/5.03 % (3917408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.58/5.03 % (3917408)CaDiCaL version: 2.1.3 % 28.58/5.03 % (3917408)Termination reason: Instruction limit % 34.81/5.72 % (3917408)Termination phase: Saturation % 34.81/5.72 % (3917408)Time elapsed: 0.257 s % 34.81/5.72 % (3917408)Peak memory usage: 94 MB % 34.81/5.72 % (3917408)Instructions burned: 836 (million) % 34.81/5.72 % (3917409)Instruction limit reached! % 34.81/5.72 % (3917409)------------------------------ % 34.81/5.72 % (3917409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.81/5.72 % (3917409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.81/5.72 % (3917409)CaDiCaL version: 2.1.3 % 34.81/5.72 % (3917409)Termination reason: Instruction limit % 34.81/5.72 % (3917409)Termination phase: Saturation % 34.81/5.72 % (3917409)Time elapsed: 0.222 s % 34.81/5.72 % (3917409)Peak memory usage: 92 MB % 34.81/5.72 % (3917409)Instructions burned: 307 (million) % 34.81/5.72 % (3917407)Instruction limit reached! % 34.81/5.72 % (3917407)------------------------------ % 34.81/5.72 % (3917407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.81/5.72 % (3917407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.81/5.72 % (3917407)CaDiCaL version: 2.1.3 % 34.81/5.72 % (3917407)Termination reason: Instruction limit % 34.81/5.72 % (3917407)Termination phase: Saturation % 34.81/5.72 % (3917407)Time elapsed: 0.280 s % 34.81/5.72 % (3917407)Peak memory usage: 90 MB % 34.81/5.72 % (3917407)Instructions burned: 491 (million) % 34.81/5.72 % (3917416)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1256012470:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2965 on theBenchmark for (2965ds/646Mi) % 34.81/5.72 % (3917417)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=4285392716:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2964 on theBenchmark for (2964ds/784Mi) % 34.81/5.72 % (3917419)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=789010444:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/246Mi) % 34.81/5.72 % (3917418)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=2548103076:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2964 on theBenchmark for (2964ds/1131Mi) % 34.81/5.72 % (3917411)Instruction limit reached! % 34.81/5.72 % (3917411)------------------------------ % 34.81/5.72 % (3917411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.81/5.72 % (3917411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.81/5.72 % (3917411)CaDiCaL version: 2.1.3 % 34.81/5.72 % (3917411)Termination reason: Instruction limit % 34.81/5.72 % (3917411)Termination phase: Saturation % 34.81/5.72 % (3917411)Time elapsed: 0.400 s % 34.81/5.72 % (3917411)Peak memory usage: 117 MB % 34.81/5.72 % (3917411)Instructions burned: 776 (million) % 34.81/5.72 % (3917402)Instruction limit reached! % 34.81/5.72 % (3917402)------------------------------ % 34.81/5.72 % (3917402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.81/5.72 % (3917402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.81/5.72 % (3917402)CaDiCaL version: 2.1.3 % 34.81/5.72 % (3917402)Termination reason: Instruction limit % 34.81/5.72 % (3917402)Termination phase: Saturation % 34.81/5.72 % (3917402)Time elapsed: 0.720 s % 34.81/5.72 % (3917402)Peak memory usage: 122 MB % 34.81/5.72 % (3917402)Instructions burned: 1090 (million) % 34.81/5.72 % (3917419)Instruction limit reached! % 34.81/5.72 % (3917419)------------------------------ % 34.81/5.72 % (3917419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.81/5.72 % (3917419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.81/5.72 % (3917419)CaDiCaL version: 2.1.3 % 34.81/5.72 % (3917419)Termination reason: Instruction limit % 34.81/5.72 % (3917419)Termination phase: Saturation % 34.81/5.72 % (3917419)Time elapsed: 0.170 s % 34.81/5.72 % (3917419)Peak memory usage: 116 MB % 34.81/5.72 % (3917419)Instructions burned: 246 (million) % 34.81/5.72 % (3917424)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=357533119:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 34.81/5.72 % (3917417)Instruction limit reached! % 34.81/5.72 % (3917417)------------------------------ % 34.81/5.72 % (3917417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.81/5.72 % (3917417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.17/7.94 % (3917417)CaDiCaL version: 2.1.3 % 51.17/7.94 % (3917417)Termination reason: Instruction limit % 51.17/7.94 % (3917417)Termination phase: Saturation % 51.17/7.94 % (3917417)Time elapsed: 0.313 s % 51.17/7.94 % (3917417)Peak memory usage: 122 MB % 51.17/7.94 % (3917417)Instructions burned: 785 (million) % 51.17/7.94 % (3917425)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=673356656:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 51.17/7.94 % (3917426)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2843477693:i=102:nm=16:rtra=on_2961 on theBenchmark for (2961ds/102Mi) % 51.17/7.94 % (3917428)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=561662614:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2960 on theBenchmark for (2960ds/1094Mi) % 51.17/7.94 % (3917426)Instruction limit reached! % 51.17/7.94 % (3917426)------------------------------ % 51.17/7.94 % (3917426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.17/7.94 % (3917426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.17/7.94 % (3917426)CaDiCaL version: 2.1.3 % 51.17/7.94 % (3917426)Termination reason: Instruction limit % 51.17/7.94 % (3917426)Termination phase: Saturation % 51.17/7.94 % (3917426)Time elapsed: 0.056 s % 51.17/7.94 % (3917426)Peak memory usage: 89 MB % 51.17/7.94 % (3917426)Instructions burned: 102 (million) % 51.17/7.94 % (3917416)Instruction limit reached! % 51.17/7.94 % (3917416)------------------------------ % 51.17/7.94 % (3917416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.17/7.94 % (3917416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.17/7.94 % (3917416)CaDiCaL version: 2.1.3 % 51.17/7.94 % (3917416)Termination reason: Instruction limit % 51.17/7.94 % (3917416)Termination phase: Saturation % 51.17/7.94 % (3917416)Time elapsed: 0.477 s % 51.17/7.94 % (3917416)Peak memory usage: 138 MB % 51.17/7.94 % (3917416)Instructions burned: 648 (million) % 51.17/7.94 % (3917425)Instruction limit reached! % 51.17/7.94 % (3917425)------------------------------ % 51.17/7.94 % (3917425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.17/7.94 % (3917425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.17/7.94 % (3917425)CaDiCaL version: 2.1.3 % 51.17/7.94 % (3917425)Termination reason: Instruction limit % 51.17/7.94 % (3917425)Termination phase: Saturation % 51.17/7.94 % (3917425)Time elapsed: 0.191 s % 51.17/7.94 % (3917425)Peak memory usage: 92 MB % 51.17/7.94 % (3917425)Instructions burned: 273 (million) % 51.17/7.94 % (3917432)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4088716875:i=6400:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/6400Mi) % 51.17/7.94 % (3917433)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=2625970102:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2959 on theBenchmark for (2959ds/868Mi) % 51.17/7.94 % (3917434)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=1604271809:i=1846:canc=cautious:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/1846Mi) % 51.17/7.94 % (3917428)Instruction limit reached! % 51.17/7.94 % (3917428)------------------------------ % 51.17/7.94 % (3917428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.17/7.94 % (3917428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.17/7.94 % (3917428)CaDiCaL version: 2.1.3 % 51.17/7.94 % (3917428)Termination reason: Instruction limit % 51.17/7.94 % (3917428)Termination phase: Saturation % 51.17/7.94 % (3917428)Time elapsed: 0.247 s % 51.17/7.94 % (3917428)Peak memory usage: 90 MB % 51.17/7.94 % (3917428)Instructions burned: 1098 (million) % 51.17/7.94 % (3917424)Instruction limit reached! % 51.17/7.94 % (3917424)------------------------------ % 51.17/7.94 % (3917424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.17/7.94 % (3917424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.17/7.94 % (3917424)CaDiCaL version: 2.1.3 % 51.17/7.94 % (3917424)Termination reason: Instruction limit % 51.17/7.94 % (3917424)Termination phase: Saturation % 51.17/7.94 % (3917424)Time elapsed: 0.457 s % 51.17/7.94 % (3917424)Peak memory usage: 93 MB % 51.17/7.94 % (3917424)Instructions burned: 775 (million) % 51.17/7.94 % (3917438)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2549633369:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2957 on theBenchmark for (2957ds/36816Mi) % 61.15/9.37 % (3917418)Instruction limit reached! % 61.15/9.37 % (3917418)------------------------------ % 61.15/9.37 % (3917418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.37 % (3917418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.37 % (3917418)CaDiCaL version: 2.1.3 % 61.15/9.37 % (3917418)Termination reason: Instruction limit % 61.15/9.37 % (3917418)Termination phase: Saturation % 61.15/9.37 % (3917418)Time elapsed: 0.730 s % 61.15/9.37 % (3917418)Peak memory usage: 123 MB % 61.15/9.37 % (3917418)Instructions burned: 1132 (million) % 61.15/9.37 % (3917439)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1940817359:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2956 on theBenchmark for (2956ds/273Mi) % 61.15/9.37 % (3917441)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=2272337425:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 61.15/9.37 % (3917439)Instruction limit reached! % 61.15/9.37 % (3917439)------------------------------ % 61.15/9.37 % (3917439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.37 % (3917439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.37 % (3917439)CaDiCaL version: 2.1.3 % 61.15/9.37 % (3917439)Termination reason: Instruction limit % 61.15/9.37 % (3917439)Termination phase: Saturation % 61.15/9.37 % (3917439)Time elapsed: 0.192 s % 61.15/9.37 % (3917439)Peak memory usage: 92 MB % 61.15/9.37 % (3917439)Instructions burned: 275 (million) % 61.15/9.37 % (3917433)Instruction limit reached! % 61.15/9.37 % (3917433)------------------------------ % 61.15/9.37 % (3917433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.37 % (3917433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.37 % (3917433)CaDiCaL version: 2.1.3 % 61.15/9.37 % (3917433)Termination reason: Instruction limit % 61.15/9.37 % (3917433)Termination phase: Saturation % 61.15/9.37 % (3917433)Time elapsed: 0.544 s % 61.15/9.37 % (3917433)Peak memory usage: 119 MB % 61.15/9.37 % (3917433)Instructions burned: 868 (million) % 61.15/9.37 % (3917444)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4007206335:i=5811:kws=precedence:nm=0:rtra=on_2953 on theBenchmark for (2953ds/5811Mi) % 61.15/9.37 % (3917445)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=1917094484:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2952 on theBenchmark for (2952ds/2216Mi) % 61.15/9.37 % (3917384)Instruction limit reached! % 61.15/9.37 % (3917384)------------------------------ % 61.15/9.37 % (3917384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.37 % (3917384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.37 % (3917384)CaDiCaL version: 2.1.3 % 61.15/9.37 % (3917384)Termination reason: Instruction limit % 61.15/9.37 % (3917384)Termination phase: Saturation % 61.15/9.37 % (3917384)Time elapsed: 2.444 s % 61.15/9.37 % (3917384)Peak memory usage: 112 MB % 61.15/9.37 % (3917384)Instructions burned: 4428 (million) % 61.15/9.37 % (3917441)Instruction limit reached! % 61.15/9.37 % (3917441)------------------------------ % 61.15/9.37 % (3917441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.37 % (3917441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.37 % (3917441)CaDiCaL version: 2.1.3 % 61.15/9.37 % (3917441)Termination reason: Instruction limit % 61.15/9.37 % (3917441)Termination phase: Saturation % 61.15/9.37 % (3917441)Time elapsed: 0.528 s % 61.15/9.37 % (3917441)Peak memory usage: 120 MB % 61.15/9.37 % (3917441)Instructions burned: 864 (million) % 61.15/9.37 % (3917434)Instruction limit reached! % 61.15/9.37 % (3917434)------------------------------ % 61.15/9.37 % (3917434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.37 % (3917434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.37 % (3917434)CaDiCaL version: 2.1.3 % 61.15/9.37 % (3917434)Termination reason: Instruction limit % 61.15/9.37 % (3917434)Termination phase: Saturation % 61.15/9.37 % (3917434)Time elapsed: 0.787 s % 61.15/9.37 % (3917434)Peak memory usage: 100 MB % 101.29/14.93 % (3917434)Instructions burned: 1848 (million) % 101.29/14.93 % (3917448)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3269389805:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2949 on theBenchmark for (2949ds/801Mi) % 101.29/14.93 % (3917449)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1050540484:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2949 on theBenchmark for (2949ds/1026Mi) % 101.29/14.93 % (3917450)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1088531315:i=3509:rtra=on_2949 on theBenchmark for (2949ds/3509Mi) % 101.29/14.93 % (3917448)Instruction limit reached! % 101.29/14.93 % (3917448)------------------------------ % 101.29/14.93 % (3917448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.29/14.93 % (3917448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.29/14.93 % (3917448)CaDiCaL version: 2.1.3 % 101.29/14.93 % (3917448)Termination reason: Instruction limit % 101.29/14.93 % (3917448)Termination phase: Saturation % 101.29/14.93 % (3917448)Time elapsed: 0.482 s % 101.29/14.93 % (3917448)Peak memory usage: 92 MB % 101.29/14.93 % (3917448)Instructions burned: 801 (million) % 101.29/14.93 % (3917454)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1198597292:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2943 on theBenchmark for (2943ds/2127Mi) % 101.29/14.93 % (3917449)Instruction limit reached! % 101.29/14.93 % (3917449)------------------------------ % 101.29/14.93 % (3917449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.29/14.93 % (3917449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.29/14.93 % (3917449)CaDiCaL version: 2.1.3 % 101.29/14.93 % (3917449)Termination reason: Instruction limit % 101.29/14.93 % (3917449)Termination phase: Saturation % 101.29/14.93 % (3917449)Time elapsed: 0.578 s % 101.29/14.93 % (3917449)Peak memory usage: 90 MB % 101.29/14.93 % (3917449)Instructions burned: 1026 (million) % 101.29/14.93 % (3917456)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=70836005:i=1959:rtra=on:fsd=on:proc=on_2942 on theBenchmark for (2942ds/1959Mi) % 101.29/14.93 % (3917445)Instruction limit reached! % 101.29/14.93 % (3917445)------------------------------ % 101.29/14.93 % (3917445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.29/14.93 % (3917445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.29/14.93 % (3917445)CaDiCaL version: 2.1.3 % 101.29/14.93 % (3917445)Termination reason: Instruction limit % 101.29/14.93 % (3917445)Termination phase: Saturation % 101.29/14.93 % (3917445)Time elapsed: 1.268 s % 101.29/14.93 % (3917445)Peak memory usage: 119 MB % 101.29/14.93 % (3917445)Instructions burned: 2217 (million) % 101.29/14.93 % (3917458)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=357352882:s2a=on:i=3553:nm=0:rtra=on_2938 on theBenchmark for (2938ds/3553Mi) % 101.29/14.93 % (3917454)Instruction limit reached! % 101.29/14.93 % (3917454)------------------------------ % 101.29/14.93 % (3917454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.29/14.93 % (3917454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.29/14.93 % (3917454)CaDiCaL version: 2.1.3 % 101.29/14.93 % (3917454)Termination reason: Instruction limit % 101.29/14.93 % (3917454)Termination phase: Saturation % 101.29/14.93 % (3917454)Time elapsed: 1.005 s % 101.29/14.93 % (3917454)Peak memory usage: 89 MB % 101.29/14.93 % (3917454)Instructions burned: 2128 (million) % 101.29/14.93 % (3917460)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2723009122:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2932 on theBenchmark for (2932ds/3201Mi) % 101.29/14.93 % (3917456)Instruction limit reached! % 101.29/14.93 % (3917456)------------------------------ % 101.29/14.93 % (3917456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.29/14.93 % (3917456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.29/14.93 % (3917456)CaDiCaL version: 2.1.3 % 101.29/14.93 % (3917456)Termination reason: Instruction limit % 101.29/14.93 % (3917456)Termination phase: Saturation % 101.29/14.93 % (3917456)Time elapsed: 1.232 s % 101.29/14.93 % (3917456)Peak memory usage: 122 MB % 101.29/14.93 % (3917456)Instructions burned: 1960 (million) % 101.29/14.93 % (3917462)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=1273492094:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2928 on theBenchmark for (2928ds/4093Mi) % 116.55/17.10 % (3917450)Instruction limit reached! % 116.55/17.10 % (3917450)------------------------------ % 116.55/17.10 % (3917450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.55/17.10 % (3917450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.55/17.10 % (3917450)CaDiCaL version: 2.1.3 % 116.55/17.10 % (3917450)Termination reason: Instruction limit % 116.55/17.10 % (3917450)Termination phase: Saturation % 116.55/17.10 % (3917450)Time elapsed: 2.350 s % 116.55/17.10 % (3917450)Peak memory usage: 105 MB % 116.55/17.10 % (3917450)Instructions burned: 3509 (million) % 116.55/17.10 % (3917432)Instruction limit reached! % 116.55/17.10 % (3917432)------------------------------ % 116.55/17.10 % (3917432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.55/17.10 % (3917432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.55/17.10 % (3917432)CaDiCaL version: 2.1.3 % 116.55/17.10 % (3917432)Termination reason: Instruction limit % 116.55/17.10 % (3917432)Termination phase: Saturation % 116.55/17.10 % (3917432)Time elapsed: 3.464 s % 116.55/17.10 % (3917432)Peak memory usage: 118 MB % 116.55/17.10 % (3917432)Instructions burned: 6401 (million) % 116.55/17.10 % (3917464)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=2221886536:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2924 on theBenchmark for (2924ds/21173Mi) % 116.55/17.10 % (3917465)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3631186290:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2923 on theBenchmark for (2923ds/10544Mi) % 116.55/17.10 % (3917444)Instruction limit reached! % 116.55/17.10 % (3917444)------------------------------ % 116.55/17.10 % (3917444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.55/17.10 % (3917444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.55/17.10 % (3917444)CaDiCaL version: 2.1.3 % 116.55/17.10 % (3917444)Termination reason: Instruction limit % 116.55/17.10 % (3917444)Termination phase: Saturation % 116.55/17.10 % (3917444)Time elapsed: 3.399 s % 116.55/17.10 % (3917444)Peak memory usage: 135 MB % 116.55/17.10 % (3917444)Instructions burned: 5811 (million) % 116.55/17.10 % (3917468)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1547836160:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2917 on theBenchmark for (2917ds/1262Mi) % 116.55/17.10 % (3917458)Instruction limit reached! % 116.55/17.10 % (3917458)------------------------------ % 116.55/17.10 % (3917458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.55/17.10 % (3917458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.55/17.10 % (3917458)CaDiCaL version: 2.1.3 % 116.55/17.10 % (3917458)Termination reason: Instruction limit % 116.55/17.10 % (3917458)Termination phase: Saturation % 116.55/17.10 % (3917458)Time elapsed: 2.103 s % 116.55/17.10 % (3917458)Peak memory usage: 106 MB % 116.55/17.10 % (3917458)Instructions burned: 3554 (million) % 116.55/17.10 % (3917460)Instruction limit reached! % 116.55/17.10 % (3917460)------------------------------ % 116.55/17.10 % (3917460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.55/17.10 % (3917460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.55/17.10 % (3917460)CaDiCaL version: 2.1.3 % 116.55/17.10 % (3917460)Termination reason: Instruction limit % 116.55/17.10 % (3917460)Termination phase: Saturation % 116.55/17.10 % (3917460)Time elapsed: 1.507 s % 116.55/17.10 % (3917460)Peak memory usage: 93 MB % 116.55/17.10 % (3917460)Instructions burned: 3202 (million) % 116.55/17.10 % (3917470)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4055288898:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2916 on theBenchmark for (2916ds/775Mi) % 116.55/17.10 % (3917471)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4018255129:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2915 on theBenchmark for (2915ds/270Mi) % 116.55/17.10 % (3917471)Instruction limit reached! % 116.55/17.10 % (3917471)------------------------------ % 116.55/17.10 % (3917471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.55/17.10 % (3917471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.55/17.10 % (3917471)CaDiCaL version: 2.1.3 % 116.55/17.10 % (3917471)Termination reason: Instruction limit % 135.40/19.87 % (3917471)Termination phase: Saturation % 135.40/19.87 % (3917471)Time elapsed: 0.187 s % 135.40/19.87 % (3917471)Peak memory usage: 91 MB % 135.40/19.87 % (3917471)Instructions burned: 271 (million) % 135.40/19.87 % (3917474)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=937343739:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2912 on theBenchmark for (2912ds/17165Mi) % 135.40/19.87 % (3917470)Instruction limit reached! % 135.40/19.87 % (3917470)------------------------------ % 135.40/19.87 % (3917470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.40/19.87 % (3917470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.40/19.87 % (3917470)CaDiCaL version: 2.1.3 % 135.40/19.87 % (3917470)Termination reason: Instruction limit % 135.40/19.87 % (3917470)Termination phase: Saturation % 135.40/19.87 % (3917470)Time elapsed: 0.411 s % 135.40/19.87 % (3917470)Peak memory usage: 92 MB % 135.40/19.87 % (3917470)Instructions burned: 775 (million) % 135.40/19.87 % (3917476)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1869968534:s2a=on:i=13094:s2at=-1:rtra=on_2910 on theBenchmark for (2910ds/13094Mi) % 135.40/19.87 % (3917468)Instruction limit reached! % 135.40/19.87 % (3917468)------------------------------ % 135.40/19.87 % (3917468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.40/19.87 % (3917468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.40/19.87 % (3917468)CaDiCaL version: 2.1.3 % 135.40/19.87 % (3917468)Termination reason: Instruction limit % 135.40/19.87 % (3917468)Termination phase: Saturation % 135.40/19.87 % (3917468)Time elapsed: 0.730 s % 135.40/19.87 % (3917468)Peak memory usage: 117 MB % 135.40/19.87 % (3917468)Instructions burned: 1262 (million) % 135.40/19.87 % (3917478)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=252635474:st=2:i=12633:rtra=on:ss=axioms_2909 on theBenchmark for (2909ds/12633Mi) % 135.40/19.87 % (3917462)Instruction limit reached! % 135.40/19.87 % (3917462)------------------------------ % 135.40/19.87 % (3917462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.40/19.87 % (3917462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.40/19.87 % (3917462)CaDiCaL version: 2.1.3 % 135.40/19.87 % (3917462)Termination reason: Instruction limit % 135.40/19.87 % (3917462)Termination phase: Saturation % 135.40/19.87 % (3917462)Time elapsed: 2.556 s % 135.40/19.87 % (3917462)Peak memory usage: 149 MB % 135.40/19.87 % (3917462)Instructions burned: 4094 (million) % 135.40/19.87 % (3917480)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1938281811:i=1783:rtra=on:gtg=position_2901 on theBenchmark for (2901ds/1783Mi) % 135.40/19.87 % (3917480)Instruction limit reached! % 135.40/19.87 % (3917480)------------------------------ % 135.40/19.87 % (3917480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.40/19.87 % (3917480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.40/19.87 % (3917480)CaDiCaL version: 2.1.3 % 135.40/19.87 % (3917480)Termination reason: Instruction limit % 135.40/19.87 % (3917480)Termination phase: Saturation % 135.40/19.87 % (3917480)Time elapsed: 1.011 s % 135.40/19.87 % (3917480)Peak memory usage: 123 MB % 135.40/19.87 % (3917480)Instructions burned: 1783 (million) % 135.40/19.87 % (3917482)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=1469397914:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2889 on theBenchmark for (2889ds/5451Mi) % 135.40/19.87 % (3917438)Instruction limit reached! % 135.40/19.87 % (3917438)------------------------------ % 135.40/19.87 % (3917438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.40/19.87 % (3917438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.40/19.87 % (3917438)CaDiCaL version: 2.1.3 % 135.40/19.87 % (3917438)Termination reason: Instruction limit % 135.40/19.87 % (3917438)Termination phase: Saturation % 135.40/19.87 % (3917438)Time elapsed: 9.739 s % 135.40/19.87 % (3917438)Peak memory usage: 103 MB % 135.40/19.87 % (3917438)Instructions burned: 36817 (million) % 135.40/19.87 % (3917689)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=2978414560:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2858 on theBenchmark for (2858ds/4975Mi) % 135.40/19.87 % (3917482)Instruction limit reached! % 135.40/19.87 % (3917482)------------------------------ % 135.40/19.87 % (3917482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.28/23.43 % (3917482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.28/23.43 % (3917482)CaDiCaL version: 2.1.3 % 161.28/23.43 % (3917482)Termination reason: Instruction limit % 161.28/23.43 % (3917482)Termination phase: Saturation % 161.28/23.43 % (3917482)Time elapsed: 3.140 s % 161.28/23.43 % (3917482)Peak memory usage: 147 MB % 161.28/23.43 % (3917482)Instructions burned: 5451 (million) % 161.28/23.43 % (3917728)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=2444420083:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2857 on theBenchmark for (2857ds/2076Mi) % 161.28/23.43 % (3917465)Instruction limit reached! % 161.28/23.43 % (3917465)------------------------------ % 161.28/23.43 % (3917465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.28/23.43 % (3917465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.28/23.43 % (3917465)CaDiCaL version: 2.1.3 % 161.28/23.43 % (3917465)Termination reason: Instruction limit % 161.28/23.43 % (3917465)Termination phase: Saturation % 161.28/23.43 % (3917465)Time elapsed: 6.916 s % 161.28/23.43 % (3917465)Peak memory usage: 186 MB % 161.28/23.43 % (3917465)Instructions burned: 10545 (million) % 161.28/23.43 % (3917815)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=408211585:i=5145:rtra=on_2852 on theBenchmark for (2852ds/5145Mi) % 161.28/23.43 % (3917476)Instruction limit reached! % 161.28/23.43 % (3917476)------------------------------ % 161.28/23.43 % (3917476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.28/23.43 % (3917476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.28/23.43 % (3917476)CaDiCaL version: 2.1.3 % 161.28/23.43 % (3917476)Termination reason: Instruction limit % 161.28/23.43 % (3917476)Termination phase: Saturation % 161.28/23.43 % (3917476)Time elapsed: 6.219 s % 161.28/23.43 % (3917476)Peak memory usage: 95 MB % 161.28/23.43 % (3917476)Instructions burned: 13095 (million) % 161.28/23.43 % (3917927)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1639437540:i=3509:rtra=on_2847 on theBenchmark for (2847ds/3509Mi) % 161.28/23.43 % (3917728)Instruction limit reached! % 161.28/23.43 % (3917728)------------------------------ % 161.28/23.43 % (3917728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.28/23.43 % (3917728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.28/23.43 % (3917728)CaDiCaL version: 2.1.3 % 161.28/23.43 % (3917728)Termination reason: Instruction limit % 161.28/23.43 % (3917728)Termination phase: Saturation % 161.28/23.43 % (3917728)Time elapsed: 1.209 s % 161.28/23.43 % (3917728)Peak memory usage: 119 MB % 161.28/23.43 % (3917728)Instructions burned: 2076 (million) % 161.28/23.43 % (3917689)Instruction limit reached! % 161.28/23.43 % (3917689)------------------------------ % 161.28/23.43 % (3917689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.28/23.43 % (3917689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.28/23.43 % (3917689)CaDiCaL version: 2.1.3 % 161.28/23.43 % (3917689)Termination reason: Instruction limit % 161.28/23.43 % (3917689)Termination phase: Saturation % 161.28/23.43 % (3917689)Time elapsed: 1.552 s % 161.28/23.43 % (3917689)Peak memory usage: 130 MB % 161.28/23.43 % (3917689)Instructions burned: 4976 (million) % 161.28/23.43 % (3917929)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2616871312:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2843 on theBenchmark for (2843ds/13800Mi) % 161.28/23.43 % (3917930)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2174762733:i=1412:rtra=on:fsd=on:proc=on_2842 on theBenchmark for (2842ds/1412Mi) % 161.28/23.43 % (3917930)Instruction limit reached! % 161.28/23.43 % (3917930)------------------------------ % 161.28/23.43 % (3917930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.28/23.43 % (3917930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.28/23.43 % (3917930)CaDiCaL version: 2.1.3 % 161.28/23.43 % (3917930)Termination reason: Instruction limit % 161.28/23.43 % (3917930)Termination phase: Saturation % 161.28/23.43 % (3917930)Time elapsed: 0.492 s % 161.28/23.43 % (3917930)Peak memory usage: 121 MB % 161.28/23.43 % (3917930)Instructions burned: 1420 (million) % 161.28/23.43 % (3917933)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 % 256.28/36.89 % (3917933)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1324740156:i=11747:aac=none:nm=0:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/11747Mi) % 256.28/36.89 % (3917478)Instruction limit reached! % 256.28/36.89 % (3917478)------------------------------ % 256.28/36.89 % (3917478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.28/36.89 % (3917478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.28/36.89 % (3917478)CaDiCaL version: 2.1.3 % 256.28/36.89 % (3917478)Termination reason: Instruction limit % 256.28/36.89 % (3917478)Termination phase: Saturation % 256.28/36.89 % (3917478)Time elapsed: 7.743 s % 256.28/36.89 % (3917478)Peak memory usage: 139 MB % 256.28/36.89 % (3917478)Instructions burned: 12634 (million) % 256.28/36.89 % (3917935)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1663609630:s2a=on:i=3553:nm=0:rtra=on_2830 on theBenchmark for (2830ds/3553Mi) % 256.28/36.89 % (3917927)Instruction limit reached! % 256.28/36.89 % (3917927)------------------------------ % 256.28/36.89 % (3917927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.28/36.89 % (3917927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.28/36.89 % (3917927)CaDiCaL version: 2.1.3 % 256.28/36.89 % (3917927)Termination reason: Instruction limit % 256.28/36.89 % (3917927)Termination phase: Saturation % 256.28/36.89 % (3917927)Time elapsed: 2.357 s % 256.28/36.89 % (3917927)Peak memory usage: 105 MB % 256.28/36.89 % (3917927)Instructions burned: 3510 (million) % 256.28/36.89 % (3917937)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2985494152:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/3201Mi) % 256.28/36.89 % (3917815)Instruction limit reached! % 256.28/36.89 % (3917815)------------------------------ % 256.28/36.89 % (3917815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.28/36.89 % (3917815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.28/36.89 % (3917815)CaDiCaL version: 2.1.3 % 256.28/36.89 % (3917815)Termination reason: Instruction limit % 256.28/36.89 % (3917815)Termination phase: Saturation % 256.28/36.89 % (3917815)Time elapsed: 3.162 s % 256.28/36.89 % (3917815)Peak memory usage: 100 MB % 256.28/36.89 % (3917815)Instructions burned: 5146 (million) % 256.28/36.89 % (3917939)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=3571534029:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2819 on theBenchmark for (2819ds/4081Mi) % 256.28/36.89 % (3917474)Instruction limit reached! % 256.28/36.89 % (3917474)------------------------------ % 256.28/36.89 % (3917474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.28/36.89 % (3917474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.28/36.89 % (3917474)CaDiCaL version: 2.1.3 % 256.28/36.89 % (3917474)Termination reason: Instruction limit % 256.28/36.89 % (3917474)Termination phase: Saturation % 256.28/36.89 % (3917474)Time elapsed: 9.478 s % 256.28/36.89 % (3917474)Peak memory usage: 175 MB % 256.28/36.89 % (3917474)Instructions burned: 17165 (million) % 256.28/36.89 % (3917941)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=4208319304:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2816 on theBenchmark for (2816ds/20260Mi) % 256.28/36.89 % (3917935)Instruction limit reached! % 256.28/36.89 % (3917935)------------------------------ % 256.28/36.89 % (3917935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.28/36.89 % (3917935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.28/36.89 % (3917935)CaDiCaL version: 2.1.3 % 256.28/36.89 % (3917935)Termination reason: Instruction limit % 256.28/36.89 % (3917935)Termination phase: Saturation % 256.28/36.89 % (3917935)Time elapsed: 2.083 s % 256.28/36.89 % (3917935)Peak memory usage: 105 MB % 256.28/36.89 % (3917935)Instructions burned: 3553 (million) % 256.28/36.89 % (3917464)Instruction limit reached! % 256.28/36.89 % (3917464)------------------------------ % 256.28/36.89 % (3917464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.28/36.89 % (3917464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.28/36.89 % (3917464)CaDiCaL version: 2.1.3 % 256.28/36.89 % (3917464)Termination reason: Instruction limit % 256.28/36.89 % (3917464)Termination phasTerminated %------------------------------------------------------------------------------