%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC444_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n004.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:03:58 PM UTC 2026 % Result : Timeout 300.33s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC444_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.16 % Computer : n004.cluster.edu % 0.09/0.16 % Model : x86_64 x86_64 % 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.16 % Memory : 8046.5625MB % 0.09/0.16 % OS : Linux 6.8.0-71-generic % 0.09/0.16 % CPULimit : 300 % 0.09/0.16 % WCLimit : 300 % 0.09/0.16 % DateTime : Mon Sep 28 09:38:07 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.20 Running first-order theorem proving % 0.09/0.20 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.57/1.21 % (236307)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.57/1.21 % (236318)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4104466566:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.57/1.21 % (236318)Instruction limit reached! % 5.57/1.21 % (236318)------------------------------ % 5.57/1.21 % (236318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.21 % (236318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.21 % (236318)CaDiCaL version: 2.1.3 % 5.57/1.21 % (236318)Termination reason: Instruction limit % 5.57/1.21 % (236318)Termination phase: Saturation % 5.57/1.21 % (236318)Time elapsed: 0.028 s % 5.57/1.21 % (236318)Peak memory usage: 116 MB % 5.57/1.21 % (236318)Instructions burned: 34 (million) % 5.57/1.21 % (236317)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1113236331:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.57/1.21 % (236313)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1733195430:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.57/1.21 % (236315)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1291584560:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.57/1.21 % (236314)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=8877921:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.57/1.21 % (236315)Instruction limit reached! % 5.57/1.21 % (236315)------------------------------ % 5.57/1.21 % (236315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.21 % (236315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.21 % (236315)CaDiCaL version: 2.1.3 % 5.57/1.21 % (236315)Termination reason: Instruction limit % 5.57/1.21 % (236315)Termination phase: Saturation % 5.57/1.21 % (236315)Time elapsed: 0.005 s % 5.57/1.21 % (236315)Peak memory usage: 88 MB % 5.57/1.21 % (236315)Instructions burned: 7 (million) % 5.57/1.21 % (236312)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1998128331:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.57/1.21 % (236316)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2067060935:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.57/1.21 % (236316)Instruction limit reached! % 5.57/1.21 % (236316)------------------------------ % 5.57/1.21 % (236316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.21 % (236316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.21 % (236316)CaDiCaL version: 2.1.3 % 5.57/1.21 % (236316)Termination reason: Instruction limit % 5.57/1.21 % (236316)Termination phase: Saturation % 5.57/1.21 % (236316)Time elapsed: 0.006 s % 5.57/1.21 % (236316)Peak memory usage: 89 MB % 5.57/1.21 % (236316)Instructions burned: 5 (million) % 5.57/1.21 % (236317)Instruction limit reached! % 5.57/1.21 % (236317)------------------------------ % 5.57/1.21 % (236317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.21 % (236317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.21 % (236317)CaDiCaL version: 2.1.3 % 5.57/1.21 % (236317)Termination reason: Instruction limit % 5.57/1.21 % (236317)Termination phase: Saturation % 5.57/1.21 % (236317)Time elapsed: 0.057 s % 5.57/1.21 % (236317)Peak memory usage: 115 MB % 5.57/1.21 % (236317)Instructions burned: 46 (million) % 5.57/1.21 % (236312)Instruction limit reached! % 5.57/1.21 % (236312)------------------------------ % 5.57/1.21 % (236312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.57/1.21 % (236312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.21 % (236312)CaDiCaL version: 2.1.3 % 5.57/1.21 % (236312)Termination reason: Instruction limit % 5.57/1.21 % (236312)Termination phase: Saturation % 5.57/1.21 % (236312)Time elapsed: 0.041 s % 5.57/1.21 % (236312)Peak memory usage: 115 MB % 5.57/1.21 % (236312)Instructions burned: 12 (million) % 5.57/1.21 % (236320)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3414973310:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 5.57/1.21 % (236320)Instruction limit reached! % 5.57/1.21 % (236320)------------------------------ % 5.57/1.21 % (236320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.48 % (236320)CaDiCaL version: 2.1.3 % 6.47/1.48 % (236320)Termination reason: Instruction limit % 6.47/1.48 % (236320)Termination phase: Saturation % 6.47/1.48 % (236320)Time elapsed: 0.007 s % 6.47/1.48 % (236320)Peak memory usage: 88 MB % 6.47/1.48 % (236320)Instructions burned: 17 (million) % 6.47/1.48 % (236314)Instruction limit reached! % 6.47/1.48 % (236314)------------------------------ % 6.47/1.48 % (236314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.48 % (236314)CaDiCaL version: 2.1.3 % 6.47/1.48 % (236314)Termination reason: Instruction limit % 6.47/1.48 % (236314)Termination phase: Saturation % 6.47/1.48 % (236314)Time elapsed: 0.236 s % 6.47/1.48 % (236314)Peak memory usage: 118 MB % 6.47/1.48 % (236314)Instructions burned: 201 (million) % 6.47/1.48 % (236325)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=1215351822:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 6.47/1.48 % (236313)Instruction limit reached! % 6.47/1.48 % (236313)------------------------------ % 6.47/1.48 % (236313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.48 % (236313)CaDiCaL version: 2.1.3 % 6.47/1.48 % (236313)Termination reason: Instruction limit % 6.47/1.48 % (236313)Termination phase: Saturation % 6.47/1.48 % (236313)Time elapsed: 0.279 s % 6.47/1.48 % (236313)Peak memory usage: 117 MB % 6.47/1.48 % (236313)Instructions burned: 307 (million) % 6.47/1.48 % (236325)Instruction limit reached! % 6.47/1.48 % (236325)------------------------------ % 6.47/1.48 % (236325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.48 % (236325)CaDiCaL version: 2.1.3 % 6.47/1.48 % (236325)Termination reason: Instruction limit % 6.47/1.48 % (236325)Termination phase: Saturation % 6.47/1.48 % (236325)Time elapsed: 0.024 s % 6.47/1.48 % (236325)Peak memory usage: 89 MB % 6.47/1.48 % (236325)Instructions burned: 30 (million) % 6.47/1.48 % (236336)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2516221902:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 6.47/1.48 % (236338)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=815742637:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 6.47/1.48 % (236337)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=499427829:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 6.47/1.48 % (236342)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2191214941:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.47/1.48 % (236336)Instruction limit reached! % 6.47/1.48 % (236336)------------------------------ % 6.47/1.48 % (236336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.48 % (236336)CaDiCaL version: 2.1.3 % 6.47/1.48 % (236336)Termination reason: Instruction limit % 6.47/1.48 % (236336)Termination phase: Saturation % 6.47/1.48 % (236336)Time elapsed: 0.019 s % 6.47/1.48 % (236336)Peak memory usage: 90 MB % 6.47/1.48 % (236336)Instructions burned: 17 (million) % 6.47/1.48 % (236338)Instruction limit reached! % 6.47/1.48 % (236338)------------------------------ % 6.47/1.48 % (236338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.48 % (236338)CaDiCaL version: 2.1.3 % 6.47/1.48 % (236338)Termination reason: Instruction limit % 6.47/1.48 % (236338)Termination phase: Saturation % 6.47/1.48 % (236338)Time elapsed: 0.027 s % 6.47/1.48 % (236338)Peak memory usage: 89 MB % 6.47/1.48 % (236338)Instructions burned: 27 (million) % 6.47/1.48 % (236337)Instruction limit reached! % 6.47/1.48 % (236337)------------------------------ % 6.47/1.48 % (236337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.48 % (236337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.78 % (236337)CaDiCaL version: 2.1.3 % 7.88/1.78 % (236337)Termination reason: Instruction limit % 7.88/1.78 % (236337)Termination phase: Saturation % 7.88/1.78 % (236337)Time elapsed: 0.030 s % 7.88/1.78 % (236337)Peak memory usage: 89 MB % 7.88/1.78 % (236337)Instructions burned: 25 (million) % 7.88/1.78 % (236342)Instruction limit reached! % 7.88/1.78 % (236342)------------------------------ % 7.88/1.78 % (236342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.88/1.78 % (236342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.78 % (236342)CaDiCaL version: 2.1.3 % 7.88/1.78 % (236342)Termination reason: Instruction limit % 7.88/1.78 % (236342)Termination phase: Saturation % 7.88/1.78 % (236342)Time elapsed: 0.034 s % 7.88/1.78 % (236342)Peak memory usage: 89 MB % 7.88/1.78 % (236342)Instructions burned: 86 (million) % 7.88/1.78 % (236349)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1782779925:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 7.88/1.78 % (236349)Instruction limit reached! % 7.88/1.78 % (236349)------------------------------ % 7.88/1.78 % (236349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.88/1.78 % (236349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.78 % (236349)CaDiCaL version: 2.1.3 % 7.88/1.78 % (236349)Termination reason: Instruction limit % 7.88/1.78 % (236349)Termination phase: Saturation % 7.88/1.78 % (236349)Time elapsed: 0.002 s % 7.88/1.78 % (236349)Peak memory usage: 88 MB % 7.88/1.78 % (236349)Instructions burned: 2 (million) % 7.88/1.78 % (236353)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3717165055:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 7.88/1.78 % (236354)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2550659045:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 7.88/1.78 % (236353)Refutation not found, incomplete strategy % 7.88/1.78 % (236353)------------------------------ % 7.88/1.78 % (236353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.88/1.78 % (236353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.78 % (236353)CaDiCaL version: 2.1.3 % 7.88/1.78 % (236353)Termination reason: Refutation not found, incomplete strategy % 7.88/1.78 % (236353)Time elapsed: 0.004 s % 7.88/1.78 % (236353)Peak memory usage: 89 MB % 7.88/1.78 % (236353)Instructions burned: 2 (million) % 7.88/1.78 % (236354)Instruction limit reached! % 7.88/1.78 % (236354)------------------------------ % 7.88/1.78 % (236354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.88/1.78 % (236354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.78 % (236354)CaDiCaL version: 2.1.3 % 7.88/1.78 % (236354)Termination reason: Instruction limit % 7.88/1.78 % (236354)Termination phase: Saturation % 7.88/1.78 % (236354)Time elapsed: 0.006 s % 7.88/1.78 % (236354)Peak memory usage: 89 MB % 7.88/1.78 % (236354)Instructions burned: 4 (million) % 7.88/1.78 % (236366)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4057060322:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi) % 7.88/1.78 % (236364)lrs+10_1_thi=all:si=on:fd=off:random_seed=4065078274:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 7.88/1.78 % (236366)Instruction limit reached! % 7.88/1.78 % (236366)------------------------------ % 7.88/1.78 % (236366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.88/1.78 % (236366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.88/1.78 % (236366)CaDiCaL version: 2.1.3 % 7.88/1.78 % (236366)Termination reason: Instruction limit % 7.88/1.78 % (236366)Termination phase: Saturation % 7.88/1.78 % (236366)Time elapsed: 0.002 s % 7.88/1.78 % (236366)Peak memory usage: 89 MB % 7.88/1.78 % (236366)Instructions burned: 2 (million) % 7.88/1.78 % (236363)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=412054773:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 7.88/1.78 % (236365)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=2497175498:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 7.88/1.78 % (236364)Instruction limit reached! % 7.88/1.78 % (236364)------------------------------ % 12.41/2.23 % (236364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236364)CaDiCaL version: 2.1.3 % 12.41/2.23 % (236364)Termination reason: Instruction limit % 12.41/2.23 % (236364)Termination phase: Saturation % 12.41/2.23 % (236364)Time elapsed: 0.066 s % 12.41/2.23 % (236364)Peak memory usage: 116 MB % 12.41/2.23 % (236364)Instructions burned: 54 (million) % 12.41/2.23 % (236365)Instruction limit reached! % 12.41/2.23 % (236365)------------------------------ % 12.41/2.23 % (236365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236365)CaDiCaL version: 2.1.3 % 12.41/2.23 % (236365)Termination reason: Instruction limit % 12.41/2.23 % (236365)Termination phase: Saturation % 12.41/2.23 % (236365)Time elapsed: 0.011 s % 12.41/2.23 % (236365)Peak memory usage: 88 MB % 12.41/2.23 % (236365)Instructions burned: 8 (million) % 12.41/2.23 % (236363)Instruction limit reached! % 12.41/2.23 % (236363)------------------------------ % 12.41/2.23 % (236363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236363)CaDiCaL version: 2.1.3 % 12.41/2.23 % (236363)Termination reason: Instruction limit % 12.41/2.23 % (236363)Termination phase: Saturation % 12.41/2.23 % (236363)Time elapsed: 0.141 s % 12.41/2.23 % (236363)Peak memory usage: 134 MB % 12.41/2.23 % (236363)Instructions burned: 66 (million) % 12.41/2.23 % (236374)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=652546160:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi) % 12.41/2.23 % (236374)Instruction limit reached! % 12.41/2.23 % (236374)------------------------------ % 12.41/2.23 % (236374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236374)CaDiCaL version: 2.1.3 % 12.41/2.23 % (236374)Termination reason: Instruction limit % 12.41/2.23 % (236374)Termination phase: Saturation % 12.41/2.23 % (236374)Time elapsed: 0.003 s % 12.41/2.23 % (236374)Peak memory usage: 88 MB % 12.41/2.23 % (236374)Instructions burned: 2 (million) % 12.41/2.23 % (236385)dis+10_1_si=on:random_seed=233298612:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 12.41/2.23 % (236385)Instruction limit reached! % 12.41/2.23 % (236385)------------------------------ % 12.41/2.23 % (236385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236385)CaDiCaL version: 2.1.3 % 12.41/2.23 % (236385)Termination reason: Instruction limit % 12.41/2.23 % (236385)Termination phase: Saturation % 12.41/2.23 % (236385)Time elapsed: 0.005 s % 12.41/2.23 % (236385)Peak memory usage: 88 MB % 12.41/2.23 % (236385)Instructions burned: 11 (million) % 12.41/2.23 % (236382)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2407082792:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 12.41/2.23 % (236395)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2458993123:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 12.41/2.23 % (236394)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3852636849:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 12.41/2.23 % (236394)Refutation not found, incomplete strategy % 12.41/2.23 % (236394)------------------------------ % 12.41/2.23 % (236394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236394)CaDiCaL version: 2.1.3 % 12.41/2.23 % (236394)Termination reason: Refutation not found, incomplete strategy % 12.41/2.23 % (236394)Time elapsed: 0.003 s % 12.41/2.23 % (236394)Peak memory usage: 89 MB % 12.41/2.23 % (236394)Instructions burned: 3 (million) % 12.41/2.23 % (236395)Instruction limit reached! % 12.41/2.23 % (236395)------------------------------ % 12.41/2.23 % (236395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.41/2.23 % (236395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.41/2.23 % (236395)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236395)Termination reason: Instruction limit % 13.22/2.51 % (236395)Termination phase: Saturation % 13.22/2.51 % (236395)Time elapsed: 0.039 s % 13.22/2.51 % (236395)Peak memory usage: 89 MB % 13.22/2.51 % (236395)Instructions burned: 35 (million) % 13.22/2.51 % (236353)------------------------------ % 13.22/2.51 % (236353)------------------------------ % 13.22/2.51 % (236405)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2969822588:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 13.22/2.51 % (236397)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2936173058:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 13.22/2.51 % (236397)Instruction limit reached! % 13.22/2.51 % (236397)------------------------------ % 13.22/2.51 % (236397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.22/2.51 % (236397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.22/2.51 % (236397)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236397)Termination reason: Instruction limit % 13.22/2.51 % (236397)Termination phase: Saturation % 13.22/2.51 % (236397)Time elapsed: 0.003 s % 13.22/2.51 % (236397)Peak memory usage: 88 MB % 13.22/2.51 % (236397)Instructions burned: 2 (million) % 13.22/2.51 % (236382)Instruction limit reached! % 13.22/2.51 % (236382)------------------------------ % 13.22/2.51 % (236382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.22/2.51 % (236382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.22/2.51 % (236382)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236382)Termination reason: Instruction limit % 13.22/2.51 % (236382)Termination phase: Saturation % 13.22/2.51 % (236382)Time elapsed: 0.160 s % 13.22/2.51 % (236382)Peak memory usage: 116 MB % 13.22/2.51 % (236382)Instructions burned: 127 (million) % 13.22/2.51 % (236401)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4118436825:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 13.22/2.51 % (236401)Instruction limit reached! % 13.22/2.51 % (236401)------------------------------ % 13.22/2.51 % (236401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.22/2.51 % (236401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.22/2.51 % (236401)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236401)Termination reason: Instruction limit % 13.22/2.51 % (236401)Termination phase: Saturation % 13.22/2.51 % (236401)Time elapsed: 0.011 s % 13.22/2.51 % (236401)Peak memory usage: 88 MB % 13.22/2.51 % (236401)Instructions burned: 8 (million) % 13.22/2.51 % (236418)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=222354379:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 13.22/2.51 % (236405)Instruction limit reached! % 13.22/2.51 % (236405)------------------------------ % 13.22/2.51 % (236405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.22/2.51 % (236405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.22/2.51 % (236405)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236405)Termination reason: Instruction limit % 13.22/2.51 % (236405)Termination phase: Saturation % 13.22/2.51 % (236405)Time elapsed: 0.165 s % 13.22/2.51 % (236405)Peak memory usage: 91 MB % 13.22/2.51 % (236405)Instructions burned: 372 (million) % 13.22/2.51 % (236418)Refutation not found, incomplete strategy % 13.22/2.51 % (236418)------------------------------ % 13.22/2.51 % (236418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.22/2.51 % (236418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.22/2.51 % (236418)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236418)Termination reason: Refutation not found, incomplete strategy % 13.22/2.51 % (236418)Time elapsed: 0.030 s % 13.22/2.51 % (236418)Peak memory usage: 116 MB % 13.22/2.51 % (236418)Instructions burned: 7 (million) % 13.22/2.51 % (236416)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2000938500:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 13.22/2.51 % (236416)Instruction limit reached! % 13.22/2.51 % (236416)------------------------------ % 13.22/2.51 % (236416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.22/2.51 % (236416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.22/2.51 % (236416)CaDiCaL version: 2.1.3 % 13.22/2.51 % (236416)Termination reason: Instruction limit % 13.22/2.51 % (236416)Termination phase: Saturation % 15.38/3.03 % (236416)Time elapsed: 0.046 s % 15.38/3.03 % (236416)Peak memory usage: 116 MB % 15.38/3.03 % (236416)Instructions burned: 13 (million) % 15.38/3.03 % (236394)------------------------------ % 15.38/3.03 % (236394)------------------------------ % 15.38/3.03 % (236422)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4022412862:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 15.38/3.03 % (236424)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4116485740:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 15.38/3.03 % (236434)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=3148951844:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 15.38/3.03 % (236422)Instruction limit reached! % 15.38/3.03 % (236422)------------------------------ % 15.38/3.03 % (236422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.38/3.03 % (236422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.38/3.03 % (236422)CaDiCaL version: 2.1.3 % 15.38/3.03 % (236422)Termination reason: Instruction limit % 15.38/3.03 % (236422)Termination phase: Saturation % 15.38/3.03 % (236422)Time elapsed: 0.013 s % 15.38/3.03 % (236422)Peak memory usage: 88 MB % 15.38/3.03 % (236422)Instructions burned: 11 (million) % 15.38/3.03 % (236436)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=3680797893:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi) % 15.38/3.03 % (236434)Instruction limit reached! % 15.38/3.03 % (236434)------------------------------ % 15.38/3.03 % (236434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.38/3.03 % (236434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.38/3.03 % (236434)CaDiCaL version: 2.1.3 % 15.38/3.03 % (236434)Termination reason: Instruction limit % 15.38/3.03 % (236434)Termination phase: Saturation % 15.38/3.03 % (236434)Time elapsed: 0.056 s % 15.38/3.03 % (236434)Peak memory usage: 90 MB % 15.38/3.03 % (236434)Instructions burned: 76 (million) % 15.38/3.03 % (236424)Instruction limit reached! % 15.38/3.03 % (236424)------------------------------ % 15.38/3.03 % (236424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.38/3.03 % (236424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.38/3.03 % (236424)CaDiCaL version: 2.1.3 % 15.38/3.03 % (236424)Termination reason: Instruction limit % 15.38/3.03 % (236424)Termination phase: Saturation % 15.38/3.03 % (236424)Time elapsed: 0.142 s % 15.38/3.03 % (236424)Peak memory usage: 133 MB % 15.38/3.03 % (236424)Instructions burned: 71 (million) % 15.38/3.03 % (236442)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3835603544:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 15.38/3.03 % (236418)------------------------------ % 15.38/3.03 % (236418)------------------------------ % 15.38/3.03 % (236436)Instruction limit reached! % 15.38/3.03 % (236436)------------------------------ % 15.38/3.03 % (236436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.38/3.03 % (236436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.38/3.03 % (236436)CaDiCaL version: 2.1.3 % 15.38/3.03 % (236436)Termination reason: Instruction limit % 15.38/3.03 % (236436)Termination phase: Saturation % 15.38/3.03 % (236436)Time elapsed: 0.152 s % 15.38/3.03 % (236436)Peak memory usage: 90 MB % 15.38/3.03 % (236436)Instructions burned: 295 (million) % 15.38/3.03 % (236448)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=26404770:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 15.38/3.03 % (236457)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=333782223:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 15.38/3.03 % (236454)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2427718893:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 15.38/3.03 % (236442)Instruction limit reached! % 15.38/3.03 % (236442)------------------------------ % 15.38/3.03 % (236442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.38/3.03 % (236442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.38/3.03 % (236442)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236442)Termination reason: Instruction limit % 20.57/3.47 % (236442)Termination phase: Saturation % 20.57/3.47 % (236442)Time elapsed: 0.161 s % 20.57/3.47 % (236442)Peak memory usage: 117 MB % 20.57/3.47 % (236442)Instructions burned: 131 (million) % 20.57/3.47 % (236466)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=464500939:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 20.57/3.47 % (236448)Instruction limit reached! % 20.57/3.47 % (236448)------------------------------ % 20.57/3.47 % (236448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.57/3.47 % (236448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.57/3.47 % (236448)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236448)Termination reason: Instruction limit % 20.57/3.47 % (236448)Termination phase: Saturation % 20.57/3.47 % (236448)Time elapsed: 0.179 s % 20.57/3.47 % (236448)Peak memory usage: 133 MB % 20.57/3.47 % (236448)Instructions burned: 131 (million) % 20.57/3.47 % (236454)Instruction limit reached! % 20.57/3.47 % (236454)------------------------------ % 20.57/3.47 % (236454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.57/3.47 % (236454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.57/3.47 % (236454)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236454)Termination reason: Instruction limit % 20.57/3.47 % (236454)Termination phase: Saturation % 20.57/3.47 % (236454)Time elapsed: 0.103 s % 20.57/3.47 % (236454)Peak memory usage: 133 MB % 20.57/3.47 % (236454)Instructions burned: 40 (million) % 20.57/3.47 % (236466)Instruction limit reached! % 20.57/3.47 % (236466)------------------------------ % 20.57/3.47 % (236466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.57/3.47 % (236466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.57/3.47 % (236466)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236466)Termination reason: Instruction limit % 20.57/3.47 % (236466)Termination phase: Saturation % 20.57/3.47 % (236466)Time elapsed: 0.093 s % 20.57/3.47 % (236466)Peak memory usage: 116 MB % 20.57/3.47 % (236466)Instructions burned: 260 (million) % 20.57/3.47 % (236463)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1053396998:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 20.57/3.47 % (236464)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=308870025:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 20.57/3.47 % (236457)Instruction limit reached! % 20.57/3.47 % (236457)------------------------------ % 20.57/3.47 % (236457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.57/3.47 % (236457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.57/3.47 % (236457)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236457)Termination reason: Instruction limit % 20.57/3.47 % (236457)Termination phase: Saturation % 20.57/3.47 % (236457)Time elapsed: 0.246 s % 20.57/3.47 % (236457)Peak memory usage: 90 MB % 20.57/3.47 % (236457)Instructions burned: 307 (million) % 20.57/3.47 % (236480)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1929431768:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 20.57/3.47 % (236480)Refutation not found, incomplete strategy % 20.57/3.47 % (236480)------------------------------ % 20.57/3.47 % (236480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.57/3.47 % (236480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.57/3.47 % (236480)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236480)Termination reason: Refutation not found, incomplete strategy % 20.57/3.47 % (236480)Time elapsed: 0.018 s % 20.57/3.47 % (236480)Peak memory usage: 115 MB % 20.57/3.47 % (236480)Instructions burned: 8 (million) % 20.57/3.47 % (236476)dis+10_1_si=on:random_seed=4078079468:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 20.57/3.47 % (236464)Instruction limit reached! % 20.57/3.47 % (236464)------------------------------ % 20.57/3.47 % (236464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.57/3.47 % (236464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.57/3.47 % (236464)CaDiCaL version: 2.1.3 % 20.57/3.47 % (236464)Termination reason: Instruction limit % 20.57/3.47 % (236464)Termination phase: Saturation % 20.57/3.47 % (236464)Time elapsed: 0.163 s % 20.57/3.47 % (236464)Peak memory usage: 118 MB % 22.18/3.98 % (236464)Instructions burned: 132 (million) % 22.18/3.98 % (236478)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3116692454:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 22.18/3.98 % (236479)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1117265110:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi) % 22.18/3.98 % (236480)------------------------------ % 22.18/3.98 % (236480)------------------------------ % 22.18/3.98 % (236489)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=664600432:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi) % 22.18/3.98 % (236479)Instruction limit reached! % 22.18/3.98 % (236479)------------------------------ % 22.18/3.98 % (236479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.18/3.98 % (236479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.98 % (236479)CaDiCaL version: 2.1.3 % 22.18/3.98 % (236479)Termination reason: Instruction limit % 22.18/3.98 % (236479)Termination phase: Saturation % 22.18/3.98 % (236479)Time elapsed: 0.149 s % 22.18/3.98 % (236479)Peak memory usage: 90 MB % 22.18/3.98 % (236479)Instructions burned: 141 (million) % 22.18/3.98 % (236492)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=1763273210:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 22.18/3.98 % (236489)Instruction limit reached! % 22.18/3.98 % (236489)------------------------------ % 22.18/3.98 % (236489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.18/3.98 % (236489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.98 % (236489)CaDiCaL version: 2.1.3 % 22.18/3.98 % (236489)Termination reason: Instruction limit % 22.18/3.98 % (236489)Termination phase: Saturation % 22.18/3.98 % (236489)Time elapsed: 0.105 s % 22.18/3.98 % (236489)Peak memory usage: 89 MB % 22.18/3.98 % (236489)Instructions burned: 122 (million) % 22.18/3.98 % (236500)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=1397847552:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 22.18/3.98 % (236500)Instruction limit reached! % 22.18/3.98 % (236500)------------------------------ % 22.18/3.98 % (236500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.18/3.98 % (236500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.98 % (236500)CaDiCaL version: 2.1.3 % 22.18/3.98 % (236500)Termination reason: Instruction limit % 22.18/3.98 % (236500)Termination phase: Saturation % 22.18/3.98 % (236500)Time elapsed: 0.043 s % 22.18/3.98 % (236500)Peak memory usage: 117 MB % 22.18/3.98 % (236500)Instructions burned: 39 (million) % 22.18/3.98 % (236492)Instruction limit reached! % 22.18/3.98 % (236492)------------------------------ % 22.18/3.98 % (236492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.18/3.98 % (236492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.98 % (236492)CaDiCaL version: 2.1.3 % 22.18/3.98 % (236492)Termination reason: Instruction limit % 22.18/3.98 % (236492)Termination phase: Saturation % 22.18/3.98 % (236492)Time elapsed: 0.137 s % 22.18/3.98 % (236492)Peak memory usage: 117 MB % 22.18/3.98 % (236492)Instructions burned: 128 (million) % 22.18/3.98 % (236478)Instruction limit reached! % 22.18/3.98 % (236478)------------------------------ % 22.18/3.98 % (236478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.18/3.98 % (236478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.98 % (236478)CaDiCaL version: 2.1.3 % 22.18/3.98 % (236478)Termination reason: Instruction limit % 22.18/3.98 % (236478)Termination phase: Saturation % 22.18/3.98 % (236478)Time elapsed: 0.328 s % 22.18/3.98 % (236478)Peak memory usage: 93 MB % 22.18/3.98 % (236478)Instructions burned: 383 (million) % 22.18/3.98 % (236505)dis+1010_1_to=kbo:si=on:random_seed=464535864:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 22.18/3.98 % (236463)Instruction limit reached! % 22.18/3.98 % (236463)------------------------------ % 22.18/3.98 % (236463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.18/3.98 % (236463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.98 % (236463)CaDiCaL version: 2.1.3 % 22.18/3.98 % (236463)Termination reason: Instruction limit % 22.18/3.98 % (236463)Termination phase: Saturation % 27.79/4.53 % (236463)Time elapsed: 0.690 s % 27.79/4.53 % (236463)Peak memory usage: 137 MB % 27.79/4.53 % (236463)Instructions burned: 598 (million) % 27.79/4.53 % (236512)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=501547840:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi) % 27.79/4.53 % (236514)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1165160156:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi) % 27.79/4.53 % (236515)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2261418096:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi) % 27.79/4.53 % (236513)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1400197373:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi) % 27.79/4.53 % (236505)Instruction limit reached! % 27.79/4.53 % (236505)------------------------------ % 27.79/4.53 % (236505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.79/4.53 % (236505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.79/4.53 % (236505)CaDiCaL version: 2.1.3 % 27.79/4.53 % (236505)Termination reason: Instruction limit % 27.79/4.53 % (236505)Termination phase: Saturation % 27.79/4.53 % (236505)Time elapsed: 0.188 s % 27.79/4.53 % (236505)Peak memory usage: 91 MB % 27.79/4.53 % (236505)Instructions burned: 178 (million) % 27.79/4.53 % (236523)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=762092574:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi) % 27.79/4.53 % (236515)Refutation not found, incomplete strategy % 27.79/4.53 % (236515)------------------------------ % 27.79/4.53 % (236515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.79/4.53 % (236515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.79/4.53 % (236515)CaDiCaL version: 2.1.3 % 27.79/4.53 % (236515)Termination reason: Refutation not found, incomplete strategy % 27.79/4.53 % (236515)Time elapsed: 0.043 s % 27.79/4.53 % (236515)Peak memory usage: 116 MB % 27.79/4.53 % (236515)Instructions burned: 9 (million) % 27.79/4.53 % (236476)Instruction limit reached! % 27.79/4.53 % (236476)------------------------------ % 27.79/4.53 % (236476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.79/4.53 % (236476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.79/4.53 % (236476)CaDiCaL version: 2.1.3 % 27.79/4.53 % (236476)Termination reason: Instruction limit % 27.79/4.53 % (236476)Termination phase: Saturation % 27.79/4.53 % (236476)Time elapsed: 0.918 s % 27.79/4.53 % (236476)Peak memory usage: 94 MB % 27.79/4.53 % (236476)Instructions burned: 1001 (million) % 27.79/4.53 % (236514)Instruction limit reached! % 27.79/4.53 % (236514)------------------------------ % 27.79/4.53 % (236514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.79/4.53 % (236514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.79/4.53 % (236514)CaDiCaL version: 2.1.3 % 27.79/4.53 % (236514)Termination reason: Instruction limit % 27.79/4.53 % (236514)Termination phase: Saturation % 27.79/4.53 % (236514)Time elapsed: 0.263 s % 27.79/4.53 % (236514)Peak memory usage: 135 MB % 27.79/4.53 % (236514)Instructions burned: 215 (million) % 27.79/4.53 % (236523)Instruction limit reached! % 27.79/4.53 % (236523)------------------------------ % 27.79/4.53 % (236523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.79/4.53 % (236523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.79/4.53 % (236523)CaDiCaL version: 2.1.3 % 27.79/4.53 % (236523)Termination reason: Instruction limit % 27.79/4.53 % (236523)Termination phase: Saturation % 27.79/4.53 % (236523)Time elapsed: 0.226 s % 27.79/4.53 % (236523)Peak memory usage: 91 MB % 27.79/4.53 % (236523)Instructions burned: 296 (million) % 27.79/4.53 % (236512)Instruction limit reached! % 27.79/4.53 % (236512)------------------------------ % 27.79/4.53 % (236512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.79/4.53 % (236512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.79/4.53 % (236512)CaDiCaL version: 2.1.3 % 27.79/4.53 % (236512)Termination reason: Instruction limit % 27.79/4.53 % (236512)Termination phase: Saturation % 27.79/4.53 % (236512)Time elapsed: 0.394 s % 27.79/4.53 % (236512)Peak memory usage: 118 MB % 27.79/4.53 % (236512)Instructions burned: 329 (million) % 30.44/5.01 % (236513)Instruction limit reached! % 30.44/5.01 % (236513)------------------------------ % 30.44/5.01 % (236513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.44/5.01 % (236513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.44/5.01 % (236513)CaDiCaL version: 2.1.3 % 30.44/5.01 % (236513)Termination reason: Instruction limit % 30.44/5.01 % (236513)Termination phase: Saturation % 30.44/5.01 % (236513)Time elapsed: 0.303 s % 30.44/5.01 % (236513)Peak memory usage: 135 MB % 30.44/5.01 % (236513)Instructions burned: 484 (million) % 30.44/5.01 % (236533)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1188947718:i=328:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/328Mi) % 30.44/5.01 % (236515)------------------------------ % 30.44/5.01 % (236515)------------------------------ % 30.44/5.01 % (236538)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3235201612:i=281:gtgl=2:rtra=on:gtg=all_2969 on theBenchmark for (2969ds/281Mi) % 30.44/5.01 % (236547)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2825886372:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi) % 30.44/5.01 % (236543)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=101074387:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi) % 30.44/5.01 % (236542)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3421968281:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi) % 30.44/5.01 % (236540)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1331170957:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi) % 30.44/5.01 % (236543)Refutation not found, incomplete strategy % 30.44/5.01 % (236543)------------------------------ % 30.44/5.01 % (236543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.44/5.01 % (236543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.44/5.01 % (236543)CaDiCaL version: 2.1.3 % 30.44/5.01 % (236543)Termination reason: Refutation not found, incomplete strategy % 30.44/5.01 % (236543)Time elapsed: 0.042 s % 30.44/5.01 % (236543)Peak memory usage: 116 MB % 30.44/5.01 % (236543)Instructions burned: 7 (million) % 30.44/5.01 % (236533)Instruction limit reached! % 30.44/5.01 % (236533)------------------------------ % 30.44/5.01 % (236533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.44/5.01 % (236533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.44/5.01 % (236533)CaDiCaL version: 2.1.3 % 30.44/5.01 % (236533)Termination reason: Instruction limit % 30.44/5.01 % (236533)Termination phase: Saturation % 30.44/5.01 % (236533)Time elapsed: 0.350 s % 30.44/5.01 % (236533)Peak memory usage: 119 MB % 30.44/5.01 % (236533)Instructions burned: 329 (million) % 30.44/5.01 % (236547)Instruction limit reached! % 30.44/5.01 % (236547)------------------------------ % 30.44/5.01 % (236547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.44/5.01 % (236547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.44/5.01 % (236547)CaDiCaL version: 2.1.3 % 30.44/5.01 % (236547)Termination reason: Instruction limit % 30.44/5.01 % (236547)Termination phase: Saturation % 30.44/5.01 % (236547)Time elapsed: 0.218 s % 30.44/5.01 % (236547)Peak memory usage: 118 MB % 30.44/5.01 % (236547)Instructions burned: 472 (million) % 30.44/5.01 % (236550)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=3308617168:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi) % 30.44/5.01 % (236538)Instruction limit reached! % 30.44/5.01 % (236538)------------------------------ % 30.44/5.01 % (236538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.44/5.01 % (236538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.44/5.01 % (236538)CaDiCaL version: 2.1.3 % 30.44/5.01 % (236538)Termination reason: Instruction limit % 30.44/5.01 % (236538)Termination phase: Saturation % 30.44/5.01 % (236538)Time elapsed: 0.294 s % 30.44/5.01 % (236538)Peak memory usage: 118 MB % 30.44/5.01 % (236538)Instructions burned: 281 (million) % 30.44/5.01 % (236542)Instruction limit reached! % 30.44/5.01 % (236542)------------------------------ % 30.44/5.01 % (236542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.05/5.63 % (236542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.05/5.63 % (236542)CaDiCaL version: 2.1.3 % 36.05/5.63 % (236542)Termination reason: Instruction limit % 36.05/5.63 % (236542)Termination phase: Saturation % 36.05/5.63 % (236542)Time elapsed: 0.289 s % 36.05/5.63 % (236542)Peak memory usage: 114 MB % 36.05/5.63 % (236542)Instructions burned: 321 (million) % 36.05/5.63 % (236563)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1220382717:i=375:kws=inv_arity_squared:rtra=on_2965 on theBenchmark for (2965ds/375Mi) % 36.05/5.63 % (236543)------------------------------ % 36.05/5.63 % (236543)------------------------------ % 36.05/5.63 % (236540)Instruction limit reached! % 36.05/5.63 % (236540)------------------------------ % 36.05/5.63 % (236540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.05/5.63 % (236540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.05/5.63 % (236540)CaDiCaL version: 2.1.3 % 36.05/5.63 % (236540)Termination reason: Instruction limit % 36.05/5.63 % (236540)Termination phase: Saturation % 36.05/5.63 % (236540)Time elapsed: 0.414 s % 36.05/5.63 % (236540)Peak memory usage: 92 MB % 36.05/5.63 % (236540)Instructions burned: 484 (million) % 36.05/5.63 % (236564)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3326926404:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/387Mi) % 36.05/5.63 % (236569)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3377351957:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi) % 36.05/5.63 % (236568)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2253211980:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2964 on theBenchmark for (2964ds/513Mi) % 36.05/5.63 % (236550)Instruction limit reached! % 36.05/5.63 % (236550)------------------------------ % 36.05/5.63 % (236550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.05/5.63 % (236550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.05/5.63 % (236550)CaDiCaL version: 2.1.3 % 36.05/5.63 % (236550)Termination reason: Instruction limit % 36.05/5.63 % (236550)Termination phase: Saturation % 36.05/5.63 % (236550)Time elapsed: 0.380 s % 36.05/5.63 % (236550)Peak memory usage: 134 MB % 36.05/5.63 % (236550)Instructions burned: 276 (million) % 36.05/5.63 % (236569)Instruction limit reached! % 36.05/5.63 % (236569)------------------------------ % 36.05/5.63 % (236569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.05/5.63 % (236569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.05/5.63 % (236569)CaDiCaL version: 2.1.3 % 36.05/5.63 % (236569)Termination reason: Instruction limit % 36.05/5.63 % (236569)Termination phase: Saturation % 36.05/5.63 % (236569)Time elapsed: 0.199 s % 36.05/5.63 % (236569)Peak memory usage: 134 MB % 36.05/5.63 % (236569)Instructions burned: 335 (million) % 36.05/5.63 % (236577)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=777963505:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2962 on theBenchmark for (2962ds/341Mi) % 36.05/5.63 % (236575)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=610687056:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi) % 36.05/5.63 % (236575)Refutation not found, incomplete strategy % 36.05/5.63 % (236575)------------------------------ % 36.05/5.63 % (236575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.05/5.63 % (236575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.05/5.63 % (236575)CaDiCaL version: 2.1.3 % 36.05/5.63 % (236575)Termination reason: Refutation not found, incomplete strategy % 36.05/5.63 % (236575)Time elapsed: 0.004 s % 36.05/5.63 % (236575)Peak memory usage: 89 MB % 36.05/5.63 % (236575)Instructions burned: 2 (million) % 36.05/5.63 % (236563)Instruction limit reached! % 36.05/5.63 % (236563)------------------------------ % 36.05/5.63 % (236563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.05/5.63 % (236563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.05/5.63 % (236563)CaDiCaL version: 2.1.3 % 36.05/5.63 % (236563)Termination reason: Instruction limit % 36.05/5.63 % (236563)Termination phase: Saturation % 36.05/5.63 % (236563)Time elapsed: 0.447 s % 36.05/5.63 % (236563)Peak memory usage: 117 MB % 36.05/5.63 % (236563)Instructions burned: 375 (million) % 42.84/6.50 % (236586)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3317456353:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/261Mi) % 42.84/6.50 % (236564)Instruction limit reached! % 42.84/6.50 % (236564)------------------------------ % 42.84/6.50 % (236564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.84/6.50 % (236564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.84/6.50 % (236564)CaDiCaL version: 2.1.3 % 42.84/6.50 % (236564)Termination reason: Instruction limit % 42.84/6.50 % (236564)Termination phase: Saturation % 42.84/6.50 % (236564)Time elapsed: 0.450 s % 42.84/6.50 % (236564)Peak memory usage: 119 MB % 42.84/6.50 % (236564)Instructions burned: 387 (million) % 42.84/6.50 % (236586)Refutation not found, incomplete strategy % 42.84/6.50 % (236586)------------------------------ % 42.84/6.50 % (236586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.84/6.50 % (236586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.84/6.50 % (236586)CaDiCaL version: 2.1.3 % 42.84/6.50 % (236586)Termination reason: Refutation not found, incomplete strategy % 42.84/6.50 % (236586)Time elapsed: 0.040 s % 42.84/6.50 % (236586)Peak memory usage: 115 MB % 42.84/6.50 % (236586)Instructions burned: 7 (million) % 42.84/6.50 % (236568)Instruction limit reached! % 42.84/6.50 % (236568)------------------------------ % 42.84/6.50 % (236568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.84/6.50 % (236568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.84/6.50 % (236568)CaDiCaL version: 2.1.3 % 42.84/6.50 % (236568)Termination reason: Instruction limit % 42.84/6.50 % (236568)Termination phase: Saturation % 42.84/6.50 % (236568)Time elapsed: 0.471 s % 42.84/6.50 % (236568)Peak memory usage: 94 MB % 42.84/6.50 % (236568)Instructions burned: 514 (million) % 42.84/6.50 % (236588)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=1533386380:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/235Mi) % 42.84/6.50 % (236577)Instruction limit reached! % 42.84/6.50 % (236577)------------------------------ % 42.84/6.50 % (236577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.84/6.50 % (236577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.84/6.50 % (236577)CaDiCaL version: 2.1.3 % 42.84/6.50 % (236577)Termination reason: Instruction limit % 42.84/6.50 % (236577)Termination phase: Saturation % 42.84/6.50 % (236577)Time elapsed: 0.348 s % 42.84/6.50 % (236577)Peak memory usage: 119 MB % 42.84/6.50 % (236577)Instructions burned: 342 (million) % 42.84/6.50 % (236575)------------------------------ % 42.84/6.50 % (236575)------------------------------ % 42.84/6.50 % (236586)------------------------------ % 42.84/6.50 % (236586)------------------------------ % 42.84/6.50 % (236597)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1181850264:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 42.84/6.50 % (236599)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3646897099:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi) % 42.84/6.50 % (236603)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2539479825:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi) % 42.84/6.50 % (236588)Instruction limit reached! % 42.84/6.50 % (236588)------------------------------ % 42.84/6.50 % (236588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.84/6.50 % (236588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.84/6.50 % (236588)CaDiCaL version: 2.1.3 % 42.84/6.50 % (236588)Termination reason: Instruction limit % 42.84/6.50 % (236588)Termination phase: Saturation % 42.84/6.50 % (236588)Time elapsed: 0.231 s % 42.84/6.50 % (236588)Peak memory usage: 116 MB % 42.84/6.50 % (236588)Instructions burned: 235 (million) % 42.84/6.50 % (236608)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=224390646:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi) % 42.84/6.50 % (236599)Instruction limit reached! % 42.84/6.50 % (236599)------------------------------ % 42.84/6.50 % (236599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.28 % (236599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.28 % (236599)CaDiCaL version: 2.1.3 % 48.11/7.28 % (236599)Termination reason: Instruction limit % 48.11/7.28 % (236599)Termination phase: Saturation % 48.11/7.28 % (236599)Time elapsed: 0.158 s % 48.11/7.28 % (236599)Peak memory usage: 90 MB % 48.11/7.28 % (236599)Instructions burned: 146 (million) % 48.11/7.28 % (236613)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1409057613:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/655Mi) % 48.11/7.28 % (236610)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1253855843:i=1052:rtra=on_2956 on theBenchmark for (2956ds/1052Mi) % 48.11/7.28 % (236597)Instruction limit reached! % 48.11/7.28 % (236597)------------------------------ % 48.11/7.28 % (236597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.28 % (236597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.28 % (236597)CaDiCaL version: 2.1.3 % 48.11/7.28 % (236597)Termination reason: Instruction limit % 48.11/7.28 % (236597)Termination phase: Saturation % 48.11/7.28 % (236597)Time elapsed: 0.294 s % 48.11/7.28 % (236597)Peak memory usage: 91 MB % 48.11/7.28 % (236597)Instructions burned: 273 (million) % 48.11/7.28 % (236617)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1304763707:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi) % 48.11/7.28 % (236621)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1116668541:i=107:rtra=on_2953 on theBenchmark for (2953ds/107Mi) % 48.11/7.28 % (236621)Refutation not found, incomplete strategy % 48.11/7.28 % (236621)------------------------------ % 48.11/7.28 % (236621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.28 % (236621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.28 % (236621)CaDiCaL version: 2.1.3 % 48.11/7.28 % (236621)Termination reason: Refutation not found, incomplete strategy % 48.11/7.28 % (236621)Time elapsed: 0.042 s % 48.11/7.28 % (236621)Peak memory usage: 116 MB % 48.11/7.28 % (236621)Instructions burned: 8 (million) % 48.11/7.28 % (236608)Instruction limit reached! % 48.11/7.28 % (236608)------------------------------ % 48.11/7.28 % (236608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.28 % (236608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.28 % (236608)CaDiCaL version: 2.1.3 % 48.11/7.28 % (236608)Termination reason: Instruction limit % 48.11/7.28 % (236608)Termination phase: Saturation % 48.11/7.28 % (236608)Time elapsed: 0.347 s % 48.11/7.28 % (236608)Peak memory usage: 134 MB % 48.11/7.28 % (236608)Instructions burned: 276 (million) % 48.11/7.28 % (236613)Instruction limit reached! % 48.11/7.28 % (236613)------------------------------ % 48.11/7.28 % (236613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.11/7.28 % (236613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.11/7.28 % (236613)CaDiCaL version: 2.1.3 % 48.11/7.28 % (236613)Termination reason: Instruction limit % 48.11/7.28 % (236613)Termination phase: Saturation % 48.11/7.28 % (236613)Time elapsed: 0.293 s % 48.11/7.28 % (236613)Peak memory usage: 92 MB % 48.11/7.28 % (236613)Instructions burned: 657 (million) % 48.11/7.28 % (236625)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2574059785:s2a=on:i=450:doe=on:nm=32:rtra=on_2952 on theBenchmark for (2952ds/450Mi) % 48.11/7.28 % (236632)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.11/7.28 % (236632)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3871621462:i=1090:aac=none:nm=0:rtra=on:rawr=on_2951 on theBenchmark for (2951ds/1090Mi) % 48.11/7.28 % (236635)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2244964404:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2950 on theBenchmark for (2950ds/130Mi) % 48.11/7.28 % (236621)------------------------------ % 48.11/7.28 % (236621)------------------------------ % 48.11/7.28 % (236635)Instruction limit reached! % 48.11/7.28 % (236635)------------------------------ % 48.11/7.28 % (236635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.24/8.00 % (236635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.24/8.00 % (236635)CaDiCaL version: 2.1.3 % 51.24/8.00 % (236635)Termination reason: Instruction limit % 51.24/8.00 % (236635)Termination phase: Saturation % 51.24/8.00 % (236635)Time elapsed: 0.059 s % 51.24/8.00 % (236635)Peak memory usage: 118 MB % 51.24/8.00 % (236635)Instructions burned: 130 (million) % 51.24/8.00 % (236647)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2376186852:i=312:kws=inv_frequency:nm=20:rtra=on_2947 on theBenchmark for (2947ds/312Mi) % 51.24/8.00 % (236647)Instruction limit reached! % 51.24/8.00 % (236647)------------------------------ % 51.24/8.00 % (236647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.24/8.00 % (236647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.24/8.00 % (236647)CaDiCaL version: 2.1.3 % 51.24/8.00 % (236647)Termination reason: Instruction limit % 51.24/8.00 % (236647)Termination phase: Saturation % 51.24/8.00 % (236647)Time elapsed: 0.159 s % 51.24/8.00 % (236647)Peak memory usage: 118 MB % 51.24/8.01 % (236647)Instructions burned: 312 (million) % 51.24/8.01 % (236648)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1829088367:i=491:doe=on:rtra=on:gtg=position_2947 on theBenchmark for (2947ds/491Mi) % 51.24/8.01 % (236625)Instruction limit reached! % 51.24/8.01 % (236625)------------------------------ % 51.24/8.01 % (236625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.24/8.01 % (236625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.24/8.01 % (236625)CaDiCaL version: 2.1.3 % 51.24/8.01 % (236625)Termination reason: Instruction limit % 51.24/8.01 % (236625)Termination phase: Saturation % 51.24/8.01 % (236625)Time elapsed: 0.556 s % 51.24/8.01 % (236625)Peak memory usage: 136 MB % 51.24/8.01 % (236625)Instructions burned: 450 (million) % 51.24/8.01 % (236610)Instruction limit reached! % 51.24/8.01 % (236610)------------------------------ % 51.24/8.01 % (236610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.24/8.01 % (236610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.24/8.01 % (236610)CaDiCaL version: 2.1.3 % 51.24/8.01 % (236610)Termination reason: Instruction limit % 51.24/8.01 % (236610)Termination phase: Saturation % 51.24/8.01 % (236610)Time elapsed: 0.943 s % 51.24/8.01 % (236610)Peak memory usage: 91 MB % 51.24/8.01 % (236610)Instructions burned: 1052 (million) % 51.24/8.01 % (236617)Instruction limit reached! % 51.24/8.01 % (236617)------------------------------ % 51.24/8.01 % (236617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.24/8.01 % (236617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.24/8.01 % (236617)CaDiCaL version: 2.1.3 % 51.24/8.01 % (236617)Termination reason: Instruction limit % 51.24/8.01 % (236617)Termination phase: Saturation % 51.24/8.01 % (236617)Time elapsed: 0.932 s % 51.24/8.01 % (236617)Peak memory usage: 92 MB % 51.24/8.01 % (236617)Instructions burned: 1054 (million) % 51.24/8.01 % (236653)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=824766224:s2a=on:i=835:s2at=2:rtra=on_2944 on theBenchmark for (2944ds/835Mi) % 51.24/8.01 % (236655)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3513948785:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2944 on theBenchmark for (2944ds/307Mi) % 51.24/8.01 % (236656)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=943443526:i=776:doe=on:rtra=on_2943 on theBenchmark for (2943ds/776Mi) % 51.24/8.01 % (236657)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1383383495:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2943 on theBenchmark for (2943ds/646Mi) % 51.24/8.01 % (236648)Instruction limit reached! % 51.24/8.01 % (236648)------------------------------ % 51.24/8.01 % (236648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.24/8.01 % (236648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.24/8.01 % (236648)CaDiCaL version: 2.1.3 % 51.24/8.01 % (236648)Termination reason: Instruction limit % 51.24/8.01 % (236648)Termination phase: Saturation % 51.24/8.01 % (236648)Time elapsed: 0.475 s % 51.24/8.01 % (236648)Peak memory usage: 92 MB % 51.24/8.01 % (236648)Instructions burned: 492 (million) % 51.24/8.01 % (236632)Instruction limit reached! % 51.24/8.01 % (236632)------------------------------ % 51.24/8.01 % (236632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.95/9.35 % (236632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.95/9.35 % (236632)CaDiCaL version: 2.1.3 % 62.95/9.35 % (236632)Termination reason: Instruction limit % 62.95/9.35 % (236632)Termination phase: Saturation % 62.95/9.35 % (236632)Time elapsed: 0.940 s % 62.95/9.35 % (236632)Peak memory usage: 121 MB % 62.95/9.35 % (236632)Instructions burned: 1091 (million) % 62.95/9.35 % (236653)Instruction limit reached! % 62.95/9.35 % (236653)------------------------------ % 62.95/9.35 % (236653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.95/9.35 % (236653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.95/9.35 % (236653)CaDiCaL version: 2.1.3 % 62.95/9.35 % (236653)Termination reason: Instruction limit % 62.95/9.35 % (236653)Termination phase: Saturation % 62.95/9.35 % (236653)Time elapsed: 0.404 s % 62.95/9.35 % (236653)Peak memory usage: 93 MB % 62.95/9.35 % (236653)Instructions burned: 836 (million) % 62.95/9.35 % (236655)Instruction limit reached! % 62.95/9.35 % (236655)------------------------------ % 62.95/9.35 % (236655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.95/9.35 % (236655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.95/9.35 % (236655)CaDiCaL version: 2.1.3 % 62.95/9.35 % (236655)Termination reason: Instruction limit % 62.95/9.35 % (236655)Termination phase: Saturation % 62.95/9.35 % (236655)Time elapsed: 0.324 s % 62.95/9.35 % (236655)Peak memory usage: 92 MB % 62.95/9.35 % (236655)Instructions burned: 307 (million) % 62.95/9.35 % (236669)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=4195600028:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2939 on theBenchmark for (2939ds/784Mi) % 62.95/9.35 % (236674)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=2044150923:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2938 on theBenchmark for (2938ds/246Mi) % 62.95/9.35 % (236672)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=393408715:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2938 on theBenchmark for (2938ds/1131Mi) % 62.95/9.35 % (236675)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3140092079:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2938 on theBenchmark for (2938ds/775Mi) % 62.95/9.35 % (236674)Instruction limit reached! % 62.95/9.35 % (236674)------------------------------ % 62.95/9.35 % (236674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.95/9.35 % (236674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.95/9.35 % (236674)CaDiCaL version: 2.1.3 % 62.95/9.35 % (236674)Termination reason: Instruction limit % 62.95/9.35 % (236674)Termination phase: Saturation % 62.95/9.35 % (236674)Time elapsed: 0.142 s % 62.95/9.35 % (236674)Peak memory usage: 116 MB % 62.95/9.35 % (236674)Instructions burned: 246 (million) % 62.95/9.35 % (236656)Instruction limit reached! % 62.95/9.35 % (236656)------------------------------ % 62.95/9.35 % (236656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.95/9.35 % (236656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.95/9.35 % (236656)CaDiCaL version: 2.1.3 % 62.95/9.35 % (236656)Termination reason: Instruction limit % 62.95/9.35 % (236656)Termination phase: Saturation % 62.95/9.35 % (236656)Time elapsed: 0.739 s % 62.95/9.35 % (236656)Peak memory usage: 122 MB % 62.95/9.35 % (236656)Instructions burned: 777 (million) % 62.95/9.35 % (236657)Instruction limit reached! % 62.95/9.35 % (236657)------------------------------ % 62.95/9.35 % (236657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.95/9.35 % (236657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.95/9.35 % (236657)CaDiCaL version: 2.1.3 % 62.95/9.35 % (236657)Termination reason: Instruction limit % 62.95/9.35 % (236657)Termination phase: Saturation % 62.95/9.35 % (236657)Time elapsed: 0.750 s % 62.95/9.35 % (236657)Peak memory usage: 137 MB % 62.95/9.35 % (236657)Instructions burned: 646 (million) % 62.95/9.35 % (236686)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=387639177:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2934 on theBenchmark for (2934ds/273Mi) % 62.95/9.35 % (236686)Instruction limit reached! % 62.95/9.35 % (236686)------------------------------ % 72.96/11.15 % (236686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/11.15 % (236686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/11.15 % (236686)CaDiCaL version: 2.1.3 % 72.96/11.15 % (236686)Termination reason: Instruction limit % 72.96/11.15 % (236686)Termination phase: Saturation % 72.96/11.15 % (236686)Time elapsed: 0.152 s % 72.96/11.15 % (236686)Peak memory usage: 91 MB % 72.96/11.15 % (236686)Instructions burned: 275 (million) % 72.96/11.15 % (236689)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2075155518:i=102:nm=16:rtra=on_2933 on theBenchmark for (2933ds/102Mi) % 72.96/11.15 % (236669)Instruction limit reached! % 72.96/11.15 % (236669)------------------------------ % 72.96/11.15 % (236669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/11.15 % (236669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/11.15 % (236669)CaDiCaL version: 2.1.3 % 72.96/11.15 % (236669)Termination reason: Instruction limit % 72.96/11.15 % (236669)Termination phase: Saturation % 72.96/11.15 % (236669)Time elapsed: 0.618 s % 72.96/11.15 % (236669)Peak memory usage: 118 MB % 72.96/11.15 % (236669)Instructions burned: 786 (million) % 72.96/11.15 % (236691)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2759705612:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2932 on theBenchmark for (2932ds/1094Mi) % 72.96/11.15 % (236689)Instruction limit reached! % 72.96/11.15 % (236689)------------------------------ % 72.96/11.15 % (236689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/11.15 % (236689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/11.15 % (236689)CaDiCaL version: 2.1.3 % 72.96/11.15 % (236689)Termination reason: Instruction limit % 72.96/11.15 % (236689)Termination phase: Saturation % 72.96/11.15 % (236689)Time elapsed: 0.099 s % 72.96/11.15 % (236689)Peak memory usage: 89 MB % 72.96/11.15 % (236689)Instructions burned: 102 (million) % 72.96/11.15 % (236695)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=233312450:i=6400:doe=on:fsr=off:rtra=on_2931 on theBenchmark for (2931ds/6400Mi) % 72.96/11.15 % (236698)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=2268804589:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/868Mi) % 72.96/11.15 % (236703)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=3139815787:i=1846:canc=cautious:fsr=off:rtra=on_2929 on theBenchmark for (2929ds/1846Mi) % 72.96/11.15 % (236675)Instruction limit reached! % 72.96/11.15 % (236675)------------------------------ % 72.96/11.15 % (236675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/11.15 % (236675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/11.15 % (236675)CaDiCaL version: 2.1.3 % 72.96/11.15 % (236675)Termination reason: Instruction limit % 72.96/11.15 % (236675)Termination phase: Saturation % 72.96/11.15 % (236675)Time elapsed: 0.828 s % 72.96/11.15 % (236675)Peak memory usage: 95 MB % 72.96/11.15 % (236675)Instructions burned: 776 (million) % 72.96/11.15 % (236672)Instruction limit reached! % 72.96/11.15 % (236672)------------------------------ % 72.96/11.15 % (236672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/11.15 % (236672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/11.15 % (236672)CaDiCaL version: 2.1.3 % 72.96/11.15 % (236672)Termination reason: Instruction limit % 72.96/11.15 % (236672)Termination phase: Saturation % 72.96/11.15 % (236672)Time elapsed: 1.115 s % 72.96/11.15 % (236672)Peak memory usage: 126 MB % 72.96/11.15 % (236672)Instructions burned: 1131 (million) % 72.96/11.15 % (236710)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1956232350:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2926 on theBenchmark for (2926ds/36816Mi) % 72.96/11.15 % (236710)Refutation not found, incomplete strategy % 72.96/11.15 % (236710)------------------------------ % 72.96/11.15 % (236710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.96/11.15 % (236710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.96/11.15 % (236710)CaDiCaL version: 2.1.3 % 72.96/11.15 % (236710)Termination reason: Refutation not found, incomplete strategy % 72.96/11.15 % (236710)Time elapsed: 0.005 s % 72.96/11.15 % (236710)Peak memory usage: 88 MB % 72.96/11.15 % (236710)Instructions burned: 3 (million) % 91.34/13.35 % (236691)Instruction limit reached! % 91.34/13.35 % (236691)------------------------------ % 91.34/13.35 % (236691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.34/13.35 % (236691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.34/13.35 % (236691)CaDiCaL version: 2.1.3 % 91.34/13.35 % (236691)Termination reason: Instruction limit % 91.34/13.35 % (236691)Termination phase: Saturation % 91.34/13.35 % (236691)Time elapsed: 0.719 s % 91.34/13.35 % (236691)Peak memory usage: 91 MB % 91.34/13.35 % (236691)Instructions burned: 1094 (million) % 91.34/13.35 % (236713)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3900198144:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2925 on theBenchmark for (2925ds/273Mi) % 91.34/13.35 % (236710)------------------------------ % 91.34/13.35 % (236710)------------------------------ % 91.34/13.35 % (236718)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=1445717575:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2922 on theBenchmark for (2922ds/863Mi) % 91.34/13.35 % (236713)Instruction limit reached! % 91.34/13.35 % (236713)------------------------------ % 91.34/13.35 % (236713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.34/13.35 % (236713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.34/13.35 % (236713)CaDiCaL version: 2.1.3 % 91.34/13.35 % (236713)Termination reason: Instruction limit % 91.34/13.35 % (236713)Termination phase: Saturation % 91.34/13.35 % (236713)Time elapsed: 0.288 s % 91.34/13.35 % (236713)Peak memory usage: 91 MB % 91.34/13.35 % (236713)Instructions burned: 273 (million) % 91.34/13.35 % (236698)Instruction limit reached! % 91.34/13.35 % (236698)------------------------------ % 91.34/13.35 % (236698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.34/13.35 % (236698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.34/13.35 % (236698)CaDiCaL version: 2.1.3 % 91.34/13.35 % (236698)Termination reason: Instruction limit % 91.34/13.35 % (236698)Termination phase: Saturation % 91.34/13.35 % (236698)Time elapsed: 0.905 s % 91.34/13.35 % (236698)Peak memory usage: 121 MB % 91.34/13.35 % (236698)Instructions burned: 868 (million) % 91.34/13.35 % (236723)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3376766096:i=5811:kws=precedence:nm=0:rtra=on_2919 on theBenchmark for (2919ds/5811Mi) % 91.34/13.35 % (236725)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=415226169:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2919 on theBenchmark for (2919ds/2216Mi) % 91.34/13.35 % (236727)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1461877127:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2918 on theBenchmark for (2918ds/801Mi) % 91.34/13.35 % (236603)Instruction limit reached! % 91.34/13.35 % (236603)------------------------------ % 91.34/13.35 % (236603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.34/13.35 % (236603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.34/13.35 % (236603)CaDiCaL version: 2.1.3 % 91.34/13.35 % (236603)Termination reason: Instruction limit % 91.34/13.35 % (236603)Termination phase: Saturation % 91.34/13.35 % (236603)Time elapsed: 4.081 s % 91.34/13.35 % (236603)Peak memory usage: 113 MB % 91.34/13.35 % (236603)Instructions burned: 4428 (million) % 91.34/13.35 % (236735)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1756688724:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2914 on theBenchmark for (2914ds/1026Mi) % 91.34/13.35 % (236718)Instruction limit reached! % 91.34/13.35 % (236718)------------------------------ % 91.34/13.35 % (236718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.34/13.35 % (236718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.34/13.35 % (236718)CaDiCaL version: 2.1.3 % 91.34/13.35 % (236718)Termination reason: Instruction limit % 91.34/13.35 % (236718)Termination phase: Saturation % 91.34/13.35 % (236718)Time elapsed: 0.878 s % 91.34/13.35 % (236718)Peak memory usage: 120 MB % 91.34/13.35 % (236718)Instructions burned: 863 (million) % 91.34/13.35 % (236703)Instruction limit reached! % 91.34/13.35 % (236703)------------------------------ % 91.34/13.35 % (236703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.34/13.35 % (236703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.03/20.67 % (236703)CaDiCaL version: 2.1.3 % 143.03/20.67 % (236703)Termination reason: Instruction limit % 143.03/20.67 % (236703)Termination phase: Saturation % 143.03/20.67 % (236703)Time elapsed: 1.678 s % 143.03/20.67 % (236703)Peak memory usage: 96 MB % 143.03/20.67 % (236703)Instructions burned: 1847 (million) % 143.03/20.67 % (236737)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=624482490:i=3509:rtra=on_2911 on theBenchmark for (2911ds/3509Mi) % 143.03/20.67 % (236727)Instruction limit reached! % 143.03/20.67 % (236727)------------------------------ % 143.03/20.67 % (236727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.03/20.67 % (236727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.03/20.67 % (236727)CaDiCaL version: 2.1.3 % 143.03/20.67 % (236727)Termination reason: Instruction limit % 143.03/20.67 % (236727)Termination phase: Saturation % 143.03/20.67 % (236727)Time elapsed: 0.737 s % 143.03/20.67 % (236727)Peak memory usage: 93 MB % 143.03/20.67 % (236727)Instructions burned: 801 (million) % 143.03/20.67 % (236738)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=366549198:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2910 on theBenchmark for (2910ds/2127Mi) % 143.03/20.68 % (236742)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1228826345:i=1959:rtra=on:fsd=on:proc=on_2908 on theBenchmark for (2908ds/1959Mi) % 143.03/20.68 % (236742)Refutation not found, incomplete strategy % 143.03/20.68 % (236742)------------------------------ % 143.03/20.68 % (236742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.03/20.68 % (236742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.03/20.68 % (236742)CaDiCaL version: 2.1.3 % 143.03/20.68 % (236742)Termination reason: Refutation not found, incomplete strategy % 143.03/20.68 % (236742)Time elapsed: 0.048 s % 143.03/20.68 % (236742)Peak memory usage: 116 MB % 143.03/20.68 % (236742)Instructions burned: 13 (million) % 143.03/20.68 % (236735)Instruction limit reached! % 143.03/20.68 % (236735)------------------------------ % 143.03/20.68 % (236735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.03/20.68 % (236735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.03/20.68 % (236735)CaDiCaL version: 2.1.3 % 143.03/20.68 % (236735)Termination reason: Instruction limit % 143.03/20.68 % (236735)Termination phase: Saturation % 143.03/20.68 % (236735)Time elapsed: 0.974 s % 143.03/20.68 % (236735)Peak memory usage: 92 MB % 143.03/20.68 % (236735)Instructions burned: 1027 (million) % 143.03/20.68 % (236742)------------------------------ % 143.03/20.68 % (236742)------------------------------ % 143.03/20.68 % (236750)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2901163600:s2a=on:i=3553:nm=0:rtra=on_2901 on theBenchmark for (2901ds/3553Mi) % 143.03/20.68 % (236695)Instruction limit reached! % 143.03/20.68 % (236695)------------------------------ % 143.03/20.68 % (236695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.03/20.68 % (236695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.03/20.68 % (236695)CaDiCaL version: 2.1.3 % 143.03/20.68 % (236695)Termination reason: Instruction limit % 143.03/20.68 % (236695)Termination phase: Saturation % 143.03/20.68 % (236695)Time elapsed: 3.019 s % 143.03/20.68 % (236695)Peak memory usage: 123 MB % 143.03/20.68 % (236695)Instructions burned: 6401 (million) % 143.03/20.68 % (236751)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1659884212:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2901 on theBenchmark for (2901ds/3201Mi) % 143.03/20.68 % (236755)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=428456075:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2898 on theBenchmark for (2898ds/4093Mi) % 143.03/20.68 % (236725)Instruction limit reached! % 143.03/20.68 % (236725)------------------------------ % 143.03/20.68 % (236725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.03/20.68 % (236725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.03/20.68 % (236725)CaDiCaL version: 2.1.3 % 143.03/20.68 % (236725)Termination reason: Instruction limit % 143.03/20.68 % (236725)Termination phase: Saturation % 143.03/20.68 % (236725)Time elapsed: 2.078 s % 143.03/20.68 % (236725)Peak memory usage: 125 MB % 143.03/20.68 % (236725)Instructions burned: 2216 (million) % 143.03/20.68 % (236758)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=3567762410:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2895 on theBenchmark for (2895ds/21173Mi) % 167.90/24.11 % (236738)Instruction limit reached! % 167.90/24.11 % (236738)------------------------------ % 167.90/24.11 % (236738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.90/24.11 % (236738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.90/24.11 % (236738)CaDiCaL version: 2.1.3 % 167.90/24.11 % (236738)Termination reason: Instruction limit % 167.90/24.11 % (236738)Termination phase: Saturation % 167.90/24.11 % (236738)Time elapsed: 1.774 s % 167.90/24.11 % (236738)Peak memory usage: 101 MB % 167.90/24.11 % (236738)Instructions burned: 2128 (million) % 167.90/24.11 % (236761)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1013163135:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2889 on theBenchmark for (2889ds/10544Mi) % 167.90/24.11 % (236737)Instruction limit reached! % 167.90/24.11 % (236737)------------------------------ % 167.90/24.11 % (236737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.90/24.11 % (236737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.90/24.11 % (236737)CaDiCaL version: 2.1.3 % 167.90/24.11 % (236737)Termination reason: Instruction limit % 167.90/24.11 % (236737)Termination phase: Saturation % 167.90/24.11 % (236737)Time elapsed: 2.525 s % 167.90/24.11 % (236737)Peak memory usage: 97 MB % 167.90/24.11 % (236737)Instructions burned: 3510 (million) % 167.90/24.11 % (236767)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1567601318:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2883 on theBenchmark for (2883ds/1262Mi) % 167.90/24.11 % (236767)Refutation not found, incomplete strategy % 167.90/24.11 % (236767)------------------------------ % 167.90/24.11 % (236767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.90/24.11 % (236767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.90/24.11 % (236767)CaDiCaL version: 2.1.3 % 167.90/24.11 % (236767)Termination reason: Refutation not found, incomplete strategy % 167.90/24.11 % (236767)Time elapsed: 0.045 s % 167.90/24.11 % (236767)Peak memory usage: 116 MB % 167.90/24.11 % (236767)Instructions burned: 9 (million) % 167.90/24.11 % (236767)------------------------------ % 167.90/24.11 % (236767)------------------------------ % 167.90/24.11 % (236755)Instruction limit reached! % 167.90/24.11 % (236755)------------------------------ % 167.90/24.11 % (236755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.90/24.11 % (236755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.90/24.11 % (236755)CaDiCaL version: 2.1.3 % 167.90/24.11 % (236755)Termination reason: Instruction limit % 167.90/24.11 % (236755)Termination phase: Saturation % 167.90/24.11 % (236755)Time elapsed: 2.053 s % 167.90/24.11 % (236755)Peak memory usage: 153 MB % 167.90/24.11 % (236755)Instructions burned: 4095 (million) % 167.90/24.11 % (236776)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2475113387:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2875 on theBenchmark for (2875ds/270Mi) % 167.90/24.11 % (236775)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1664137291:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2875 on theBenchmark for (2875ds/775Mi) % 167.90/24.11 % (236776)Instruction limit reached! % 167.90/24.11 % (236776)------------------------------ % 167.90/24.11 % (236776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.90/24.11 % (236776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.90/24.11 % (236776)CaDiCaL version: 2.1.3 % 167.90/24.11 % (236776)Termination reason: Instruction limit % 167.90/24.11 % (236776)Termination phase: Saturation % 167.90/24.11 % (236776)Time elapsed: 0.155 s % 167.90/24.11 % (236776)Peak memory usage: 91 MB % 167.90/24.11 % (236776)Instructions burned: 270 (million) % 167.90/24.11 % (236751)Instruction limit reached! % 167.90/24.11 % (236751)------------------------------ % 167.90/24.11 % (236751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.90/24.11 % (236751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.90/24.11 % (236751)CaDiCaL version: 2.1.3 % 167.90/24.11 % (236751)Termination reason: Instruction limit % 167.90/24.11 % (236751)Termination phase: Saturation % 167.90/24.11 % (236751)Time elapsed: 2.817 s % 186.17/26.73 % (236751)Peak memory usage: 95 MB % 186.17/26.73 % (236751)Instructions burned: 3201 (million) % 186.17/26.73 % (236779)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=707479013:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2872 on theBenchmark for (2872ds/17165Mi) % 186.17/26.73 % (236780)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1452400381:s2a=on:i=13094:s2at=-1:rtra=on_2870 on theBenchmark for (2870ds/13094Mi) % 186.17/26.73 % (236750)Instruction limit reached! % 186.17/26.73 % (236750)------------------------------ % 186.17/26.73 % (236750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.17/26.73 % (236750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.17/26.73 % (236750)CaDiCaL version: 2.1.3 % 186.17/26.73 % (236750)Termination reason: Instruction limit % 186.17/26.73 % (236750)Termination phase: Saturation % 186.17/26.73 % (236750)Time elapsed: 3.314 s % 186.17/26.73 % (236750)Peak memory usage: 99 MB % 186.17/26.73 % (236750)Instructions burned: 3554 (million) % 186.17/26.73 % (236723)Instruction limit reached! % 186.17/26.73 % (236723)------------------------------ % 186.17/26.73 % (236723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.17/26.73 % (236723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.17/26.73 % (236723)CaDiCaL version: 2.1.3 % 186.17/26.73 % (236723)Termination reason: Instruction limit % 186.17/26.73 % (236723)Termination phase: Saturation % 186.17/26.73 % (236723)Time elapsed: 5.233 s % 186.17/26.73 % (236723)Peak memory usage: 137 MB % 186.17/26.73 % (236723)Instructions burned: 5811 (million) % 186.17/26.73 % (236775)Instruction limit reached! % 186.17/26.73 % (236775)------------------------------ % 186.17/26.73 % (236775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.17/26.73 % (236775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.17/26.73 % (236775)CaDiCaL version: 2.1.3 % 186.17/26.73 % (236775)Termination reason: Instruction limit % 186.17/26.73 % (236775)Termination phase: Saturation % 186.17/26.73 % (236775)Time elapsed: 0.817 s % 186.17/26.73 % (236775)Peak memory usage: 95 MB % 186.17/26.73 % (236775)Instructions burned: 775 (million) % 186.17/26.73 % (236783)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1400265590:st=2:i=12633:rtra=on:ss=axioms_2865 on theBenchmark for (2865ds/12633Mi) % 186.17/26.73 % (236784)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=406533633:i=1783:rtra=on:gtg=position_2865 on theBenchmark for (2865ds/1783Mi) % 186.17/26.73 % (236785)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=771414515:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2864 on theBenchmark for (2864ds/5451Mi) % 186.17/26.73 % (236784)Instruction limit reached! % 186.17/26.73 % (236784)------------------------------ % 186.17/26.73 % (236784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.17/26.73 % (236784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.17/26.73 % (236784)CaDiCaL version: 2.1.3 % 186.17/26.73 % (236784)Termination reason: Instruction limit % 186.17/26.73 % (236784)Termination phase: Saturation % 186.17/26.73 % (236784)Time elapsed: 1.820 s % 186.17/26.73 % (236784)Peak memory usage: 127 MB % 186.17/26.73 % (236784)Instructions burned: 1783 (million) % 186.17/26.73 % (236793)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=3049400503:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2844 on theBenchmark for (2844ds/4975Mi) % 186.17/26.73 % (236785)Instruction limit reached! % 186.17/26.73 % (236785)------------------------------ % 186.17/26.73 % (236785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.17/26.73 % (236785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.17/26.73 % (236785)CaDiCaL version: 2.1.3 % 186.17/26.73 % (236785)Termination reason: Instruction limit % 186.17/26.73 % (236785)Termination phase: Saturation % 186.17/26.73 % (236785)Time elapsed: 5.277 s % 186.17/26.73 % (236785)Peak memory usage: 146 MB % 186.17/26.73 % (236785)Instructions burned: 5451 (million) % 186.17/26.73 % (236802)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=2081519506:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2809 on theBenchmark for (2809ds/2076Mi) % 186.17/26.73 % (236793)Instruction limit reached! % 186.17/26.73 % (236793)------------------------------ % 215.60/30.83 % (236793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.60/30.83 % (236793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.60/30.83 % (236793)CaDiCaL version: 2.1.3 % 215.60/30.83 % (236793)Termination reason: Instruction limit % 215.60/30.83 % (236793)Termination phase: Saturation % 215.60/30.83 % (236793)Time elapsed: 4.437 s % 215.60/30.83 % (236793)Peak memory usage: 128 MB % 215.60/30.83 % (236793)Instructions burned: 4976 (million) % 215.60/30.83 % (236804)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2264709377:i=5145:rtra=on_2797 on theBenchmark for (2797ds/5145Mi) % 215.60/30.83 % (236779)Instruction limit reached! % 215.60/30.83 % (236779)------------------------------ % 215.60/30.83 % (236779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.60/30.83 % (236779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.60/30.83 % (236779)CaDiCaL version: 2.1.3 % 215.60/30.83 % (236779)Termination reason: Instruction limit % 215.60/30.83 % (236779)Termination phase: Saturation % 215.60/30.83 % (236779)Time elapsed: 7.832 s % 215.60/30.83 % (236779)Peak memory usage: 143 MB % 215.60/30.83 % (236779)Instructions burned: 17167 (million) % 215.60/30.83 % (236808)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1189734127:i=3509:rtra=on_2791 on theBenchmark for (2791ds/3509Mi) % 215.60/30.83 % (236802)Instruction limit reached! % 215.60/30.83 % (236802)------------------------------ % 215.60/30.83 % (236802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.60/30.83 % (236802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.60/30.83 % (236802)CaDiCaL version: 2.1.3 % 215.60/30.83 % (236802)Termination reason: Instruction limit % 215.60/30.83 % (236802)Termination phase: Saturation % 215.60/30.83 % (236802)Time elapsed: 1.897 s % 215.60/30.83 % (236802)Peak memory usage: 123 MB % 215.60/30.83 % (236802)Instructions burned: 2077 (million) % 215.60/30.83 % (236811)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1121078338:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2786 on theBenchmark for (2786ds/13800Mi) % 215.60/30.83 % (236761)Instruction limit reached! % 215.60/30.83 % (236761)------------------------------ % 215.60/30.83 % (236761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.60/30.83 % (236761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.60/30.83 % (236761)CaDiCaL version: 2.1.3 % 215.60/30.83 % (236761)Termination reason: Instruction limit % 215.60/30.83 % (236761)Termination phase: Saturation % 215.60/30.83 % (236761)Time elapsed: 10.944 s % 215.60/30.83 % (236761)Peak memory usage: 193 MB % 215.60/30.83 % (236761)Instructions burned: 10544 (million) % 215.60/30.83 % (236808)Instruction limit reached! % 215.60/30.83 % (236808)------------------------------ % 215.60/30.83 % (236808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.60/30.83 % (236808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.60/30.83 % (236808)CaDiCaL version: 2.1.3 % 215.60/30.83 % (236808)Termination reason: Instruction limit % 215.60/30.83 % (236808)Termination phase: Saturation % 215.60/30.83 % (236808)Time elapsed: 1.277 s % 215.60/30.83 % (236808)Peak memory usage: 97 MB % 215.60/30.83 % (236808)Instructions burned: 3512 (million) % 215.60/30.83 % (236821)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 % 215.60/30.83 % (236821)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1296952611:i=11747:aac=none:nm=0:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/11747Mi) % 215.60/30.83 % (236820)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1752244126:i=1412:rtra=on:fsd=on:proc=on_2777 on theBenchmark for (2777ds/1412Mi) % 215.60/30.83 % (236783)Instruction limit reached! % 215.60/30.83 % (236783)------------------------------ % 215.60/30.83 % (236783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.60/30.83 % (236783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.60/30.83 % (236783)CaDiCaL version: 2.1.3 % 215.60/30.83 % (236783)Termination reason: Instruction limit % 215.60/30.83 % (236783)Termination phase: Saturation % 215.60/30.83 % (236783)Time elapsed: 9.989 s % 215.60/30.83 % (236783)Peak memory usage: 108 MB % 215.60/30.83 % (236783)Instructions burned: 12634 (million) % 270.45/38.55 % (236820)Instruction limit reached! % 270.45/38.55 % (236820)------------------------------ % 270.45/38.55 % (236820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.45/38.55 % (236820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.45/38.55 % (236820)CaDiCaL version: 2.1.3 % 270.45/38.55 % (236820)Termination reason: Instruction limit % 270.45/38.55 % (236820)Termination phase: Saturation % 270.45/38.55 % (236820)Time elapsed: 1.427 s % 270.45/38.55 % (236820)Peak memory usage: 121 MB % 270.45/38.55 % (236820)Instructions burned: 1412 (million) % 270.45/38.55 % (236824)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2172492423:s2a=on:i=3553:nm=0:rtra=on_2762 on theBenchmark for (2762ds/3553Mi) % 270.45/38.55 % (236827)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2032015363:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/3201Mi) % 270.45/38.55 % (236780)Instruction limit reached! % 270.45/38.55 % (236780)------------------------------ % 270.45/38.55 % (236780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.45/38.55 % (236780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.45/38.55 % (236780)CaDiCaL version: 2.1.3 % 270.45/38.55 % (236780)Termination reason: Instruction limit % 270.45/38.55 % (236780)Termination phase: Saturation % 270.45/38.55 % (236780)Time elapsed: 11.310 s % 270.45/38.55 % (236780)Peak memory usage: 139 MB % 270.45/38.55 % (236780)Instructions burned: 13094 (million) % 270.45/38.55 % (236821)Refutation not found, incomplete strategy % 270.45/38.55 % (236821)------------------------------ % 270.45/38.55 % (236821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.45/38.55 % (236821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.45/38.55 % (236821)CaDiCaL version: 2.1.3 % 270.45/38.55 % (236821)Termination reason: Refutation not found, incomplete strategy % 270.45/38.55 % (236821)Time elapsed: 2.080 s % 270.45/38.55 % (236821)Peak memory usage: 136 MB % 270.45/38.55 % (236821)Instructions burned: 4853 (million) % 270.45/38.55 % (236821)------------------------------ % 270.45/38.55 % (236821)------------------------------ % 270.45/38.55 % (236831)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=1775307181:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2754 on theBenchmark for (2754ds/4081Mi) % 270.45/38.55 % (236835)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=3441182870:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2751 on theBenchmark for (2751ds/20260Mi) % 270.45/38.55 % (236804)Instruction limit reached! % 270.45/38.55 % (236804)------------------------------ % 270.45/38.55 % (236804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.45/38.55 % (236804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.45/38.55 % (236804)CaDiCaL version: 2.1.3 % 270.45/38.55 % (236804)Termination reason: Instruction limit % 270.45/38.55 % (236804)Termination phase: Saturation % 270.45/38.55 % (236804)Time elapsed: 4.738 s % 270.45/38.55 % (236804)Peak memory usage: 100 MB % 270.45/38.55 % (236804)Instructions burned: 5145 (million) % 270.45/38.55 % (236843)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2682298198:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2746 on theBenchmark for (2746ds/58627Mi) % 270.45/38.55 % (236843)Refutation not found, incomplete strategy % 270.45/38.55 % (236843)------------------------------ % 270.45/38.55 % (236843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.45/38.55 % (236843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.45/38.55 % (236843)CaDiCaL version: 2.1.3 % 270.45/38.55 % (236843)Termination reason: Refutation not found, incomplete strategy % 270.45/38.55 % (236843)Time elapsed: 0.005 s % 270.45/38.55 % (236843)Peak memory usage: 88 MB % 270.45/38.55 % (236843)Instructions burned: 3 (million) % 270.45/38.55 % (236843)------------------------------ % 270.45/38.55 % (236843)------------------------------ % 270.45/38.55 % (236853)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4125047639:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2739 on theBenchmark for (2739ds/6258Mi) % 270.45/38.55 % (236827)Refutation not found, incomplete strategy % 270.45/38.55 % (236827)------------------------------ % 270.45/38.55 % (236827)Version: VamTerminated %------------------------------------------------------------------------------