%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX134_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:57 PM UTC 2026 % Result : Timeout 291.57s 42.00s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX134_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.22 % Computer : n011.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 15:03:15 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.24/0.28 Running first-order theorem proving % 0.24/0.28 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.63/1.55 % (3449845)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.63/1.55 % (3449852)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2726131606:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 4.63/1.55 % (3449852)Instruction limit reached! % 4.63/1.55 % (3449852)------------------------------ % 4.63/1.55 % (3449852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.55 % (3449852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.55 % (3449852)CaDiCaL version: 2.1.3 % 4.63/1.55 % (3449852)Termination reason: Instruction limit % 4.63/1.55 % (3449852)Termination phase: Property scanning % 4.63/1.55 % (3449852)Time elapsed: 0.006 s % 4.63/1.55 % (3449852)Peak memory usage: 85 MB % 4.63/1.55 % (3449852)Instructions burned: 13 (million) % 4.63/1.55 % (3449857)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1802903986:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 4.63/1.55 % (3449858)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1151942256:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 4.63/1.55 % (3449856)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2565212711:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 4.63/1.55 % (3449854)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2020724960:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 4.63/1.55 % (3449855)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=58299048:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 4.63/1.55 % (3449853)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3776107880:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 4.63/1.55 % (3449856)Instruction limit reached! % 4.63/1.55 % (3449856)------------------------------ % 4.63/1.55 % (3449856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.55 % (3449856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.55 % (3449856)CaDiCaL version: 2.1.3 % 4.63/1.55 % (3449856)Termination reason: Instruction limit % 4.63/1.55 % (3449856)Termination phase: Property scanning % 4.63/1.55 % (3449856)Time elapsed: 0.003 s % 4.63/1.55 % (3449856)Peak memory usage: 84 MB % 4.63/1.55 % (3449856)Instructions burned: 5 (million) % 4.63/1.55 % (3449855)Instruction limit reached! % 4.63/1.55 % (3449855)------------------------------ % 4.63/1.55 % (3449855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.55 % (3449855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.55 % (3449855)CaDiCaL version: 2.1.3 % 4.63/1.55 % (3449855)Termination reason: Instruction limit % 4.63/1.55 % (3449855)Termination phase: Property scanning % 4.63/1.55 % (3449855)Time elapsed: 0.006 s % 4.63/1.55 % (3449855)Peak memory usage: 85 MB % 4.63/1.55 % (3449855)Instructions burned: 7 (million) % 4.63/1.55 % (3449858)Instruction limit reached! % 4.63/1.55 % (3449858)------------------------------ % 4.63/1.55 % (3449858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.55 % (3449858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.55 % (3449858)CaDiCaL version: 2.1.3 % 4.63/1.55 % (3449858)Termination reason: Instruction limit % 4.63/1.55 % (3449858)Termination phase: Property scanning % 4.63/1.55 % (3449858)Time elapsed: 0.026 s % 4.63/1.55 % (3449858)Peak memory usage: 85 MB % 4.63/1.55 % (3449858)Instructions burned: 33 (million) % 4.63/1.55 % (3449857)Instruction limit reached! % 4.63/1.55 % (3449857)------------------------------ % 4.63/1.55 % (3449857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.63/1.55 % (3449857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.63/1.55 % (3449857)CaDiCaL version: 2.1.3 % 4.63/1.55 % (3449857)Termination reason: Instruction limit % 4.63/1.55 % (3449857)Termination phase: Property scanning % 4.63/1.55 % (3449857)Time elapsed: 0.035 s % 4.63/1.55 % (3449857)Peak memory usage: 85 MB % 4.63/1.55 % (3449857)Instructions burned: 47 (million) % 4.63/1.55 % (3449860)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1404003794:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 4.63/1.55 % (3449860)Instruction limit reached! % 4.63/1.55 % (3449860)------------------------------ % 6.25/1.86 % (3449860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.86 % (3449860)CaDiCaL version: 2.1.3 % 6.25/1.86 % (3449860)Termination reason: Instruction limit % 6.25/1.86 % (3449860)Termination phase: Property scanning % 6.25/1.86 % (3449860)Time elapsed: 0.006 s % 6.25/1.86 % (3449860)Peak memory usage: 85 MB % 6.25/1.86 % (3449860)Instructions burned: 16 (million) % 6.25/1.86 % (3449854)Instruction limit reached! % 6.25/1.86 % (3449854)------------------------------ % 6.25/1.86 % (3449854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.86 % (3449854)CaDiCaL version: 2.1.3 % 6.25/1.86 % (3449854)Termination reason: Instruction limit % 6.25/1.86 % (3449854)Termination phase: Saturation % 6.25/1.86 % (3449854)Time elapsed: 0.180 s % 6.25/1.86 % (3449854)Peak memory usage: 111 MB % 6.25/1.86 % (3449854)Instructions burned: 201 (million) % 6.25/1.86 % (3449867)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=3696204554:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/29Mi) % 6.25/1.86 % (3449867)Instruction limit reached! % 6.25/1.86 % (3449867)------------------------------ % 6.25/1.86 % (3449867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.86 % (3449867)CaDiCaL version: 2.1.3 % 6.25/1.86 % (3449867)Termination reason: Instruction limit % 6.25/1.86 % (3449867)Termination phase: Property scanning % 6.25/1.86 % (3449867)Time elapsed: 0.022 s % 6.25/1.86 % (3449867)Peak memory usage: 85 MB % 6.25/1.86 % (3449867)Instructions burned: 29 (million) % 6.25/1.86 % (3449868)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3485983287:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 6.25/1.86 % (3449868)Instruction limit reached! % 6.25/1.86 % (3449868)------------------------------ % 6.25/1.86 % (3449868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.86 % (3449868)CaDiCaL version: 2.1.3 % 6.25/1.86 % (3449868)Termination reason: Instruction limit % 6.25/1.86 % (3449868)Termination phase: Property scanning % 6.25/1.86 % (3449868)Time elapsed: 0.013 s % 6.25/1.86 % (3449868)Peak memory usage: 85 MB % 6.25/1.86 % (3449868)Instructions burned: 17 (million) % 6.25/1.86 % (3449869)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1581718330:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi) % 6.25/1.86 % (3449853)Instruction limit reached! % 6.25/1.86 % (3449853)------------------------------ % 6.25/1.86 % (3449853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.86 % (3449853)CaDiCaL version: 2.1.3 % 6.25/1.86 % (3449853)Termination reason: Instruction limit % 6.25/1.86 % (3449853)Termination phase: Saturation % 6.25/1.86 % (3449853)Time elapsed: 0.261 s % 6.25/1.86 % (3449853)Peak memory usage: 112 MB % 6.25/1.86 % (3449853)Instructions burned: 308 (million) % 6.25/1.86 % (3449869)Instruction limit reached! % 6.25/1.86 % (3449869)------------------------------ % 6.25/1.86 % (3449869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.25/1.86 % (3449869)CaDiCaL version: 2.1.3 % 6.25/1.86 % (3449869)Termination reason: Instruction limit % 6.25/1.86 % (3449869)Termination phase: Property scanning % 6.25/1.86 % (3449869)Time elapsed: 0.009 s % 6.25/1.86 % (3449869)Peak memory usage: 85 MB % 6.25/1.86 % (3449869)Instructions burned: 24 (million) % 6.25/1.86 % (3449870)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=231879655:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.25/1.86 % (3449870)Instruction limit reached! % 6.25/1.86 % (3449870)------------------------------ % 6.25/1.86 % (3449870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.25/1.86 % (3449870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.05 % (3449870)CaDiCaL version: 2.1.3 % 7.42/2.05 % (3449870)Termination reason: Instruction limit % 7.42/2.05 % (3449870)Termination phase: Property scanning % 7.42/2.05 % (3449870)Time elapsed: 0.021 s % 7.42/2.05 % (3449870)Peak memory usage: 85 MB % 7.42/2.05 % (3449870)Instructions burned: 27 (million) % 7.42/2.05 % (3449872)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2098860393:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi) % 7.42/2.05 % (3449872)Instruction limit reached! % 7.42/2.05 % (3449872)------------------------------ % 7.42/2.05 % (3449872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.05 % (3449872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.05 % (3449872)CaDiCaL version: 2.1.3 % 7.42/2.05 % (3449872)Termination reason: Instruction limit % 7.42/2.05 % (3449872)Termination phase: Property scanning % 7.42/2.05 % (3449872)Time elapsed: 0.065 s % 7.42/2.05 % (3449872)Peak memory usage: 85 MB % 7.42/2.05 % (3449872)Instructions burned: 85 (million) % 7.42/2.05 % (3449873)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1975967441:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 7.42/2.05 % (3449873)Instruction limit reached! % 7.42/2.05 % (3449873)------------------------------ % 7.42/2.05 % (3449873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.05 % (3449873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.05 % (3449873)CaDiCaL version: 2.1.3 % 7.42/2.05 % (3449873)Termination reason: Instruction limit % 7.42/2.05 % (3449873)Termination phase: shuffling % 7.42/2.05 % (3449873)Time elapsed: 0.003 s % 7.42/2.05 % (3449873)Peak memory usage: 85 MB % 7.42/2.05 % (3449873)Instructions burned: 4 (million) % 7.42/2.05 % (3449879)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=811605065:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 7.42/2.05 % (3449877)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3957106412:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi) % 7.42/2.05 % (3449876)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1392979090:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi) % 7.42/2.05 % (3449880)lrs+10_1_thi=all:si=on:fd=off:random_seed=1790531560:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 7.42/2.05 % (3449877)Instruction limit reached! % 7.42/2.05 % (3449877)------------------------------ % 7.42/2.05 % (3449877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.05 % (3449877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.05 % (3449877)CaDiCaL version: 2.1.3 % 7.42/2.05 % (3449877)Termination reason: Instruction limit % 7.42/2.05 % (3449877)Termination phase: Property scanning % 7.42/2.05 % (3449877)Time elapsed: 0.003 s % 7.42/2.05 % (3449877)Peak memory usage: 85 MB % 7.42/2.05 % (3449877)Instructions burned: 5 (million) % 7.42/2.05 % (3449879)Instruction limit reached! % 7.42/2.05 % (3449879)------------------------------ % 7.42/2.05 % (3449879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.05 % (3449879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.05 % (3449879)CaDiCaL version: 2.1.3 % 7.42/2.05 % (3449879)Termination reason: Instruction limit % 7.42/2.05 % (3449879)Termination phase: Property scanning % 7.42/2.05 % (3449879)Time elapsed: 0.027 s % 7.42/2.05 % (3449879)Peak memory usage: 86 MB % 7.42/2.05 % (3449879)Instructions burned: 68 (million) % 7.42/2.05 % (3449876)Refutation not found, incomplete strategy % 7.42/2.05 % (3449876)------------------------------ % 7.42/2.05 % (3449876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.42/2.05 % (3449876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.42/2.05 % (3449876)CaDiCaL version: 2.1.3 % 7.42/2.05 % (3449876)Termination reason: Refutation not found, incomplete strategy % 7.42/2.05 % (3449876)Time elapsed: 0.030 s % 7.42/2.05 % (3449876)Peak memory usage: 87 MB % 7.42/2.05 % (3449876)Instructions burned: 41 (million) % 7.42/2.05 % (3449880)Instruction limit reached! % 7.42/2.05 % (3449880)------------------------------ % 7.42/2.05 % (3449880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.33 % (3449880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.33 % (3449880)CaDiCaL version: 2.1.3 % 10.44/2.33 % (3449880)Termination reason: Instruction limit % 10.44/2.33 % (3449880)Termination phase: Property scanning % 10.44/2.33 % (3449880)Time elapsed: 0.040 s % 10.44/2.33 % (3449880)Peak memory usage: 84 MB % 10.44/2.33 % (3449880)Instructions burned: 53 (million) % 10.44/2.33 % (3449882)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=521326093:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi) % 10.44/2.33 % (3449882)Instruction limit reached! % 10.44/2.33 % (3449882)------------------------------ % 10.44/2.33 % (3449882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.33 % (3449882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.33 % (3449882)CaDiCaL version: 2.1.3 % 10.44/2.33 % (3449882)Termination reason: Instruction limit % 10.44/2.33 % (3449882)Termination phase: Property scanning % 10.44/2.33 % (3449882)Time elapsed: 0.008 s % 10.44/2.33 % (3449882)Peak memory usage: 85 MB % 10.44/2.33 % (3449882)Instructions burned: 9 (million) % 10.44/2.33 % (3449884)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1640201356:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 10.44/2.33 % (3449884)Instruction limit reached! % 10.44/2.33 % (3449884)------------------------------ % 10.44/2.33 % (3449884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.33 % (3449884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.33 % (3449884)CaDiCaL version: 2.1.3 % 10.44/2.33 % (3449884)Termination reason: Instruction limit % 10.44/2.33 % (3449884)Termination phase: shuffling % 10.44/2.33 % (3449884)Time elapsed: 0.002 s % 10.44/2.33 % (3449884)Peak memory usage: 85 MB % 10.44/2.33 % (3449884)Instructions burned: 3 (million) % 10.44/2.33 % (3449892)dis+10_1_si=on:random_seed=1785715862:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 10.44/2.33 % (3449892)Instruction limit reached! % 10.44/2.33 % (3449892)------------------------------ % 10.44/2.33 % (3449892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.33 % (3449892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.33 % (3449892)CaDiCaL version: 2.1.3 % 10.44/2.33 % (3449892)Termination reason: Instruction limit % 10.44/2.33 % (3449892)Termination phase: Property scanning % 10.44/2.33 % (3449892)Time elapsed: 0.005 s % 10.44/2.33 % (3449892)Peak memory usage: 85 MB % 10.44/2.33 % (3449892)Instructions burned: 12 (million) % 10.44/2.33 % (3449887)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1733946779:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 10.44/2.33 % (3449887)Instruction limit reached! % 10.44/2.33 % (3449887)------------------------------ % 10.44/2.33 % (3449887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.33 % (3449887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.33 % (3449887)CaDiCaL version: 2.1.3 % 10.44/2.33 % (3449887)Termination reason: Instruction limit % 10.44/2.33 % (3449887)Termination phase: shuffling % 10.44/2.33 % (3449887)Time elapsed: 0.002 s % 10.44/2.33 % (3449887)Peak memory usage: 85 MB % 10.44/2.33 % (3449887)Instructions burned: 3 (million) % 10.44/2.33 % (3449893)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2859335514:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 10.44/2.33 % (3449893)Instruction limit reached! % 10.44/2.33 % (3449893)------------------------------ % 10.44/2.33 % (3449893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.44/2.33 % (3449893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/2.33 % (3449893)CaDiCaL version: 2.1.3 % 10.44/2.33 % (3449893)Termination reason: Instruction limit % 10.44/2.33 % (3449893)Termination phase: Property scanning % 10.44/2.33 % (3449893)Time elapsed: 0.012 s % 10.44/2.33 % (3449893)Peak memory usage: 85 MB % 10.44/2.33 % (3449893)Instructions burned: 28 (million) % 10.44/2.33 % (3449891)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2593203739:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi) % 10.44/2.33 % (3449895)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2125914134: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) % 11.80/2.67 % (3449891)Instruction limit reached! % 11.80/2.67 % (3449891)------------------------------ % 11.80/2.67 % (3449891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.80/2.67 % (3449891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.80/2.67 % (3449891)CaDiCaL version: 2.1.3 % 11.80/2.67 % (3449891)Termination reason: Instruction limit % 11.80/2.67 % (3449891)Termination phase: Saturation % 11.80/2.67 % (3449891)Time elapsed: 0.126 s % 11.80/2.67 % (3449891)Peak memory usage: 112 MB % 11.80/2.67 % (3449891)Instructions burned: 127 (million) % 11.80/2.67 % (3449900)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2082932237:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 11.80/2.67 % (3449900)Instruction limit reached! % 11.80/2.67 % (3449900)------------------------------ % 11.80/2.67 % (3449900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.80/2.67 % (3449900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.80/2.67 % (3449900)CaDiCaL version: 2.1.3 % 11.80/2.67 % (3449900)Termination reason: Instruction limit % 11.80/2.67 % (3449900)Termination phase: Property scanning % 11.80/2.67 % (3449900)Time elapsed: 0.003 s % 11.80/2.67 % (3449900)Peak memory usage: 85 MB % 11.80/2.67 % (3449900)Instructions burned: 8 (million) % 11.80/2.67 % (3449897)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3429758558:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi) % 11.80/2.67 % (3449897)Instruction limit reached! % 11.80/2.67 % (3449897)------------------------------ % 11.80/2.67 % (3449897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.80/2.67 % (3449897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.80/2.67 % (3449897)CaDiCaL version: 2.1.3 % 11.80/2.67 % (3449897)Termination reason: Instruction limit % 11.80/2.67 % (3449897)Termination phase: shuffling % 11.80/2.67 % (3449897)Time elapsed: 0.002 s % 11.80/2.67 % (3449897)Peak memory usage: 85 MB % 11.80/2.67 % (3449897)Instructions burned: 3 (million) % 11.80/2.67 % (3449895)Instruction limit reached! % 11.80/2.67 % (3449895)------------------------------ % 11.80/2.67 % (3449895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.80/2.67 % (3449895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.80/2.67 % (3449895)CaDiCaL version: 2.1.3 % 11.80/2.67 % (3449895)Termination reason: Instruction limit % 11.80/2.67 % (3449895)Termination phase: Property scanning % 11.80/2.67 % (3449895)Time elapsed: 0.028 s % 11.80/2.67 % (3449895)Peak memory usage: 85 MB % 11.80/2.67 % (3449895)Instructions burned: 36 (million) % 11.80/2.67 % (3449903)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1369248293:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 11.80/2.67 % (3449903)Instruction limit reached! % 11.80/2.67 % (3449903)------------------------------ % 11.80/2.67 % (3449903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.80/2.67 % (3449903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.80/2.67 % (3449903)CaDiCaL version: 2.1.3 % 11.80/2.67 % (3449903)Termination reason: Instruction limit % 11.80/2.67 % (3449903)Termination phase: Property scanning % 11.80/2.67 % (3449903)Time elapsed: 0.006 s % 11.80/2.67 % (3449903)Peak memory usage: 85 MB % 11.80/2.67 % (3449903)Instructions burned: 14 (million) % 11.80/2.67 % (3449876)------------------------------ % 11.80/2.67 % (3449876)------------------------------ % 11.80/2.67 % (3449902)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1542770779:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 11.80/2.67 % (3449909)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2864353480:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 11.80/2.67 % (3449909)Instruction limit reached! % 11.80/2.67 % (3449909)------------------------------ % 11.80/2.67 % (3449909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.80/2.67 % (3449909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.80/2.67 % (3449909)CaDiCaL version: 2.1.3 % 11.80/2.67 % (3449909)Termination reason: Instruction limit % 11.80/2.67 % (3449909)Termination phase: Property scanning % 11.80/2.67 % (3449909)Time elapsed: 0.007 s % 16.93/3.22 % (3449909)Peak memory usage: 85 MB % 16.93/3.22 % (3449909)Instructions burned: 17 (million) % 16.93/3.22 % (3449902)Refutation not found, incomplete strategy % 16.93/3.22 % (3449902)------------------------------ % 16.93/3.22 % (3449902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.93/3.22 % (3449902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.93/3.22 % (3449902)CaDiCaL version: 2.1.3 % 16.93/3.22 % (3449902)Termination reason: Refutation not found, incomplete strategy % 16.93/3.22 % (3449902)Time elapsed: 0.121 s % 16.93/3.22 % (3449902)Peak memory usage: 89 MB % 16.93/3.22 % (3449902)Instructions burned: 161 (million) % 16.93/3.22 % (3449908)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1825626716:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 16.93/3.22 % (3449910)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2233334318:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi) % 16.93/3.22 % (3449912)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=1710827594:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi) % 16.93/3.22 % (3449913)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=3066747145:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 16.93/3.22 % (3449910)Instruction limit reached! % 16.93/3.22 % (3449910)------------------------------ % 16.93/3.22 % (3449910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.93/3.22 % (3449910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.93/3.22 % (3449910)CaDiCaL version: 2.1.3 % 16.93/3.22 % (3449910)Termination reason: Instruction limit % 16.93/3.22 % (3449910)Termination phase: Property scanning % 16.93/3.22 % (3449910)Time elapsed: 0.029 s % 16.93/3.22 % (3449910)Peak memory usage: 85 MB % 16.93/3.22 % (3449910)Instructions burned: 71 (million) % 16.93/3.22 % (3449914)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3571309383:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi) % 16.93/3.22 % (3449912)Instruction limit reached! % 16.93/3.22 % (3449912)------------------------------ % 16.93/3.22 % (3449912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.93/3.22 % (3449912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.93/3.22 % (3449912)CaDiCaL version: 2.1.3 % 16.93/3.22 % (3449912)Termination reason: Instruction limit % 16.93/3.22 % (3449912)Termination phase: Property scanning % 16.93/3.22 % (3449912)Time elapsed: 0.057 s % 16.93/3.22 % (3449912)Peak memory usage: 86 MB % 16.93/3.22 % (3449912)Instructions burned: 75 (million) % 16.93/3.22 % (3449908)Refutation not found, incomplete strategy % 16.93/3.22 % (3449908)------------------------------ % 16.93/3.22 % (3449908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.93/3.22 % (3449908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.93/3.22 % (3449908)CaDiCaL version: 2.1.3 % 16.93/3.22 % (3449908)Termination reason: Refutation not found, incomplete strategy % 16.93/3.22 % (3449908)Time elapsed: 0.087 s % 16.93/3.22 % (3449908)Peak memory usage: 111 MB % 16.93/3.22 % (3449908)Instructions burned: 73 (million) % 16.93/3.22 % (3449914)Instruction limit reached! % 16.93/3.22 % (3449914)------------------------------ % 16.93/3.22 % (3449914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.93/3.22 % (3449914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.93/3.22 % (3449914)CaDiCaL version: 2.1.3 % 16.93/3.22 % (3449914)Termination reason: Instruction limit % 16.93/3.22 % (3449914)Termination phase: Twee Goal Transformation % 16.93/3.22 % (3449914)Time elapsed: 0.100 s % 16.93/3.22 % (3449914)Peak memory usage: 87 MB % 16.93/3.22 % (3449914)Instructions burned: 130 (million) % 16.93/3.22 % (3449917)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2147514458:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 16.93/3.22 % (3449917)Instruction limit reached! % 16.93/3.22 % (3449917)------------------------------ % 16.93/3.22 % (3449917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.93/3.22 % (3449917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.70/3.53 % (3449917)CaDiCaL version: 2.1.3 % 17.70/3.53 % (3449917)Termination reason: Instruction limit % 17.70/3.53 % (3449917)Termination phase: Saturation % 17.70/3.53 % (3449917)Time elapsed: 0.083 s % 17.70/3.53 % (3449917)Peak memory usage: 128 MB % 17.70/3.53 % (3449917)Instructions burned: 131 (million) % 17.70/3.53 % (3449913)Instruction limit reached! % 17.70/3.53 % (3449913)------------------------------ % 17.70/3.53 % (3449913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.70/3.53 % (3449913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.70/3.53 % (3449913)CaDiCaL version: 2.1.3 % 17.70/3.53 % (3449913)Termination reason: Instruction limit % 17.70/3.53 % (3449913)Termination phase: Saturation % 17.70/3.53 % (3449913)Time elapsed: 0.218 s % 17.70/3.53 % (3449913)Peak memory usage: 90 MB % 17.70/3.53 % (3449913)Instructions burned: 297 (million) % 17.70/3.53 % (3449922)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3442196215:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi) % 17.70/3.53 % (3449922)Instruction limit reached! % 17.70/3.53 % (3449922)------------------------------ % 17.70/3.53 % (3449922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.70/3.53 % (3449922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.70/3.53 % (3449922)CaDiCaL version: 2.1.3 % 17.70/3.53 % (3449922)Termination reason: Instruction limit % 17.70/3.53 % (3449922)Termination phase: Property scanning % 17.70/3.53 % (3449922)Time elapsed: 0.017 s % 17.70/3.53 % (3449922)Peak memory usage: 85 MB % 17.70/3.53 % (3449922)Instructions burned: 42 (million) % 17.70/3.53 % (3449924)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2275487193:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi) % 17.70/3.53 % (3449902)------------------------------ % 17.70/3.53 % (3449902)------------------------------ % 17.70/3.53 % (3449926)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=590349715:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi) % 17.70/3.53 % (3449927)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3268440893:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi) % 17.70/3.53 % (3449908)------------------------------ % 17.70/3.53 % (3449908)------------------------------ % 17.70/3.53 % (3449928)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=1492425498:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi) % 17.70/3.53 % (3449924)Refutation not found, incomplete strategy % 17.70/3.53 % (3449924)------------------------------ % 17.70/3.53 % (3449924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.70/3.53 % (3449924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.70/3.53 % (3449924)CaDiCaL version: 2.1.3 % 17.70/3.53 % (3449924)Termination reason: Refutation not found, incomplete strategy % 17.70/3.53 % (3449924)Time elapsed: 0.170 s % 17.70/3.53 % (3449924)Peak memory usage: 89 MB % 17.70/3.53 % (3449924)Instructions burned: 226 (million) % 17.70/3.53 % (3449927)Instruction limit reached! % 17.70/3.53 % (3449927)------------------------------ % 17.70/3.53 % (3449927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.70/3.53 % (3449927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.70/3.53 % (3449927)CaDiCaL version: 2.1.3 % 17.70/3.53 % (3449927)Termination reason: Instruction limit % 17.70/3.53 % (3449927)Termination phase: Saturation % 17.70/3.53 % (3449927)Time elapsed: 0.069 s % 17.70/3.53 % (3449927)Peak memory usage: 111 MB % 17.70/3.53 % (3449927)Instructions burned: 132 (million) % 17.70/3.53 % (3449930)dis+10_1_si=on:random_seed=3656175075:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi) % 17.70/3.53 % (3449928)Refutation not found, incomplete strategy % 17.70/3.53 % (3449928)------------------------------ % 17.70/3.53 % (3449928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.70/3.53 % (3449928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.70/3.53 % (3449928)CaDiCaL version: 2.1.3 % 17.70/3.53 % (3449928)Termination reason: Refutation not found, incomplete strategy % 17.70/3.53 % (3449928)Time elapsed: 0.090 s % 17.70/3.53 % (3449928)Peak memory usage: 111 MB % 17.70/3.53 % (3449928)Instructions burned: 76 (million) % 19.43/3.82 % (3449933)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=202544663:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi) % 19.43/3.82 % (3449937)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=188684963:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi) % 19.43/3.82 % (3449937)Instruction limit reached! % 19.43/3.82 % (3449937)------------------------------ % 19.43/3.82 % (3449937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.82 % (3449937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.82 % (3449937)CaDiCaL version: 2.1.3 % 19.43/3.82 % (3449937)Termination reason: Instruction limit % 19.43/3.82 % (3449937)Termination phase: Saturation % 19.43/3.82 % (3449937)Time elapsed: 0.027 s % 19.43/3.82 % (3449937)Peak memory usage: 88 MB % 19.43/3.82 % (3449937)Instructions burned: 66 (million) % 19.43/3.82 % (3449936)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1422747473:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 19.43/3.82 % (3449936)Instruction limit reached! % 19.43/3.82 % (3449936)------------------------------ % 19.43/3.82 % (3449936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.82 % (3449936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.82 % (3449936)CaDiCaL version: 2.1.3 % 19.43/3.82 % (3449936)Termination reason: Instruction limit % 19.43/3.82 % (3449936)Termination phase: Saturation % 19.43/3.82 % (3449936)Time elapsed: 0.106 s % 19.43/3.82 % (3449936)Peak memory usage: 88 MB % 19.43/3.82 % (3449936)Instructions burned: 141 (million) % 19.43/3.82 % (3449933)Instruction limit reached! % 19.43/3.82 % (3449933)------------------------------ % 19.43/3.82 % (3449933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.82 % (3449933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.82 % (3449933)CaDiCaL version: 2.1.3 % 19.43/3.82 % (3449933)Termination reason: Instruction limit % 19.43/3.82 % (3449933)Termination phase: Saturation % 19.43/3.82 % (3449933)Time elapsed: 0.269 s % 19.43/3.82 % (3449933)Peak memory usage: 90 MB % 19.43/3.82 % (3449933)Instructions burned: 383 (million) % 19.43/3.82 % (3449924)------------------------------ % 19.43/3.82 % (3449924)------------------------------ % 19.43/3.82 % (3449926)Instruction limit reached! % 19.43/3.82 % (3449926)------------------------------ % 19.43/3.82 % (3449926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.82 % (3449926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.82 % (3449926)CaDiCaL version: 2.1.3 % 19.43/3.82 % (3449926)Termination reason: Instruction limit % 19.43/3.82 % (3449926)Termination phase: Saturation % 19.43/3.82 % (3449926)Time elapsed: 0.518 s % 19.43/3.82 % (3449926)Peak memory usage: 136 MB % 19.43/3.82 % (3449926)Instructions burned: 598 (million) % 19.43/3.82 % (3449941)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=674669145:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 19.43/3.82 % (3449928)------------------------------ % 19.43/3.82 % (3449928)------------------------------ % 19.43/3.82 % (3449941)Instruction limit reached! % 19.43/3.82 % (3449941)------------------------------ % 19.43/3.82 % (3449941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.82 % (3449941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.82 % (3449941)CaDiCaL version: 2.1.3 % 19.43/3.82 % (3449941)Termination reason: Instruction limit % 19.43/3.82 % (3449941)Termination phase: Saturation % 19.43/3.82 % (3449941)Time elapsed: 0.049 s % 19.43/3.82 % (3449941)Peak memory usage: 88 MB % 19.43/3.82 % (3449941)Instructions burned: 124 (million) % 19.43/3.82 % (3449943)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=3249474701:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi) % 19.43/3.82 % (3449944)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=2204677567:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 19.43/3.82 % (3449944)Instruction limit reached! % 19.43/3.82 % (3449944)------------------------------ % 19.43/3.82 % (3449944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.82 % (3449944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.40 % (3449944)CaDiCaL version: 2.1.3 % 25.43/4.40 % (3449944)Termination reason: Instruction limit % 25.43/4.40 % (3449944)Termination phase: Property scanning % 25.43/4.40 % (3449944)Time elapsed: 0.030 s % 25.43/4.40 % (3449944)Peak memory usage: 85 MB % 25.43/4.40 % (3449944)Instructions burned: 39 (million) % 25.43/4.40 % (3449945)dis+1010_1_to=kbo:si=on:random_seed=1587253972:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi) % 25.43/4.40 % (3449946)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2588059270:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/329Mi) % 25.43/4.40 % (3449949)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1369271350:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi) % 25.43/4.40 % (3449943)Instruction limit reached! % 25.43/4.40 % (3449943)------------------------------ % 25.43/4.40 % (3449943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.40 % (3449943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.40 % (3449943)CaDiCaL version: 2.1.3 % 25.43/4.40 % (3449943)Termination reason: Instruction limit % 25.43/4.40 % (3449943)Termination phase: Saturation % 25.43/4.40 % (3449943)Time elapsed: 0.098 s % 25.43/4.40 % (3449943)Peak memory usage: 88 MB % 25.43/4.40 % (3449943)Instructions burned: 128 (million) % 25.43/4.40 % (3449948)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=602781667:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 25.43/4.40 % (3449930)Instruction limit reached! % 25.43/4.40 % (3449930)------------------------------ % 25.43/4.40 % (3449930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.40 % (3449930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.40 % (3449930)CaDiCaL version: 2.1.3 % 25.43/4.40 % (3449930)Termination reason: Instruction limit % 25.43/4.40 % (3449930)Termination phase: Saturation % 25.43/4.40 % (3449930)Time elapsed: 0.692 s % 25.43/4.40 % (3449930)Peak memory usage: 90 MB % 25.43/4.40 % (3449930)Instructions burned: 1000 (million) % 25.43/4.40 % (3449945)Instruction limit reached! % 25.43/4.40 % (3449945)------------------------------ % 25.43/4.40 % (3449945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.40 % (3449945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.40 % (3449945)CaDiCaL version: 2.1.3 % 25.43/4.40 % (3449945)Termination reason: Instruction limit % 25.43/4.40 % (3449945)Termination phase: Property scanning % 25.43/4.40 % (3449945)Time elapsed: 0.133 s % 25.43/4.40 % (3449945)Peak memory usage: 86 MB % 25.43/4.40 % (3449945)Instructions burned: 175 (million) % 25.43/4.40 % (3449949)Instruction limit reached! % 25.43/4.40 % (3449949)------------------------------ % 25.43/4.40 % (3449949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.40 % (3449949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.40 % (3449949)CaDiCaL version: 2.1.3 % 25.43/4.40 % (3449949)Termination reason: Instruction limit % 25.43/4.40 % (3449949)Termination phase: Saturation % 25.43/4.40 % (3449949)Time elapsed: 0.118 s % 25.43/4.40 % (3449949)Peak memory usage: 129 MB % 25.43/4.40 % (3449949)Instructions burned: 216 (million) % 25.43/4.40 % (3449953)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4206070757:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi) % 25.43/4.40 % (3449946)Instruction limit reached! % 25.43/4.40 % (3449946)------------------------------ % 25.43/4.40 % (3449946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.43/4.40 % (3449946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.43/4.40 % (3449946)CaDiCaL version: 2.1.3 % 25.43/4.40 % (3449946)Termination reason: Instruction limit % 25.43/4.40 % (3449946)Termination phase: Saturation % 25.43/4.40 % (3449946)Time elapsed: 0.281 s % 25.43/4.40 % (3449946)Peak memory usage: 117 MB % 25.43/4.40 % (3449946)Instructions burned: 330 (million) % 25.43/4.40 % (3449958)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=279183189:i=328:kws=inv_frequency:nm=20:rtra=on_2974 on theBenchmark for (2974ds/328Mi) % 25.43/4.40 % (3449956)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=549603210:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi) % 26.15/4.76 % (3449960)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=837581127:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi) % 26.15/4.76 % (3449959)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=9006856:i=281:gtgl=2:rtra=on:gtg=all_2973 on theBenchmark for (2973ds/281Mi) % 26.15/4.76 % (3449956)Refutation not found, incomplete strategy % 26.15/4.76 % (3449956)------------------------------ % 26.15/4.76 % (3449956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449956)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449956)Termination reason: Refutation not found, incomplete strategy % 26.15/4.76 % (3449956)Time elapsed: 0.053 s % 26.15/4.76 % (3449956)Peak memory usage: 87 MB % 26.15/4.76 % (3449956)Instructions burned: 70 (million) % 26.15/4.76 % (3449960)Refutation not found, incomplete strategy % 26.15/4.76 % (3449960)------------------------------ % 26.15/4.76 % (3449960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449960)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449960)Termination reason: Refutation not found, incomplete strategy % 26.15/4.76 % (3449960)Time elapsed: 0.026 s % 26.15/4.76 % (3449960)Peak memory usage: 88 MB % 26.15/4.76 % (3449960)Instructions burned: 68 (million) % 26.15/4.76 % (3449948)Instruction limit reached! % 26.15/4.76 % (3449948)------------------------------ % 26.15/4.76 % (3449948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449948)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449948)Termination reason: Instruction limit % 26.15/4.76 % (3449948)Termination phase: Saturation % 26.15/4.76 % (3449948)Time elapsed: 0.419 s % 26.15/4.76 % (3449948)Peak memory usage: 133 MB % 26.15/4.76 % (3449948)Instructions burned: 483 (million) % 26.15/4.76 % (3449964)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2771447910:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi) % 26.15/4.76 % (3449953)Instruction limit reached! % 26.15/4.76 % (3449953)------------------------------ % 26.15/4.76 % (3449953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449953)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449953)Termination reason: Instruction limit % 26.15/4.76 % (3449953)Termination phase: Saturation % 26.15/4.76 % (3449953)Time elapsed: 0.291 s % 26.15/4.76 % (3449953)Peak memory usage: 113 MB % 26.15/4.76 % (3449953)Instructions burned: 350 (million) % 26.15/4.76 % (3449964)Refutation not found, incomplete strategy % 26.15/4.76 % (3449964)------------------------------ % 26.15/4.76 % (3449964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449964)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449964)Termination reason: Refutation not found, incomplete strategy % 26.15/4.76 % (3449964)Time elapsed: 0.055 s % 26.15/4.76 % (3449964)Peak memory usage: 112 MB % 26.15/4.76 % (3449964)Instructions burned: 73 (million) % 26.15/4.76 % (3449958)Instruction limit reached! % 26.15/4.76 % (3449958)------------------------------ % 26.15/4.76 % (3449958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449958)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449958)Termination reason: Instruction limit % 26.15/4.76 % (3449958)Termination phase: Saturation % 26.15/4.76 % (3449958)Time elapsed: 0.273 s % 26.15/4.76 % (3449958)Peak memory usage: 112 MB % 26.15/4.76 % (3449958)Instructions burned: 328 (million) % 26.15/4.76 % (3449959)Instruction limit reached! % 26.15/4.76 % (3449959)------------------------------ % 26.15/4.76 % (3449959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.15/4.76 % (3449959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.15/4.76 % (3449959)CaDiCaL version: 2.1.3 % 26.15/4.76 % (3449959)Termination reason: Instruction limit % 26.15/4.76 % (3449959)Termination phase: Saturation % 26.15/4.76 % (3449959)Time elapsed: 0.238 s % 26.15/4.76 % (3449959)Peak memory usage: 112 MB % 31.24/5.39 % (3449959)Instructions burned: 282 (million) % 31.24/5.39 % (3449960)------------------------------ % 31.24/5.39 % (3449960)------------------------------ % 31.24/5.39 % (3449956)------------------------------ % 31.24/5.39 % (3449956)------------------------------ % 31.24/5.39 % (3449968)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4232728462:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi) % 31.24/5.39 % (3449969)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2422925923:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 31.24/5.39 % (3449972)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3444029768:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/387Mi) % 31.24/5.39 % (3449970)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=4126892563:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 31.24/5.39 % (3449968)Refutation not found, incomplete strategy % 31.24/5.39 % (3449968)------------------------------ % 31.24/5.39 % (3449968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.39 % (3449968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.39 % (3449968)CaDiCaL version: 2.1.3 % 31.24/5.39 % (3449968)Termination reason: Refutation not found, incomplete strategy % 31.24/5.39 % (3449968)Time elapsed: 0.087 s % 31.24/5.39 % (3449968)Peak memory usage: 111 MB % 31.24/5.39 % (3449968)Instructions burned: 72 (million) % 31.24/5.39 % (3449972)Refutation not found, incomplete strategy % 31.24/5.39 % (3449972)------------------------------ % 31.24/5.39 % (3449972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.39 % (3449972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.39 % (3449972)CaDiCaL version: 2.1.3 % 31.24/5.39 % (3449972)Termination reason: Refutation not found, incomplete strategy % 31.24/5.39 % (3449972)Time elapsed: 0.049 s % 31.24/5.39 % (3449972)Peak memory usage: 111 MB % 31.24/5.39 % (3449972)Instructions burned: 77 (million) % 31.24/5.39 % (3449971)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=520641631:i=375:kws=inv_arity_squared:rtra=on_2968 on theBenchmark for (2968ds/375Mi) % 31.24/5.39 % (3449964)------------------------------ % 31.24/5.39 % (3449964)------------------------------ % 31.24/5.39 % (3449974)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2321776279:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2967 on theBenchmark for (2967ds/513Mi) % 31.24/5.39 % (3449970)Instruction limit reached! % 31.24/5.39 % (3449970)------------------------------ % 31.24/5.39 % (3449970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.39 % (3449970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.39 % (3449970)CaDiCaL version: 2.1.3 % 31.24/5.39 % (3449970)Termination reason: Instruction limit % 31.24/5.39 % (3449970)Termination phase: Saturation % 31.24/5.39 % (3449970)Time elapsed: 0.262 s % 31.24/5.39 % (3449970)Peak memory usage: 129 MB % 31.24/5.39 % (3449970)Instructions burned: 277 (million) % 31.24/5.39 % (3449972)------------------------------ % 31.24/5.39 % (3449972)------------------------------ % 31.24/5.39 % (3449969)Instruction limit reached! % 31.24/5.39 % (3449969)------------------------------ % 31.24/5.39 % (3449969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.39 % (3449969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.39 % (3449969)CaDiCaL version: 2.1.3 % 31.24/5.39 % (3449969)Termination reason: Instruction limit % 31.24/5.39 % (3449969)Termination phase: Saturation % 31.24/5.39 % (3449969)Time elapsed: 0.377 s % 31.24/5.39 % (3449969)Peak memory usage: 112 MB % 31.24/5.39 % (3449969)Instructions burned: 471 (million) % 31.24/5.39 % (3449971)Instruction limit reached! % 31.24/5.39 % (3449971)------------------------------ % 31.24/5.39 % (3449971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.24/5.39 % (3449971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.24/5.39 % (3449971)CaDiCaL version: 2.1.3 % 31.24/5.39 % (3449971)Termination reason: Instruction limit % 31.24/5.39 % (3449971)Termination phase: Saturation % 31.24/5.39 % (3449971)Time elapsed: 0.314 s % 37.34/6.09 % (3449971)Peak memory usage: 113 MB % 37.34/6.09 % (3449971)Instructions burned: 377 (million) % 37.34/6.09 % (3449979)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1533056675:i=334:rtra=on_2965 on theBenchmark for (2965ds/334Mi) % 37.34/6.09 % (3449968)------------------------------ % 37.34/6.09 % (3449968)------------------------------ % 37.34/6.09 % (3449982)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=614952513:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2964 on theBenchmark for (2964ds/341Mi) % 37.34/6.09 % (3449981)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=538376073:i=359:rtra=on:gtg=exists_top:ss=axioms_2964 on theBenchmark for (2964ds/359Mi) % 37.34/6.09 % (3449983)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2104599049:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/261Mi) % 37.34/6.09 % (3449981)Refutation not found, incomplete strategy % 37.34/6.09 % (3449981)------------------------------ % 37.34/6.09 % (3449981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.34/6.09 % (3449981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.34/6.09 % (3449981)CaDiCaL version: 2.1.3 % 37.34/6.09 % (3449981)Termination reason: Refutation not found, incomplete strategy % 37.34/6.09 % (3449981)Time elapsed: 0.074 s % 37.34/6.09 % (3449981)Peak memory usage: 88 MB % 37.34/6.09 % (3449981)Instructions burned: 97 (million) % 37.34/6.09 % (3449974)Instruction limit reached! % 37.34/6.09 % (3449974)------------------------------ % 37.34/6.09 % (3449974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.34/6.09 % (3449974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.34/6.09 % (3449974)CaDiCaL version: 2.1.3 % 37.34/6.09 % (3449974)Termination reason: Instruction limit % 37.34/6.09 % (3449974)Termination phase: Saturation % 37.34/6.09 % (3449974)Time elapsed: 0.376 s % 37.34/6.09 % (3449974)Peak memory usage: 90 MB % 37.34/6.09 % (3449974)Instructions burned: 514 (million) % 37.34/6.09 % (3449982)Instruction limit reached! % 37.34/6.09 % (3449982)------------------------------ % 37.34/6.09 % (3449982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.34/6.09 % (3449982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.34/6.09 % (3449982)CaDiCaL version: 2.1.3 % 37.34/6.09 % (3449982)Termination reason: Instruction limit % 37.34/6.09 % (3449982)Termination phase: Saturation % 37.34/6.09 % (3449982)Time elapsed: 0.152 s % 37.34/6.09 % (3449982)Peak memory usage: 117 MB % 37.34/6.09 % (3449982)Instructions burned: 341 (million) % 37.34/6.09 % (3449984)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=928966087:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/235Mi) % 37.34/6.09 % (3449986)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=716010350:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 37.34/6.09 % (3449983)Refutation not found, incomplete strategy % 37.34/6.09 % (3449983)------------------------------ % 37.34/6.09 % (3449983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.34/6.09 % (3449983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.34/6.09 % (3449983)CaDiCaL version: 2.1.3 % 37.34/6.09 % (3449983)Termination reason: Refutation not found, incomplete strategy % 37.34/6.09 % (3449983)Time elapsed: 0.067 s % 37.34/6.09 % (3449983)Peak memory usage: 111 MB % 37.34/6.09 % (3449983)Instructions burned: 48 (million) % 37.34/6.09 % (3449979)Instruction limit reached! % 37.34/6.09 % (3449979)------------------------------ % 37.34/6.09 % (3449979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.34/6.09 % (3449979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.34/6.09 % (3449979)CaDiCaL version: 2.1.3 % 37.34/6.09 % (3449979)Termination reason: Instruction limit % 37.34/6.09 % (3449979)Termination phase: Saturation % 37.34/6.09 % (3449979)Time elapsed: 0.307 s % 37.34/6.09 % (3449979)Peak memory usage: 130 MB % 37.34/6.09 % (3449979)Instructions burned: 334 (million) % 37.34/6.09 % (3449984)Refutation not found, incomplete strategy % 37.34/6.09 % (3449984)------------------------------ % 37.34/6.09 % (3449984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.98/6.68 % (3449984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.98/6.68 % (3449984)CaDiCaL version: 2.1.3 % 39.98/6.68 % (3449984)Termination reason: Refutation not found, incomplete strategy % 39.98/6.68 % (3449984)Time elapsed: 0.091 s % 39.98/6.68 % (3449984)Peak memory usage: 111 MB % 39.98/6.68 % (3449984)Instructions burned: 76 (million) % 39.98/6.68 % (3449991)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1048859047:i=4428:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/4428Mi) % 39.98/6.68 % (3449986)Instruction limit reached! % 39.98/6.68 % (3449986)------------------------------ % 39.98/6.68 % (3449986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.98/6.68 % (3449986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.98/6.68 % (3449986)CaDiCaL version: 2.1.3 % 39.98/6.68 % (3449986)Termination reason: Instruction limit % 39.98/6.68 % (3449986)Termination phase: Saturation % 39.98/6.68 % (3449986)Time elapsed: 0.206 s % 39.98/6.68 % (3449986)Peak memory usage: 90 MB % 39.98/6.68 % (3449986)Instructions burned: 274 (million) % 39.98/6.68 % (3449990)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3908334992:i=146:doe=on:rtra=on_2960 on theBenchmark for (2960ds/146Mi) % 39.98/6.68 % (3449994)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=362560032:avsq=on:i=276:avsqr=1,2:rtra=on_2959 on theBenchmark for (2959ds/276Mi) % 39.98/6.68 % (3449981)------------------------------ % 39.98/6.68 % (3449981)------------------------------ % 39.98/6.68 % (3449990)Instruction limit reached! % 39.98/6.68 % (3449990)------------------------------ % 39.98/6.68 % (3449990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.98/6.68 % (3449990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.98/6.68 % (3449990)CaDiCaL version: 2.1.3 % 39.98/6.68 % (3449990)Termination reason: Instruction limit % 39.98/6.68 % (3449990)Termination phase: Saturation % 39.98/6.68 % (3449990)Time elapsed: 0.110 s % 39.98/6.68 % (3449990)Peak memory usage: 88 MB % 39.98/6.68 % (3449990)Instructions burned: 147 (million) % 39.98/6.68 % (3449983)------------------------------ % 39.98/6.68 % (3449983)------------------------------ % 39.98/6.68 % (3449996)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=432653323:i=1052:rtra=on_2958 on theBenchmark for (2958ds/1052Mi) % 39.98/6.68 % (3449984)------------------------------ % 39.98/6.68 % (3449984)------------------------------ % 39.98/6.68 % (3449994)Instruction limit reached! % 39.98/6.68 % (3449994)------------------------------ % 39.98/6.68 % (3449994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.98/6.68 % (3449994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.98/6.68 % (3449994)CaDiCaL version: 2.1.3 % 39.98/6.68 % (3449994)Termination reason: Instruction limit % 39.98/6.68 % (3449994)Termination phase: Saturation % 39.98/6.68 % (3449994)Time elapsed: 0.261 s % 39.98/6.68 % (3449994)Peak memory usage: 130 MB % 39.98/6.68 % (3449994)Instructions burned: 276 (million) % 39.98/6.68 % (3449999)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4274629089:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi) % 39.98/6.68 % (3450000)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1671960687:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2956 on theBenchmark for (2956ds/1054Mi) % 39.98/6.68 % (3450000)Refutation not found, incomplete strategy % 39.98/6.68 % (3450000)------------------------------ % 39.98/6.68 % (3450000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.98/6.68 % (3450000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.98/6.68 % (3450000)CaDiCaL version: 2.1.3 % 39.98/6.68 % (3450000)Termination reason: Refutation not found, incomplete strategy % 39.98/6.68 % (3450000)Time elapsed: 0.032 s % 39.98/6.68 % (3450000)Peak memory usage: 87 MB % 39.98/6.68 % (3450000)Instructions burned: 42 (million) % 39.98/6.68 % (3450002)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3558034415:i=107:rtra=on_2956 on theBenchmark for (2956ds/107Mi) % 39.98/6.68 % (3450003)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3053814667:s2a=on:i=450:doe=on:nm=32:rtra=on_2955 on theBenchmark for (2955ds/450Mi) % 45.01/7.20 % (3450002)Instruction limit reached! % 45.01/7.20 % (3450002)------------------------------ % 45.01/7.20 % (3450002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.01/7.20 % (3450002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.01/7.20 % (3450002)CaDiCaL version: 2.1.3 % 45.01/7.20 % (3450002)Termination reason: Instruction limit % 45.01/7.20 % (3450002)Termination phase: Saturation % 45.01/7.20 % (3450002)Time elapsed: 0.081 s % 45.01/7.20 % (3450002)Peak memory usage: 88 MB % 45.01/7.20 % (3450002)Instructions burned: 108 (million) % 45.01/7.20 % (3450005)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 % 45.01/7.20 % (3450005)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=951718085:i=1090:aac=none:nm=0:rtra=on:rawr=on_2954 on theBenchmark for (2954ds/1090Mi) % 45.01/7.20 % (3449999)Refutation not found, incomplete strategy % 45.01/7.20 % (3449999)------------------------------ % 45.01/7.20 % (3449999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.01/7.20 % (3449999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.01/7.20 % (3449999)CaDiCaL version: 2.1.3 % 45.01/7.20 % (3449999)Termination reason: Refutation not found, incomplete strategy % 45.01/7.20 % (3449999)Time elapsed: 0.391 s % 45.01/7.20 % (3449999)Peak memory usage: 95 MB % 45.01/7.20 % (3449999)Instructions burned: 526 (million) % 45.01/7.20 % (3450000)------------------------------ % 45.01/7.20 % (3450000)------------------------------ % 45.01/7.20 % (3450009)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2263121761:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2953 on theBenchmark for (2953ds/130Mi) % 45.01/7.20 % (3450003)Instruction limit reached! % 45.01/7.20 % (3450003)------------------------------ % 45.01/7.20 % (3450003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.01/7.20 % (3450003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.01/7.20 % (3450003)CaDiCaL version: 2.1.3 % 45.01/7.20 % (3450003)Termination reason: Instruction limit % 45.01/7.20 % (3450003)Termination phase: Saturation % 45.01/7.20 % (3450003)Time elapsed: 0.391 s % 45.01/7.20 % (3450003)Peak memory usage: 130 MB % 45.01/7.20 % (3450003)Instructions burned: 450 (million) % 45.01/7.20 % (3449996)Instruction limit reached! % 45.01/7.20 % (3449996)------------------------------ % 45.01/7.20 % (3449996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.01/7.20 % (3449996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.01/7.20 % (3449996)CaDiCaL version: 2.1.3 % 45.01/7.20 % (3449996)Termination reason: Instruction limit % 45.01/7.20 % (3449996)Termination phase: Saturation % 45.01/7.20 % (3449996)Time elapsed: 0.730 s % 45.01/7.20 % (3449996)Peak memory usage: 91 MB % 45.01/7.20 % (3449996)Instructions burned: 1052 (million) % 45.01/7.20 % (3450009)Instruction limit reached! % 45.01/7.20 % (3450009)------------------------------ % 45.01/7.20 % (3450009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.01/7.20 % (3450009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.01/7.20 % (3450009)CaDiCaL version: 2.1.3 % 45.01/7.20 % (3450009)Termination reason: Instruction limit % 45.01/7.20 % (3450009)Termination phase: Twee Goal Transformation % 45.01/7.20 % (3450009)Time elapsed: 0.102 s % 45.01/7.20 % (3450009)Peak memory usage: 87 MB % 45.01/7.20 % (3450009)Instructions burned: 130 (million) % 45.01/7.20 % (3450012)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1703505557:i=312:kws=inv_frequency:nm=20:rtra=on_2950 on theBenchmark for (2950ds/312Mi) % 45.01/7.20 % (3449999)------------------------------ % 45.01/7.20 % (3449999)------------------------------ % 45.01/7.20 % (3450013)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=741855130:i=491:doe=on:rtra=on:gtg=position_2949 on theBenchmark for (2949ds/491Mi) % 45.01/7.20 % (3450014)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3002949507:s2a=on:i=835:s2at=2:rtra=on_2948 on theBenchmark for (2948ds/835Mi) % 45.01/7.20 % (3450015)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=397117204:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2948 on theBenchmark for (2948ds/307Mi) % 46.13/7.81 % (3450012)Instruction limit reached! % 46.13/7.81 % (3450012)------------------------------ % 46.13/7.81 % (3450012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.13/7.81 % (3450012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.13/7.81 % (3450012)CaDiCaL version: 2.1.3 % 46.13/7.81 % (3450012)Termination reason: Instruction limit % 46.13/7.81 % (3450012)Termination phase: Saturation % 46.13/7.81 % (3450012)Time elapsed: 0.262 s % 46.13/7.81 % (3450012)Peak memory usage: 112 MB % 46.13/7.81 % (3450012)Instructions burned: 312 (million) % 46.13/7.81 % (3450013)Refutation not found, incomplete strategy % 46.13/7.81 % (3450013)------------------------------ % 46.13/7.81 % (3450013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.13/7.81 % (3450013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.13/7.81 % (3450013)CaDiCaL version: 2.1.3 % 46.13/7.81 % (3450013)Termination reason: Refutation not found, incomplete strategy % 46.13/7.81 % (3450013)Time elapsed: 0.156 s % 46.13/7.81 % (3450013)Peak memory usage: 90 MB % 46.13/7.81 % (3450013)Instructions burned: 251 (million) % 46.13/7.81 % (3450015)Refutation not found, incomplete strategy % 46.13/7.81 % (3450015)------------------------------ % 46.13/7.81 % (3450015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.13/7.81 % (3450015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.13/7.81 % (3450015)CaDiCaL version: 2.1.3 % 46.13/7.81 % (3450015)Termination reason: Refutation not found, incomplete strategy % 46.13/7.81 % (3450015)Time elapsed: 0.146 s % 46.13/7.81 % (3450015)Peak memory usage: 90 MB % 46.13/7.81 % (3450015)Instructions burned: 195 (million) % 46.13/7.81 % (3450018)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2124724128:i=776:doe=on:rtra=on_2946 on theBenchmark for (2946ds/776Mi) % 46.13/7.81 % (3450005)Instruction limit reached! % 46.13/7.81 % (3450005)------------------------------ % 46.13/7.81 % (3450005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.13/7.81 % (3450005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.13/7.81 % (3450005)CaDiCaL version: 2.1.3 % 46.13/7.81 % (3450005)Termination reason: Instruction limit % 46.13/7.81 % (3450005)Termination phase: Saturation % 46.13/7.81 % (3450005)Time elapsed: 0.827 s % 46.13/7.81 % (3450005)Peak memory usage: 118 MB % 46.13/7.81 % (3450005)Instructions burned: 1090 (million) % 46.13/7.81 % (3450022)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3586492192:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2945 on theBenchmark for (2945ds/646Mi) % 46.13/7.81 % (3449991)Instruction limit reached! % 46.13/7.81 % (3449991)------------------------------ % 46.13/7.81 % (3449991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.13/7.81 % (3449991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.13/7.81 % (3449991)CaDiCaL version: 2.1.3 % 46.13/7.81 % (3449991)Termination reason: Instruction limit % 46.13/7.81 % (3449991)Termination phase: Saturation % 46.13/7.81 % (3449991)Time elapsed: 1.622 s % 46.13/7.81 % (3449991)Peak memory usage: 90 MB % 46.13/7.81 % (3449991)Instructions burned: 4430 (million) % 46.13/7.81 % (3450013)------------------------------ % 46.13/7.81 % (3450013)------------------------------ % 46.13/7.81 % (3450025)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=602435890:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2943 on theBenchmark for (2943ds/784Mi) % 46.13/7.82 % (3450015)------------------------------ % 46.13/7.82 % (3450015)------------------------------ % 46.13/7.82 % (3450027)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=1547349934:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2942 on theBenchmark for (2942ds/1131Mi) % 46.13/7.82 % (3450014)Instruction limit reached! % 46.13/7.82 % (3450014)------------------------------ % 46.13/7.82 % (3450014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.13/7.82 % (3450014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.13/7.82 % (3450014)CaDiCaL version: 2.1.3 % 46.13/7.82 % (3450014)Termination reason: Instruction limit % 46.13/7.82 % (3450014)Termination phase: Saturation % 46.13/7.82 % (3450014)Time elapsed: 0.589 s % 46.13/7.82 % (3450014)Peak memory usage: 89 MB % 59.04/9.16 % (3450014)Instructions burned: 835 (million) % 59.04/9.16 % (3450028)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=872870414:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2941 on theBenchmark for (2941ds/246Mi) % 59.04/9.16 % (3450028)Refutation not found, incomplete strategy % 59.04/9.16 % (3450028)------------------------------ % 59.04/9.16 % (3450028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.04/9.16 % (3450028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.04/9.16 % (3450028)CaDiCaL version: 2.1.3 % 59.04/9.16 % (3450028)Termination reason: Refutation not found, incomplete strategy % 59.04/9.16 % (3450028)Time elapsed: 0.048 s % 59.04/9.16 % (3450028)Peak memory usage: 111 MB % 59.04/9.16 % (3450028)Instructions burned: 76 (million) % 59.04/9.16 % (3450018)Instruction limit reached! % 59.04/9.16 % (3450018)------------------------------ % 59.04/9.16 % (3450018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.04/9.16 % (3450018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.04/9.16 % (3450018)CaDiCaL version: 2.1.3 % 59.04/9.16 % (3450018)Termination reason: Instruction limit % 59.04/9.16 % (3450018)Termination phase: Saturation % 59.04/9.16 % (3450018)Time elapsed: 0.571 s % 59.04/9.16 % (3450018)Peak memory usage: 114 MB % 59.04/9.16 % (3450018)Instructions burned: 777 (million) % 59.04/9.16 % (3450030)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3026954418:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2940 on theBenchmark for (2940ds/775Mi) % 59.04/9.16 % (3450022)Instruction limit reached! % 59.04/9.16 % (3450022)------------------------------ % 59.04/9.16 % (3450022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.04/9.16 % (3450022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.04/9.16 % (3450022)CaDiCaL version: 2.1.3 % 59.04/9.16 % (3450022)Termination reason: Instruction limit % 59.04/9.16 % (3450022)Termination phase: Saturation % 59.04/9.16 % (3450022)Time elapsed: 0.532 s % 59.04/9.16 % (3450022)Peak memory usage: 136 MB % 59.04/9.16 % (3450022)Instructions burned: 647 (million) % 59.04/9.16 % (3450032)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4092359118:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2940 on theBenchmark for (2940ds/273Mi) % 59.04/9.16 % (3450030)Refutation not found, incomplete strategy % 59.04/9.16 % (3450030)------------------------------ % 59.04/9.16 % (3450030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.04/9.16 % (3450030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.04/9.16 % (3450030)CaDiCaL version: 2.1.3 % 59.04/9.16 % (3450030)Termination reason: Refutation not found, incomplete strategy % 59.04/9.16 % (3450030)Time elapsed: 0.055 s % 59.04/9.16 % (3450030)Peak memory usage: 88 MB % 59.04/9.16 % (3450030)Instructions burned: 74 (million) % 59.04/9.16 % (3450028)------------------------------ % 59.04/9.16 % (3450028)------------------------------ % 59.04/9.16 % (3450034)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3784907855:i=102:nm=16:rtra=on_2938 on theBenchmark for (2938ds/102Mi) % 59.04/9.16 % (3450036)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2998802092:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2937 on theBenchmark for (2937ds/1094Mi) % 59.04/9.16 % (3450032)Instruction limit reached! % 59.04/9.16 % (3450032)------------------------------ % 59.04/9.16 % (3450032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.04/9.16 % (3450032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.04/9.16 % (3450032)CaDiCaL version: 2.1.3 % 59.04/9.16 % (3450032)Termination reason: Instruction limit % 59.04/9.16 % (3450032)Termination phase: Saturation % 59.04/9.16 % (3450032)Time elapsed: 0.209 s % 59.04/9.16 % (3450032)Peak memory usage: 91 MB % 59.04/9.16 % (3450032)Instructions burned: 273 (million) % 59.04/9.16 % (3450025)Instruction limit reached! % 59.04/9.16 % (3450025)------------------------------ % 59.04/9.16 % (3450025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.04/9.16 % (3450025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.04/9.16 % (3450025)CaDiCaL version: 2.1.3 % 59.04/9.16 % (3450025)Termination reason: Instruction limit % 59.04/9.16 % (3450025)Termination phase: Saturation % 77.07/11.70 % (3450025)Time elapsed: 0.588 s % 77.07/11.70 % (3450025)Peak memory usage: 113 MB % 77.07/11.70 % (3450025)Instructions burned: 784 (million) % 77.07/11.70 % (3450034)Instruction limit reached! % 77.07/11.70 % (3450034)------------------------------ % 77.07/11.70 % (3450034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.07/11.70 % (3450034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.07/11.70 % (3450034)CaDiCaL version: 2.1.3 % 77.07/11.70 % (3450034)Termination reason: Instruction limit % 77.07/11.70 % (3450034)Termination phase: Saturation % 77.07/11.70 % (3450034)Time elapsed: 0.078 s % 77.07/11.70 % (3450034)Peak memory usage: 88 MB % 77.07/11.70 % (3450034)Instructions burned: 103 (million) % 77.07/11.70 % (3450038)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2212731990:i=6400:doe=on:fsr=off:rtra=on_2936 on theBenchmark for (2936ds/6400Mi) % 77.07/11.70 % (3450030)------------------------------ % 77.07/11.70 % (3450030)------------------------------ % 77.07/11.70 % (3450042)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=2046750711:i=1846:canc=cautious:fsr=off:rtra=on_2935 on theBenchmark for (2935ds/1846Mi) % 77.07/11.70 % (3450041)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=4141449967:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2935 on theBenchmark for (2935ds/868Mi) % 77.07/11.70 % (3450027)Instruction limit reached! % 77.07/11.70 % (3450027)------------------------------ % 77.07/11.70 % (3450027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.07/11.70 % (3450027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.07/11.70 % (3450027)CaDiCaL version: 2.1.3 % 77.07/11.70 % (3450027)Termination reason: Instruction limit % 77.07/11.70 % (3450027)Termination phase: Saturation % 77.07/11.70 % (3450027)Time elapsed: 0.730 s % 77.07/11.70 % (3450027)Peak memory usage: 114 MB % 77.07/11.70 % (3450027)Instructions burned: 1131 (million) % 77.07/11.70 % (3450043)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=634967979:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2935 on theBenchmark for (2935ds/36816Mi) % 77.07/11.70 % (3450042)Refutation not found, incomplete strategy % 77.07/11.70 % (3450042)------------------------------ % 77.07/11.70 % (3450042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.07/11.70 % (3450042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.07/11.70 % (3450042)CaDiCaL version: 2.1.3 % 77.07/11.70 % (3450042)Termination reason: Refutation not found, incomplete strategy % 77.07/11.70 % (3450042)Time elapsed: 0.112 s % 77.07/11.70 % (3450042)Peak memory usage: 89 MB % 77.07/11.70 % (3450042)Instructions burned: 170 (million) % 77.07/11.70 % (3450036)Instruction limit reached! % 77.07/11.70 % (3450036)------------------------------ % 77.07/11.70 % (3450036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.07/11.70 % (3450036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.07/11.70 % (3450036)CaDiCaL version: 2.1.3 % 77.07/11.70 % (3450036)Termination reason: Instruction limit % 77.07/11.70 % (3450036)Termination phase: Saturation % 77.07/11.70 % (3450036)Time elapsed: 0.391 s % 77.07/11.70 % (3450036)Peak memory usage: 91 MB % 77.07/11.70 % (3450036)Instructions burned: 1096 (million) % 77.07/11.70 % (3450048)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=3442129246:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2933 on theBenchmark for (2933ds/863Mi) % 77.07/11.70 % (3450045)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1465585820:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2933 on theBenchmark for (2933ds/273Mi) % 77.07/11.70 % (3450050)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2937155562:i=5811:kws=precedence:nm=0:rtra=on_2931 on theBenchmark for (2931ds/5811Mi) % 77.07/11.70 % (3450045)Instruction limit reached! % 77.07/11.70 % (3450045)------------------------------ % 77.07/11.70 % (3450045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.07/11.70 % (3450045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.07/11.70 % (3450045)CaDiCaL version: 2.1.3 % 77.07/11.70 % (3450045)Termination reason: Instruction limit % 77.07/11.70 % (3450045)Termination phase: Saturation % 81.48/12.62 % (3450045)Time elapsed: 0.208 s % 81.48/12.62 % (3450045)Peak memory usage: 91 MB % 81.48/12.62 % (3450045)Instructions burned: 273 (million) % 81.48/12.62 % (3450042)------------------------------ % 81.48/12.62 % (3450042)------------------------------ % 81.48/12.62 % (3450048)Instruction limit reached! % 81.48/12.62 % (3450048)------------------------------ % 81.48/12.62 % (3450048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.48/12.62 % (3450048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.48/12.62 % (3450048)CaDiCaL version: 2.1.3 % 81.48/12.62 % (3450048)Termination reason: Instruction limit % 81.48/12.62 % (3450048)Termination phase: Saturation % 81.48/12.62 % (3450048)Time elapsed: 0.417 s % 81.48/12.62 % (3450048)Peak memory usage: 128 MB % 81.48/12.62 % (3450048)Instructions burned: 863 (million) % 81.48/12.62 % (3450054)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=3752502471:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2929 on theBenchmark for (2929ds/2216Mi) % 81.48/12.62 % (3450055)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3986061230:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2928 on theBenchmark for (2928ds/801Mi) % 81.48/12.62 % (3450041)Instruction limit reached! % 81.48/12.62 % (3450041)------------------------------ % 81.48/12.62 % (3450041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.48/12.62 % (3450041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.48/12.62 % (3450041)CaDiCaL version: 2.1.3 % 81.48/12.62 % (3450041)Termination reason: Instruction limit % 81.48/12.62 % (3450041)Termination phase: Saturation % 81.48/12.62 % (3450041)Time elapsed: 0.738 s % 81.48/12.62 % (3450041)Peak memory usage: 128 MB % 81.48/12.62 % (3450041)Instructions burned: 868 (million) % 81.48/12.62 % (3450056)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2328023785:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2927 on theBenchmark for (2927ds/1026Mi) % 81.48/12.62 % (3450056)Refutation not found, incomplete strategy % 81.48/12.62 % (3450056)------------------------------ % 81.48/12.62 % (3450056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.48/12.62 % (3450056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.48/12.62 % (3450056)CaDiCaL version: 2.1.3 % 81.48/12.62 % (3450056)Termination reason: Refutation not found, incomplete strategy % 81.48/12.62 % (3450056)Time elapsed: 0.017 s % 81.48/12.62 % (3450056)Peak memory usage: 87 MB % 81.48/12.62 % (3450056)Instructions burned: 42 (million) % 81.48/12.62 % (3450059)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4274117117:i=3509:rtra=on_2925 on theBenchmark for (2925ds/3509Mi) % 81.48/12.62 % (3450056)------------------------------ % 81.48/12.62 % (3450056)------------------------------ % 81.48/12.62 % (3450055)Refutation not found, incomplete strategy % 81.48/12.62 % (3450055)------------------------------ % 81.48/12.62 % (3450055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.48/12.62 % (3450055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.48/12.62 % (3450055)CaDiCaL version: 2.1.3 % 81.48/12.62 % (3450055)Termination reason: Refutation not found, incomplete strategy % 81.48/12.62 % (3450055)Time elapsed: 0.483 s % 81.48/12.62 % (3450055)Peak memory usage: 95 MB % 81.48/12.62 % (3450055)Instructions burned: 529 (million) % 81.48/12.62 % (3450062)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1979476638:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2922 on theBenchmark for (2922ds/2127Mi) % 81.48/12.62 % (3450062)Refutation not found, incomplete strategy % 81.48/12.62 % (3450062)------------------------------ % 81.48/12.62 % (3450062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.48/12.62 % (3450062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.48/12.62 % (3450062)CaDiCaL version: 2.1.3 % 81.48/12.62 % (3450062)Termination reason: Refutation not found, incomplete strategy % 81.48/12.62 % (3450062)Time elapsed: 0.028 s % 81.48/12.62 % (3450062)Peak memory usage: 87 MB % 81.48/12.62 % (3450062)Instructions burned: 70 (million) % 81.48/12.62 % (3450062)------------------------------ % 81.48/12.62 % (3450062)------------------------------ % 81.48/12.62 % (3450055)------------------------------ % 81.48/12.62 % (3450055)------------------------------ % 81.48/12.62 % (3450064)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2265665192:i=1959:rtra=on:fsd=on:proc=on_2917 on theBenchmark for (2917ds/1959Mi) % 116.29/17.22 % (3450065)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1784330158:s2a=on:i=3553:nm=0:rtra=on_2917 on theBenchmark for (2917ds/3553Mi) % 116.29/17.22 % (3450054)Instruction limit reached! % 116.29/17.22 % (3450054)------------------------------ % 116.29/17.22 % (3450054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.29/17.22 % (3450054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.29/17.22 % (3450054)CaDiCaL version: 2.1.3 % 116.29/17.22 % (3450054)Termination reason: Instruction limit % 116.29/17.22 % (3450054)Termination phase: Saturation % 116.29/17.22 % (3450054)Time elapsed: 1.630 s % 116.29/17.22 % (3450054)Peak memory usage: 119 MB % 116.29/17.22 % (3450054)Instructions burned: 2217 (million) % 116.29/17.22 % (3450064)Instruction limit reached! % 116.29/17.22 % (3450064)------------------------------ % 116.29/17.22 % (3450064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.29/17.22 % (3450064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.29/17.22 % (3450064)CaDiCaL version: 2.1.3 % 116.29/17.22 % (3450064)Termination reason: Instruction limit % 116.29/17.22 % (3450064)Termination phase: Saturation % 116.29/17.22 % (3450064)Time elapsed: 0.770 s % 116.29/17.22 % (3450064)Peak memory usage: 119 MB % 116.29/17.22 % (3450064)Instructions burned: 1959 (million) % 116.29/17.22 % (3450068)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2814081311:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2910 on theBenchmark for (2910ds/3201Mi) % 116.29/17.22 % (3450069)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=3323890303:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2907 on theBenchmark for (2907ds/4093Mi) % 116.29/17.22 % (3450068)Refutation not found, incomplete strategy % 116.29/17.22 % (3450068)------------------------------ % 116.29/17.22 % (3450068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.29/17.22 % (3450068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.29/17.22 % (3450068)CaDiCaL version: 2.1.3 % 116.29/17.22 % (3450068)Termination reason: Refutation not found, incomplete strategy % 116.29/17.22 % (3450068)Time elapsed: 0.458 s % 116.29/17.22 % (3450068)Peak memory usage: 93 MB % 116.29/17.22 % (3450068)Instructions burned: 609 (million) % 116.29/17.22 % (3450059)Instruction limit reached! % 116.29/17.22 % (3450059)------------------------------ % 116.29/17.22 % (3450059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.29/17.22 % (3450059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.29/17.22 % (3450059)CaDiCaL version: 2.1.3 % 116.29/17.22 % (3450059)Termination reason: Instruction limit % 116.29/17.22 % (3450059)Termination phase: Saturation % 116.29/17.22 % (3450059)Time elapsed: 2.378 s % 116.29/17.22 % (3450059)Peak memory usage: 90 MB % 116.29/17.22 % (3450059)Instructions burned: 3510 (million) % 116.29/17.22 % (3450068)------------------------------ % 116.29/17.22 % (3450068)------------------------------ % 116.29/17.22 % (3450072)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=1931529905:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2899 on theBenchmark for (2899ds/21173Mi) % 116.29/17.22 % (3450073)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=688391880:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2899 on theBenchmark for (2899ds/10544Mi) % 116.29/17.22 % (3450072)Refutation not found, incomplete strategy % 116.29/17.22 % (3450072)------------------------------ % 116.29/17.22 % (3450072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.29/17.22 % (3450072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.29/17.22 % (3450072)CaDiCaL version: 2.1.3 % 116.29/17.22 % (3450072)Termination reason: Refutation not found, incomplete strategy % 116.29/17.22 % (3450072)Time elapsed: 0.063 s % 116.29/17.22 % (3450072)Peak memory usage: 112 MB % 116.29/17.22 % (3450072)Instructions burned: 41 (million) % 116.29/17.22 % (3450072)------------------------------ % 116.29/17.22 % (3450072)------------------------------ % 116.29/17.22 % (3450077)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1662711809:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/1262Mi) % 134.61/19.83 % (3450065)Instruction limit reached! % 134.61/19.83 % (3450065)------------------------------ % 134.61/19.83 % (3450065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.61/19.83 % (3450065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.61/19.83 % (3450065)CaDiCaL version: 2.1.3 % 134.61/19.83 % (3450065)Termination reason: Instruction limit % 134.61/19.83 % (3450065)Termination phase: Saturation % 134.61/19.83 % (3450065)Time elapsed: 2.476 s % 134.61/19.83 % (3450065)Peak memory usage: 91 MB % 134.61/19.83 % (3450065)Instructions burned: 3554 (million) % 134.61/19.83 % (3450038)Instruction limit reached! % 134.61/19.83 % (3450038)------------------------------ % 134.61/19.83 % (3450038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.61/19.83 % (3450038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.61/19.83 % (3450038)CaDiCaL version: 2.1.3 % 134.61/19.83 % (3450038)Termination reason: Instruction limit % 134.61/19.83 % (3450038)Termination phase: Saturation % 134.61/19.83 % (3450038)Time elapsed: 4.516 s % 134.61/19.83 % (3450038)Peak memory usage: 90 MB % 134.61/19.83 % (3450038)Instructions burned: 6401 (million) % 134.61/19.83 % (3450080)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1070729902:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2889 on theBenchmark for (2889ds/775Mi) % 134.61/19.83 % (3450080)Refutation not found, incomplete strategy % 134.61/19.83 % (3450080)------------------------------ % 134.61/19.83 % (3450080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.61/19.83 % (3450080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.61/19.83 % (3450080)CaDiCaL version: 2.1.3 % 134.61/19.83 % (3450080)Termination reason: Refutation not found, incomplete strategy % 134.61/19.83 % (3450080)Time elapsed: 0.040 s % 134.61/19.83 % (3450080)Peak memory usage: 88 MB % 134.61/19.83 % (3450080)Instructions burned: 74 (million) % 134.61/19.83 % (3450050)Instruction limit reached! % 134.61/19.83 % (3450050)------------------------------ % 134.61/19.83 % (3450050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.61/19.83 % (3450050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.61/19.83 % (3450050)CaDiCaL version: 2.1.3 % 134.61/19.83 % (3450050)Termination reason: Instruction limit % 134.61/19.83 % (3450050)Termination phase: Saturation % 134.61/19.83 % (3450050)Time elapsed: 4.268 s % 134.61/19.83 % (3450050)Peak memory usage: 119 MB % 134.61/19.83 % (3450050)Instructions burned: 5811 (million) % 134.61/19.83 % (3450081)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3239078883:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2888 on theBenchmark for (2888ds/270Mi) % 134.61/19.83 % (3450081)Instruction limit reached! % 134.61/19.83 % (3450081)------------------------------ % 134.61/19.83 % (3450081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.61/19.83 % (3450081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.61/19.83 % (3450081)CaDiCaL version: 2.1.3 % 134.61/19.83 % (3450081)Termination reason: Instruction limit % 134.61/19.83 % (3450081)Termination phase: Saturation % 134.61/19.83 % (3450081)Time elapsed: 0.106 s % 134.61/19.83 % (3450081)Peak memory usage: 90 MB % 134.61/19.83 % (3450081)Instructions burned: 271 (million) % 134.61/19.83 % (3450084)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2389030600:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2886 on theBenchmark for (2886ds/17165Mi) % 134.61/19.83 % (3450085)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=507505168:s2a=on:i=13094:s2at=-1:rtra=on_2885 on theBenchmark for (2885ds/13094Mi) % 134.61/19.83 % (3450080)------------------------------ % 134.61/19.83 % (3450080)------------------------------ % 134.61/19.83 % (3450077)Instruction limit reached! % 134.61/19.83 % (3450077)------------------------------ % 134.61/19.83 % (3450077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.61/19.83 % (3450077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.61/19.83 % (3450077)CaDiCaL version: 2.1.3 % 134.61/19.83 % (3450077)Termination reason: Instruction limit % 134.61/19.83 % (3450077)Termination phase: Saturation % 134.61/19.83 % (3450077)Time elapsed: 0.893 s % 134.61/19.83 % (3450077)Peak memory usage: 119 MB % 134.61/19.83 % (3450077)Instructions burned: 1262 (million) % 134.61/19.83 % (3450089)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2752950928:st=2:i=12633:rtra=on:ss=axioms_2882 on theBenchmark for (2882ds/12633Mi) % 154.47/22.66 % (3450089)Refutation not found, incomplete strategy % 154.47/22.66 % (3450089)------------------------------ % 154.47/22.66 % (3450089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.47/22.66 % (3450089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.47/22.66 % (3450089)CaDiCaL version: 2.1.3 % 154.47/22.66 % (3450089)Termination reason: Refutation not found, incomplete strategy % 154.47/22.66 % (3450089)Time elapsed: 0.027 s % 154.47/22.66 % (3450089)Peak memory usage: 87 MB % 154.47/22.66 % (3450089)Instructions burned: 65 (million) % 154.47/22.66 % (3450090)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2809735600:i=1783:rtra=on:gtg=position_2881 on theBenchmark for (2881ds/1783Mi) % 154.47/22.66 % (3450089)------------------------------ % 154.47/22.66 % (3450089)------------------------------ % 154.47/22.66 % (3450069)Instruction limit reached! % 154.47/22.66 % (3450069)------------------------------ % 154.47/22.66 % (3450069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.47/22.66 % (3450069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.47/22.66 % (3450069)CaDiCaL version: 2.1.3 % 154.47/22.66 % (3450069)Termination reason: Instruction limit % 154.47/22.66 % (3450069)Termination phase: Saturation % 154.47/22.66 % (3450069)Time elapsed: 2.871 s % 154.47/22.66 % (3450069)Peak memory usage: 132 MB % 154.47/22.66 % (3450069)Instructions burned: 4093 (million) % 154.47/22.66 % (3450095)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=1998705713:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2876 on theBenchmark for (2876ds/4975Mi) % 154.47/22.66 % (3450094)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=109738601:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2876 on theBenchmark for (2876ds/5451Mi) % 154.47/22.66 % (3450090)Instruction limit reached! % 154.47/22.66 % (3450090)------------------------------ % 154.47/22.66 % (3450090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.47/22.66 % (3450090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.47/22.66 % (3450090)CaDiCaL version: 2.1.3 % 154.47/22.66 % (3450090)Termination reason: Instruction limit % 154.47/22.66 % (3450090)Termination phase: Saturation % 154.47/22.66 % (3450090)Time elapsed: 1.318 s % 154.47/22.66 % (3450090)Peak memory usage: 119 MB % 154.47/22.66 % (3450090)Instructions burned: 1783 (million) % 154.47/22.66 % (3450100)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=1304059495:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2865 on theBenchmark for (2865ds/2076Mi) % 154.47/22.66 % (3450100)Instruction limit reached! % 154.47/22.66 % (3450100)------------------------------ % 154.47/22.66 % (3450100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.47/22.66 % (3450100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.47/22.66 % (3450100)CaDiCaL version: 2.1.3 % 154.47/22.66 % (3450100)Termination reason: Instruction limit % 154.47/22.66 % (3450100)Termination phase: Saturation % 154.47/22.66 % (3450100)Time elapsed: 1.524 s % 154.47/22.66 % (3450100)Peak memory usage: 120 MB % 154.47/22.66 % (3450100)Instructions burned: 2076 (million) % 154.47/22.66 % (3450108)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2656823809:i=5145:rtra=on_2847 on theBenchmark for (2847ds/5145Mi) % 154.47/22.66 % (3450094)Instruction limit reached! % 154.47/22.66 % (3450094)------------------------------ % 154.47/22.66 % (3450094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.47/22.66 % (3450094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.47/22.66 % (3450094)CaDiCaL version: 2.1.3 % 154.47/22.66 % (3450094)Termination reason: Instruction limit % 154.47/22.66 % (3450094)Termination phase: Saturation % 154.47/22.66 % (3450094)Time elapsed: 3.804 s % 154.47/22.66 % (3450094)Peak memory usage: 120 MB % 154.47/22.66 % (3450094)Instructions burned: 5452 (million) % 154.47/22.66 % (3450085)Instruction limit reached! % 154.47/22.66 % (3450085)------------------------------ % 154.47/22.66 % (3450085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.47/22.66 % (3450085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.33/33.49 % (3450085)CaDiCaL version: 2.1.3 % 231.33/33.49 % (3450085)Termination reason: Instruction limit % 231.33/33.49 % (3450085)Termination phase: Saturation % 231.33/33.49 % (3450085)Time elapsed: 4.827 s % 231.33/33.49 % (3450085)Peak memory usage: 107 MB % 231.33/33.49 % (3450085)Instructions burned: 13096 (million) % 231.33/33.49 % (3450095)Instruction limit reached! % 231.33/33.49 % (3450095)------------------------------ % 231.33/33.49 % (3450095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.33/33.49 % (3450095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.33/33.49 % (3450095)CaDiCaL version: 2.1.3 % 231.33/33.49 % (3450095)Termination reason: Instruction limit % 231.33/33.49 % (3450095)Termination phase: Saturation % 231.33/33.49 % (3450095)Time elapsed: 4.050 s % 231.33/33.49 % (3450095)Peak memory usage: 131 MB % 231.33/33.49 % (3450095)Instructions burned: 4976 (million) % 231.33/33.49 % (3450112)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4107756002:i=3509:rtra=on_2836 on theBenchmark for (2836ds/3509Mi) % 231.33/33.49 % (3450113)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=4072371601:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2834 on theBenchmark for (2834ds/13800Mi) % 231.33/33.49 % (3450113)Refutation not found, incomplete strategy % 231.33/33.49 % (3450113)------------------------------ % 231.33/33.49 % (3450113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.33/33.49 % (3450113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.33/33.49 % (3450113)CaDiCaL version: 2.1.3 % 231.33/33.49 % (3450113)Termination reason: Refutation not found, incomplete strategy % 231.33/33.49 % (3450113)Time elapsed: 0.028 s % 231.33/33.49 % (3450113)Peak memory usage: 87 MB % 231.33/33.49 % (3450113)Instructions burned: 70 (million) % 231.33/33.49 % (3450115)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4171409260:i=1412:rtra=on:fsd=on:proc=on_2833 on theBenchmark for (2833ds/1412Mi) % 231.33/33.49 % (3450113)------------------------------ % 231.33/33.49 % (3450113)------------------------------ % 231.33/33.49 % (3450118)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 % 231.33/33.49 % (3450118)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2520951177:i=11747:aac=none:nm=0:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/11747Mi) % 231.33/33.49 % (3450115)Instruction limit reached! % 231.33/33.49 % (3450115)------------------------------ % 231.33/33.49 % (3450115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.33/33.49 % (3450115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.33/33.49 % (3450115)CaDiCaL version: 2.1.3 % 231.33/33.49 % (3450115)Termination reason: Instruction limit % 231.33/33.49 % (3450115)Termination phase: Saturation % 231.33/33.49 % (3450115)Time elapsed: 1.047 s % 231.33/33.49 % (3450115)Peak memory usage: 119 MB % 231.33/33.49 % (3450115)Instructions burned: 1413 (million) % 231.33/33.49 % (3450120)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3220823122:s2a=on:i=3553:nm=0:rtra=on_2820 on theBenchmark for (2820ds/3553Mi) % 231.33/33.49 % (3450073)Instruction limit reached! % 231.33/33.49 % (3450073)------------------------------ % 231.33/33.49 % (3450073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.33/33.49 % (3450073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.33/33.49 % (3450073)CaDiCaL version: 2.1.3 % 231.33/33.49 % (3450073)Termination reason: Instruction limit % 231.33/33.49 % (3450073)Termination phase: Saturation % 231.33/33.49 % (3450073)Time elapsed: 8.605 s % 231.33/33.49 % (3450073)Peak memory usage: 165 MB % 231.33/33.49 % (3450073)Instructions burned: 10544 (million) % 231.33/33.49 % (3450112)Instruction limit reached! % 231.33/33.49 % (3450112)------------------------------ % 231.33/33.49 % (3450112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.33/33.49 % (3450112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.33/33.49 % (3450112)CaDiCaL version: 2.1.3 % 231.33/33.49 % (3450112)Termination reason: Instruction limit % 231.33/33.49 % (3450112)Termination phase: Saturation % 231.33/33.49 % (3450112)Time elapsed: 2.438 s % 231.33/33.49 % (3450112)Peak memory usage: 89 MB % 231.33/33.49 % (3450112)Instructions burned: 3510 (million) % 231.33/33.49 % (3450108)Instruction limit reached! % 231.33/33.49 % (3450108)------------------------------ % 231.33/33.49 % (3450108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.10/37.04 % (3450108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.10/37.04 % (3450108)CaDiCaL version: 2.1.3 % 257.10/37.04 % (3450108)Termination reason: Instruction limit % 257.10/37.04 % (3450108)Termination phase: Saturation % 257.10/37.04 % (3450108)Time elapsed: 3.589 s % 257.10/37.04 % (3450108)Peak memory usage: 95 MB % 257.10/37.04 % (3450108)Instructions burned: 5146 (million) % 257.10/37.04 % (3450125)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1487543527:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2811 on theBenchmark for (2811ds/3201Mi) % 257.10/37.04 % (3450128)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=3600103859:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2809 on theBenchmark for (2809ds/4081Mi) % 257.10/37.04 % (3450129)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=2172772980:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2808 on theBenchmark for (2808ds/20260Mi) % 257.10/37.04 % (3450129)Refutation not found, incomplete strategy % 257.10/37.04 % (3450129)------------------------------ % 257.10/37.04 % (3450129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.10/37.04 % (3450129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.10/37.04 % (3450129)CaDiCaL version: 2.1.3 % 257.10/37.04 % (3450129)Termination reason: Refutation not found, incomplete strategy % 257.10/37.04 % (3450129)Time elapsed: 0.070 s % 257.10/37.04 % (3450129)Peak memory usage: 112 MB % 257.10/37.04 % (3450129)Instructions burned: 41 (million) % 257.10/37.04 % (3450125)Refutation not found, incomplete strategy % 257.10/37.04 % (3450125)------------------------------ % 257.10/37.04 % (3450125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.10/37.04 % (3450125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.10/37.04 % (3450125)CaDiCaL version: 2.1.3 % 257.10/37.04 % (3450125)Termination reason: Refutation not found, incomplete strategy % 257.10/37.04 % (3450125)Time elapsed: 0.507 s % 257.10/37.04 % (3450125)Peak memory usage: 93 MB % 257.10/37.04 % (3450125)Instructions burned: 668 (million) % 257.10/37.04 % (3450129)------------------------------ % 257.10/37.04 % (3450129)------------------------------ % 257.10/37.04 % (3450125)------------------------------ % 257.10/37.04 % (3450125)------------------------------ % 257.10/37.04 % (3450134)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3666942590:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2802 on theBenchmark for (2802ds/58627Mi) % 257.10/37.04 % (3450137)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1412018337:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2799 on theBenchmark for (2799ds/6258Mi) % 257.10/37.04 % (3450120)Instruction limit reached! % 257.10/37.04 % (3450120)------------------------------ % 257.10/37.04 % (3450120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.10/37.04 % (3450120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.10/37.04 % (3450120)CaDiCaL version: 2.1.3 % 257.10/37.04 % (3450120)Termination reason: Instruction limit % 257.10/37.04 % (3450120)Termination phase: Saturation % 257.10/37.04 % (3450120)Time elapsed: 2.395 s % 257.10/37.04 % (3450120)Peak memory usage: 91 MB % 257.10/37.04 % (3450120)Instructions burned: 3554 (million) % 257.10/37.04 % (3450142)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2810176825:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2794 on theBenchmark for (2794ds/34001Mi) % 257.10/37.04 % (3450118)Instruction limit reached! % 257.10/37.04 % (3450118)------------------------------ % 257.10/37.04 % (3450118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.10/37.04 % (3450118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.10/37.04 % (3450118)CaDiCaL version: 2.1.3 % 257.10/37.04 % (3450118)Termination reason: Instruction limit % 257.10/37.04 % (3450118)Termination phase: Saturation % 257.10/37.04 % (3450118)Time elapsed: 4.524 s % 257.10/37.04 % (3450118)Peak memory usage: 123 MB % 257.10/37.04 % (3450118)Instructions burned: 11747 (million) % 257.10/37.04 % (3450149)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2552910540:s2a=on:i=71622:s2at=-1:rtra=on_2782 on theBenchmark for (2782ds/71622Mi) % 272.25/39.27 % (3450128)Instruction limit reached! % 272.25/39.27 % (3450128)------------------------------ % 272.25/39.27 % (3450128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.25/39.27 % (3450128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.25/39.27 % (3450128)CaDiCaL version: 2.1.3 % 272.25/39.27 % (3450128)Termination reason: Instruction limit % 272.25/39.27 % (3450128)Termination phase: Saturation % 272.25/39.27 % (3450128)Time elapsed: 2.860 s % 272.25/39.27 % (3450128)Peak memory usage: 132 MB % 272.25/39.27 % (3450128)Instructions burned: 4081 (million) % 272.25/39.27 % (3450153)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=878650305:i=24001:kws=precedence:nm=0:rtra=on_2778 on theBenchmark for (2778ds/24001Mi) % 272.25/39.27 % (3450084)Instruction limit reached! % 272.25/39.27 % (3450084)------------------------------ % 272.25/39.27 % (3450084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.25/39.27 % (3450084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.25/39.27 % (3450084)CaDiCaL version: 2.1.3 % 272.25/39.27 % (3450084)Termination reason: Instruction limit % 272.25/39.27 % (3450084)Termination phase: Saturation % 272.25/39.27 % (3450084)Time elapsed: 11.834 s % 272.25/39.27 % (3450084)Peak memory usage: 90 MB % 272.25/39.27 % (3450084)Instructions burned: 17165 (million) % 272.25/39.27 % (3450169)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=2548869113:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2765 on theBenchmark for (2765ds/2076Mi) % 272.25/39.27 % (3450137)Instruction limit reached! % 272.25/39.27 % (3450137)------------------------------ % 272.25/39.27 % (3450137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.25/39.27 % (3450137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.25/39.27 % (3450137)CaDiCaL version: 2.1.3 % 272.25/39.27 % (3450137)Termination reason: Instruction limit % 272.25/39.27 % (3450137)Termination phase: Saturation % 272.25/39.27 % (3450137)Time elapsed: 4.531 s % 272.25/39.27 % (3450137)Peak memory usage: 120 MB % 272.25/39.27 % (3450137)Instructions burned: 6258 (million) % 272.25/39.27 % (3450188)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3254907156:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2751 on theBenchmark for (2751ds/83971Mi) % 272.25/39.27 % (3450169)Instruction limit reached! % 272.25/39.27 % (3450169)------------------------------ % 272.25/39.27 % (3450169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.25/39.27 % (3450169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.25/39.27 % (3450169)CaDiCaL version: 2.1.3 % 272.25/39.27 % (3450169)Termination reason: Instruction limit % 272.25/39.27 % (3450169)Termination phase: Saturation % 272.25/39.27 % (3450169)Time elapsed: 1.475 s % 272.25/39.27 % (3450169)Peak memory usage: 119 MB % 272.25/39.27 % (3450169)Instructions burned: 2077 (million) % 272.25/39.27 % (3450194)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=681038268:i=83944:rtra=on_2748 on theBenchmark for (2748ds/83944Mi) % 272.25/39.27 % (3450043)Instruction limit reached! % 272.25/39.27 % (3450043)------------------------------ % 272.25/39.27 % (3450043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.25/39.27 % (3450043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.25/39.27 % (3450043)CaDiCaL version: 2.1.3 % 272.25/39.27 % (3450043)Termination reason: Instruction limit % 272.25/39.27 % (3450043)Termination phase: Saturation % 272.25/39.27 % (3450043)Time elapsed: 22.518 s % 272.25/39.27 % (3450043)Peak memory usage: 105 MB % 272.25/39.27 % (3450043)Instructions burned: 36818 (million) % 272.25/39.27 % (3450264)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3376011401:i=9201:rtra=on_2707 on theBenchmark for (2707ds/9201Mi) % 272.25/39.27 % (3450264)Instruction limit reached! % 272.25/39.27 % (3450264)------------------------------ % 272.25/39.27 % (3450264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.25/39.27 % (3450264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.25/39.27 % (3450264)CaDiCaL version: 2.1.3 % 272.25/39.27 % (3450264)Termination reason: Instruction limit % 272.25/39.27 % (3450264)Termination phase: Saturation % 272.25/39.27 % (3450264)Time elapsed: 3.371 s % 272.25/39.27 % (3450264)Peak memory usage: 90 MB % 272.25/39.27 % (3450264)Instructions burned: 9203 (million) % 283.80/40.90 % (3450267)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 % 283.80/40.90 % (3450267)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1823823911:i=6806:aac=none:nm=0:rtra=on:rawr=on_2672 on theBenchmark for (2672ds/6806Mi) % 283.80/40.90 % (3450153)Instruction limit reached! % 283.80/40.90 % (3450153)------------------------------ % 283.80/40.90 % (3450153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.80/40.90 % (3450153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.80/40.90 % (3450153)CaDiCaL version: 2.1.3 % 283.80/40.90 % (3450153)Termination reason: Instruction limit % 283.80/40.90 % (3450153)Termination phase: Saturation % 283.80/40.90 % (3450153)Time elapsed: 12.166 s % 283.80/40.90 % (3450153)Peak memory usage: 126 MB % 283.80/40.90 % (3450153)Instructions burned: 24002 (million) % 283.80/40.90 % (3450269)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1256575148:s2a=on:i=3553:nm=0:rtra=on_2653 on theBenchmark for (2653ds/3553Mi) % 283.80/40.90 % (3450267)Instruction limit reached! % 283.80/40.90 % (3450267)------------------------------ % 283.80/40.90 % (3450267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.80/40.90 % (3450267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.80/40.90 % (3450267)CaDiCaL version: 2.1.3 % 283.80/40.90 % (3450267)Termination reason: Instruction limit % 283.80/40.90 % (3450267)Termination phase: Saturation % 283.80/40.90 % (3450267)Time elapsed: 2.464 s % 283.80/40.90 % (3450267)Peak memory usage: 119 MB % 283.80/40.90 % (3450267)Instructions burned: 6808 (million) % 283.80/40.90 % (3450271)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=37918260:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2646 on theBenchmark for (2646ds/2064Mi) % 283.80/40.90 % (3450142)Instruction limit reached! % 283.80/40.90 % (3450142)------------------------------ % 283.80/40.90 % (3450142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.80/40.90 % (3450142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.80/40.90 % (3450142)CaDiCaL version: 2.1.3 % 283.80/40.90 % (3450142)Termination reason: Instruction limit % 283.80/40.90 % (3450142)Termination phase: Saturation % 283.80/40.90 % (3450142)Time elapsed: 14.890 s % 283.80/40.90 % (3450142)Peak memory usage: 92 MB % 283.80/40.90 % (3450142)Instructions burned: 34002 (million) % 283.80/40.90 % (3450273)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=1601498950:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2642 on theBenchmark for (2642ds/20260Mi) % 283.80/40.90 % (3450273)Refutation not found, incomplete strategy % 283.80/40.90 % (3450273)------------------------------ % 283.80/40.90 % (3450273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.80/40.90 % (3450273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.80/40.90 % (3450273)CaDiCaL version: 2.1.3 % 283.80/40.90 % (3450273)Termination reason: Refutation not found, incomplete strategy % 283.80/40.90 % (3450273)Time elapsed: 0.039 s % 283.80/40.90 % (3450273)Peak memory usage: 112 MB % 283.80/40.90 % (3450273)Instructions burned: 41 (million) % 283.80/40.90 % (3450269)Instruction limit reached! % 283.80/40.90 % (3450269)------------------------------ % 283.80/40.90 % (3450269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.80/40.90 % (3450269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.80/40.90 % (3450269)CaDiCaL version: 2.1.3 % 283.80/40.90 % (3450269)Termination reason: Instruction limit % 283.80/40.90 % (3450269)Termination phase: Saturation % 283.80/40.90 % (3450269)Time elapsed: 1.290 s % 283.80/40.90 % (3450269)Peak memory usage: 92 MB % 283.80/40.90 % (3450269)Instructions burned: 3553 (million) % 283.80/40.90 % (3450273)------------------------------ % 283.80/40.90 % (3450273)------------------------------ % 283.80/40.90 % (3450275)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1395404385:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2639 on theBenchmark for (2639ds/1244Mi) % 283.80/40.90 % (3450271)Instruction limit reached! % 283.80/40.90 % (3450271)------------------------------ % 291.57/42.00 % (3450271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.57/42.00 % (3450271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.57/42.00 % (3450271)CaDiCaL version: 2.1.3 % 291.57/42.00 % (3450271)Termination reason: Instruction limit % 291.57/42.00 % (3450271)Termination phase: Saturation % 291.57/42.00 % (3450271)Time elapsed: 0.789 s % 291.57/42.00 % (3450271)Peak memory usage: 132 MB % 291.57/42.00 % (3450271)Instructions burned: 2064 (million) % 291.57/42.00 % (3450276)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=4268369271:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2638 on theBenchmark for (2638ds/58261Mi) % 291.57/42.00 % (3450278)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 % 291.57/42.00 % (3450278)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4001631468:i=6806:aac=none:nm=0:rtra=on:rawr=on_2636 on theBenchmark for (2636ds/6806Mi) % 291.57/42.00 % (3450275)Instruction limit reached! % 291.57/42.00 % (3450275)------------------------------ % 291.57/42.00 % (3450275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.57/42.00 % (3450275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.57/42.00 % (3450275)CaDiCaL version: 2.1.3 % 291.57/42.00 % (3450275)Termination reason: Instruction limit % 291.57/42.00 % (3450275)Termination phase: Saturation % 291.57/42.00 % (3450275)Time elapsed: 0.480 s % 291.57/42.00 % (3450275)Peak memory usage: 119 MB % 291.57/42.00 % (3450275)Instructions burned: 1247 (million) % 291.57/42.00 % (3450281)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=681741925:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2632 on theBenchmark for (2632ds/4081Mi) % 291.57/42.00 % (3450149)Instruction limit reached! % 291.57/42.00 % (3450149)------------------------------ % 291.57/42.00 % (3450149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.57/42.00 % (3450149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.57/42.00 % (3450149)CaDiCaL version: 2.1.3 % 291.57/42.00 % (3450149)Termination reason: Instruction limit % 291.57/42.00 % (3450149)Termination phase: Saturation % 291.57/42.00 % (3450149)Time elapsed: 15.886 s % 291.57/42.00 % (3450149)Peak memory usage: 124 MB % 291.57/42.00 % (3450149)Instructions burned: 71624 (million) % 291.57/42.00 % (3450283)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1403987959:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2621 on theBenchmark for (2621ds/1701Mi) % 291.57/42.00 % (3450283)Instruction limit reached! % 291.57/42.00 % (3450283)------------------------------ % 291.57/42.00 % (3450283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.57/42.00 % (3450283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.57/42.00 % (3450283)CaDiCaL version: 2.1.3 % 291.57/42.00 % (3450283)Termination reason: Instruction limit % 291.57/42.00 % (3450283)Termination phase: Saturation % 291.57/42.00 % (3450283)Time elapsed: 0.343 s % 291.57/42.00 % (3450283)Peak memory usage: 119 MB % 291.57/42.00 % (3450283)Instructions burned: 1707 (million) % 291.57/42.00 % (3450281)Instruction limit reached! % 291.57/42.00 % (3450281)------------------------------ % 291.57/42.00 % (3450281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.57/42.00 % (3450281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.57/42.00 % (3450281)CaDiCaL version: 2.1.3 % 291.57/42.00 % (3450281)Termination reason: Instruction limit % 291.57/42.00 % (3450281)Termination phase: Saturation % 291.57/42.00 % (3450281)Time elapsed: 1.525 s % 291.57/42.00 % (3450281)Peak memory usage: 132 MB % 291.57/42.00 % (3450281)Instructions burned: 4082 (million) % 291.57/42.00 % (3450285)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=2792411476:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2617 on theBenchmark for (2617ds/57001Mi) % 291.57/42.00 % (3450286)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 % 296.41/42.68 % (3450286)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3161315446:i=8622:aac=none:nm=0:rtra=on:rawr=on_2616 on theBenchmark for (2616ds/8622Mi) % 296.41/42.68 % (3450278)Instruction limit reached! % 296.41/42.68 % (3450278)------------------------------ % 296.41/42.68 % (3450278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.41/42.68 % (3450278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.41/42.68 % (3450278)CaDiCaL version: 2.1.3 % 296.41/42.68 % (3450278)Termination reason: Instruction limit % 296.41/42.68 % (3450278)Termination phase: Saturation % 296.41/42.68 % (3450278)Time elapsed: 2.475 s % 296.41/42.68 % (3450278)Peak memory usage: 119 MB % 296.41/42.68 % (3450278)Instructions burned: 6808 (million) % 296.41/42.68 % (3450289)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2514928639:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2610 on theBenchmark for (2610ds/24Mi) % 296.41/42.68 % (3450289)Instruction limit reached! % 296.41/42.68 % (3450289)------------------------------ % 296.41/42.68 % (3450289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.41/42.68 % (3450289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.41/42.68 % (3450289)CaDiCaL version: 2.1.3 % 296.41/42.68 % (3450289)Termination reason: Instruction limit % 296.41/42.68 % (3450289)Termination phase: Property scanning % 296.41/42.68 % (3450289)Time elapsed: 0.009 s % 296.41/42.68 % (3450289)Peak memory usage: 85 MB % 296.41/42.68 % (3450289)Instructions burned: 26 (million) % 296.41/42.68 % (3450291)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2049648338:i=614:kws=precedence:nm=0:rtra=on_2608 on theBenchmark for (2608ds/614Mi) % 296.41/42.68 % (3450291)Instruction limit reached! % 296.41/42.68 % (3450291)------------------------------ % 296.41/42.68 % (3450291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.41/42.68 % (3450291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.41/42.68 % (3450291)CaDiCaL version: 2.1.3 % 296.41/42.68 % (3450291)Termination reason: Instruction limit % 296.41/42.68 % (3450291)Termination phase: Saturation % 296.41/42.68 % (3450291)Time elapsed: 0.251 s % 296.41/42.68 % (3450291)Peak memory usage: 118 MB % 296.41/42.68 % (3450291)Instructions burned: 616 (million) % 296.41/42.68 % (3450293)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2050389681:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2604 on theBenchmark for (2604ds/402Mi) % 296.41/42.68 % (3450293)Instruction limit reached! % 296.41/42.68 % (3450293)------------------------------ % 296.41/42.68 % (3450293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.41/42.68 % (3450293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.41/42.68 % (3450293)CaDiCaL version: 2.1.3 % 296.41/42.68 % (3450293)Termination reason: Instruction limit % 296.41/42.68 % (3450293)Termination phase: Saturation % 296.41/42.68 % (3450293)Time elapsed: 0.174 s % 296.41/42.68 % (3450293)Peak memory usage: 117 MB % 296.41/42.68 % (3450293)Instructions burned: 403 (million) % 296.41/42.68 % (3450295)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1452171271:s2a=on:i=14:rtra=on:inst=on_2601 on theBenchmark for (2601ds/14Mi) % 296.41/42.68 % (3450295)Instruction limit reached! % 296.41/42.68 % (3450295)------------------------------ % 296.41/42.68 % (3450295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.41/42.68 % (3450295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.41/42.68 % (3450295)CaDiCaL version: 2.1.3 % 296.41/42.68 % (3450295)Termination reason: Instruction limit % 296.41/42.68 % (3450295)Termination phase: Property scanning % 296.41/42.68 % (3450295)Time elapsed: 0.006 s % 296.41/42.68 % (3450295)Peak memory usage: 85 MB % 296.41/42.68 % (3450295)Instructions burned: 16 (million) % 296.41/42.68 % (3450297)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3819602737:i=8:rtra=on_2599 on theBenchmark for (2599ds/8Mi) % 296.41/42.68 % (3450297)Instruction limit reached! % 296.41/42.68 % (3450297)------------------------------ % 296.41/42.68 % (3450297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.41/42.68 % (3450297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.41/42.68 % (3450297)CaDiCaL version: 2.1.3 % 296.41/42.68 % (3450297)Termination reason: Instruction limit % 296.41/42.68 % (3450297)TeTerminated %------------------------------------------------------------------------------