%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW826_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:54 PM UTC 2026 % Result : Timeout 299.77s 43.02s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW826_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.19 % Computer : n019.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 14:31:03 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.23 Running first-order theorem proving % 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.42/1.18 % (4043469)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.42/1.18 % (4043476)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3657341012:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.42/1.18 % (4043479)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1954082191:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.42/1.18 % (4043475)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3872610899:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.42/1.18 % (4043478)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1212671740:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.42/1.18 % (4043474)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=371401930:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.42/1.18 % (4043477)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=303195636:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.42/1.18 % (4043478)Instruction limit reached! % 3.42/1.18 % (4043478)------------------------------ % 3.42/1.18 % (4043478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.18 % (4043478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.18 % (4043478)CaDiCaL version: 2.1.3 % 3.42/1.18 % (4043478)Termination reason: Instruction limit % 3.42/1.18 % (4043478)Termination phase: Property scanning % 3.42/1.18 % (4043478)Time elapsed: 0.003 s % 3.42/1.18 % (4043478)Peak memory usage: 85 MB % 3.42/1.18 % (4043478)Instructions burned: 6 (million) % 3.42/1.18 % (4043477)Instruction limit reached! % 3.42/1.18 % (4043477)------------------------------ % 3.42/1.18 % (4043477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.18 % (4043477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.18 % (4043477)CaDiCaL version: 2.1.3 % 3.42/1.18 % (4043477)Termination reason: Instruction limit % 3.42/1.18 % (4043477)Termination phase: Property scanning % 3.42/1.18 % (4043477)Time elapsed: 0.004 s % 3.42/1.18 % (4043477)Peak memory usage: 85 MB % 3.42/1.18 % (4043477)Instructions burned: 8 (million) % 3.42/1.18 % (4043474)Instruction limit reached! % 3.42/1.18 % (4043474)------------------------------ % 3.42/1.18 % (4043474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.18 % (4043474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.18 % (4043474)CaDiCaL version: 2.1.3 % 3.42/1.18 % (4043474)Termination reason: Instruction limit % 3.42/1.18 % (4043474)Termination phase: Property scanning % 3.42/1.18 % (4043474)Time elapsed: 0.006 s % 3.42/1.18 % (4043474)Peak memory usage: 85 MB % 3.42/1.18 % (4043474)Instructions burned: 14 (million) % 3.42/1.18 % (4043480)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=149816811:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.42/1.18 % (4043480)Instruction limit reached! % 3.42/1.18 % (4043480)------------------------------ % 3.42/1.18 % (4043480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.18 % (4043480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.18 % (4043480)CaDiCaL version: 2.1.3 % 3.42/1.18 % (4043480)Termination reason: Instruction limit % 3.42/1.18 % (4043480)Termination phase: Function definition elimination % 3.42/1.18 % (4043480)Time elapsed: 0.017 s % 3.42/1.18 % (4043480)Peak memory usage: 87 MB % 3.42/1.18 % (4043480)Instructions burned: 34 (million) % 3.42/1.18 % (4043476)Instruction limit reached! % 3.42/1.18 % (4043476)------------------------------ % 3.42/1.18 % (4043476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.18 % (4043476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.42/1.18 % (4043476)CaDiCaL version: 2.1.3 % 3.42/1.18 % (4043476)Termination reason: Instruction limit % 3.42/1.18 % (4043476)Termination phase: Saturation % 3.42/1.18 % (4043476)Time elapsed: 0.089 s % 3.42/1.18 % (4043476)Peak memory usage: 118 MB % 3.42/1.18 % (4043476)Instructions burned: 201 (million) % 3.42/1.18 % (4043479)Instruction limit reached! % 3.42/1.18 % (4043479)------------------------------ % 3.42/1.18 % (4043479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.42/1.18 % (4043479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.31 % (4043479)CaDiCaL version: 2.1.3 % 4.34/1.31 % (4043479)Termination reason: Instruction limit % 4.34/1.31 % (4043479)Termination phase: Saturation % 4.34/1.31 % (4043479)Time elapsed: 0.046 s % 4.34/1.31 % (4043479)Peak memory usage: 113 MB % 4.34/1.31 % (4043479)Instructions burned: 47 (million) % 4.34/1.31 % (4043490)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4200283432:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.34/1.31 % (4043488)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3413107913:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 4.34/1.31 % (4043492)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=2337295909:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.34/1.31 % (4043489)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=813973346:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.34/1.31 % (4043488)Refutation not found, incomplete strategy % 4.34/1.31 % (4043488)------------------------------ % 4.34/1.31 % (4043488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.31 % (4043488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.31 % (4043488)CaDiCaL version: 2.1.3 % 4.34/1.31 % (4043488)Termination reason: Refutation not found, incomplete strategy % 4.34/1.31 % (4043488)Time elapsed: 0.006 s % 4.34/1.31 % (4043488)Peak memory usage: 88 MB % 4.34/1.31 % (4043488)Instructions burned: 10 (million) % 4.34/1.31 % (4043492)Instruction limit reached! % 4.34/1.31 % (4043492)------------------------------ % 4.34/1.31 % (4043492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.31 % (4043492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.31 % (4043492)CaDiCaL version: 2.1.3 % 4.34/1.31 % (4043492)Termination reason: Instruction limit % 4.34/1.31 % (4043492)Termination phase: Function definition elimination % 4.34/1.31 % (4043492)Time elapsed: 0.008 s % 4.34/1.31 % (4043492)Peak memory usage: 87 MB % 4.34/1.31 % (4043492)Instructions burned: 32 (million) % 4.34/1.31 % (4043490)Instruction limit reached! % 4.34/1.31 % (4043490)------------------------------ % 4.34/1.31 % (4043490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.31 % (4043490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.31 % (4043490)CaDiCaL version: 2.1.3 % 4.34/1.31 % (4043490)Termination reason: Instruction limit % 4.34/1.31 % (4043490)Termination phase: Preprocessing 3 % 4.34/1.31 % (4043490)Time elapsed: 0.009 s % 4.34/1.31 % (4043490)Peak memory usage: 87 MB % 4.34/1.31 % (4043490)Instructions burned: 17 (million) % 4.34/1.31 % (4043491)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2526075574:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi) % 4.34/1.31 % (4043489)Instruction limit reached! % 4.34/1.31 % (4043489)------------------------------ % 4.34/1.31 % (4043489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.31 % (4043489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.31 % (4043489)CaDiCaL version: 2.1.3 % 4.34/1.31 % (4043489)Termination reason: Instruction limit % 4.34/1.31 % (4043489)Termination phase: Property scanning % 4.34/1.31 % (4043489)Time elapsed: 0.015 s % 4.34/1.31 % (4043489)Peak memory usage: 87 MB % 4.34/1.31 % (4043489)Instructions burned: 30 (million) % 4.34/1.31 % (4043491)Instruction limit reached! % 4.34/1.31 % (4043491)------------------------------ % 4.34/1.31 % (4043491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.34/1.31 % (4043491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.34/1.31 % (4043491)CaDiCaL version: 2.1.3 % 4.34/1.31 % (4043491)Termination reason: Instruction limit % 4.34/1.31 % (4043491)Termination phase: Property scanning % 4.34/1.31 % (4043491)Time elapsed: 0.014 s % 4.34/1.31 % (4043491)Peak memory usage: 87 MB % 4.34/1.31 % (4043491)Instructions burned: 25 (million) % 4.34/1.31 % (4043493)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=396639354:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 4.34/1.31 % (4043475)Instruction limit reached! % 4.96/1.47 % (4043475)------------------------------ % 4.96/1.47 % (4043475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.96/1.47 % (4043475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.96/1.47 % (4043475)CaDiCaL version: 2.1.3 % 4.96/1.47 % (4043475)Termination reason: Instruction limit % 4.96/1.47 % (4043475)Termination phase: Saturation % 4.96/1.47 % (4043475)Time elapsed: 0.204 s % 4.96/1.47 % (4043475)Peak memory usage: 118 MB % 4.96/1.47 % (4043475)Instructions burned: 308 (million) % 4.96/1.47 % (4043493)Instruction limit reached! % 4.96/1.47 % (4043493)------------------------------ % 4.96/1.47 % (4043493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.96/1.47 % (4043493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.96/1.47 % (4043493)CaDiCaL version: 2.1.3 % 4.96/1.47 % (4043493)Termination reason: Instruction limit % 4.96/1.47 % (4043493)Termination phase: Saturation % 4.96/1.47 % (4043493)Time elapsed: 0.044 s % 4.96/1.47 % (4043493)Peak memory usage: 90 MB % 4.96/1.47 % (4043493)Instructions burned: 85 (million) % 4.96/1.47 % (4043499)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1512122904:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 4.96/1.47 % (4043499)Refutation not found, incomplete strategy % 4.96/1.47 % (4043499)------------------------------ % 4.96/1.47 % (4043499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.96/1.47 % (4043499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.96/1.47 % (4043499)CaDiCaL version: 2.1.3 % 4.96/1.47 % (4043499)Termination reason: Refutation not found, incomplete strategy % 4.96/1.47 % (4043499)Time elapsed: 0.003 s % 4.96/1.47 % (4043499)Peak memory usage: 88 MB % 4.96/1.47 % (4043499)Instructions burned: 9 (million) % 4.96/1.47 % (4043498)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3454099247:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 4.96/1.47 % (4043498)Instruction limit reached! % 4.96/1.47 % (4043498)------------------------------ % 4.96/1.47 % (4043498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.96/1.47 % (4043498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.96/1.47 % (4043498)CaDiCaL version: 2.1.3 % 4.96/1.47 % (4043498)Termination reason: Instruction limit % 4.96/1.47 % (4043498)Termination phase: Property scanning % 4.96/1.47 % (4043498)Time elapsed: 0.002 s % 4.96/1.47 % (4043498)Peak memory usage: 85 MB % 4.96/1.47 % (4043498)Instructions burned: 3 (million) % 4.96/1.47 % (4043501)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1488818146:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 4.96/1.47 % (4043501)Instruction limit reached! % 4.96/1.47 % (4043501)------------------------------ % 4.96/1.47 % (4043501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.96/1.47 % (4043501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.96/1.47 % (4043501)CaDiCaL version: 2.1.3 % 4.96/1.47 % (4043501)Termination reason: Instruction limit % 4.96/1.47 % (4043501)Termination phase: Property scanning % 4.96/1.47 % (4043501)Time elapsed: 0.003 s % 4.96/1.47 % (4043501)Peak memory usage: 85 MB % 4.96/1.47 % (4043501)Instructions burned: 5 (million) % 4.96/1.47 % (4043502)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2843771499:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 4.96/1.47 % (4043504)lrs+10_1_thi=all:si=on:fd=off:random_seed=1815952599:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 4.96/1.47 % (4043505)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=135867546:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi) % 4.96/1.47 % (4043504)Instruction limit reached! % 4.96/1.47 % (4043504)------------------------------ % 4.96/1.47 % (4043504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.96/1.47 % (4043504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.96/1.47 % (4043504)CaDiCaL version: 2.1.3 % 4.96/1.47 % (4043504)Termination reason: Instruction limit % 4.96/1.47 % (4043504)Termination phase: Saturation % 4.96/1.47 % (4043504)Time elapsed: 0.026 s % 4.96/1.47 % (4043504)Peak memory usage: 87 MB % 6.26/1.63 % (4043504)Instructions burned: 54 (million) % 6.26/1.63 % (4043505)Instruction limit reached! % 6.26/1.63 % (4043505)------------------------------ % 6.26/1.63 % (4043505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.26/1.63 % (4043505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.26/1.63 % (4043505)CaDiCaL version: 2.1.3 % 6.26/1.63 % (4043505)Termination reason: Instruction limit % 6.26/1.63 % (4043505)Termination phase: Property scanning % 6.26/1.63 % (4043505)Time elapsed: 0.004 s % 6.26/1.63 % (4043505)Peak memory usage: 85 MB % 6.26/1.63 % (4043505)Instructions burned: 9 (million) % 6.26/1.63 % (4043502)Instruction limit reached! % 6.26/1.63 % (4043502)------------------------------ % 6.26/1.63 % (4043502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.26/1.63 % (4043502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.26/1.63 % (4043502)CaDiCaL version: 2.1.3 % 6.26/1.63 % (4043502)Termination reason: Instruction limit % 6.26/1.63 % (4043502)Termination phase: Saturation % 6.26/1.63 % (4043502)Time elapsed: 0.076 s % 6.26/1.63 % (4043502)Peak memory usage: 130 MB % 6.26/1.63 % (4043502)Instructions burned: 66 (million) % 6.26/1.63 % (4043488)------------------------------ % 6.26/1.63 % (4043488)------------------------------ % 6.26/1.63 % (4043499)------------------------------ % 6.26/1.63 % (4043499)------------------------------ % 6.26/1.63 % (4043509)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1256427550:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.26/1.63 % (4043509)Instruction limit reached! % 6.26/1.63 % (4043509)------------------------------ % 6.26/1.63 % (4043509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.26/1.63 % (4043509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.26/1.63 % (4043509)CaDiCaL version: 2.1.3 % 6.26/1.63 % (4043509)Termination reason: Instruction limit % 6.26/1.63 % (4043509)Termination phase: Property scanning % 6.26/1.63 % (4043509)Time elapsed: 0.002 s % 6.26/1.63 % (4043509)Peak memory usage: 85 MB % 6.26/1.63 % (4043509)Instructions burned: 3 (million) % 6.26/1.63 % (4043510)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=420411297:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi) % 6.26/1.63 % (4043510)Instruction limit reached! % 6.26/1.63 % (4043510)------------------------------ % 6.26/1.63 % (4043510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.26/1.63 % (4043510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.26/1.63 % (4043510)CaDiCaL version: 2.1.3 % 6.26/1.63 % (4043510)Termination reason: Instruction limit % 6.26/1.63 % (4043510)Termination phase: Property scanning % 6.26/1.63 % (4043510)Time elapsed: 0.002 s % 6.26/1.63 % (4043510)Peak memory usage: 85 MB % 6.26/1.63 % (4043510)Instructions burned: 3 (million) % 6.26/1.63 % (4043516)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3107499964:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.26/1.63 % (4043516)Instruction limit reached! % 6.26/1.63 % (4043516)------------------------------ % 6.26/1.63 % (4043516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.26/1.63 % (4043516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.26/1.63 % (4043516)CaDiCaL version: 2.1.3 % 6.26/1.63 % (4043516)Termination reason: Instruction limit % 6.26/1.63 % (4043516)Termination phase: Property scanning % 6.26/1.63 % (4043516)Time elapsed: 0.009 s % 6.26/1.63 % (4043516)Peak memory usage: 87 MB % 6.26/1.63 % (4043516)Instructions burned: 31 (million) % 6.26/1.63 % (4043514)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=612827168:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.26/1.63 % (4043515)dis+10_1_si=on:random_seed=2216460378:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.26/1.63 % (4043515)Instruction limit reached! % 6.26/1.63 % (4043515)------------------------------ % 6.26/1.63 % (4043515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.26/1.63 % (4043515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.26/1.63 % (4043515)CaDiCaL version: 2.1.3 % 6.26/1.63 % (4043515)Termination reason: Instruction limit % 6.26/1.63 % (4043515)Termination phase: Property scanning % 6.26/1.63 % (4043515)Time elapsed: 0.005 s % 6.26/1.63 % (4043515)Peak memory usage: 85 MB % 6.26/1.63 % (4043515)Instructions burned: 11 (million) % 7.34/1.86 % (4043521)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2479911121:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi) % 7.34/1.86 % (4043518)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3848034827:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi) % 7.34/1.86 % (4043517)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=860242061: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) % 7.34/1.86 % (4043518)Instruction limit reached! % 7.34/1.86 % (4043518)------------------------------ % 7.34/1.86 % (4043518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.86 % (4043518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.86 % (4043518)CaDiCaL version: 2.1.3 % 7.34/1.86 % (4043518)Termination reason: Instruction limit % 7.34/1.86 % (4043518)Termination phase: Property scanning % 7.34/1.86 % (4043518)Time elapsed: 0.002 s % 7.34/1.86 % (4043518)Peak memory usage: 85 MB % 7.34/1.86 % (4043518)Instructions burned: 3 (million) % 7.34/1.86 % (4043521)Instruction limit reached! % 7.34/1.86 % (4043521)------------------------------ % 7.34/1.86 % (4043521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.86 % (4043521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.86 % (4043521)CaDiCaL version: 2.1.3 % 7.34/1.86 % (4043521)Termination reason: Instruction limit % 7.34/1.86 % (4043521)Termination phase: Property scanning % 7.34/1.86 % (4043521)Time elapsed: 0.004 s % 7.34/1.86 % (4043521)Peak memory usage: 85 MB % 7.34/1.86 % (4043521)Instructions burned: 8 (million) % 7.34/1.86 % (4043517)Instruction limit reached! % 7.34/1.86 % (4043517)------------------------------ % 7.34/1.86 % (4043517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.86 % (4043517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.86 % (4043517)CaDiCaL version: 2.1.3 % 7.34/1.86 % (4043517)Termination reason: Instruction limit % 7.34/1.86 % (4043517)Termination phase: Function definition elimination % 7.34/1.86 % (4043517)Time elapsed: 0.019 s % 7.34/1.86 % (4043517)Peak memory usage: 87 MB % 7.34/1.86 % (4043517)Instructions burned: 35 (million) % 7.34/1.86 % (4043522)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4248237695:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi) % 7.34/1.86 % (4043525)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1557868063:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi) % 7.34/1.86 % (4043525)Instruction limit reached! % 7.34/1.86 % (4043525)------------------------------ % 7.34/1.86 % (4043525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.86 % (4043525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.86 % (4043525)CaDiCaL version: 2.1.3 % 7.34/1.86 % (4043525)Termination reason: Instruction limit % 7.34/1.86 % (4043525)Termination phase: Property scanning % 7.34/1.86 % (4043525)Time elapsed: 0.004 s % 7.34/1.86 % (4043525)Peak memory usage: 85 MB % 7.34/1.86 % (4043525)Instructions burned: 17 (million) % 7.34/1.86 % (4043514)Instruction limit reached! % 7.34/1.86 % (4043514)------------------------------ % 7.34/1.86 % (4043514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.86 % (4043514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.86 % (4043514)CaDiCaL version: 2.1.3 % 7.34/1.86 % (4043514)Termination reason: Instruction limit % 7.34/1.86 % (4043514)Termination phase: Saturation % 7.34/1.86 % (4043514)Time elapsed: 0.103 s % 7.34/1.86 % (4043514)Peak memory usage: 117 MB % 7.34/1.86 % (4043514)Instructions burned: 127 (million) % 7.34/1.86 % (4043527)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2382528981:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi) % 7.34/1.86 % (4043536)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=2054606763:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi) % 7.34/1.86 % (4043534)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=776520622:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi) % 9.97/2.09 % (4043532)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1090837516:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi) % 9.97/2.09 % (4043531)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3791062253:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi) % 9.97/2.09 % (4043527)Refutation not found, incomplete strategy % 9.97/2.09 % (4043527)------------------------------ % 9.97/2.09 % (4043527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.97/2.09 % (4043527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.97/2.09 % (4043527)CaDiCaL version: 2.1.3 % 9.97/2.09 % (4043527)Termination reason: Refutation not found, incomplete strategy % 9.97/2.09 % (4043527)Time elapsed: 0.033 s % 9.97/2.09 % (4043527)Peak memory usage: 111 MB % 9.97/2.09 % (4043527)Instructions burned: 19 (million) % 9.97/2.09 % (4043531)Instruction limit reached! % 9.97/2.09 % (4043531)------------------------------ % 9.97/2.09 % (4043531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.97/2.09 % (4043531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.97/2.09 % (4043531)CaDiCaL version: 2.1.3 % 9.97/2.09 % (4043531)Termination reason: Instruction limit % 9.97/2.09 % (4043531)Termination phase: shuffling % 9.97/2.09 % (4043531)Time elapsed: 0.006 s % 9.97/2.09 % (4043531)Peak memory usage: 85 MB % 9.97/2.09 % (4043531)Instructions burned: 10 (million) % 9.97/2.09 % (4043534)Instruction limit reached! % 9.97/2.09 % (4043534)------------------------------ % 9.97/2.09 % (4043534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.97/2.09 % (4043534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.97/2.09 % (4043534)CaDiCaL version: 2.1.3 % 9.97/2.09 % (4043534)Termination reason: Instruction limit % 9.97/2.09 % (4043534)Termination phase: Saturation % 9.97/2.09 % (4043534)Time elapsed: 0.041 s % 9.97/2.09 % (4043534)Peak memory usage: 90 MB % 9.97/2.09 % (4043534)Instructions burned: 75 (million) % 9.97/2.09 % (4043537)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=603039000:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi) % 9.97/2.09 % (4043532)Instruction limit reached! % 9.97/2.09 % (4043532)------------------------------ % 9.97/2.09 % (4043532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.97/2.09 % (4043532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.97/2.09 % (4043532)CaDiCaL version: 2.1.3 % 9.97/2.09 % (4043532)Termination reason: Instruction limit % 9.97/2.09 % (4043532)Termination phase: Saturation % 9.97/2.09 % (4043532)Time elapsed: 0.077 s % 9.97/2.09 % (4043532)Peak memory usage: 130 MB % 9.97/2.09 % (4043532)Instructions burned: 72 (million) % 9.97/2.09 % (4043536)Instruction limit reached! % 9.97/2.09 % (4043536)------------------------------ % 9.97/2.09 % (4043536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.97/2.09 % (4043536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.97/2.09 % (4043536)CaDiCaL version: 2.1.3 % 9.97/2.09 % (4043536)Termination reason: Instruction limit % 9.97/2.09 % (4043536)Termination phase: Saturation % 9.97/2.09 % (4043536)Time elapsed: 0.094 s % 9.97/2.09 % (4043536)Peak memory usage: 92 MB % 9.97/2.09 % (4043536)Instructions burned: 294 (million) % 9.97/2.09 % (4043522)Instruction limit reached! % 9.97/2.09 % (4043522)------------------------------ % 9.97/2.09 % (4043522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.97/2.09 % (4043522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.97/2.09 % (4043522)CaDiCaL version: 2.1.3 % 9.97/2.09 % (4043522)Termination reason: Instruction limit % 9.97/2.09 % (4043522)Termination phase: Saturation % 9.97/2.09 % (4043522)Time elapsed: 0.232 s % 9.97/2.09 % (4043522)Peak memory usage: 94 MB % 9.97/2.09 % (4043522)Instructions burned: 370 (million) % 9.97/2.09 % (4043543)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=66558858:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi) % 9.97/2.09 % (4043537)Instruction limit reached! % 9.97/2.09 % (4043537)------------------------------ % 9.97/2.09 % (4043537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.42/2.40 % (4043537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.42/2.40 % (4043537)CaDiCaL version: 2.1.3 % 11.42/2.40 % (4043537)Termination reason: Instruction limit % 11.42/2.40 % (4043537)Termination phase: Saturation % 11.42/2.40 % (4043537)Time elapsed: 0.097 s % 11.42/2.40 % (4043537)Peak memory usage: 117 MB % 11.42/2.40 % (4043537)Instructions burned: 131 (million) % 11.42/2.40 % (4043544)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3634165632:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi) % 11.42/2.40 % (4043547)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1764217934:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi) % 11.42/2.40 % (4043544)Instruction limit reached! % 11.42/2.40 % (4043544)------------------------------ % 11.42/2.40 % (4043544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.42/2.40 % (4043544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.42/2.40 % (4043544)CaDiCaL version: 2.1.3 % 11.42/2.40 % (4043544)Termination reason: Instruction limit % 11.42/2.40 % (4043544)Termination phase: Property scanning % 11.42/2.40 % (4043544)Time elapsed: 0.020 s % 11.42/2.40 % (4043544)Peak memory usage: 87 MB % 11.42/2.40 % (4043544)Instructions burned: 42 (million) % 11.42/2.40 % (4043546)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4140288831:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi) % 11.42/2.40 % (4043548)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=525899933:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 11.42/2.40 % (4043527)------------------------------ % 11.42/2.40 % (4043527)------------------------------ % 11.42/2.40 % (4043543)Instruction limit reached! % 11.42/2.40 % (4043543)------------------------------ % 11.42/2.40 % (4043543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.42/2.40 % (4043543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.42/2.40 % (4043543)CaDiCaL version: 2.1.3 % 11.42/2.40 % (4043543)Termination reason: Instruction limit % 11.42/2.40 % (4043543)Termination phase: Saturation % 11.42/2.40 % (4043543)Time elapsed: 0.126 s % 11.42/2.40 % (4043543)Peak memory usage: 135 MB % 11.42/2.40 % (4043543)Instructions burned: 132 (million) % 11.42/2.40 % (4043550)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=2157089826:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi) % 11.42/2.40 % (4043550)Refutation not found, incomplete strategy % 11.42/2.40 % (4043550)------------------------------ % 11.42/2.40 % (4043550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.42/2.40 % (4043550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.42/2.40 % (4043550)CaDiCaL version: 2.1.3 % 11.42/2.40 % (4043550)Termination reason: Refutation not found, incomplete strategy % 11.42/2.40 % (4043550)Time elapsed: 0.034 s % 11.42/2.40 % (4043550)Peak memory usage: 111 MB % 11.42/2.40 % (4043550)Instructions burned: 20 (million) % 11.42/2.40 % (4043553)dis+10_1_si=on:random_seed=3798786859:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi) % 11.42/2.40 % (4043548)Instruction limit reached! % 11.42/2.40 % (4043548)------------------------------ % 11.42/2.40 % (4043548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.42/2.40 % (4043548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.42/2.40 % (4043548)CaDiCaL version: 2.1.3 % 11.42/2.40 % (4043548)Termination reason: Instruction limit % 11.42/2.40 % (4043548)Termination phase: Saturation % 11.42/2.40 % (4043548)Time elapsed: 0.096 s % 11.42/2.40 % (4043548)Peak memory usage: 118 MB % 11.42/2.40 % (4043548)Instructions burned: 132 (million) % 11.42/2.40 % (4043546)Instruction limit reached! % 11.42/2.40 % (4043546)------------------------------ % 11.42/2.40 % (4043546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.42/2.40 % (4043546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.42/2.40 % (4043546)CaDiCaL version: 2.1.3 % 11.42/2.40 % (4043546)Termination reason: Instruction limit % 11.42/2.40 % (4043546)Termination phase: Saturation % 11.42/2.40 % (4043546)Time elapsed: 0.170 s % 11.42/2.40 % (4043546)Peak memory usage: 92 MB % 11.42/2.40 % (4043546)Instructions burned: 308 (million) % 12.10/2.59 % (4043557)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1233613557:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi) % 12.10/2.59 % (4043556)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=367379377:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi) % 12.10/2.59 % (4043547)Instruction limit reached! % 12.10/2.59 % (4043547)------------------------------ % 12.10/2.59 % (4043547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.59 % (4043547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.59 % (4043547)CaDiCaL version: 2.1.3 % 12.10/2.59 % (4043547)Termination reason: Instruction limit % 12.10/2.59 % (4043547)Termination phase: Saturation % 12.10/2.59 % (4043547)Time elapsed: 0.231 s % 12.10/2.59 % (4043547)Peak memory usage: 140 MB % 12.10/2.59 % (4043547)Instructions burned: 598 (million) % 12.10/2.59 % (4043557)Instruction limit reached! % 12.10/2.59 % (4043557)------------------------------ % 12.10/2.59 % (4043557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.59 % (4043557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.59 % (4043557)CaDiCaL version: 2.1.3 % 12.10/2.59 % (4043557)Termination reason: Instruction limit % 12.10/2.59 % (4043557)Termination phase: Saturation % 12.10/2.59 % (4043557)Time elapsed: 0.088 s % 12.10/2.59 % (4043557)Peak memory usage: 91 MB % 12.10/2.59 % (4043557)Instructions burned: 141 (million) % 12.10/2.59 % (4043560)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2523661981:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi) % 12.10/2.59 % (4043564)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=2118913482:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi) % 12.10/2.59 % (4043563)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2099617566:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi) % 12.10/2.59 % (4043564)Refutation not found, incomplete strategy % 12.10/2.59 % (4043564)------------------------------ % 12.10/2.59 % (4043564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.59 % (4043564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.59 % (4043564)CaDiCaL version: 2.1.3 % 12.10/2.59 % (4043564)Termination reason: Refutation not found, incomplete strategy % 12.10/2.59 % (4043564)Time elapsed: 0.037 s % 12.10/2.59 % (4043564)Peak memory usage: 114 MB % 12.10/2.59 % (4043564)Instructions burned: 74 (million) % 12.10/2.59 % (4043560)Refutation not found, incomplete strategy % 12.10/2.59 % (4043560)------------------------------ % 12.10/2.59 % (4043560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.59 % (4043560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.59 % (4043560)CaDiCaL version: 2.1.3 % 12.10/2.59 % (4043560)Termination reason: Refutation not found, incomplete strategy % 12.10/2.59 % (4043560)Time elapsed: 0.059 s % 12.10/2.59 % (4043560)Peak memory usage: 114 MB % 12.10/2.59 % (4043560)Instructions burned: 63 (million) % 12.10/2.59 % (4043550)------------------------------ % 12.10/2.59 % (4043550)------------------------------ % 12.10/2.59 % (4043563)Instruction limit reached! % 12.10/2.59 % (4043563)------------------------------ % 12.10/2.59 % (4043563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.59 % (4043563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.59 % (4043563)CaDiCaL version: 2.1.3 % 12.10/2.59 % (4043563)Termination reason: Instruction limit % 12.10/2.59 % (4043563)Termination phase: Saturation % 12.10/2.59 % (4043563)Time elapsed: 0.071 s % 12.10/2.59 % (4043563)Peak memory usage: 90 MB % 12.10/2.59 % (4043563)Instructions burned: 122 (million) % 12.10/2.59 % (4043566)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=2196404316:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi) % 12.10/2.59 % (4043556)Instruction limit reached! % 12.10/2.59 % (4043556)------------------------------ % 12.10/2.59 % (4043556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.10/2.59 % (4043556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.10/2.59 % (4043556)CaDiCaL version: 2.1.3 % 12.10/2.59 % (4043556)Termination reason: Instruction limit % 15.02/2.97 % (4043556)Termination phase: Saturation % 15.02/2.97 % (4043556)Time elapsed: 0.229 s % 15.02/2.97 % (4043556)Peak memory usage: 98 MB % 15.02/2.97 % (4043556)Instructions burned: 384 (million) % 15.02/2.97 % (4043566)Instruction limit reached! % 15.02/2.97 % (4043566)------------------------------ % 15.02/2.97 % (4043566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.02/2.97 % (4043566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.02/2.97 % (4043566)CaDiCaL version: 2.1.3 % 15.02/2.97 % (4043566)Termination reason: Instruction limit % 15.02/2.97 % (4043566)Termination phase: Property scanning % 15.02/2.97 % (4043566)Time elapsed: 0.019 s % 15.02/2.97 % (4043566)Peak memory usage: 87 MB % 15.02/2.97 % (4043566)Instructions burned: 39 (million) % 15.02/2.97 % (4043564)------------------------------ % 15.02/2.97 % (4043564)------------------------------ % 15.02/2.97 % (4043569)dis+1010_1_to=kbo:si=on:random_seed=1690428035:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi) % 15.02/2.97 % (4043570)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1180630686:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi) % 15.02/2.97 % (4043572)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2859878284:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi) % 15.02/2.97 % (4043573)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3261532823:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi) % 15.02/2.97 % (4043574)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1738997326:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi) % 15.02/2.97 % (4043560)------------------------------ % 15.02/2.97 % (4043560)------------------------------ % 15.02/2.97 % (4043569)Instruction limit reached! % 15.02/2.97 % (4043569)------------------------------ % 15.02/2.97 % (4043569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.02/2.97 % (4043569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.02/2.97 % (4043569)CaDiCaL version: 2.1.3 % 15.02/2.97 % (4043569)Termination reason: Instruction limit % 15.02/2.97 % (4043569)Termination phase: Saturation % 15.02/2.97 % (4043569)Time elapsed: 0.108 s % 15.02/2.97 % (4043569)Peak memory usage: 91 MB % 15.02/2.97 % (4043569)Instructions burned: 175 (million) % 15.02/2.97 % (4043574)Instruction limit reached! % 15.02/2.97 % (4043574)------------------------------ % 15.02/2.97 % (4043574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.02/2.97 % (4043574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.02/2.97 % (4043574)CaDiCaL version: 2.1.3 % 15.02/2.97 % (4043574)Termination reason: Instruction limit % 15.02/2.97 % (4043574)Termination phase: Saturation % 15.02/2.97 % (4043574)Time elapsed: 0.128 s % 15.02/2.97 % (4043574)Peak memory usage: 120 MB % 15.02/2.97 % (4043574)Instructions burned: 351 (million) % 15.02/2.97 % (4043553)Instruction limit reached! % 15.02/2.97 % (4043553)------------------------------ % 15.02/2.97 % (4043553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.02/2.97 % (4043553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.02/2.97 % (4043553)CaDiCaL version: 2.1.3 % 15.02/2.97 % (4043553)Termination reason: Instruction limit % 15.02/2.97 % (4043553)Termination phase: Saturation % 15.02/2.97 % (4043553)Time elapsed: 0.569 s % 15.02/2.97 % (4043553)Peak memory usage: 95 MB % 15.02/2.97 % (4043553)Instructions burned: 1001 (million) % 15.02/2.97 % (4043573)Instruction limit reached! % 15.02/2.97 % (4043573)------------------------------ % 15.02/2.97 % (4043573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.02/2.97 % (4043573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.02/2.97 % (4043573)CaDiCaL version: 2.1.3 % 15.02/2.97 % (4043573)Termination reason: Instruction limit % 15.02/2.97 % (4043573)Termination phase: Saturation % 15.02/2.97 % (4043573)Time elapsed: 0.158 s % 15.02/2.97 % (4043573)Peak memory usage: 137 MB % 15.02/2.97 % (4043573)Instructions burned: 216 (million) % 15.02/2.97 % (4043581)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1557409095:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi) % 15.02/2.97 % (4043580)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1311647839:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi) % 17.80/3.21 % (4043580)Refutation not found, incomplete strategy % 17.80/3.21 % (4043580)------------------------------ % 17.80/3.21 % (4043580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.21 % (4043580)CaDiCaL version: 2.1.3 % 17.80/3.21 % (4043580)Termination reason: Refutation not found, incomplete strategy % 17.80/3.21 % (4043580)Time elapsed: 0.008 s % 17.80/3.21 % (4043580)Peak memory usage: 88 MB % 17.80/3.21 % (4043580)Instructions burned: 15 (million) % 17.80/3.21 % (4043570)Instruction limit reached! % 17.80/3.21 % (4043570)------------------------------ % 17.80/3.21 % (4043570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.21 % (4043570)CaDiCaL version: 2.1.3 % 17.80/3.21 % (4043570)Termination reason: Instruction limit % 17.80/3.21 % (4043570)Termination phase: Saturation % 17.80/3.21 % (4043570)Time elapsed: 0.250 s % 17.80/3.21 % (4043570)Peak memory usage: 119 MB % 17.80/3.21 % (4043570)Instructions burned: 329 (million) % 17.80/3.21 % (4043582)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=336738713:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi) % 17.80/3.21 % (4043583)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=224426405:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi) % 17.80/3.21 % (4043583)Refutation not found, incomplete strategy % 17.80/3.21 % (4043583)------------------------------ % 17.80/3.21 % (4043583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.21 % (4043583)CaDiCaL version: 2.1.3 % 17.80/3.21 % (4043583)Termination reason: Refutation not found, incomplete strategy % 17.80/3.21 % (4043583)Time elapsed: 0.008 s % 17.80/3.21 % (4043583)Peak memory usage: 88 MB % 17.80/3.21 % (4043583)Instructions burned: 15 (million) % 17.80/3.21 % (4043586)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2552775607:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi) % 17.80/3.21 % (4043586)Refutation not found, incomplete strategy % 17.80/3.21 % (4043586)------------------------------ % 17.80/3.21 % (4043586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.21 % (4043586)CaDiCaL version: 2.1.3 % 17.80/3.21 % (4043586)Termination reason: Refutation not found, incomplete strategy % 17.80/3.21 % (4043586)Time elapsed: 0.033 s % 17.80/3.21 % (4043586)Peak memory usage: 112 MB % 17.80/3.21 % (4043586)Instructions burned: 19 (million) % 17.80/3.21 % (4043587)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2478672078:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi) % 17.80/3.21 % (4043582)Instruction limit reached! % 17.80/3.21 % (4043582)------------------------------ % 17.80/3.21 % (4043582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.21 % (4043582)CaDiCaL version: 2.1.3 % 17.80/3.21 % (4043582)Termination reason: Instruction limit % 17.80/3.21 % (4043582)Termination phase: Saturation % 17.80/3.21 % (4043582)Time elapsed: 0.108 s % 17.80/3.21 % (4043582)Peak memory usage: 119 MB % 17.80/3.21 % (4043582)Instructions burned: 283 (million) % 17.80/3.21 % (4043572)Instruction limit reached! % 17.80/3.21 % (4043572)------------------------------ % 17.80/3.21 % (4043572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.80/3.21 % (4043572)CaDiCaL version: 2.1.3 % 17.80/3.21 % (4043572)Termination reason: Instruction limit % 17.80/3.21 % (4043572)Termination phase: Saturation % 17.80/3.21 % (4043572)Time elapsed: 0.343 s % 17.80/3.21 % (4043572)Peak memory usage: 136 MB % 17.80/3.21 % (4043572)Instructions burned: 483 (million) % 17.80/3.21 % (4043587)Refutation not found, incomplete strategy % 17.80/3.21 % (4043587)------------------------------ % 17.80/3.21 % (4043587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.80/3.21 % (4043587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.09/3.50 % (4043587)CaDiCaL version: 2.1.3 % 19.09/3.50 % (4043587)Termination reason: Refutation not found, incomplete strategy % 19.09/3.50 % (4043587)Time elapsed: 0.032 s % 19.09/3.50 % (4043587)Peak memory usage: 111 MB % 19.09/3.50 % (4043587)Instructions burned: 19 (million) % 19.09/3.50 % (4043581)Instruction limit reached! % 19.09/3.50 % (4043581)------------------------------ % 19.09/3.50 % (4043581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.09/3.50 % (4043581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.09/3.50 % (4043581)CaDiCaL version: 2.1.3 % 19.09/3.50 % (4043581)Termination reason: Instruction limit % 19.09/3.50 % (4043581)Termination phase: Saturation % 19.09/3.50 % (4043581)Time elapsed: 0.221 s % 19.09/3.50 % (4043581)Peak memory usage: 119 MB % 19.09/3.50 % (4043581)Instructions burned: 329 (million) % 19.09/3.50 % (4043580)------------------------------ % 19.09/3.50 % (4043580)------------------------------ % 19.09/3.50 % (4043592)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2438450251:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi) % 19.09/3.50 % (4043593)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=1483852403:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi) % 19.09/3.50 % (4043583)------------------------------ % 19.09/3.50 % (4043583)------------------------------ % 19.09/3.50 % (4043594)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2899608854:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi) % 19.09/3.50 % (4043586)------------------------------ % 19.09/3.50 % (4043586)------------------------------ % 19.09/3.50 % (4043596)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3588352870:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi) % 19.09/3.50 % (4043592)Instruction limit reached! % 19.09/3.50 % (4043592)------------------------------ % 19.09/3.50 % (4043592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.09/3.50 % (4043592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.09/3.50 % (4043592)CaDiCaL version: 2.1.3 % 19.09/3.50 % (4043592)Termination reason: Instruction limit % 19.09/3.50 % (4043592)Termination phase: Saturation % 19.09/3.50 % (4043592)Time elapsed: 0.172 s % 19.09/3.50 % (4043592)Peak memory usage: 121 MB % 19.09/3.50 % (4043592)Instructions burned: 472 (million) % 19.09/3.50 % (4043587)------------------------------ % 19.09/3.50 % (4043587)------------------------------ % 19.09/3.50 % (4043596)Refutation not found, incomplete strategy % 19.09/3.50 % (4043596)------------------------------ % 19.09/3.50 % (4043596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.09/3.50 % (4043596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.09/3.50 % (4043596)CaDiCaL version: 2.1.3 % 19.09/3.50 % (4043596)Termination reason: Refutation not found, incomplete strategy % 19.09/3.50 % (4043596)Time elapsed: 0.034 s % 19.09/3.50 % (4043596)Peak memory usage: 112 MB % 19.09/3.50 % (4043596)Instructions burned: 21 (million) % 19.09/3.50 % (4043598)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2133029855:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi) % 19.09/3.50 % (4043602)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2062635802:i=359:rtra=on:gtg=exists_top:ss=axioms_2978 on theBenchmark for (2978ds/359Mi) % 19.09/3.50 % (4043601)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4126655268:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi) % 19.09/3.50 % (4043593)Instruction limit reached! % 19.09/3.50 % (4043593)------------------------------ % 19.09/3.50 % (4043593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.09/3.50 % (4043593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.09/3.50 % (4043593)CaDiCaL version: 2.1.3 % 19.09/3.50 % (4043593)Termination reason: Instruction limit % 19.09/3.50 % (4043593)Termination phase: Saturation % 19.09/3.50 % (4043593)Time elapsed: 0.219 s % 19.09/3.50 % (4043593)Peak memory usage: 135 MB % 19.09/3.50 % (4043593)Instructions burned: 276 (million) % 19.09/3.50 % (4043603)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3084706728:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi) % 20.86/3.90 % (4043594)Instruction limit reached! % 20.86/3.90 % (4043594)------------------------------ % 20.86/3.90 % (4043594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.86/3.90 % (4043594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.86/3.90 % (4043594)CaDiCaL version: 2.1.3 % 20.86/3.90 % (4043594)Termination reason: Instruction limit % 20.86/3.90 % (4043594)Termination phase: Saturation % 20.86/3.90 % (4043594)Time elapsed: 0.248 s % 20.86/3.90 % (4043594)Peak memory usage: 120 MB % 20.86/3.90 % (4043594)Instructions burned: 375 (million) % 20.86/3.90 % (4043602)Instruction limit reached! % 20.86/3.90 % (4043602)------------------------------ % 20.86/3.90 % (4043602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.86/3.90 % (4043602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.86/3.90 % (4043602)CaDiCaL version: 2.1.3 % 20.86/3.90 % (4043602)Termination reason: Instruction limit % 20.86/3.90 % (4043602)Termination phase: Saturation % 20.86/3.90 % (4043602)Time elapsed: 0.102 s % 20.86/3.90 % (4043602)Peak memory usage: 91 MB % 20.86/3.90 % (4043602)Instructions burned: 362 (million) % 20.86/3.90 % (4043607)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=650275576:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi) % 20.86/3.90 % (4043596)------------------------------ % 20.86/3.90 % (4043596)------------------------------ % 20.86/3.90 % (4043607)Refutation not found, incomplete strategy % 20.86/3.90 % (4043607)------------------------------ % 20.86/3.90 % (4043607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.86/3.90 % (4043607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.86/3.90 % (4043607)CaDiCaL version: 2.1.3 % 20.86/3.90 % (4043607)Termination reason: Refutation not found, incomplete strategy % 20.86/3.90 % (4043607)Time elapsed: 0.031 s % 20.86/3.90 % (4043607)Peak memory usage: 111 MB % 20.86/3.90 % (4043607)Instructions burned: 14 (million) % 20.86/3.90 % (4043610)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1689068104:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2976 on theBenchmark for (2976ds/273Mi) % 20.86/3.90 % (4043609)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=34330653:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi) % 20.86/3.90 % (4043601)Instruction limit reached! % 20.86/3.90 % (4043601)------------------------------ % 20.86/3.90 % (4043601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.86/3.90 % (4043601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.86/3.90 % (4043601)CaDiCaL version: 2.1.3 % 20.86/3.90 % (4043601)Termination reason: Instruction limit % 20.86/3.90 % (4043601)Termination phase: Saturation % 20.86/3.90 % (4043601)Time elapsed: 0.252 s % 20.86/3.90 % (4043601)Peak memory usage: 137 MB % 20.86/3.90 % (4043601)Instructions burned: 335 (million) % 20.86/3.90 % (4043609)Refutation not found, incomplete strategy % 20.86/3.90 % (4043609)------------------------------ % 20.86/3.90 % (4043609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.86/3.90 % (4043609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.86/3.90 % (4043609)CaDiCaL version: 2.1.3 % 20.86/3.90 % (4043609)Termination reason: Refutation not found, incomplete strategy % 20.86/3.90 % (4043609)Time elapsed: 0.033 s % 20.86/3.90 % (4043609)Peak memory usage: 112 MB % 20.86/3.90 % (4043609)Instructions burned: 20 (million) % 20.86/3.90 % (4043610)Instruction limit reached! % 20.86/3.90 % (4043610)------------------------------ % 20.86/3.90 % (4043610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.86/3.90 % (4043610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.86/3.90 % (4043610)CaDiCaL version: 2.1.3 % 20.86/3.90 % (4043610)Termination reason: Instruction limit % 20.86/3.90 % (4043610)Termination phase: Saturation % 20.86/3.90 % (4043610)Time elapsed: 0.098 s % 20.86/3.90 % (4043610)Peak memory usage: 93 MB % 20.86/3.90 % (4043610)Instructions burned: 276 (million) % 20.86/3.90 % (4043598)Instruction limit reached! % 20.86/3.90 % (4043598)------------------------------ % 26.09/4.45 % (4043598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.09/4.45 % (4043598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.09/4.45 % (4043598)CaDiCaL version: 2.1.3 % 26.09/4.45 % (4043598)Termination reason: Instruction limit % 26.09/4.45 % (4043598)Termination phase: Saturation % 26.09/4.45 % (4043598)Time elapsed: 0.324 s % 26.09/4.45 % (4043598)Peak memory usage: 95 MB % 26.09/4.45 % (4043598)Instructions burned: 513 (million) % 26.09/4.45 % (4043603)Instruction limit reached! % 26.09/4.45 % (4043603)------------------------------ % 26.09/4.45 % (4043603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.09/4.45 % (4043603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.09/4.45 % (4043603)CaDiCaL version: 2.1.3 % 26.09/4.45 % (4043603)Termination reason: Instruction limit % 26.09/4.45 % (4043603)Termination phase: Saturation % 26.09/4.45 % (4043603)Time elapsed: 0.238 s % 26.09/4.45 % (4043603)Peak memory usage: 125 MB % 26.09/4.45 % (4043603)Instructions burned: 342 (million) % 26.09/4.45 % (4043612)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2611631666:i=146:doe=on:rtra=on_2975 on theBenchmark for (2975ds/146Mi) % 26.09/4.45 % (4043616)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=2056987372:avsq=on:i=276:avsqr=1,2:rtra=on_2974 on theBenchmark for (2974ds/276Mi) % 26.09/4.45 % (4043615)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2692299821:i=4428:doe=on:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/4428Mi) % 26.09/4.45 % (4043612)Instruction limit reached! % 26.09/4.45 % (4043612)------------------------------ % 26.09/4.45 % (4043612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.09/4.45 % (4043612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.09/4.45 % (4043612)CaDiCaL version: 2.1.3 % 26.09/4.45 % (4043612)Termination reason: Instruction limit % 26.09/4.45 % (4043612)Termination phase: Saturation % 26.09/4.45 % (4043612)Time elapsed: 0.093 s % 26.09/4.45 % (4043612)Peak memory usage: 91 MB % 26.09/4.45 % (4043612)Instructions burned: 146 (million) % 26.09/4.45 % (4043607)------------------------------ % 26.09/4.45 % (4043607)------------------------------ % 26.09/4.45 % (4043619)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4123448450:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi) % 26.09/4.45 % (4043618)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=258383812:i=1052:rtra=on_2974 on theBenchmark for (2974ds/1052Mi) % 26.09/4.45 % (4043616)Instruction limit reached! % 26.09/4.45 % (4043616)------------------------------ % 26.09/4.45 % (4043616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.09/4.45 % (4043616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.09/4.45 % (4043616)CaDiCaL version: 2.1.3 % 26.09/4.45 % (4043616)Termination reason: Instruction limit % 26.09/4.45 % (4043616)Termination phase: Saturation % 26.09/4.45 % (4043616)Time elapsed: 0.125 s % 26.09/4.45 % (4043616)Peak memory usage: 135 MB % 26.09/4.45 % (4043616)Instructions burned: 277 (million) % 26.09/4.45 % (4043609)------------------------------ % 26.09/4.45 % (4043609)------------------------------ % 26.09/4.45 % (4043622)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=170340249:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2973 on theBenchmark for (2973ds/1054Mi) % 26.09/4.45 % (4043622)Refutation not found, incomplete strategy % 26.09/4.45 % (4043622)------------------------------ % 26.09/4.45 % (4043622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.09/4.45 % (4043622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.09/4.45 % (4043622)CaDiCaL version: 2.1.3 % 26.09/4.45 % (4043622)Termination reason: Refutation not found, incomplete strategy % 26.09/4.45 % (4043622)Time elapsed: 0.006 s % 26.09/4.45 % (4043622)Peak memory usage: 87 MB % 26.09/4.45 % (4043622)Instructions burned: 10 (million) % 26.09/4.45 % (4043625)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1974698058:i=107:rtra=on_2973 on theBenchmark for (2973ds/107Mi) % 26.09/4.45 % (4043626)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1934210975:s2a=on:i=450:doe=on:nm=32:rtra=on_2972 on theBenchmark for (2972ds/450Mi) % 27.20/4.73 % (4043625)Refutation not found, incomplete strategy % 27.20/4.73 % (4043625)------------------------------ % 27.20/4.73 % (4043625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.73 % (4043625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.73 % (4043625)CaDiCaL version: 2.1.3 % 27.20/4.73 % (4043625)Termination reason: Refutation not found, incomplete strategy % 27.20/4.73 % (4043625)Time elapsed: 0.059 s % 27.20/4.73 % (4043625)Peak memory usage: 114 MB % 27.20/4.73 % (4043625)Instructions burned: 68 (million) % 27.20/4.73 % (4043627)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 % 27.20/4.73 % (4043627)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2301596373:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi) % 27.20/4.73 % (4043626)Instruction limit reached! % 27.20/4.73 % (4043626)------------------------------ % 27.20/4.73 % (4043626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.73 % (4043626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.73 % (4043626)CaDiCaL version: 2.1.3 % 27.20/4.73 % (4043626)Termination reason: Instruction limit % 27.20/4.73 % (4043626)Termination phase: Saturation % 27.20/4.73 % (4043626)Time elapsed: 0.175 s % 27.20/4.73 % (4043626)Peak memory usage: 136 MB % 27.20/4.73 % (4043626)Instructions burned: 452 (million) % 27.20/4.73 % (4043619)Instruction limit reached! % 27.20/4.73 % (4043619)------------------------------ % 27.20/4.73 % (4043619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.73 % (4043619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.73 % (4043619)CaDiCaL version: 2.1.3 % 27.20/4.73 % (4043619)Termination reason: Instruction limit % 27.20/4.73 % (4043619)Termination phase: Saturation % 27.20/4.73 % (4043619)Time elapsed: 0.341 s % 27.20/4.73 % (4043619)Peak memory usage: 93 MB % 27.20/4.73 % (4043619)Instructions burned: 655 (million) % 27.20/4.73 % (4043622)------------------------------ % 27.20/4.73 % (4043622)------------------------------ % 27.20/4.73 % (4043625)------------------------------ % 27.20/4.73 % (4043625)------------------------------ % 27.20/4.73 % (4043633)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1996680556:i=312:kws=inv_frequency:nm=20:rtra=on_2969 on theBenchmark for (2969ds/312Mi) % 27.20/4.73 % (4043632)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2290753679:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi) % 27.20/4.73 % (4043634)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1646554801:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi) % 27.20/4.73 % (4043634)Refutation not found, incomplete strategy % 27.20/4.73 % (4043634)------------------------------ % 27.20/4.73 % (4043634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.73 % (4043634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.73 % (4043634)CaDiCaL version: 2.1.3 % 27.20/4.73 % (4043634)Termination reason: Refutation not found, incomplete strategy % 27.20/4.73 % (4043634)Time elapsed: 0.036 s % 27.20/4.73 % (4043634)Peak memory usage: 90 MB % 27.20/4.73 % (4043634)Instructions burned: 68 (million) % 27.20/4.73 % (4043633)Instruction limit reached! % 27.20/4.73 % (4043633)------------------------------ % 27.20/4.73 % (4043633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.20/4.73 % (4043633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.20/4.73 % (4043633)CaDiCaL version: 2.1.3 % 27.20/4.73 % (4043633)Termination reason: Instruction limit % 27.20/4.73 % (4043633)Termination phase: Saturation % 27.20/4.73 % (4043633)Time elapsed: 0.115 s % 27.20/4.73 % (4043633)Peak memory usage: 119 MB % 27.20/4.73 % (4043633)Instructions burned: 313 (million) % 27.20/4.73 % (4043636)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=4284094922:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 27.20/4.73 % (4043632)Instruction limit reached! % 27.20/4.73 % (4043632)------------------------------ % 27.20/4.73 % (4043632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.61/5.36 % (4043632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.61/5.36 % (4043632)CaDiCaL version: 2.1.3 % 32.61/5.36 % (4043632)Termination reason: Instruction limit % 32.61/5.36 % (4043632)Termination phase: Saturation % 32.61/5.36 % (4043632)Time elapsed: 0.096 s % 32.61/5.36 % (4043632)Peak memory usage: 117 MB % 32.61/5.36 % (4043632)Instructions burned: 131 (million) % 32.61/5.36 % (4043618)Instruction limit reached! % 32.61/5.36 % (4043618)------------------------------ % 32.61/5.36 % (4043618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.61/5.36 % (4043618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.61/5.36 % (4043618)CaDiCaL version: 2.1.3 % 32.61/5.36 % (4043618)Termination reason: Instruction limit % 32.61/5.36 % (4043618)Termination phase: Saturation % 32.61/5.36 % (4043618)Time elapsed: 0.590 s % 32.61/5.36 % (4043618)Peak memory usage: 97 MB % 32.61/5.36 % (4043618)Instructions burned: 1054 (million) % 32.61/5.36 % (4043639)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1703670334:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 32.61/5.36 % (4043639)Refutation not found, incomplete strategy % 32.61/5.36 % (4043639)------------------------------ % 32.61/5.36 % (4043639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.61/5.36 % (4043639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.61/5.36 % (4043639)CaDiCaL version: 2.1.3 % 32.61/5.36 % (4043639)Termination reason: Refutation not found, incomplete strategy % 32.61/5.36 % (4043639)Time elapsed: 0.027 s % 32.61/5.36 % (4043639)Peak memory usage: 90 MB % 32.61/5.36 % (4043639)Instructions burned: 87 (million) % 32.61/5.36 % (4043641)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=828631967:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 32.61/5.36 % (4043642)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=520746792:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2967 on theBenchmark for (2967ds/646Mi) % 32.61/5.36 % (4043634)------------------------------ % 32.61/5.36 % (4043634)------------------------------ % 32.61/5.36 % (4043639)------------------------------ % 32.61/5.36 % (4043639)------------------------------ % 32.61/5.36 % (4043646)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=3317634648:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/784Mi) % 32.61/5.36 % (4043647)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=3360779773:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2965 on theBenchmark for (2965ds/1131Mi) % 32.61/5.36 % (4043627)Instruction limit reached! % 32.61/5.36 % (4043627)------------------------------ % 32.61/5.36 % (4043627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.61/5.36 % (4043627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.61/5.36 % (4043627)CaDiCaL version: 2.1.3 % 32.61/5.36 % (4043627)Termination reason: Instruction limit % 32.61/5.36 % (4043627)Termination phase: Saturation % 32.61/5.36 % (4043627)Time elapsed: 0.689 s % 32.61/5.36 % (4043627)Peak memory usage: 126 MB % 32.61/5.36 % (4043627)Instructions burned: 1090 (million) % 32.61/5.36 % (4043636)Instruction limit reached! % 32.61/5.36 % (4043636)------------------------------ % 32.61/5.36 % (4043636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.61/5.36 % (4043636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.61/5.36 % (4043636)CaDiCaL version: 2.1.3 % 32.61/5.36 % (4043636)Termination reason: Instruction limit % 32.61/5.36 % (4043636)Termination phase: Saturation % 32.61/5.36 % (4043636)Time elapsed: 0.483 s % 32.61/5.36 % (4043636)Peak memory usage: 96 MB % 32.61/5.36 % (4043636)Instructions burned: 836 (million) % 32.61/5.36 % (4043650)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=891705979:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/246Mi) % 32.61/5.36 % (4043650)Refutation not found, incomplete strategy % 32.61/5.36 % (4043650)------------------------------ % 32.61/5.36 % (4043650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.61/5.36 % (4043650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043650)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043650)Termination reason: Refutation not found, incomplete strategy % 40.17/6.37 % (4043650)Time elapsed: 0.033 s % 40.17/6.37 % (4043650)Peak memory usage: 111 MB % 40.17/6.37 % (4043650)Instructions burned: 20 (million) % 40.17/6.37 % (4043651)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=8890172:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/775Mi) % 40.17/6.37 % (4043641)Instruction limit reached! % 40.17/6.37 % (4043641)------------------------------ % 40.17/6.37 % (4043641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.17/6.37 % (4043641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043641)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043641)Termination reason: Instruction limit % 40.17/6.37 % (4043641)Termination phase: Saturation % 40.17/6.37 % (4043641)Time elapsed: 0.483 s % 40.17/6.37 % (4043641)Peak memory usage: 123 MB % 40.17/6.37 % (4043641)Instructions burned: 776 (million) % 40.17/6.37 % (4043651)Refutation not found, incomplete strategy % 40.17/6.37 % (4043651)------------------------------ % 40.17/6.37 % (4043651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.17/6.37 % (4043651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043651)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043651)Termination reason: Refutation not found, incomplete strategy % 40.17/6.37 % (4043651)Time elapsed: 0.009 s % 40.17/6.37 % (4043651)Peak memory usage: 88 MB % 40.17/6.37 % (4043651)Instructions burned: 17 (million) % 40.17/6.37 % (4043642)Instruction limit reached! % 40.17/6.37 % (4043642)------------------------------ % 40.17/6.37 % (4043642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.17/6.37 % (4043642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043642)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043642)Termination reason: Instruction limit % 40.17/6.37 % (4043642)Termination phase: Saturation % 40.17/6.37 % (4043642)Time elapsed: 0.447 s % 40.17/6.37 % (4043642)Peak memory usage: 140 MB % 40.17/6.37 % (4043642)Instructions burned: 646 (million) % 40.17/6.37 % (4043647)Instruction limit reached! % 40.17/6.37 % (4043647)------------------------------ % 40.17/6.37 % (4043647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.17/6.37 % (4043647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043647)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043647)Termination reason: Instruction limit % 40.17/6.37 % (4043647)Termination phase: Saturation % 40.17/6.37 % (4043647)Time elapsed: 0.399 s % 40.17/6.37 % (4043647)Peak memory usage: 135 MB % 40.17/6.37 % (4043647)Instructions burned: 1132 (million) % 40.17/6.37 % (4043654)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3413222113:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 40.17/6.37 % (4043655)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1827796456:i=102:nm=16:rtra=on_2961 on theBenchmark for (2961ds/102Mi) % 40.17/6.37 % (4043650)------------------------------ % 40.17/6.37 % (4043650)------------------------------ % 40.17/6.37 % (4043655)Instruction limit reached! % 40.17/6.37 % (4043655)------------------------------ % 40.17/6.37 % (4043655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.17/6.37 % (4043655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043655)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043655)Termination reason: Instruction limit % 40.17/6.37 % (4043655)Termination phase: Saturation % 40.17/6.37 % (4043655)Time elapsed: 0.059 s % 40.17/6.37 % (4043655)Peak memory usage: 90 MB % 40.17/6.37 % (4043655)Instructions burned: 103 (million) % 40.17/6.37 % (4043656)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=157039846:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2960 on theBenchmark for (2960ds/1094Mi) % 40.17/6.37 % (4043646)Instruction limit reached! % 40.17/6.37 % (4043646)------------------------------ % 40.17/6.37 % (4043646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.17/6.37 % (4043646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.17/6.37 % (4043646)CaDiCaL version: 2.1.3 % 40.17/6.37 % (4043646)Termination reason: Instruction limit % 40.17/6.37 % (4043646)Termination phase: Saturation % 54.30/8.34 % (4043646)Time elapsed: 0.496 s % 54.30/8.34 % (4043646)Peak memory usage: 122 MB % 54.30/8.34 % (4043646)Instructions burned: 785 (million) % 54.30/8.34 % (4043651)------------------------------ % 54.30/8.34 % (4043651)------------------------------ % 54.30/8.34 % (4043654)Instruction limit reached! % 54.30/8.34 % (4043654)------------------------------ % 54.30/8.34 % (4043654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.30/8.34 % (4043654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.30/8.34 % (4043654)CaDiCaL version: 2.1.3 % 54.30/8.34 % (4043654)Termination reason: Instruction limit % 54.30/8.34 % (4043654)Termination phase: Saturation % 54.30/8.34 % (4043654)Time elapsed: 0.176 s % 54.30/8.34 % (4043654)Peak memory usage: 92 MB % 54.30/8.34 % (4043654)Instructions burned: 274 (million) % 54.30/8.34 % (4043659)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=387096550:i=6400:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/6400Mi) % 54.30/8.34 % (4043660)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=623996840:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2959 on theBenchmark for (2959ds/868Mi) % 54.30/8.34 % (4043662)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=3556363412:i=1846:canc=cautious:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/1846Mi) % 54.30/8.34 % (4043663)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3944943440:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2959 on theBenchmark for (2959ds/36816Mi) % 54.30/8.34 % (4043662)Refutation not found, incomplete strategy % 54.30/8.34 % (4043662)------------------------------ % 54.30/8.34 % (4043662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.30/8.34 % (4043662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.30/8.34 % (4043662)CaDiCaL version: 2.1.3 % 54.30/8.34 % (4043662)Termination reason: Refutation not found, incomplete strategy % 54.30/8.34 % (4043662)Time elapsed: 0.034 s % 54.30/8.34 % (4043662)Peak memory usage: 90 MB % 54.30/8.34 % (4043662)Instructions burned: 63 (million) % 54.30/8.34 % (4043664)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3182241641:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 54.30/8.34 % (4043656)Instruction limit reached! % 54.30/8.34 % (4043656)------------------------------ % 54.30/8.34 % (4043656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.30/8.34 % (4043656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.30/8.34 % (4043656)CaDiCaL version: 2.1.3 % 54.30/8.34 % (4043656)Termination reason: Instruction limit % 54.30/8.34 % (4043656)Termination phase: Saturation % 54.30/8.34 % (4043656)Time elapsed: 0.351 s % 54.30/8.34 % (4043656)Peak memory usage: 100 MB % 54.30/8.34 % (4043656)Instructions burned: 1096 (million) % 54.30/8.34 % (4043664)Instruction limit reached! % 54.30/8.34 % (4043664)------------------------------ % 54.30/8.34 % (4043664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.30/8.34 % (4043664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.30/8.34 % (4043664)CaDiCaL version: 2.1.3 % 54.30/8.34 % (4043664)Termination reason: Instruction limit % 54.30/8.34 % (4043664)Termination phase: Saturation % 54.30/8.34 % (4043664)Time elapsed: 0.176 s % 54.30/8.34 % (4043664)Peak memory usage: 92 MB % 54.30/8.34 % (4043664)Instructions burned: 274 (million) % 54.30/8.34 % (4043662)------------------------------ % 54.30/8.34 % (4043662)------------------------------ % 54.30/8.34 % (4043670)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=443096169:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/863Mi) % 54.30/8.34 % (4043671)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2493581737:i=5811:kws=precedence:nm=0:rtra=on_2955 on theBenchmark for (2955ds/5811Mi) % 54.30/8.34 % (4043672)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=3742582956:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2955 on theBenchmark for (2955ds/2216Mi) % 54.30/8.34 % (4043660)Instruction limit reached! % 54.30/8.34 % (4043660)------------------------------ % 56.15/8.76 % (4043660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.15/8.76 % (4043660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.15/8.76 % (4043660)CaDiCaL version: 2.1.3 % 56.15/8.76 % (4043660)Termination reason: Instruction limit % 56.15/8.76 % (4043660)Termination phase: Saturation % 56.15/8.76 % (4043660)Time elapsed: 0.512 s % 56.15/8.76 % (4043660)Peak memory usage: 122 MB % 56.15/8.76 % (4043660)Instructions burned: 869 (million) % 56.15/8.76 % (4043670)Instruction limit reached! % 56.15/8.76 % (4043670)------------------------------ % 56.15/8.76 % (4043670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.15/8.76 % (4043670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.15/8.76 % (4043670)CaDiCaL version: 2.1.3 % 56.15/8.76 % (4043670)Termination reason: Instruction limit % 56.15/8.76 % (4043670)Termination phase: Saturation % 56.15/8.76 % (4043670)Time elapsed: 0.276 s % 56.15/8.76 % (4043670)Peak memory usage: 122 MB % 56.15/8.76 % (4043670)Instructions burned: 866 (million) % 56.15/8.76 % (4043676)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1733233480:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/801Mi) % 56.15/8.76 % (4043677)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2357622095:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2952 on theBenchmark for (2952ds/1026Mi) % 56.15/8.76 % (4043677)Refutation not found, incomplete strategy % 56.15/8.76 % (4043677)------------------------------ % 56.15/8.76 % (4043677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.15/8.76 % (4043677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.15/8.76 % (4043677)CaDiCaL version: 2.1.3 % 56.15/8.76 % (4043677)Termination reason: Refutation not found, incomplete strategy % 56.15/8.76 % (4043677)Time elapsed: 0.003 s % 56.15/8.76 % (4043677)Peak memory usage: 87 MB % 56.15/8.76 % (4043677)Instructions burned: 10 (million) % 56.15/8.76 % (4043677)------------------------------ % 56.15/8.76 % (4043677)------------------------------ % 56.15/8.76 % (4043680)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1944753263:i=3509:rtra=on_2949 on theBenchmark for (2949ds/3509Mi) % 56.15/8.76 % (4043615)Instruction limit reached! % 56.15/8.76 % (4043615)------------------------------ % 56.15/8.76 % (4043615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.15/8.76 % (4043615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.15/8.76 % (4043615)CaDiCaL version: 2.1.3 % 56.15/8.76 % (4043615)Termination reason: Instruction limit % 56.15/8.76 % (4043615)Termination phase: Saturation % 56.15/8.76 % (4043615)Time elapsed: 2.569 s % 56.15/8.76 % (4043615)Peak memory usage: 120 MB % 56.15/8.76 % (4043615)Instructions burned: 4428 (million) % 56.15/8.76 % (4043676)Instruction limit reached! % 56.15/8.76 % (4043676)------------------------------ % 56.15/8.76 % (4043676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.15/8.76 % (4043676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.15/8.76 % (4043676)CaDiCaL version: 2.1.3 % 56.15/8.76 % (4043676)Termination reason: Instruction limit % 56.15/8.76 % (4043676)Termination phase: Saturation % 56.15/8.76 % (4043676)Time elapsed: 0.423 s % 56.15/8.76 % (4043676)Peak memory usage: 94 MB % 56.15/8.76 % (4043676)Instructions burned: 801 (million) % 56.15/8.76 % (4043682)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4264326341:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2947 on theBenchmark for (2947ds/2127Mi) % 56.15/8.76 % (4043682)Refutation not found, incomplete strategy % 56.15/8.76 % (4043682)------------------------------ % 56.15/8.76 % (4043682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.15/8.76 % (4043682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.15/8.76 % (4043682)CaDiCaL version: 2.1.3 % 56.15/8.76 % (4043682)Termination reason: Refutation not found, incomplete strategy % 56.15/8.76 % (4043682)Time elapsed: 0.008 s % 56.15/8.76 % (4043682)Peak memory usage: 88 MB % 56.15/8.76 % (4043682)Instructions burned: 15 (million) % 56.15/8.76 % (4043683)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1534245009:i=1959:rtra=on:fsd=on:proc=on_2947 on theBenchmark for (2947ds/1959Mi) % 56.15/8.76 % (4043682)------------------------------ % 56.15/8.76 % (4043682)------------------------------ % 56.15/8.76 % (4043686)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=474592556:s2a=on:i=3553:nm=0:rtra=on_2944 on theBenchmark for (2944ds/3553Mi) % 79.39/11.94 % (4043672)Instruction limit reached! % 79.39/11.94 % (4043672)------------------------------ % 79.39/11.94 % (4043672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.39/11.94 % (4043672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.39/11.94 % (4043672)CaDiCaL version: 2.1.3 % 79.39/11.94 % (4043672)Termination reason: Instruction limit % 79.39/11.94 % (4043672)Termination phase: Saturation % 79.39/11.94 % (4043672)Time elapsed: 1.289 s % 79.39/11.94 % (4043672)Peak memory usage: 136 MB % 79.39/11.94 % (4043672)Instructions burned: 2218 (million) % 79.39/11.94 % (4043688)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=371974258:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2940 on theBenchmark for (2940ds/3201Mi) % 79.39/11.94 % (4043680)Instruction limit reached! % 79.39/11.94 % (4043680)------------------------------ % 79.39/11.94 % (4043680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.39/11.94 % (4043680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.39/11.94 % (4043680)CaDiCaL version: 2.1.3 % 79.39/11.94 % (4043680)Termination reason: Instruction limit % 79.39/11.94 % (4043680)Termination phase: Saturation % 79.39/11.94 % (4043680)Time elapsed: 1.135 s % 79.39/11.94 % (4043680)Peak memory usage: 116 MB % 79.39/11.94 % (4043680)Instructions burned: 3511 (million) % 79.39/11.94 % (4043690)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=1568945616:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2937 on theBenchmark for (2937ds/4093Mi) % 79.39/11.94 % (4043683)Instruction limit reached! % 79.39/11.94 % (4043683)------------------------------ % 79.39/11.94 % (4043683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.39/11.94 % (4043683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.39/11.94 % (4043683)CaDiCaL version: 2.1.3 % 79.39/11.94 % (4043683)Termination reason: Instruction limit % 79.39/11.94 % (4043683)Termination phase: Saturation % 79.39/11.94 % (4043683)Time elapsed: 1.221 s % 79.39/11.94 % (4043683)Peak memory usage: 138 MB % 79.39/11.94 % (4043683)Instructions burned: 1959 (million) % 79.39/11.94 % (4043692)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=2441830417:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2933 on theBenchmark for (2933ds/21173Mi) % 79.39/11.94 % (4043692)Refutation not found, incomplete strategy % 79.39/11.94 % (4043692)------------------------------ % 79.39/11.94 % (4043692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.39/11.94 % (4043692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.39/11.94 % (4043692)CaDiCaL version: 2.1.3 % 79.39/11.94 % (4043692)Termination reason: Refutation not found, incomplete strategy % 79.39/11.94 % (4043692)Time elapsed: 0.030 s % 79.39/11.94 % (4043692)Peak memory usage: 112 MB % 79.39/11.94 % (4043692)Instructions burned: 13 (million) % 79.39/11.94 % (4043692)------------------------------ % 79.39/11.94 % (4043692)------------------------------ % 79.39/11.94 % (4043694)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=432977727:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2929 on theBenchmark for (2929ds/10544Mi) % 79.39/11.94 % (4043688)Instruction limit reached! % 79.39/11.94 % (4043688)------------------------------ % 79.39/11.94 % (4043688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.39/11.94 % (4043688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.39/11.94 % (4043688)CaDiCaL version: 2.1.3 % 79.39/11.94 % (4043688)Termination reason: Instruction limit % 79.39/11.94 % (4043688)Termination phase: Saturation % 79.39/11.94 % (4043688)Time elapsed: 1.480 s % 79.39/11.94 % (4043688)Peak memory usage: 104 MB % 79.39/11.94 % (4043688)Instructions burned: 3201 (million) % 79.39/11.94 % (4043696)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1004632490:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2924 on theBenchmark for (2924ds/1262Mi) % 79.39/11.94 % (4043690)Instruction limit reached! % 79.39/11.94 % (4043690)------------------------------ % 79.39/11.94 % (4043690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.82/14.01 % (4043690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.82/14.01 % (4043690)CaDiCaL version: 2.1.3 % 93.82/14.01 % (4043690)Termination reason: Instruction limit % 93.82/14.01 % (4043690)Termination phase: Saturation % 93.82/14.01 % (4043690)Time elapsed: 1.350 s % 93.82/14.01 % (4043690)Peak memory usage: 164 MB % 93.82/14.01 % (4043690)Instructions burned: 4095 (million) % 93.82/14.01 % (4043698)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4039415341:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2923 on theBenchmark for (2923ds/775Mi) % 93.82/14.01 % (4043698)Refutation not found, incomplete strategy % 93.82/14.01 % (4043698)------------------------------ % 93.82/14.01 % (4043698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.82/14.01 % (4043698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.82/14.01 % (4043698)CaDiCaL version: 2.1.3 % 93.82/14.01 % (4043698)Termination reason: Refutation not found, incomplete strategy % 93.82/14.01 % (4043698)Time elapsed: 0.005 s % 93.82/14.01 % (4043698)Peak memory usage: 88 MB % 93.82/14.01 % (4043698)Instructions burned: 17 (million) % 93.82/14.01 % (4043659)Instruction limit reached! % 93.82/14.01 % (4043659)------------------------------ % 93.82/14.01 % (4043659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.82/14.01 % (4043659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.82/14.01 % (4043659)CaDiCaL version: 2.1.3 % 93.82/14.01 % (4043659)Termination reason: Instruction limit % 93.82/14.01 % (4043659)Termination phase: Saturation % 93.82/14.01 % (4043659)Time elapsed: 3.620 s % 93.82/14.01 % (4043659)Peak memory usage: 130 MB % 93.82/14.01 % (4043659)Instructions burned: 6400 (million) % 93.82/14.01 % (4043671)Instruction limit reached! % 93.82/14.01 % (4043671)------------------------------ % 93.82/14.01 % (4043671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.82/14.01 % (4043671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.82/14.01 % (4043671)CaDiCaL version: 2.1.3 % 93.82/14.01 % (4043671)Termination reason: Instruction limit % 93.82/14.01 % (4043671)Termination phase: Saturation % 93.82/14.01 % (4043671)Time elapsed: 3.243 s % 93.82/14.01 % (4043671)Peak memory usage: 139 MB % 93.82/14.01 % (4043671)Instructions burned: 5813 (million) % 93.82/14.01 % (4043686)Instruction limit reached! % 93.82/14.01 % (4043686)------------------------------ % 93.82/14.01 % (4043686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.82/14.01 % (4043686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.82/14.01 % (4043686)CaDiCaL version: 2.1.3 % 93.82/14.01 % (4043686)Termination reason: Instruction limit % 93.82/14.01 % (4043686)Termination phase: Saturation % 93.82/14.01 % (4043686)Time elapsed: 2.195 s % 93.82/14.01 % (4043686)Peak memory usage: 116 MB % 93.82/14.01 % (4043686)Instructions burned: 3554 (million) % 93.82/14.01 % (4043700)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4055615781:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2922 on theBenchmark for (2922ds/270Mi) % 93.82/14.01 % (4043698)------------------------------ % 93.82/14.01 % (4043698)------------------------------ % 93.82/14.01 % (4043701)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=163378296:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2921 on theBenchmark for (2921ds/17165Mi) % 93.82/14.01 % (4043704)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=164004782:st=2:i=12633:rtra=on:ss=axioms_2920 on theBenchmark for (2920ds/12633Mi) % 93.82/14.01 % (4043704)Refutation not found, incomplete strategy % 93.82/14.01 % (4043704)------------------------------ % 93.82/14.01 % (4043704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.82/14.01 % (4043704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.82/14.01 % (4043704)CaDiCaL version: 2.1.3 % 93.82/14.01 % (4043704)Termination reason: Refutation not found, incomplete strategy % 93.82/14.01 % (4043704)Time elapsed: 0.004 s % 93.82/14.01 % (4043704)Peak memory usage: 88 MB % 93.82/14.01 % (4043704)Instructions burned: 15 (million) % 93.82/14.01 % (4043702)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2468347867:s2a=on:i=13094:s2at=-1:rtra=on_2920 on theBenchmark for (2920ds/13094Mi) % 93.82/14.01 % (4043700)Instruction limit reached! % 93.82/14.01 % (4043700)------------------------------ % 121.87/17.84 % (4043700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.87/17.84 % (4043700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.87/17.84 % (4043700)CaDiCaL version: 2.1.3 % 121.87/17.84 % (4043700)Termination reason: Instruction limit % 121.87/17.84 % (4043700)Termination phase: Saturation % 121.87/17.84 % (4043700)Time elapsed: 0.179 s % 121.87/17.84 % (4043700)Peak memory usage: 92 MB % 121.87/17.84 % (4043700)Instructions burned: 270 (million) % 121.87/17.84 % (4043704)------------------------------ % 121.87/17.84 % (4043704)------------------------------ % 121.87/17.84 % (4043708)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=69240894:i=1783:rtra=on:gtg=position_2918 on theBenchmark for (2918ds/1783Mi) % 121.87/17.84 % (4043709)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=1094895970:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2918 on theBenchmark for (2918ds/5451Mi) % 121.87/17.84 % (4043696)Instruction limit reached! % 121.87/17.84 % (4043696)------------------------------ % 121.87/17.84 % (4043696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.87/17.84 % (4043696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.87/17.84 % (4043696)CaDiCaL version: 2.1.3 % 121.87/17.84 % (4043696)Termination reason: Instruction limit % 121.87/17.84 % (4043696)Termination phase: Saturation % 121.87/17.84 % (4043696)Time elapsed: 0.735 s % 121.87/17.84 % (4043696)Peak memory usage: 128 MB % 121.87/17.84 % (4043696)Instructions burned: 1263 (million) % 121.87/17.84 % (4043712)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=3649994707:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2916 on theBenchmark for (2916ds/4975Mi) % 121.87/17.84 % (4043708)Instruction limit reached! % 121.87/17.84 % (4043708)------------------------------ % 121.87/17.84 % (4043708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.87/17.84 % (4043708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.87/17.84 % (4043708)CaDiCaL version: 2.1.3 % 121.87/17.84 % (4043708)Termination reason: Instruction limit % 121.87/17.84 % (4043708)Termination phase: Saturation % 121.87/17.84 % (4043708)Time elapsed: 1.076 s % 121.87/17.84 % (4043708)Peak memory usage: 127 MB % 121.87/17.84 % (4043708)Instructions burned: 1783 (million) % 121.87/17.84 % (4043714)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=1031141042:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2906 on theBenchmark for (2906ds/2076Mi) % 121.87/17.84 % (4043709)Instruction limit reached! % 121.87/17.84 % (4043709)------------------------------ % 121.87/17.84 % (4043709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.87/17.84 % (4043709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.87/17.84 % (4043709)CaDiCaL version: 2.1.3 % 121.87/17.84 % (4043709)Termination reason: Instruction limit % 121.87/17.84 % (4043709)Termination phase: Saturation % 121.87/17.84 % (4043709)Time elapsed: 1.714 s % 121.87/17.84 % (4043709)Peak memory usage: 142 MB % 121.87/17.84 % (4043709)Instructions burned: 5452 (million) % 121.87/17.84 % (4043716)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3361555852:i=5145:rtra=on_2900 on theBenchmark for (2900ds/5145Mi) % 121.87/17.84 % (4043714)Instruction limit reached! % 121.87/17.84 % (4043714)------------------------------ % 121.87/17.84 % (4043714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.87/17.84 % (4043714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.87/17.84 % (4043714)CaDiCaL version: 2.1.3 % 121.87/17.84 % (4043714)Termination reason: Instruction limit % 121.87/17.84 % (4043714)Termination phase: Saturation % 121.87/17.84 % (4043714)Time elapsed: 1.211 s % 121.87/17.84 % (4043714)Peak memory usage: 136 MB % 121.87/17.84 % (4043714)Instructions burned: 2077 (million) % 121.87/17.84 % (4043718)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4008763407:i=3509:rtra=on_2893 on theBenchmark for (2893ds/3509Mi) % 121.87/17.84 % (4043712)Instruction limit reached! % 121.87/17.84 % (4043712)------------------------------ % 121.87/17.84 % (4043712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.87/17.84 % (4043712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.87/17.84 % (4043712)CaDiCaL version: 2.1.3 % 214.54/31.02 % (4043712)Termination reason: Instruction limit % 214.54/31.02 % (4043712)Termination phase: Saturation % 214.54/31.02 % (4043712)Time elapsed: 2.763 s % 214.54/31.02 % (4043712)Peak memory usage: 146 MB % 214.54/31.02 % (4043712)Instructions burned: 4976 (million) % 214.54/31.02 % (4043720)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4257719865:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2887 on theBenchmark for (2887ds/13800Mi) % 214.54/31.02 % (4043720)Refutation not found, incomplete strategy % 214.54/31.02 % (4043720)------------------------------ % 214.54/31.02 % (4043720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.54/31.02 % (4043720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.54/31.02 % (4043720)CaDiCaL version: 2.1.3 % 214.54/31.02 % (4043720)Termination reason: Refutation not found, incomplete strategy % 214.54/31.02 % (4043720)Time elapsed: 0.008 s % 214.54/31.02 % (4043720)Peak memory usage: 88 MB % 214.54/31.02 % (4043720)Instructions burned: 15 (million) % 214.54/31.02 % (4043716)Instruction limit reached! % 214.54/31.02 % (4043716)------------------------------ % 214.54/31.02 % (4043716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.54/31.02 % (4043716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.54/31.02 % (4043716)CaDiCaL version: 2.1.3 % 214.54/31.02 % (4043716)Termination reason: Instruction limit % 214.54/31.02 % (4043716)Termination phase: Saturation % 214.54/31.02 % (4043716)Time elapsed: 1.463 s % 214.54/31.02 % (4043716)Peak memory usage: 129 MB % 214.54/31.02 % (4043716)Instructions burned: 5145 (million) % 214.54/31.02 % (4043722)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3114029877:i=1412:rtra=on:fsd=on:proc=on_2884 on theBenchmark for (2884ds/1412Mi) % 214.54/31.02 % (4043720)------------------------------ % 214.54/31.02 % (4043720)------------------------------ % 214.54/31.02 % (4043724)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 % 214.54/31.02 % (4043724)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2921882975:i=11747:aac=none:nm=0:rtra=on:rawr=on_2883 on theBenchmark for (2883ds/11747Mi) % 214.54/31.02 % (4043722)Instruction limit reached! % 214.54/31.02 % (4043722)------------------------------ % 214.54/31.02 % (4043722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.54/31.02 % (4043722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.54/31.02 % (4043722)CaDiCaL version: 2.1.3 % 214.54/31.02 % (4043722)Termination reason: Instruction limit % 214.54/31.02 % (4043722)Termination phase: Saturation % 214.54/31.02 % (4043722)Time elapsed: 0.486 s % 214.54/31.02 % (4043722)Peak memory usage: 134 MB % 214.54/31.02 % (4043722)Instructions burned: 1412 (million) % 214.54/31.02 % (4043726)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2995267364:s2a=on:i=3553:nm=0:rtra=on_2879 on theBenchmark for (2879ds/3553Mi) % 214.54/31.02 % (4043718)Instruction limit reached! % 214.54/31.02 % (4043718)------------------------------ % 214.54/31.02 % (4043718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.54/31.02 % (4043718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.54/31.02 % (4043718)CaDiCaL version: 2.1.3 % 214.54/31.02 % (4043718)Termination reason: Instruction limit % 214.54/31.02 % (4043718)Termination phase: Saturation % 214.54/31.02 % (4043718)Time elapsed: 2.108 s % 214.54/31.02 % (4043718)Peak memory usage: 117 MB % 214.54/31.02 % (4043718)Instructions burned: 3509 (million) % 214.54/31.02 % (4043728)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1361871724:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2871 on theBenchmark for (2871ds/3201Mi) % 214.54/31.02 % (4043694)Instruction limit reached! % 214.54/31.02 % (4043694)------------------------------ % 214.54/31.02 % (4043694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.54/31.02 % (4043694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.54/31.02 % (4043694)CaDiCaL version: 2.1.3 % 214.54/31.02 % (4043694)Termination reason: Instruction limit % 214.54/31.02 % (4043694)Termination phase: Saturation % 214.54/31.02 % (4043694)Time elapsed: 6.034 s % 214.54/31.02 % (4043694)Peak memory usage: 290 MB % 214.54/31.02 % (4043694)Instructions burned: 10544 (million) % 214.54/31.02 % (4043732)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=3943991955:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2867 on theBenchmark for (2867ds/4081Mi) % 238.00/34.26 % (4043726)Instruction limit reached! % 238.00/34.26 % (4043726)------------------------------ % 238.00/34.26 % (4043726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.00/34.26 % (4043726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.00/34.26 % (4043726)CaDiCaL version: 2.1.3 % 238.00/34.26 % (4043726)Termination reason: Instruction limit % 238.00/34.26 % (4043726)Termination phase: Saturation % 238.00/34.26 % (4043726)Time elapsed: 1.174 s % 238.00/34.26 % (4043726)Peak memory usage: 116 MB % 238.00/34.26 % (4043726)Instructions burned: 3553 (million) % 238.00/34.26 % (4043755)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=1164987766:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2866 on theBenchmark for (2866ds/20260Mi) % 238.00/34.26 % (4043755)Refutation not found, incomplete strategy % 238.00/34.26 % (4043755)------------------------------ % 238.00/34.26 % (4043755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.00/34.26 % (4043755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.00/34.26 % (4043755)CaDiCaL version: 2.1.3 % 238.00/34.26 % (4043755)Termination reason: Refutation not found, incomplete strategy % 238.00/34.26 % (4043755)Time elapsed: 0.018 s % 238.00/34.26 % (4043755)Peak memory usage: 113 MB % 238.00/34.26 % (4043755)Instructions burned: 13 (million) % 238.00/34.26 % (4043755)------------------------------ % 238.00/34.26 % (4043755)------------------------------ % 238.00/34.26 % (4043856)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1472921525:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2863 on theBenchmark for (2863ds/58627Mi) % 238.00/34.26 % (4043702)Instruction limit reached! % 238.00/34.26 % (4043702)------------------------------ % 238.00/34.26 % (4043702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.00/34.26 % (4043702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.00/34.26 % (4043702)CaDiCaL version: 2.1.3 % 238.00/34.26 % (4043702)Termination reason: Instruction limit % 238.00/34.26 % (4043702)Termination phase: Saturation % 238.00/34.26 % (4043702)Time elapsed: 5.882 s % 238.00/34.26 % (4043702)Peak memory usage: 136 MB % 238.00/34.26 % (4043702)Instructions burned: 13096 (million) % 238.00/34.26 % (4043929)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1757927766:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2860 on theBenchmark for (2860ds/6258Mi) % 238.00/34.26 % (4043728)Instruction limit reached! % 238.00/34.26 % (4043728)------------------------------ % 238.00/34.26 % (4043728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.00/34.26 % (4043728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.00/34.26 % (4043728)CaDiCaL version: 2.1.3 % 238.00/34.26 % (4043728)Termination reason: Instruction limit % 238.00/34.26 % (4043728)Termination phase: Saturation % 238.00/34.26 % (4043728)Time elapsed: 1.500 s % 238.00/34.26 % (4043728)Peak memory usage: 104 MB % 238.00/34.26 % (4043728)Instructions burned: 3202 (million) % 238.00/34.26 % (4044081)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=258593678:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2854 on theBenchmark for (2854ds/34001Mi) % 238.00/34.26 % (4043732)Instruction limit reached! % 238.00/34.26 % (4043732)------------------------------ % 238.00/34.26 % (4043732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.00/34.26 % (4043732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.00/34.26 % (4043732)CaDiCaL version: 2.1.3 % 238.00/34.26 % (4043732)Termination reason: Instruction limit % 238.00/34.26 % (4043732)Termination phase: Saturation % 238.00/34.26 % (4043732)Time elapsed: 2.439 s % 238.00/34.26 % (4043732)Peak memory usage: 162 MB % 238.00/34.26 % (4043732)Instructions burned: 4082 (million) % 238.00/34.26 % (4044083)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=3075144264:s2a=on:i=71622:s2at=-1:rtra=on_2841 on theBenchmark for (2841ds/71622Mi) % 238.00/34.26 % (4043929)Instruction limit reached! % 238.00/34.26 % (4043929)------------------------------ % 238.00/34.26 % (4043929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4043929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.19/40.72 % (4043929)CaDiCaL version: 2.1.3 % 284.19/40.72 % (4043929)Termination reason: Instruction limit % 284.19/40.72 % (4043929)Termination phase: Saturation % 284.19/40.72 % (4043929)Time elapsed: 3.119 s % 284.19/40.72 % (4043929)Peak memory usage: 148 MB % 284.19/40.72 % (4043929)Instructions burned: 6259 (million) % 284.19/40.72 % (4044085)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3831859112:i=24001:kws=precedence:nm=0:rtra=on_2828 on theBenchmark for (2828ds/24001Mi) % 284.19/40.72 % (4043701)Instruction limit reached! % 284.19/40.72 % (4043701)------------------------------ % 284.19/40.72 % (4043701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4043701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.19/40.72 % (4043701)CaDiCaL version: 2.1.3 % 284.19/40.72 % (4043701)Termination reason: Instruction limit % 284.19/40.72 % (4043701)Termination phase: Saturation % 284.19/40.72 % (4043701)Time elapsed: 9.689 s % 284.19/40.72 % (4043701)Peak memory usage: 175 MB % 284.19/40.72 % (4043701)Instructions burned: 17166 (million) % 284.19/40.72 % (4044087)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=150644017:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2823 on theBenchmark for (2823ds/2076Mi) % 284.19/40.72 % (4043724)Instruction limit reached! % 284.19/40.72 % (4043724)------------------------------ % 284.19/40.72 % (4043724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4043724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.19/40.72 % (4043724)CaDiCaL version: 2.1.3 % 284.19/40.72 % (4043724)Termination reason: Instruction limit % 284.19/40.72 % (4043724)Termination phase: Saturation % 284.19/40.72 % (4043724)Time elapsed: 6.387 s % 284.19/40.72 % (4043724)Peak memory usage: 177 MB % 284.19/40.72 % (4043724)Instructions burned: 11747 (million) % 284.19/40.72 % (4044089)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=1977055659:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2817 on theBenchmark for (2817ds/83971Mi) % 284.19/40.72 % (4044087)Instruction limit reached! % 284.19/40.72 % (4044087)------------------------------ % 284.19/40.72 % (4044087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4044087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.19/40.72 % (4044087)CaDiCaL version: 2.1.3 % 284.19/40.72 % (4044087)Termination reason: Instruction limit % 284.19/40.72 % (4044087)Termination phase: Saturation % 284.19/40.72 % (4044087)Time elapsed: 1.204 s % 284.19/40.72 % (4044087)Peak memory usage: 135 MB % 284.19/40.72 % (4044087)Instructions burned: 2078 (million) % 284.19/40.72 % (4044091)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=2972229981:i=83944:rtra=on_2809 on theBenchmark for (2809ds/83944Mi) % 284.19/40.72 % (4043663)Instruction limit reached! % 284.19/40.72 % (4043663)------------------------------ % 284.19/40.72 % (4043663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4043663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.19/40.72 % (4043663)CaDiCaL version: 2.1.3 % 284.19/40.72 % (4043663)Termination reason: Instruction limit % 284.19/40.72 % (4043663)Termination phase: Saturation % 284.19/40.72 % (4043663)Time elapsed: 21.005 s % 284.19/40.72 % (4043663)Peak memory usage: 293 MB % 284.19/40.72 % (4043663)Instructions burned: 36819 (million) % 284.19/40.72 % (4044093)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3762506686:i=9201:rtra=on_2747 on theBenchmark for (2747ds/9201Mi) % 284.19/40.72 % (4044085)Instruction limit reached! % 284.19/40.72 % (4044085)------------------------------ % 284.19/40.72 % (4044085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4044085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.19/40.72 % (4044085)CaDiCaL version: 2.1.3 % 284.19/40.72 % (4044085)Termination reason: Instruction limit % 284.19/40.72 % (4044085)Termination phase: Saturation % 284.19/40.72 % (4044085)Time elapsed: 12.991 s % 284.19/40.72 % (4044085)Peak memory usage: 191 MB % 284.19/40.72 % (4044085)Instructions burned: 24001 (million) % 284.19/40.72 % (4044081)Instruction limit reached! % 284.19/40.72 % (4044081)------------------------------ % 284.19/40.72 % (4044081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.19/40.72 % (4044081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.77/43.02 % (4044081)CaDiCaL version: 2.1.3 % 299.77/43.02 % (4044081)Termination reason: Instruction limit % 299.77/43.02 % (4044081)Termination phase: Saturation % 299.77/43.02 % (4044081)Time elapsed: 15.704 s % 299.77/43.02 % (4044081)Peak memory usage: 502 MB % 299.77/43.02 % (4044081)Instructions burned: 34002 (million) % 299.77/43.02 % (4044349)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 % 299.77/43.02 % (4044349)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=250788433:i=6806:aac=none:nm=0:rtra=on:rawr=on_2696 on theBenchmark for (2696ds/6806Mi) % 299.77/43.02 % (4044360)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3067369442:s2a=on:i=3553:nm=0:rtra=on_2695 on theBenchmark for (2695ds/3553Mi) % 299.77/43.02 % (4044093)Instruction limit reached! % 299.77/43.02 % (4044093)------------------------------ % 299.77/43.02 % (4044093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.77/43.02 % (4044093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.77/43.02 % (4044093)CaDiCaL version: 2.1.3 % 299.77/43.02 % (4044093)Termination reason: Instruction limit % 299.77/43.02 % (4044093)Termination phase: Saturation % 299.77/43.02 % (4044093)Time elapsed: 6.082 s % 299.77/43.02 % (4044093)Peak memory usage: 149 MB % 299.77/43.02 % (4044093)Instructions burned: 9201 (million) % 299.77/43.02 % (4044408)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=1745018870:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2684 on theBenchmark for (2684ds/2064Mi) % 299.77/43.02 % (4043856)Instruction limit reached! % 299.77/43.02 % (4043856)------------------------------ % 299.77/43.02 % (4043856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.77/43.02 % (4043856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.77/43.02 % (4043856)CaDiCaL version: 2.1.3 % 299.77/43.02 % (4043856)Termination reason: Instruction limit % 299.77/43.02 % (4043856)Termination phase: Saturation % 299.77/43.02 % (4043856)Time elapsed: 18.723 s % 299.77/43.02 % (4043856)Peak memory usage: 394 MB % 299.77/43.02 % (4043856)Instructions burned: 58628 (million) % 299.77/43.02 % (4044439)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=2825223938:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2675 on theBenchmark for (2675ds/20260Mi) % 299.77/43.02 % (4044439)Refutation not found, incomplete strategy % 299.77/43.02 % (4044439)------------------------------ % 299.77/43.02 % (4044439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.77/43.02 % (4044439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.77/43.02 % (4044439)CaDiCaL version: 2.1.3 % 299.77/43.02 % (4044439)Termination reason: Refutation not found, incomplete strategy % 299.77/43.02 % (4044439)Time elapsed: 0.025 s % 299.77/43.02 % (4044439)Peak memory usage: 112 MB % 299.77/43.02 % (4044439)Instructions burned: 13 (million) % 299.77/43.02 % (4044439)------------------------------ % 299.77/43.02 % (4044439)------------------------------ % 299.77/43.02 % (4044450)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2963805517:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2671 on theBenchmark for (2671ds/1244Mi) % 299.77/43.02 % (4044450)Instruction limit reached! % 299.77/43.02 % (4044450)------------------------------ % 299.77/43.02 % (4044450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.77/43.02 % (4044450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.77/43.02 % (4044450)CaDiCaL version: 2.1.3 % 299.77/43.02 % (4044450)Termination reason: Instruction limit % 299.77/43.02 % (4044450)Termination phase: Saturation % 299.77/43.02 % (4044450)Time elapsed: 0.576 s % 299.77/43.02 % (4044450)Peak memory usage: 128 MB % 299.77/43.02 % (4044450)Instructions burned: 1245 (million) % 299.77/43.02 % (4044408)Instruction limit reached! % 299.77/43.02 % (4044408)------------------------------ % 299.77/43.02 % (4044408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.77/43.02 % (4044408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.77/43.02 % (4044408)CaDiCaL version: 2.1.3 % 299.77/43.02 % (4044408)Termination reason: Instruction limit % 300.76/43.08 % (4044408)Termination phase: Saturation % 300.76/43.08 % (4044408)Time elapsed: 1.893 s % 300.76/43.08 % (4044408)Peak memory usage: 150 MB % 300.76/43.08 % (4044408)Instructions burned: 2064 (million) % 300.76/43.08 % (4044469)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=849821139:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2664 on theBenchmark for (2664ds/58261Mi) % 300.76/43.08 % (4044470)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 % 300.76/43.08 % (4044470)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1649508458:i=6806:aac=none:nm=0:rtra=on:rawr=on_2663 on theBenchmark for (2663ds/6806Mi) % 300.76/43.08 % (4044360)Instruction limit reached! % 300.76/43.08 % (4044360)------------------------------ % 300.76/43.08 % (4044360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044360)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044360)Termination reason: Instruction limit % 300.76/43.08 % (4044360)Termination phase: Saturation % 300.76/43.08 % (4044360)Time elapsed: 3.378 s % 300.76/43.08 % (4044360)Peak memory usage: 116 MB % 300.76/43.08 % (4044360)Instructions burned: 3553 (million) % 300.76/43.08 % (4044485)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=942629497:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2659 on theBenchmark for (2659ds/4081Mi) % 300.76/43.08 % (4044349)Instruction limit reached! % 300.76/43.08 % (4044349)------------------------------ % 300.76/43.08 % (4044349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044349)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044349)Termination reason: Instruction limit % 300.76/43.08 % (4044349)Termination phase: Saturation % 300.76/43.08 % (4044349)Time elapsed: 6.0000 s % 300.76/43.08 % (4044349)Peak memory usage: 157 MB % 300.76/43.08 % (4044349)Instructions burned: 6806 (million) % 300.76/43.08 % (4044534)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2318904607:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2634 on theBenchmark for (2634ds/1701Mi) % 300.76/43.08 % (4044485)Instruction limit reached! % 300.76/43.08 % (4044485)------------------------------ % 300.76/43.08 % (4044485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044485)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044485)Termination reason: Instruction limit % 300.76/43.08 % (4044485)Termination phase: Saturation % 300.76/43.08 % (4044485)Time elapsed: 3.889 s % 300.76/43.08 % (4044485)Peak memory usage: 166 MB % 300.76/43.08 % (4044485)Instructions burned: 4081 (million) % 300.76/43.08 % (4044534)Instruction limit reached! % 300.76/43.08 % (4044534)------------------------------ % 300.76/43.08 % (4044534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044534)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044534)Termination reason: Instruction limit % 300.76/43.08 % (4044534)Termination phase: Saturation % 300.76/43.08 % (4044534)Time elapsed: 1.469 s % 300.76/43.08 % (4044534)Peak memory usage: 132 MB % 300.76/43.08 % (4044534)Instructions burned: 1702 (million) % 300.76/43.08 % (4044558)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=2613448604:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2618 on theBenchmark for (2618ds/57001Mi) % 300.76/43.08 % (4044561)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 % 300.76/43.08 % (4044561)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4074486672:i=8622:aac=none:nm=0:rtra=on:rawr=on_2618 on theBenchmark for (2618ds/8622Mi) % 300.76/43.08 % (4044470)Instruction limit reached! % 300.76/43.08 % (4044470)------------------------------ % 300.76/43.08 % (4044470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044470)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044470)Termination reason: Instruction limit % 300.76/43.08 % (4044470)Termination phase: Saturation % 300.76/43.08 % (4044470)Time elapsed: 6.231 s % 300.76/43.08 % (4044470)Peak memory usage: 158 MB % 300.76/43.08 % (4044470)Instructions burned: 6807 (million) % 300.76/43.08 % (4044578)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1808701063:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2599 on theBenchmark for (2599ds/24Mi) % 300.76/43.08 % (4044578)Instruction limit reached! % 300.76/43.08 % (4044578)------------------------------ % 300.76/43.08 % (4044578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044578)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044578)Termination reason: Instruction limit % 300.76/43.08 % (4044578)Termination phase: SInE selection % 300.76/43.08 % (4044578)Time elapsed: 0.021 s % 300.76/43.08 % (4044578)Peak memory usage: 86 MB % 300.76/43.08 % (4044578)Instructions burned: 24 (million) % 300.76/43.08 % (4044580)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3191321101:i=614:kws=precedence:nm=0:rtra=on_2596 on theBenchmark for (2596ds/614Mi) % 300.76/43.08 % (4044580)Instruction limit reached! % 300.76/43.08 % (4044580)------------------------------ % 300.76/43.08 % (4044580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044580)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044580)Termination reason: Instruction limit % 300.76/43.08 % (4044580)Termination phase: Saturation % 300.76/43.08 % (4044580)Time elapsed: 0.611 s % 300.76/43.08 % (4044580)Peak memory usage: 121 MB % 300.76/43.08 % (4044580)Instructions burned: 614 (million) % 300.76/43.08 % (4044586)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=768495413:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2588 on theBenchmark for (2588ds/402Mi) % 300.76/43.08 % (4044586)Instruction limit reached! % 300.76/43.08 % (4044586)------------------------------ % 300.76/43.08 % (4044586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044586)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044586)Termination reason: Instruction limit % 300.76/43.08 % (4044586)Termination phase: Saturation % 300.76/43.08 % (4044586)Time elapsed: 0.455 s % 300.76/43.08 % (4044586)Peak memory usage: 120 MB % 300.76/43.08 % (4044586)Instructions burned: 402 (million) % 300.76/43.08 % (4044590)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1257544998:s2a=on:i=14:rtra=on:inst=on_2582 on theBenchmark for (2582ds/14Mi) % 300.76/43.08 % (4044590)Instruction limit reached! % 300.76/43.08 % (4044590)------------------------------ % 300.76/43.08 % (4044590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044590)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044590)Termination reason: Instruction limit % 300.76/43.08 % (4044590)Termination phase: Preprocessing 1 % 300.76/43.08 % (4044590)Time elapsed: 0.012 s % 300.76/43.08 % (4044590)Peak memory usage: 86 MB % 300.76/43.08 % (4044590)Instructions burned: 14 (million) % 300.76/43.08 % (4044593)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2458491116:i=8:rtra=on_2580 on theBenchmark for (2580ds/8Mi) % 300.76/43.08 % (4044593)Instruction limit reached! % 300.76/43.08 % (4044593)------------------------------ % 300.76/43.08 % (4044593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.76/43.08 % (4044593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.76/43.08 % (4044593)CaDiCaL version: 2.1.3 % 300.76/43.08 % (4044593)Termination reason: Instruction limit % 300.76/43.08 % (4044593)Termination phase: Property scanning % 300.76/43.08 % (4044593)Time elapsed: 0.009 s % 300.76/43.08 % (4044593)Peak memory usage: 86 MB % 300.76/43.08 % (4044593)Instructions burned: 9 (million) % 300.76/43.08 % (4044596)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1139236380:i=92:rtra=on_2578 on theBenchmark for % 300.76/43.08 Terminated %------------------------------------------------------------------------------