%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW601_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:54 PM UTC 2026 % Result : Timeout 300.27s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW601_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.24 % Computer : n026.cluster.edu % 0.10/0.24 % Model : x86_64 x86_64 % 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.24 % Memory : 8046.5625MB % 0.10/0.24 % OS : Linux 6.8.0-71-generic % 0.10/0.24 % CPULimit : 300 % 0.10/0.24 % WCLimit : 300 % 0.10/0.24 % DateTime : Mon Sep 28 14:23:56 UTC 2026 % 0.10/0.24 % CPUTime : % 0.10/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.23/0.29 Running first-order theorem proving % 0.23/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.00/1.74 % (3881160)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 5.00/1.74 % (3881170)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1313569378:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 5.00/1.74 % (3881170)Instruction limit reached! % 5.00/1.74 % (3881170)------------------------------ % 5.00/1.74 % (3881170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.74 % (3881170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.74 % (3881170)CaDiCaL version: 2.1.3 % 5.00/1.74 % (3881170)Termination reason: Instruction limit % 5.00/1.74 % (3881170)Termination phase: Saturation % 5.00/1.74 % (3881170)Time elapsed: 0.049 s % 5.00/1.74 % (3881170)Peak memory usage: 116 MB % 5.00/1.74 % (3881170)Instructions burned: 47 (million) % 5.00/1.74 % (3881167)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3292903827:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 5.00/1.74 % (3881168)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1024089092:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 5.00/1.74 % (3881165)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1924801196:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 5.00/1.74 % (3881166)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2142015417:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 5.00/1.74 % (3881168)Instruction limit reached! % 5.00/1.74 % (3881168)------------------------------ % 5.00/1.74 % (3881168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.74 % (3881168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.74 % (3881168)CaDiCaL version: 2.1.3 % 5.00/1.74 % (3881168)Termination reason: Instruction limit % 5.00/1.74 % (3881168)Termination phase: Saturation % 5.00/1.74 % (3881168)Time elapsed: 0.008 s % 5.00/1.74 % (3881168)Peak memory usage: 86 MB % 5.00/1.74 % (3881168)Instructions burned: 8 (million) % 5.00/1.74 % (3881169)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3329318089:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 5.00/1.74 % (3881169)Instruction limit reached! % 5.00/1.74 % (3881169)------------------------------ % 5.00/1.74 % (3881169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.74 % (3881169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.74 % (3881169)CaDiCaL version: 2.1.3 % 5.00/1.74 % (3881169)Termination reason: Instruction limit % 5.00/1.74 % (3881169)Termination phase: Preprocessing 3 % 5.00/1.74 % (3881169)Time elapsed: 0.005 s % 5.00/1.74 % (3881169)Peak memory usage: 86 MB % 5.00/1.74 % (3881169)Instructions burned: 4 (million) % 5.00/1.74 % (3881171)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3539095267:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 5.00/1.74 % (3881165)Instruction limit reached! % 5.00/1.74 % (3881165)------------------------------ % 5.00/1.74 % (3881165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.74 % (3881165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.74 % (3881165)CaDiCaL version: 2.1.3 % 5.00/1.74 % (3881165)Termination reason: Instruction limit % 5.00/1.74 % (3881165)Termination phase: Saturation % 5.00/1.74 % (3881165)Time elapsed: 0.040 s % 5.00/1.74 % (3881165)Peak memory usage: 112 MB % 5.00/1.74 % (3881165)Instructions burned: 12 (million) % 5.00/1.74 % (3881171)Instruction limit reached! % 5.00/1.74 % (3881171)------------------------------ % 5.00/1.74 % (3881171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.00/1.74 % (3881171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.00/1.74 % (3881171)CaDiCaL version: 2.1.3 % 5.00/1.74 % (3881171)Termination reason: Instruction limit % 5.00/1.74 % (3881171)Termination phase: Saturation % 5.00/1.74 % (3881171)Time elapsed: 0.067 s % 5.00/1.74 % (3881171)Peak memory usage: 116 MB % 5.00/1.74 % (3881171)Instructions burned: 33 (million) % 5.00/1.74 % (3881173)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1828769458:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi) % 5.00/1.74 % (3881173)Instruction limit reached! % 5.00/1.74 % (3881173)------------------------------ % 6.61/1.99 % (3881173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.99 % (3881173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.99 % (3881173)CaDiCaL version: 2.1.3 % 6.61/1.99 % (3881173)Termination reason: Instruction limit % 6.61/1.99 % (3881173)Termination phase: Saturation % 6.61/1.99 % (3881173)Time elapsed: 0.009 s % 6.61/1.99 % (3881173)Peak memory usage: 88 MB % 6.61/1.99 % (3881173)Instructions burned: 15 (million) % 6.61/1.99 % (3881182)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1420616869:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 6.61/1.99 % (3881179)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=3204480311:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi) % 6.61/1.99 % (3881167)Instruction limit reached! % 6.61/1.99 % (3881167)------------------------------ % 6.61/1.99 % (3881167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.99 % (3881167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.99 % (3881167)CaDiCaL version: 2.1.3 % 6.61/1.99 % (3881167)Termination reason: Instruction limit % 6.61/1.99 % (3881167)Termination phase: Saturation % 6.61/1.99 % (3881167)Time elapsed: 0.233 s % 6.61/1.99 % (3881167)Peak memory usage: 119 MB % 6.61/1.99 % (3881167)Instructions burned: 201 (million) % 6.61/1.99 % (3881182)Instruction limit reached! % 6.61/1.99 % (3881182)------------------------------ % 6.61/1.99 % (3881182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.99 % (3881182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.99 % (3881182)CaDiCaL version: 2.1.3 % 6.61/1.99 % (3881182)Termination reason: Instruction limit % 6.61/1.99 % (3881182)Termination phase: Saturation % 6.61/1.99 % (3881182)Time elapsed: 0.029 s % 6.61/1.99 % (3881182)Peak memory usage: 89 MB % 6.61/1.99 % (3881182)Instructions burned: 24 (million) % 6.61/1.99 % (3881181)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2826288452:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi) % 6.61/1.99 % (3881181)Instruction limit reached! % 6.61/1.99 % (3881181)------------------------------ % 6.61/1.99 % (3881181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.99 % (3881181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.99 % (3881181)CaDiCaL version: 2.1.3 % 6.61/1.99 % (3881181)Termination reason: Instruction limit % 6.61/1.99 % (3881181)Termination phase: Saturation % 6.61/1.99 % (3881181)Time elapsed: 0.018 s % 6.61/1.99 % (3881181)Peak memory usage: 88 MB % 6.61/1.99 % (3881181)Instructions burned: 16 (million) % 6.61/1.99 % (3881179)Instruction limit reached! % 6.61/1.99 % (3881179)------------------------------ % 6.61/1.99 % (3881179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.99 % (3881179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.99 % (3881179)CaDiCaL version: 2.1.3 % 6.61/1.99 % (3881179)Termination reason: Instruction limit % 6.61/1.99 % (3881179)Termination phase: Saturation % 6.61/1.99 % (3881179)Time elapsed: 0.035 s % 6.61/1.99 % (3881179)Peak memory usage: 89 MB % 6.61/1.99 % (3881179)Instructions burned: 29 (million) % 6.61/1.99 % (3881185)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2378660914:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi) % 6.61/1.99 % (3881183)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=1270157625:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi) % 6.61/1.99 % (3881183)Instruction limit reached! % 6.61/1.99 % (3881183)------------------------------ % 6.61/1.99 % (3881183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.99 % (3881183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.99 % (3881183)CaDiCaL version: 2.1.3 % 6.61/1.99 % (3881183)Termination reason: Instruction limit % 6.61/1.99 % (3881183)Termination phase: Saturation % 6.61/1.99 % (3881183)Time elapsed: 0.029 s % 6.61/1.99 % (3881183)Peak memory usage: 89 MB % 6.61/1.99 % (3881183)Instructions burned: 27 (million) % 6.61/1.99 % (3881185)Instruction limit reached! % 6.61/1.99 % (3881185)------------------------------ % 6.61/1.99 % (3881185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.71/2.23 % (3881185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.71/2.23 % (3881185)CaDiCaL version: 2.1.3 % 8.71/2.23 % (3881185)Termination reason: Instruction limit % 8.71/2.23 % (3881185)Termination phase: Saturation % 8.71/2.23 % (3881185)Time elapsed: 0.038 s % 8.71/2.23 % (3881185)Peak memory usage: 89 MB % 8.71/2.23 % (3881185)Instructions burned: 87 (million) % 8.71/2.23 % (3881166)Instruction limit reached! % 8.71/2.23 % (3881166)------------------------------ % 8.71/2.23 % (3881166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.71/2.23 % (3881166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.71/2.23 % (3881166)CaDiCaL version: 2.1.3 % 8.71/2.23 % (3881166)Termination reason: Instruction limit % 8.71/2.23 % (3881166)Termination phase: Saturation % 8.71/2.23 % (3881166)Time elapsed: 0.382 s % 8.71/2.23 % (3881166)Peak memory usage: 117 MB % 8.71/2.23 % (3881166)Instructions burned: 307 (million) % 8.71/2.23 % (3881190)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3956562227:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi) % 8.71/2.23 % (3881189)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2902316424:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi) % 8.71/2.23 % (3881189)Instruction limit reached! % 8.71/2.23 % (3881189)------------------------------ % 8.71/2.23 % (3881189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.71/2.23 % (3881189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.71/2.23 % (3881189)CaDiCaL version: 2.1.3 % 8.71/2.23 % (3881189)Termination reason: Instruction limit % 8.71/2.23 % (3881189)Termination phase: Preprocessing 1 % 8.71/2.23 % (3881189)Time elapsed: 0.003 s % 8.71/2.23 % (3881189)Peak memory usage: 85 MB % 8.71/2.23 % (3881189)Instructions burned: 3 (million) % 8.71/2.23 % (3881191)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1378428796:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi) % 8.71/2.23 % (3881192)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=90927274:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi) % 8.71/2.23 % (3881191)Instruction limit reached! % 8.71/2.23 % (3881191)------------------------------ % 8.71/2.23 % (3881191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.71/2.23 % (3881191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.71/2.23 % (3881191)CaDiCaL version: 2.1.3 % 8.71/2.23 % (3881191)Termination reason: Instruction limit % 8.71/2.23 % (3881191)Termination phase: Preprocessing 3 % 8.71/2.23 % (3881191)Time elapsed: 0.005 s % 8.71/2.23 % (3881191)Peak memory usage: 86 MB % 8.71/2.23 % (3881191)Instructions burned: 4 (million) % 8.71/2.23 % (3881196)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=1775098536:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi) % 8.71/2.23 % (3881196)Instruction limit reached! % 8.71/2.23 % (3881196)------------------------------ % 8.71/2.23 % (3881196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.71/2.23 % (3881196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.71/2.23 % (3881196)CaDiCaL version: 2.1.3 % 8.71/2.23 % (3881196)Termination reason: Instruction limit % 8.71/2.23 % (3881196)Termination phase: Equality proxy % 8.71/2.23 % (3881196)Time elapsed: 0.006 s % 8.71/2.23 % (3881196)Peak memory usage: 87 MB % 8.71/2.23 % (3881196)Instructions burned: 10 (million) % 8.71/2.23 % (3881195)lrs+10_1_thi=all:si=on:fd=off:random_seed=1067320776:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi) % 8.71/2.23 % (3881197)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3688838534:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi) % 8.71/2.23 % (3881197)Instruction limit reached! % 8.71/2.23 % (3881197)------------------------------ % 8.71/2.23 % (3881197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.71/2.23 % (3881197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.71/2.23 % (3881197)CaDiCaL version: 2.1.3 % 8.71/2.23 % (3881197)Termination reason: Instruction limit % 8.71/2.23 % (3881197)Termination phase: Unused predicate definition removal % 10.21/2.51 % (3881197)Time elapsed: 0.003 s % 10.21/2.51 % (3881197)Peak memory usage: 85 MB % 10.21/2.51 % (3881197)Instructions burned: 2 (million) % 10.21/2.51 % (3881192)Instruction limit reached! % 10.21/2.51 % (3881192)------------------------------ % 10.21/2.51 % (3881192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.51 % (3881192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.51 % (3881192)CaDiCaL version: 2.1.3 % 10.21/2.51 % (3881192)Termination reason: Instruction limit % 10.21/2.51 % (3881192)Termination phase: Saturation % 10.21/2.51 % (3881192)Time elapsed: 0.134 s % 10.21/2.51 % (3881192)Peak memory usage: 134 MB % 10.21/2.51 % (3881192)Instructions burned: 66 (million) % 10.21/2.51 % (3881195)Instruction limit reached! % 10.21/2.51 % (3881195)------------------------------ % 10.21/2.51 % (3881195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.51 % (3881195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.51 % (3881195)CaDiCaL version: 2.1.3 % 10.21/2.51 % (3881195)Termination reason: Instruction limit % 10.21/2.51 % (3881195)Termination phase: Saturation % 10.21/2.51 % (3881195)Time elapsed: 0.091 s % 10.21/2.51 % (3881195)Peak memory usage: 118 MB % 10.21/2.51 % (3881195)Instructions burned: 53 (million) % 10.21/2.51 % (3881190)Instruction limit reached! % 10.21/2.51 % (3881190)------------------------------ % 10.21/2.51 % (3881190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.51 % (3881190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.51 % (3881190)CaDiCaL version: 2.1.3 % 10.21/2.51 % (3881190)Termination reason: Instruction limit % 10.21/2.51 % (3881190)Termination phase: Saturation % 10.21/2.51 % (3881190)Time elapsed: 0.198 s % 10.21/2.51 % (3881190)Peak memory usage: 91 MB % 10.21/2.51 % (3881190)Instructions burned: 182 (million) % 10.21/2.51 % (3881205)dis+10_1_si=on:random_seed=3596342205:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 10.21/2.51 % (3881200)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2775729376:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi) % 10.21/2.51 % (3881205)Instruction limit reached! % 10.21/2.51 % (3881205)------------------------------ % 10.21/2.51 % (3881205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.51 % (3881205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.51 % (3881205)CaDiCaL version: 2.1.3 % 10.21/2.51 % (3881205)Termination reason: Instruction limit % 10.21/2.51 % (3881205)Termination phase: Saturation % 10.21/2.51 % (3881205)Time elapsed: 0.012 s % 10.21/2.51 % (3881205)Peak memory usage: 88 MB % 10.21/2.51 % (3881205)Instructions burned: 11 (million) % 10.21/2.51 % (3881200)Instruction limit reached! % 10.21/2.51 % (3881200)------------------------------ % 10.21/2.51 % (3881200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.51 % (3881200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.51 % (3881200)CaDiCaL version: 2.1.3 % 10.21/2.51 % (3881200)Termination reason: Instruction limit % 10.21/2.51 % (3881200)Termination phase: Preprocessing 1 % 10.21/2.51 % (3881200)Time elapsed: 0.003 s % 10.21/2.51 % (3881200)Peak memory usage: 85 MB % 10.21/2.51 % (3881200)Instructions burned: 3 (million) % 10.21/2.51 % (3881203)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=463911439:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi) % 10.21/2.51 % (3881208)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1319138111:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi) % 10.21/2.51 % (3881208)Refutation not found, incomplete strategy % 10.21/2.51 % (3881208)------------------------------ % 10.21/2.51 % (3881208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.21/2.51 % (3881208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.21/2.51 % (3881208)CaDiCaL version: 2.1.3 % 10.21/2.51 % (3881208)Termination reason: Refutation not found, incomplete strategy % 10.21/2.51 % (3881208)Time elapsed: 0.008 s % 10.21/2.51 % (3881208)Peak memory usage: 89 MB % 10.21/2.51 % (3881208)Instructions burned: 14 (million) % 10.21/2.51 % (3881214)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3570895267:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi) % 10.21/2.51 % (3881209)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1710262020:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi) % 11.56/2.84 % (3881211)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4115762837:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 11.56/2.84 % (3881211)Instruction limit reached! % 11.56/2.84 % (3881211)------------------------------ % 11.56/2.84 % (3881211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.84 % (3881211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.84 % (3881211)CaDiCaL version: 2.1.3 % 11.56/2.84 % (3881211)Termination reason: Instruction limit % 11.56/2.84 % (3881211)Termination phase: Equality resolution with deletion % 11.56/2.84 % (3881211)Time elapsed: 0.007 s % 11.56/2.84 % (3881211)Peak memory usage: 86 MB % 11.56/2.84 % (3881211)Instructions burned: 6 (million) % 11.56/2.84 % (3881212)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1270615691:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi) % 11.56/2.84 % (3881209)Instruction limit reached! % 11.56/2.84 % (3881209)------------------------------ % 11.56/2.84 % (3881209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.84 % (3881209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.84 % (3881209)CaDiCaL version: 2.1.3 % 11.56/2.84 % (3881209)Termination reason: Instruction limit % 11.56/2.84 % (3881209)Termination phase: Saturation % 11.56/2.84 % (3881209)Time elapsed: 0.042 s % 11.56/2.84 % (3881209)Peak memory usage: 89 MB % 11.56/2.84 % (3881209)Instructions burned: 35 (million) % 11.56/2.84 % (3881212)Instruction limit reached! % 11.56/2.84 % (3881212)------------------------------ % 11.56/2.84 % (3881212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.84 % (3881212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.84 % (3881212)CaDiCaL version: 2.1.3 % 11.56/2.84 % (3881212)Termination reason: Instruction limit % 11.56/2.84 % (3881212)Termination phase: Saturation % 11.56/2.84 % (3881212)Time elapsed: 0.009 s % 11.56/2.84 % (3881212)Peak memory usage: 88 MB % 11.56/2.84 % (3881212)Instructions burned: 8 (million) % 11.56/2.84 % (3881203)Instruction limit reached! % 11.56/2.84 % (3881203)------------------------------ % 11.56/2.84 % (3881203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.84 % (3881203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.84 % (3881203)CaDiCaL version: 2.1.3 % 11.56/2.84 % (3881203)Termination reason: Instruction limit % 11.56/2.84 % (3881203)Termination phase: Saturation % 11.56/2.84 % (3881203)Time elapsed: 0.189 s % 11.56/2.84 % (3881203)Peak memory usage: 117 MB % 11.56/2.84 % (3881203)Instructions burned: 127 (million) % 11.56/2.84 % (3881215)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3864504225:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi) % 11.56/2.84 % (3881215)Instruction limit reached! % 11.56/2.84 % (3881215)------------------------------ % 11.56/2.84 % (3881215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.84 % (3881215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.84 % (3881215)CaDiCaL version: 2.1.3 % 11.56/2.84 % (3881215)Termination reason: Instruction limit % 11.56/2.84 % (3881215)Termination phase: Saturation % 11.56/2.84 % (3881215)Time elapsed: 0.039 s % 11.56/2.84 % (3881215)Peak memory usage: 110 MB % 11.56/2.84 % (3881215)Instructions burned: 13 (million) % 11.56/2.84 % (3881208)------------------------------ % 11.56/2.84 % (3881208)------------------------------ % 11.56/2.84 % (3881223)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1632754607:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 11.56/2.84 % (3881223)Instruction limit reached! % 11.56/2.84 % (3881223)------------------------------ % 11.56/2.84 % (3881223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.56/2.84 % (3881223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.56/2.84 % (3881223)CaDiCaL version: 2.1.3 % 11.56/2.84 % (3881223)Termination reason: Instruction limit % 11.56/2.84 % (3881223)Termination phase: Saturation % 11.56/2.84 % (3881223)Time elapsed: 0.013 s % 11.56/2.84 % (3881223)Peak memory usage: 88 MB % 11.56/2.84 % (3881223)Instructions burned: 10 (million) % 15.75/3.21 % (3881222)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3398997194:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 15.75/3.21 % (3881228)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=733800094:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 15.75/3.21 % (3881225)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=729163828:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi) % 15.75/3.21 % (3881226)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=763965570:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 15.75/3.21 % (3881214)Instruction limit reached! % 15.75/3.21 % (3881214)------------------------------ % 15.75/3.21 % (3881214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.75/3.21 % (3881214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/3.21 % (3881214)CaDiCaL version: 2.1.3 % 15.75/3.21 % (3881214)Termination reason: Instruction limit % 15.75/3.21 % (3881214)Termination phase: Saturation % 15.75/3.21 % (3881214)Time elapsed: 0.323 s % 15.75/3.21 % (3881214)Peak memory usage: 92 MB % 15.75/3.21 % (3881214)Instructions burned: 371 (million) % 15.75/3.21 % (3881227)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=1056776301:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 15.75/3.21 % (3881226)Instruction limit reached! % 15.75/3.21 % (3881226)------------------------------ % 15.75/3.21 % (3881226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.75/3.21 % (3881226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/3.21 % (3881226)CaDiCaL version: 2.1.3 % 15.75/3.21 % (3881226)Termination reason: Instruction limit % 15.75/3.21 % (3881226)Termination phase: Saturation % 15.75/3.21 % (3881226)Time elapsed: 0.063 s % 15.75/3.21 % (3881226)Peak memory usage: 91 MB % 15.75/3.21 % (3881226)Instructions burned: 75 (million) % 15.75/3.21 % (3881230)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=73546400:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 15.75/3.21 % (3881225)Instruction limit reached! % 15.75/3.21 % (3881225)------------------------------ % 15.75/3.21 % (3881225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.75/3.21 % (3881225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/3.21 % (3881225)CaDiCaL version: 2.1.3 % 15.75/3.21 % (3881225)Termination reason: Instruction limit % 15.75/3.21 % (3881225)Termination phase: Saturation % 15.75/3.21 % (3881225)Time elapsed: 0.136 s % 15.75/3.21 % (3881225)Peak memory usage: 133 MB % 15.75/3.21 % (3881225)Instructions burned: 71 (million) % 15.75/3.21 % (3881228)Instruction limit reached! % 15.75/3.21 % (3881228)------------------------------ % 15.75/3.21 % (3881228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.75/3.21 % (3881228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/3.21 % (3881228)CaDiCaL version: 2.1.3 % 15.75/3.21 % (3881228)Termination reason: Instruction limit % 15.75/3.21 % (3881228)Termination phase: Saturation % 15.75/3.21 % (3881228)Time elapsed: 0.167 s % 15.75/3.21 % (3881228)Peak memory usage: 117 MB % 15.75/3.21 % (3881228)Instructions burned: 130 (million) % 15.75/3.21 % (3881230)Instruction limit reached! % 15.75/3.21 % (3881230)------------------------------ % 15.75/3.21 % (3881230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.75/3.21 % (3881230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/3.21 % (3881230)CaDiCaL version: 2.1.3 % 15.75/3.21 % (3881230)Termination reason: Instruction limit % 15.75/3.21 % (3881230)Termination phase: Saturation % 15.75/3.21 % (3881230)Time elapsed: 0.111 s % 15.75/3.21 % (3881230)Peak memory usage: 134 MB % 15.75/3.21 % (3881230)Instructions burned: 131 (million) % 15.75/3.21 % (3881222)Instruction limit reached! % 15.75/3.21 % (3881222)------------------------------ % 15.75/3.21 % (3881222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.75/3.21 % (3881222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/3.21 % (3881222)CaDiCaL version: 2.1.3 % 15.75/3.21 % (3881222)Termination reason: Instruction limit % 18.31/3.76 % (3881222)Termination phase: Saturation % 18.31/3.76 % (3881222)Time elapsed: 0.267 s % 18.31/3.76 % (3881222)Peak memory usage: 120 MB % 18.31/3.76 % (3881222)Instructions burned: 226 (million) % 18.31/3.76 % (3881239)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2384883273:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi) % 18.31/3.76 % (3881236)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3904458682:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi) % 18.31/3.76 % (3881241)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2855933081:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi) % 18.31/3.76 % (3881227)Instruction limit reached! % 18.31/3.76 % (3881227)------------------------------ % 18.31/3.76 % (3881227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.76 % (3881227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.76 % (3881227)CaDiCaL version: 2.1.3 % 18.31/3.76 % (3881227)Termination reason: Instruction limit % 18.31/3.76 % (3881227)Termination phase: Saturation % 18.31/3.76 % (3881227)Time elapsed: 0.316 s % 18.31/3.76 % (3881227)Peak memory usage: 91 MB % 18.31/3.76 % (3881227)Instructions burned: 294 (million) % 18.31/3.76 % (3881236)Instruction limit reached! % 18.31/3.76 % (3881236)------------------------------ % 18.31/3.76 % (3881236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.76 % (3881236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.76 % (3881236)CaDiCaL version: 2.1.3 % 18.31/3.76 % (3881236)Termination reason: Instruction limit % 18.31/3.76 % (3881236)Termination phase: Saturation % 18.31/3.76 % (3881236)Time elapsed: 0.100 s % 18.31/3.76 % (3881236)Peak memory usage: 133 MB % 18.31/3.76 % (3881236)Instructions burned: 40 (million) % 18.31/3.76 % (3881243)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=2456574451:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi) % 18.31/3.76 % (3881242)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1082484224:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi) % 18.31/3.76 % (3881246)dis+10_1_si=on:random_seed=4266718083:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi) % 18.31/3.76 % (3881251)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3472111076:i=383:fsr=off:rtra=on:ev=force_2983 on theBenchmark for (2983ds/383Mi) % 18.31/3.76 % (3881243)Instruction limit reached! % 18.31/3.76 % (3881243)------------------------------ % 18.31/3.76 % (3881243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.76 % (3881243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.76 % (3881243)CaDiCaL version: 2.1.3 % 18.31/3.76 % (3881243)Termination reason: Instruction limit % 18.31/3.76 % (3881243)Termination phase: Saturation % 18.31/3.76 % (3881243)Time elapsed: 0.169 s % 18.31/3.76 % (3881243)Peak memory usage: 119 MB % 18.31/3.76 % (3881243)Instructions burned: 260 (million) % 18.31/3.76 % (3881242)Instruction limit reached! % 18.31/3.76 % (3881242)------------------------------ % 18.31/3.76 % (3881242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.76 % (3881242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.76 % (3881242)CaDiCaL version: 2.1.3 % 18.31/3.76 % (3881242)Termination reason: Instruction limit % 18.31/3.76 % (3881242)Termination phase: Saturation % 18.31/3.76 % (3881242)Time elapsed: 0.172 s % 18.31/3.76 % (3881242)Peak memory usage: 119 MB % 18.31/3.76 % (3881242)Instructions burned: 131 (million) % 18.31/3.76 % (3881239)Instruction limit reached! % 18.31/3.76 % (3881239)------------------------------ % 18.31/3.76 % (3881239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.31/3.76 % (3881239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/3.76 % (3881239)CaDiCaL version: 2.1.3 % 18.31/3.76 % (3881239)Termination reason: Instruction limit % 18.31/3.76 % (3881239)Termination phase: Saturation % 18.31/3.76 % (3881239)Time elapsed: 0.300 s % 18.31/3.76 % (3881239)Peak memory usage: 92 MB % 18.31/3.76 % (3881239)Instructions burned: 307 (million) % 18.31/3.76 % (3881252)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1087608318:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi) % 23.01/4.21 % (3881259)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1036912429:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi) % 23.01/4.21 % (3881241)Instruction limit reached! % 23.01/4.21 % (3881241)------------------------------ % 23.01/4.21 % (3881241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.01/4.21 % (3881241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.01/4.21 % (3881241)CaDiCaL version: 2.1.3 % 23.01/4.21 % (3881241)Termination reason: Instruction limit % 23.01/4.21 % (3881241)Termination phase: Saturation % 23.01/4.21 % (3881241)Time elapsed: 0.419 s % 23.01/4.21 % (3881241)Peak memory usage: 137 MB % 23.01/4.21 % (3881241)Instructions burned: 599 (million) % 23.01/4.21 % (3881252)Instruction limit reached! % 23.01/4.21 % (3881252)------------------------------ % 23.01/4.21 % (3881252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.01/4.21 % (3881252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.01/4.21 % (3881252)CaDiCaL version: 2.1.3 % 23.01/4.21 % (3881252)Termination reason: Instruction limit % 23.01/4.21 % (3881252)Termination phase: Saturation % 23.01/4.21 % (3881252)Time elapsed: 0.161 s % 23.01/4.21 % (3881252)Peak memory usage: 90 MB % 23.01/4.21 % (3881252)Instructions burned: 141 (million) % 23.01/4.21 % (3881258)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3642603574:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi) % 23.01/4.21 % (3881260)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=1054080753:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi) % 23.01/4.21 % (3881259)Instruction limit reached! % 23.01/4.21 % (3881259)------------------------------ % 23.01/4.21 % (3881259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.01/4.21 % (3881259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.01/4.21 % (3881259)CaDiCaL version: 2.1.3 % 23.01/4.21 % (3881259)Termination reason: Instruction limit % 23.01/4.21 % (3881259)Termination phase: Saturation % 23.01/4.21 % (3881259)Time elapsed: 0.085 s % 23.01/4.21 % (3881259)Peak memory usage: 90 MB % 23.01/4.21 % (3881259)Instructions burned: 121 (million) % 23.01/4.21 % (3881258)Refutation not found, incomplete strategy % 23.01/4.21 % (3881258)------------------------------ % 23.01/4.21 % (3881258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.01/4.21 % (3881258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.01/4.21 % (3881258)CaDiCaL version: 2.1.3 % 23.01/4.21 % (3881258)Termination reason: Refutation not found, incomplete strategy % 23.01/4.21 % (3881258)Time elapsed: 0.054 s % 23.01/4.21 % (3881258)Peak memory usage: 116 MB % 23.01/4.21 % (3881258)Instructions burned: 19 (million) % 23.01/4.21 % (3881267)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2910975192:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/329Mi) % 23.01/4.21 % (3881263)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=4052891819:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi) % 23.01/4.21 % (3881260)Instruction limit reached! % 23.01/4.21 % (3881260)------------------------------ % 23.01/4.21 % (3881260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.01/4.21 % (3881260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.01/4.21 % (3881260)CaDiCaL version: 2.1.3 % 23.01/4.21 % (3881260)Termination reason: Instruction limit % 23.01/4.21 % (3881260)Termination phase: Saturation % 23.01/4.21 % (3881260)Time elapsed: 0.166 s % 23.01/4.21 % (3881260)Peak memory usage: 117 MB % 23.01/4.21 % (3881260)Instructions burned: 128 (million) % 23.01/4.21 % (3881251)Instruction limit reached! % 23.01/4.21 % (3881251)------------------------------ % 23.01/4.21 % (3881251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.01/4.21 % (3881251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.01/4.21 % (3881251)CaDiCaL version: 2.1.3 % 23.01/4.21 % (3881251)Termination reason: Instruction limit % 23.01/4.21 % (3881251)Termination phase: Saturation % 23.01/4.21 % (3881251)Time elapsed: 0.414 s % 23.01/4.21 % (3881251)Peak memory usage: 95 MB % 25.31/4.73 % (3881251)Instructions burned: 383 (million) % 25.31/4.73 % (3881265)dis+1010_1_to=kbo:si=on:random_seed=2823539057:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi) % 25.31/4.73 % (3881263)Instruction limit reached! % 25.31/4.73 % (3881263)------------------------------ % 25.31/4.73 % (3881263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.31/4.73 % (3881263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.31/4.73 % (3881263)CaDiCaL version: 2.1.3 % 25.31/4.73 % (3881263)Termination reason: Instruction limit % 25.31/4.73 % (3881263)Termination phase: Saturation % 25.31/4.73 % (3881263)Time elapsed: 0.077 s % 25.31/4.73 % (3881263)Peak memory usage: 116 MB % 25.31/4.73 % (3881263)Instructions burned: 39 (million) % 25.31/4.73 % (3881271)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2666065319:thitd=on:i=215:nm=0:rtra=on:ev=force_2977 on theBenchmark for (2977ds/215Mi) % 25.31/4.73 % (3881267)Instruction limit reached! % 25.31/4.73 % (3881267)------------------------------ % 25.31/4.73 % (3881267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.31/4.73 % (3881267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.31/4.73 % (3881267)CaDiCaL version: 2.1.3 % 25.31/4.73 % (3881267)Termination reason: Instruction limit % 25.31/4.73 % (3881267)Termination phase: Saturation % 25.31/4.73 % (3881267)Time elapsed: 0.201 s % 25.31/4.73 % (3881267)Peak memory usage: 119 MB % 25.31/4.73 % (3881267)Instructions burned: 329 (million) % 25.31/4.73 % (3881270)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3962362376:s2a=on:i=483:doe=on:nm=32:rtra=on_2977 on theBenchmark for (2977ds/483Mi) % 25.31/4.73 % (3881265)Instruction limit reached! % 25.31/4.73 % (3881265)------------------------------ % 25.31/4.73 % (3881265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.31/4.73 % (3881265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.31/4.73 % (3881265)CaDiCaL version: 2.1.3 % 25.31/4.73 % (3881265)Termination reason: Instruction limit % 25.31/4.73 % (3881265)Termination phase: Saturation % 25.31/4.73 % (3881265)Time elapsed: 0.196 s % 25.31/4.73 % (3881265)Peak memory usage: 91 MB % 25.31/4.73 % (3881265)Instructions burned: 175 (million) % 25.31/4.73 % (3881258)------------------------------ % 25.31/4.73 % (3881258)------------------------------ % 25.31/4.73 % (3881273)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=101105882:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi) % 25.31/4.73 % (3881275)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3456200303:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi) % 25.31/4.73 % (3881277)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4251126943:i=328:kws=inv_frequency:nm=20:rtra=on_2975 on theBenchmark for (2975ds/328Mi) % 25.31/4.73 % (3881271)Instruction limit reached! % 25.31/4.73 % (3881271)------------------------------ % 25.31/4.73 % (3881271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.31/4.73 % (3881271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.31/4.73 % (3881271)CaDiCaL version: 2.1.3 % 25.31/4.73 % (3881271)Termination reason: Instruction limit % 25.31/4.73 % (3881271)Termination phase: Saturation % 25.31/4.73 % (3881271)Time elapsed: 0.271 s % 25.31/4.73 % (3881271)Peak memory usage: 135 MB % 25.31/4.73 % (3881271)Instructions burned: 215 (million) % 25.31/4.73 % (3881278)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1966648279:i=281:gtgl=2:rtra=on:gtg=all_2974 on theBenchmark for (2974ds/281Mi) % 25.31/4.73 % (3881275)Instruction limit reached! % 25.31/4.73 % (3881275)------------------------------ % 25.31/4.73 % (3881275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.31/4.73 % (3881275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.31/4.73 % (3881275)CaDiCaL version: 2.1.3 % 25.31/4.73 % (3881275)Termination reason: Instruction limit % 25.31/4.73 % (3881275)Termination phase: Saturation % 25.31/4.73 % (3881275)Time elapsed: 0.158 s % 25.31/4.73 % (3881275)Peak memory usage: 92 MB % 25.31/4.73 % (3881275)Instructions burned: 296 (million) % 25.31/4.73 % (3881246)Instruction limit reached! % 25.31/4.73 % (3881246)------------------------------ % 25.31/4.73 % (3881246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.43/5.11 % (3881246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.43/5.11 % (3881246)CaDiCaL version: 2.1.3 % 29.43/5.11 % (3881246)Termination reason: Instruction limit % 29.43/5.11 % (3881246)Termination phase: Saturation % 29.43/5.11 % (3881246)Time elapsed: 1.023 s % 29.43/5.11 % (3881246)Peak memory usage: 97 MB % 29.43/5.11 % (3881246)Instructions burned: 1000 (million) % 29.43/5.11 % (3881284)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1022551962:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2972 on theBenchmark for (2972ds/321Mi) % 29.43/5.11 % (3881282)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2124124689:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi) % 29.43/5.11 % (3881273)Instruction limit reached! % 29.43/5.11 % (3881273)------------------------------ % 29.43/5.11 % (3881273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.43/5.11 % (3881273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.43/5.11 % (3881273)CaDiCaL version: 2.1.3 % 29.43/5.11 % (3881273)Termination reason: Instruction limit % 29.43/5.11 % (3881273)Termination phase: Saturation % 29.43/5.11 % (3881273)Time elapsed: 0.415 s % 29.43/5.11 % (3881273)Peak memory usage: 119 MB % 29.43/5.11 % (3881273)Instructions burned: 350 (million) % 29.43/5.11 % (3881270)Instruction limit reached! % 29.43/5.11 % (3881270)------------------------------ % 29.43/5.11 % (3881270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.43/5.11 % (3881270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.43/5.11 % (3881270)CaDiCaL version: 2.1.3 % 29.43/5.11 % (3881270)Termination reason: Instruction limit % 29.43/5.11 % (3881270)Termination phase: Saturation % 29.43/5.11 % (3881270)Time elapsed: 0.558 s % 29.43/5.11 % (3881270)Peak memory usage: 136 MB % 29.43/5.11 % (3881270)Instructions burned: 483 (million) % 29.43/5.11 % (3881285)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3524006777:i=416:rtra=on:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/416Mi) % 29.43/5.11 % (3881284)Instruction limit reached! % 29.43/5.11 % (3881284)------------------------------ % 29.43/5.11 % (3881284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.43/5.11 % (3881284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.43/5.11 % (3881284)CaDiCaL version: 2.1.3 % 29.43/5.11 % (3881284)Termination reason: Instruction limit % 29.43/5.11 % (3881284)Termination phase: Saturation % 29.43/5.11 % (3881284)Time elapsed: 0.144 s % 29.43/5.11 % (3881284)Peak memory usage: 113 MB % 29.43/5.11 % (3881284)Instructions burned: 321 (million) % 29.43/5.11 % (3881278)Instruction limit reached! % 29.43/5.11 % (3881278)------------------------------ % 29.43/5.11 % (3881278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.43/5.11 % (3881278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.43/5.11 % (3881278)CaDiCaL version: 2.1.3 % 29.43/5.11 % (3881278)Termination reason: Instruction limit % 29.43/5.11 % (3881278)Termination phase: Saturation % 29.43/5.11 % (3881278)Time elapsed: 0.337 s % 29.43/5.11 % (3881278)Peak memory usage: 118 MB % 29.43/5.11 % (3881278)Instructions burned: 281 (million) % 29.43/5.11 % (3881277)Instruction limit reached! % 29.43/5.11 % (3881277)------------------------------ % 29.43/5.11 % (3881277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.43/5.11 % (3881277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.43/5.11 % (3881277)CaDiCaL version: 2.1.3 % 29.43/5.11 % (3881277)Termination reason: Instruction limit % 29.43/5.11 % (3881277)Termination phase: Saturation % 29.43/5.11 % (3881277)Time elapsed: 0.389 s % 29.43/5.11 % (3881277)Peak memory usage: 118 MB % 29.43/5.11 % (3881277)Instructions burned: 328 (million) % 29.43/5.11 % (3881288)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3018574692:i=471:thf=on:kws=precedence:rtra=on_2970 on theBenchmark for (2970ds/471Mi) % 29.43/5.11 % (3881291)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1283723644:i=375:kws=inv_arity_squared:rtra=on_2969 on theBenchmark for (2969ds/375Mi) % 29.43/5.11 % (3881290)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=128881159:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 32.10/5.70 % (3881292)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4084568645:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi) % 32.10/5.70 % (3881293)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=137771111:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2969 on theBenchmark for (2969ds/513Mi) % 32.10/5.70 % (3881282)Instruction limit reached! % 32.10/5.70 % (3881282)------------------------------ % 32.10/5.70 % (3881282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.10/5.70 % (3881282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.10/5.70 % (3881282)CaDiCaL version: 2.1.3 % 32.10/5.70 % (3881282)Termination reason: Instruction limit % 32.10/5.70 % (3881282)Termination phase: Saturation % 32.10/5.70 % (3881282)Time elapsed: 0.434 s % 32.10/5.70 % (3881282)Peak memory usage: 91 MB % 32.10/5.70 % (3881282)Instructions burned: 485 (million) % 32.10/5.70 % (3881291)Instruction limit reached! % 32.10/5.70 % (3881291)------------------------------ % 32.10/5.70 % (3881291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.10/5.70 % (3881291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.10/5.70 % (3881291)CaDiCaL version: 2.1.3 % 32.10/5.70 % (3881291)Termination reason: Instruction limit % 32.10/5.70 % (3881291)Termination phase: Saturation % 32.10/5.70 % (3881291)Time elapsed: 0.224 s % 32.10/5.70 % (3881291)Peak memory usage: 118 MB % 32.10/5.70 % (3881291)Instructions burned: 376 (million) % 32.10/5.70 % (3881285)Instruction limit reached! % 32.10/5.70 % (3881285)------------------------------ % 32.10/5.70 % (3881285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.10/5.70 % (3881285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.10/5.70 % (3881285)CaDiCaL version: 2.1.3 % 32.10/5.70 % (3881285)Termination reason: Instruction limit % 32.10/5.70 % (3881285)Termination phase: Saturation % 32.10/5.70 % (3881285)Time elapsed: 0.459 s % 32.10/5.70 % (3881285)Peak memory usage: 122 MB % 32.10/5.70 % (3881285)Instructions burned: 416 (million) % 32.10/5.70 % (3881300)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2112993420:i=334:rtra=on_2966 on theBenchmark for (2966ds/334Mi) % 32.10/5.70 % (3881301)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2948576150:i=359:rtra=on:gtg=exists_top:ss=axioms_2965 on theBenchmark for (2965ds/359Mi) % 32.10/5.70 % (3881290)Instruction limit reached! % 32.10/5.70 % (3881290)------------------------------ % 32.10/5.70 % (3881290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.10/5.70 % (3881290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.10/5.70 % (3881290)CaDiCaL version: 2.1.3 % 32.10/5.70 % (3881290)Termination reason: Instruction limit % 32.10/5.70 % (3881290)Termination phase: Saturation % 32.10/5.70 % (3881290)Time elapsed: 0.373 s % 32.10/5.70 % (3881290)Peak memory usage: 136 MB % 32.10/5.70 % (3881290)Instructions burned: 276 (million) % 32.10/5.70 % (3881292)Instruction limit reached! % 32.10/5.70 % (3881292)------------------------------ % 32.10/5.70 % (3881292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.10/5.70 % (3881292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.10/5.70 % (3881292)CaDiCaL version: 2.1.3 % 32.10/5.70 % (3881292)Termination reason: Instruction limit % 32.10/5.70 % (3881292)Termination phase: Saturation % 32.10/5.70 % (3881292)Time elapsed: 0.376 s % 32.10/5.70 % (3881292)Peak memory usage: 119 MB % 32.10/5.70 % (3881292)Instructions burned: 387 (million) % 32.10/5.70 % (3881288)Instruction limit reached! % 32.10/5.70 % (3881288)------------------------------ % 32.10/5.70 % (3881288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.10/5.70 % (3881288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.10/5.70 % (3881288)CaDiCaL version: 2.1.3 % 32.10/5.70 % (3881288)Termination reason: Instruction limit % 32.10/5.70 % (3881288)Termination phase: Saturation % 32.10/5.70 % (3881288)Time elapsed: 0.524 s % 32.10/5.70 % (3881288)Peak memory usage: 119 MB % 32.10/5.70 % (3881288)Instructions burned: 471 (million) % 32.10/5.70 % (3881302)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2077771769:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2965 on theBenchmark for (2965ds/341Mi) % 32.10/5.70 % (3881301)Instruction limit reached! % 39.27/6.52 % (3881301)------------------------------ % 39.27/6.52 % (3881301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.27/6.52 % (3881301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.27/6.52 % (3881301)CaDiCaL version: 2.1.3 % 39.27/6.52 % (3881301)Termination reason: Instruction limit % 39.27/6.52 % (3881301)Termination phase: Saturation % 39.27/6.52 % (3881301)Time elapsed: 0.202 s % 39.27/6.52 % (3881301)Peak memory usage: 92 MB % 39.27/6.52 % (3881301)Instructions burned: 360 (million) % 39.27/6.52 % (3881305)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=109774799:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/261Mi) % 39.27/6.52 % (3881293)Instruction limit reached! % 39.27/6.52 % (3881293)------------------------------ % 39.27/6.52 % (3881293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.27/6.52 % (3881293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.27/6.52 % (3881293)CaDiCaL version: 2.1.3 % 39.27/6.52 % (3881293)Termination reason: Instruction limit % 39.27/6.52 % (3881293)Termination phase: Saturation % 39.27/6.52 % (3881293)Time elapsed: 0.541 s % 39.27/6.52 % (3881293)Peak memory usage: 94 MB % 39.27/6.52 % (3881293)Instructions burned: 513 (million) % 39.27/6.52 % (3881306)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=2495433658:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/235Mi) % 39.27/6.52 % (3881308)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=643590883:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 39.27/6.52 % (3881309)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3290790286:i=146:doe=on:rtra=on_2962 on theBenchmark for (2962ds/146Mi) % 39.27/6.52 % (3881300)Instruction limit reached! % 39.27/6.52 % (3881300)------------------------------ % 39.27/6.52 % (3881300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.27/6.52 % (3881300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.27/6.52 % (3881300)CaDiCaL version: 2.1.3 % 39.27/6.52 % (3881300)Termination reason: Instruction limit % 39.27/6.52 % (3881300)Termination phase: Saturation % 39.27/6.52 % (3881300)Time elapsed: 0.409 s % 39.27/6.52 % (3881300)Peak memory usage: 136 MB % 39.27/6.52 % (3881300)Instructions burned: 335 (million) % 39.27/6.52 % (3881309)Instruction limit reached! % 39.27/6.52 % (3881309)------------------------------ % 39.27/6.52 % (3881309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.27/6.52 % (3881309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.27/6.52 % (3881309)CaDiCaL version: 2.1.3 % 39.27/6.52 % (3881309)Termination reason: Instruction limit % 39.27/6.52 % (3881309)Termination phase: Saturation % 39.27/6.52 % (3881309)Time elapsed: 0.087 s % 39.27/6.52 % (3881309)Peak memory usage: 90 MB % 39.27/6.52 % (3881309)Instructions burned: 146 (million) % 39.27/6.52 % (3881311)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2242793629:i=4428:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/4428Mi) % 39.27/6.52 % (3881305)Instruction limit reached! % 39.27/6.52 % (3881305)------------------------------ % 39.27/6.52 % (3881305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.27/6.52 % (3881305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.27/6.52 % (3881305)CaDiCaL version: 2.1.3 % 39.27/6.52 % (3881305)Termination reason: Instruction limit % 39.27/6.52 % (3881305)Termination phase: Saturation % 39.27/6.52 % (3881305)Time elapsed: 0.269 s % 39.27/6.52 % (3881305)Peak memory usage: 118 MB % 39.27/6.52 % (3881305)Instructions burned: 261 (million) % 39.27/6.52 % (3881302)Instruction limit reached! % 39.27/6.52 % (3881302)------------------------------ % 39.27/6.52 % (3881302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.27/6.52 % (3881302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.27/6.52 % (3881302)CaDiCaL version: 2.1.3 % 39.27/6.52 % (3881302)Termination reason: Instruction limit % 39.27/6.52 % (3881302)Termination phase: Saturation % 39.27/6.52 % (3881302)Time elapsed: 0.421 s % 39.27/6.52 % (3881302)Peak memory usage: 120 MB % 39.27/6.52 % (3881302)Instructions burned: 341 (million) % 39.27/6.52 % (3881316)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4014523683:i=1052:rtra=on_2959 on theBenchmark for (2959ds/1052Mi) % 44.12/7.23 % (3881306)Instruction limit reached! % 44.12/7.23 % (3881306)------------------------------ % 44.12/7.23 % (3881306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.12/7.23 % (3881306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.12/7.23 % (3881306)CaDiCaL version: 2.1.3 % 44.12/7.23 % (3881306)Termination reason: Instruction limit % 44.12/7.23 % (3881306)Termination phase: Saturation % 44.12/7.23 % (3881306)Time elapsed: 0.296 s % 44.12/7.23 % (3881306)Peak memory usage: 119 MB % 44.12/7.23 % (3881306)Instructions burned: 235 (million) % 44.12/7.23 % (3881315)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=413581359:avsq=on:i=276:avsqr=1,2:rtra=on_2960 on theBenchmark for (2960ds/276Mi) % 44.12/7.23 % (3881308)Instruction limit reached! % 44.12/7.23 % (3881308)------------------------------ % 44.12/7.23 % (3881308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.12/7.23 % (3881308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.12/7.23 % (3881308)CaDiCaL version: 2.1.3 % 44.12/7.23 % (3881308)Termination reason: Instruction limit % 44.12/7.23 % (3881308)Termination phase: Saturation % 44.12/7.23 % (3881308)Time elapsed: 0.317 s % 44.12/7.23 % (3881308)Peak memory usage: 92 MB % 44.12/7.23 % (3881308)Instructions burned: 273 (million) % 44.12/7.23 % (3881319)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1187592471:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2958 on theBenchmark for (2958ds/1054Mi) % 44.12/7.23 % (3881318)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1803226675:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/655Mi) % 44.12/7.23 % (3881321)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=342352909:i=107:rtra=on_2958 on theBenchmark for (2958ds/107Mi) % 44.12/7.23 % (3881323)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4137852079:s2a=on:i=450:doe=on:nm=32:rtra=on_2957 on theBenchmark for (2957ds/450Mi) % 44.12/7.23 % (3881321)Instruction limit reached! % 44.12/7.23 % (3881321)------------------------------ % 44.12/7.23 % (3881321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.12/7.23 % (3881321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.12/7.23 % (3881321)CaDiCaL version: 2.1.3 % 44.12/7.23 % (3881321)Termination reason: Instruction limit % 44.12/7.23 % (3881321)Termination phase: Saturation % 44.12/7.23 % (3881321)Time elapsed: 0.143 s % 44.12/7.23 % (3881321)Peak memory usage: 117 MB % 44.12/7.23 % (3881321)Instructions burned: 108 (million) % 44.12/7.23 % (3881315)Instruction limit reached! % 44.12/7.23 % (3881315)------------------------------ % 44.12/7.23 % (3881315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.12/7.23 % (3881315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.12/7.23 % (3881315)CaDiCaL version: 2.1.3 % 44.12/7.23 % (3881315)Termination reason: Instruction limit % 44.12/7.23 % (3881315)Termination phase: Saturation % 44.12/7.23 % (3881315)Time elapsed: 0.371 s % 44.12/7.23 % (3881315)Peak memory usage: 135 MB % 44.12/7.23 % (3881315)Instructions burned: 276 (million) % 44.12/7.23 % (3881316)Instruction limit reached! % 44.12/7.23 % (3881316)------------------------------ % 44.12/7.23 % (3881316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.12/7.23 % (3881316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.12/7.23 % (3881316)CaDiCaL version: 2.1.3 % 44.12/7.23 % (3881316)Termination reason: Instruction limit % 44.12/7.23 % (3881316)Termination phase: Saturation % 44.12/7.23 % (3881316)Time elapsed: 0.579 s % 44.12/7.23 % (3881316)Peak memory usage: 97 MB % 44.12/7.23 % (3881316)Instructions burned: 1052 (million) % 44.12/7.23 % (3881328)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 % 44.12/7.23 % (3881328)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3037716053:i=1090:aac=none:nm=0:rtra=on:rawr=on_2954 on theBenchmark for (2954ds/1090Mi) % 47.46/7.83 % (3881329)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=199939171:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2954 on theBenchmark for (2954ds/130Mi) % 47.46/7.83 % (3881330)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3168011175:i=312:kws=inv_frequency:nm=20:rtra=on_2952 on theBenchmark for (2952ds/312Mi) % 47.46/7.83 % (3881323)Instruction limit reached! % 47.46/7.83 % (3881323)------------------------------ % 47.46/7.83 % (3881323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.46/7.83 % (3881323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.46/7.83 % (3881323)CaDiCaL version: 2.1.3 % 47.46/7.83 % (3881323)Termination reason: Instruction limit % 47.46/7.83 % (3881323)Termination phase: Saturation % 47.46/7.83 % (3881323)Time elapsed: 0.505 s % 47.46/7.83 % (3881323)Peak memory usage: 136 MB % 47.46/7.83 % (3881323)Instructions burned: 451 (million) % 47.46/7.83 % (3881329)Instruction limit reached! % 47.46/7.83 % (3881329)------------------------------ % 47.46/7.83 % (3881329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.46/7.83 % (3881329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.46/7.83 % (3881329)CaDiCaL version: 2.1.3 % 47.46/7.83 % (3881329)Termination reason: Instruction limit % 47.46/7.83 % (3881329)Termination phase: Saturation % 47.46/7.83 % (3881329)Time elapsed: 0.172 s % 47.46/7.83 % (3881329)Peak memory usage: 118 MB % 47.46/7.83 % (3881329)Instructions burned: 131 (million) % 47.46/7.83 % (3881318)Instruction limit reached! % 47.46/7.83 % (3881318)------------------------------ % 47.46/7.83 % (3881318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.46/7.83 % (3881318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.46/7.83 % (3881318)CaDiCaL version: 2.1.3 % 47.46/7.83 % (3881318)Termination reason: Instruction limit % 47.46/7.83 % (3881318)Termination phase: Saturation % 47.46/7.83 % (3881318)Time elapsed: 0.657 s % 47.46/7.83 % (3881318)Peak memory usage: 97 MB % 47.46/7.83 % (3881318)Instructions burned: 656 (million) % 47.46/7.83 % (3881330)Instruction limit reached! % 47.46/7.83 % (3881330)------------------------------ % 47.46/7.83 % (3881330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.46/7.83 % (3881330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.46/7.83 % (3881330)CaDiCaL version: 2.1.3 % 47.46/7.83 % (3881330)Termination reason: Instruction limit % 47.46/7.83 % (3881330)Termination phase: Saturation % 47.46/7.83 % (3881330)Time elapsed: 0.200 s % 47.46/7.83 % (3881330)Peak memory usage: 118 MB % 47.46/7.83 % (3881330)Instructions burned: 313 (million) % 47.46/7.83 % (3881345)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=346705997:i=491:doe=on:rtra=on:gtg=position_2950 on theBenchmark for (2950ds/491Mi) % 47.46/7.83 % (3881346)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=319373126:s2a=on:i=835:s2at=2:rtra=on_2950 on theBenchmark for (2950ds/835Mi) % 47.46/7.83 % (3881347)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=379683054:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2950 on theBenchmark for (2950ds/307Mi) % 47.46/7.83 % (3881353)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=483982105:i=776:doe=on:rtra=on_2948 on theBenchmark for (2948ds/776Mi) % 47.46/7.83 % (3881319)Instruction limit reached! % 47.46/7.83 % (3881319)------------------------------ % 47.46/7.83 % (3881319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.46/7.83 % (3881319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.46/7.83 % (3881319)CaDiCaL version: 2.1.3 % 47.46/7.83 % (3881319)Termination reason: Instruction limit % 47.46/7.83 % (3881319)Termination phase: Saturation % 47.46/7.83 % (3881319)Time elapsed: 1.101 s % 47.46/7.83 % (3881319)Peak memory usage: 97 MB % 47.46/7.83 % (3881319)Instructions burned: 1054 (million) % 47.46/7.83 % (3881347)Instruction limit reached! % 47.46/7.83 % (3881347)------------------------------ % 47.46/7.83 % (3881347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.46/7.83 % (3881347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.46/7.83 % (3881347)CaDiCaL version: 2.1.3 % 47.46/7.83 % (3881347)Termination reason: Instruction limit % 47.46/7.83 % (3881347)Termination phase: Saturation % 47.46/7.83 % (3881347)Time elapsed: 0.345 s % 47.46/7.83 % (3881347)Peak memory usage: 93 MB % 61.40/9.66 % (3881347)Instructions burned: 307 (million) % 61.40/9.66 % (3881358)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2761269329:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2945 on theBenchmark for (2945ds/646Mi) % 61.40/9.66 % (3881353)Instruction limit reached! % 61.40/9.66 % (3881353)------------------------------ % 61.40/9.66 % (3881353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.40/9.66 % (3881353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.40/9.66 % (3881353)CaDiCaL version: 2.1.3 % 61.40/9.66 % (3881353)Termination reason: Instruction limit % 61.40/9.66 % (3881353)Termination phase: Saturation % 61.40/9.66 % (3881353)Time elapsed: 0.409 s % 61.40/9.66 % (3881353)Peak memory usage: 124 MB % 61.40/9.66 % (3881353)Instructions burned: 778 (million) % 61.40/9.66 % (3881345)Instruction limit reached! % 61.40/9.66 % (3881345)------------------------------ % 61.40/9.66 % (3881345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.40/9.66 % (3881345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.40/9.66 % (3881345)CaDiCaL version: 2.1.3 % 61.40/9.66 % (3881345)Termination reason: Instruction limit % 61.40/9.66 % (3881345)Termination phase: Saturation % 61.40/9.66 % (3881345)Time elapsed: 0.521 s % 61.40/9.66 % (3881345)Peak memory usage: 93 MB % 61.40/9.66 % (3881345)Instructions burned: 491 (million) % 61.40/9.66 % (3881359)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=3282374153:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2944 on theBenchmark for (2944ds/784Mi) % 61.40/9.66 % (3881328)Instruction limit reached! % 61.40/9.66 % (3881328)------------------------------ % 61.40/9.66 % (3881328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.40/9.66 % (3881328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.40/9.66 % (3881328)CaDiCaL version: 2.1.3 % 61.40/9.66 % (3881328)Termination reason: Instruction limit % 61.40/9.66 % (3881328)Termination phase: Saturation % 61.40/9.66 % (3881328)Time elapsed: 1.070 s % 61.40/9.66 % (3881328)Peak memory usage: 123 MB % 61.40/9.66 % (3881328)Instructions burned: 1090 (million) % 61.40/9.66 % (3881361)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=4279643856:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2943 on theBenchmark for (2943ds/1131Mi) % 61.40/9.66 % (3881362)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=2920948752:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2942 on theBenchmark for (2942ds/246Mi) % 61.40/9.66 % (3881365)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1686650215:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/775Mi) % 61.40/9.66 % (3881346)Instruction limit reached! % 61.40/9.66 % (3881346)------------------------------ % 61.40/9.66 % (3881346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.40/9.66 % (3881346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.40/9.66 % (3881346)CaDiCaL version: 2.1.3 % 61.40/9.66 % (3881346)Termination reason: Instruction limit % 61.40/9.66 % (3881346)Termination phase: Saturation % 61.40/9.66 % (3881346)Time elapsed: 0.897 s % 61.40/9.66 % (3881346)Peak memory usage: 97 MB % 61.40/9.66 % (3881346)Instructions burned: 835 (million) % 61.40/9.66 % (3881362)Instruction limit reached! % 61.40/9.66 % (3881362)------------------------------ % 61.40/9.66 % (3881362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.40/9.66 % (3881362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.40/9.66 % (3881362)CaDiCaL version: 2.1.3 % 61.40/9.66 % (3881362)Termination reason: Instruction limit % 61.40/9.66 % (3881362)Termination phase: Saturation % 61.40/9.66 % (3881362)Time elapsed: 0.306 s % 61.40/9.66 % (3881362)Peak memory usage: 119 MB % 61.40/9.66 % (3881362)Instructions burned: 246 (million) % 61.40/9.66 % (3881358)Instruction limit reached! % 61.40/9.66 % (3881358)------------------------------ % 61.40/9.66 % (3881358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.40/9.66 % (3881358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.40/9.66 % (3881358)CaDiCaL version: 2.1.3 % 61.40/9.66 % (3881358)Termination reason: Instruction limit % 85.04/12.91 % (3881358)Termination phase: Saturation % 85.04/12.91 % (3881358)Time elapsed: 0.663 s % 85.04/12.91 % (3881358)Peak memory usage: 138 MB % 85.04/12.91 % (3881358)Instructions burned: 647 (million) % 85.04/12.91 % (3881368)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2522082734:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2938 on theBenchmark for (2938ds/273Mi) % 85.04/12.91 % (3881369)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2151822995:i=102:nm=16:rtra=on_2937 on theBenchmark for (2937ds/102Mi) % 85.04/12.91 % (3881361)Instruction limit reached! % 85.04/12.91 % (3881361)------------------------------ % 85.04/12.91 % (3881361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.04/12.91 % (3881361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.04/12.91 % (3881361)CaDiCaL version: 2.1.3 % 85.04/12.91 % (3881361)Termination reason: Instruction limit % 85.04/12.91 % (3881361)Termination phase: Saturation % 85.04/12.91 % (3881361)Time elapsed: 0.676 s % 85.04/12.91 % (3881361)Peak memory usage: 125 MB % 85.04/12.91 % (3881361)Instructions burned: 1132 (million) % 85.04/12.91 % (3881370)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3411630390:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2937 on theBenchmark for (2937ds/1094Mi) % 85.04/12.91 % (3881359)Instruction limit reached! % 85.04/12.91 % (3881359)------------------------------ % 85.04/12.91 % (3881359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.04/12.91 % (3881359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.04/12.91 % (3881359)CaDiCaL version: 2.1.3 % 85.04/12.91 % (3881359)Termination reason: Instruction limit % 85.04/12.91 % (3881359)Termination phase: Saturation % 85.04/12.91 % (3881359)Time elapsed: 0.766 s % 85.04/12.91 % (3881359)Peak memory usage: 119 MB % 85.04/12.91 % (3881359)Instructions burned: 784 (million) % 85.04/12.91 % (3881369)Instruction limit reached! % 85.04/12.91 % (3881369)------------------------------ % 85.04/12.91 % (3881369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.04/12.91 % (3881369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.04/12.91 % (3881369)CaDiCaL version: 2.1.3 % 85.04/12.91 % (3881369)Termination reason: Instruction limit % 85.04/12.91 % (3881369)Termination phase: Saturation % 85.04/12.91 % (3881369)Time elapsed: 0.110 s % 85.04/12.91 % (3881369)Peak memory usage: 89 MB % 85.04/12.91 % (3881369)Instructions burned: 102 (million) % 85.04/12.91 % (3881368)Instruction limit reached! % 85.04/12.91 % (3881368)------------------------------ % 85.04/12.91 % (3881368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.04/12.91 % (3881368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.04/12.91 % (3881368)CaDiCaL version: 2.1.3 % 85.04/12.91 % (3881368)Termination reason: Instruction limit % 85.04/12.91 % (3881368)Termination phase: Saturation % 85.04/12.91 % (3881368)Time elapsed: 0.316 s % 85.04/12.91 % (3881368)Peak memory usage: 92 MB % 85.04/12.91 % (3881368)Instructions burned: 273 (million) % 85.04/12.91 % (3881373)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2928535739:i=6400:doe=on:fsr=off:rtra=on_2935 on theBenchmark for (2935ds/6400Mi) % 85.04/12.91 % (3881376)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=3401101111:i=1846:canc=cautious:fsr=off:rtra=on_2934 on theBenchmark for (2934ds/1846Mi) % 85.04/12.91 % (3881375)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=545732257:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2934 on theBenchmark for (2934ds/868Mi) % 85.04/12.91 % (3881365)Instruction limit reached! % 85.04/12.91 % (3881365)------------------------------ % 85.04/12.91 % (3881365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.04/12.91 % (3881365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.04/12.91 % (3881365)CaDiCaL version: 2.1.3 % 85.04/12.91 % (3881365)Termination reason: Instruction limit % 85.04/12.91 % (3881365)Termination phase: Saturation % 85.04/12.91 % (3881365)Time elapsed: 0.794 s % 85.04/12.91 % (3881365)Peak memory usage: 96 MB % 85.04/12.91 % (3881365)Instructions burned: 776 (million) % 85.04/12.91 % (3881378)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1007633004:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2933 on theBenchmark for (2933ds/36816Mi) % 96.54/14.70 % (3881383)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3575269755:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2931 on theBenchmark for (2931ds/273Mi) % 96.54/14.70 % (3881383)Instruction limit reached! % 96.54/14.70 % (3881383)------------------------------ % 96.54/14.70 % (3881383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.54/14.70 % (3881383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.54/14.70 % (3881383)CaDiCaL version: 2.1.3 % 96.54/14.70 % (3881383)Termination reason: Instruction limit % 96.54/14.70 % (3881383)Termination phase: Saturation % 96.54/14.70 % (3881383)Time elapsed: 0.296 s % 96.54/14.70 % (3881383)Peak memory usage: 92 MB % 96.54/14.70 % (3881383)Instructions burned: 273 (million) % 96.54/14.70 % (3881390)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=412360503:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2926 on theBenchmark for (2926ds/863Mi) % 96.54/14.70 % (3881370)Instruction limit reached! % 96.54/14.70 % (3881370)------------------------------ % 96.54/14.70 % (3881370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.54/14.70 % (3881370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.54/14.70 % (3881370)CaDiCaL version: 2.1.3 % 96.54/14.70 % (3881370)Termination reason: Instruction limit % 96.54/14.70 % (3881370)Termination phase: Saturation % 96.54/14.70 % (3881370)Time elapsed: 1.095 s % 96.54/14.70 % (3881370)Peak memory usage: 95 MB % 96.54/14.70 % (3881370)Instructions burned: 1094 (million) % 96.54/14.70 % (3881375)Instruction limit reached! % 96.54/14.70 % (3881375)------------------------------ % 96.54/14.70 % (3881375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.54/14.70 % (3881375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.54/14.70 % (3881375)CaDiCaL version: 2.1.3 % 96.54/14.70 % (3881375)Termination reason: Instruction limit % 96.54/14.70 % (3881375)Termination phase: Saturation % 96.54/14.70 % (3881375)Time elapsed: 0.927 s % 96.54/14.70 % (3881375)Peak memory usage: 123 MB % 96.54/14.70 % (3881375)Instructions burned: 869 (million) % 96.54/14.70 % (3881394)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=38333426:i=5811:kws=precedence:nm=0:rtra=on_2923 on theBenchmark for (2923ds/5811Mi) % 96.54/14.70 % (3881399)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=683793734:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2922 on theBenchmark for (2922ds/2216Mi) % 96.54/14.70 % (3881376)Instruction limit reached! % 96.54/14.70 % (3881376)------------------------------ % 96.54/14.70 % (3881376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.54/14.70 % (3881376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.54/14.70 % (3881376)CaDiCaL version: 2.1.3 % 96.54/14.70 % (3881376)Termination reason: Instruction limit % 96.54/14.70 % (3881376)Termination phase: Saturation % 96.54/14.70 % (3881376)Time elapsed: 1.686 s % 96.54/14.70 % (3881376)Peak memory usage: 104 MB % 96.54/14.70 % (3881376)Instructions burned: 1846 (million) % 96.54/14.70 % (3881390)Instruction limit reached! % 96.54/14.70 % (3881390)------------------------------ % 96.54/14.70 % (3881390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.54/14.70 % (3881390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.54/14.70 % (3881390)CaDiCaL version: 2.1.3 % 96.54/14.70 % (3881390)Termination reason: Instruction limit % 96.54/14.70 % (3881390)Termination phase: Saturation % 96.54/14.70 % (3881390)Time elapsed: 0.925 s % 96.54/14.70 % (3881390)Peak memory usage: 122 MB % 96.54/14.70 % (3881390)Instructions burned: 863 (million) % 96.54/14.70 % (3881405)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2617213142:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2915 on theBenchmark for (2915ds/1026Mi) % 96.54/14.70 % (3881404)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2062424395:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2915 on theBenchmark for (2915ds/801Mi) % 96.54/14.70 % (3881311)Instruction limit reached! % 96.54/14.70 % (3881311)------------------------------ % 96.54/14.70 % (3881311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881311)CaDiCaL version: 2.1.3 % 154.05/22.65 % (3881311)Termination reason: Instruction limit % 154.05/22.65 % (3881311)Termination phase: Saturation % 154.05/22.65 % (3881311)Time elapsed: 4.618 s % 154.05/22.65 % (3881311)Peak memory usage: 118 MB % 154.05/22.65 % (3881311)Instructions burned: 4428 (million) % 154.05/22.65 % (3881408)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1404003960:i=3509:rtra=on_2912 on theBenchmark for (2912ds/3509Mi) % 154.05/22.65 % (3881404)Instruction limit reached! % 154.05/22.65 % (3881404)------------------------------ % 154.05/22.65 % (3881404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881404)CaDiCaL version: 2.1.3 % 154.05/22.65 % (3881404)Termination reason: Instruction limit % 154.05/22.65 % (3881404)Termination phase: Saturation % 154.05/22.65 % (3881404)Time elapsed: 0.797 s % 154.05/22.65 % (3881404)Peak memory usage: 97 MB % 154.05/22.65 % (3881404)Instructions burned: 801 (million) % 154.05/22.65 % (3881410)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2016845770:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2905 on theBenchmark for (2905ds/2127Mi) % 154.05/22.65 % (3881405)Instruction limit reached! % 154.05/22.65 % (3881405)------------------------------ % 154.05/22.65 % (3881405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881405)CaDiCaL version: 2.1.3 % 154.05/22.65 % (3881405)Termination reason: Instruction limit % 154.05/22.65 % (3881405)Termination phase: Saturation % 154.05/22.65 % (3881405)Time elapsed: 1.054 s % 154.05/22.65 % (3881405)Peak memory usage: 98 MB % 154.05/22.65 % (3881405)Instructions burned: 1027 (million) % 154.05/22.65 % (3881373)Instruction limit reached! % 154.05/22.65 % (3881373)------------------------------ % 154.05/22.65 % (3881373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881373)CaDiCaL version: 2.1.3 % 154.05/22.65 % (3881373)Termination reason: Instruction limit % 154.05/22.65 % (3881373)Termination phase: Saturation % 154.05/22.65 % (3881373)Time elapsed: 3.114 s % 154.05/22.65 % (3881373)Peak memory usage: 141 MB % 154.05/22.65 % (3881373)Instructions burned: 6401 (million) % 154.05/22.65 % (3881414)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2059049312:i=1959:rtra=on:fsd=on:proc=on_2902 on theBenchmark for (2902ds/1959Mi) % 154.05/22.65 % (3881415)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=831671613:s2a=on:i=3553:nm=0:rtra=on_2902 on theBenchmark for (2902ds/3553Mi) % 154.05/22.65 % (3881399)Instruction limit reached! % 154.05/22.65 % (3881399)------------------------------ % 154.05/22.65 % (3881399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881399)CaDiCaL version: 2.1.3 % 154.05/22.65 % (3881399)Termination reason: Instruction limit % 154.05/22.65 % (3881399)Termination phase: Saturation % 154.05/22.65 % (3881399)Time elapsed: 2.196 s % 154.05/22.65 % (3881399)Peak memory usage: 142 MB % 154.05/22.65 % (3881399)Instructions burned: 2216 (million) % 154.05/22.65 % (3881420)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1766290662:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2898 on theBenchmark for (2898ds/3201Mi) % 154.05/22.65 % (3881410)Instruction limit reached! % 154.05/22.65 % (3881410)------------------------------ % 154.05/22.65 % (3881410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881410)CaDiCaL version: 2.1.3 % 154.05/22.65 % (3881410)Termination reason: Instruction limit % 154.05/22.65 % (3881410)Termination phase: Saturation % 154.05/22.65 % (3881410)Time elapsed: 2.071 s % 154.05/22.65 % (3881410)Peak memory usage: 104 MB % 154.05/22.65 % (3881410)Instructions burned: 2127 (million) % 154.05/22.65 % (3881414)Instruction limit reached! % 154.05/22.65 % (3881414)------------------------------ % 154.05/22.65 % (3881414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.05/22.65 % (3881414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.65 % (3881414)CaDiCaL version: 2.1.3 % 183.77/26.85 % (3881414)Termination reason: Instruction limit % 183.77/26.85 % (3881414)Termination phase: Saturation % 183.77/26.85 % (3881414)Time elapsed: 2.031 s % 183.77/26.85 % (3881414)Peak memory usage: 127 MB % 183.77/26.85 % (3881414)Instructions burned: 1959 (million) % 183.77/26.85 % (3881426)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=1097044231:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2882 on theBenchmark for (2882ds/4093Mi) % 183.77/26.85 % (3881415)Instruction limit reached! % 183.77/26.85 % (3881415)------------------------------ % 183.77/26.85 % (3881415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.77/26.85 % (3881415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.77/26.85 % (3881415)CaDiCaL version: 2.1.3 % 183.77/26.85 % (3881415)Termination reason: Instruction limit % 183.77/26.85 % (3881415)Termination phase: Saturation % 183.77/26.85 % (3881415)Time elapsed: 2.046 s % 183.77/26.85 % (3881415)Peak memory usage: 109 MB % 183.77/26.85 % (3881415)Instructions burned: 3553 (million) % 183.77/26.85 % (3881431)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=350843810:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2880 on theBenchmark for (2880ds/21173Mi) % 183.77/26.85 % (3881433)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1242853168:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2879 on theBenchmark for (2879ds/10544Mi) % 183.77/26.85 % (3881408)Instruction limit reached! % 183.77/26.85 % (3881408)------------------------------ % 183.77/26.85 % (3881408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.77/26.85 % (3881408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.77/26.85 % (3881408)CaDiCaL version: 2.1.3 % 183.77/26.85 % (3881408)Termination reason: Instruction limit % 183.77/26.85 % (3881408)Termination phase: Saturation % 183.77/26.85 % (3881408)Time elapsed: 3.586 s % 183.77/26.85 % (3881408)Peak memory usage: 115 MB % 183.77/26.85 % (3881408)Instructions burned: 3509 (million) % 183.77/26.85 % (3881436)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3103822129:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2874 on theBenchmark for (2874ds/1262Mi) % 183.77/26.85 % (3881420)Instruction limit reached! % 183.77/26.85 % (3881420)------------------------------ % 183.77/26.85 % (3881420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.77/26.85 % (3881420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.77/26.85 % (3881420)CaDiCaL version: 2.1.3 % 183.77/26.85 % (3881420)Termination reason: Instruction limit % 183.77/26.85 % (3881420)Termination phase: Saturation % 183.77/26.85 % (3881420)Time elapsed: 2.877 s % 183.77/26.85 % (3881420)Peak memory usage: 124 MB % 183.77/26.85 % (3881420)Instructions burned: 3201 (million) % 183.77/26.85 % (3881394)Instruction limit reached! % 183.77/26.85 % (3881394)------------------------------ % 183.77/26.85 % (3881394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.77/26.85 % (3881394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.77/26.85 % (3881394)CaDiCaL version: 2.1.3 % 183.77/26.85 % (3881394)Termination reason: Instruction limit % 183.77/26.85 % (3881394)Termination phase: Saturation % 183.77/26.85 % (3881394)Time elapsed: 5.464 s % 183.77/26.85 % (3881394)Peak memory usage: 130 MB % 183.77/26.85 % (3881394)Instructions burned: 5812 (million) % 183.77/26.85 % (3881440)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3945883447:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2868 on theBenchmark for (2868ds/775Mi) % 183.77/26.85 % (3881441)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3990448578:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2866 on theBenchmark for (2866ds/270Mi) % 183.77/26.85 % (3881441)Instruction limit reached! % 183.77/26.85 % (3881441)------------------------------ % 183.77/26.85 % (3881441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.77/26.85 % (3881441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.77/26.85 % (3881441)CaDiCaL version: 2.1.3 % 183.77/26.85 % (3881441)Termination reason: Instruction limit % 183.77/26.85 % (3881441)Termination phase: Saturation % 183.77/26.85 % (3881441)Time elapsed: 0.273 s % 209.64/30.51 % (3881441)Peak memory usage: 92 MB % 209.64/30.51 % (3881441)Instructions burned: 271 (million) % 209.64/30.51 % (3881436)Instruction limit reached! % 209.64/30.51 % (3881436)------------------------------ % 209.64/30.51 % (3881436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.64/30.51 % (3881436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.64/30.51 % (3881436)CaDiCaL version: 2.1.3 % 209.64/30.51 % (3881436)Termination reason: Instruction limit % 209.64/30.51 % (3881436)Termination phase: Saturation % 209.64/30.51 % (3881436)Time elapsed: 1.114 s % 209.64/30.51 % (3881436)Peak memory usage: 120 MB % 209.64/30.51 % (3881436)Instructions burned: 1263 (million) % 209.64/30.51 % (3881452)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1605002562:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2862 on theBenchmark for (2862ds/17165Mi) % 209.64/30.51 % (3881453)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1229163678:s2a=on:i=13094:s2at=-1:rtra=on_2861 on theBenchmark for (2861ds/13094Mi) % 209.64/30.51 % (3881440)Instruction limit reached! % 209.64/30.51 % (3881440)------------------------------ % 209.64/30.51 % (3881440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.64/30.51 % (3881440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.64/30.51 % (3881440)CaDiCaL version: 2.1.3 % 209.64/30.51 % (3881440)Termination reason: Instruction limit % 209.64/30.51 % (3881440)Termination phase: Saturation % 209.64/30.51 % (3881440)Time elapsed: 0.824 s % 209.64/30.51 % (3881440)Peak memory usage: 96 MB % 209.64/30.51 % (3881440)Instructions burned: 775 (million) % 209.64/30.51 % (3881456)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3734686384:st=2:i=12633:rtra=on:ss=axioms_2857 on theBenchmark for (2857ds/12633Mi) % 209.64/30.51 % (3881426)Instruction limit reached! % 209.64/30.51 % (3881426)------------------------------ % 209.64/30.51 % (3881426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.64/30.51 % (3881426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.64/30.51 % (3881426)CaDiCaL version: 2.1.3 % 209.64/30.51 % (3881426)Termination reason: Instruction limit % 209.64/30.51 % (3881426)Termination phase: Saturation % 209.64/30.51 % (3881426)Time elapsed: 4.054 s % 209.64/30.51 % (3881426)Peak memory usage: 143 MB % 209.64/30.51 % (3881426)Instructions burned: 4093 (million) % 209.64/30.51 % (3881458)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1075994951:i=1783:rtra=on:gtg=position_2839 on theBenchmark for (2839ds/1783Mi) % 209.64/30.51 % (3881433)Instruction limit reached! % 209.64/30.51 % (3881433)------------------------------ % 209.64/30.51 % (3881433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.64/30.51 % (3881433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.64/30.51 % (3881433)CaDiCaL version: 2.1.3 % 209.64/30.51 % (3881433)Termination reason: Instruction limit % 209.64/30.51 % (3881433)Termination phase: Saturation % 209.64/30.51 % (3881433)Time elapsed: 4.524 s % 209.64/30.51 % (3881433)Peak memory usage: 142 MB % 209.64/30.51 % (3881433)Instructions burned: 10545 (million) % 209.64/30.51 % (3881460)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=1743257524:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2833 on theBenchmark for (2833ds/5451Mi) % 209.64/30.51 % (3881458)Instruction limit reached! % 209.64/30.51 % (3881458)------------------------------ % 209.64/30.51 % (3881458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.64/30.51 % (3881458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.64/30.51 % (3881458)CaDiCaL version: 2.1.3 % 209.64/30.51 % (3881458)Termination reason: Instruction limit % 209.64/30.51 % (3881458)Termination phase: Saturation % 209.64/30.51 % (3881458)Time elapsed: 1.745 s % 209.64/30.51 % (3881458)Peak memory usage: 123 MB % 209.64/30.51 % (3881458)Instructions burned: 1783 (million) % 209.64/30.51 % (3881462)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=1136328210:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2819 on theBenchmark for (2819ds/4975Mi) % 209.64/30.51 % (3881460)Instruction limit reached! % 209.64/30.51 % (3881460)------------------------------ % 209.64/30.51 % (3881460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.64/30.51 % (3881460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.33/38.19 % (3881460)CaDiCaL version: 2.1.3 % 264.33/38.19 % (3881460)Termination reason: Instruction limit % 264.33/38.19 % (3881460)Termination phase: Saturation % 264.33/38.19 % (3881460)Time elapsed: 4.829 s % 264.33/38.19 % (3881460)Peak memory usage: 126 MB % 264.33/38.19 % (3881460)Instructions burned: 5452 (million) % 264.33/38.19 % (3881453)Instruction limit reached! % 264.33/38.19 % (3881453)------------------------------ % 264.33/38.19 % (3881453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.33/38.19 % (3881453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.33/38.19 % (3881453)CaDiCaL version: 2.1.3 % 264.33/38.19 % (3881453)Termination reason: Instruction limit % 264.33/38.19 % (3881453)Termination phase: Saturation % 264.33/38.19 % (3881453)Time elapsed: 7.830 s % 264.33/38.19 % (3881453)Peak memory usage: 149 MB % 264.33/38.19 % (3881453)Instructions burned: 13096 (million) % 264.33/38.19 % (3881472)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=928572993:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2783 on theBenchmark for (2783ds/2076Mi) % 264.33/38.19 % (3881473)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4181925119:i=5145:rtra=on_2781 on theBenchmark for (2781ds/5145Mi) % 264.33/38.19 % (3881462)Instruction limit reached! % 264.33/38.19 % (3881462)------------------------------ % 264.33/38.19 % (3881462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.33/38.19 % (3881462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.33/38.19 % (3881462)CaDiCaL version: 2.1.3 % 264.33/38.19 % (3881462)Termination reason: Instruction limit % 264.33/38.19 % (3881462)Termination phase: Saturation % 264.33/38.19 % (3881462)Time elapsed: 4.308 s % 264.33/38.19 % (3881462)Peak memory usage: 127 MB % 264.33/38.19 % (3881462)Instructions burned: 4976 (million) % 264.33/38.19 % (3881478)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=150639109:i=3509:rtra=on_2774 on theBenchmark for (2774ds/3509Mi) % 264.33/38.19 % (3881472)Instruction limit reached! % 264.33/38.19 % (3881472)------------------------------ % 264.33/38.19 % (3881472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.33/38.19 % (3881472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.33/38.19 % (3881472)CaDiCaL version: 2.1.3 % 264.33/38.19 % (3881472)Termination reason: Instruction limit % 264.33/38.19 % (3881472)Termination phase: Saturation % 264.33/38.19 % (3881472)Time elapsed: 2.156 s % 264.33/38.19 % (3881472)Peak memory usage: 141 MB % 264.33/38.19 % (3881472)Instructions burned: 2076 (million) % 264.33/38.19 % (3881480)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3451498151:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2759 on theBenchmark for (2759ds/13800Mi) % 264.33/38.19 % (3881473)Instruction limit reached! % 264.33/38.19 % (3881473)------------------------------ % 264.33/38.19 % (3881473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.33/38.19 % (3881473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.33/38.19 % (3881473)CaDiCaL version: 2.1.3 % 264.33/38.19 % (3881473)Termination reason: Instruction limit % 264.33/38.19 % (3881473)Termination phase: Saturation % 264.33/38.19 % (3881473)Time elapsed: 2.707 s % 264.33/38.19 % (3881473)Peak memory usage: 123 MB % 264.33/38.19 % (3881473)Instructions burned: 5146 (million) % 264.33/38.19 % (3881482)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2028971298:i=1412:rtra=on:fsd=on:proc=on_2752 on theBenchmark for (2752ds/1412Mi) % 264.33/38.19 % (3881482)Instruction limit reached! % 264.33/38.19 % (3881482)------------------------------ % 264.33/38.19 % (3881482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.33/38.19 % (3881482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.33/38.19 % (3881482)CaDiCaL version: 2.1.3 % 264.33/38.19 % (3881482)Termination reason: Instruction limit % 264.33/38.19 % (3881482)Termination phase: Saturation % 264.33/38.19 % (3881482)Time elapsed: 0.833 s % 264.33/38.19 % (3881482)Peak memory usage: 126 MB % 264.33/38.19 % (3881482)Instructions burned: 1412 (million) % 264.33/38.19 % (3881484)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 % 264.33/38.19 % (3881484)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=Terminated %------------------------------------------------------------------------------