%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW833_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:37:54 PM UTC 2026 % Result : Timeout 300.20s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW833_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.24 % Computer : n011.cluster.edu % 0.11/0.24 % Model : x86_64 x86_64 % 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.24 % Memory : 8046.5625MB % 0.11/0.24 % OS : Linux 6.8.0-71-generic % 0.11/0.24 % CPULimit : 300 % 0.11/0.24 % WCLimit : 300 % 0.11/0.24 % DateTime : Mon Sep 28 14:31:15 UTC 2026 % 0.11/0.25 % CPUTime : % 0.11/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.25/0.30 Running first-order theorem proving % 0.25/0.30 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.36/1.72 % (3429355)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.36/1.72 % (3429369)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=513313671:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.36/1.72 % (3429370)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2482211401:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.36/1.72 % (3429369)Instruction limit reached! % 5.36/1.72 % (3429369)------------------------------ % 5.36/1.72 % (3429369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.36/1.72 % (3429369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.72 % (3429369)CaDiCaL version: 2.1.3 % 5.36/1.72 % (3429369)Termination reason: Instruction limit % 5.36/1.72 % (3429369)Termination phase: Saturation % 5.36/1.72 % (3429369)Time elapsed: 0.042 s % 5.36/1.72 % (3429369)Peak memory usage: 116 MB % 5.36/1.72 % (3429369)Instructions burned: 46 (million) % 5.36/1.72 % (3429366)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=480579655:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.36/1.72 % (3429365)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=251834742:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.36/1.72 % (3429364)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3851517768:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.36/1.72 % (3429370)Instruction limit reached! % 5.36/1.72 % (3429370)------------------------------ % 5.36/1.72 % (3429370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.36/1.72 % (3429370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.72 % (3429370)CaDiCaL version: 2.1.3 % 5.36/1.72 % (3429370)Termination reason: Instruction limit % 5.36/1.72 % (3429370)Termination phase: Saturation % 5.36/1.72 % (3429370)Time elapsed: 0.058 s % 5.36/1.72 % (3429370)Peak memory usage: 110 MB % 5.36/1.72 % (3429370)Instructions burned: 33 (million) % 5.36/1.72 % (3429367)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1860718481:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.36/1.72 % (3429368)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3842042003:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.36/1.72 % (3429364)Instruction limit reached! % 5.36/1.72 % (3429364)------------------------------ % 5.36/1.72 % (3429364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.36/1.72 % (3429364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.72 % (3429364)CaDiCaL version: 2.1.3 % 5.36/1.72 % (3429364)Termination reason: Instruction limit % 5.36/1.72 % (3429364)Termination phase: Property scanning % 5.36/1.72 % (3429364)Time elapsed: 0.010 s % 5.36/1.72 % (3429364)Peak memory usage: 85 MB % 5.36/1.72 % (3429364)Instructions burned: 12 (million) % 5.36/1.72 % (3429367)Instruction limit reached! % 5.36/1.72 % (3429367)------------------------------ % 5.36/1.72 % (3429367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.36/1.72 % (3429367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.72 % (3429367)CaDiCaL version: 2.1.3 % 5.36/1.72 % (3429367)Termination reason: Instruction limit % 5.36/1.72 % (3429367)Termination phase: SInE selection % 5.36/1.72 % (3429367)Time elapsed: 0.005 s % 5.36/1.72 % (3429367)Peak memory usage: 86 MB % 5.36/1.72 % (3429367)Instructions burned: 9 (million) % 5.36/1.72 % (3429368)Instruction limit reached! % 5.36/1.72 % (3429368)------------------------------ % 5.36/1.72 % (3429368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.36/1.72 % (3429368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.72 % (3429368)CaDiCaL version: 2.1.3 % 5.36/1.72 % (3429368)Termination reason: Instruction limit % 5.36/1.72 % (3429368)Termination phase: Property scanning % 5.36/1.72 % (3429368)Time elapsed: 0.006 s % 5.36/1.72 % (3429368)Peak memory usage: 86 MB % 5.36/1.72 % (3429368)Instructions burned: 6 (million) % 5.36/1.72 % (3429373)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2937574325:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.36/1.72 % (3429373)Refutation not found, incomplete strategy % 5.36/1.72 % (3429373)------------------------------ % 8.58/2.08 % (3429373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.08 % (3429373)CaDiCaL version: 2.1.3 % 8.58/2.08 % (3429373)Termination reason: Refutation not found, incomplete strategy % 8.58/2.08 % (3429373)Time elapsed: 0.004 s % 8.58/2.08 % (3429373)Peak memory usage: 88 MB % 8.58/2.08 % (3429373)Instructions burned: 7 (million) % 8.58/2.08 % (3429380)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1791605601:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 8.58/2.08 % (3429380)Instruction limit reached! % 8.58/2.08 % (3429380)------------------------------ % 8.58/2.08 % (3429380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.08 % (3429380)CaDiCaL version: 2.1.3 % 8.58/2.08 % (3429380)Termination reason: Instruction limit % 8.58/2.08 % (3429380)Termination phase: Property scanning % 8.58/2.08 % (3429380)Time elapsed: 0.012 s % 8.58/2.08 % (3429380)Peak memory usage: 87 MB % 8.58/2.08 % (3429380)Instructions burned: 18 (million) % 8.58/2.08 % (3429366)Instruction limit reached! % 8.58/2.08 % (3429366)------------------------------ % 8.58/2.08 % (3429366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.08 % (3429366)CaDiCaL version: 2.1.3 % 8.58/2.08 % (3429366)Termination reason: Instruction limit % 8.58/2.08 % (3429366)Termination phase: Saturation % 8.58/2.08 % (3429366)Time elapsed: 0.215 s % 8.58/2.08 % (3429366)Peak memory usage: 118 MB % 8.58/2.08 % (3429366)Instructions burned: 201 (million) % 8.58/2.08 % (3429381)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2262819831:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 8.58/2.08 % (3429382)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=3330864882:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 8.58/2.08 % (3429379)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=4137521452:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 8.58/2.08 % (3429381)Instruction limit reached! % 8.58/2.08 % (3429381)------------------------------ % 8.58/2.08 % (3429381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.08 % (3429381)CaDiCaL version: 2.1.3 % 8.58/2.08 % (3429381)Termination reason: Instruction limit % 8.58/2.08 % (3429381)Termination phase: Property scanning % 8.58/2.08 % (3429381)Time elapsed: 0.023 s % 8.58/2.08 % (3429381)Peak memory usage: 87 MB % 8.58/2.08 % (3429381)Instructions burned: 24 (million) % 8.58/2.08 % (3429382)Instruction limit reached! % 8.58/2.08 % (3429382)------------------------------ % 8.58/2.08 % (3429382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.08 % (3429382)CaDiCaL version: 2.1.3 % 8.58/2.08 % (3429382)Termination reason: Instruction limit % 8.58/2.08 % (3429382)Termination phase: Property scanning % 8.58/2.08 % (3429382)Time elapsed: 0.025 s % 8.58/2.08 % (3429382)Peak memory usage: 87 MB % 8.58/2.08 % (3429382)Instructions burned: 27 (million) % 8.58/2.08 % (3429379)Instruction limit reached! % 8.58/2.08 % (3429379)------------------------------ % 8.58/2.08 % (3429379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.58/2.08 % (3429379)CaDiCaL version: 2.1.3 % 8.58/2.08 % (3429379)Termination reason: Instruction limit % 8.58/2.08 % (3429379)Termination phase: Saturation % 8.58/2.08 % (3429379)Time elapsed: 0.026 s % 8.58/2.08 % (3429379)Peak memory usage: 87 MB % 8.58/2.08 % (3429379)Instructions burned: 29 (million) % 8.58/2.08 % (3429365)Instruction limit reached! % 8.58/2.08 % (3429365)------------------------------ % 8.58/2.08 % (3429365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.58/2.08 % (3429365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.57/2.31 % (3429365)CaDiCaL version: 2.1.3 % 9.57/2.31 % (3429365)Termination reason: Instruction limit % 9.57/2.31 % (3429365)Termination phase: Saturation % 9.57/2.31 % (3429365)Time elapsed: 0.314 s % 9.57/2.31 % (3429365)Peak memory usage: 118 MB % 9.57/2.31 % (3429365)Instructions burned: 307 (million) % 9.57/2.31 % (3429373)------------------------------ % 9.57/2.31 % (3429373)------------------------------ % 9.57/2.31 % (3429385)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3689878360:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 9.57/2.31 % (3429386)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=164196357:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 9.57/2.31 % (3429386)Instruction limit reached! % 9.57/2.31 % (3429386)------------------------------ % 9.57/2.31 % (3429386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.57/2.31 % (3429386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.57/2.31 % (3429386)CaDiCaL version: 2.1.3 % 9.57/2.31 % (3429386)Termination reason: Instruction limit % 9.57/2.31 % (3429386)Termination phase: Property scanning % 9.57/2.31 % (3429386)Time elapsed: 0.003 s % 9.57/2.31 % (3429386)Peak memory usage: 85 MB % 9.57/2.31 % (3429386)Instructions burned: 3 (million) % 9.57/2.31 % (3429385)Instruction limit reached! % 9.57/2.31 % (3429385)------------------------------ % 9.57/2.31 % (3429385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.57/2.31 % (3429385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.57/2.31 % (3429385)CaDiCaL version: 2.1.3 % 9.57/2.31 % (3429385)Termination reason: Instruction limit % 9.57/2.31 % (3429385)Termination phase: Saturation % 9.57/2.31 % (3429385)Time elapsed: 0.082 s % 9.57/2.31 % (3429385)Peak memory usage: 90 MB % 9.57/2.31 % (3429385)Instructions burned: 85 (million) % 9.57/2.31 % (3429394)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=2404497034:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 9.57/2.31 % (3429394)Instruction limit reached! % 9.57/2.31 % (3429394)------------------------------ % 9.57/2.31 % (3429394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.57/2.31 % (3429394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.57/2.31 % (3429394)CaDiCaL version: 2.1.3 % 9.57/2.31 % (3429394)Termination reason: Instruction limit % 9.57/2.31 % (3429394)Termination phase: Property scanning % 9.57/2.31 % (3429394)Time elapsed: 0.002 s % 9.57/2.31 % (3429394)Peak memory usage: 85 MB % 9.57/2.31 % (3429394)Instructions burned: 9 (million) % 9.57/2.31 % (3429390)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=866190870:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 9.57/2.31 % (3429390)Refutation not found, incomplete strategy % 9.57/2.31 % (3429390)------------------------------ % 9.57/2.31 % (3429390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.57/2.31 % (3429390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.57/2.31 % (3429390)CaDiCaL version: 2.1.3 % 9.57/2.31 % (3429390)Termination reason: Refutation not found, incomplete strategy % 9.57/2.31 % (3429390)Time elapsed: 0.007 s % 9.57/2.31 % (3429390)Peak memory usage: 87 MB % 9.57/2.31 % (3429390)Instructions burned: 7 (million) % 9.57/2.31 % (3429392)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3016809217:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 9.57/2.31 % (3429391)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3801849736:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 9.57/2.31 % (3429393)lrs+10_1_thi=all:si=on:fd=off:random_seed=3639186353:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 9.57/2.31 % (3429391)Instruction limit reached! % 9.57/2.31 % (3429391)------------------------------ % 9.57/2.31 % (3429391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.57/2.31 % (3429391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.57/2.31 % (3429391)CaDiCaL version: 2.1.3 % 9.57/2.31 % (3429391)Termination reason: Instruction limit % 9.57/2.31 % (3429391)Termination phase: Including theory axioms % 9.57/2.31 % (3429391)Time elapsed: 0.004 s % 10.80/2.61 % (3429391)Peak memory usage: 85 MB % 10.80/2.61 % (3429391)Instructions burned: 4 (million) % 10.80/2.61 % (3429393)Instruction limit reached! % 10.80/2.61 % (3429393)------------------------------ % 10.80/2.61 % (3429393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.80/2.61 % (3429393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.80/2.61 % (3429393)CaDiCaL version: 2.1.3 % 10.80/2.61 % (3429393)Termination reason: Instruction limit % 10.80/2.61 % (3429393)Termination phase: Saturation % 10.80/2.61 % (3429393)Time elapsed: 0.077 s % 10.80/2.61 % (3429393)Peak memory usage: 113 MB % 10.80/2.61 % (3429393)Instructions burned: 53 (million) % 10.80/2.61 % (3429392)Instruction limit reached! % 10.80/2.61 % (3429392)------------------------------ % 10.80/2.61 % (3429392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.80/2.61 % (3429392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.80/2.61 % (3429392)CaDiCaL version: 2.1.3 % 10.80/2.61 % (3429392)Termination reason: Instruction limit % 10.80/2.61 % (3429392)Termination phase: Saturation % 10.80/2.61 % (3429392)Time elapsed: 0.122 s % 10.80/2.61 % (3429392)Peak memory usage: 135 MB % 10.80/2.61 % (3429392)Instructions burned: 66 (million) % 10.80/2.61 % (3429400)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1748011247:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 10.80/2.61 % (3429397)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4161412825:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 10.80/2.61 % (3429397)Instruction limit reached! % 10.80/2.61 % (3429397)------------------------------ % 10.80/2.61 % (3429397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.80/2.61 % (3429397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.80/2.61 % (3429397)CaDiCaL version: 2.1.3 % 10.80/2.61 % (3429397)Termination reason: Instruction limit % 10.80/2.61 % (3429397)Termination phase: Property scanning % 10.80/2.61 % (3429397)Time elapsed: 0.003 s % 10.80/2.61 % (3429397)Peak memory usage: 85 MB % 10.80/2.61 % (3429397)Instructions burned: 2 (million) % 10.80/2.61 % (3429399)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4163920527:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 10.80/2.61 % (3429399)Instruction limit reached! % 10.80/2.61 % (3429399)------------------------------ % 10.80/2.61 % (3429399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.80/2.61 % (3429399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.80/2.61 % (3429399)CaDiCaL version: 2.1.3 % 10.80/2.61 % (3429399)Termination reason: Instruction limit % 10.80/2.61 % (3429399)Termination phase: Property scanning % 10.80/2.61 % (3429399)Time elapsed: 0.003 s % 10.80/2.61 % (3429399)Peak memory usage: 85 MB % 10.80/2.61 % (3429399)Instructions burned: 3 (million) % 10.80/2.61 % (3429400)Instruction limit reached! % 10.80/2.61 % (3429400)------------------------------ % 10.80/2.61 % (3429400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.80/2.61 % (3429400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.80/2.61 % (3429400)CaDiCaL version: 2.1.3 % 10.80/2.61 % (3429400)Termination reason: Instruction limit % 10.80/2.61 % (3429400)Termination phase: Saturation % 10.80/2.61 % (3429400)Time elapsed: 0.081 s % 10.80/2.61 % (3429400)Peak memory usage: 117 MB % 10.80/2.61 % (3429400)Instructions burned: 128 (million) % 10.80/2.61 % (3429405)dis+10_1_si=on:random_seed=3425621378:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.80/2.61 % (3429405)Instruction limit reached! % 10.80/2.61 % (3429405)------------------------------ % 10.80/2.61 % (3429405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.80/2.61 % (3429405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.80/2.61 % (3429405)CaDiCaL version: 2.1.3 % 10.80/2.61 % (3429405)Termination reason: Instruction limit % 10.80/2.61 % (3429405)Termination phase: Preprocessing 2 % 10.80/2.61 % (3429405)Time elapsed: 0.011 s % 10.80/2.61 % (3429405)Peak memory usage: 86 MB % 10.80/2.61 % (3429405)Instructions burned: 11 (million) % 10.80/2.61 % (3429406)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2070176169:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 10.80/2.61 % (3429406)Instruction limit reached! % 10.80/2.61 % (3429406)------------------------------ % 10.80/2.61 % (3429406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.73/2.97 % (3429406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.73/2.97 % (3429406)CaDiCaL version: 2.1.3 % 12.73/2.97 % (3429406)Termination reason: Instruction limit % 12.73/2.97 % (3429406)Termination phase: Property scanning % 12.73/2.97 % (3429406)Time elapsed: 0.026 s % 12.73/2.97 % (3429406)Peak memory usage: 87 MB % 12.73/2.97 % (3429406)Instructions burned: 27 (million) % 12.73/2.97 % (3429390)------------------------------ % 12.73/2.97 % (3429390)------------------------------ % 12.73/2.97 % (3429410)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=13414252:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 12.73/2.97 % (3429409)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=529472113:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 12.73/2.97 % (3429410)Instruction limit reached! % 12.73/2.97 % (3429410)------------------------------ % 12.73/2.97 % (3429410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.73/2.97 % (3429410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.73/2.97 % (3429410)CaDiCaL version: 2.1.3 % 12.73/2.97 % (3429410)Termination reason: Instruction limit % 12.73/2.97 % (3429410)Termination phase: Property scanning % 12.73/2.97 % (3429410)Time elapsed: 0.003 s % 12.73/2.97 % (3429410)Peak memory usage: 85 MB % 12.73/2.97 % (3429410)Instructions burned: 2 (million) % 12.73/2.97 % (3429412)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=60418155:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 12.73/2.97 % (3429412)Instruction limit reached! % 12.73/2.97 % (3429412)------------------------------ % 12.73/2.97 % (3429412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.73/2.97 % (3429412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.73/2.97 % (3429412)CaDiCaL version: 2.1.3 % 12.73/2.97 % (3429412)Termination reason: Instruction limit % 12.73/2.97 % (3429412)Termination phase: SInE selection % 12.73/2.97 % (3429412)Time elapsed: 0.004 s % 12.73/2.97 % (3429412)Peak memory usage: 85 MB % 12.73/2.97 % (3429412)Instructions burned: 9 (million) % 12.73/2.97 % (3429409)Instruction limit reached! % 12.73/2.97 % (3429409)------------------------------ % 12.73/2.97 % (3429409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.73/2.97 % (3429409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.73/2.97 % (3429409)CaDiCaL version: 2.1.3 % 12.73/2.97 % (3429409)Termination reason: Instruction limit % 12.73/2.97 % (3429409)Termination phase: Saturation % 12.73/2.97 % (3429409)Time elapsed: 0.032 s % 12.73/2.97 % (3429409)Peak memory usage: 88 MB % 12.73/2.97 % (3429409)Instructions burned: 36 (million) % 12.73/2.97 % (3429413)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=871384589:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 12.73/2.97 % (3429415)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1444782183:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi) % 12.73/2.97 % (3429415)Instruction limit reached! % 12.73/2.97 % (3429415)------------------------------ % 12.73/2.97 % (3429415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.73/2.97 % (3429415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.73/2.97 % (3429415)CaDiCaL version: 2.1.3 % 12.73/2.97 % (3429415)Termination reason: Instruction limit % 12.73/2.97 % (3429415)Termination phase: Property scanning % 12.73/2.97 % (3429415)Time elapsed: 0.012 s % 12.73/2.97 % (3429415)Peak memory usage: 85 MB % 12.73/2.97 % (3429415)Instructions burned: 14 (million) % 12.73/2.97 % (3429423)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=2680444667:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 12.73/2.97 % (3429421)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=398477920:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 12.73/2.97 % (3429417)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=123938659:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi) % 17.48/3.46 % (3429420)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=39611456:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 17.48/3.46 % (3429420)Instruction limit reached! % 17.48/3.46 % (3429420)------------------------------ % 17.48/3.46 % (3429420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.48/3.46 % (3429420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.48/3.46 % (3429420)CaDiCaL version: 2.1.3 % 17.48/3.46 % (3429420)Termination reason: Instruction limit % 17.48/3.46 % (3429420)Termination phase: Preprocessing 3 % 17.48/3.46 % (3429420)Time elapsed: 0.010 s % 17.48/3.46 % (3429420)Peak memory usage: 86 MB % 17.48/3.46 % (3429420)Instructions burned: 10 (million) % 17.48/3.46 % (3429423)Instruction limit reached! % 17.48/3.46 % (3429423)------------------------------ % 17.48/3.46 % (3429423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.48/3.46 % (3429423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.48/3.46 % (3429423)CaDiCaL version: 2.1.3 % 17.48/3.46 % (3429423)Termination reason: Instruction limit % 17.48/3.46 % (3429423)Termination phase: Saturation % 17.48/3.46 % (3429423)Time elapsed: 0.053 s % 17.48/3.46 % (3429423)Peak memory usage: 91 MB % 17.48/3.46 % (3429423)Instructions burned: 75 (million) % 17.48/3.46 % (3429417)Refutation not found, incomplete strategy % 17.48/3.46 % (3429417)------------------------------ % 17.48/3.46 % (3429417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.48/3.46 % (3429417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.48/3.46 % (3429417)CaDiCaL version: 2.1.3 % 17.48/3.46 % (3429417)Termination reason: Refutation not found, incomplete strategy % 17.48/3.46 % (3429417)Time elapsed: 0.046 s % 17.48/3.46 % (3429417)Peak memory usage: 111 MB % 17.48/3.46 % (3429417)Instructions burned: 15 (million) % 17.48/3.46 % (3429424)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=2278503742:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi) % 17.48/3.46 % (3429421)Instruction limit reached! % 17.48/3.46 % (3429421)------------------------------ % 17.48/3.46 % (3429421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.48/3.46 % (3429421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.48/3.46 % (3429421)CaDiCaL version: 2.1.3 % 17.48/3.46 % (3429421)Termination reason: Instruction limit % 17.48/3.46 % (3429421)Termination phase: Saturation % 17.48/3.46 % (3429421)Time elapsed: 0.123 s % 17.48/3.46 % (3429421)Peak memory usage: 134 MB % 17.48/3.46 % (3429421)Instructions burned: 71 (million) % 17.48/3.46 % (3429413)Instruction limit reached! % 17.48/3.46 % (3429413)------------------------------ % 17.48/3.46 % (3429413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.48/3.46 % (3429413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.48/3.46 % (3429413)CaDiCaL version: 2.1.3 % 17.48/3.46 % (3429413)Termination reason: Instruction limit % 17.48/3.46 % (3429413)Termination phase: Saturation % 17.48/3.46 % (3429413)Time elapsed: 0.316 s % 17.48/3.46 % (3429413)Peak memory usage: 91 MB % 17.48/3.46 % (3429413)Instructions burned: 370 (million) % 17.48/3.46 % (3429432)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3256687765:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 17.48/3.46 % (3429427)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2718171215:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 17.48/3.46 % (3429433)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=171665136:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 17.48/3.46 % (3429433)Instruction limit reached! % 17.48/3.46 % (3429433)------------------------------ % 17.48/3.46 % (3429433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.48/3.46 % (3429433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.48/3.46 % (3429433)CaDiCaL version: 2.1.3 % 17.48/3.46 % (3429433)Termination reason: Instruction limit % 17.48/3.46 % (3429433)Termination phase: Saturation % 17.48/3.46 % (3429433)Time elapsed: 0.043 s % 17.48/3.46 % (3429433)Peak memory usage: 110 MB % 17.48/3.46 % (3429433)Instructions burned: 40 (million) % 17.48/3.46 % (3429432)Instruction limit reached! % 17.48/3.46 % (3429432)------------------------------ % 19.61/3.93 % (3429432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.93 % (3429432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.93 % (3429432)CaDiCaL version: 2.1.3 % 19.61/3.93 % (3429432)Termination reason: Instruction limit % 19.61/3.93 % (3429432)Termination phase: Saturation % 19.61/3.93 % (3429432)Time elapsed: 0.103 s % 19.61/3.93 % (3429432)Peak memory usage: 134 MB % 19.61/3.93 % (3429432)Instructions burned: 132 (million) % 19.61/3.93 % (3429424)Instruction limit reached! % 19.61/3.93 % (3429424)------------------------------ % 19.61/3.93 % (3429424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.93 % (3429424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.93 % (3429424)CaDiCaL version: 2.1.3 % 19.61/3.93 % (3429424)Termination reason: Instruction limit % 19.61/3.93 % (3429424)Termination phase: Saturation % 19.61/3.93 % (3429424)Time elapsed: 0.273 s % 19.61/3.93 % (3429424)Peak memory usage: 92 MB % 19.61/3.93 % (3429424)Instructions burned: 295 (million) % 19.61/3.93 % (3429427)Instruction limit reached! % 19.61/3.93 % (3429427)------------------------------ % 19.61/3.93 % (3429427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.93 % (3429427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.93 % (3429427)CaDiCaL version: 2.1.3 % 19.61/3.93 % (3429427)Termination reason: Instruction limit % 19.61/3.93 % (3429427)Termination phase: Saturation % 19.61/3.93 % (3429427)Time elapsed: 0.157 s % 19.61/3.93 % (3429427)Peak memory usage: 117 MB % 19.61/3.93 % (3429427)Instructions burned: 130 (million) % 19.61/3.93 % (3429435)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3623159844:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 19.61/3.93 % (3429417)------------------------------ % 19.61/3.93 % (3429417)------------------------------ % 19.61/3.93 % (3429438)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1212631335:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 19.61/3.93 % (3429441)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=1942955000:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 19.61/3.93 % (3429440)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2393910840:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 19.61/3.93 % (3429441)Refutation not found, incomplete strategy % 19.61/3.93 % (3429441)------------------------------ % 19.61/3.93 % (3429441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.93 % (3429441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.93 % (3429441)CaDiCaL version: 2.1.3 % 19.61/3.93 % (3429441)Termination reason: Refutation not found, incomplete strategy % 19.61/3.93 % (3429441)Time elapsed: 0.035 s % 19.61/3.93 % (3429441)Peak memory usage: 112 MB % 19.61/3.93 % (3429441)Instructions burned: 16 (million) % 19.61/3.93 % (3429443)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=530757385:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 19.61/3.93 % (3429442)dis+10_1_si=on:random_seed=2281469564:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi) % 19.61/3.93 % (3429435)Instruction limit reached! % 19.61/3.93 % (3429435)------------------------------ % 19.61/3.93 % (3429435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.93 % (3429435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.93 % (3429435)CaDiCaL version: 2.1.3 % 19.61/3.93 % (3429435)Termination reason: Instruction limit % 19.61/3.93 % (3429435)Termination phase: Saturation % 19.61/3.93 % (3429435)Time elapsed: 0.242 s % 19.61/3.93 % (3429435)Peak memory usage: 92 MB % 19.61/3.93 % (3429435)Instructions burned: 308 (million) % 19.61/3.93 % (3429440)Instruction limit reached! % 19.61/3.93 % (3429440)------------------------------ % 19.61/3.93 % (3429440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.93 % (3429440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.93 % (3429440)CaDiCaL version: 2.1.3 % 19.61/3.93 % (3429440)Termination reason: Instruction limit % 19.61/3.93 % (3429440)Termination phase: Saturation % 24.10/4.34 % (3429440)Time elapsed: 0.156 s % 24.10/4.34 % (3429440)Peak memory usage: 118 MB % 24.10/4.34 % (3429440)Instructions burned: 131 (million) % 24.10/4.34 % (3429445)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2163925964:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 24.10/4.34 % (3429443)Instruction limit reached! % 24.10/4.34 % (3429443)------------------------------ % 24.10/4.34 % (3429443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.10/4.34 % (3429443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.10/4.34 % (3429443)CaDiCaL version: 2.1.3 % 24.10/4.34 % (3429443)Termination reason: Instruction limit % 24.10/4.34 % (3429443)Termination phase: Saturation % 24.10/4.34 % (3429443)Time elapsed: 0.206 s % 24.10/4.34 % (3429443)Peak memory usage: 100 MB % 24.10/4.34 % (3429443)Instructions burned: 383 (million) % 24.10/4.34 % (3429445)Instruction limit reached! % 24.10/4.34 % (3429445)------------------------------ % 24.10/4.34 % (3429445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.10/4.34 % (3429445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.10/4.34 % (3429445)CaDiCaL version: 2.1.3 % 24.10/4.34 % (3429445)Termination reason: Instruction limit % 24.10/4.34 % (3429445)Termination phase: Saturation % 24.10/4.34 % (3429445)Time elapsed: 0.146 s % 24.10/4.34 % (3429445)Peak memory usage: 90 MB % 24.10/4.34 % (3429445)Instructions burned: 141 (million) % 24.10/4.34 % (3429441)------------------------------ % 24.10/4.34 % (3429441)------------------------------ % 24.10/4.34 % (3429451)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3295600394:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi) % 24.10/4.34 % (3429452)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3085586661:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 24.10/4.34 % (3429454)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=3144748384:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 24.10/4.34 % (3429451)Refutation not found, incomplete strategy % 24.10/4.34 % (3429451)------------------------------ % 24.10/4.34 % (3429451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.10/4.34 % (3429451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.10/4.34 % (3429451)CaDiCaL version: 2.1.3 % 24.10/4.34 % (3429451)Termination reason: Refutation not found, incomplete strategy % 24.10/4.34 % (3429451)Time elapsed: 0.079 s % 24.10/4.34 % (3429451)Peak memory usage: 113 MB % 24.10/4.34 % (3429451)Instructions burned: 49 (million) % 24.10/4.34 % (3429454)Refutation not found, incomplete strategy % 24.10/4.34 % (3429454)------------------------------ % 24.10/4.34 % (3429454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.10/4.34 % (3429454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.10/4.34 % (3429454)CaDiCaL version: 2.1.3 % 24.10/4.34 % (3429454)Termination reason: Refutation not found, incomplete strategy % 24.10/4.34 % (3429454)Time elapsed: 0.047 s % 24.10/4.34 % (3429454)Peak memory usage: 114 MB % 24.10/4.34 % (3429454)Instructions burned: 53 (million) % 24.10/4.34 % (3429452)Instruction limit reached! % 24.10/4.34 % (3429452)------------------------------ % 24.10/4.34 % (3429452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.10/4.34 % (3429452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.10/4.34 % (3429452)CaDiCaL version: 2.1.3 % 24.10/4.34 % (3429452)Termination reason: Instruction limit % 24.10/4.34 % (3429452)Termination phase: Saturation % 24.10/4.34 % (3429452)Time elapsed: 0.113 s % 24.10/4.34 % (3429452)Peak memory usage: 90 MB % 24.10/4.34 % (3429452)Instructions burned: 123 (million) % 24.10/4.34 % (3429455)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=2388468832:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi) % 24.10/4.34 % (3429438)Instruction limit reached! % 24.10/4.34 % (3429438)------------------------------ % 24.10/4.34 % (3429438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.10/4.34 % (3429438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.10/4.34 % (3429438)CaDiCaL version: 2.1.3 % 24.10/4.34 % (3429438)Termination reason: Instruction limit % 24.10/4.34 % (3429438)Termination phase: Saturation % 24.10/4.34 % (3429438)Time elapsed: 0.688 s % 26.88/4.95 % (3429438)Peak memory usage: 143 MB % 26.88/4.95 % (3429438)Instructions burned: 598 (million) % 26.88/4.95 % (3429456)dis+1010_1_to=kbo:si=on:random_seed=3798885564:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 26.88/4.95 % (3429455)Instruction limit reached! % 26.88/4.95 % (3429455)------------------------------ % 26.88/4.95 % (3429455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.88/4.95 % (3429455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.88/4.95 % (3429455)CaDiCaL version: 2.1.3 % 26.88/4.95 % (3429455)Termination reason: Instruction limit % 26.88/4.95 % (3429455)Termination phase: Saturation % 26.88/4.95 % (3429455)Time elapsed: 0.037 s % 26.88/4.95 % (3429455)Peak memory usage: 89 MB % 26.88/4.95 % (3429455)Instructions burned: 39 (million) % 26.88/4.95 % (3429465)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4000285264:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 26.88/4.95 % (3429454)------------------------------ % 26.88/4.95 % (3429454)------------------------------ % 26.88/4.95 % (3429456)Instruction limit reached! % 26.88/4.95 % (3429456)------------------------------ % 26.88/4.95 % (3429456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.88/4.95 % (3429456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.88/4.95 % (3429456)CaDiCaL version: 2.1.3 % 26.88/4.95 % (3429456)Termination reason: Instruction limit % 26.88/4.95 % (3429456)Termination phase: Saturation % 26.88/4.95 % (3429456)Time elapsed: 0.178 s % 26.88/4.95 % (3429456)Peak memory usage: 91 MB % 26.88/4.95 % (3429456)Instructions burned: 175 (million) % 26.88/4.95 % (3429451)------------------------------ % 26.88/4.95 % (3429451)------------------------------ % 26.88/4.95 % (3429472)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3707255853:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi) % 26.88/4.95 % (3429473)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2855305822:thitd=on:i=215:nm=0:rtra=on:ev=force_2973 on theBenchmark for (2973ds/215Mi) % 26.88/4.95 % (3429478)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=320535904:i=349:rtra=on_2972 on theBenchmark for (2972ds/349Mi) % 26.88/4.95 % (3429442)Instruction limit reached! % 26.88/4.95 % (3429442)------------------------------ % 26.88/4.95 % (3429442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.88/4.95 % (3429442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.88/4.95 % (3429442)CaDiCaL version: 2.1.3 % 26.88/4.95 % (3429442)Termination reason: Instruction limit % 26.88/4.95 % (3429442)Termination phase: Saturation % 26.88/4.95 % (3429442)Time elapsed: 0.891 s % 26.88/4.95 % (3429442)Peak memory usage: 94 MB % 26.88/4.95 % (3429442)Instructions burned: 1000 (million) % 26.88/4.95 % (3429480)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3468612867:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 26.88/4.95 % (3429480)Refutation not found, incomplete strategy % 26.88/4.95 % (3429480)------------------------------ % 26.88/4.95 % (3429480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.88/4.95 % (3429480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.88/4.95 % (3429480)CaDiCaL version: 2.1.3 % 26.88/4.95 % (3429480)Termination reason: Refutation not found, incomplete strategy % 26.88/4.95 % (3429480)Time elapsed: 0.006 s % 26.88/4.95 % (3429480)Peak memory usage: 88 MB % 26.88/4.95 % (3429480)Instructions burned: 11 (million) % 26.88/4.95 % (3429465)Instruction limit reached! % 26.88/4.95 % (3429465)------------------------------ % 26.88/4.95 % (3429465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.88/4.95 % (3429465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.88/4.95 % (3429465)CaDiCaL version: 2.1.3 % 26.88/4.95 % (3429465)Termination reason: Instruction limit % 26.88/4.95 % (3429465)Termination phase: Saturation % 26.88/4.95 % (3429465)Time elapsed: 0.336 s % 26.88/4.95 % (3429465)Peak memory usage: 118 MB % 26.88/4.95 % (3429465)Instructions burned: 329 (million) % 26.88/4.95 % (3429484)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3923918162:i=328:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/328Mi) % 31.21/5.34 % (3429473)Instruction limit reached! % 31.21/5.34 % (3429473)------------------------------ % 31.21/5.34 % (3429473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.21/5.34 % (3429473)CaDiCaL version: 2.1.3 % 31.21/5.34 % (3429473)Termination reason: Instruction limit % 31.21/5.34 % (3429473)Termination phase: Saturation % 31.21/5.34 % (3429473)Time elapsed: 0.220 s % 31.21/5.34 % (3429473)Peak memory usage: 137 MB % 31.21/5.34 % (3429473)Instructions burned: 215 (million) % 31.21/5.34 % (3429480)------------------------------ % 31.21/5.34 % (3429480)------------------------------ % 31.21/5.34 % (3429489)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=803871662:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi) % 31.21/5.34 % (3429478)Instruction limit reached! % 31.21/5.34 % (3429478)------------------------------ % 31.21/5.34 % (3429478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.21/5.34 % (3429478)CaDiCaL version: 2.1.3 % 31.21/5.34 % (3429478)Termination reason: Instruction limit % 31.21/5.34 % (3429478)Termination phase: Saturation % 31.21/5.34 % (3429478)Time elapsed: 0.349 s % 31.21/5.34 % (3429478)Peak memory usage: 118 MB % 31.21/5.34 % (3429478)Instructions burned: 349 (million) % 31.21/5.34 % (3429492)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2625715449:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi) % 31.21/5.34 % (3429492)Refutation not found, incomplete strategy % 31.21/5.34 % (3429492)------------------------------ % 31.21/5.34 % (3429492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.21/5.34 % (3429492)CaDiCaL version: 2.1.3 % 31.21/5.34 % (3429492)Termination reason: Refutation not found, incomplete strategy % 31.21/5.34 % (3429492)Time elapsed: 0.011 s % 31.21/5.34 % (3429492)Peak memory usage: 88 MB % 31.21/5.34 % (3429492)Instructions burned: 11 (million) % 31.21/5.34 % (3429472)Instruction limit reached! % 31.21/5.34 % (3429472)------------------------------ % 31.21/5.34 % (3429472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.21/5.34 % (3429472)CaDiCaL version: 2.1.3 % 31.21/5.34 % (3429472)Termination reason: Instruction limit % 31.21/5.34 % (3429472)Termination phase: Saturation % 31.21/5.34 % (3429472)Time elapsed: 0.510 s % 31.21/5.34 % (3429472)Peak memory usage: 137 MB % 31.21/5.34 % (3429472)Instructions burned: 483 (million) % 31.21/5.34 % (3429494)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2072701662:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi) % 31.21/5.34 % (3429484)Instruction limit reached! % 31.21/5.34 % (3429484)------------------------------ % 31.21/5.34 % (3429484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.21/5.34 % (3429484)CaDiCaL version: 2.1.3 % 31.21/5.34 % (3429484)Termination reason: Instruction limit % 31.21/5.34 % (3429484)Termination phase: Saturation % 31.21/5.34 % (3429484)Time elapsed: 0.344 s % 31.21/5.34 % (3429484)Peak memory usage: 119 MB % 31.21/5.34 % (3429484)Instructions burned: 329 (million) % 31.21/5.34 % (3429494)Refutation not found, incomplete strategy % 31.21/5.34 % (3429494)------------------------------ % 31.21/5.34 % (3429494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.21/5.34 % (3429494)CaDiCaL version: 2.1.3 % 31.21/5.34 % (3429494)Termination reason: Refutation not found, incomplete strategy % 31.21/5.34 % (3429494)Time elapsed: 0.047 s % 31.21/5.34 % (3429494)Peak memory usage: 112 MB % 31.21/5.34 % (3429494)Instructions burned: 16 (million) % 31.21/5.34 % (3429495)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=252712396:i=416:rtra=on:gtg=position:ss=axioms_2967 on theBenchmark for (2967ds/416Mi) % 31.21/5.34 % (3429495)Refutation not found, incomplete strategy % 31.21/5.34 % (3429495)------------------------------ % 31.21/5.34 % (3429495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.21/5.34 % (3429495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.28/5.96 % (3429495)CaDiCaL version: 2.1.3 % 33.28/5.96 % (3429495)Termination reason: Refutation not found, incomplete strategy % 33.28/5.96 % (3429495)Time elapsed: 0.026 s % 33.28/5.96 % (3429495)Peak memory usage: 111 MB % 33.28/5.96 % (3429495)Instructions burned: 15 (million) % 33.28/5.96 % (3429497)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3104076190:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 33.28/5.96 % (3429489)Instruction limit reached! % 33.28/5.96 % (3429489)------------------------------ % 33.28/5.96 % (3429489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.28/5.96 % (3429489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.28/5.96 % (3429489)CaDiCaL version: 2.1.3 % 33.28/5.96 % (3429489)Termination reason: Instruction limit % 33.28/5.96 % (3429489)Termination phase: Saturation % 33.28/5.96 % (3429489)Time elapsed: 0.318 s % 33.28/5.96 % (3429489)Peak memory usage: 118 MB % 33.28/5.96 % (3429489)Instructions burned: 281 (million) % 33.28/5.96 % (3429499)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=2023471117:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi) % 33.28/5.96 % (3429501)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=823356146:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi) % 33.28/5.96 % (3429495)------------------------------ % 33.28/5.96 % (3429495)------------------------------ % 33.28/5.96 % (3429492)------------------------------ % 33.28/5.96 % (3429492)------------------------------ % 33.28/5.96 % (3429494)------------------------------ % 33.28/5.96 % (3429494)------------------------------ % 33.28/5.96 % (3429504)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1300795552:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/387Mi) % 33.28/5.96 % (3429507)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3275216859:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2963 on theBenchmark for (2963ds/513Mi) % 33.28/5.96 % (3429504)Refutation not found, incomplete strategy % 33.28/5.96 % (3429504)------------------------------ % 33.28/5.96 % (3429504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.28/5.96 % (3429504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.28/5.96 % (3429504)CaDiCaL version: 2.1.3 % 33.28/5.96 % (3429504)Termination reason: Refutation not found, incomplete strategy % 33.28/5.96 % (3429504)Time elapsed: 0.047 s % 33.28/5.96 % (3429504)Peak memory usage: 112 MB % 33.28/5.96 % (3429504)Instructions burned: 17 (million) % 33.28/5.96 % (3429508)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=759107105:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi) % 33.28/5.96 % (3429499)Instruction limit reached! % 33.28/5.96 % (3429499)------------------------------ % 33.28/5.96 % (3429499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.28/5.96 % (3429499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.28/5.96 % (3429499)CaDiCaL version: 2.1.3 % 33.28/5.96 % (3429499)Termination reason: Instruction limit % 33.28/5.96 % (3429499)Termination phase: Saturation % 33.28/5.96 % (3429499)Time elapsed: 0.307 s % 33.28/5.96 % (3429499)Peak memory usage: 135 MB % 33.28/5.96 % (3429499)Instructions burned: 276 (million) % 33.28/5.96 % (3429497)Instruction limit reached! % 33.28/5.96 % (3429497)------------------------------ % 33.28/5.96 % (3429497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.28/5.96 % (3429497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.28/5.96 % (3429497)CaDiCaL version: 2.1.3 % 33.28/5.96 % (3429497)Termination reason: Instruction limit % 33.28/5.96 % (3429497)Termination phase: Saturation % 33.28/5.96 % (3429497)Time elapsed: 0.464 s % 33.28/5.96 % (3429497)Peak memory usage: 119 MB % 33.28/5.96 % (3429497)Instructions burned: 471 (million) % 33.28/5.96 % (3429501)Instruction limit reached! % 33.28/5.96 % (3429501)------------------------------ % 33.28/5.96 % (3429501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.28/5.96 % (3429501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.34/6.61 % (3429501)CaDiCaL version: 2.1.3 % 39.34/6.61 % (3429501)Termination reason: Instruction limit % 39.34/6.61 % (3429501)Termination phase: Saturation % 39.34/6.61 % (3429501)Time elapsed: 0.385 s % 39.34/6.61 % (3429501)Peak memory usage: 119 MB % 39.34/6.61 % (3429501)Instructions burned: 375 (million) % 39.34/6.61 % (3429507)Instruction limit reached! % 39.34/6.61 % (3429507)------------------------------ % 39.34/6.61 % (3429507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.34/6.61 % (3429507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.34/6.61 % (3429507)CaDiCaL version: 2.1.3 % 39.34/6.61 % (3429507)Termination reason: Instruction limit % 39.34/6.61 % (3429507)Termination phase: Saturation % 39.34/6.61 % (3429507)Time elapsed: 0.229 s % 39.34/6.61 % (3429507)Peak memory usage: 93 MB % 39.34/6.61 % (3429507)Instructions burned: 516 (million) % 39.34/6.61 % (3429510)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2163888384:i=359:rtra=on:gtg=exists_top:ss=axioms_2961 on theBenchmark for (2961ds/359Mi) % 39.34/6.61 % (3429513)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3937027700:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 39.34/6.61 % (3429508)Instruction limit reached! % 39.34/6.61 % (3429508)------------------------------ % 39.34/6.61 % (3429508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.34/6.61 % (3429508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.34/6.61 % (3429508)CaDiCaL version: 2.1.3 % 39.34/6.61 % (3429508)Termination reason: Instruction limit % 39.34/6.61 % (3429508)Termination phase: Saturation % 39.34/6.61 % (3429508)Time elapsed: 0.349 s % 39.34/6.61 % (3429508)Peak memory usage: 135 MB % 39.34/6.61 % (3429508)Instructions burned: 334 (million) % 39.34/6.61 % (3429504)------------------------------ % 39.34/6.61 % (3429504)------------------------------ % 39.34/6.61 % (3429517)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2692078532:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 39.34/6.61 % (3429514)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=156064584:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 39.34/6.61 % (3429514)Refutation not found, incomplete strategy % 39.34/6.61 % (3429514)------------------------------ % 39.34/6.61 % (3429514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.34/6.61 % (3429514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.34/6.61 % (3429514)CaDiCaL version: 2.1.3 % 39.34/6.61 % (3429514)Termination reason: Refutation not found, incomplete strategy % 39.34/6.61 % (3429514)Time elapsed: 0.042 s % 39.34/6.61 % (3429514)Peak memory usage: 111 MB % 39.34/6.61 % (3429514)Instructions burned: 12 (million) % 39.34/6.61 % (3429515)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=2736005382:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/235Mi) % 39.34/6.61 % (3429515)Refutation not found, incomplete strategy % 39.34/6.61 % (3429515)------------------------------ % 39.34/6.61 % (3429515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.34/6.61 % (3429515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.34/6.61 % (3429515)CaDiCaL version: 2.1.3 % 39.34/6.61 % (3429515)Termination reason: Refutation not found, incomplete strategy % 39.34/6.61 % (3429515)Time elapsed: 0.048 s % 39.34/6.61 % (3429515)Peak memory usage: 111 MB % 39.34/6.61 % (3429515)Instructions burned: 16 (million) % 39.34/6.61 % (3429510)Instruction limit reached! % 39.34/6.61 % (3429510)------------------------------ % 39.34/6.61 % (3429510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.34/6.61 % (3429510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.34/6.61 % (3429510)CaDiCaL version: 2.1.3 % 39.34/6.61 % (3429510)Termination reason: Instruction limit % 39.34/6.61 % (3429510)Termination phase: Saturation % 39.34/6.61 % (3429510)Time elapsed: 0.328 s % 39.34/6.61 % (3429510)Peak memory usage: 92 MB % 39.34/6.61 % (3429510)Instructions burned: 359 (million) % 39.34/6.61 % (3429517)Instruction limit reached! % 39.34/6.61 % (3429517)------------------------------ % 39.34/6.61 % (3429517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.42/7.40 % (3429517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.42/7.40 % (3429517)CaDiCaL version: 2.1.3 % 45.42/7.40 % (3429517)Termination reason: Instruction limit % 45.42/7.40 % (3429517)Termination phase: Saturation % 45.42/7.40 % (3429517)Time elapsed: 0.160 s % 45.42/7.40 % (3429517)Peak memory usage: 92 MB % 45.42/7.40 % (3429517)Instructions burned: 279 (million) % 45.42/7.40 % (3429520)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3446775168:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi) % 45.42/7.40 % (3429519)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2563250340:i=146:doe=on:rtra=on_2957 on theBenchmark for (2957ds/146Mi) % 45.42/7.40 % (3429513)Instruction limit reached! % 45.42/7.40 % (3429513)------------------------------ % 45.42/7.40 % (3429513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.42/7.40 % (3429513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.42/7.40 % (3429513)CaDiCaL version: 2.1.3 % 45.42/7.40 % (3429513)Termination reason: Instruction limit % 45.42/7.40 % (3429513)Termination phase: Saturation % 45.42/7.40 % (3429513)Time elapsed: 0.381 s % 45.42/7.40 % (3429513)Peak memory usage: 125 MB % 45.42/7.40 % (3429513)Instructions burned: 341 (million) % 45.42/7.40 % (3429519)Instruction limit reached! % 45.42/7.40 % (3429519)------------------------------ % 45.42/7.40 % (3429519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.42/7.40 % (3429519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.42/7.40 % (3429519)CaDiCaL version: 2.1.3 % 45.42/7.40 % (3429519)Termination reason: Instruction limit % 45.42/7.40 % (3429519)Termination phase: Saturation % 45.42/7.40 % (3429519)Time elapsed: 0.149 s % 45.42/7.40 % (3429519)Peak memory usage: 90 MB % 45.42/7.40 % (3429519)Instructions burned: 146 (million) % 45.42/7.40 % (3429525)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=947563659:i=1052:rtra=on_2955 on theBenchmark for (2955ds/1052Mi) % 45.42/7.40 % (3429524)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=1124457612:avsq=on:i=276:avsqr=1,2:rtra=on_2955 on theBenchmark for (2955ds/276Mi) % 45.42/7.40 % (3429514)------------------------------ % 45.42/7.40 % (3429514)------------------------------ % 45.42/7.40 % (3429515)------------------------------ % 45.42/7.40 % (3429515)------------------------------ % 45.42/7.40 % (3429528)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3775129053:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/655Mi) % 45.42/7.40 % (3429530)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=305212542:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2953 on theBenchmark for (2953ds/1054Mi) % 45.42/7.40 % (3429530)Refutation not found, incomplete strategy % 45.42/7.40 % (3429530)------------------------------ % 45.42/7.40 % (3429530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.42/7.40 % (3429530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.42/7.40 % (3429530)CaDiCaL version: 2.1.3 % 45.42/7.40 % (3429530)Termination reason: Refutation not found, incomplete strategy % 45.42/7.40 % (3429530)Time elapsed: 0.007 s % 45.42/7.40 % (3429530)Peak memory usage: 87 MB % 45.42/7.40 % (3429530)Instructions burned: 7 (million) % 45.42/7.40 % (3429524)Instruction limit reached! % 45.42/7.40 % (3429524)------------------------------ % 45.42/7.40 % (3429524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.42/7.40 % (3429524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.42/7.40 % (3429524)CaDiCaL version: 2.1.3 % 45.42/7.40 % (3429524)Termination reason: Instruction limit % 45.42/7.40 % (3429524)Termination phase: Saturation % 45.42/7.40 % (3429524)Time elapsed: 0.309 s % 45.42/7.40 % (3429524)Peak memory usage: 135 MB % 45.42/7.40 % (3429524)Instructions burned: 276 (million) % 45.42/7.40 % (3429532)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=296720812:i=107:rtra=on_2952 on theBenchmark for (2952ds/107Mi) % 45.42/7.40 % (3429533)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2100253276:s2a=on:i=450:doe=on:nm=32:rtra=on_2951 on theBenchmark for (2951ds/450Mi) % 45.42/7.40 % (3429532)Refutation not found, incomplete strategy % 48.87/8.02 % (3429532)------------------------------ % 48.87/8.02 % (3429532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.87/8.02 % (3429532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/8.02 % (3429532)CaDiCaL version: 2.1.3 % 48.87/8.02 % (3429532)Termination reason: Refutation not found, incomplete strategy % 48.87/8.02 % (3429532)Time elapsed: 0.076 s % 48.87/8.02 % (3429532)Peak memory usage: 114 MB % 48.87/8.02 % (3429532)Instructions burned: 48 (million) % 48.87/8.02 % (3429537)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 % 48.87/8.02 % (3429537)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1770452021:i=1090:aac=none:nm=0:rtra=on:rawr=on_2949 on theBenchmark for (2949ds/1090Mi) % 48.87/8.02 % (3429530)------------------------------ % 48.87/8.02 % (3429530)------------------------------ % 48.87/8.02 % (3429525)Instruction limit reached! % 48.87/8.02 % (3429525)------------------------------ % 48.87/8.02 % (3429525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.87/8.02 % (3429525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/8.02 % (3429525)CaDiCaL version: 2.1.3 % 48.87/8.02 % (3429525)Termination reason: Instruction limit % 48.87/8.02 % (3429525)Termination phase: Saturation % 48.87/8.02 % (3429525)Time elapsed: 0.689 s % 48.87/8.02 % (3429525)Peak memory usage: 97 MB % 48.87/8.02 % (3429525)Instructions burned: 1052 (million) % 48.87/8.02 % (3429528)Instruction limit reached! % 48.87/8.02 % (3429528)------------------------------ % 48.87/8.02 % (3429528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.87/8.02 % (3429528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/8.02 % (3429528)CaDiCaL version: 2.1.3 % 48.87/8.02 % (3429528)Termination reason: Instruction limit % 48.87/8.02 % (3429528)Termination phase: Saturation % 48.87/8.02 % (3429528)Time elapsed: 0.540 s % 48.87/8.02 % (3429528)Peak memory usage: 93 MB % 48.87/8.02 % (3429528)Instructions burned: 656 (million) % 48.87/8.02 % (3429532)------------------------------ % 48.87/8.02 % (3429532)------------------------------ % 48.87/8.02 % (3429540)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=670604385:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2946 on theBenchmark for (2946ds/130Mi) % 48.87/8.02 % (3429542)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2109323067:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 48.87/8.02 % (3429533)Instruction limit reached! % 48.87/8.02 % (3429533)------------------------------ % 48.87/8.02 % (3429533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.87/8.02 % (3429533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/8.02 % (3429533)CaDiCaL version: 2.1.3 % 48.87/8.02 % (3429533)Termination reason: Instruction limit % 48.87/8.02 % (3429533)Termination phase: Saturation % 48.87/8.02 % (3429533)Time elapsed: 0.513 s % 48.87/8.02 % (3429533)Peak memory usage: 137 MB % 48.87/8.02 % (3429533)Instructions burned: 450 (million) % 48.87/8.02 % (3429541)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2294671609:i=312:kws=inv_frequency:nm=20:rtra=on_2946 on theBenchmark for (2946ds/312Mi) % 48.87/8.02 % (3429542)Refutation not found, incomplete strategy % 48.87/8.02 % (3429542)------------------------------ % 48.87/8.02 % (3429542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.87/8.02 % (3429542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/8.02 % (3429542)CaDiCaL version: 2.1.3 % 48.87/8.02 % (3429542)Termination reason: Refutation not found, incomplete strategy % 48.87/8.02 % (3429542)Time elapsed: 0.030 s % 48.87/8.02 % (3429542)Peak memory usage: 90 MB % 48.87/8.02 % (3429542)Instructions burned: 46 (million) % 48.87/8.02 % (3429540)Instruction limit reached! % 48.87/8.02 % (3429540)------------------------------ % 48.87/8.02 % (3429540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.87/8.02 % (3429540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.87/8.02 % (3429540)CaDiCaL version: 2.1.3 % 48.87/8.02 % (3429540)Termination reason: Instruction limit % 48.87/8.02 % (3429540)Termination phase: Saturation % 55.31/9.01 % (3429540)Time elapsed: 0.154 s % 55.31/9.01 % (3429540)Peak memory usage: 117 MB % 55.31/9.01 % (3429540)Instructions burned: 130 (million) % 55.31/9.01 % (3429543)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3598299419:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi) % 55.31/9.01 % (3429547)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2217518293:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2943 on theBenchmark for (2943ds/307Mi) % 55.31/9.01 % (3429537)Instruction limit reached! % 55.31/9.01 % (3429537)------------------------------ % 55.31/9.01 % (3429537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.31/9.01 % (3429537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.31/9.01 % (3429537)CaDiCaL version: 2.1.3 % 55.31/9.01 % (3429537)Termination reason: Instruction limit % 55.31/9.01 % (3429537)Termination phase: Saturation % 55.31/9.01 % (3429537)Time elapsed: 0.554 s % 55.31/9.01 % (3429537)Peak memory usage: 125 MB % 55.31/9.01 % (3429537)Instructions burned: 1090 (million) % 55.31/9.01 % (3429547)Refutation not found, incomplete strategy % 55.31/9.01 % (3429547)------------------------------ % 55.31/9.01 % (3429547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.31/9.01 % (3429547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.31/9.01 % (3429547)CaDiCaL version: 2.1.3 % 55.31/9.01 % (3429547)Termination reason: Refutation not found, incomplete strategy % 55.31/9.01 % (3429547)Time elapsed: 0.041 s % 55.31/9.01 % (3429547)Peak memory usage: 90 MB % 55.31/9.01 % (3429547)Instructions burned: 58 (million) % 55.31/9.01 % (3429541)Instruction limit reached! % 55.31/9.01 % (3429541)------------------------------ % 55.31/9.01 % (3429541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.31/9.01 % (3429541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.31/9.01 % (3429541)CaDiCaL version: 2.1.3 % 55.31/9.01 % (3429541)Termination reason: Instruction limit % 55.31/9.01 % (3429541)Termination phase: Saturation % 55.31/9.01 % (3429541)Time elapsed: 0.331 s % 55.31/9.01 % (3429541)Peak memory usage: 118 MB % 55.31/9.01 % (3429541)Instructions burned: 312 (million) % 55.31/9.01 % (3429548)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=231360013:i=776:doe=on:rtra=on_2942 on theBenchmark for (2942ds/776Mi) % 55.31/9.01 % (3429542)------------------------------ % 55.31/9.01 % (3429542)------------------------------ % 55.31/9.01 % (3429551)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2206142169:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2941 on theBenchmark for (2941ds/646Mi) % 55.31/9.01 % (3429547)------------------------------ % 55.31/9.01 % (3429547)------------------------------ % 55.31/9.01 % (3429552)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=4169721637:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2940 on theBenchmark for (2940ds/784Mi) % 55.31/9.01 % (3429555)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=3721949817:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2939 on theBenchmark for (2939ds/1131Mi) % 55.31/9.01 % (3429551)Instruction limit reached! % 55.31/9.01 % (3429551)------------------------------ % 55.31/9.01 % (3429551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.31/9.01 % (3429551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.31/9.01 % (3429551)CaDiCaL version: 2.1.3 % 55.31/9.01 % (3429551)Termination reason: Instruction limit % 55.31/9.01 % (3429551)Termination phase: Saturation % 55.31/9.01 % (3429551)Time elapsed: 0.425 s % 55.31/9.01 % (3429551)Peak memory usage: 144 MB % 55.31/9.01 % (3429551)Instructions burned: 646 (million) % 55.31/9.01 % (3429543)Instruction limit reached! % 55.31/9.01 % (3429543)------------------------------ % 55.31/9.01 % (3429543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.31/9.01 % (3429543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.31/9.01 % (3429543)CaDiCaL version: 2.1.3 % 55.31/9.01 % (3429543)Termination reason: Instruction limit % 55.31/9.01 % (3429543)Termination phase: Saturation % 55.31/9.01 % (3429543)Time elapsed: 0.759 s % 55.31/9.01 % (3429543)Peak memory usage: 95 MB % 55.31/9.01 % (3429543)Instructions burned: 835 (million) % 55.31/9.01 % (3429557)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=2820564464:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi) % 68.62/10.62 % (3429557)Refutation not found, incomplete strategy % 68.62/10.62 % (3429557)------------------------------ % 68.62/10.62 % (3429557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.62/10.62 % (3429557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.62/10.62 % (3429557)CaDiCaL version: 2.1.3 % 68.62/10.62 % (3429557)Termination reason: Refutation not found, incomplete strategy % 68.62/10.62 % (3429557)Time elapsed: 0.047 s % 68.62/10.62 % (3429557)Peak memory usage: 111 MB % 68.62/10.62 % (3429557)Instructions burned: 16 (million) % 68.62/10.62 % (3429559)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1878190499:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/775Mi) % 68.62/10.62 % (3429559)Refutation not found, incomplete strategy % 68.62/10.62 % (3429559)------------------------------ % 68.62/10.62 % (3429559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.62/10.62 % (3429559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.62/10.62 % (3429559)CaDiCaL version: 2.1.3 % 68.62/10.62 % (3429559)Termination reason: Refutation not found, incomplete strategy % 68.62/10.62 % (3429559)Time elapsed: 0.006 s % 68.62/10.62 % (3429559)Peak memory usage: 88 MB % 68.62/10.62 % (3429559)Instructions burned: 12 (million) % 68.62/10.62 % (3429548)Instruction limit reached! % 68.62/10.62 % (3429548)------------------------------ % 68.62/10.62 % (3429548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.62/10.62 % (3429548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.62/10.62 % (3429548)CaDiCaL version: 2.1.3 % 68.62/10.62 % (3429548)Termination reason: Instruction limit % 68.62/10.62 % (3429548)Termination phase: Saturation % 68.62/10.62 % (3429548)Time elapsed: 0.768 s % 68.62/10.62 % (3429548)Peak memory usage: 123 MB % 68.62/10.62 % (3429548)Instructions burned: 776 (million) % 68.62/10.62 % (3429561)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2641648408:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2934 on theBenchmark for (2934ds/273Mi) % 68.62/10.62 % (3429552)Instruction limit reached! % 68.62/10.62 % (3429552)------------------------------ % 68.62/10.62 % (3429552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.62/10.62 % (3429552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.62/10.62 % (3429552)CaDiCaL version: 2.1.3 % 68.62/10.62 % (3429552)Termination reason: Instruction limit % 68.62/10.62 % (3429552)Termination phase: Saturation % 68.62/10.62 % (3429552)Time elapsed: 0.672 s % 68.62/10.62 % (3429552)Peak memory usage: 118 MB % 68.62/10.62 % (3429552)Instructions burned: 784 (million) % 68.62/10.62 % (3429559)------------------------------ % 68.62/10.62 % (3429559)------------------------------ % 68.62/10.62 % (3429557)------------------------------ % 68.62/10.62 % (3429557)------------------------------ % 68.62/10.62 % (3429563)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1852263778:i=102:nm=16:rtra=on_2932 on theBenchmark for (2932ds/102Mi) % 68.62/10.62 % (3429561)Instruction limit reached! % 68.62/10.62 % (3429561)------------------------------ % 68.62/10.62 % (3429561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.62/10.62 % (3429561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.62/10.62 % (3429561)CaDiCaL version: 2.1.3 % 68.62/10.62 % (3429561)Termination reason: Instruction limit % 68.62/10.62 % (3429561)Termination phase: Saturation % 68.62/10.62 % (3429561)Time elapsed: 0.279 s % 68.62/10.62 % (3429561)Peak memory usage: 92 MB % 68.62/10.62 % (3429561)Instructions burned: 274 (million) % 68.62/10.62 % (3429566)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2573297643:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi) % 68.62/10.62 % (3429565)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3942997635:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2931 on theBenchmark for (2931ds/1094Mi) % 68.62/10.62 % (3429563)Instruction limit reached! % 68.62/10.62 % (3429563)------------------------------ % 68.62/10.62 % (3429563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.62/10.62 % (3429563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.65/13.94 % (3429563)CaDiCaL version: 2.1.3 % 91.65/13.94 % (3429563)Termination reason: Instruction limit % 91.65/13.94 % (3429563)Termination phase: Saturation % 91.65/13.94 % (3429563)Time elapsed: 0.098 s % 91.65/13.94 % (3429563)Peak memory usage: 90 MB % 91.65/13.94 % (3429563)Instructions burned: 103 (million) % 91.65/13.94 % (3429567)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=4246222201:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/868Mi) % 91.65/13.94 % (3429569)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=3272540497:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi) % 91.65/13.94 % (3429572)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1402477275:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2928 on theBenchmark for (2928ds/36816Mi) % 91.65/13.94 % (3429569)Refutation not found, incomplete strategy % 91.65/13.94 % (3429569)------------------------------ % 91.65/13.94 % (3429569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.65/13.94 % (3429569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.65/13.94 % (3429569)CaDiCaL version: 2.1.3 % 91.65/13.94 % (3429569)Termination reason: Refutation not found, incomplete strategy % 91.65/13.94 % (3429569)Time elapsed: 0.043 s % 91.65/13.94 % (3429569)Peak memory usage: 90 MB % 91.65/13.94 % (3429569)Instructions burned: 44 (million) % 91.65/13.94 % (3429555)Instruction limit reached! % 91.65/13.94 % (3429555)------------------------------ % 91.65/13.94 % (3429555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.65/13.94 % (3429555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.65/13.94 % (3429555)CaDiCaL version: 2.1.3 % 91.65/13.94 % (3429555)Termination reason: Instruction limit % 91.65/13.94 % (3429555)Termination phase: Saturation % 91.65/13.94 % (3429555)Time elapsed: 1.229 s % 91.65/13.94 % (3429555)Peak memory usage: 137 MB % 91.65/13.94 % (3429555)Instructions burned: 1131 (million) % 91.65/13.94 % (3429578)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=766512149:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2924 on theBenchmark for (2924ds/273Mi) % 91.65/13.94 % (3429569)------------------------------ % 91.65/13.94 % (3429569)------------------------------ % 91.65/13.94 % (3429520)Instruction limit reached! % 91.65/13.94 % (3429520)------------------------------ % 91.65/13.94 % (3429520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.65/13.94 % (3429520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.65/13.94 % (3429520)CaDiCaL version: 2.1.3 % 91.65/13.94 % (3429520)Termination reason: Instruction limit % 91.65/13.94 % (3429520)Termination phase: Saturation % 91.65/13.94 % (3429520)Time elapsed: 3.483 s % 91.65/13.94 % (3429520)Peak memory usage: 107 MB % 91.65/13.94 % (3429520)Instructions burned: 4428 (million) % 91.65/13.94 % (3429567)Instruction limit reached! % 91.65/13.94 % (3429567)------------------------------ % 91.65/13.94 % (3429567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.65/13.94 % (3429567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.65/13.94 % (3429567)CaDiCaL version: 2.1.3 % 91.65/13.94 % (3429567)Termination reason: Instruction limit % 91.65/13.94 % (3429567)Termination phase: Saturation % 91.65/13.94 % (3429567)Time elapsed: 0.767 s % 91.65/13.94 % (3429567)Peak memory usage: 123 MB % 91.65/13.94 % (3429567)Instructions burned: 868 (million) % 91.65/13.94 % (3429580)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=2409357324:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2922 on theBenchmark for (2922ds/863Mi) % 91.65/13.94 % (3429578)Instruction limit reached! % 91.65/13.94 % (3429578)------------------------------ % 91.65/13.94 % (3429578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.65/13.94 % (3429578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.65/13.94 % (3429578)CaDiCaL version: 2.1.3 % 91.65/13.94 % (3429578)Termination reason: Instruction limit % 91.65/13.94 % (3429578)Termination phase: Saturation % 91.65/13.94 % (3429578)Time elapsed: 0.294 s % 91.65/13.94 % (3429578)Peak memory usage: 92 MB % 91.65/13.94 % (3429578)Instructions burned: 273 (million) % 91.65/13.94 % (3429565)Instruction limit reached! % 98.15/14.99 % (3429565)------------------------------ % 98.15/14.99 % (3429565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.15/14.99 % (3429565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.15/14.99 % (3429565)CaDiCaL version: 2.1.3 % 98.15/14.99 % (3429565)Termination reason: Instruction limit % 98.15/14.99 % (3429565)Termination phase: Saturation % 98.15/14.99 % (3429565)Time elapsed: 0.989 s % 98.15/14.99 % (3429565)Peak memory usage: 94 MB % 98.15/14.99 % (3429565)Instructions burned: 1100 (million) % 98.15/14.99 % (3429582)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=4155731765:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2920 on theBenchmark for (2920ds/2216Mi) % 98.15/14.99 % (3429581)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1429597514:i=5811:kws=precedence:nm=0:rtra=on_2920 on theBenchmark for (2920ds/5811Mi) % 98.15/14.99 % (3429584)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2379828956:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2919 on theBenchmark for (2919ds/801Mi) % 98.15/14.99 % (3429585)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=705006518:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2918 on theBenchmark for (2918ds/1026Mi) % 98.15/14.99 % (3429585)Refutation not found, incomplete strategy % 98.15/14.99 % (3429585)------------------------------ % 98.15/14.99 % (3429585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.15/14.99 % (3429585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.15/14.99 % (3429585)CaDiCaL version: 2.1.3 % 98.15/14.99 % (3429585)Termination reason: Refutation not found, incomplete strategy % 98.15/14.99 % (3429585)Time elapsed: 0.008 s % 98.15/14.99 % (3429585)Peak memory usage: 87 MB % 98.15/14.99 % (3429585)Instructions burned: 7 (million) % 98.15/14.99 % (3429585)------------------------------ % 98.15/14.99 % (3429585)------------------------------ % 98.15/14.99 % (3429580)Instruction limit reached! % 98.15/14.99 % (3429580)------------------------------ % 98.15/14.99 % (3429580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.15/14.99 % (3429580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.15/14.99 % (3429580)CaDiCaL version: 2.1.3 % 98.15/14.99 % (3429580)Termination reason: Instruction limit % 98.15/14.99 % (3429580)Termination phase: Saturation % 98.15/14.99 % (3429580)Time elapsed: 0.804 s % 98.15/14.99 % (3429580)Peak memory usage: 122 MB % 98.15/14.99 % (3429580)Instructions burned: 863 (million) % 98.15/14.99 % (3429584)Instruction limit reached! % 98.15/14.99 % (3429584)------------------------------ % 98.15/14.99 % (3429584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.15/14.99 % (3429584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.15/14.99 % (3429584)CaDiCaL version: 2.1.3 % 98.15/14.99 % (3429584)Termination reason: Instruction limit % 98.15/14.99 % (3429584)Termination phase: Saturation % 98.15/14.99 % (3429584)Time elapsed: 0.733 s % 98.15/14.99 % (3429584)Peak memory usage: 94 MB % 98.15/14.99 % (3429584)Instructions burned: 802 (million) % 98.15/14.99 % (3429591)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2971514562:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/2127Mi) % 98.15/14.99 % (3429590)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4074609799:i=3509:rtra=on_2911 on theBenchmark for (2911ds/3509Mi) % 98.15/14.99 % (3429591)Refutation not found, incomplete strategy % 98.15/14.99 % (3429591)------------------------------ % 98.15/14.99 % (3429591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.15/14.99 % (3429591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.15/14.99 % (3429591)CaDiCaL version: 2.1.3 % 98.15/14.99 % (3429591)Termination reason: Refutation not found, incomplete strategy % 98.15/14.99 % (3429591)Time elapsed: 0.010 s % 98.15/14.99 % (3429591)Peak memory usage: 88 MB % 98.15/14.99 % (3429591)Instructions burned: 11 (million) % 98.15/14.99 % (3429592)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2285448452:i=1959:rtra=on:fsd=on:proc=on_2909 on theBenchmark for (2909ds/1959Mi) % 98.15/14.99 % (3429591)------------------------------ % 98.15/14.99 % (3429591)------------------------------ % 98.15/14.99 % (3429596)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=932540197:s2a=on:i=3553:nm=0:rtra=on_2905 on theBenchmark for (2905ds/3553Mi) % 138.39/20.45 % (3429582)Instruction limit reached! % 138.39/20.45 % (3429582)------------------------------ % 138.39/20.45 % (3429582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.39/20.45 % (3429582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.39/20.45 % (3429582)CaDiCaL version: 2.1.3 % 138.39/20.45 % (3429582)Termination reason: Instruction limit % 138.39/20.45 % (3429582)Termination phase: Saturation % 138.39/20.45 % (3429582)Time elapsed: 2.205 s % 138.39/20.45 % (3429582)Peak memory usage: 141 MB % 138.39/20.45 % (3429582)Instructions burned: 2216 (million) % 138.39/20.45 % (3429598)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1219991538:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2895 on theBenchmark for (2895ds/3201Mi) % 138.39/20.45 % (3429592)Instruction limit reached! % 138.39/20.45 % (3429592)------------------------------ % 138.39/20.45 % (3429592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.39/20.45 % (3429592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.39/20.45 % (3429592)CaDiCaL version: 2.1.3 % 138.39/20.45 % (3429592)Termination reason: Instruction limit % 138.39/20.45 % (3429592)Termination phase: Saturation % 138.39/20.45 % (3429592)Time elapsed: 1.885 s % 138.39/20.45 % (3429592)Peak memory usage: 144 MB % 138.39/20.45 % (3429592)Instructions burned: 1959 (million) % 138.39/20.45 % (3429600)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=3370506973:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2887 on theBenchmark for (2887ds/4093Mi) % 138.39/20.45 % (3429566)Instruction limit reached! % 138.39/20.45 % (3429566)------------------------------ % 138.39/20.45 % (3429566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.39/20.45 % (3429566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.39/20.45 % (3429566)CaDiCaL version: 2.1.3 % 138.39/20.45 % (3429566)Termination reason: Instruction limit % 138.39/20.45 % (3429566)Termination phase: Saturation % 138.39/20.45 % (3429566)Time elapsed: 5.076 s % 138.39/20.45 % (3429566)Peak memory usage: 121 MB % 138.39/20.45 % (3429566)Instructions burned: 6400 (million) % 138.39/20.45 % (3429590)Instruction limit reached! % 138.39/20.45 % (3429590)------------------------------ % 138.39/20.45 % (3429590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.39/20.45 % (3429590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.39/20.45 % (3429590)CaDiCaL version: 2.1.3 % 138.39/20.45 % (3429590)Termination reason: Instruction limit % 138.39/20.45 % (3429590)Termination phase: Saturation % 138.39/20.45 % (3429590)Time elapsed: 3.402 s % 138.39/20.45 % (3429590)Peak memory usage: 109 MB % 138.39/20.45 % (3429590)Instructions burned: 3509 (million) % 138.39/20.45 % (3429602)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=2916398017:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2877 on theBenchmark for (2877ds/21173Mi) % 138.39/20.45 % (3429602)Refutation not found, incomplete strategy % 138.39/20.45 % (3429602)------------------------------ % 138.39/20.45 % (3429602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.39/20.45 % (3429602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.39/20.45 % (3429602)CaDiCaL version: 2.1.3 % 138.39/20.45 % (3429602)Termination reason: Refutation not found, incomplete strategy % 138.39/20.45 % (3429602)Time elapsed: 0.042 s % 138.39/20.45 % (3429602)Peak memory usage: 113 MB % 138.39/20.45 % (3429602)Instructions burned: 10 (million) % 138.39/20.45 % (3429604)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2453744246:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2875 on theBenchmark for (2875ds/10544Mi) % 138.39/20.45 % (3429602)------------------------------ % 138.39/20.45 % (3429602)------------------------------ % 138.39/20.45 % (3429596)Instruction limit reached! % 138.39/20.45 % (3429596)------------------------------ % 138.39/20.45 % (3429596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.39/20.45 % (3429596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.39/20.45 % (3429596)CaDiCaL version: 2.1.3 % 138.39/20.45 % (3429596)Termination reason: Instruction limit % 138.39/20.45 % (3429596)Termination phase: Saturation % 162.60/23.85 % (3429596)Time elapsed: 3.315 s % 162.60/23.85 % (3429596)Peak memory usage: 112 MB % 162.60/23.85 % (3429596)Instructions burned: 3553 (million) % 162.60/23.85 % (3429606)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2656405963:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2870 on theBenchmark for (2870ds/1262Mi) % 162.60/23.85 % (3429598)Instruction limit reached! % 162.60/23.85 % (3429598)------------------------------ % 162.60/23.85 % (3429598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.60/23.85 % (3429598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.60/23.85 % (3429598)CaDiCaL version: 2.1.3 % 162.60/23.85 % (3429598)Termination reason: Instruction limit % 162.60/23.85 % (3429598)Termination phase: Saturation % 162.60/23.85 % (3429598)Time elapsed: 2.614 s % 162.60/23.85 % (3429598)Peak memory usage: 102 MB % 162.60/23.85 % (3429598)Instructions burned: 3202 (million) % 162.60/23.85 % (3429607)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=111672709:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2869 on theBenchmark for (2869ds/775Mi) % 162.60/23.85 % (3429607)Refutation not found, incomplete strategy % 162.60/23.85 % (3429607)------------------------------ % 162.60/23.85 % (3429607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.60/23.85 % (3429607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.60/23.85 % (3429607)CaDiCaL version: 2.1.3 % 162.60/23.85 % (3429607)Termination reason: Refutation not found, incomplete strategy % 162.60/23.85 % (3429607)Time elapsed: 0.012 s % 162.60/23.85 % (3429607)Peak memory usage: 88 MB % 162.60/23.85 % (3429607)Instructions burned: 12 (million) % 162.60/23.85 % (3429581)Instruction limit reached! % 162.60/23.85 % (3429581)------------------------------ % 162.60/23.85 % (3429581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.60/23.85 % (3429581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.60/23.85 % (3429581)CaDiCaL version: 2.1.3 % 162.60/23.85 % (3429581)Termination reason: Instruction limit % 162.60/23.85 % (3429581)Termination phase: Saturation % 162.60/23.85 % (3429581)Time elapsed: 5.102 s % 162.60/23.85 % (3429581)Peak memory usage: 144 MB % 162.60/23.85 % (3429581)Instructions burned: 5812 (million) % 162.60/23.85 % (3429609)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1131313014:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2866 on theBenchmark for (2866ds/270Mi) % 162.60/23.85 % (3429611)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2352903067:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2866 on theBenchmark for (2866ds/17165Mi) % 162.60/23.85 % (3429607)------------------------------ % 162.60/23.85 % (3429607)------------------------------ % 162.60/23.85 % (3429606)Instruction limit reached! % 162.60/23.85 % (3429606)------------------------------ % 162.60/23.85 % (3429606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.60/23.85 % (3429606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.60/23.85 % (3429606)CaDiCaL version: 2.1.3 % 162.60/23.85 % (3429606)Termination reason: Instruction limit % 162.60/23.85 % (3429606)Termination phase: Saturation % 162.60/23.85 % (3429606)Time elapsed: 0.682 s % 162.60/23.85 % (3429606)Peak memory usage: 125 MB % 162.60/23.85 % (3429606)Instructions burned: 1264 (million) % 162.60/23.85 % (3429609)Instruction limit reached! % 162.60/23.85 % (3429609)------------------------------ % 162.60/23.85 % (3429609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.60/23.85 % (3429609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.60/23.85 % (3429609)CaDiCaL version: 2.1.3 % 162.60/23.85 % (3429609)Termination reason: Instruction limit % 162.60/23.85 % (3429609)Termination phase: Saturation % 162.60/23.85 % (3429609)Time elapsed: 0.275 s % 162.60/23.85 % (3429609)Peak memory usage: 92 MB % 162.60/23.85 % (3429609)Instructions burned: 270 (million) % 162.60/23.85 % (3429614)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2417030812:s2a=on:i=13094:s2at=-1:rtra=on_2862 on theBenchmark for (2862ds/13094Mi) % 162.60/23.85 % (3429616)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=4081992591:i=1783:rtra=on:gtg=position_2861 on theBenchmark for (2861ds/1783Mi) % 162.60/23.85 % (3429615)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1699404269:st=2:i=12633:rtra=on:ss=axioms_2861 on theBenchmark for (2861ds/12633Mi) % 193.44/28.16 % (3429615)Refutation not found, incomplete strategy % 193.44/28.16 % (3429615)------------------------------ % 193.44/28.16 % (3429615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.44/28.16 % (3429615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.44/28.16 % (3429615)CaDiCaL version: 2.1.3 % 193.44/28.16 % (3429615)Termination reason: Refutation not found, incomplete strategy % 193.44/28.16 % (3429615)Time elapsed: 0.009 s % 193.44/28.16 % (3429615)Peak memory usage: 88 MB % 193.44/28.16 % (3429615)Instructions burned: 10 (million) % 193.44/28.16 % (3429615)------------------------------ % 193.44/28.16 % (3429615)------------------------------ % 193.44/28.16 % (3429620)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=1278979914:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2854 on theBenchmark for (2854ds/5451Mi) % 193.44/28.16 % (3429600)Instruction limit reached! % 193.44/28.16 % (3429600)------------------------------ % 193.44/28.16 % (3429600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.44/28.16 % (3429600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.44/28.16 % (3429600)CaDiCaL version: 2.1.3 % 193.44/28.16 % (3429600)Termination reason: Instruction limit % 193.44/28.16 % (3429600)Termination phase: Saturation % 193.44/28.16 % (3429600)Time elapsed: 3.476 s % 193.44/28.16 % (3429600)Peak memory usage: 152 MB % 193.44/28.16 % (3429600)Instructions burned: 4093 (million) % 193.44/28.16 % (3429624)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=1917497374:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2850 on theBenchmark for (2850ds/4975Mi) % 193.44/28.16 % (3429616)Instruction limit reached! % 193.44/28.16 % (3429616)------------------------------ % 193.44/28.16 % (3429616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.44/28.16 % (3429616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.44/28.16 % (3429616)CaDiCaL version: 2.1.3 % 193.44/28.16 % (3429616)Termination reason: Instruction limit % 193.44/28.16 % (3429616)Termination phase: Saturation % 193.44/28.16 % (3429616)Time elapsed: 1.370 s % 193.44/28.16 % (3429616)Peak memory usage: 130 MB % 193.44/28.16 % (3429616)Instructions burned: 1784 (million) % 193.44/28.16 % (3429633)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=1127097788:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2845 on theBenchmark for (2845ds/2076Mi) % 193.44/28.16 % (3429624)Instruction limit reached! % 193.44/28.16 % (3429624)------------------------------ % 193.44/28.16 % (3429624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.44/28.16 % (3429624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.44/28.16 % (3429624)CaDiCaL version: 2.1.3 % 193.44/28.16 % (3429624)Termination reason: Instruction limit % 193.44/28.16 % (3429624)Termination phase: Saturation % 193.44/28.16 % (3429624)Time elapsed: 2.095 s % 193.44/28.16 % (3429624)Peak memory usage: 146 MB % 193.44/28.16 % (3429624)Instructions burned: 4978 (million) % 193.44/28.16 % (3429648)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2084523195:i=5145:rtra=on_2826 on theBenchmark for (2826ds/5145Mi) % 193.44/28.16 % (3429633)Instruction limit reached! % 193.44/28.16 % (3429633)------------------------------ % 193.44/28.16 % (3429633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.44/28.16 % (3429633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.44/28.16 % (3429633)CaDiCaL version: 2.1.3 % 193.44/28.16 % (3429633)Termination reason: Instruction limit % 193.44/28.16 % (3429633)Termination phase: Saturation % 193.44/28.16 % (3429633)Time elapsed: 2.069 s % 193.44/28.16 % (3429633)Peak memory usage: 141 MB % 193.44/28.16 % (3429633)Instructions burned: 2077 (million) % 193.44/28.16 % (3429650)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=628038603:i=3509:rtra=on_2821 on theBenchmark for (2821ds/3509Mi) % 193.44/28.16 % (3429620)Instruction limit reached! % 193.44/28.16 % (3429620)------------------------------ % 193.44/28.16 % (3429620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.44/28.16 % (3429620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.44/28.16 % (3429620)CaDiCaL version: 2.1.3 % 193.44/28.16 % (3429620)Termination reason: Instruction limit % 269.77/38.96 % (3429620)Termination phase: Saturation % 269.77/38.96 % (3429620)Time elapsed: 4.810 s % 269.77/38.96 % (3429620)Peak memory usage: 147 MB % 269.77/38.96 % (3429620)Instructions burned: 5451 (million) % 269.77/38.96 % (3429658)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3143213754:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2804 on theBenchmark for (2804ds/13800Mi) % 269.77/38.96 % (3429658)Refutation not found, incomplete strategy % 269.77/38.96 % (3429658)------------------------------ % 269.77/38.96 % (3429658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.77/38.96 % (3429658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.77/38.96 % (3429658)CaDiCaL version: 2.1.3 % 269.77/38.96 % (3429658)Termination reason: Refutation not found, incomplete strategy % 269.77/38.96 % (3429658)Time elapsed: 0.011 s % 269.77/38.96 % (3429658)Peak memory usage: 88 MB % 269.77/38.96 % (3429658)Instructions burned: 11 (million) % 269.77/38.96 % (3429648)Instruction limit reached! % 269.77/38.96 % (3429648)------------------------------ % 269.77/38.96 % (3429648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.77/38.96 % (3429648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.77/38.96 % (3429648)CaDiCaL version: 2.1.3 % 269.77/38.96 % (3429648)Termination reason: Instruction limit % 269.77/38.96 % (3429648)Termination phase: Saturation % 269.77/38.96 % (3429648)Time elapsed: 2.317 s % 269.77/38.96 % (3429648)Peak memory usage: 124 MB % 269.77/38.96 % (3429648)Instructions burned: 5146 (million) % 269.77/38.96 % (3429660)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3738735146:i=1412:rtra=on:fsd=on:proc=on_2800 on theBenchmark for (2800ds/1412Mi) % 269.77/38.96 % (3429658)------------------------------ % 269.77/38.96 % (3429658)------------------------------ % 269.77/38.96 % (3429662)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 % 269.77/38.96 % (3429662)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2495107570:i=11747:aac=none:nm=0:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/11747Mi) % 269.77/38.96 % (3429660)Instruction limit reached! % 269.77/38.96 % (3429660)------------------------------ % 269.77/38.96 % (3429660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.77/38.96 % (3429660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.77/38.96 % (3429660)CaDiCaL version: 2.1.3 % 269.77/38.96 % (3429660)Termination reason: Instruction limit % 269.77/38.96 % (3429660)Termination phase: Saturation % 269.77/38.96 % (3429660)Time elapsed: 0.659 s % 269.77/38.96 % (3429660)Peak memory usage: 138 MB % 269.77/38.96 % (3429660)Instructions burned: 1413 (million) % 269.77/38.96 % (3429672)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=80008193:s2a=on:i=3553:nm=0:rtra=on_2791 on theBenchmark for (2791ds/3553Mi) % 269.77/38.96 % (3429650)Instruction limit reached! % 269.77/38.96 % (3429650)------------------------------ % 269.77/38.96 % (3429650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.77/38.96 % (3429650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.77/38.96 % (3429650)CaDiCaL version: 2.1.3 % 269.77/38.96 % (3429650)Termination reason: Instruction limit % 269.77/38.96 % (3429650)Termination phase: Saturation % 269.77/38.96 % (3429650)Time elapsed: 3.211 s % 269.77/38.96 % (3429650)Peak memory usage: 109 MB % 269.77/38.96 % (3429650)Instructions burned: 3510 (million) % 269.77/38.96 % (3429674)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=139816362:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/3201Mi) % 269.77/38.96 % (3429604)Instruction limit reached! % 269.77/38.96 % (3429604)------------------------------ % 269.77/38.96 % (3429604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.77/38.96 % (3429604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.77/38.96 % (3429604)CaDiCaL version: 2.1.3 % 269.77/38.96 % (3429604)Termination reason: Instruction limit % 269.77/38.96 % (3429604)Termination phase: Saturation % 269.77/38.96 % (3429604)Time elapsed: 10.226 s % 269.77/38.96 % (3429604)Peak memory usage: 241 MB % 269.77/38.96 % (3429604)Instructions burned: 10544 (million) % 269.77/38.96 % (3429672)Instruction limit reached! % 269.77/38.96 % (3429672)------------------------------ % 269.77/38.96 % (3429672)Version: Vampire 5.0.1 (Terminated %------------------------------------------------------------------------------