%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW578_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n009.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:30:51 PM UTC 2026 % Result : Timeout 300.74s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW578_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.20 % Computer : n009.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:20:00 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/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 % 5.20/1.56 % (3057200)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.20/1.56 % (3057339)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2967092804:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.20/1.56 % (3057339)Instruction limit reached! % 5.20/1.56 % (3057339)------------------------------ % 5.20/1.56 % (3057339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.56 % (3057339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.56 % (3057339)CaDiCaL version: 2.1.3 % 5.20/1.56 % (3057339)Termination reason: Instruction limit % 5.20/1.56 % (3057339)Termination phase: Property scanning % 5.20/1.56 % (3057339)Time elapsed: 0.004 s % 5.20/1.56 % (3057339)Peak memory usage: 86 MB % 5.20/1.56 % (3057339)Instructions burned: 7 (million) % 5.20/1.56 % (3057336)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1362662247:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.20/1.56 % (3057340)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=149132488:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.20/1.56 % (3057337)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1334541937:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.20/1.56 % (3057342)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2088431315:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.20/1.56 % (3057340)Instruction limit reached! % 5.20/1.56 % (3057340)------------------------------ % 5.20/1.56 % (3057340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.56 % (3057340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.56 % (3057341)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1366332913:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.20/1.56 % (3057340)CaDiCaL version: 2.1.3 % 5.20/1.56 % (3057340)Termination reason: Instruction limit % 5.20/1.56 % (3057340)Termination phase: Preprocessing 3 % 5.20/1.56 % (3057340)Time elapsed: 0.005 s % 5.20/1.56 % (3057340)Peak memory usage: 86 MB % 5.20/1.56 % (3057340)Instructions burned: 4 (million) % 5.20/1.56 % (3057335)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1660469075:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.20/1.56 % (3057335)Instruction limit reached! % 5.20/1.56 % (3057335)------------------------------ % 5.20/1.56 % (3057335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.56 % (3057335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.56 % (3057335)CaDiCaL version: 2.1.3 % 5.20/1.56 % (3057335)Termination reason: Instruction limit % 5.20/1.56 % (3057335)Termination phase: Saturation % 5.20/1.56 % (3057335)Time elapsed: 0.020 s % 5.20/1.56 % (3057335)Peak memory usage: 94 MB % 5.20/1.56 % (3057335)Instructions burned: 12 (million) % 5.20/1.56 % (3057342)Instruction limit reached! % 5.20/1.56 % (3057342)------------------------------ % 5.20/1.56 % (3057342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.56 % (3057342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.56 % (3057342)CaDiCaL version: 2.1.3 % 5.20/1.56 % (3057342)Termination reason: Instruction limit % 5.20/1.56 % (3057342)Termination phase: Saturation % 5.20/1.56 % (3057342)Time elapsed: 0.063 s % 5.20/1.56 % (3057342)Peak memory usage: 116 MB % 5.20/1.56 % (3057342)Instructions burned: 33 (million) % 5.20/1.56 % (3057341)Instruction limit reached! % 5.20/1.56 % (3057341)------------------------------ % 5.20/1.56 % (3057341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.56 % (3057341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.56 % (3057341)CaDiCaL version: 2.1.3 % 5.20/1.56 % (3057341)Termination reason: Instruction limit % 5.20/1.56 % (3057341)Termination phase: Saturation % 5.20/1.56 % (3057341)Time elapsed: 0.081 s % 5.20/1.56 % (3057341)Peak memory usage: 116 MB % 5.20/1.56 % (3057341)Instructions burned: 46 (million) % 5.20/1.56 % (3057359)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3870401678:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.20/1.56 % (3057336)Instruction limit reached! % 5.20/1.56 % (3057336)------------------------------ % 6.55/1.76 % (3057336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.76 % (3057336)CaDiCaL version: 2.1.3 % 6.55/1.76 % (3057336)Termination reason: Instruction limit % 6.55/1.76 % (3057336)Termination phase: Property scanning % 6.55/1.76 % (3057336)Time elapsed: 0.237 s % 6.55/1.76 % (3057336)Peak memory usage: 87 MB % 6.55/1.76 % (3057336)Instructions burned: 307 (million) % 6.55/1.76 % (3057359)Instruction limit reached! % 6.55/1.76 % (3057359)------------------------------ % 6.55/1.76 % (3057359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.76 % (3057359)CaDiCaL version: 2.1.3 % 6.55/1.76 % (3057359)Termination reason: Instruction limit % 6.55/1.76 % (3057359)Termination phase: Saturation % 6.55/1.76 % (3057359)Time elapsed: 0.009 s % 6.55/1.76 % (3057359)Peak memory usage: 89 MB % 6.55/1.76 % (3057359)Instructions burned: 15 (million) % 6.55/1.76 % (3057337)Instruction limit reached! % 6.55/1.76 % (3057337)------------------------------ % 6.55/1.76 % (3057337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.76 % (3057337)CaDiCaL version: 2.1.3 % 6.55/1.76 % (3057337)Termination reason: Instruction limit % 6.55/1.76 % (3057337)Termination phase: Saturation % 6.55/1.76 % (3057337)Time elapsed: 0.227 s % 6.55/1.76 % (3057337)Peak memory usage: 119 MB % 6.55/1.76 % (3057337)Instructions burned: 204 (million) % 6.55/1.76 % (3057367)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=843242046:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.55/1.76 % (3057368)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=647563299:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 6.55/1.76 % (3057367)Instruction limit reached! % 6.55/1.76 % (3057367)------------------------------ % 6.55/1.76 % (3057367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.76 % (3057367)CaDiCaL version: 2.1.3 % 6.55/1.76 % (3057367)Termination reason: Instruction limit % 6.55/1.76 % (3057367)Termination phase: Property scanning % 6.55/1.76 % (3057367)Time elapsed: 0.026 s % 6.55/1.76 % (3057367)Peak memory usage: 87 MB % 6.55/1.76 % (3057367)Instructions burned: 30 (million) % 6.55/1.76 % (3057368)Instruction limit reached! % 6.55/1.76 % (3057368)------------------------------ % 6.55/1.76 % (3057368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.76 % (3057368)CaDiCaL version: 2.1.3 % 6.55/1.76 % (3057368)Termination reason: Instruction limit % 6.55/1.76 % (3057368)Termination phase: Saturation % 6.55/1.76 % (3057368)Time elapsed: 0.017 s % 6.55/1.76 % (3057368)Peak memory usage: 88 MB % 6.55/1.76 % (3057368)Instructions burned: 16 (million) % 6.55/1.76 % (3057370)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=966060524:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 6.55/1.76 % (3057370)Instruction limit reached! % 6.55/1.76 % (3057370)------------------------------ % 6.55/1.76 % (3057370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.76 % (3057370)CaDiCaL version: 2.1.3 % 6.55/1.76 % (3057370)Termination reason: Instruction limit % 6.55/1.76 % (3057370)Termination phase: Saturation % 6.55/1.76 % (3057370)Time elapsed: 0.011 s % 6.55/1.76 % (3057370)Peak memory usage: 89 MB % 6.55/1.76 % (3057370)Instructions burned: 26 (million) % 6.55/1.76 % (3057372)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=2986521827:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.55/1.76 % (3057372)Instruction limit reached! % 6.55/1.76 % (3057372)------------------------------ % 6.55/1.76 % (3057372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.76 % (3057372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.96 % (3057372)CaDiCaL version: 2.1.3 % 7.58/1.96 % (3057372)Termination reason: Instruction limit % 7.58/1.96 % (3057372)Termination phase: Saturation % 7.58/1.96 % (3057372)Time elapsed: 0.030 s % 7.58/1.96 % (3057372)Peak memory usage: 89 MB % 7.58/1.96 % (3057372)Instructions burned: 27 (million) % 7.58/1.96 % (3057374)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3812906083:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 7.58/1.96 % (3057376)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=187781873:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 7.58/1.96 % (3057375)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3729224473:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 7.58/1.96 % (3057375)Instruction limit reached! % 7.58/1.96 % (3057375)------------------------------ % 7.58/1.96 % (3057375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.58/1.96 % (3057375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.96 % (3057375)CaDiCaL version: 2.1.3 % 7.58/1.96 % (3057375)Termination reason: Instruction limit % 7.58/1.96 % (3057375)Termination phase: Preprocessing 1 % 7.58/1.96 % (3057375)Time elapsed: 0.003 s % 7.58/1.96 % (3057375)Peak memory usage: 85 MB % 7.58/1.96 % (3057375)Instructions burned: 2 (million) % 7.58/1.96 % (3057384)lrs+10_1_thi=all:si=on:fd=off:random_seed=3142034179:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 7.58/1.96 % (3057374)Instruction limit reached! % 7.58/1.96 % (3057374)------------------------------ % 7.58/1.96 % (3057374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.58/1.96 % (3057374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.96 % (3057374)CaDiCaL version: 2.1.3 % 7.58/1.96 % (3057374)Termination reason: Instruction limit % 7.58/1.96 % (3057374)Termination phase: Saturation % 7.58/1.96 % (3057374)Time elapsed: 0.079 s % 7.58/1.96 % (3057374)Peak memory usage: 89 MB % 7.58/1.96 % (3057374)Instructions burned: 85 (million) % 7.58/1.96 % (3057379)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3340414424:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 7.58/1.96 % (3057384)Instruction limit reached! % 7.58/1.96 % (3057384)------------------------------ % 7.58/1.96 % (3057384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.58/1.96 % (3057384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.96 % (3057384)CaDiCaL version: 2.1.3 % 7.58/1.96 % (3057384)Termination reason: Instruction limit % 7.58/1.96 % (3057384)Termination phase: Saturation % 7.58/1.96 % (3057384)Time elapsed: 0.052 s % 7.58/1.96 % (3057384)Peak memory usage: 116 MB % 7.58/1.96 % (3057384)Instructions burned: 53 (million) % 7.58/1.96 % (3057379)Instruction limit reached! % 7.58/1.96 % (3057379)------------------------------ % 7.58/1.96 % (3057379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.58/1.96 % (3057379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.96 % (3057379)CaDiCaL version: 2.1.3 % 7.58/1.96 % (3057379)Termination reason: Instruction limit % 7.58/1.96 % (3057379)Termination phase: Preprocessing 3 % 7.58/1.96 % (3057379)Time elapsed: 0.004 s % 7.58/1.96 % (3057379)Peak memory usage: 86 MB % 7.58/1.96 % (3057379)Instructions burned: 5 (million) % 7.58/1.96 % (3057382)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3953563039:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 7.58/1.96 % (3057393)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=979390132:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 7.58/1.96 % (3057393)Instruction limit reached! % 7.58/1.96 % (3057393)------------------------------ % 7.58/1.96 % (3057393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.58/1.96 % (3057393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.58/1.96 % (3057393)CaDiCaL version: 2.1.3 % 7.58/1.96 % (3057393)Termination reason: Instruction limit % 7.58/1.96 % (3057393)Termination phase: Property scanning % 7.58/1.96 % (3057393)Time elapsed: 0.009 s % 7.58/1.96 % (3057393)Peak memory usage: 86 MB % 7.58/1.96 % (3057393)Instructions burned: 8 (million) % 11.48/2.39 % (3057376)Instruction limit reached! % 11.48/2.39 % (3057376)------------------------------ % 11.48/2.39 % (3057376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.39 % (3057376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.39 % (3057376)CaDiCaL version: 2.1.3 % 11.48/2.39 % (3057376)Termination reason: Instruction limit % 11.48/2.39 % (3057376)Termination phase: Saturation % 11.48/2.39 % (3057376)Time elapsed: 0.204 s % 11.48/2.39 % (3057376)Peak memory usage: 91 MB % 11.48/2.39 % (3057376)Instructions burned: 181 (million) % 11.48/2.39 % (3057382)Instruction limit reached! % 11.48/2.39 % (3057382)------------------------------ % 11.48/2.39 % (3057382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.39 % (3057382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.39 % (3057382)CaDiCaL version: 2.1.3 % 11.48/2.39 % (3057382)Termination reason: Instruction limit % 11.48/2.39 % (3057382)Termination phase: Saturation % 11.48/2.39 % (3057382)Time elapsed: 0.136 s % 11.48/2.39 % (3057382)Peak memory usage: 134 MB % 11.48/2.39 % (3057382)Instructions burned: 66 (million) % 11.48/2.39 % (3057402)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=898304595:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 11.48/2.39 % (3057402)Instruction limit reached! % 11.48/2.39 % (3057402)------------------------------ % 11.48/2.39 % (3057402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.39 % (3057402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.39 % (3057402)CaDiCaL version: 2.1.3 % 11.48/2.39 % (3057402)Termination reason: Instruction limit % 11.48/2.39 % (3057402)Termination phase: shuffling % 11.48/2.39 % (3057402)Time elapsed: 0.003 s % 11.48/2.39 % (3057402)Peak memory usage: 86 MB % 11.48/2.39 % (3057402)Instructions burned: 2 (million) % 11.48/2.39 % (3057408)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=753663925:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 11.48/2.39 % (3057407)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1825007658:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 11.48/2.39 % (3057407)Instruction limit reached! % 11.48/2.39 % (3057407)------------------------------ % 11.48/2.39 % (3057407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.39 % (3057407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.39 % (3057407)CaDiCaL version: 2.1.3 % 11.48/2.39 % (3057407)Termination reason: Instruction limit % 11.48/2.39 % (3057407)Termination phase: Preprocessing 1 % 11.48/2.39 % (3057407)Time elapsed: 0.003 s % 11.48/2.39 % (3057407)Peak memory usage: 85 MB % 11.48/2.39 % (3057407)Instructions burned: 2 (million) % 11.48/2.39 % (3057409)dis+10_1_si=on:random_seed=1638625647:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 11.48/2.39 % (3057413)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3518647344:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 11.48/2.39 % (3057409)Instruction limit reached! % 11.48/2.39 % (3057409)------------------------------ % 11.48/2.39 % (3057409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.39 % (3057409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.39 % (3057409)CaDiCaL version: 2.1.3 % 11.48/2.39 % (3057409)Termination reason: Instruction limit % 11.48/2.39 % (3057409)Termination phase: Property scanning % 11.48/2.39 % (3057409)Time elapsed: 0.011 s % 11.48/2.39 % (3057409)Peak memory usage: 87 MB % 11.48/2.39 % (3057409)Instructions burned: 11 (million) % 11.48/2.39 % (3057408)Instruction limit reached! % 11.48/2.39 % (3057408)------------------------------ % 11.48/2.39 % (3057408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.48/2.39 % (3057408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.48/2.39 % (3057408)CaDiCaL version: 2.1.3 % 11.48/2.39 % (3057408)Termination reason: Instruction limit % 11.48/2.39 % (3057408)Termination phase: Saturation % 11.48/2.39 % (3057408)Time elapsed: 0.102 s % 11.48/2.39 % (3057408)Peak memory usage: 118 MB % 11.48/2.39 % (3057408)Instructions burned: 128 (million) % 11.48/2.39 % (3057413)Instruction limit reached! % 11.48/2.39 % (3057413)------------------------------ % 11.48/2.39 % (3057413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.56/2.67 % (3057413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.56/2.67 % (3057413)CaDiCaL version: 2.1.3 % 12.56/2.67 % (3057413)Termination reason: Instruction limit % 12.56/2.67 % (3057413)Termination phase: Saturation % 12.56/2.67 % (3057413)Time elapsed: 0.027 s % 12.56/2.67 % (3057413)Peak memory usage: 89 MB % 12.56/2.67 % (3057413)Instructions burned: 36 (million) % 12.56/2.67 % (3057412)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=837430382:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 12.56/2.67 % (3057412)Refutation not found, incomplete strategy % 12.56/2.67 % (3057412)------------------------------ % 12.56/2.67 % (3057412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.56/2.67 % (3057412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.56/2.67 % (3057412)CaDiCaL version: 2.1.3 % 12.56/2.67 % (3057412)Termination reason: Refutation not found, incomplete strategy % 12.56/2.67 % (3057412)Time elapsed: 0.021 s % 12.56/2.67 % (3057412)Peak memory usage: 89 MB % 12.56/2.67 % (3057412)Instructions burned: 19 (million) % 12.56/2.67 % (3057415)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1683360214:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 12.56/2.67 % (3057415)Instruction limit reached! % 12.56/2.67 % (3057415)------------------------------ % 12.56/2.67 % (3057415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.56/2.67 % (3057415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.56/2.67 % (3057415)CaDiCaL version: 2.1.3 % 12.56/2.67 % (3057415)Termination reason: Instruction limit % 12.56/2.67 % (3057415)Termination phase: Preprocessing 1 % 12.56/2.67 % (3057415)Time elapsed: 0.003 s % 12.56/2.67 % (3057415)Peak memory usage: 85 MB % 12.56/2.67 % (3057415)Instructions burned: 2 (million) % 12.56/2.67 % (3057416)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1657033514:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 12.56/2.67 % (3057416)Instruction limit reached! % 12.56/2.67 % (3057416)------------------------------ % 12.56/2.67 % (3057416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.56/2.67 % (3057416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.56/2.67 % (3057416)CaDiCaL version: 2.1.3 % 12.56/2.67 % (3057416)Termination reason: Instruction limit % 12.56/2.67 % (3057416)Termination phase: Equality resolution with deletion % 12.56/2.67 % (3057416)Time elapsed: 0.009 s % 12.56/2.67 % (3057416)Peak memory usage: 86 MB % 12.56/2.67 % (3057416)Instructions burned: 8 (million) % 12.56/2.67 % (3057424)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4024854981:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 12.56/2.67 % (3057425)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=908343440:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 12.56/2.67 % (3057419)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2510729820:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 12.56/2.67 % (3057425)Instruction limit reached! % 12.56/2.67 % (3057425)------------------------------ % 12.56/2.67 % (3057425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.56/2.67 % (3057425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.56/2.67 % (3057425)CaDiCaL version: 2.1.3 % 12.56/2.67 % (3057425)Termination reason: Instruction limit % 12.56/2.67 % (3057425)Termination phase: Saturation % 12.56/2.67 % (3057425)Time elapsed: 0.007 s % 12.56/2.67 % (3057425)Peak memory usage: 88 MB % 12.56/2.67 % (3057425)Instructions burned: 10 (million) % 12.56/2.67 % (3057422)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=37527071:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 12.56/2.67 % (3057422)Instruction limit reached! % 12.56/2.67 % (3057422)------------------------------ % 12.56/2.67 % (3057422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.56/2.67 % (3057422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.56/2.67 % (3057422)CaDiCaL version: 2.1.3 % 12.56/2.67 % (3057422)Termination reason: Instruction limit % 12.56/2.67 % (3057422)Termination phase: Saturation % 13.84/2.89 % (3057422)Time elapsed: 0.020 s % 13.84/2.89 % (3057422)Peak memory usage: 93 MB % 13.84/2.89 % (3057422)Instructions burned: 13 (million) % 13.84/2.89 % (3057424)Instruction limit reached! % 13.84/2.89 % (3057424)------------------------------ % 13.84/2.89 % (3057424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.89 % (3057424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.89 % (3057424)CaDiCaL version: 2.1.3 % 13.84/2.89 % (3057424)Termination reason: Instruction limit % 13.84/2.89 % (3057424)Termination phase: Saturation % 13.84/2.89 % (3057424)Time elapsed: 0.150 s % 13.84/2.89 % (3057424)Peak memory usage: 119 MB % 13.84/2.89 % (3057424)Instructions burned: 226 (million) % 13.84/2.89 % (3057436)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=1392035215:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 13.84/2.89 % (3057430)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2348961973:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 13.84/2.89 % (3057431)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=339980730:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 13.84/2.89 % (3057439)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4165639688:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 13.84/2.89 % (3057412)------------------------------ % 13.84/2.89 % (3057412)------------------------------ % 13.84/2.89 % (3057431)Instruction limit reached! % 13.84/2.89 % (3057431)------------------------------ % 13.84/2.89 % (3057431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.89 % (3057431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.89 % (3057431)CaDiCaL version: 2.1.3 % 13.84/2.89 % (3057431)Termination reason: Instruction limit % 13.84/2.89 % (3057431)Termination phase: Saturation % 13.84/2.89 % (3057431)Time elapsed: 0.082 s % 13.84/2.89 % (3057431)Peak memory usage: 90 MB % 13.84/2.89 % (3057431)Instructions burned: 76 (million) % 13.84/2.89 % (3057439)Instruction limit reached! % 13.84/2.89 % (3057439)------------------------------ % 13.84/2.89 % (3057439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.89 % (3057439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.89 % (3057439)CaDiCaL version: 2.1.3 % 13.84/2.89 % (3057439)Termination reason: Instruction limit % 13.84/2.89 % (3057439)Termination phase: Property scanning % 13.84/2.89 % (3057439)Time elapsed: 0.102 s % 13.84/2.89 % (3057439)Peak memory usage: 87 MB % 13.84/2.89 % (3057439)Instructions burned: 130 (million) % 13.84/2.89 % (3057442)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=401459930:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 13.84/2.89 % (3057419)Instruction limit reached! % 13.84/2.89 % (3057419)------------------------------ % 13.84/2.89 % (3057419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.89 % (3057419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.89 % (3057419)CaDiCaL version: 2.1.3 % 13.84/2.89 % (3057419)Termination reason: Instruction limit % 13.84/2.89 % (3057419)Termination phase: Saturation % 13.84/2.89 % (3057419)Time elapsed: 0.363 s % 13.84/2.89 % (3057419)Peak memory usage: 91 MB % 13.84/2.89 % (3057419)Instructions burned: 370 (million) % 13.84/2.89 % (3057430)Instruction limit reached! % 13.84/2.89 % (3057430)------------------------------ % 13.84/2.89 % (3057430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.89 % (3057430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.89 % (3057430)CaDiCaL version: 2.1.3 % 13.84/2.89 % (3057430)Termination reason: Instruction limit % 13.84/2.89 % (3057430)Termination phase: Saturation % 13.84/2.89 % (3057430)Time elapsed: 0.141 s % 13.84/2.89 % (3057430)Peak memory usage: 133 MB % 13.84/2.89 % (3057430)Instructions burned: 71 (million) % 13.84/2.89 % (3057436)Instruction limit reached! % 13.84/2.89 % (3057436)------------------------------ % 13.84/2.89 % (3057436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.84/2.89 % (3057436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.84/2.89 % (3057436)CaDiCaL version: 2.1.3 % 13.84/2.89 % (3057436)Termination reason: Instruction limit % 17.65/3.18 % (3057436)Termination phase: Property scanning % 17.65/3.18 % (3057436)Time elapsed: 0.225 s % 17.65/3.18 % (3057436)Peak memory usage: 87 MB % 17.65/3.18 % (3057436)Instructions burned: 295 (million) % 17.65/3.18 % (3057442)Instruction limit reached! % 17.65/3.18 % (3057442)------------------------------ % 17.65/3.18 % (3057442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.18 % (3057442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.18 % (3057442)CaDiCaL version: 2.1.3 % 17.65/3.18 % (3057442)Termination reason: Instruction limit % 17.65/3.18 % (3057442)Termination phase: Saturation % 17.65/3.18 % (3057442)Time elapsed: 0.115 s % 17.65/3.18 % (3057442)Peak memory usage: 134 MB % 17.65/3.18 % (3057442)Instructions burned: 131 (million) % 17.65/3.18 % (3057449)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3310058726:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 17.65/3.18 % (3057450)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=915219288:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 17.65/3.18 % (3057451)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2102614646:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 17.65/3.18 % (3057453)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2768760421:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 17.65/3.18 % (3057454)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=2309313268:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 17.65/3.18 % (3057449)Instruction limit reached! % 17.65/3.18 % (3057449)------------------------------ % 17.65/3.18 % (3057449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.18 % (3057449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.18 % (3057449)CaDiCaL version: 2.1.3 % 17.65/3.18 % (3057449)Termination reason: Instruction limit % 17.65/3.18 % (3057449)Termination phase: Saturation % 17.65/3.18 % (3057449)Time elapsed: 0.069 s % 17.65/3.18 % (3057449)Peak memory usage: 134 MB % 17.65/3.18 % (3057449)Instructions burned: 40 (million) % 17.65/3.18 % (3057457)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3006601038:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 17.65/3.18 % (3057455)dis+10_1_si=on:random_seed=3917699675:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi) % 17.65/3.18 % (3057453)Instruction limit reached! % 17.65/3.18 % (3057453)------------------------------ % 17.65/3.18 % (3057453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.18 % (3057453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.18 % (3057453)CaDiCaL version: 2.1.3 % 17.65/3.18 % (3057453)Termination reason: Instruction limit % 17.65/3.18 % (3057453)Termination phase: Saturation % 17.65/3.18 % (3057453)Time elapsed: 0.113 s % 17.65/3.18 % (3057453)Peak memory usage: 117 MB % 17.65/3.18 % (3057453)Instructions burned: 132 (million) % 17.65/3.18 % (3057450)Instruction limit reached! % 17.65/3.18 % (3057450)------------------------------ % 17.65/3.18 % (3057450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.18 % (3057450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.18 % (3057450)CaDiCaL version: 2.1.3 % 17.65/3.18 % (3057450)Termination reason: Instruction limit % 17.65/3.18 % (3057450)Termination phase: Saturation % 17.65/3.18 % (3057450)Time elapsed: 0.190 s % 17.65/3.18 % (3057450)Peak memory usage: 91 MB % 17.65/3.18 % (3057450)Instructions burned: 308 (million) % 17.65/3.18 % (3057457)Instruction limit reached! % 17.65/3.18 % (3057457)------------------------------ % 17.65/3.18 % (3057457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.18 % (3057457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.18 % (3057457)CaDiCaL version: 2.1.3 % 17.65/3.18 % (3057457)Termination reason: Instruction limit % 17.65/3.18 % (3057457)Termination phase: Saturation % 17.65/3.18 % (3057457)Time elapsed: 0.127 s % 17.65/3.18 % (3057457)Peak memory usage: 95 MB % 17.65/3.18 % (3057457)Instructions burned: 383 (million) % 17.65/3.18 % (3057488)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3616588711:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 18.43/3.48 % (3057454)Instruction limit reached! % 18.43/3.48 % (3057454)------------------------------ % 18.43/3.48 % (3057454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.43/3.48 % (3057454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.43/3.48 % (3057454)CaDiCaL version: 2.1.3 % 18.43/3.48 % (3057454)Termination reason: Instruction limit % 18.43/3.48 % (3057454)Termination phase: Saturation % 18.43/3.48 % (3057454)Time elapsed: 0.199 s % 18.43/3.48 % (3057454)Peak memory usage: 117 MB % 18.43/3.48 % (3057454)Instructions burned: 260 (million) % 18.43/3.48 % (3057513)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1304883599:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 18.43/3.48 % (3057535)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=4148689600:s2a=on:i=128:s2at=5:ins=3:rtra=on_2980 on theBenchmark for (2980ds/128Mi) % 18.43/3.48 % (3057488)Instruction limit reached! % 18.43/3.48 % (3057488)------------------------------ % 18.43/3.48 % (3057488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.43/3.48 % (3057488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.43/3.48 % (3057488)CaDiCaL version: 2.1.3 % 18.43/3.48 % (3057488)Termination reason: Instruction limit % 18.43/3.48 % (3057488)Termination phase: Saturation % 18.43/3.48 % (3057488)Time elapsed: 0.101 s % 18.43/3.48 % (3057488)Peak memory usage: 90 MB % 18.43/3.48 % (3057488)Instructions burned: 143 (million) % 18.43/3.48 % (3057513)Instruction limit reached! % 18.43/3.48 % (3057513)------------------------------ % 18.43/3.48 % (3057513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.43/3.48 % (3057513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.43/3.48 % (3057513)CaDiCaL version: 2.1.3 % 18.43/3.48 % (3057513)Termination reason: Instruction limit % 18.43/3.48 % (3057513)Termination phase: Saturation % 18.43/3.48 % (3057513)Time elapsed: 0.062 s % 18.43/3.48 % (3057513)Peak memory usage: 116 MB % 18.43/3.48 % (3057513)Instructions burned: 66 (million) % 18.43/3.48 % (3057534)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3363979616:i=121:nm=16:rtra=on_2980 on theBenchmark for (2980ds/121Mi) % 18.43/3.48 % (3057535)Instruction limit reached! % 18.43/3.48 % (3057535)------------------------------ % 18.43/3.48 % (3057535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.43/3.48 % (3057535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.43/3.48 % (3057535)CaDiCaL version: 2.1.3 % 18.43/3.48 % (3057535)Termination reason: Instruction limit % 18.43/3.48 % (3057535)Termination phase: Saturation % 18.43/3.48 % (3057535)Time elapsed: 0.059 s % 18.43/3.48 % (3057535)Peak memory usage: 118 MB % 18.43/3.48 % (3057535)Instructions burned: 129 (million) % 18.43/3.48 % (3057549)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=1103062970:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi) % 18.43/3.48 % (3057534)Instruction limit reached! % 18.43/3.48 % (3057534)------------------------------ % 18.43/3.48 % (3057534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.43/3.48 % (3057534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.43/3.48 % (3057534)CaDiCaL version: 2.1.3 % 18.43/3.48 % (3057534)Termination reason: Instruction limit % 18.43/3.48 % (3057534)Termination phase: Saturation % 18.43/3.48 % (3057534)Time elapsed: 0.078 s % 18.43/3.48 % (3057534)Peak memory usage: 89 MB % 18.43/3.48 % (3057534)Instructions burned: 121 (million) % 18.43/3.48 % (3057451)Instruction limit reached! % 18.43/3.48 % (3057451)------------------------------ % 18.43/3.48 % (3057451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.43/3.48 % (3057451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.43/3.48 % (3057451)CaDiCaL version: 2.1.3 % 18.43/3.48 % (3057451)Termination reason: Instruction limit % 18.43/3.48 % (3057451)Termination phase: Saturation % 18.43/3.48 % (3057451)Time elapsed: 0.427 s % 18.43/3.48 % (3057451)Peak memory usage: 141 MB % 18.43/3.48 % (3057451)Instructions burned: 599 (million) % 18.43/3.48 % (3057549)Instruction limit reached! % 18.43/3.48 % (3057549)------------------------------ % 18.43/3.48 % (3057549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.61/3.80 % (3057549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.61/3.80 % (3057549)CaDiCaL version: 2.1.3 % 20.61/3.80 % (3057549)Termination reason: Instruction limit % 20.61/3.80 % (3057549)Termination phase: Saturation % 20.61/3.80 % (3057549)Time elapsed: 0.050 s % 20.61/3.80 % (3057549)Peak memory usage: 116 MB % 20.61/3.80 % (3057549)Instructions burned: 40 (million) % 20.61/3.80 % (3057567)dis+1010_1_to=kbo:si=on:random_seed=687555506:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi) % 20.61/3.80 % (3057581)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3546087257:s2a=on:i=483:doe=on:nm=32:rtra=on_2978 on theBenchmark for (2978ds/483Mi) % 20.61/3.80 % (3057579)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=826918988:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/329Mi) % 20.61/3.80 % (3057567)Instruction limit reached! % 20.61/3.80 % (3057567)------------------------------ % 20.61/3.80 % (3057567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.61/3.80 % (3057567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.61/3.80 % (3057567)CaDiCaL version: 2.1.3 % 20.61/3.80 % (3057567)Termination reason: Instruction limit % 20.61/3.80 % (3057567)Termination phase: Property scanning % 20.61/3.80 % (3057567)Time elapsed: 0.065 s % 20.61/3.80 % (3057567)Peak memory usage: 87 MB % 20.61/3.80 % (3057567)Instructions burned: 175 (million) % 20.61/3.80 % (3057583)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3194725419:thitd=on:i=215:nm=0:rtra=on:ev=force_2978 on theBenchmark for (2978ds/215Mi) % 20.61/3.80 % (3057585)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=378198257:st=2:i=295:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/295Mi) % 20.61/3.80 % (3057584)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2340072112:i=349:rtra=on_2977 on theBenchmark for (2977ds/349Mi) % 20.61/3.80 % (3057583)Instruction limit reached! % 20.61/3.80 % (3057583)------------------------------ % 20.61/3.80 % (3057583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.61/3.80 % (3057583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.61/3.80 % (3057583)CaDiCaL version: 2.1.3 % 20.61/3.80 % (3057583)Termination reason: Instruction limit % 20.61/3.80 % (3057583)Termination phase: Property scanning % 20.61/3.80 % (3057583)Time elapsed: 0.080 s % 20.61/3.80 % (3057583)Peak memory usage: 87 MB % 20.61/3.80 % (3057583)Instructions burned: 216 (million) % 20.61/3.80 % (3057581)Instruction limit reached! % 20.61/3.80 % (3057581)------------------------------ % 20.61/3.80 % (3057581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.61/3.80 % (3057581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.61/3.80 % (3057581)CaDiCaL version: 2.1.3 % 20.61/3.80 % (3057581)Termination reason: Instruction limit % 20.61/3.80 % (3057581)Termination phase: Saturation % 20.61/3.80 % (3057581)Time elapsed: 0.195 s % 20.61/3.80 % (3057581)Peak memory usage: 136 MB % 20.61/3.80 % (3057581)Instructions burned: 486 (million) % 20.61/3.80 % (3057597)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3413370769:i=328:kws=inv_frequency:nm=20:rtra=on_2977 on theBenchmark for (2977ds/328Mi) % 20.61/3.80 % (3057455)Instruction limit reached! % 20.61/3.80 % (3057455)------------------------------ % 20.61/3.80 % (3057455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.61/3.80 % (3057455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.61/3.80 % (3057455)CaDiCaL version: 2.1.3 % 20.61/3.80 % (3057455)Termination reason: Instruction limit % 20.61/3.80 % (3057455)Termination phase: Saturation % 20.61/3.80 % (3057455)Time elapsed: 0.629 s % 20.61/3.80 % (3057455)Peak memory usage: 96 MB % 20.61/3.80 % (3057455)Instructions burned: 1000 (million) % 20.61/3.80 % (3057579)Instruction limit reached! % 20.61/3.80 % (3057579)------------------------------ % 20.61/3.80 % (3057579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.61/3.80 % (3057579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.61/3.80 % (3057579)CaDiCaL version: 2.1.3 % 20.61/3.80 % (3057579)Termination reason: Instruction limit % 20.61/3.80 % (3057579)Termination phase: Saturation % 21.32/4.03 % (3057579)Time elapsed: 0.252 s % 21.32/4.03 % (3057579)Peak memory usage: 119 MB % 21.32/4.03 % (3057579)Instructions burned: 329 (million) % 21.32/4.03 % (3057585)Instruction limit reached! % 21.32/4.03 % (3057585)------------------------------ % 21.32/4.03 % (3057585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.32/4.03 % (3057585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.32/4.03 % (3057585)CaDiCaL version: 2.1.3 % 21.32/4.03 % (3057585)Termination reason: Instruction limit % 21.32/4.03 % (3057585)Termination phase: Saturation % 21.32/4.03 % (3057585)Time elapsed: 0.167 s % 21.32/4.03 % (3057585)Peak memory usage: 91 MB % 21.32/4.03 % (3057585)Instructions burned: 295 (million) % 21.32/4.03 % (3057642)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1736355061:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/484Mi) % 21.32/4.03 % (3057584)Instruction limit reached! % 21.32/4.03 % (3057584)------------------------------ % 21.32/4.03 % (3057584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.32/4.03 % (3057584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.32/4.03 % (3057584)CaDiCaL version: 2.1.3 % 21.32/4.03 % (3057584)Termination reason: Instruction limit % 21.32/4.03 % (3057584)Termination phase: Saturation % 21.32/4.03 % (3057584)Time elapsed: 0.192 s % 21.32/4.03 % (3057584)Peak memory usage: 117 MB % 21.32/4.03 % (3057584)Instructions burned: 349 (million) % 21.32/4.03 % (3057640)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1384253791:i=281:gtgl=2:rtra=on:gtg=all_2975 on theBenchmark for (2975ds/281Mi) % 21.32/4.03 % (3057643)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2078800837:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2975 on theBenchmark for (2975ds/321Mi) % 21.32/4.03 % (3057642)Instruction limit reached! % 21.32/4.03 % (3057642)------------------------------ % 21.32/4.03 % (3057642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.32/4.03 % (3057642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.32/4.03 % (3057642)CaDiCaL version: 2.1.3 % 21.32/4.03 % (3057642)Termination reason: Instruction limit % 21.32/4.03 % (3057642)Termination phase: Property scanning % 21.32/4.03 % (3057642)Time elapsed: 0.093 s % 21.32/4.03 % (3057642)Peak memory usage: 87 MB % 21.32/4.03 % (3057642)Instructions burned: 486 (million) % 21.32/4.03 % (3057644)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2799923103:i=416:rtra=on:gtg=position:ss=axioms_2975 on theBenchmark for (2975ds/416Mi) % 21.32/4.03 % (3057645)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2826236327:i=471:thf=on:kws=precedence:rtra=on_2974 on theBenchmark for (2974ds/471Mi) % 21.32/4.03 % (3057597)Instruction limit reached! % 21.32/4.03 % (3057597)------------------------------ % 21.32/4.03 % (3057597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.32/4.03 % (3057597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.32/4.03 % (3057597)CaDiCaL version: 2.1.3 % 21.32/4.03 % (3057597)Termination reason: Instruction limit % 21.32/4.03 % (3057597)Termination phase: Saturation % 21.32/4.03 % (3057597)Time elapsed: 0.239 s % 21.32/4.03 % (3057597)Peak memory usage: 118 MB % 21.32/4.03 % (3057597)Instructions burned: 329 (million) % 21.32/4.03 % (3057648)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=2778236878:avsq=on:i=276:avsqr=1,2:rtra=on_2974 on theBenchmark for (2974ds/276Mi) % 21.32/4.03 % (3057650)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3013422561:i=375:kws=inv_arity_squared:rtra=on_2973 on theBenchmark for (2973ds/375Mi) % 21.32/4.03 % (3057640)Instruction limit reached! % 21.32/4.03 % (3057640)------------------------------ % 21.32/4.03 % (3057640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.32/4.03 % (3057640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.32/4.03 % (3057640)CaDiCaL version: 2.1.3 % 21.32/4.03 % (3057640)Termination reason: Instruction limit % 21.32/4.03 % (3057640)Termination phase: Saturation % 21.32/4.03 % (3057640)Time elapsed: 0.214 s % 21.32/4.03 % (3057640)Peak memory usage: 118 MB % 21.32/4.03 % (3057640)Instructions burned: 282 (million) % 21.32/4.03 % (3057643)Instruction limit reached! % 21.32/4.03 % (3057643)------------------------------ % 25.43/4.46 % (3057643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.46 % (3057643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.46 % (3057643)CaDiCaL version: 2.1.3 % 25.43/4.46 % (3057643)Termination reason: Instruction limit % 25.43/4.46 % (3057643)Termination phase: Saturation % 25.43/4.46 % (3057643)Time elapsed: 0.170 s % 25.43/4.46 % (3057643)Peak memory usage: 114 MB % 25.43/4.46 % (3057643)Instructions burned: 322 (million) % 25.43/4.46 % (3057653)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=550593378:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/387Mi) % 25.43/4.46 % (3057644)Instruction limit reached! % 25.43/4.46 % (3057644)------------------------------ % 25.43/4.46 % (3057644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.46 % (3057644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.46 % (3057644)CaDiCaL version: 2.1.3 % 25.43/4.46 % (3057644)Termination reason: Instruction limit % 25.43/4.46 % (3057644)Termination phase: Saturation % 25.43/4.46 % (3057644)Time elapsed: 0.251 s % 25.43/4.46 % (3057644)Peak memory usage: 123 MB % 25.43/4.46 % (3057644)Instructions burned: 418 (million) % 25.43/4.46 % (3057650)Instruction limit reached! % 25.43/4.46 % (3057650)------------------------------ % 25.43/4.46 % (3057650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.46 % (3057650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.46 % (3057650)CaDiCaL version: 2.1.3 % 25.43/4.46 % (3057650)Termination reason: Instruction limit % 25.43/4.46 % (3057650)Termination phase: Saturation % 25.43/4.46 % (3057650)Time elapsed: 0.146 s % 25.43/4.46 % (3057650)Peak memory usage: 118 MB % 25.43/4.46 % (3057650)Instructions burned: 377 (million) % 25.43/4.46 % (3057648)Instruction limit reached! % 25.43/4.46 % (3057648)------------------------------ % 25.43/4.46 % (3057648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.46 % (3057648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.46 % (3057648)CaDiCaL version: 2.1.3 % 25.43/4.46 % (3057648)Termination reason: Instruction limit % 25.43/4.46 % (3057648)Termination phase: Saturation % 25.43/4.46 % (3057648)Time elapsed: 0.214 s % 25.43/4.46 % (3057648)Peak memory usage: 135 MB % 25.43/4.46 % (3057648)Instructions burned: 276 (million) % 25.43/4.46 % (3057657)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=844996832:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2972 on theBenchmark for (2972ds/513Mi) % 25.43/4.46 % (3057658)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2064972310:i=334:rtra=on_2971 on theBenchmark for (2971ds/334Mi) % 25.43/4.46 % (3057645)Instruction limit reached! % 25.43/4.46 % (3057645)------------------------------ % 25.43/4.46 % (3057645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.46 % (3057645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.46 % (3057645)CaDiCaL version: 2.1.3 % 25.43/4.46 % (3057645)Termination reason: Instruction limit % 25.43/4.46 % (3057645)Termination phase: Saturation % 25.43/4.46 % (3057645)Time elapsed: 0.319 s % 25.43/4.46 % (3057645)Peak memory usage: 119 MB % 25.43/4.46 % (3057645)Instructions burned: 471 (million) % 25.43/4.46 % (3057661)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1280146954:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2970 on theBenchmark for (2970ds/341Mi) % 25.43/4.46 % (3057660)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3274763009:i=359:rtra=on:gtg=exists_top:ss=axioms_2970 on theBenchmark for (2970ds/359Mi) % 25.43/4.46 % (3057663)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3634135875:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/261Mi) % 25.43/4.46 % (3057653)Instruction limit reached! % 25.43/4.46 % (3057653)------------------------------ % 25.43/4.46 % (3057653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.46 % (3057653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.46 % (3057653)CaDiCaL version: 2.1.3 % 25.43/4.46 % (3057653)Termination reason: Instruction limit % 25.43/4.46 % (3057653)Termination phase: Saturation % 27.81/4.86 % (3057653)Time elapsed: 0.287 s % 27.81/4.86 % (3057653)Peak memory usage: 119 MB % 27.81/4.86 % (3057653)Instructions burned: 387 (million) % 27.81/4.86 % (3057661)Instruction limit reached! % 27.81/4.86 % (3057661)------------------------------ % 27.81/4.86 % (3057661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.81/4.86 % (3057661)CaDiCaL version: 2.1.3 % 27.81/4.86 % (3057661)Termination reason: Instruction limit % 27.81/4.86 % (3057661)Termination phase: Saturation % 27.81/4.86 % (3057661)Time elapsed: 0.129 s % 27.81/4.86 % (3057661)Peak memory usage: 120 MB % 27.81/4.86 % (3057661)Instructions burned: 344 (million) % 27.81/4.86 % (3057665)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=14181448:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2970 on theBenchmark for (2970ds/235Mi) % 27.81/4.86 % (3057658)Instruction limit reached! % 27.81/4.86 % (3057658)------------------------------ % 27.81/4.86 % (3057658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.81/4.86 % (3057658)CaDiCaL version: 2.1.3 % 27.81/4.86 % (3057658)Termination reason: Instruction limit % 27.81/4.86 % (3057658)Termination phase: Saturation % 27.81/4.86 % (3057658)Time elapsed: 0.273 s % 27.81/4.86 % (3057658)Peak memory usage: 135 MB % 27.81/4.86 % (3057658)Instructions burned: 336 (million) % 27.81/4.86 % (3057657)Instruction limit reached! % 27.81/4.86 % (3057657)------------------------------ % 27.81/4.86 % (3057657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.81/4.86 % (3057657)CaDiCaL version: 2.1.3 % 27.81/4.86 % (3057657)Termination reason: Instruction limit % 27.81/4.86 % (3057657)Termination phase: Saturation % 27.81/4.86 % (3057657)Time elapsed: 0.322 s % 27.81/4.86 % (3057657)Peak memory usage: 92 MB % 27.81/4.86 % (3057657)Instructions burned: 514 (million) % 27.81/4.86 % (3057660)Instruction limit reached! % 27.81/4.86 % (3057660)------------------------------ % 27.81/4.86 % (3057660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.81/4.86 % (3057660)CaDiCaL version: 2.1.3 % 27.81/4.86 % (3057660)Termination reason: Instruction limit % 27.81/4.86 % (3057660)Termination phase: Saturation % 27.81/4.86 % (3057660)Time elapsed: 0.207 s % 27.81/4.86 % (3057660)Peak memory usage: 92 MB % 27.81/4.86 % (3057660)Instructions burned: 359 (million) % 27.81/4.86 % (3057663)Instruction limit reached! % 27.81/4.86 % (3057663)------------------------------ % 27.81/4.86 % (3057663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.81/4.86 % (3057663)CaDiCaL version: 2.1.3 % 27.81/4.86 % (3057663)Termination reason: Instruction limit % 27.81/4.86 % (3057663)Termination phase: Saturation % 27.81/4.86 % (3057663)Time elapsed: 0.194 s % 27.81/4.86 % (3057663)Peak memory usage: 117 MB % 27.81/4.86 % (3057663)Instructions burned: 261 (million) % 27.81/4.86 % (3057670)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2938180643:i=146:doe=on:rtra=on_2968 on theBenchmark for (2968ds/146Mi) % 27.81/4.86 % (3057669)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=791784291:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2968 on theBenchmark for (2968ds/273Mi) % 27.81/4.86 % (3057670)Instruction limit reached! % 27.81/4.86 % (3057670)------------------------------ % 27.81/4.86 % (3057670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.81/4.86 % (3057670)CaDiCaL version: 2.1.3 % 27.81/4.86 % (3057670)Termination reason: Instruction limit % 27.81/4.86 % (3057670)Termination phase: Saturation % 27.81/4.86 % (3057670)Time elapsed: 0.055 s % 27.81/4.86 % (3057670)Peak memory usage: 90 MB % 27.81/4.86 % (3057670)Instructions burned: 146 (million) % 27.81/4.86 % (3057665)Instruction limit reached! % 27.81/4.86 % (3057665)------------------------------ % 27.81/4.86 % (3057665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.81/4.86 % (3057665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.31/5.43 % (3057665)CaDiCaL version: 2.1.3 % 33.31/5.43 % (3057665)Termination reason: Instruction limit % 33.31/5.43 % (3057665)Termination phase: Saturation % 33.31/5.43 % (3057665)Time elapsed: 0.186 s % 33.31/5.43 % (3057665)Peak memory usage: 117 MB % 33.31/5.43 % (3057665)Instructions burned: 236 (million) % 33.31/5.43 % (3057673)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=3445504926:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi) % 33.31/5.43 % (3057672)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=604789173:i=4428:doe=on:fsr=off:rtra=on_2967 on theBenchmark for (2967ds/4428Mi) % 33.31/5.43 % (3057674)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2319447891:i=1052:rtra=on_2967 on theBenchmark for (2967ds/1052Mi) % 33.31/5.43 % (3057677)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3521848568:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2967 on theBenchmark for (2967ds/655Mi) % 33.31/5.43 % (3057669)Instruction limit reached! % 33.31/5.43 % (3057669)------------------------------ % 33.31/5.43 % (3057669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.31/5.43 % (3057669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.31/5.43 % (3057669)CaDiCaL version: 2.1.3 % 33.31/5.43 % (3057669)Termination reason: Instruction limit % 33.31/5.43 % (3057669)Termination phase: Saturation % 33.31/5.43 % (3057669)Time elapsed: 0.199 s % 33.31/5.43 % (3057669)Peak memory usage: 93 MB % 33.31/5.43 % (3057669)Instructions burned: 274 (million) % 33.31/5.43 % (3057678)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1239888086:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2966 on theBenchmark for (2966ds/1054Mi) % 33.31/5.43 % (3057673)Instruction limit reached! % 33.31/5.43 % (3057673)------------------------------ % 33.31/5.43 % (3057673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.31/5.43 % (3057673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.31/5.43 % (3057673)CaDiCaL version: 2.1.3 % 33.31/5.43 % (3057673)Termination reason: Instruction limit % 33.31/5.43 % (3057673)Termination phase: Saturation % 33.31/5.43 % (3057673)Time elapsed: 0.123 s % 33.31/5.43 % (3057673)Peak memory usage: 135 MB % 33.31/5.43 % (3057673)Instructions burned: 277 (million) % 33.31/5.43 % (3057679)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3564226808:i=107:rtra=on_2966 on theBenchmark for (2966ds/107Mi) % 33.31/5.43 % (3057679)Refutation not found, incomplete strategy % 33.31/5.43 % (3057679)------------------------------ % 33.31/5.43 % (3057679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.31/5.43 % (3057679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.31/5.43 % (3057679)CaDiCaL version: 2.1.3 % 33.31/5.43 % (3057679)Termination reason: Refutation not found, incomplete strategy % 33.31/5.43 % (3057679)Time elapsed: 0.043 s % 33.31/5.43 % (3057679)Peak memory usage: 116 MB % 33.31/5.43 % (3057679)Instructions burned: 28 (million) % 33.31/5.43 % (3057684)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2304844405:s2a=on:i=450:doe=on:nm=32:rtra=on_2965 on theBenchmark for (2965ds/450Mi) % 33.31/5.43 % (3057687)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 % 33.31/5.43 % (3057687)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4018121898:i=1090:aac=none:nm=0:rtra=on:rawr=on_2964 on theBenchmark for (2964ds/1090Mi) % 33.31/5.43 % (3057677)Instruction limit reached! % 33.31/5.43 % (3057677)------------------------------ % 33.31/5.43 % (3057677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.31/5.43 % (3057677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.31/5.43 % (3057677)CaDiCaL version: 2.1.3 % 33.31/5.43 % (3057677)Termination reason: Instruction limit % 33.31/5.43 % (3057677)Termination phase: Saturation % 33.31/5.43 % (3057677)Time elapsed: 0.354 s % 33.31/5.43 % (3057677)Peak memory usage: 93 MB % 33.31/5.43 % (3057677)Instructions burned: 656 (million) % 33.31/5.43 % (3057679)------------------------------ % 35.22/5.76 % (3057679)------------------------------ % 35.22/5.76 % (3057687)Instruction limit reached! % 35.22/5.76 % (3057687)------------------------------ % 35.22/5.76 % (3057687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.22/5.76 % (3057687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.22/5.76 % (3057687)CaDiCaL version: 2.1.3 % 35.22/5.76 % (3057687)Termination reason: Instruction limit % 35.22/5.76 % (3057687)Termination phase: Saturation % 35.22/5.76 % (3057687)Time elapsed: 0.239 s % 35.22/5.76 % (3057687)Peak memory usage: 115 MB % 35.22/5.76 % (3057687)Instructions burned: 1094 (million) % 35.22/5.76 % (3057690)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1216250674:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2962 on theBenchmark for (2962ds/130Mi) % 35.22/5.76 % (3057684)Instruction limit reached! % 35.22/5.76 % (3057684)------------------------------ % 35.22/5.76 % (3057684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.22/5.76 % (3057684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.22/5.76 % (3057684)CaDiCaL version: 2.1.3 % 35.22/5.76 % (3057684)Termination reason: Instruction limit % 35.22/5.76 % (3057684)Termination phase: Saturation % 35.22/5.76 % (3057684)Time elapsed: 0.333 s % 35.22/5.76 % (3057684)Peak memory usage: 136 MB % 35.22/5.76 % (3057684)Instructions burned: 450 (million) % 35.22/5.76 % (3057691)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1738604213:i=312:kws=inv_frequency:nm=20:rtra=on_2962 on theBenchmark for (2962ds/312Mi) % 35.22/5.76 % (3057690)Instruction limit reached! % 35.22/5.76 % (3057690)------------------------------ % 35.22/5.76 % (3057690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.22/5.76 % (3057690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.22/5.76 % (3057690)CaDiCaL version: 2.1.3 % 35.22/5.76 % (3057690)Termination reason: Instruction limit % 35.22/5.76 % (3057690)Termination phase: Property scanning % 35.22/5.76 % (3057690)Time elapsed: 0.050 s % 35.22/5.76 % (3057690)Peak memory usage: 87 MB % 35.22/5.76 % (3057690)Instructions burned: 132 (million) % 35.22/5.76 % (3057692)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3838319922:i=491:doe=on:rtra=on:gtg=position_2961 on theBenchmark for (2961ds/491Mi) % 35.22/5.76 % (3057695)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2229723168:s2a=on:i=835:s2at=2:rtra=on_2960 on theBenchmark for (2960ds/835Mi) % 35.22/5.76 % (3057674)Instruction limit reached! % 35.22/5.76 % (3057674)------------------------------ % 35.22/5.76 % (3057674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.22/5.76 % (3057674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.22/5.76 % (3057674)CaDiCaL version: 2.1.3 % 35.22/5.76 % (3057674)Termination reason: Instruction limit % 35.22/5.76 % (3057674)Termination phase: Saturation % 35.22/5.76 % (3057674)Time elapsed: 0.706 s % 35.22/5.76 % (3057674)Peak memory usage: 95 MB % 35.22/5.76 % (3057674)Instructions burned: 1054 (million) % 35.22/5.76 % (3057696)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=4000112096:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2960 on theBenchmark for (2960ds/307Mi) % 35.22/5.76 % (3057692)Instruction limit reached! % 35.22/5.76 % (3057692)------------------------------ % 35.22/5.76 % (3057692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.22/5.76 % (3057692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.22/5.76 % (3057692)CaDiCaL version: 2.1.3 % 35.22/5.76 % (3057692)Termination reason: Instruction limit % 35.22/5.76 % (3057692)Termination phase: Saturation % 35.22/5.76 % (3057692)Time elapsed: 0.168 s % 35.22/5.76 % (3057692)Peak memory usage: 93 MB % 35.22/5.76 % (3057692)Instructions burned: 492 (million) % 35.22/5.76 % (3057678)Instruction limit reached! % 35.22/5.76 % (3057678)------------------------------ % 35.22/5.76 % (3057678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.22/5.76 % (3057678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.22/5.76 % (3057678)CaDiCaL version: 2.1.3 % 35.22/5.76 % (3057678)Termination reason: Instruction limit % 35.22/5.76 % (3057678)Termination phase: Saturation % 35.22/5.76 % (3057678)Time elapsed: 0.679 s % 35.22/5.76 % (3057678)Peak memory usage: 94 MB % 35.22/5.76 % (3057678)Instructions burned: 1055 (million) % 35.22/5.76 % (3057691)Instruction limit reached! % 35.22/5.76 % (3057691)------------------------------ % 41.48/6.70 % (3057691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.48/6.70 % (3057691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.48/6.70 % (3057691)CaDiCaL version: 2.1.3 % 41.48/6.70 % (3057691)Termination reason: Instruction limit % 41.48/6.70 % (3057691)Termination phase: Saturation % 41.48/6.70 % (3057691)Time elapsed: 0.230 s % 41.48/6.70 % (3057691)Peak memory usage: 118 MB % 41.48/6.70 % (3057691)Instructions burned: 314 (million) % 41.48/6.70 % (3057699)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3435457298:i=776:doe=on:rtra=on_2958 on theBenchmark for (2958ds/776Mi) % 41.48/6.70 % (3057701)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2030876008:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2958 on theBenchmark for (2958ds/646Mi) % 41.48/6.70 % (3057702)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=3048474769:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2958 on theBenchmark for (2958ds/784Mi) % 41.48/6.70 % (3057696)Instruction limit reached! % 41.48/6.70 % (3057696)------------------------------ % 41.48/6.70 % (3057696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.48/6.70 % (3057696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.48/6.70 % (3057696)CaDiCaL version: 2.1.3 % 41.48/6.70 % (3057696)Termination reason: Instruction limit % 41.48/6.70 % (3057696)Termination phase: Saturation % 41.48/6.70 % (3057696)Time elapsed: 0.210 s % 41.48/6.70 % (3057696)Peak memory usage: 92 MB % 41.48/6.70 % (3057696)Instructions burned: 307 (million) % 41.48/6.70 % (3057703)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=1167404602:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2958 on theBenchmark for (2958ds/1131Mi) % 41.48/6.70 % (3057707)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=2569105814:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2956 on theBenchmark for (2956ds/246Mi) % 41.48/6.70 % (3057701)Instruction limit reached! % 41.48/6.70 % (3057701)------------------------------ % 41.48/6.70 % (3057701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.48/6.70 % (3057701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.48/6.70 % (3057701)CaDiCaL version: 2.1.3 % 41.48/6.70 % (3057701)Termination reason: Instruction limit % 41.48/6.70 % (3057701)Termination phase: Saturation % 41.48/6.70 % (3057701)Time elapsed: 0.245 s % 41.48/6.70 % (3057701)Peak memory usage: 141 MB % 41.48/6.70 % (3057701)Instructions burned: 649 (million) % 41.48/6.70 % (3057695)Instruction limit reached! % 41.48/6.70 % (3057695)------------------------------ % 41.48/6.70 % (3057695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.48/6.70 % (3057695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.48/6.70 % (3057695)CaDiCaL version: 2.1.3 % 41.48/6.70 % (3057695)Termination reason: Instruction limit % 41.48/6.70 % (3057695)Termination phase: Saturation % 41.48/6.70 % (3057695)Time elapsed: 0.441 s % 41.48/6.70 % (3057695)Peak memory usage: 94 MB % 41.48/6.70 % (3057695)Instructions burned: 836 (million) % 41.48/6.70 % (3057710)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1062103546:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2954 on theBenchmark for (2954ds/775Mi) % 41.48/6.70 % (3057707)Instruction limit reached! % 41.48/6.70 % (3057707)------------------------------ % 41.48/6.70 % (3057707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.48/6.70 % (3057707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.48/6.70 % (3057707)CaDiCaL version: 2.1.3 % 41.48/6.70 % (3057707)Termination reason: Instruction limit % 41.48/6.70 % (3057707)Termination phase: Saturation % 41.48/6.70 % (3057707)Time elapsed: 0.189 s % 41.48/6.70 % (3057707)Peak memory usage: 118 MB % 41.48/6.70 % (3057707)Instructions burned: 246 (million) % 41.48/6.70 % (3057711)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=74076296:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2954 on theBenchmark for (2954ds/273Mi) % 41.48/6.70 % (3057699)Instruction limit reached! % 41.48/6.70 % (3057699)------------------------------ % 53.04/8.17 % (3057699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.04/8.17 % (3057699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.04/8.17 % (3057699)CaDiCaL version: 2.1.3 % 53.04/8.17 % (3057699)Termination reason: Instruction limit % 53.04/8.17 % (3057699)Termination phase: Saturation % 53.04/8.17 % (3057699)Time elapsed: 0.504 s % 53.04/8.17 % (3057699)Peak memory usage: 124 MB % 53.04/8.17 % (3057699)Instructions burned: 776 (million) % 53.04/8.17 % (3057713)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=78618088:i=102:nm=16:rtra=on_2953 on theBenchmark for (2953ds/102Mi) % 53.04/8.17 % (3057713)Instruction limit reached! % 53.04/8.17 % (3057713)------------------------------ % 53.04/8.17 % (3057713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.04/8.17 % (3057713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.04/8.17 % (3057713)CaDiCaL version: 2.1.3 % 53.04/8.17 % (3057713)Termination reason: Instruction limit % 53.04/8.17 % (3057713)Termination phase: Saturation % 53.04/8.17 % (3057713)Time elapsed: 0.065 s % 53.04/8.17 % (3057713)Peak memory usage: 89 MB % 53.04/8.17 % (3057713)Instructions burned: 103 (million) % 53.04/8.17 % (3057711)Instruction limit reached! % 53.04/8.17 % (3057711)------------------------------ % 53.04/8.17 % (3057711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.04/8.17 % (3057711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.04/8.17 % (3057711)CaDiCaL version: 2.1.3 % 53.04/8.17 % (3057711)Termination reason: Instruction limit % 53.04/8.17 % (3057711)Termination phase: Saturation % 53.04/8.17 % (3057711)Time elapsed: 0.199 s % 53.04/8.17 % (3057711)Peak memory usage: 93 MB % 53.04/8.17 % (3057711)Instructions burned: 274 (million) % 53.04/8.17 % (3057710)Instruction limit reached! % 53.04/8.17 % (3057710)------------------------------ % 53.04/8.17 % (3057710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.04/8.17 % (3057710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.04/8.17 % (3057710)CaDiCaL version: 2.1.3 % 53.04/8.17 % (3057710)Termination reason: Instruction limit % 53.04/8.17 % (3057710)Termination phase: Saturation % 53.04/8.17 % (3057710)Time elapsed: 0.292 s % 53.04/8.17 % (3057710)Peak memory usage: 95 MB % 53.04/8.17 % (3057710)Instructions burned: 776 (million) % 53.04/8.17 % (3057702)Instruction limit reached! % 53.04/8.17 % (3057702)------------------------------ % 53.04/8.17 % (3057702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.04/8.17 % (3057702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.04/8.17 % (3057702)CaDiCaL version: 2.1.3 % 53.04/8.17 % (3057702)Termination reason: Instruction limit % 53.04/8.17 % (3057702)Termination phase: Saturation % 53.04/8.17 % (3057702)Time elapsed: 0.610 s % 53.04/8.17 % (3057702)Peak memory usage: 125 MB % 53.04/8.17 % (3057702)Instructions burned: 784 (million) % 53.04/8.17 % (3057715)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2318412266:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2952 on theBenchmark for (2952ds/1094Mi) % 53.04/8.17 % (3057719)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=877338830:i=1846:canc=cautious:fsr=off:rtra=on_2950 on theBenchmark for (2950ds/1846Mi) % 53.04/8.17 % (3057717)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1783500402:i=6400:doe=on:fsr=off:rtra=on_2950 on theBenchmark for (2950ds/6400Mi) % 53.04/8.17 % (3057718)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=4119165739:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2950 on theBenchmark for (2950ds/868Mi) % 53.04/8.17 % (3057703)Instruction limit reached! % 53.04/8.17 % (3057703)------------------------------ % 53.04/8.17 % (3057703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.04/8.17 % (3057703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.04/8.17 % (3057703)CaDiCaL version: 2.1.3 % 53.04/8.17 % (3057703)Termination reason: Instruction limit % 53.04/8.17 % (3057703)Termination phase: Saturation % 53.04/8.17 % (3057703)Time elapsed: 0.735 s % 53.04/8.17 % (3057703)Peak memory usage: 124 MB % 53.04/8.17 % (3057703)Instructions burned: 1132 (million) % 53.04/8.17 % (3057721)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2209181027:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2950 on theBenchmark for (2950ds/36816Mi) % 62.89/9.67 % (3057726)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3900455940:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2949 on theBenchmark for (2949ds/273Mi) % 62.89/9.67 % (3057726)Instruction limit reached! % 62.89/9.67 % (3057726)------------------------------ % 62.89/9.67 % (3057726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.89/9.67 % (3057726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.89/9.67 % (3057726)CaDiCaL version: 2.1.3 % 62.89/9.67 % (3057726)Termination reason: Instruction limit % 62.89/9.67 % (3057726)Termination phase: Saturation % 62.89/9.67 % (3057726)Time elapsed: 0.198 s % 62.89/9.67 % (3057726)Peak memory usage: 92 MB % 62.89/9.67 % (3057726)Instructions burned: 273 (million) % 62.89/9.67 % (3057718)Instruction limit reached! % 62.89/9.67 % (3057718)------------------------------ % 62.89/9.67 % (3057718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.89/9.67 % (3057718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.89/9.67 % (3057718)CaDiCaL version: 2.1.3 % 62.89/9.67 % (3057718)Termination reason: Instruction limit % 62.89/9.67 % (3057718)Termination phase: Saturation % 62.89/9.67 % (3057718)Time elapsed: 0.366 s % 62.89/9.67 % (3057718)Peak memory usage: 117 MB % 62.89/9.67 % (3057718)Instructions burned: 870 (million) % 62.89/9.67 % (3057729)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=69873616:i=5811:kws=precedence:nm=0:rtra=on_2945 on theBenchmark for (2945ds/5811Mi) % 62.89/9.67 % (3057728)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=1147648195:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2945 on theBenchmark for (2945ds/863Mi) % 62.89/9.67 % (3057715)Instruction limit reached! % 62.89/9.67 % (3057715)------------------------------ % 62.89/9.67 % (3057715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.89/9.67 % (3057715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.89/9.67 % (3057715)CaDiCaL version: 2.1.3 % 62.89/9.67 % (3057715)Termination reason: Instruction limit % 62.89/9.67 % (3057715)Termination phase: Saturation % 62.89/9.67 % (3057715)Time elapsed: 0.669 s % 62.89/9.67 % (3057715)Peak memory usage: 95 MB % 62.89/9.67 % (3057715)Instructions burned: 1094 (million) % 62.89/9.67 % (3057719)Instruction limit reached! % 62.89/9.67 % (3057719)------------------------------ % 62.89/9.67 % (3057719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.89/9.67 % (3057719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.89/9.67 % (3057719)CaDiCaL version: 2.1.3 % 62.89/9.67 % (3057719)Termination reason: Instruction limit % 62.89/9.67 % (3057719)Termination phase: Saturation % 62.89/9.67 % (3057719)Time elapsed: 0.586 s % 62.89/9.67 % (3057719)Peak memory usage: 99 MB % 62.89/9.67 % (3057719)Instructions burned: 1846 (million) % 62.89/9.67 % (3057733)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1090798676:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2943 on theBenchmark for (2943ds/801Mi) % 62.89/9.67 % (3057732)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=4080155924:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2944 on theBenchmark for (2944ds/2216Mi) % 62.89/9.67 % (3057728)Instruction limit reached! % 62.89/9.67 % (3057728)------------------------------ % 62.89/9.67 % (3057728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.89/9.67 % (3057728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.89/9.67 % (3057728)CaDiCaL version: 2.1.3 % 62.89/9.67 % (3057728)Termination reason: Instruction limit % 62.89/9.67 % (3057728)Termination phase: Saturation % 62.89/9.67 % (3057728)Time elapsed: 0.360 s % 62.89/9.67 % (3057728)Peak memory usage: 117 MB % 62.89/9.67 % (3057728)Instructions burned: 864 (million) % 62.89/9.67 % (3057733)Instruction limit reached! % 62.89/9.67 % (3057733)------------------------------ % 62.89/9.67 % (3057733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.89/9.67 % (3057733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.89/9.67 % (3057733)CaDiCaL version: 2.1.3 % 62.89/9.67 % (3057733)Termination reason: Instruction limit % 99.29/14.76 % (3057733)Termination phase: Saturation % 99.29/14.76 % (3057733)Time elapsed: 0.300 s % 99.29/14.76 % (3057733)Peak memory usage: 97 MB % 99.29/14.76 % (3057733)Instructions burned: 801 (million) % 99.29/14.76 % (3057736)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3158726316:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2940 on theBenchmark for (2940ds/1026Mi) % 99.29/14.76 % (3057672)Instruction limit reached! % 99.29/14.76 % (3057672)------------------------------ % 99.29/14.76 % (3057672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.29/14.76 % (3057672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.29/14.76 % (3057672)CaDiCaL version: 2.1.3 % 99.29/14.76 % (3057672)Termination reason: Instruction limit % 99.29/14.76 % (3057672)Termination phase: Saturation % 99.29/14.76 % (3057672)Time elapsed: 2.725 s % 99.29/14.76 % (3057672)Peak memory usage: 115 MB % 99.29/14.76 % (3057672)Instructions burned: 4428 (million) % 99.29/14.76 % (3057737)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2563272437:i=3509:rtra=on_2939 on theBenchmark for (2939ds/3509Mi) % 99.29/14.76 % (3057739)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=826498266:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2938 on theBenchmark for (2938ds/2127Mi) % 99.29/14.76 % (3057736)Instruction limit reached! % 99.29/14.76 % (3057736)------------------------------ % 99.29/14.76 % (3057736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.29/14.76 % (3057736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.29/14.76 % (3057736)CaDiCaL version: 2.1.3 % 99.29/14.76 % (3057736)Termination reason: Instruction limit % 99.29/14.76 % (3057736)Termination phase: Saturation % 99.29/14.76 % (3057736)Time elapsed: 0.668 s % 99.29/14.76 % (3057736)Peak memory usage: 94 MB % 99.29/14.76 % (3057736)Instructions burned: 1028 (million) % 99.29/14.76 % (3057742)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2971724735:i=1959:rtra=on:fsd=on:proc=on_2932 on theBenchmark for (2932ds/1959Mi) % 99.29/14.76 % (3057732)Instruction limit reached! % 99.29/14.76 % (3057732)------------------------------ % 99.29/14.76 % (3057732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.29/14.76 % (3057732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.29/14.76 % (3057732)CaDiCaL version: 2.1.3 % 99.29/14.76 % (3057732)Termination reason: Instruction limit % 99.29/14.76 % (3057732)Termination phase: Saturation % 99.29/14.76 % (3057732)Time elapsed: 1.297 s % 99.29/14.76 % (3057732)Peak memory usage: 128 MB % 99.29/14.76 % (3057732)Instructions burned: 2217 (million) % 99.29/14.76 % (3057744)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2852770999:s2a=on:i=3553:nm=0:rtra=on_2929 on theBenchmark for (2929ds/3553Mi) % 99.29/14.76 % (3057739)Instruction limit reached! % 99.29/14.76 % (3057739)------------------------------ % 99.29/14.76 % (3057739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.29/14.76 % (3057739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.29/14.76 % (3057739)CaDiCaL version: 2.1.3 % 99.29/14.76 % (3057739)Termination reason: Instruction limit % 99.29/14.76 % (3057739)Termination phase: Saturation % 99.29/14.76 % (3057739)Time elapsed: 1.003 s % 99.29/14.76 % (3057739)Peak memory usage: 102 MB % 99.29/14.76 % (3057739)Instructions burned: 2129 (million) % 99.29/14.76 % (3057737)Instruction limit reached! % 99.29/14.76 % (3057737)------------------------------ % 99.29/14.76 % (3057737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.29/14.76 % (3057737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.29/14.76 % (3057737)CaDiCaL version: 2.1.3 % 99.29/14.76 % (3057737)Termination reason: Instruction limit % 99.29/14.76 % (3057737)Termination phase: Saturation % 99.29/14.76 % (3057737)Time elapsed: 1.229 s % 99.29/14.76 % (3057737)Peak memory usage: 109 MB % 99.29/14.76 % (3057737)Instructions burned: 3512 (million) % 99.29/14.76 % (3057746)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3121335214:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2927 on theBenchmark for (2927ds/3201Mi) % 99.29/14.76 % (3057747)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=1165150053:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2926 on theBenchmark for (2926ds/4093Mi) % 121.71/17.92 % (3057742)Instruction limit reached! % 121.71/17.92 % (3057742)------------------------------ % 121.71/17.92 % (3057742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.71/17.92 % (3057742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.71/17.92 % (3057742)CaDiCaL version: 2.1.3 % 121.71/17.92 % (3057742)Termination reason: Instruction limit % 121.71/17.92 % (3057742)Termination phase: Saturation % 121.71/17.92 % (3057742)Time elapsed: 1.155 s % 121.71/17.92 % (3057742)Peak memory usage: 125 MB % 121.71/17.92 % (3057742)Instructions burned: 1959 (million) % 121.71/17.92 % (3057750)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=281165838:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2919 on theBenchmark for (2919ds/21173Mi) % 121.71/17.92 % (3057729)Instruction limit reached! % 121.71/17.92 % (3057729)------------------------------ % 121.71/17.92 % (3057729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.71/17.92 % (3057729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.71/17.92 % (3057729)CaDiCaL version: 2.1.3 % 121.71/17.92 % (3057729)Termination reason: Instruction limit % 121.71/17.92 % (3057729)Termination phase: Saturation % 121.71/17.92 % (3057729)Time elapsed: 2.965 s % 121.71/17.92 % (3057729)Peak memory usage: 141 MB % 121.71/17.92 % (3057729)Instructions burned: 5812 (million) % 121.71/17.92 % (3057752)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=544101544:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2914 on theBenchmark for (2914ds/10544Mi) % 121.71/17.92 % (3057747)Instruction limit reached! % 121.71/17.92 % (3057747)------------------------------ % 121.71/17.92 % (3057747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.71/17.92 % (3057747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.71/17.92 % (3057747)CaDiCaL version: 2.1.3 % 121.71/17.92 % (3057747)Termination reason: Instruction limit % 121.71/17.92 % (3057747)Termination phase: Saturation % 121.71/17.92 % (3057747)Time elapsed: 1.335 s % 121.71/17.92 % (3057747)Peak memory usage: 145 MB % 121.71/17.92 % (3057747)Instructions burned: 4097 (million) % 121.71/17.92 % (3057746)Instruction limit reached! % 121.71/17.92 % (3057746)------------------------------ % 121.71/17.92 % (3057746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.71/17.92 % (3057746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.71/17.92 % (3057746)CaDiCaL version: 2.1.3 % 121.71/17.92 % (3057746)Termination reason: Instruction limit % 121.71/17.92 % (3057746)Termination phase: Saturation % 121.71/17.92 % (3057746)Time elapsed: 1.401 s % 121.71/17.92 % (3057746)Peak memory usage: 94 MB % 121.71/17.92 % (3057746)Instructions burned: 3202 (million) % 121.71/17.92 % (3057717)Instruction limit reached! % 121.71/17.92 % (3057717)------------------------------ % 121.71/17.92 % (3057717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.71/17.92 % (3057717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.71/17.92 % (3057717)CaDiCaL version: 2.1.3 % 121.71/17.92 % (3057717)Termination reason: Instruction limit % 121.71/17.92 % (3057717)Termination phase: Saturation % 121.71/17.92 % (3057717)Time elapsed: 3.817 s % 121.71/17.92 % (3057717)Peak memory usage: 124 MB % 121.71/17.92 % (3057717)Instructions burned: 6401 (million) % 121.71/17.92 % (3057744)Instruction limit reached! % 121.71/17.92 % (3057744)------------------------------ % 121.71/17.92 % (3057744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.71/17.92 % (3057744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.71/17.92 % (3057744)CaDiCaL version: 2.1.3 % 121.71/17.92 % (3057744)Termination reason: Instruction limit % 121.71/17.92 % (3057744)Termination phase: Saturation % 121.71/17.92 % (3057744)Time elapsed: 1.649 s % 121.71/17.92 % (3057744)Peak memory usage: 106 MB % 121.71/17.92 % (3057744)Instructions burned: 3555 (million) % 121.71/17.92 % (3057755)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=132167618:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/775Mi) % 121.71/17.92 % (3057754)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2975325095:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2911 on theBenchmark for (2911ds/1262Mi) % 121.71/17.92 % (3057756)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1349813378:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2911 on theBenchmark for (2911ds/270Mi) % 139.33/20.37 % (3057757)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2528405531:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2911 on theBenchmark for (2911ds/17165Mi) % 139.33/20.37 % (3057756)Instruction limit reached! % 139.33/20.37 % (3057756)------------------------------ % 139.33/20.37 % (3057756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.33/20.37 % (3057756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.33/20.37 % (3057756)CaDiCaL version: 2.1.3 % 139.33/20.37 % (3057756)Termination reason: Instruction limit % 139.33/20.37 % (3057756)Termination phase: Saturation % 139.33/20.37 % (3057756)Time elapsed: 0.191 s % 139.33/20.37 % (3057756)Peak memory usage: 93 MB % 139.33/20.37 % (3057756)Instructions burned: 271 (million) % 139.33/20.37 % (3057755)Instruction limit reached! % 139.33/20.37 % (3057755)------------------------------ % 139.33/20.37 % (3057755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.33/20.37 % (3057755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.33/20.37 % (3057755)CaDiCaL version: 2.1.3 % 139.33/20.37 % (3057755)Termination reason: Instruction limit % 139.33/20.37 % (3057755)Termination phase: Saturation % 139.33/20.37 % (3057755)Time elapsed: 0.289 s % 139.33/20.37 % (3057755)Peak memory usage: 95 MB % 139.33/20.37 % (3057755)Instructions burned: 777 (million) % 139.33/20.37 % (3057763)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=187905340:st=2:i=12633:rtra=on:ss=axioms_2907 on theBenchmark for (2907ds/12633Mi) % 139.33/20.37 % (3057762)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1458427551:s2a=on:i=13094:s2at=-1:rtra=on_2908 on theBenchmark for (2908ds/13094Mi) % 139.33/20.37 % (3057754)Instruction limit reached! % 139.33/20.37 % (3057754)------------------------------ % 139.33/20.37 % (3057754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.33/20.37 % (3057754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.33/20.37 % (3057754)CaDiCaL version: 2.1.3 % 139.33/20.37 % (3057754)Termination reason: Instruction limit % 139.33/20.37 % (3057754)Termination phase: Saturation % 139.33/20.37 % (3057754)Time elapsed: 0.670 s % 139.33/20.37 % (3057754)Peak memory usage: 120 MB % 139.33/20.37 % (3057754)Instructions burned: 1263 (million) % 139.33/20.37 % (3057766)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=320820265:i=1783:rtra=on:gtg=position_2903 on theBenchmark for (2903ds/1783Mi) % 139.33/20.37 % (3057766)Instruction limit reached! % 139.33/20.37 % (3057766)------------------------------ % 139.33/20.37 % (3057766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.33/20.37 % (3057766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.33/20.37 % (3057766)CaDiCaL version: 2.1.3 % 139.33/20.37 % (3057766)Termination reason: Instruction limit % 139.33/20.37 % (3057766)Termination phase: Saturation % 139.33/20.37 % (3057766)Time elapsed: 1.064 s % 139.33/20.37 % (3057766)Peak memory usage: 122 MB % 139.33/20.37 % (3057766)Instructions burned: 1784 (million) % 139.33/20.37 % (3057768)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=3380708632:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2891 on theBenchmark for (2891ds/5451Mi) % 139.33/20.37 % (3057768)Instruction limit reached! % 139.33/20.37 % (3057768)------------------------------ % 139.33/20.37 % (3057768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.33/20.37 % (3057768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.33/20.37 % (3057768)CaDiCaL version: 2.1.3 % 139.33/20.37 % (3057768)Termination reason: Instruction limit % 139.33/20.37 % (3057768)Termination phase: Saturation % 139.33/20.37 % (3057768)Time elapsed: 2.581 s % 139.33/20.37 % (3057768)Peak memory usage: 139 MB % 139.33/20.37 % (3057768)Instructions burned: 5452 (million) % 139.33/20.37 % (3057903)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=3867657221:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2863 on theBenchmark for (2863ds/4975Mi) % 139.33/20.37 % (3057763)Instruction limit reached! % 139.33/20.37 % (3057763)------------------------------ % 139.33/20.37 % (3057763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.33/20.37 % (3057763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.82/24.11 % (3057763)CaDiCaL version: 2.1.3 % 165.82/24.11 % (3057763)Termination reason: Instruction limit % 165.82/24.11 % (3057763)Termination phase: Saturation % 165.82/24.11 % (3057763)Time elapsed: 4.740 s % 165.82/24.11 % (3057763)Peak memory usage: 142 MB % 165.82/24.11 % (3057763)Instructions burned: 12634 (million) % 165.82/24.11 % (3058020)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=1922349368:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2859 on theBenchmark for (2859ds/2076Mi) % 165.82/24.11 % (3058020)Instruction limit reached! % 165.82/24.11 % (3058020)------------------------------ % 165.82/24.11 % (3058020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.82/24.11 % (3058020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.82/24.11 % (3058020)CaDiCaL version: 2.1.3 % 165.82/24.11 % (3058020)Termination reason: Instruction limit % 165.82/24.11 % (3058020)Termination phase: Saturation % 165.82/24.11 % (3058020)Time elapsed: 0.662 s % 165.82/24.11 % (3058020)Peak memory usage: 130 MB % 165.82/24.11 % (3058020)Instructions burned: 2079 (million) % 165.82/24.11 % (3058117)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2231825039:i=5145:rtra=on_2851 on theBenchmark for (2851ds/5145Mi) % 165.82/24.11 % (3057752)Instruction limit reached! % 165.82/24.11 % (3057752)------------------------------ % 165.82/24.11 % (3057752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.82/24.11 % (3057752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.82/24.11 % (3057752)CaDiCaL version: 2.1.3 % 165.82/24.11 % (3057752)Termination reason: Instruction limit % 165.82/24.11 % (3057752)Termination phase: Saturation % 165.82/24.11 % (3057752)Time elapsed: 6.770 s % 165.82/24.11 % (3057752)Peak memory usage: 173 MB % 165.82/24.11 % (3057752)Instructions burned: 10545 (million) % 165.82/24.11 % (3058119)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2693844763:i=3509:rtra=on_2845 on theBenchmark for (2845ds/3509Mi) % 165.82/24.11 % (3057903)Instruction limit reached! % 165.82/24.11 % (3057903)------------------------------ % 165.82/24.11 % (3057903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.82/24.11 % (3057903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.82/24.11 % (3057903)CaDiCaL version: 2.1.3 % 165.82/24.11 % (3057903)Termination reason: Instruction limit % 165.82/24.11 % (3057903)Termination phase: Saturation % 165.82/24.11 % (3057903)Time elapsed: 2.429 s % 165.82/24.11 % (3057903)Peak memory usage: 139 MB % 165.82/24.11 % (3057903)Instructions burned: 4975 (million) % 165.82/24.11 % (3058121)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3555111180:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2838 on theBenchmark for (2838ds/13800Mi) % 165.82/24.11 % (3058117)Instruction limit reached! % 165.82/24.11 % (3058117)------------------------------ % 165.82/24.11 % (3058117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.82/24.11 % (3058117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.82/24.11 % (3058117)CaDiCaL version: 2.1.3 % 165.82/24.11 % (3058117)Termination reason: Instruction limit % 165.82/24.11 % (3058117)Termination phase: Saturation % 165.82/24.11 % (3058117)Time elapsed: 1.777 s % 165.82/24.11 % (3058117)Peak memory usage: 112 MB % 165.82/24.11 % (3058117)Instructions burned: 5148 (million) % 165.82/24.11 % (3058123)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2331229706:i=1412:rtra=on:fsd=on:proc=on_2832 on theBenchmark for (2832ds/1412Mi) % 165.82/24.11 % (3057762)Instruction limit reached! % 165.82/24.11 % (3057762)------------------------------ % 165.82/24.11 % (3057762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.82/24.11 % (3057762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.82/24.11 % (3057762)CaDiCaL version: 2.1.3 % 165.82/24.11 % (3057762)Termination reason: Instruction limit % 165.82/24.11 % (3057762)Termination phase: Saturation % 165.82/24.11 % (3057762)Time elapsed: 7.715 s % 165.82/24.11 % (3057762)Peak memory usage: 160 MB % 165.82/24.11 % (3057762)Instructions burned: 13095 (million) % 165.82/24.11 % (3058125)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 % 165.82/24.11 % (3058125)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1035650915:i=11747:aac=none:nm=0:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/11747Mi) % 250.09/35.93 % (3058123)Instruction limit reached! % 250.09/35.93 % (3058123)------------------------------ % 250.09/35.93 % (3058123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.09/35.93 % (3058123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.09/35.93 % (3058123)CaDiCaL version: 2.1.3 % 250.09/35.93 % (3058123)Termination reason: Instruction limit % 250.09/35.93 % (3058123)Termination phase: Saturation % 250.09/35.93 % (3058123)Time elapsed: 0.462 s % 250.09/35.93 % (3058123)Peak memory usage: 122 MB % 250.09/35.93 % (3058123)Instructions burned: 1414 (million) % 250.09/35.93 % (3058127)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=514061405:s2a=on:i=3553:nm=0:rtra=on_2826 on theBenchmark for (2826ds/3553Mi) % 250.09/35.93 % (3058119)Instruction limit reached! % 250.09/35.93 % (3058119)------------------------------ % 250.09/35.93 % (3058119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.09/35.93 % (3058119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.09/35.93 % (3058119)CaDiCaL version: 2.1.3 % 250.09/35.93 % (3058119)Termination reason: Instruction limit % 250.09/35.93 % (3058119)Termination phase: Saturation % 250.09/35.93 % (3058119)Time elapsed: 2.342 s % 250.09/35.93 % (3058119)Peak memory usage: 107 MB % 250.09/35.93 % (3058119)Instructions burned: 3510 (million) % 250.09/35.93 % (3057750)Instruction limit reached! % 250.09/35.93 % (3057750)------------------------------ % 250.09/35.93 % (3057750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.09/35.93 % (3057750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.09/35.93 % (3057750)CaDiCaL version: 2.1.3 % 250.09/35.93 % (3057750)Termination reason: Instruction limit % 250.09/35.93 % (3057750)Termination phase: Saturation % 250.09/35.93 % (3057750)Time elapsed: 10.025 s % 250.09/35.93 % (3057750)Peak memory usage: 150 MB % 250.09/35.93 % (3057750)Instructions burned: 21173 (million) % 250.09/35.93 % (3058129)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3105921778:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/3201Mi) % 250.09/35.93 % (3058127)Instruction limit reached! % 250.09/35.93 % (3058127)------------------------------ % 250.09/35.93 % (3058127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.09/35.93 % (3058127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.09/35.93 % (3058127)CaDiCaL version: 2.1.3 % 250.09/35.93 % (3058127)Termination reason: Instruction limit % 250.09/35.93 % (3058127)Termination phase: Saturation % 250.09/35.93 % (3058127)Time elapsed: 0.833 s % 250.09/35.93 % (3058127)Peak memory usage: 103 MB % 250.09/35.93 % (3058127)Instructions burned: 3555 (million) % 250.09/35.93 % (3058131)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=910319918:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2817 on theBenchmark for (2817ds/4081Mi) % 250.09/35.93 % (3058132)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=3639614466:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2816 on theBenchmark for (2816ds/20260Mi) % 250.09/35.93 % (3057757)Instruction limit reached! % 250.09/35.93 % (3057757)------------------------------ % 250.09/35.93 % (3057757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.09/35.93 % (3057757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.09/35.93 % (3057757)CaDiCaL version: 2.1.3 % 250.09/35.93 % (3057757)Termination reason: Instruction limit % 250.09/35.93 % (3057757)Termination phase: Saturation % 250.09/35.93 % (3057757)Time elapsed: 9.710 s % 250.09/35.93 % (3057757)Peak memory usage: 214 MB % 250.09/35.93 % (3057757)Instructions burned: 17166 (million) % 250.09/35.93 % (3058135)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4162462686:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2812 on theBenchmark for (2812ds/58627Mi) % 250.09/35.93 % (3058129)Instruction limit reached! % 250.09/35.93 % (3058129)------------------------------ % 250.09/35.93 % (3058129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.09/35.93 % (3058129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.Terminated %------------------------------------------------------------------------------