%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX116_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:55 PM UTC 2026 % Result : Timeout 300.49s 43.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX116_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.23 % Computer : n007.cluster.edu % 0.10/0.23 % Model : x86_64 x86_64 % 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.23 % Memory : 8046.5625MB % 0.10/0.23 % OS : Linux 6.8.0-71-generic % 0.10/0.23 % CPULimit : 300 % 0.10/0.23 % WCLimit : 300 % 0.10/0.23 % DateTime : Mon Sep 28 15:00:10 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.26/0.29 Running first-order theorem proving % 0.26/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.20/1.86 % (2477729)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.20/1.86 % (2477752)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=462941507:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.20/1.86 % (2477752)Instruction limit reached! % 5.20/1.86 % (2477752)------------------------------ % 5.20/1.86 % (2477752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.86 % (2477752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.86 % (2477752)CaDiCaL version: 2.1.3 % 5.20/1.86 % (2477752)Termination reason: Instruction limit % 5.20/1.86 % (2477752)Termination phase: Saturation % 5.20/1.86 % (2477752)Time elapsed: 0.005 s % 5.20/1.86 % (2477752)Peak memory usage: 88 MB % 5.20/1.86 % (2477752)Instructions burned: 5 (million) % 5.20/1.86 % (2477753)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3320673430:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.20/1.86 % (2477754)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=810740557:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.20/1.86 % (2477748)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=119430255:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.20/1.86 % (2477750)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3651577293:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.20/1.86 % (2477749)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3796516098:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.20/1.86 % (2477751)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=128703736:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.20/1.86 % (2477751)Instruction limit reached! % 5.20/1.86 % (2477751)------------------------------ % 5.20/1.86 % (2477751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.86 % (2477751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.86 % (2477751)CaDiCaL version: 2.1.3 % 5.20/1.86 % (2477751)Termination reason: Instruction limit % 5.20/1.86 % (2477751)Termination phase: Saturation % 5.20/1.86 % (2477751)Time elapsed: 0.005 s % 5.20/1.86 % (2477751)Peak memory usage: 88 MB % 5.20/1.86 % (2477751)Instructions burned: 8 (million) % 5.20/1.86 % (2477748)Instruction limit reached! % 5.20/1.86 % (2477748)------------------------------ % 5.20/1.86 % (2477748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.86 % (2477748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.86 % (2477748)CaDiCaL version: 2.1.3 % 5.20/1.86 % (2477748)Termination reason: Instruction limit % 5.20/1.86 % (2477748)Termination phase: Saturation % 5.20/1.86 % (2477748)Time elapsed: 0.041 s % 5.20/1.86 % (2477748)Peak memory usage: 113 MB % 5.20/1.86 % (2477748)Instructions burned: 12 (million) % 5.20/1.86 % (2477754)Instruction limit reached! % 5.20/1.86 % (2477754)------------------------------ % 5.20/1.86 % (2477754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.86 % (2477754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.86 % (2477754)CaDiCaL version: 2.1.3 % 5.20/1.86 % (2477754)Termination reason: Instruction limit % 5.20/1.86 % (2477754)Termination phase: Saturation % 5.20/1.86 % (2477754)Time elapsed: 0.066 s % 5.20/1.86 % (2477754)Peak memory usage: 116 MB % 5.20/1.86 % (2477754)Instructions burned: 33 (million) % 5.20/1.86 % (2477753)Instruction limit reached! % 5.20/1.86 % (2477753)------------------------------ % 5.20/1.86 % (2477753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.20/1.86 % (2477753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.20/1.86 % (2477753)CaDiCaL version: 2.1.3 % 5.20/1.86 % (2477753)Termination reason: Instruction limit % 5.20/1.86 % (2477753)Termination phase: Saturation % 5.20/1.86 % (2477753)Time elapsed: 0.080 s % 5.20/1.86 % (2477753)Peak memory usage: 116 MB % 5.20/1.86 % (2477753)Instructions burned: 47 (million) % 5.20/1.86 % (2477756)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2098918225:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.20/1.86 % (2477756)Instruction limit reached! % 5.20/1.86 % (2477756)------------------------------ % 5.20/1.86 % (2477756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.79/2.14 % (2477756)CaDiCaL version: 2.1.3 % 8.79/2.14 % (2477756)Termination reason: Instruction limit % 8.79/2.14 % (2477756)Termination phase: Saturation % 8.79/2.14 % (2477756)Time elapsed: 0.018 s % 8.79/2.14 % (2477756)Peak memory usage: 89 MB % 8.79/2.14 % (2477756)Instructions burned: 15 (million) % 8.79/2.14 % (2477763)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=568239386:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 8.79/2.14 % (2477763)Instruction limit reached! % 8.79/2.14 % (2477763)------------------------------ % 8.79/2.14 % (2477763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.79/2.14 % (2477763)CaDiCaL version: 2.1.3 % 8.79/2.14 % (2477763)Termination reason: Instruction limit % 8.79/2.14 % (2477763)Termination phase: Saturation % 8.79/2.14 % (2477763)Time elapsed: 0.018 s % 8.79/2.14 % (2477763)Peak memory usage: 89 MB % 8.79/2.14 % (2477763)Instructions burned: 29 (million) % 8.79/2.14 % (2477765)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1054707747:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 8.79/2.14 % (2477750)Instruction limit reached! % 8.79/2.14 % (2477750)------------------------------ % 8.79/2.14 % (2477750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.79/2.14 % (2477750)CaDiCaL version: 2.1.3 % 8.79/2.14 % (2477750)Termination reason: Instruction limit % 8.79/2.14 % (2477750)Termination phase: Saturation % 8.79/2.14 % (2477750)Time elapsed: 0.278 s % 8.79/2.14 % (2477750)Peak memory usage: 118 MB % 8.79/2.14 % (2477750)Instructions burned: 201 (million) % 8.79/2.14 % (2477764)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3237294139:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 8.79/2.14 % (2477766)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=2426884203:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 8.79/2.14 % (2477766)Refutation not found, incomplete strategy % 8.79/2.14 % (2477766)------------------------------ % 8.79/2.14 % (2477766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.79/2.14 % (2477766)CaDiCaL version: 2.1.3 % 8.79/2.14 % (2477766)Termination reason: Refutation not found, incomplete strategy % 8.79/2.14 % (2477766)Time elapsed: 0.009 s % 8.79/2.14 % (2477766)Peak memory usage: 89 MB % 8.79/2.14 % (2477766)Instructions burned: 7 (million) % 8.79/2.14 % (2477764)Instruction limit reached! % 8.79/2.14 % (2477764)------------------------------ % 8.79/2.14 % (2477764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.79/2.14 % (2477764)CaDiCaL version: 2.1.3 % 8.79/2.14 % (2477764)Termination reason: Instruction limit % 8.79/2.14 % (2477764)Termination phase: Saturation % 8.79/2.14 % (2477764)Time elapsed: 0.016 s % 8.79/2.14 % (2477764)Peak memory usage: 89 MB % 8.79/2.14 % (2477764)Instructions burned: 16 (million) % 8.79/2.14 % (2477765)Instruction limit reached! % 8.79/2.14 % (2477765)------------------------------ % 8.79/2.14 % (2477765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.79/2.14 % (2477765)CaDiCaL version: 2.1.3 % 8.79/2.14 % (2477765)Termination reason: Instruction limit % 8.79/2.14 % (2477765)Termination phase: Saturation % 8.79/2.14 % (2477765)Time elapsed: 0.021 s % 8.79/2.14 % (2477765)Peak memory usage: 89 MB % 8.79/2.14 % (2477765)Instructions burned: 25 (million) % 8.79/2.14 % (2477749)Instruction limit reached! % 8.79/2.14 % (2477749)------------------------------ % 8.79/2.14 % (2477749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.79/2.14 % (2477749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.12/2.41 % (2477749)CaDiCaL version: 2.1.3 % 10.12/2.41 % (2477749)Termination reason: Instruction limit % 10.12/2.41 % (2477749)Termination phase: Saturation % 10.12/2.41 % (2477749)Time elapsed: 0.351 s % 10.12/2.41 % (2477749)Peak memory usage: 118 MB % 10.12/2.41 % (2477749)Instructions burned: 307 (million) % 10.12/2.41 % (2477770)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2830251852:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 10.12/2.41 % (2477770)Instruction limit reached! % 10.12/2.41 % (2477770)------------------------------ % 10.12/2.41 % (2477770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.12/2.41 % (2477770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.12/2.41 % (2477770)CaDiCaL version: 2.1.3 % 10.12/2.41 % (2477770)Termination reason: Instruction limit % 10.12/2.41 % (2477770)Termination phase: Property scanning % 10.12/2.41 % (2477770)Time elapsed: 0.002 s % 10.12/2.41 % (2477770)Peak memory usage: 86 MB % 10.12/2.41 % (2477770)Instructions burned: 3 (million) % 10.12/2.41 % (2477769)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1876910625:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 10.12/2.41 % (2477777)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3875943936:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 10.12/2.41 % (2477777)Instruction limit reached! % 10.12/2.41 % (2477777)------------------------------ % 10.12/2.41 % (2477777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.12/2.41 % (2477777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.12/2.41 % (2477777)CaDiCaL version: 2.1.3 % 10.12/2.41 % (2477777)Termination reason: Instruction limit % 10.12/2.41 % (2477777)Termination phase: Property scanning % 10.12/2.41 % (2477777)Time elapsed: 0.005 s % 10.12/2.41 % (2477777)Peak memory usage: 86 MB % 10.12/2.41 % (2477777)Instructions burned: 4 (million) % 10.12/2.41 % (2477776)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=930884597:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 10.12/2.41 % (2477769)Instruction limit reached! % 10.12/2.41 % (2477769)------------------------------ % 10.12/2.41 % (2477769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.12/2.41 % (2477769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.12/2.41 % (2477769)CaDiCaL version: 2.1.3 % 10.12/2.41 % (2477769)Termination reason: Instruction limit % 10.12/2.41 % (2477769)Termination phase: Saturation % 10.12/2.41 % (2477769)Time elapsed: 0.085 s % 10.12/2.41 % (2477769)Peak memory usage: 89 MB % 10.12/2.41 % (2477769)Instructions burned: 85 (million) % 10.12/2.41 % (2477778)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=906438517:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi) % 10.12/2.41 % (2477779)lrs+10_1_thi=all:si=on:fd=off:random_seed=283833798:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 10.12/2.41 % (2477781)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=1569648384:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 10.12/2.41 % (2477781)Instruction limit reached! % 10.12/2.41 % (2477781)------------------------------ % 10.12/2.41 % (2477781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.12/2.41 % (2477781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.12/2.41 % (2477781)CaDiCaL version: 2.1.3 % 10.12/2.41 % (2477781)Termination reason: Instruction limit % 10.12/2.41 % (2477781)Termination phase: Saturation % 10.12/2.41 % (2477781)Time elapsed: 0.004 s % 10.12/2.41 % (2477781)Peak memory usage: 88 MB % 10.12/2.41 % (2477781)Instructions burned: 8 (million) % 10.12/2.41 % (2477766)------------------------------ % 10.12/2.41 % (2477766)------------------------------ % 10.12/2.41 % (2477776)Instruction limit reached! % 10.12/2.41 % (2477776)------------------------------ % 10.12/2.41 % (2477776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.12/2.41 % (2477776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.12/2.41 % (2477776)CaDiCaL version: 2.1.3 % 10.12/2.41 % (2477776)Termination reason: Instruction limit % 10.12/2.41 % (2477776)Termination phase: Saturation % 10.12/2.41 % (2477776)Time elapsed: 0.161 s % 10.12/2.41 % (2477776)Peak memory usage: 91 MB % 12.11/2.87 % (2477776)Instructions burned: 181 (million) % 12.11/2.87 % (2477778)Instruction limit reached! % 12.11/2.87 % (2477778)------------------------------ % 12.11/2.87 % (2477778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.11/2.87 % (2477778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.11/2.87 % (2477778)CaDiCaL version: 2.1.3 % 12.11/2.87 % (2477778)Termination reason: Instruction limit % 12.11/2.87 % (2477778)Termination phase: Saturation % 12.11/2.87 % (2477778)Time elapsed: 0.139 s % 12.11/2.87 % (2477778)Peak memory usage: 134 MB % 12.11/2.87 % (2477778)Instructions burned: 67 (million) % 12.11/2.87 % (2477779)Instruction limit reached! % 12.11/2.87 % (2477779)------------------------------ % 12.11/2.87 % (2477779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.11/2.87 % (2477779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.11/2.87 % (2477779)CaDiCaL version: 2.1.3 % 12.11/2.87 % (2477779)Termination reason: Instruction limit % 12.11/2.87 % (2477779)Termination phase: Saturation % 12.11/2.87 % (2477779)Time elapsed: 0.091 s % 12.11/2.87 % (2477779)Peak memory usage: 116 MB % 12.11/2.87 % (2477779)Instructions burned: 53 (million) % 12.11/2.87 % (2477784)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2506356908:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 12.11/2.87 % (2477784)Instruction limit reached! % 12.11/2.87 % (2477784)------------------------------ % 12.11/2.87 % (2477784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.11/2.87 % (2477784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.11/2.87 % (2477784)CaDiCaL version: 2.1.3 % 12.11/2.87 % (2477784)Termination reason: Instruction limit % 12.11/2.87 % (2477784)Termination phase: Equality resolution with deletion % 12.11/2.87 % (2477784)Time elapsed: 0.002 s % 12.11/2.87 % (2477784)Peak memory usage: 86 MB % 12.11/2.87 % (2477784)Instructions burned: 3 (million) % 12.11/2.87 % (2477787)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3460006717:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi) % 12.11/2.87 % (2477787)Instruction limit reached! % 12.11/2.87 % (2477787)------------------------------ % 12.11/2.87 % (2477787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.11/2.87 % (2477787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.11/2.87 % (2477787)CaDiCaL version: 2.1.3 % 12.11/2.87 % (2477787)Termination reason: Instruction limit % 12.11/2.87 % (2477787)Termination phase: Preprocessing 3 % 12.11/2.87 % (2477787)Time elapsed: 0.003 s % 12.11/2.87 % (2477787)Peak memory usage: 86 MB % 12.11/2.87 % (2477787)Instructions burned: 2 (million) % 12.11/2.87 % (2477790)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=725917451:i=127:doe=on:rtra=on_2990 on theBenchmark for (2990ds/127Mi) % 12.11/2.87 % (2477792)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2160790126:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 12.11/2.87 % (2477792)Refutation not found, incomplete strategy % 12.11/2.87 % (2477792)------------------------------ % 12.11/2.87 % (2477792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.11/2.87 % (2477792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.11/2.87 % (2477792)CaDiCaL version: 2.1.3 % 12.11/2.87 % (2477792)Termination reason: Refutation not found, incomplete strategy % 12.11/2.87 % (2477792)Time elapsed: 0.010 s % 12.11/2.87 % (2477792)Peak memory usage: 89 MB % 12.11/2.87 % (2477792)Instructions burned: 8 (million) % 12.11/2.87 % (2477791)dis+10_1_si=on:random_seed=1574097445:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 12.11/2.87 % (2477791)Instruction limit reached! % 12.11/2.87 % (2477791)------------------------------ % 12.11/2.87 % (2477791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.11/2.87 % (2477791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.11/2.87 % (2477791)CaDiCaL version: 2.1.3 % 12.11/2.87 % (2477791)Termination reason: Instruction limit % 12.11/2.87 % (2477791)Termination phase: Saturation % 12.11/2.87 % (2477791)Time elapsed: 0.012 s % 12.11/2.87 % (2477791)Peak memory usage: 88 MB % 12.11/2.87 % (2477791)Instructions burned: 10 (million) % 12.11/2.87 % (2477794)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1538629890:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 16.37/3.19 % (2477793)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3354674960:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 16.37/3.19 % (2477794)Instruction limit reached! % 16.37/3.19 % (2477794)------------------------------ % 16.37/3.19 % (2477794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.37/3.19 % (2477794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.37/3.19 % (2477794)CaDiCaL version: 2.1.3 % 16.37/3.19 % (2477794)Termination reason: Instruction limit % 16.37/3.19 % (2477794)Termination phase: Property scanning % 16.37/3.19 % (2477794)Time elapsed: 0.004 s % 16.37/3.19 % (2477794)Peak memory usage: 86 MB % 16.37/3.19 % (2477794)Instructions burned: 3 (million) % 16.37/3.19 % (2477793)Instruction limit reached! % 16.37/3.19 % (2477793)------------------------------ % 16.37/3.19 % (2477793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.37/3.19 % (2477793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.37/3.19 % (2477793)CaDiCaL version: 2.1.3 % 16.37/3.19 % (2477793)Termination reason: Instruction limit % 16.37/3.19 % (2477793)Termination phase: Saturation % 16.37/3.19 % (2477793)Time elapsed: 0.044 s % 16.37/3.19 % (2477793)Peak memory usage: 89 MB % 16.37/3.19 % (2477793)Instructions burned: 35 (million) % 16.37/3.19 % (2477798)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3715530585:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 16.37/3.19 % (2477796)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2971487039:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 16.37/3.19 % (2477790)Instruction limit reached! % 16.37/3.19 % (2477790)------------------------------ % 16.37/3.19 % (2477790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.37/3.19 % (2477790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.37/3.19 % (2477790)CaDiCaL version: 2.1.3 % 16.37/3.19 % (2477790)Termination reason: Instruction limit % 16.37/3.19 % (2477790)Termination phase: Saturation % 16.37/3.19 % (2477790)Time elapsed: 0.182 s % 16.37/3.19 % (2477790)Peak memory usage: 117 MB % 16.37/3.19 % (2477790)Instructions burned: 127 (million) % 16.37/3.19 % (2477796)Instruction limit reached! % 16.37/3.19 % (2477796)------------------------------ % 16.37/3.19 % (2477796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.37/3.19 % (2477796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.37/3.19 % (2477796)CaDiCaL version: 2.1.3 % 16.37/3.19 % (2477796)Termination reason: Instruction limit % 16.37/3.19 % (2477796)Termination phase: Saturation % 16.37/3.19 % (2477796)Time elapsed: 0.009 s % 16.37/3.19 % (2477796)Peak memory usage: 88 MB % 16.37/3.19 % (2477796)Instructions burned: 8 (million) % 16.37/3.19 % (2477798)Instruction limit reached! % 16.37/3.19 % (2477798)------------------------------ % 16.37/3.19 % (2477798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.37/3.19 % (2477798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.37/3.19 % (2477798)CaDiCaL version: 2.1.3 % 16.37/3.19 % (2477798)Termination reason: Instruction limit % 16.37/3.19 % (2477798)Termination phase: Saturation % 16.37/3.19 % (2477798)Time elapsed: 0.164 s % 16.37/3.19 % (2477798)Peak memory usage: 95 MB % 16.37/3.19 % (2477798)Instructions burned: 371 (million) % 16.37/3.19 % (2477802)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1021203337:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/13Mi) % 16.37/3.19 % (2477805)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1684080857:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi) % 16.37/3.19 % (2477802)Instruction limit reached! % 16.37/3.19 % (2477802)------------------------------ % 16.37/3.19 % (2477802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.37/3.19 % (2477802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.37/3.19 % (2477802)CaDiCaL version: 2.1.3 % 16.37/3.19 % (2477802)Termination reason: Instruction limit % 16.37/3.19 % (2477802)Termination phase: Saturation % 16.37/3.19 % (2477802)Time elapsed: 0.043 s % 16.37/3.19 % (2477802)Peak memory usage: 112 MB % 16.37/3.19 % (2477802)Instructions burned: 13 (million) % 18.51/3.64 % (2477807)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1130168648:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi) % 18.51/3.64 % (2477809)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=255994913:i=71:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/71Mi) % 18.51/3.64 % (2477807)Instruction limit reached! % 18.51/3.64 % (2477807)------------------------------ % 18.51/3.64 % (2477807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.51/3.64 % (2477807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.51/3.64 % (2477807)CaDiCaL version: 2.1.3 % 18.51/3.64 % (2477807)Termination reason: Instruction limit % 18.51/3.64 % (2477807)Termination phase: Saturation % 18.51/3.64 % (2477807)Time elapsed: 0.013 s % 18.51/3.64 % (2477807)Peak memory usage: 88 MB % 18.51/3.64 % (2477807)Instructions burned: 10 (million) % 18.51/3.64 % (2477792)------------------------------ % 18.51/3.64 % (2477792)------------------------------ % 18.51/3.64 % (2477810)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=3355233944:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2986 on theBenchmark for (2986ds/75Mi) % 18.51/3.64 % (2477811)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=1105404143:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2985 on theBenchmark for (2985ds/294Mi) % 18.51/3.64 % (2477810)Instruction limit reached! % 18.51/3.64 % (2477810)------------------------------ % 18.51/3.64 % (2477810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.51/3.64 % (2477810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.51/3.64 % (2477810)CaDiCaL version: 2.1.3 % 18.51/3.64 % (2477810)Termination reason: Instruction limit % 18.51/3.64 % (2477810)Termination phase: Saturation % 18.51/3.64 % (2477810)Time elapsed: 0.078 s % 18.51/3.64 % (2477810)Peak memory usage: 91 MB % 18.51/3.64 % (2477810)Instructions burned: 75 (million) % 18.51/3.64 % (2477809)Instruction limit reached! % 18.51/3.64 % (2477809)------------------------------ % 18.51/3.64 % (2477809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.51/3.64 % (2477809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.51/3.64 % (2477809)CaDiCaL version: 2.1.3 % 18.51/3.64 % (2477809)Termination reason: Instruction limit % 18.51/3.64 % (2477809)Termination phase: Saturation % 18.51/3.64 % (2477809)Time elapsed: 0.141 s % 18.51/3.64 % (2477809)Peak memory usage: 133 MB % 18.51/3.64 % (2477809)Instructions burned: 71 (million) % 18.51/3.64 % (2477817)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2813772235:i=131:rtra=on_2984 on theBenchmark for (2984ds/131Mi) % 18.51/3.64 % (2477814)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2173217918:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/130Mi) % 18.51/3.64 % (2477805)Instruction limit reached! % 18.51/3.64 % (2477805)------------------------------ % 18.51/3.64 % (2477805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.51/3.64 % (2477805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.51/3.64 % (2477805)CaDiCaL version: 2.1.3 % 18.51/3.64 % (2477805)Termination reason: Instruction limit % 18.51/3.64 % (2477805)Termination phase: Saturation % 18.51/3.64 % (2477805)Time elapsed: 0.289 s % 18.51/3.64 % (2477805)Peak memory usage: 119 MB % 18.51/3.64 % (2477805)Instructions burned: 226 (million) % 18.51/3.64 % (2477817)Instruction limit reached! % 18.51/3.64 % (2477817)------------------------------ % 18.51/3.64 % (2477817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.51/3.64 % (2477817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.51/3.64 % (2477817)CaDiCaL version: 2.1.3 % 18.51/3.64 % (2477817)Termination reason: Instruction limit % 18.51/3.64 % (2477817)Termination phase: Saturation % 18.51/3.64 % (2477817)Time elapsed: 0.108 s % 18.51/3.64 % (2477817)Peak memory usage: 135 MB % 18.51/3.64 % (2477817)Instructions burned: 132 (million) % 18.51/3.64 % (2477819)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=475146361:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2983 on theBenchmark for (2983ds/40Mi) % 18.51/3.64 % (2477814)Instruction limit reached! % 18.51/3.64 % (2477814)------------------------------ % 18.51/3.64 % (2477814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.38/4.15 % (2477814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.38/4.15 % (2477814)CaDiCaL version: 2.1.3 % 23.38/4.15 % (2477814)Termination reason: Instruction limit % 23.38/4.15 % (2477814)Termination phase: Saturation % 23.38/4.15 % (2477814)Time elapsed: 0.175 s % 23.38/4.15 % (2477814)Peak memory usage: 118 MB % 23.38/4.15 % (2477814)Instructions burned: 130 (million) % 23.38/4.15 % (2477821)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3914480460:i=307:rtra=on:gtg=exists_top_2982 on theBenchmark for (2982ds/307Mi) % 23.38/4.15 % (2477811)Instruction limit reached! % 23.38/4.15 % (2477811)------------------------------ % 23.38/4.15 % (2477811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.38/4.15 % (2477811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.38/4.15 % (2477811)CaDiCaL version: 2.1.3 % 23.38/4.15 % (2477811)Termination reason: Instruction limit % 23.38/4.15 % (2477811)Termination phase: Saturation % 23.38/4.15 % (2477811)Time elapsed: 0.320 s % 23.38/4.15 % (2477811)Peak memory usage: 91 MB % 23.38/4.15 % (2477811)Instructions burned: 294 (million) % 23.38/4.15 % (2477822)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1025657620:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/598Mi) % 23.38/4.15 % (2477819)Instruction limit reached! % 23.38/4.15 % (2477819)------------------------------ % 23.38/4.15 % (2477819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.38/4.15 % (2477819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.38/4.15 % (2477819)CaDiCaL version: 2.1.3 % 23.38/4.15 % (2477819)Termination reason: Instruction limit % 23.38/4.15 % (2477819)Termination phase: Saturation % 23.38/4.15 % (2477819)Time elapsed: 0.102 s % 23.38/4.15 % (2477819)Peak memory usage: 133 MB % 23.38/4.15 % (2477819)Instructions burned: 40 (million) % 23.38/4.15 % (2477825)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=353269569:i=131:canc=cautious:fsr=off:rtra=on_2981 on theBenchmark for (2981ds/131Mi) % 23.38/4.15 % (2477827)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=3418269444:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2981 on theBenchmark for (2981ds/259Mi) % 23.38/4.15 % (2477825)Instruction limit reached! % 23.38/4.15 % (2477825)------------------------------ % 23.38/4.15 % (2477825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.38/4.15 % (2477825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.38/4.15 % (2477825)CaDiCaL version: 2.1.3 % 23.38/4.15 % (2477825)Termination reason: Instruction limit % 23.38/4.15 % (2477825)Termination phase: Saturation % 23.38/4.15 % (2477825)Time elapsed: 0.154 s % 23.38/4.15 % (2477825)Peak memory usage: 117 MB % 23.38/4.15 % (2477825)Instructions burned: 131 (million) % 23.38/4.15 % (2477827)Instruction limit reached! % 23.38/4.15 % (2477827)------------------------------ % 23.38/4.15 % (2477827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.38/4.15 % (2477827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.38/4.15 % (2477827)CaDiCaL version: 2.1.3 % 23.38/4.15 % (2477827)Termination reason: Instruction limit % 23.38/4.15 % (2477827)Termination phase: Saturation % 23.38/4.15 % (2477827)Time elapsed: 0.137 s % 23.38/4.15 % (2477827)Peak memory usage: 119 MB % 23.38/4.15 % (2477827)Instructions burned: 262 (million) % 23.38/4.15 % (2477829)dis+10_1_si=on:random_seed=942093556:s2a=on:i=1000:rtra=on:gtg=exists_all_2980 on theBenchmark for (2980ds/1000Mi) % 23.38/4.15 % (2477830)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1846422916:i=383:fsr=off:rtra=on:ev=force_2980 on theBenchmark for (2980ds/383Mi) % 23.38/4.15 % (2477821)Instruction limit reached! % 23.38/4.15 % (2477821)------------------------------ % 23.38/4.15 % (2477821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.38/4.15 % (2477821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.38/4.15 % (2477821)CaDiCaL version: 2.1.3 % 23.38/4.15 % (2477821)Termination reason: Instruction limit % 23.38/4.15 % (2477821)Termination phase: Saturation % 23.38/4.15 % (2477821)Time elapsed: 0.315 s % 23.38/4.15 % (2477821)Peak memory usage: 92 MB % 23.38/4.15 % (2477821)Instructions burned: 307 (million) % 23.38/4.15 % (2477832)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1943254304:i=141:doe=on:rtra=on_2979 on theBenchmark for (2979ds/141Mi) % 24.28/4.69 % (2477836)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2467366891:i=121:nm=16:rtra=on_2977 on theBenchmark for (2977ds/121Mi) % 24.28/4.69 % (2477836)Instruction limit reached! % 24.28/4.69 % (2477836)------------------------------ % 24.28/4.69 % (2477836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.69 % (2477836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.69 % (2477836)CaDiCaL version: 2.1.3 % 24.28/4.69 % (2477836)Termination reason: Instruction limit % 24.28/4.69 % (2477836)Termination phase: Saturation % 24.28/4.69 % (2477836)Time elapsed: 0.062 s % 24.28/4.69 % (2477836)Peak memory usage: 89 MB % 24.28/4.69 % (2477836)Instructions burned: 123 (million) % 24.28/4.69 % (2477832)Instruction limit reached! % 24.28/4.69 % (2477832)------------------------------ % 24.28/4.69 % (2477832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.69 % (2477832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.69 % (2477832)CaDiCaL version: 2.1.3 % 24.28/4.69 % (2477832)Termination reason: Instruction limit % 24.28/4.69 % (2477832)Termination phase: Saturation % 24.28/4.69 % (2477832)Time elapsed: 0.161 s % 24.28/4.69 % (2477832)Peak memory usage: 90 MB % 24.28/4.69 % (2477832)Instructions burned: 143 (million) % 24.28/4.69 % (2477835)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3111310566:i=65:nm=16:rtra=on_2977 on theBenchmark for (2977ds/65Mi) % 24.28/4.69 % (2477840)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=3619496473:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 24.28/4.69 % (2477835)Instruction limit reached! % 24.28/4.69 % (2477835)------------------------------ % 24.28/4.69 % (2477835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.69 % (2477835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.69 % (2477835)CaDiCaL version: 2.1.3 % 24.28/4.69 % (2477835)Termination reason: Instruction limit % 24.28/4.69 % (2477835)Termination phase: Saturation % 24.28/4.69 % (2477835)Time elapsed: 0.104 s % 24.28/4.69 % (2477835)Peak memory usage: 118 MB % 24.28/4.69 % (2477835)Instructions burned: 66 (million) % 24.28/4.69 % (2477830)Instruction limit reached! % 24.28/4.69 % (2477830)------------------------------ % 24.28/4.69 % (2477830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.69 % (2477830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.69 % (2477830)CaDiCaL version: 2.1.3 % 24.28/4.69 % (2477830)Termination reason: Instruction limit % 24.28/4.69 % (2477830)Termination phase: Saturation % 24.28/4.69 % (2477830)Time elapsed: 0.353 s % 24.28/4.69 % (2477830)Peak memory usage: 92 MB % 24.28/4.69 % (2477830)Instructions burned: 383 (million) % 24.28/4.69 % (2477822)Instruction limit reached! % 24.28/4.69 % (2477822)------------------------------ % 24.28/4.69 % (2477822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.69 % (2477822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.69 % (2477822)CaDiCaL version: 2.1.3 % 24.28/4.69 % (2477822)Termination reason: Instruction limit % 24.28/4.69 % (2477822)Termination phase: Saturation % 24.28/4.69 % (2477822)Time elapsed: 0.656 s % 24.28/4.69 % (2477822)Peak memory usage: 137 MB % 24.28/4.69 % (2477822)Instructions burned: 598 (million) % 24.28/4.69 % (2477842)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=3611940881:i=39:ins=3:rtra=on_2975 on theBenchmark for (2975ds/39Mi) % 24.28/4.69 % (2477842)Instruction limit reached! % 24.28/4.69 % (2477842)------------------------------ % 24.28/4.69 % (2477842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.28/4.69 % (2477842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.28/4.69 % (2477842)CaDiCaL version: 2.1.3 % 24.28/4.69 % (2477842)Termination reason: Instruction limit % 24.28/4.69 % (2477842)Termination phase: Saturation % 24.28/4.69 % (2477842)Time elapsed: 0.040 s % 24.28/4.69 % (2477842)Peak memory usage: 116 MB % 24.28/4.69 % (2477842)Instructions burned: 41 (million) % 24.28/4.69 % (2477840)Instruction limit reached! % 24.28/4.69 % (2477840)------------------------------ % 24.28/4.69 % (2477840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.58/5.21 % (2477843)dis+1010_1_to=kbo:si=on:random_seed=3372865548:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi) % 30.58/5.21 % (2477840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.58/5.21 % (2477840)CaDiCaL version: 2.1.3 % 30.58/5.21 % (2477840)Termination reason: Instruction limit % 30.58/5.21 % (2477840)Termination phase: Saturation % 30.58/5.21 % (2477840)Time elapsed: 0.169 s % 30.58/5.21 % (2477840)Peak memory usage: 119 MB % 30.58/5.21 % (2477840)Instructions burned: 129 (million) % 30.58/5.21 % (2477847)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3160780057:s2a=on:i=483:doe=on:nm=32:rtra=on_2973 on theBenchmark for (2973ds/483Mi) % 30.58/5.21 % (2477846)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2535412288:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/329Mi) % 30.58/5.21 % (2477850)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3403858610:i=349:rtra=on_2972 on theBenchmark for (2972ds/349Mi) % 30.58/5.21 % (2477849)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=171662910:thitd=on:i=215:nm=0:rtra=on:ev=force_2973 on theBenchmark for (2973ds/215Mi) % 30.58/5.21 % (2477843)Instruction limit reached! % 30.58/5.21 % (2477843)------------------------------ % 30.58/5.21 % (2477843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.58/5.21 % (2477843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.58/5.21 % (2477843)CaDiCaL version: 2.1.3 % 30.58/5.21 % (2477843)Termination reason: Instruction limit % 30.58/5.21 % (2477843)Termination phase: Saturation % 30.58/5.21 % (2477843)Time elapsed: 0.184 s % 30.58/5.21 % (2477843)Peak memory usage: 91 MB % 30.58/5.21 % (2477843)Instructions burned: 175 (million) % 30.58/5.21 % (2477852)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3190777011:st=2:i=295:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/295Mi) % 30.58/5.21 % (2477852)Instruction limit reached! % 30.58/5.21 % (2477852)------------------------------ % 30.58/5.21 % (2477852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.58/5.21 % (2477852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.58/5.21 % (2477852)CaDiCaL version: 2.1.3 % 30.58/5.21 % (2477852)Termination reason: Instruction limit % 30.58/5.21 % (2477852)Termination phase: Saturation % 30.58/5.21 % (2477852)Time elapsed: 0.122 s % 30.58/5.21 % (2477852)Peak memory usage: 90 MB % 30.58/5.21 % (2477852)Instructions burned: 295 (million) % 30.58/5.21 % (2477849)Instruction limit reached! % 30.58/5.21 % (2477849)------------------------------ % 30.58/5.21 % (2477849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.58/5.21 % (2477849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.58/5.21 % (2477849)CaDiCaL version: 2.1.3 % 30.58/5.21 % (2477849)Termination reason: Instruction limit % 30.58/5.21 % (2477849)Termination phase: Saturation % 30.58/5.21 % (2477849)Time elapsed: 0.270 s % 30.58/5.21 % (2477849)Peak memory usage: 135 MB % 30.58/5.21 % (2477849)Instructions burned: 215 (million) % 30.58/5.21 % (2477857)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=708200599:i=328:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/328Mi) % 30.58/5.21 % (2477850)Instruction limit reached! % 30.58/5.21 % (2477850)------------------------------ % 30.58/5.21 % (2477850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.58/5.21 % (2477850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.58/5.21 % (2477850)CaDiCaL version: 2.1.3 % 30.58/5.21 % (2477850)Termination reason: Instruction limit % 30.58/5.21 % (2477850)Termination phase: Saturation % 30.58/5.21 % (2477850)Time elapsed: 0.359 s % 30.58/5.21 % (2477850)Peak memory usage: 117 MB % 30.58/5.21 % (2477850)Instructions burned: 349 (million) % 30.58/5.21 % (2477846)Instruction limit reached! % 30.58/5.21 % (2477846)------------------------------ % 30.58/5.21 % (2477846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.58/5.21 % (2477846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.58/5.21 % (2477846)CaDiCaL version: 2.1.3 % 30.58/5.21 % (2477846)Termination reason: Instruction limit % 32.25/5.60 % (2477846)Termination phase: Saturation % 32.25/5.60 % (2477846)Time elapsed: 0.386 s % 32.25/5.60 % (2477846)Peak memory usage: 119 MB % 32.25/5.60 % (2477846)Instructions burned: 329 (million) % 32.25/5.60 % (2477829)Instruction limit reached! % 32.25/5.60 % (2477829)------------------------------ % 32.25/5.60 % (2477829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.60 % (2477829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.60 % (2477829)CaDiCaL version: 2.1.3 % 32.25/5.60 % (2477829)Termination reason: Instruction limit % 32.25/5.60 % (2477829)Termination phase: Saturation % 32.25/5.60 % (2477829)Time elapsed: 1.004 s % 32.25/5.60 % (2477829)Peak memory usage: 96 MB % 32.25/5.60 % (2477829)Instructions burned: 1000 (million) % 32.25/5.60 % (2477859)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=491905095:i=281:gtgl=2:rtra=on:gtg=all_2969 on theBenchmark for (2969ds/281Mi) % 32.25/5.60 % (2477847)Instruction limit reached! % 32.25/5.60 % (2477847)------------------------------ % 32.25/5.60 % (2477847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.60 % (2477847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.60 % (2477847)CaDiCaL version: 2.1.3 % 32.25/5.60 % (2477847)Termination reason: Instruction limit % 32.25/5.60 % (2477847)Termination phase: Saturation % 32.25/5.60 % (2477847)Time elapsed: 0.614 s % 32.25/5.60 % (2477847)Peak memory usage: 136 MB % 32.25/5.60 % (2477847)Instructions burned: 483 (million) % 32.25/5.60 % (2477859)Instruction limit reached! % 32.25/5.60 % (2477859)------------------------------ % 32.25/5.60 % (2477859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.60 % (2477859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.60 % (2477859)CaDiCaL version: 2.1.3 % 32.25/5.60 % (2477859)Termination reason: Instruction limit % 32.25/5.60 % (2477859)Termination phase: Saturation % 32.25/5.60 % (2477859)Time elapsed: 0.164 s % 32.25/5.60 % (2477859)Peak memory usage: 117 MB % 32.25/5.60 % (2477859)Instructions burned: 283 (million) % 32.25/5.60 % (2477860)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=926176740:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/484Mi) % 32.25/5.60 % (2477862)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1117725296:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2967 on theBenchmark for (2967ds/321Mi) % 32.25/5.60 % (2477863)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3339166425:i=416:rtra=on:gtg=position:ss=axioms_2967 on theBenchmark for (2967ds/416Mi) % 32.25/5.60 % (2477864)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=675270719:i=471:thf=on:kws=precedence:rtra=on_2967 on theBenchmark for (2967ds/471Mi) % 32.25/5.60 % (2477857)Instruction limit reached! % 32.25/5.60 % (2477857)------------------------------ % 32.25/5.60 % (2477857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.60 % (2477857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.60 % (2477857)CaDiCaL version: 2.1.3 % 32.25/5.60 % (2477857)Termination reason: Instruction limit % 32.25/5.60 % (2477857)Termination phase: Saturation % 32.25/5.60 % (2477857)Time elapsed: 0.367 s % 32.25/5.60 % (2477857)Peak memory usage: 120 MB % 32.25/5.60 % (2477857)Instructions burned: 329 (million) % 32.25/5.60 % (2477868)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2925190312:i=375:kws=inv_arity_squared:rtra=on_2965 on theBenchmark for (2965ds/375Mi) % 32.25/5.60 % (2477867)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=3900230006:avsq=on:i=276:avsqr=1,2:rtra=on_2965 on theBenchmark for (2965ds/276Mi) % 32.25/5.60 % (2477862)Instruction limit reached! % 32.25/5.60 % (2477862)------------------------------ % 32.25/5.60 % (2477862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.60 % (2477862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.60 % (2477862)CaDiCaL version: 2.1.3 % 32.25/5.60 % (2477862)Termination reason: Instruction limit % 32.25/5.60 % (2477862)Termination phase: Saturation % 32.25/5.60 % (2477862)Time elapsed: 0.278 s % 32.25/5.60 % (2477862)Peak memory usage: 114 MB % 32.25/5.60 % (2477862)Instructions burned: 321 (million) % 32.25/5.60 % (2477872)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3475622698:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/387Mi) % 38.16/6.33 % (2477868)Instruction limit reached! % 38.16/6.33 % (2477868)------------------------------ % 38.16/6.33 % (2477868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.16/6.33 % (2477868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.16/6.33 % (2477868)CaDiCaL version: 2.1.3 % 38.16/6.33 % (2477868)Termination reason: Instruction limit % 38.16/6.33 % (2477868)Termination phase: Saturation % 38.16/6.33 % (2477868)Time elapsed: 0.210 s % 38.16/6.33 % (2477868)Peak memory usage: 119 MB % 38.16/6.33 % (2477868)Instructions burned: 375 (million) % 38.16/6.33 % (2477860)Instruction limit reached! % 38.16/6.33 % (2477860)------------------------------ % 38.16/6.33 % (2477860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.16/6.33 % (2477860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.16/6.33 % (2477860)CaDiCaL version: 2.1.3 % 38.16/6.33 % (2477860)Termination reason: Instruction limit % 38.16/6.33 % (2477860)Termination phase: Saturation % 38.16/6.33 % (2477860)Time elapsed: 0.455 s % 38.16/6.33 % (2477860)Peak memory usage: 92 MB % 38.16/6.33 % (2477860)Instructions burned: 484 (million) % 38.16/6.33 % (2477863)Instruction limit reached! % 38.16/6.33 % (2477863)------------------------------ % 38.16/6.33 % (2477863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.16/6.33 % (2477863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.16/6.33 % (2477863)CaDiCaL version: 2.1.3 % 38.16/6.33 % (2477863)Termination reason: Instruction limit % 38.16/6.33 % (2477863)Termination phase: Saturation % 38.16/6.33 % (2477863)Time elapsed: 0.446 s % 38.16/6.33 % (2477863)Peak memory usage: 120 MB % 38.16/6.33 % (2477863)Instructions burned: 417 (million) % 38.16/6.33 % (2477876)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2325332171:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2962 on theBenchmark for (2962ds/513Mi) % 38.16/6.33 % (2477864)Instruction limit reached! % 38.16/6.33 % (2477864)------------------------------ % 38.16/6.33 % (2477864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.16/6.33 % (2477864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.16/6.33 % (2477864)CaDiCaL version: 2.1.3 % 38.16/6.33 % (2477864)Termination reason: Instruction limit % 38.16/6.33 % (2477864)Termination phase: Saturation % 38.16/6.33 % (2477864)Time elapsed: 0.515 s % 38.16/6.33 % (2477864)Peak memory usage: 122 MB % 38.16/6.33 % (2477864)Instructions burned: 471 (million) % 38.16/6.33 % (2477867)Instruction limit reached! % 38.16/6.33 % (2477867)------------------------------ % 38.16/6.33 % (2477867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.16/6.33 % (2477867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.16/6.33 % (2477867)CaDiCaL version: 2.1.3 % 38.16/6.33 % (2477867)Termination reason: Instruction limit % 38.16/6.33 % (2477867)Termination phase: Saturation % 38.16/6.33 % (2477867)Time elapsed: 0.363 s % 38.16/6.33 % (2477867)Peak memory usage: 136 MB % 38.16/6.33 % (2477867)Instructions burned: 279 (million) % 38.16/6.33 % (2477877)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2975546433:i=334:rtra=on_2961 on theBenchmark for (2961ds/334Mi) % 38.16/6.33 % (2477878)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3201560265:i=359:rtra=on:gtg=exists_top:ss=axioms_2960 on theBenchmark for (2960ds/359Mi) % 38.16/6.33 % (2477872)Instruction limit reached! % 38.16/6.33 % (2477872)------------------------------ % 38.16/6.33 % (2477872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.16/6.33 % (2477872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.16/6.33 % (2477872)CaDiCaL version: 2.1.3 % 38.16/6.33 % (2477872)Termination reason: Instruction limit % 38.16/6.33 % (2477872)Termination phase: Saturation % 38.16/6.33 % (2477872)Time elapsed: 0.418 s % 38.16/6.33 % (2477872)Peak memory usage: 119 MB % 38.16/6.33 % (2477872)Instructions burned: 387 (million) % 38.16/6.33 % (2477879)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3817218677:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi) % 38.16/6.33 % (2477877)Instruction limit reached! % 38.16/6.33 % (2477877)------------------------------ % 44.97/7.22 % (2477877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.97/7.22 % (2477877)CaDiCaL version: 2.1.3 % 44.97/7.22 % (2477877)Termination reason: Instruction limit % 44.97/7.22 % (2477877)Termination phase: Saturation % 44.97/7.22 % (2477877)Time elapsed: 0.202 s % 44.97/7.22 % (2477877)Peak memory usage: 137 MB % 44.97/7.22 % (2477877)Instructions burned: 336 (million) % 44.97/7.22 % (2477881)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=214593459:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/261Mi) % 44.97/7.22 % (2477883)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=1813402698:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2958 on theBenchmark for (2958ds/235Mi) % 44.97/7.22 % (2477885)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3631209237:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2957 on theBenchmark for (2957ds/273Mi) % 44.97/7.22 % (2477887)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3973980701:i=146:doe=on:rtra=on_2956 on theBenchmark for (2956ds/146Mi) % 44.97/7.22 % (2477878)Instruction limit reached! % 44.97/7.22 % (2477878)------------------------------ % 44.97/7.22 % (2477878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.97/7.22 % (2477878)CaDiCaL version: 2.1.3 % 44.97/7.22 % (2477878)Termination reason: Instruction limit % 44.97/7.22 % (2477878)Termination phase: Saturation % 44.97/7.22 % (2477878)Time elapsed: 0.349 s % 44.97/7.22 % (2477878)Peak memory usage: 92 MB % 44.97/7.22 % (2477878)Instructions burned: 359 (million) % 44.97/7.22 % (2477876)Instruction limit reached! % 44.97/7.22 % (2477876)------------------------------ % 44.97/7.22 % (2477876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.97/7.22 % (2477876)CaDiCaL version: 2.1.3 % 44.97/7.22 % (2477876)Termination reason: Instruction limit % 44.97/7.22 % (2477876)Termination phase: Saturation % 44.97/7.22 % (2477876)Time elapsed: 0.501 s % 44.97/7.22 % (2477876)Peak memory usage: 93 MB % 44.97/7.22 % (2477876)Instructions burned: 513 (million) % 44.97/7.22 % (2477879)Instruction limit reached! % 44.97/7.22 % (2477879)------------------------------ % 44.97/7.22 % (2477879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.97/7.22 % (2477879)CaDiCaL version: 2.1.3 % 44.97/7.22 % (2477879)Termination reason: Instruction limit % 44.97/7.22 % (2477879)Termination phase: Saturation % 44.97/7.22 % (2477879)Time elapsed: 0.348 s % 44.97/7.22 % (2477879)Peak memory usage: 118 MB % 44.97/7.22 % (2477879)Instructions burned: 341 (million) % 44.97/7.22 % (2477887)Instruction limit reached! % 44.97/7.22 % (2477887)------------------------------ % 44.97/7.22 % (2477887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.97/7.22 % (2477887)CaDiCaL version: 2.1.3 % 44.97/7.22 % (2477887)Termination reason: Instruction limit % 44.97/7.22 % (2477887)Termination phase: Saturation % 44.97/7.22 % (2477887)Time elapsed: 0.080 s % 44.97/7.22 % (2477887)Peak memory usage: 90 MB % 44.97/7.22 % (2477887)Instructions burned: 148 (million) % 44.97/7.22 % (2477881)Refutation not found, incomplete strategy % 44.97/7.22 % (2477881)------------------------------ % 44.97/7.22 % (2477881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.97/7.22 % (2477881)CaDiCaL version: 2.1.3 % 44.97/7.22 % (2477881)Termination reason: Refutation not found, incomplete strategy % 44.97/7.22 % (2477881)Time elapsed: 0.311 s % 44.97/7.22 % (2477881)Peak memory usage: 119 MB % 44.97/7.22 % (2477881)Instructions burned: 258 (million) % 44.97/7.22 % (2477883)Instruction limit reached! % 44.97/7.22 % (2477883)------------------------------ % 44.97/7.22 % (2477883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.97/7.22 % (2477883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.75/7.96 % (2477883)CaDiCaL version: 2.1.3 % 47.75/7.96 % (2477883)Termination reason: Instruction limit % 47.75/7.96 % (2477883)Termination phase: Saturation % 47.75/7.96 % (2477883)Time elapsed: 0.292 s % 47.75/7.96 % (2477883)Peak memory usage: 119 MB % 47.75/7.96 % (2477883)Instructions burned: 235 (million) % 47.75/7.96 % (2477885)Instruction limit reached! % 47.75/7.96 % (2477885)------------------------------ % 47.75/7.96 % (2477885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.75/7.96 % (2477885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.75/7.96 % (2477885)CaDiCaL version: 2.1.3 % 47.75/7.96 % (2477885)Termination reason: Instruction limit % 47.75/7.96 % (2477885)Termination phase: Saturation % 47.75/7.96 % (2477885)Time elapsed: 0.331 s % 47.75/7.96 % (2477885)Peak memory usage: 93 MB % 47.75/7.96 % (2477885)Instructions burned: 273 (million) % 47.75/7.96 % (2477893)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=2802621324:avsq=on:i=276:avsqr=1,2:rtra=on_2954 on theBenchmark for (2954ds/276Mi) % 47.75/7.96 % (2477892)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2714125705:i=4428:doe=on:fsr=off:rtra=on_2954 on theBenchmark for (2954ds/4428Mi) % 47.75/7.96 % (2477895)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=199430414:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2953 on theBenchmark for (2953ds/655Mi) % 47.75/7.96 % (2477894)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=26622282:i=1052:rtra=on_2953 on theBenchmark for (2953ds/1052Mi) % 47.75/7.96 % (2477896)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2823907855:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2952 on theBenchmark for (2952ds/1054Mi) % 47.75/7.96 % (2477897)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2564927034:i=107:rtra=on_2951 on theBenchmark for (2951ds/107Mi) % 47.75/7.96 % (2477881)------------------------------ % 47.75/7.96 % (2477881)------------------------------ % 47.75/7.96 % (2477897)Refutation not found, incomplete strategy % 47.75/7.96 % (2477897)------------------------------ % 47.75/7.96 % (2477897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.75/7.96 % (2477897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.75/7.96 % (2477897)CaDiCaL version: 2.1.3 % 47.75/7.96 % (2477897)Termination reason: Refutation not found, incomplete strategy % 47.75/7.96 % (2477897)Time elapsed: 0.049 s % 47.75/7.96 % (2477897)Peak memory usage: 116 MB % 47.75/7.96 % (2477897)Instructions burned: 15 (million) % 47.75/7.96 % (2477893)Instruction limit reached! % 47.75/7.96 % (2477893)------------------------------ % 47.75/7.96 % (2477893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.75/7.96 % (2477893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.75/7.96 % (2477893)CaDiCaL version: 2.1.3 % 47.75/7.96 % (2477893)Termination reason: Instruction limit % 47.75/7.96 % (2477893)Termination phase: Saturation % 47.75/7.96 % (2477893)Time elapsed: 0.347 s % 47.75/7.96 % (2477893)Peak memory usage: 136 MB % 47.75/7.96 % (2477893)Instructions burned: 276 (million) % 47.75/7.96 % (2477895)Instruction limit reached! % 47.75/7.96 % (2477895)------------------------------ % 47.75/7.96 % (2477895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.75/7.96 % (2477895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.75/7.96 % (2477895)CaDiCaL version: 2.1.3 % 47.75/7.96 % (2477895)Termination reason: Instruction limit % 47.75/7.96 % (2477895)Termination phase: Saturation % 47.75/7.96 % (2477895)Time elapsed: 0.354 s % 47.75/7.96 % (2477895)Peak memory usage: 96 MB % 47.75/7.96 % (2477895)Instructions burned: 657 (million) % 47.75/7.96 % (2477904)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1288106354:s2a=on:i=450:doe=on:nm=32:rtra=on_2949 on theBenchmark for (2949ds/450Mi) % 47.75/7.96 % (2477906)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1278903332:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2948 on theBenchmark for (2948ds/130Mi) % 47.75/7.96 % (2477906)Instruction limit reached! % 47.75/7.96 % (2477906)------------------------------ % 47.75/7.96 % (2477906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.71/8.64 % (2477906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.71/8.64 % (2477906)CaDiCaL version: 2.1.3 % 53.71/8.64 % (2477906)Termination reason: Instruction limit % 53.71/8.64 % (2477906)Termination phase: Saturation % 53.71/8.64 % (2477906)Time elapsed: 0.082 s % 53.71/8.64 % (2477906)Peak memory usage: 119 MB % 53.71/8.64 % (2477906)Instructions burned: 132 (million) % 53.71/8.64 % (2477905)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 % 53.71/8.64 % (2477905)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1417966016:i=1090:aac=none:nm=0:rtra=on:rawr=on_2948 on theBenchmark for (2948ds/1090Mi) % 53.71/8.64 % (2477897)------------------------------ % 53.71/8.64 % (2477897)------------------------------ % 53.71/8.64 % (2477909)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=445757957:i=312:kws=inv_frequency:nm=20:rtra=on_2945 on theBenchmark for (2945ds/312Mi) % 53.71/8.64 % (2477911)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2798541768:i=491:doe=on:rtra=on:gtg=position_2945 on theBenchmark for (2945ds/491Mi) % 53.71/8.64 % (2477909)Instruction limit reached! % 53.71/8.64 % (2477909)------------------------------ % 53.71/8.64 % (2477909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.71/8.64 % (2477909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.71/8.64 % (2477909)CaDiCaL version: 2.1.3 % 53.71/8.64 % (2477909)Termination reason: Instruction limit % 53.71/8.64 % (2477909)Termination phase: Saturation % 53.71/8.64 % (2477909)Time elapsed: 0.171 s % 53.71/8.64 % (2477909)Peak memory usage: 120 MB % 53.71/8.64 % (2477909)Instructions burned: 313 (million) % 53.71/8.64 % (2477894)Instruction limit reached! % 53.71/8.64 % (2477894)------------------------------ % 53.71/8.64 % (2477894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.71/8.64 % (2477894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.71/8.64 % (2477894)CaDiCaL version: 2.1.3 % 53.71/8.64 % (2477894)Termination reason: Instruction limit % 53.71/8.64 % (2477894)Termination phase: Saturation % 53.71/8.64 % (2477894)Time elapsed: 1.018 s % 53.71/8.64 % (2477894)Peak memory usage: 94 MB % 53.71/8.64 % (2477894)Instructions burned: 1052 (million) % 53.71/8.64 % (2477904)Instruction limit reached! % 53.71/8.64 % (2477904)------------------------------ % 53.71/8.64 % (2477904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.71/8.64 % (2477904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.71/8.64 % (2477904)CaDiCaL version: 2.1.3 % 53.71/8.64 % (2477904)Termination reason: Instruction limit % 53.71/8.64 % (2477904)Termination phase: Saturation % 53.71/8.64 % (2477904)Time elapsed: 0.573 s % 53.71/8.64 % (2477904)Peak memory usage: 136 MB % 53.71/8.64 % (2477904)Instructions burned: 450 (million) % 53.71/8.64 % (2477896)Instruction limit reached! % 53.71/8.64 % (2477896)------------------------------ % 53.71/8.64 % (2477896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.71/8.64 % (2477896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.71/8.64 % (2477896)CaDiCaL version: 2.1.3 % 53.71/8.64 % (2477896)Termination reason: Instruction limit % 53.71/8.64 % (2477896)Termination phase: Saturation % 53.71/8.64 % (2477896)Time elapsed: 0.993 s % 53.71/8.64 % (2477896)Peak memory usage: 93 MB % 53.71/8.64 % (2477896)Instructions burned: 1054 (million) % 53.71/8.64 % (2477914)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3441187384:s2a=on:i=835:s2at=2:rtra=on_2941 on theBenchmark for (2941ds/835Mi) % 53.71/8.64 % (2477915)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2846143673:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2941 on theBenchmark for (2941ds/307Mi) % 53.71/8.64 % (2477916)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=401711650:i=776:doe=on:rtra=on_2940 on theBenchmark for (2940ds/776Mi) % 53.71/8.64 % (2477917)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=621935336:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi) % 53.71/8.64 % (2477911)Instruction limit reached! % 53.71/8.64 % (2477911)------------------------------ % 53.71/8.64 % (2477911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.18/10.23 % (2477911)CaDiCaL version: 2.1.3 % 66.18/10.23 % (2477911)Termination reason: Instruction limit % 66.18/10.23 % (2477911)Termination phase: Saturation % 66.18/10.23 % (2477911)Time elapsed: 0.533 s % 66.18/10.23 % (2477911)Peak memory usage: 95 MB % 66.18/10.23 % (2477911)Instructions burned: 491 (million) % 66.18/10.23 % (2477915)Instruction limit reached! % 66.18/10.23 % (2477915)------------------------------ % 66.18/10.23 % (2477915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.18/10.23 % (2477915)CaDiCaL version: 2.1.3 % 66.18/10.23 % (2477915)Termination reason: Instruction limit % 66.18/10.23 % (2477915)Termination phase: Saturation % 66.18/10.23 % (2477915)Time elapsed: 0.324 s % 66.18/10.23 % (2477915)Peak memory usage: 92 MB % 66.18/10.23 % (2477915)Instructions burned: 307 (million) % 66.18/10.23 % (2477914)Instruction limit reached! % 66.18/10.23 % (2477914)------------------------------ % 66.18/10.23 % (2477914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.18/10.23 % (2477914)CaDiCaL version: 2.1.3 % 66.18/10.23 % (2477914)Termination reason: Instruction limit % 66.18/10.23 % (2477914)Termination phase: Saturation % 66.18/10.23 % (2477914)Time elapsed: 0.441 s % 66.18/10.23 % (2477914)Peak memory usage: 95 MB % 66.18/10.23 % (2477914)Instructions burned: 836 (million) % 66.18/10.23 % (2477905)Instruction limit reached! % 66.18/10.23 % (2477905)------------------------------ % 66.18/10.23 % (2477905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.18/10.23 % (2477905)CaDiCaL version: 2.1.3 % 66.18/10.23 % (2477905)Termination reason: Instruction limit % 66.18/10.23 % (2477905)Termination phase: Saturation % 66.18/10.23 % (2477905)Time elapsed: 1.067 s % 66.18/10.23 % (2477905)Peak memory usage: 126 MB % 66.18/10.23 % (2477905)Instructions burned: 1090 (million) % 66.18/10.23 % (2477922)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=3123348701:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2936 on theBenchmark for (2936ds/784Mi) % 66.18/10.23 % (2477923)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=2791500584:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2935 on theBenchmark for (2935ds/1131Mi) % 66.18/10.23 % (2477924)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=1858450701:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2935 on theBenchmark for (2935ds/246Mi) % 66.18/10.23 % (2477925)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=917133149:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/775Mi) % 66.18/10.23 % (2477916)Instruction limit reached! % 66.18/10.23 % (2477916)------------------------------ % 66.18/10.23 % (2477916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.18/10.23 % (2477916)CaDiCaL version: 2.1.3 % 66.18/10.23 % (2477916)Termination reason: Instruction limit % 66.18/10.23 % (2477916)Termination phase: Saturation % 66.18/10.23 % (2477916)Time elapsed: 0.721 s % 66.18/10.23 % (2477916)Peak memory usage: 118 MB % 66.18/10.23 % (2477916)Instructions burned: 776 (million) % 66.18/10.23 % (2477917)Instruction limit reached! % 66.18/10.23 % (2477917)------------------------------ % 66.18/10.23 % (2477917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.18/10.23 % (2477917)CaDiCaL version: 2.1.3 % 66.18/10.23 % (2477917)Termination reason: Instruction limit % 66.18/10.23 % (2477917)Termination phase: Saturation % 66.18/10.23 % (2477917)Time elapsed: 0.701 s % 66.18/10.23 % (2477917)Peak memory usage: 139 MB % 66.18/10.23 % (2477917)Instructions burned: 646 (million) % 66.18/10.23 % (2477924)Instruction limit reached! % 66.18/10.23 % (2477924)------------------------------ % 66.18/10.23 % (2477924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.18/10.23 % (2477924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.85/13.42 % (2477924)CaDiCaL version: 2.1.3 % 88.85/13.42 % (2477924)Termination reason: Instruction limit % 88.85/13.42 % (2477924)Termination phase: Saturation % 88.85/13.42 % (2477924)Time elapsed: 0.291 s % 88.85/13.42 % (2477924)Peak memory usage: 119 MB % 88.85/13.42 % (2477924)Instructions burned: 246 (million) % 88.85/13.42 % (2477930)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=747119859:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2930 on theBenchmark for (2930ds/273Mi) % 88.85/13.42 % (2477931)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1566643872:i=102:nm=16:rtra=on_2930 on theBenchmark for (2930ds/102Mi) % 88.85/13.42 % (2477923)Instruction limit reached! % 88.85/13.42 % (2477923)------------------------------ % 88.85/13.42 % (2477923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.85/13.42 % (2477923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.85/13.42 % (2477923)CaDiCaL version: 2.1.3 % 88.85/13.42 % (2477923)Termination reason: Instruction limit % 88.85/13.42 % (2477923)Termination phase: Saturation % 88.85/13.42 % (2477923)Time elapsed: 0.591 s % 88.85/13.42 % (2477923)Peak memory usage: 121 MB % 88.85/13.42 % (2477923)Instructions burned: 1132 (million) % 88.85/13.42 % (2477932)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1416082989:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2929 on theBenchmark for (2929ds/1094Mi) % 88.85/13.42 % (2477931)Instruction limit reached! % 88.85/13.42 % (2477931)------------------------------ % 88.85/13.42 % (2477931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.85/13.42 % (2477931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.85/13.42 % (2477931)CaDiCaL version: 2.1.3 % 88.85/13.42 % (2477931)Termination reason: Instruction limit % 88.85/13.42 % (2477931)Termination phase: Saturation % 88.85/13.42 % (2477931)Time elapsed: 0.105 s % 88.85/13.42 % (2477931)Peak memory usage: 89 MB % 88.85/13.42 % (2477931)Instructions burned: 103 (million) % 88.85/13.42 % (2477930)Instruction limit reached! % 88.85/13.42 % (2477930)------------------------------ % 88.85/13.42 % (2477930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.85/13.42 % (2477930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.85/13.42 % (2477930)CaDiCaL version: 2.1.3 % 88.85/13.42 % (2477930)Termination reason: Instruction limit % 88.85/13.42 % (2477930)Termination phase: Saturation % 88.85/13.42 % (2477930)Time elapsed: 0.314 s % 88.85/13.42 % (2477930)Peak memory usage: 93 MB % 88.85/13.42 % (2477930)Instructions burned: 273 (million) % 88.85/13.42 % (2477935)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2792924186:i=6400:doe=on:fsr=off:rtra=on_2927 on theBenchmark for (2927ds/6400Mi) % 88.85/13.42 % (2477922)Instruction limit reached! % 88.85/13.42 % (2477922)------------------------------ % 88.85/13.42 % (2477922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.85/13.42 % (2477922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.85/13.42 % (2477922)CaDiCaL version: 2.1.3 % 88.85/13.42 % (2477922)Termination reason: Instruction limit % 88.85/13.42 % (2477922)Termination phase: Saturation % 88.85/13.42 % (2477922)Time elapsed: 0.908 s % 88.85/13.42 % (2477922)Peak memory usage: 122 MB % 88.85/13.42 % (2477922)Instructions burned: 784 (million) % 88.85/13.42 % (2477925)Instruction limit reached! % 88.85/13.42 % (2477925)------------------------------ % 88.85/13.42 % (2477925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.85/13.42 % (2477925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.85/13.42 % (2477925)CaDiCaL version: 2.1.3 % 88.85/13.42 % (2477925)Termination reason: Instruction limit % 88.85/13.42 % (2477925)Termination phase: Saturation % 88.85/13.42 % (2477925)Time elapsed: 0.783 s % 88.85/13.42 % (2477925)Peak memory usage: 97 MB % 88.85/13.42 % (2477925)Instructions burned: 776 (million) % 88.85/13.42 % (2477937)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=4075441066:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2926 on theBenchmark for (2926ds/868Mi) % 88.85/13.42 % (2477942)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2858802009:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2924 on theBenchmark for (2924ds/36816Mi) % 88.85/13.42 % (2477940)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=3661375019:i=1846:canc=cautious:fsr=off:rtra=on_2925 on theBenchmark for (2925ds/1846Mi) % 102.10/15.40 % (2477943)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1297243149:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2924 on theBenchmark for (2924ds/273Mi) % 102.10/15.40 % (2477943)Instruction limit reached! % 102.10/15.40 % (2477943)------------------------------ % 102.10/15.40 % (2477943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.40 % (2477943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.40 % (2477943)CaDiCaL version: 2.1.3 % 102.10/15.40 % (2477943)Termination reason: Instruction limit % 102.10/15.40 % (2477943)Termination phase: Saturation % 102.10/15.40 % (2477943)Time elapsed: 0.268 s % 102.10/15.40 % (2477943)Peak memory usage: 93 MB % 102.10/15.40 % (2477943)Instructions burned: 274 (million) % 102.10/15.40 % (2477953)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=3042374384:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2918 on theBenchmark for (2918ds/863Mi) % 102.10/15.40 % (2477932)Instruction limit reached! % 102.10/15.40 % (2477932)------------------------------ % 102.10/15.40 % (2477932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.40 % (2477932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.40 % (2477932)CaDiCaL version: 2.1.3 % 102.10/15.40 % (2477932)Termination reason: Instruction limit % 102.10/15.40 % (2477932)Termination phase: Saturation % 102.10/15.40 % (2477932)Time elapsed: 1.116 s % 102.10/15.40 % (2477932)Peak memory usage: 97 MB % 102.10/15.40 % (2477932)Instructions burned: 1094 (million) % 102.10/15.40 % (2477937)Instruction limit reached! % 102.10/15.40 % (2477937)------------------------------ % 102.10/15.40 % (2477937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.40 % (2477937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.40 % (2477937)CaDiCaL version: 2.1.3 % 102.10/15.40 % (2477937)Termination reason: Instruction limit % 102.10/15.40 % (2477937)Termination phase: Saturation % 102.10/15.40 % (2477937)Time elapsed: 0.888 s % 102.10/15.40 % (2477937)Peak memory usage: 121 MB % 102.10/15.40 % (2477937)Instructions burned: 868 (million) % 102.10/15.40 % (2477958)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2792221441:i=5811:kws=precedence:nm=0:rtra=on_2915 on theBenchmark for (2915ds/5811Mi) % 102.10/15.40 % (2477960)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=1025594433:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2914 on theBenchmark for (2914ds/2216Mi) % 102.10/15.40 % (2477892)Instruction limit reached! % 102.10/15.40 % (2477892)------------------------------ % 102.10/15.40 % (2477892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.40 % (2477892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.40 % (2477892)CaDiCaL version: 2.1.3 % 102.10/15.40 % (2477892)Termination reason: Instruction limit % 102.10/15.40 % (2477892)Termination phase: Saturation % 102.10/15.40 % (2477892)Time elapsed: 4.258 s % 102.10/15.40 % (2477892)Peak memory usage: 111 MB % 102.10/15.40 % (2477892)Instructions burned: 4428 (million) % 102.10/15.40 % (2477940)Instruction limit reached! % 102.10/15.40 % (2477940)------------------------------ % 102.10/15.40 % (2477940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.40 % (2477940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.40 % (2477940)CaDiCaL version: 2.1.3 % 102.10/15.40 % (2477940)Termination reason: Instruction limit % 102.10/15.40 % (2477940)Termination phase: Saturation % 102.10/15.40 % (2477940)Time elapsed: 1.565 s % 102.10/15.40 % (2477940)Peak memory usage: 96 MB % 102.10/15.40 % (2477940)Instructions burned: 1846 (million) % 102.10/15.40 % (2477953)Instruction limit reached! % 102.10/15.40 % (2477953)------------------------------ % 102.10/15.40 % (2477953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.40 % (2477953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.40 % (2477953)CaDiCaL version: 2.1.3 % 102.10/15.40 % (2477953)Termination reason: Instruction limit % 102.10/15.40 % (2477953)Termination phase: Saturation % 102.10/15.40 % (2477953)Time elapsed: 0.883 s % 145.94/21.41 % (2477953)Peak memory usage: 121 MB % 145.94/21.41 % (2477953)Instructions burned: 863 (million) % 145.94/21.41 % (2477966)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1399016937:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2909 on theBenchmark for (2909ds/801Mi) % 145.94/21.41 % (2477967)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2352277366:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2906 on theBenchmark for (2906ds/1026Mi) % 145.94/21.41 % (2477968)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=457881512:i=3509:rtra=on_2906 on theBenchmark for (2906ds/3509Mi) % 145.94/21.41 % (2477966)Instruction limit reached! % 145.94/21.41 % (2477966)------------------------------ % 145.94/21.41 % (2477966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.94/21.41 % (2477966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.94/21.41 % (2477966)CaDiCaL version: 2.1.3 % 145.94/21.41 % (2477966)Termination reason: Instruction limit % 145.94/21.41 % (2477966)Termination phase: Saturation % 145.94/21.41 % (2477966)Time elapsed: 0.840 s % 145.94/21.41 % (2477966)Peak memory usage: 97 MB % 145.94/21.41 % (2477966)Instructions burned: 801 (million) % 145.94/21.41 % (2477967)Instruction limit reached! % 145.94/21.41 % (2477967)------------------------------ % 145.94/21.41 % (2477967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.94/21.41 % (2477967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.94/21.41 % (2477967)CaDiCaL version: 2.1.3 % 145.94/21.41 % (2477967)Termination reason: Instruction limit % 145.94/21.41 % (2477967)Termination phase: Saturation % 145.94/21.41 % (2477967)Time elapsed: 0.937 s % 145.94/21.41 % (2477967)Peak memory usage: 93 MB % 145.94/21.41 % (2477967)Instructions burned: 1027 (million) % 145.94/21.41 % (2477974)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=683224102:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2897 on theBenchmark for (2897ds/2127Mi) % 145.94/21.41 % (2477935)Instruction limit reached! % 145.94/21.41 % (2477935)------------------------------ % 145.94/21.41 % (2477935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.94/21.41 % (2477935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.94/21.41 % (2477935)CaDiCaL version: 2.1.3 % 145.94/21.41 % (2477935)Termination reason: Instruction limit % 145.94/21.41 % (2477935)Termination phase: Saturation % 145.94/21.41 % (2477935)Time elapsed: 3.101 s % 145.94/21.41 % (2477935)Peak memory usage: 120 MB % 145.94/21.41 % (2477935)Instructions burned: 6401 (million) % 145.94/21.41 % (2477960)Instruction limit reached! % 145.94/21.41 % (2477960)------------------------------ % 145.94/21.41 % (2477960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.94/21.41 % (2477960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.94/21.41 % (2477960)CaDiCaL version: 2.1.3 % 145.94/21.41 % (2477960)Termination reason: Instruction limit % 145.94/21.41 % (2477960)Termination phase: Saturation % 145.94/21.41 % (2477960)Time elapsed: 1.950 s % 145.94/21.41 % (2477960)Peak memory usage: 122 MB % 145.94/21.41 % (2477960)Instructions burned: 2216 (million) % 145.94/21.41 % (2477977)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=510571668:i=1959:rtra=on:fsd=on:proc=on_2894 on theBenchmark for (2894ds/1959Mi) % 145.94/21.41 % (2477979)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3047862451:s2a=on:i=3553:nm=0:rtra=on_2893 on theBenchmark for (2893ds/3553Mi) % 145.94/21.41 % (2477980)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=575150175:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/3201Mi) % 145.94/21.41 % (2477974)Instruction limit reached! % 145.94/21.41 % (2477974)------------------------------ % 145.94/21.41 % (2477974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.94/21.41 % (2477974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.94/21.41 % (2477974)CaDiCaL version: 2.1.3 % 145.94/21.41 % (2477974)Termination reason: Instruction limit % 145.94/21.41 % (2477974)Termination phase: Saturation % 145.94/21.41 % (2477974)Time elapsed: 1.831 s % 145.94/21.41 % (2477974)Peak memory usage: 92 MB % 145.94/21.41 % (2477974)Instructions burned: 2127 (million) % 145.94/21.41 % (2477977)Instruction limit reached! % 145.94/21.41 % (2477977)------------------------------ % 145.94/21.41 % (2477977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.24/28.22 % (2477977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.24/28.22 % (2477977)CaDiCaL version: 2.1.3 % 194.24/28.22 % (2477977)Termination reason: Instruction limit % 194.24/28.22 % (2477977)Termination phase: Saturation % 194.24/28.22 % (2477977)Time elapsed: 1.709 s % 194.24/28.22 % (2477977)Peak memory usage: 120 MB % 194.24/28.22 % (2477977)Instructions burned: 1959 (million) % 194.24/28.22 % (2477979)Instruction limit reached! % 194.24/28.22 % (2477979)------------------------------ % 194.24/28.22 % (2477979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.24/28.22 % (2477979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.24/28.22 % (2477979)CaDiCaL version: 2.1.3 % 194.24/28.22 % (2477979)Termination reason: Instruction limit % 194.24/28.22 % (2477979)Termination phase: Saturation % 194.24/28.22 % (2477979)Time elapsed: 1.731 s % 194.24/28.22 % (2477979)Peak memory usage: 112 MB % 194.24/28.22 % (2477979)Instructions burned: 3553 (million) % 194.24/28.22 % (2477992)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=2037874393:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2876 on theBenchmark for (2876ds/4093Mi) % 194.24/28.22 % (2477968)Instruction limit reached! % 194.24/28.22 % (2477968)------------------------------ % 194.24/28.22 % (2477968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.24/28.22 % (2477968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.24/28.22 % (2477968)CaDiCaL version: 2.1.3 % 194.24/28.22 % (2477968)Termination reason: Instruction limit % 194.24/28.22 % (2477968)Termination phase: Saturation % 194.24/28.22 % (2477968)Time elapsed: 3.123 s % 194.24/28.22 % (2477968)Peak memory usage: 108 MB % 194.24/28.22 % (2477968)Instructions burned: 3509 (million) % 194.24/28.22 % (2477993)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=1568239961:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2874 on theBenchmark for (2874ds/21173Mi) % 194.24/28.22 % (2477994)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=527119389:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2874 on theBenchmark for (2874ds/10544Mi) % 194.24/28.22 % (2477996)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=923039328:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2872 on theBenchmark for (2872ds/1262Mi) % 194.24/28.22 % (2477980)Instruction limit reached! % 194.24/28.22 % (2477980)------------------------------ % 194.24/28.22 % (2477980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.24/28.22 % (2477980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.24/28.22 % (2477980)CaDiCaL version: 2.1.3 % 194.24/28.22 % (2477980)Termination reason: Instruction limit % 194.24/28.22 % (2477980)Termination phase: Saturation % 194.24/28.22 % (2477980)Time elapsed: 2.716 s % 194.24/28.22 % (2477980)Peak memory usage: 93 MB % 194.24/28.22 % (2477980)Instructions burned: 3202 (million) % 194.24/28.22 % (2478010)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1697816731:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2862 on theBenchmark for (2862ds/775Mi) % 194.24/28.22 % (2477996)Instruction limit reached! % 194.24/28.22 % (2477996)------------------------------ % 194.24/28.22 % (2477996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.24/28.22 % (2477996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.24/28.22 % (2477996)CaDiCaL version: 2.1.3 % 194.24/28.22 % (2477996)Termination reason: Instruction limit % 194.24/28.22 % (2477996)Termination phase: Saturation % 194.24/28.22 % (2477996)Time elapsed: 1.135 s % 194.24/28.22 % (2477996)Peak memory usage: 122 MB % 194.24/28.22 % (2477996)Instructions burned: 1262 (million) % 194.24/28.22 % (2477958)Instruction limit reached! % 194.24/28.22 % (2477958)------------------------------ % 194.24/28.22 % (2477958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.24/28.22 % (2477958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.24/28.22 % (2477958)CaDiCaL version: 2.1.3 % 194.24/28.22 % (2477958)Termination reason: Instruction limit % 194.24/28.22 % (2477958)Termination phase: Saturation % 194.24/28.22 % (2477958)Time elapsed: 5.491 s % 194.24/28.22 % (2477958)Peak memory usage: 140 MB % 194.24/28.22 % (2477958)Instructions burned: 5811 (million) % 194.24/28.22 % (2478012)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1615014141:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2858 on theBenchmark for (2858ds/270Mi) % 209.61/30.48 % (2478013)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3737160986:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2857 on theBenchmark for (2857ds/17165Mi) % 209.61/30.48 % (2478010)Instruction limit reached! % 209.61/30.48 % (2478010)------------------------------ % 209.61/30.48 % (2478010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.61/30.48 % (2478010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.61/30.48 % (2478010)CaDiCaL version: 2.1.3 % 209.61/30.48 % (2478010)Termination reason: Instruction limit % 209.61/30.48 % (2478010)Termination phase: Saturation % 209.61/30.48 % (2478010)Time elapsed: 0.798 s % 209.61/30.48 % (2478010)Peak memory usage: 95 MB % 209.61/30.48 % (2478010)Instructions burned: 777 (million) % 209.61/30.48 % (2478012)Instruction limit reached! % 209.61/30.48 % (2478012)------------------------------ % 209.61/30.48 % (2478012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.61/30.48 % (2478012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.61/30.48 % (2478012)CaDiCaL version: 2.1.3 % 209.61/30.48 % (2478012)Termination reason: Instruction limit % 209.61/30.48 % (2478012)Termination phase: Saturation % 209.61/30.48 % (2478012)Time elapsed: 0.323 s % 209.61/30.48 % (2478012)Peak memory usage: 93 MB % 209.61/30.48 % (2478012)Instructions burned: 270 (million) % 209.61/30.48 % (2478016)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1028169939:s2a=on:i=13094:s2at=-1:rtra=on_2851 on theBenchmark for (2851ds/13094Mi) % 209.61/30.48 % (2478017)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1847051351:st=2:i=12633:rtra=on:ss=axioms_2851 on theBenchmark for (2851ds/12633Mi) % 209.61/30.48 % (2477992)Instruction limit reached! % 209.61/30.48 % (2477992)------------------------------ % 209.61/30.48 % (2477992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.61/30.48 % (2477992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.61/30.48 % (2477992)CaDiCaL version: 2.1.3 % 209.61/30.48 % (2477992)Termination reason: Instruction limit % 209.61/30.48 % (2477992)Termination phase: Saturation % 209.61/30.48 % (2477992)Time elapsed: 3.803 s % 209.61/30.48 % (2477992)Peak memory usage: 142 MB % 209.61/30.48 % (2477992)Instructions burned: 4094 (million) % 209.61/30.48 % (2478022)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1329464134:i=1783:rtra=on:gtg=position_2835 on theBenchmark for (2835ds/1783Mi) % 209.61/30.48 % (2477994)Instruction limit reached! % 209.61/30.48 % (2477994)------------------------------ % 209.61/30.48 % (2477994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.61/30.48 % (2477994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.61/30.48 % (2477994)CaDiCaL version: 2.1.3 % 209.61/30.48 % (2477994)Termination reason: Instruction limit % 209.61/30.48 % (2477994)Termination phase: Saturation % 209.61/30.48 % (2477994)Time elapsed: 4.674 s % 209.61/30.48 % (2477994)Peak memory usage: 145 MB % 209.61/30.48 % (2477994)Instructions burned: 10546 (million) % 209.61/30.48 % (2478024)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=4082636526:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2825 on theBenchmark for (2825ds/5451Mi) % 209.61/30.48 % (2478022)Instruction limit reached! % 209.61/30.48 % (2478022)------------------------------ % 209.61/30.48 % (2478022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.61/30.48 % (2478022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.61/30.48 % (2478022)CaDiCaL version: 2.1.3 % 209.61/30.48 % (2478022)Termination reason: Instruction limit % 209.61/30.48 % (2478022)Termination phase: Saturation % 209.61/30.48 % (2478022)Time elapsed: 1.748 s % 209.61/30.48 % (2478022)Peak memory usage: 123 MB % 209.61/30.48 % (2478022)Instructions burned: 1783 (million) % 209.61/30.48 % (2478032)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=1593064015:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2814 on theBenchmark for (2814ds/4975Mi) % 209.61/30.48 % (2478024)Instruction limit reached! % 209.61/30.48 % (2478024)------------------------------ % 209.61/30.48 % (2478024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.88/35.97 % (2478024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.88/35.97 % (2478024)CaDiCaL version: 2.1.3 % 248.88/35.97 % (2478024)Termination reason: Instruction limit % 248.88/35.97 % (2478024)Termination phase: Saturation % 248.88/35.97 % (2478024)Time elapsed: 2.786 s % 248.88/35.97 % (2478024)Peak memory usage: 130 MB % 248.88/35.97 % (2478024)Instructions burned: 5453 (million) % 248.88/35.97 % (2478042)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=3094785755:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2794 on theBenchmark for (2794ds/2076Mi) % 248.88/35.97 % (2478042)Instruction limit reached! % 248.88/35.97 % (2478042)------------------------------ % 248.88/35.97 % (2478042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.88/35.97 % (2478042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.88/35.97 % (2478042)CaDiCaL version: 2.1.3 % 248.88/35.97 % (2478042)Termination reason: Instruction limit % 248.88/35.97 % (2478042)Termination phase: Saturation % 248.88/35.97 % (2478042)Time elapsed: 0.975 s % 248.88/35.97 % (2478042)Peak memory usage: 122 MB % 248.88/35.97 % (2478042)Instructions burned: 2078 (million) % 248.88/35.97 % (2478044)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=438406594:i=5145:rtra=on_2782 on theBenchmark for (2782ds/5145Mi) % 248.88/35.97 % (2478032)Instruction limit reached! % 248.88/35.97 % (2478032)------------------------------ % 248.88/35.97 % (2478032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.88/35.97 % (2478032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.88/35.97 % (2478032)CaDiCaL version: 2.1.3 % 248.88/35.97 % (2478032)Termination reason: Instruction limit % 248.88/35.97 % (2478032)Termination phase: Saturation % 248.88/35.97 % (2478032)Time elapsed: 4.505 s % 248.88/35.97 % (2478032)Peak memory usage: 126 MB % 248.88/35.97 % (2478032)Instructions burned: 4975 (million) % 248.88/35.97 % (2478048)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3741392607:i=3509:rtra=on_2766 on theBenchmark for (2766ds/3509Mi) % 248.88/35.97 % (2478044)Instruction limit reached! % 248.88/35.97 % (2478044)------------------------------ % 248.88/35.97 % (2478044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.88/35.97 % (2478044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.88/35.97 % (2478044)CaDiCaL version: 2.1.3 % 248.88/35.97 % (2478044)Termination reason: Instruction limit % 248.88/35.97 % (2478044)Termination phase: Saturation % 248.88/35.97 % (2478044)Time elapsed: 2.748 s % 248.88/35.97 % (2478044)Peak memory usage: 110 MB % 248.88/35.97 % (2478044)Instructions burned: 5147 (million) % 248.88/35.97 % (2478054)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=199914870:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2753 on theBenchmark for (2753ds/13800Mi) % 248.88/35.97 % (2478048)Instruction limit reached! % 248.88/35.97 % (2478048)------------------------------ % 248.88/35.97 % (2478048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.88/35.97 % (2478048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.88/35.97 % (2478048)CaDiCaL version: 2.1.3 % 248.88/35.97 % (2478048)Termination reason: Instruction limit % 248.88/35.97 % (2478048)Termination phase: Saturation % 248.88/35.97 % (2478048)Time elapsed: 3.104 s % 248.88/35.97 % (2478048)Peak memory usage: 106 MB % 248.88/35.97 % (2478048)Instructions burned: 3511 (million) % 248.88/35.97 % (2478060)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1585748276:i=1412:rtra=on:fsd=on:proc=on_2732 on theBenchmark for (2732ds/1412Mi) % 248.88/35.97 % (2478016)Instruction limit reached! % 248.88/35.97 % (2478016)------------------------------ % 248.88/35.97 % (2478016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.88/35.97 % (2478016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.88/35.97 % (2478016)CaDiCaL version: 2.1.3 % 248.88/35.97 % (2478016)Termination reason: Instruction limit % 248.88/35.97 % (2478016)Termination phase: Saturation % 248.88/35.97 % (2478016)Time elapsed: 12.083 s % 248.88/35.97 % (2478016)Peak memory usage: 166 MB % 248.88/35.97 % (2478016)Instructions burned: 13095 (million) % 248.88/35.97 % (2478133)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 300.49/43.17 % (2478133)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3715480669:i=11747:aac=none:nm=0:rtra=on:rawr=on_2728 on theBenchmark for (2728ds/11747Mi) % 300.49/43.17 % (2478013)Instruction limit reached! % 300.49/43.17 % (2478013)------------------------------ % 300.49/43.17 % (2478013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.49/43.17 % (2478013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/43.17 % (2478013)CaDiCaL version: 2.1.3 % 300.49/43.17 % (2478013)Termination reason: Instruction limit % 300.49/43.17 % (2478013)Termination phase: Saturation % 300.49/43.17 % (2478013)Time elapsed: 12.911 s % 300.49/43.17 % (2478013)Peak memory usage: 203 MB % 300.49/43.17 % (2478013)Instructions burned: 17167 (million) % 300.49/43.17 % (2478181)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=940463191:s2a=on:i=3553:nm=0:rtra=on_2725 on theBenchmark for (2725ds/3553Mi) % 300.49/43.17 % (2478060)Instruction limit reached! % 300.49/43.17 % (2478060)------------------------------ % 300.49/43.17 % (2478060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.49/43.17 % (2478060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/43.17 % (2478060)CaDiCaL version: 2.1.3 % 300.49/43.17 % (2478060)Termination reason: Instruction limit % 300.49/43.17 % (2478060)Termination phase: Saturation % 300.49/43.17 % (2478060)Time elapsed: 0.776 s % 300.49/43.17 % (2478060)Peak memory usage: 121 MB % 300.49/43.17 % (2478060)Instructions burned: 1413 (million) % 300.49/43.17 % (2478219)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2445594228:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2723 on theBenchmark for (2723ds/3201Mi) % 300.49/43.17 % (2478017)Instruction limit reached! % 300.49/43.17 % (2478017)------------------------------ % 300.49/43.17 % (2478017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.49/43.17 % (2478017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/43.17 % (2478017)CaDiCaL version: 2.1.3 % 300.49/43.17 % (2478017)Termination reason: Instruction limit % 300.49/43.17 % (2478017)Termination phase: Saturation % 300.49/43.17 % (2478017)Time elapsed: 12.897 s % 300.49/43.17 % (2478017)Peak memory usage: 151 MB % 300.49/43.17 % (2478017)Instructions burned: 12633 (million) % 300.49/43.17 % (2478221)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=270661905:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2719 on theBenchmark for (2719ds/4081Mi) % 300.49/43.17 % (2478054)Instruction limit reached! % 300.49/43.17 % (2478054)------------------------------ % 300.49/43.17 % (2478054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.49/43.17 % (2478054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/43.17 % (2478054)CaDiCaL version: 2.1.3 % 300.49/43.17 % (2478054)Termination reason: Instruction limit % 300.49/43.17 % (2478054)Termination phase: Saturation % 300.49/43.17 % (2478054)Time elapsed: 4.279 s % 300.49/43.17 % (2478054)Peak memory usage: 100 MB % 300.49/43.17 % (2478054)Instructions burned: 13802 (million) % 300.49/43.17 % (2478223)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=3590407555:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2707 on theBenchmark for (2707ds/20260Mi) % 300.49/43.17 % (2478219)Instruction limit reached! % 300.49/43.17 % (2478219)------------------------------ % 300.49/43.17 % (2478219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.49/43.17 % (2478219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/43.17 % (2478219)CaDiCaL version: 2.1.3 % 300.49/43.17 % (2478219)Termination reason: Instruction limit % 300.49/43.17 % (2478219)Termination phase: Saturation % 300.49/43.17 % (2478219)Time elapsed: 1.520 s % 300.49/43.17 % (2478219)Peak memory usage: 93 MB % 300.49/43.17 % (2478219)Instructions burned: 3201 (million) % 300.49/43.17 % (2478225)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1006868728:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2706 on theBenchmark for (2706ds/58627Mi) % 300.49/43.17 % (2478181)Instruction limit reached! % 300.49/43.17 % (2478181)------------------------------ % 300.49/43.17 % (2478181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14: % 300.49/43.18 Terminated %------------------------------------------------------------------------------